GRRRRIIIINNNDDD

Changes

1 changed files (+48/-0)

• InsertionSort.lean (new)
  • @@ -0,0 +1,48 @@
    + -- Simplified version of https://jamesoswald.dev/posts/lean4-insertion-sort/ + -- Also inspired by https://gist.github.com/Kha/96d67c8b947b48f8786aea90857fbb5c + + /-- Inserts a natural number n into a sorted list. -/ + @[grind] + def sInsert (n : Nat) : List Nat → List Nat + | [] => [n] + | h :: t => + if n ≤ h then + n :: h :: t + else + h :: sInsert n t + + /-- Insertion sort -/ + @[grind] + def sort : List Nat → List Nat + | [] => [] + | h :: t => sInsert h (sort t) + + /-- Predicate for a list being sorted -/ + @[grind] + def sorted : List Nat → Prop + -- An empty list is sorted + | [] => True + -- A list containing a single element is sorted + | [_] => True + -- A list with more than 2 elements is only sorted if all elements are ordered. + | h1 :: h2 :: t => h1 ≤ h2 ∧ sorted (h2 :: t) + + /-- If a sorted list is passed to sInsert, + it will return a sorted list after inserting a new elm. -/ + theorem sInsert_sorted (l : List Nat) (n : Nat) : sorted l → sorted (sInsert n l) := by + induction l with + | nil => grind + | cons _ t1 => cases t1 <;> grind + + theorem sort_sorted (l : List Nat) : 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. -/ + theorem sInsert_perm (l : List Nat) (n : Nat) : (n :: l).Perm (sInsert n l) := by + induction l <;> grind + + /-- Sort returns a permutation of the input list. -/ + theorem sort_perm (l : List Nat) : l.Perm (sort l) := by + induction l with + | nil => simp [sort] + | cons h t ih => grind [sInsert_perm (sort t) h]