Last active
January 23, 2026 01:59
-
-
Save bhargavkulk/a43b17e7ff25125e837bbdcebcc180cc to your computer and use it in GitHub Desktop.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| namespace NatList | |
| -- We define the set of NatLists: | |
| -- 1. nil is a NatList | |
| -- 2. If head is a Nat and tail is NatList | |
| -- then head :: tail is a NatList | |
| inductive NatList: Type | |
| | nil: NatList | |
| | cons (head : Nat) (tail : NatList) : NatList | |
| open NatList | |
| infixr:67 " :: " => cons | |
| notation "[]" => nil | |
| #check 1 :: 2 :: 3 :: [] | |
| -- Lean 4: 1 :: 2 :: 3 :: [] : NatList | |
| def length (l: NatList) : Nat := | |
| match l with | |
| | [] => 0 | |
| | _ :: t => 1 + (length t) | |
| def append (l1 : NatList) (l2 : NatList) : NatList := | |
| match l1 with | |
| | [] => l2 | |
| | h :: t => h :: (append t l2) | |
| infixr:67 " ++ " => NatList.append | |
| theorem append_length: forall l1 l2, | |
| length (l1 ++ l2) = length l1 + length l2 := | |
| by | |
| sorry | |
| -- Time to prove something non-trivial: | |
| def insert (n : Nat) (l : NatList) : NatList := | |
| match l with | |
| | [] => n :: [] | |
| | h :: t => if decide (n <= h) | |
| then n :: h :: t | |
| else h :: insert n t | |
| def insertion_sort (l : NatList) : NatList := | |
| match l with | |
| | [] => [] | |
| | h :: t => insert h (insertion_sort t) | |
| example: | |
| insertion_sort (5 :: 4 :: 3 :: 2 :: 1 :: []) = 1 :: 2 :: 3 :: 4 :: 5 :: [] := | |
| by | |
| -- unfold sort | |
| simp [insertion_sort] | |
| -- unfold insert | |
| simp [insert] | |
| inductive Sorted : NatList -> Prop | |
| | nil : Sorted nil | |
| | lone : forall (n : Nat), Sorted (n :: []) | |
| | cons : forall x y l, x <= y -> Sorted (y :: l) -> Sorted (x :: y :: l) | |
| -- use `of_decide_eq_false` and `of_decide_eq_true` to turn | |
| -- decide (x <= y) = false/true into propositions. | |
| theorem insert_Sorted : forall n l, | |
| Sorted l -> Sorted (insert n l) := | |
| by | |
| intro n l Hsorted | |
| induction Hsorted with | |
| | nil => | |
| sorry | |
| | lone n' => | |
| sorry | |
| | cons x y l Hle Hsorted IH => | |
| sorry | |
| theorem insertion_sort_sorted: forall l, | |
| Sorted (insertion_sort l) := | |
| by | |
| intro l | |
| induction l with | |
| | nil => | |
| apply Sorted.nil | |
| | cons h t IHt => | |
| dsimp [insertion_sort] | |
| apply insert_Sorted | |
| assumption | |
| -- A bad sort | |
| def bad_sort(_ : NatList): NatList := [] | |
| theorem bad_sort_sorted: forall l, | |
| Sorted (bad_sort l) := | |
| by | |
| intro l | |
| simp [bad_sort] | |
| apply Sorted.nil | |
| -- clearly `bad_sort` is not a sorting algorithm | |
| -- Sorted is not the only spec required to prove an algorithm is sorted | |
| -- You also need to show that sorted(list) and list are permutations | |
| inductive Permutation : NatList -> NatList -> Prop | |
| | nil : Permutation [] [] | |
| | skip : forall (x : Nat) (l l' : NatList), | |
| Permutation l l' -> | |
| Permutation (x :: l) (x :: l') | |
| | swap : forall (x y : Nat) (l : NatList), | |
| Permutation (y :: x :: l) (x :: y :: l) | |
| | trans : forall (l l' l'' : NatList), | |
| Permutation l l' -> | |
| Permutation l' l'' -> | |
| Permutation l l'' | |
| theorem Permutations_are_equal: forall l1 l2, | |
| l1 = l2 -> Permutation l1 l2 := | |
| by | |
| sorry | |
| theorem insert_is_Permutation: forall x l, | |
| Permutation (x :: l) (insert x l) := | |
| by | |
| sorry | |
| theorem sort_is_Permutation: forall l, | |
| Permutation l (insertion_sort l) := | |
| by | |
| sorry | |
| theorem bad_sort_is_not_Permutation: | |
| ¬ (forall l, Permutation l (bad_sort l)) := | |
| by | |
| sorry | |
| end NatList |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment