Skip to content

Commit e54ec5f

Browse files
Shreyas4991Shreyas4991
committed
Big PR
1 parent 83f543e commit e54ec5f

14 files changed

Lines changed: 1065 additions & 7 deletions

File tree

‎Cslib.lean‎

Lines changed: 9 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,14 @@
11
module -- shake: keep-all
22

3-
public import Cslib.Algorithms.Lean.MergeSort.MergeSort
4-
public import Cslib.Algorithms.Lean.TimeM
3+
public import Cslib.AlgorithmsTheory.Algorithms.ListInsertionSort
4+
public import Cslib.AlgorithmsTheory.Algorithms.ListLinearSearch
5+
public import Cslib.AlgorithmsTheory.Algorithms.ListOrderedInsert
6+
public import Cslib.AlgorithmsTheory.Algorithms.MergeSort
7+
public import Cslib.AlgorithmsTheory.Lean.MergeSort.MergeSort
8+
public import Cslib.AlgorithmsTheory.Lean.TimeM
9+
public import Cslib.AlgorithmsTheory.Models.ListComparisonSearch
10+
public import Cslib.AlgorithmsTheory.Models.ListComparisonSort
11+
public import Cslib.AlgorithmsTheory.QueryModel
512
public import Cslib.Computability.Automata.Acceptors.Acceptor
613
public import Cslib.Computability.Automata.Acceptors.OmegaAcceptor
714
public import Cslib.Computability.Automata.DA.Basic

‎Cslib/AlgorithmsTheory/Algorithms/ListInsertionSort.lean‎

Lines changed: 100 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,100 @@
1+
/-
2+
Copyright (c) 2026 Shreyas Srinivas. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Shreyas Srinivas, Eric Wieser
5+
-/
6+
module
7+
8+
public import Cslib.AlgorithmsTheory.QueryModel
9+
public import Cslib.AlgorithmsTheory.Algorithms.ListOrderedInsert
10+
public import Mathlib
11+
12+
@[expose] public section
13+
14+
/-!
15+
# Insertion sort in a list
16+
17+
In this file we state and prove the correctness and complexity of insertion sort in lists under
18+
the `SortOps` model. This insertionSort evaluates identically to the upstream version of
19+
`List.insertionSort`
20+
--
21+
22+
## Main Definitions
23+
24+
- `insertionSort` : Insertion sort algorithm in the `SortOps` query model
25+
26+
## Main results
27+
28+
- `insertionSort_eval`: `insertionSort` evaluates identically to `List.insertionSort`.
29+
- `insertionSort_permutation` : `insertionSort` outputs a permutation of the input list.
30+
- `insertionSort_sorted` : `insertionSort` outputs a sorted list.
31+
- `insertionSort_complexity` : `insertionSort` takes at most n * (n + 1) comparisons and
32+
(n + 1) * (n + 2) list head-insertions.
33+
-/
34+
35+
namespace Cslib
36+
37+
namespace Algorithms
38+
39+
open Prog
40+
41+
/-- The insertionSort algorithms on lists with the `SortOps` query. -/
42+
def insertionSort (l : List α) : Prog (SortOps α) (List α) :=
43+
match l with
44+
| [] => return []
45+
| x :: xs => do
46+
let rest ← insertionSort xs
47+
insertOrd x rest
48+
49+
@[simp]
50+
theorem insertionSort_eval (l : List α) (le : α → α → Prop) [DecidableRel le] :
51+
(insertionSort l).eval (sortModel le) = l.insertionSort le := by
52+
induction l with simp_all [insertionSort]
53+
54+
theorem insertionSort_permutation (l : List α) (le : α → α → Prop) [DecidableRel le] :
55+
((insertionSort l).eval (sortModel le)).Perm l := by
56+
simp [insertionSort_eval, List.perm_insertionSort]
57+
58+
theorem insertionSort_sorted
59+
(l : List α) (le : α → α → Prop) [DecidableRel le] [Std.Total le] [IsTrans α le] :
60+
((insertionSort l).eval (sortModel le)).Pairwise le := by
61+
simpa using List.pairwise_insertionSort _ _
62+
63+
lemma insertionSort_length (l : List α) (le : α → α → Prop) [DecidableRel le] :
64+
((insertionSort l).eval (sortModel le)).length = l.length := by
65+
simp
66+
67+
lemma insertionSort_time_compares (head : α) (tail : List α) (le : α → α → Prop) [DecidableRel le] :
68+
((insertionSort (head :: tail)).time (sortModel le)).compares =
69+
((insertionSort tail).time (sortModel le)).compares +
70+
((insertOrd head (tail.insertionSort le)).time (sortModel le)).compares := by
71+
simp [insertionSort]
72+
73+
lemma insertionSort_time_inserts (head : α) (tail : List α) (le : α → α → Prop) [DecidableRel le] :
74+
((insertionSort (head :: tail)).time (sortModel le)).inserts =
75+
((insertionSort tail).time (sortModel le)).inserts +
76+
((insertOrd head (tail.insertionSort le)).time (sortModel le)).inserts := by
77+
simp [insertionSort]
78+
79+
theorem insertionSort_complexity (l : List α) (le : α → α → Prop) [DecidableRel le] :
80+
((insertionSort l).time (sortModel le))
81+
≤ ⟨l.length * (l.length + 1), (l.length + 1) * (l.length + 2)⟩ := by
82+
induction l with
83+
| nil =>
84+
simp [insertionSort]
85+
| cons head tail ih =>
86+
have h := insertOrd_complexity_upper_bound (tail.insertionSort le) head le
87+
simp_all only [List.length_cons, List.length_insertionSort]
88+
obtain ⟨ih₁,ih₂⟩ := ih
89+
obtain ⟨h₁,h₂⟩ := h
90+
refine ⟨?_, ?_⟩
91+
· clear h₂
92+
rw [insertionSort_time_compares]
93+
nlinarith [ih₁, h₁]
94+
· clear h₁
95+
rw [insertionSort_time_inserts]
96+
nlinarith [ih₂, h₂]
97+
98+
end Algorithms
99+
100+
end Cslib

