Make InsertionSort generic, use inductive predicate instead of def

Changes

1 changed files (+23/-18)

• InsertionSort.lean
  • @@ -1,9 +1,11 @@
    -- 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. -/ + variable [LE α] [DecidableLE α] + + /-- Inserts an element n into a sorted list. -/ @[grind] - def sInsert (n : Nat) : List Nat → List Nat + def sInsert (n : α) : List α → List α | [] => [n] | h :: t => if n ≤ h then
  • @@ -13,36 +15,39 @@ def sInsert (n : Nat) : List Nat → List Nat
    /-- Insertion sort -/ @[grind] - def sort : List Nat → List Nat + def sort : List α → List α | [] => [] | h :: t => sInsert h (sort t) - /-- Predicate for a list being sorted -/ + /-- Inductive predicate for a list being sorted -/ @[grind] - def sorted : List Nat → Prop + inductive sorted : List α → Prop where -- An empty list is sorted - | [] => True + | nil : sorted [] -- A list containing a single element is sorted - | [_] => True + | single x : sorted [x] -- A list with more than 2 elements is only sorted if all elements are ordered. - | h1 :: h2 :: t => h1 ≤ h2 ∧ sorted (h2 :: t) + | 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 elm. -/ - theorem sInsert_sorted (l : List Nat) (n : Nat) : sorted l → sorted (sInsert n l) := by + /-- 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 _ t1 => cases t1 <;> grind - theorem sort_sorted (l : List Nat) : sorted (sort l) := by + 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. -/ - theorem sInsert_perm (l : List Nat) (n : Nat) : (n :: l).Perm (sInsert n l) := by + /-- 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 (l : List Nat) : l.Perm (sort l) := by + /-- `sort` returns a permutation of the input list. -/ + theorem sort_perm [BEq α] [LawfulBEq α] : l.Perm (sort l) := by induction l with - | nil => simp [sort] - | cons h t ih => grind [sInsert_perm (sort t) h] + | nil => grind + | cons h t => grind [sInsert_perm (sort t) (n := h)]