Simplify InsertionSort.lean even more, archive older version

Changes

2 changed files (+83/-46)

• InsertionSort.lean
  • @@ -1,59 +1,37 @@
    - -- Simplified version of https://jamesoswald.dev/posts/lean4-insertion-sort/ - -- Also inspired by https://gist.github.com/Kha/96d67c8b947b48f8786aea90857fbb5c + variable [LE α] [DecidableLE α] [Std.IsLinearOrder α] [BEq α] [LawfulBEq α] (xs : List α) - 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 + def insert (a : α) + | [] => [a] + | x :: xs => + if a ≤ x then + a :: x :: xs else - h :: sInsert n t + x :: insert a xs - /-- Insertion sort -/ @[grind] - def sort : List α → List α + def insertionSort : List α → List α | [] => [] - | h :: t => sInsert h (sort t) + | x :: xs => insert x (insertionSort xs) - /-- 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. - | h1 :: h2 :: t => h1 ≤ h2 ∧ sorted (h2 :: 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) + 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) -/ - 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 + theorem insertCorrect x : (Sorted xs → Sorted (insert x xs)) ∧ (x :: xs).Perm (insert x xs) := by + induction xs with | nil => grind - | cons _ t1 => cases t1 <;> 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 + | cons _ t => cases t <;> grind - /-- `sort` returns a permutation of the input list. -/ - theorem sort_perm [BEq α] [LawfulBEq α] : l.Perm (sort l) := by - induction l with + theorem insertionSortCorrect : Sorted (insertionSort xs) ∧ xs.Perm (insertionSort xs) := by + induction xs with | nil => grind - | cons h t => grind [sInsert_perm (sort t) (n := h)] + | cons h t => grind [insertCorrect (insertionSort t) h]
• InsertionSortOld.lean (new)
  • @@ -0,0 +1,59 @@
    + -- 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)]