‎Cslib/AlgorithmsTheory/Algorithms/ListLinearSearch.lean‎

Lines changed: 83 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,83 @@
1+
/-
2+
Copyright (c) 2026 Shreyas Srinivas. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Shreyas Srinivas, Eric Wieser
5+
-/
6+
7+
module
8+
9+
public import Cslib.AlgorithmsTheory.QueryModel
10+
public import Cslib.AlgorithmsTheory.Models.ListComparisonSearch
11+
public import Mathlib
12+
13+
@[expose] public section
14+
15+
/-!
16+
# Linear search in a list
17+
18+
In this file we state and prove the correctness and complexity of linear search in lists under
19+
the `ListSearch` model.
20+
--
21+
22+
## Main Definitions
23+
24+
- `listLinearSearch` : Linear search algorithm in the `ListSearch` query model
25+
26+
## Main results
27+
28+
- `listLinearSearch_eval`: `insertOrd` evaluates identically to `List.contains`.
29+
- `listLinearSearchM_time_complexity_upper_bound` : `linearSearch` takes at most `n`
30+
comparison operations
31+
- `listLinearSearchM_time_complexity_lower_bound` : There exist lists on which `linearSearch` needs
32+
`n` comparisons
33+
-/
34+
namespace Cslib
35+
36+
namespace Algorithms
37+
38+
open Prog
39+
40+
open ListSearch in
41+
/-- Linear Search in Lists on top of the `ListSearch` query model. -/
42+
def listLinearSearch (l : List α) (x : α) : Prog (ListSearch α) Bool := do
43+
match l with
44+
| [] => return false
45+
| l :: ls =>
46+
let cmp : Bool ← compare (l :: ls) x
47+
if cmp then
48+
return true
49+
else
50+
listLinearSearch ls x
51+
52+
@[simp, grind =]
53+
lemma listLinearSearch_eval [BEq α] (l : List α) (x : α) :
54+
(listLinearSearch l x).eval ListSearch.natCost = l.contains x := by
55+
fun_induction l.elem x with simp_all [listLinearSearch]
56+
57+
lemma listLinearSearchM_correct_true [BEq α] [LawfulBEq α] (l : List α)
58+
{x : α} (x_mem_l : x ∈ l) : (listLinearSearch l x).eval ListSearch.natCost = true := by
59+
simp [x_mem_l]
60+
61+
lemma listLinearSearchM_correct_false [BEq α] [LawfulBEq α] (l : List α)
62+
{x : α} (x_mem_l : x ∉ l) : (listLinearSearch l x).eval ListSearch.natCost = false := by
63+
simp [x_mem_l]
64+
65+
lemma listLinearSearchM_time_complexity_upper_bound [BEq α] (l : List α) (x : α) :
66+
(listLinearSearch l x).time ListSearch.natCost ≤ l.length := by
67+
fun_induction l.elem x with
68+
| case1 => simp [listLinearSearch]
69+
| case2 => simp_all [listLinearSearch]
70+
| case3 =>
71+
simp_all [listLinearSearch]
72+
grind
73+
74+
-- This statement is wrong
75+
lemma listLinearSearchM_time_complexity_lower_bound [DecidableEq α] [Nonempty α] :
76+
∃ l : List α, ∃ x : α, (listLinearSearch l x).time ListSearch.natCost = l.length := by
77+
inhabit α
78+
refine ⟨[], default, ?_⟩
79+
simp_all [ListSearch.natCost, listLinearSearch]
80+
81+
end Algorithms
82+
83+
end Cslib

