Changes

5 changed files (+2/-120)

• InsertionSort.lean (deleted)
  • @@ -1,37 +0,0 @@
    - variable [LE α] [DecidableLE α] [Std.IsLinearOrder α] [BEq α] [LawfulBEq α] (xs : List α) - - @[grind] - def insert (a : α) - | [] => [a] - | x :: xs => - if a ≤ x then - a :: x :: xs - else - x :: insert a xs - - @[grind] - def insertionSort : List α → List α - | [] => [] - | x :: xs => insert x (insertionSort xs) - - @[grind] - def Sorted : List α → Prop - | [] | [_] => True - | x :: x' :: xs => x ≤ x' ∧ Sorted (x' :: xs) - /- - This also works: - inductive Sorted : List α → Prop where - | nil : Sorted [] - | single x : Sorted [x] - | cons_cons x x' xs : x ≤ x' → Sorted (x' :: xs) → Sorted (x :: x' :: xs) - -/ - - theorem insertCorrect x : (Sorted xs → Sorted (insert x xs)) ∧ (x :: xs).Perm (insert x xs) := by - induction xs with - | nil => grind - | cons _ t => cases t <;> grind - - theorem insertionSortCorrect : Sorted (insertionSort xs) ∧ xs.Perm (insertionSort xs) := by - induction xs with - | nil => grind - | cons h t => grind [insertCorrect (insertionSort t) h]
• InsertionSortGolf.lean (deleted)
  • @@ -1,21 +0,0 @@
    - variable[LE α][DecidableLE α][Std.IsLinearOrder α][BEq α][LawfulBEq α](l:List α) - - @[grind]def I(n:α) - |[]=>[n] - |h::t=>ite (n≤h) (n::h::t) (h::I n t) - - @[grind]def S:List α→List α - |[]=>[] - |h::t=>I h<|S t - - @[grind]def D:List α→Prop - |[]|[_]=>True - |h::h'::t=>h≤h'∧D (h'::t) - - theorem A:(D l→D (I n l))∧(n::l).Perm (I n l):=by induction l with - |nil=>grind - |cons _ t=>cases t<;>grind - - example:D (S l)∧l.Perm (S l):=by induction l with - |nil=>grind - |cons h t=>grind[A (n:=h)<|S t]
• InsertionSortOld.lean (deleted)
  • @@ -1,59 +0,0 @@
    - -- Simplified version of https://jamesoswald.dev/posts/lean4-insertion-sort/ - -- Also inspired by https://gist.github.com/Kha/96d67c8b947b48f8786aea90857fbb5c - - variable [LE α] [DecidableLE α] - - /-- Inserts an element n into a sorted list. -/ - @[grind] - def sInsert (n : α) : List α → List α - | [] => [n] - | h :: t => - if n ≤ h then - n :: h :: t - else - h :: sInsert n t - - /-- Insertion sort -/ - @[grind] - def sort : List α → List α - | [] => [] - | h :: t => sInsert h (sort t) - - /-- Predicate for a list being sorted -/ - @[grind] - def sorted : List α → Prop - -- An empty list is sorted - | [] => True - -- A list containing a single element is sorted - | [_] => True - -- A list with 2 or more elements is only sorted if all elements are ordered. - | h :: h' :: t => h ≤ h' ∧ sorted (h' :: t) - /- This also works: - inductive sorted : List α → Prop where - | nil : sorted [] - | single x : sorted [x] - | cons_cons x x' xs : x ≤ x' → sorted (x' :: xs) → sorted (x :: x' :: xs) - -/ - - variable (l : List α) - - /-- If a sorted list is passed to `sInsert`, - it will return a sorted list after inserting a new element. -/ - theorem sInsert_sorted [Std.IsLinearOrder α] : sorted l → sorted (sInsert n l) := by - induction l with - | nil => grind - | cons _ t => cases t <;> grind - - theorem sort_sorted [Std.IsLinearOrder α] : sorted (sort l) := by - induction l <;> grind [sInsert_sorted] - - /-- A list l with n is a permutation of a list the list with n inserted into it. - We need `LawfulBEq` because grind uses it via `List.perm_iff_count`. -/ - theorem sInsert_perm [BEq α] [LawfulBEq α] : (n :: l).Perm (sInsert n l) := by - induction l <;> grind - - /-- `sort` returns a permutation of the input list. -/ - theorem sort_perm [BEq α] [LawfulBEq α] : l.Perm (sort l) := by - induction l with - | nil => grind - | cons h t => grind [sInsert_perm (sort t) (n := h)]
• InsertionSortSupergolf.lean (deleted)
  • @@ -1,1 +0,0 @@
    - variable[LE α][DecidableLE α][Std.IsLinearOrder α][BEq α][LawfulBEq α](l:List α)@[grind]def I(n:α)|[]=>[n]|h::t=>ite (n≤h) (n::h::t) (h::I n t)@[grind]def S:List α→List α|[]=>[]|h::t=>I h<|S t@[grind]def D:List α→Prop|[]|[_]=>True|h::h'::t=>h≤h'∧D (h'::t)theorem A(n):(D l→D (I n l))∧(n::l).Perm (I n l):=by induction l with|nil=>grind|cons _ t=>cases t<;>grind example:D (S l)∧l.Perm (S l):=by induction l with|nil=>grind|cons h t=>grind[A (S t) h]
• Sort.lean
  • @@ -23,8 +23,8 @@ theorem perm : ICan'tBelieveItCanSort A |>.Perm A := by
    generalize h : ICan'tBelieveItCanSort A = x apply Id.of_wp_run_eq h mvcgen invariants - · ⇓⟨_, A'⟩ => ⌜Array.Perm A A'.toArray⌝ - · ⇓⟨_, A'⟩ => ⌜Array.Perm A A'.toArray⌝ + · ⇓⟨_, A'⟩ => ⌜A.Perm A'.toArray⌝ + · ⇓⟨_, A'⟩ => ⌜A.Perm A'.toArray⌝ with grind [Array.Perm.trans, Array.Perm.symm, Array.swap_perm] theorem sorted : ICan'tBelieveItCanSort A |>.Pairwise (· ≤ ·) := by