‎Cslib/AlgorithmsTheory/Algorithms/ListOrderedInsert.lean‎

Lines changed: 96 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,96 @@
1+
/-
2+
Copyright (c) 2026 Shreyas Srinivas. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Shreyas Srinivas, Eric Wieser
5+
-/
6+
7+
module
8+
9+
public import Cslib.AlgorithmsTheory.QueryModel
10+
public import Cslib.AlgorithmsTheory.Models.ListComparisonSort
11+
public import Mathlib
12+
13+
@[expose] public section
14+
15+
/-!
16+
# Ordered insertion in a list
17+
18+
In this file we state and prove the correctness and complexity of ordered insertions in lists under
19+
the `SortOps` model. This ordered insert is later used in `insertionSort` mirroring the structure
20+
in upstream libraries for the pure lean code versions of these declarations.
21+
22+
--
23+
24+
## Main Definitions
25+
26+
- `insertOrd` : ordered insert algorithm in the `SortOps` query model
27+
28+
## Main results
29+
30+
- `insertOrd_eval`: `insertOrd` evaluates identically to `List.orderedInsert`.
31+
- `insertOrd_complexity_upper_bound` : Shows that `insertOrd` takes at most `n` comparisons,
32+
and `n + 1` list head-insertion operations.
33+
- `insertOrd_sorted` : Applying `insertOrd` to a sorted list yields a sorted list.
34+
-/
35+
36+
namespace Cslib
37+
namespace Algorithms
38+
39+
open Prog
40+
41+
open SortOps
42+
43+
/--
44+
Performs ordered insertion of `x` into a list `l` in the `SortOps` query model.
45+
If `l` is sorted, then `x` is inserted into `l` such that the resultant list is also sorted.
46+
-/
47+
def insertOrd (x : α) (l : List α) : Prog (SortOps α) (List α) := do
48+
match l with
49+
| [] => insertHead x l
50+
| a :: as =>
51+
if (← cmpLE x a : Bool) then
52+
insertHead x (a :: as)
53+
else
54+
let res ← insertOrd x as
55+
insertHead a res
56+
57+
@[simp]
58+
lemma insertOrd_eval (x : α) (l : List α) (le : α → α → Prop) [DecidableRel le] :
59+
(insertOrd x l).eval (sortModel le) = l.orderedInsert le x := by
60+
induction l with
61+
| nil =>
62+
simp [insertOrd, sortModel]
63+
| cons head tail ih =>
64+
by_cases h_head : le x head
65+
· simp [insertOrd, h_head]
66+
· simp [insertOrd, h_head, ih]
67+
68+
-- to upstream
69+
@[simp]
70+
lemma _root_.List.length_orderedInsert (x : α) (l : List α) [DecidableRel r] :
71+
(l.orderedInsert r x).length = l.length + 1 := by
72+
induction l <;> grind
73+
74+
theorem insertOrd_complexity_upper_bound
75+
(l : List α) (x : α) (le : α → α → Prop) [DecidableRel le] :
76+
(insertOrd x l).time (sortModel le) ≤ ⟨l.length, l.length + 1⟩ := by
77+
induction l with
78+
| nil =>
79+
simp [insertOrd, sortModel]
80+
| cons head tail ih =>
81+
obtain ⟨ih_compares, ih_inserts⟩ := ih
82+
rw [insertOrd]
83+
by_cases h_head : le x head
84+
· simp [h_head]
85+
· simp [h_head]
86+
grind
87+
88+
lemma insertOrd_sorted
89+
(l : List α) (x : α) (le : α → α → Prop) [DecidableRel le] [Std.Total le] [IsTrans _ le] :
90+
l.Pairwise le → ((insertOrd x l).eval (sortModel le)).Pairwise le := by
91+
rw [insertOrd_eval]
92+
exact List.Pairwise.orderedInsert _ _
93+
94+
end Algorithms
95+
96+
end Cslib

0 commit comments

Comments
 (0)