feat: query complexity model for algorithms theory

Cslib.lean

@@ -1,7 +1,14 @@
 module  -- shake: keep-all
 
-public import Cslib.Algorithms.Lean.MergeSort.MergeSort
-public import Cslib.Algorithms.Lean.TimeM
+public import Cslib.AlgorithmsTheory.Algorithms.ListInsertionSort
+public import Cslib.AlgorithmsTheory.Algorithms.ListLinearSearch
+public import Cslib.AlgorithmsTheory.Algorithms.ListOrderedInsert
+public import Cslib.AlgorithmsTheory.Algorithms.MergeSort
+public import Cslib.AlgorithmsTheory.Lean.MergeSort.MergeSort
+public import Cslib.AlgorithmsTheory.Lean.TimeM
+public import Cslib.AlgorithmsTheory.Models.ListComparisonSearch
+public import Cslib.AlgorithmsTheory.Models.ListComparisonSort
+public import Cslib.AlgorithmsTheory.QueryModel
 public import Cslib.Computability.Automata.Acceptors.Acceptor
 public import Cslib.Computability.Automata.Acceptors.OmegaAcceptor
 public import Cslib.Computability.Automata.DA.Basic

Cslib/AlgorithmsTheory/Algorithms/ListInsertionSort.lean

@@ -0,0 +1,90 @@
+/-
+Copyright (c) 2026 Shreyas Srinivas. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Shreyas Srinivas, Eric Wieser
+-/
+module
+
+public import Cslib.AlgorithmsTheory.Algorithms.ListOrderedInsert
+public import Mathlib.Tactic.Linarith
+
+@[expose] public section
+
+/-!
+# Insertion sort in a list
+
+In this file we state and prove the correctness and complexity of insertion sort in lists under
+the `SortOps` model. This insertionSort evaluates identically to the upstream version of
+`List.insertionSort`
+--
+
+## Main Definitions
+
+- `insertionSort` : Insertion sort algorithm in the `SortOps` query model
+
+## Main results
+
+- `insertionSort_eval`: `insertionSort` evaluates identically to `List.insertionSort`.
+- `insertionSort_permutation` :  `insertionSort` outputs a permutation of the input list.
+- `insertionSort_sorted` : `insertionSort` outputs a sorted list.
+- `insertionSort_complexity` : `insertionSort` takes at most n * (n + 1) comparisons and
+  (n + 1) * (n + 2) list head-insertions.
+-/
+
+namespace Cslib
+
+namespace Algorithms
+
+open Prog
+
+/-- The insertionSort algorithms on lists with the `SortOps` query. -/
+def insertionSort (l : List α) : Prog (SortOps α) (List α) :=
+  match l with
+  | [] => return []
+  | x :: xs => do
+      let rest ← insertionSort xs
+      insertOrd x rest
+
+@[simp]
+theorem insertionSort_eval (l : List α) (le : α → α → Prop) [DecidableRel le] :
+    (insertionSort l).eval (sortModel le) = l.insertionSort le := by
+  induction l with simp_all [insertionSort]
+
+theorem insertionSort_permutation (l : List α) (le : α → α → Prop) [DecidableRel le] :
+    ((insertionSort l).eval (sortModel le)).Perm l := by
+    simp [insertionSort_eval, List.perm_insertionSort]
+
+theorem insertionSort_sorted
+    (l : List α) (le : α → α → Prop) [DecidableRel le] [Std.Total le] [IsTrans α le] :
+    ((insertionSort l).eval (sortModel le)).Pairwise le := by
+  simpa using List.pairwise_insertionSort _ _
+
+lemma insertionSort_length (l : List α) (le : α → α → Prop) [DecidableRel le] :
+    ((insertionSort l).eval (sortModel le)).length = l.length := by
+  simp
+
+lemma insertionSort_time_compares (head : α) (tail : List α) (le : α → α → Prop) [DecidableRel le] :
+    ((insertionSort (head :: tail)).time (sortModel le)).compares =
+      ((insertionSort tail).time (sortModel le)).compares +
+        ((insertOrd head (tail.insertionSort le)).time (sortModel le)).compares := by
+  simp [insertionSort]
+
+lemma insertionSort_time_inserts (head : α) (tail : List α) (le : α → α → Prop) [DecidableRel le] :
+    ((insertionSort (head :: tail)).time (sortModel le)).inserts =
+      ((insertionSort tail).time (sortModel le)).inserts +
+        ((insertOrd head (tail.insertionSort le)).time (sortModel le)).inserts := by
+  simp [insertionSort]
+
+theorem insertionSort_complexity (l : List α) (le : α → α → Prop) [DecidableRel le] :
+    ((insertionSort l).time (sortModel le))
+      ≤ ⟨l.length * (l.length + 1), (l.length + 1) * (l.length + 2)⟩ := by
+  induction l with
+  | nil =>
+    simp [insertionSort]
+  | cons head tail ih =>
+    grind [insertOrd_complexity_upper_bound, List.length_insertionSort, SortOpsCost.le_def,
+      insertionSort_time_compares, insertionSort_time_inserts]
+
+end Algorithms
+
+end Cslib

Cslib/AlgorithmsTheory/Algorithms/ListLinearSearch.lean

@@ -0,0 +1,100 @@
+/-
+Copyright (c) 2026 Shreyas Srinivas. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Shreyas Srinivas, Eric Wieser
+-/
+
+module
+
+public import Cslib.AlgorithmsTheory.QueryModel
+public import Cslib.AlgorithmsTheory.Models.ListComparisonSearch
+public import Mathlib.Algebra.Order.Group.Nat
+public import Mathlib.Data.Int.ConditionallyCompleteOrder
+public import Mathlib.Order.ConditionallyCompleteLattice.Basic
+public import Mathlib.Tactic.Set
+
+@[expose] public section
+
+/-!
+# Linear search in a list
+
+In this file we state and prove the correctness and complexity of linear search in lists under
+the `ListSearch` model.
+--
+
+## Main Definitions
+
+- `listLinearSearch` : Linear search algorithm in the `ListSearch` query model
+
+## Main results
+
+- `listLinearSearch_eval`: `insertOrd` evaluates identically to `List.contains`.
+- `listLinearSearchM_time_complexity_upper_bound` : `linearSearch` takes at most `n`
+  comparison operations
+- `listLinearSearchM_time_complexity_lower_bound` : There exist lists on which `linearSearch` needs
+  `n` comparisons
+-/
+namespace Cslib
+
+namespace Algorithms
+
+open Prog
+
+open ListSearch in
+/-- Linear Search in Lists on top of the `ListSearch` query model. -/
+def listLinearSearch (l : List α) (x : α) : Prog (ListSearch α) Bool := do
+  match l with
+  | [] => return false
+  | l :: ls =>
+    let cmp : Bool ← compare (l :: ls) x
+    if cmp then
+      return true
+    else
+      listLinearSearch ls x
+
+@[simp, grind =]
+lemma listLinearSearch_eval [BEq α] (l : List α) (x : α) :
+    (listLinearSearch l x).eval ListSearch.natCost = l.contains x := by
+  fun_induction l.elem x with simp_all [listLinearSearch]
+
+lemma listLinearSearchM_correct_true [BEq α] [LawfulBEq α] (l : List α)
+    {x : α} (x_mem_l : x ∈ l) : (listLinearSearch l x).eval ListSearch.natCost = true := by
+  simp [x_mem_l]
+
+lemma listLinearSearchM_correct_false [BEq α] [LawfulBEq α] (l : List α)
+    {x : α} (x_mem_l : x ∉ l) : (listLinearSearch l x).eval ListSearch.natCost = false := by
+  simp [x_mem_l]
+
+lemma listLinearSearchM_time_complexity_upper_bound [BEq α] (l : List α) (x : α) :
+    (listLinearSearch l x).time ListSearch.natCost ≤ l.length := by
+  fun_induction l.elem x with
+  | case1 => simp [listLinearSearch]
+  | case2 => simp_all [listLinearSearch]
+  | case3 =>
+    simp_all [listLinearSearch]
+    lia
+
+lemma listLinearSearchM_time_complexity_lower_bound [DecidableEq α] [Nontrivial α] :
+    ∀ n, ∃ l : List α, ∃ x : α, l.length = n
+      ∧ (listLinearSearch l x).time ListSearch.natCost = l.length := by
+  intro n
+  obtain ⟨x, y, hneq⟩ := exists_pair_ne α
+  use (List.replicate n y), x
+  refine ⟨?_, ?_⟩
+  · simp
+  · induction n with
+    | zero => simp [listLinearSearch, List.replicate]
+    | succ m ih =>
+      simp only [List.replicate, listLinearSearch, FreeM.lift_def, FreeM.pure_eq_pure,
+        FreeM.bind_eq_bind, FreeM.liftBind_bind, FreeM.pure_bind, time_liftBind,
+        ListSearch.natCost_cost, ListSearch.natCost_evalQuery, List.head?_cons,
+        Option.some_beq_some, beq_iff_eq, List.length_cons, List.length_replicate]
+      split_ifs with hxy_eq
+      · exfalso
+        tauto
+      · rw [ih, List.length_replicate, add_comm]
+
+
+end Algorithms
+
+end Cslib

Cslib/AlgorithmsTheory/Algorithms/ListOrderedInsert.lean

@@ -0,0 +1,99 @@
+/-
+Copyright (c) 2026 Shreyas Srinivas. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Shreyas Srinivas, Eric Wieser
+-/
+
+module
+
+public import Cslib.AlgorithmsTheory.QueryModel
+public import Cslib.AlgorithmsTheory.Models.ListComparisonSort
+public import Mathlib.Algebra.Order.Group.Nat
+public import Mathlib.Data.Int.ConditionallyCompleteOrder
+public import Mathlib.Data.List.Sort
+public import Mathlib.Order.ConditionallyCompleteLattice.Basic
+
+@[expose] public section
+
+/-!
+# Ordered insertion in a list
+
+In this file we state and prove the correctness and complexity of ordered insertions in lists under
+the `SortOps` model. This ordered insert is later used in `insertionSort` mirroring the structure
+in upstream libraries for the pure lean code versions of these declarations.
+
+--
+
+## Main Definitions
+
+- `insertOrd` : ordered insert algorithm in the `SortOps` query model
+
+## Main results
+
+- `insertOrd_eval`: `insertOrd` evaluates identically to `List.orderedInsert`.
+- `insertOrd_complexity_upper_bound` : Shows that `insertOrd` takes at most `n` comparisons,
+   and `n + 1` list head-insertion operations.
+- `insertOrd_sorted` : Applying `insertOrd` to a sorted list yields a sorted list.
+-/
+
+namespace Cslib
+namespace Algorithms
+
+open Prog
+
+open SortOps
+
+/--
+Performs ordered insertion of `x` into a list `l` in the `SortOps` query model.
+If `l` is sorted, then `x` is inserted into `l` such that the resultant list is also sorted.
+-/
+def insertOrd (x : α) (l : List α) : Prog (SortOps α) (List α) := do
+  match l with
+  | [] => insertHead x l
+  | a :: as =>
+      if (← cmpLE x a : Bool) then
+        insertHead x (a :: as)
+      else
+        let res ← insertOrd x as
+        insertHead a res
+
+@[simp]
+lemma insertOrd_eval (x : α) (l : List α) (le : α → α → Prop) [DecidableRel le] :
+    (insertOrd x l).eval (sortModel le) = l.orderedInsert le x := by
+  induction l with
+  | nil =>
+    simp [insertOrd, sortModel]
+  | cons head tail ih =>
+    by_cases h_head : le x head
+    · simp [insertOrd, h_head]
+    · simp [insertOrd, h_head, ih]
+
+-- TODO : to upstream
+@[simp]
+lemma _root_.List.length_orderedInsert (x : α) (l : List α) [DecidableRel r] :
+    (l.orderedInsert r x).length = l.length + 1 := by
+  induction l <;> grind
+
+theorem insertOrd_complexity_upper_bound
+    (l : List α) (x : α) (le : α → α → Prop) [DecidableRel le] :
+    (insertOrd x l).time (sortModel le) ≤ ⟨l.length, l.length + 1⟩ := by
+  induction l with
+  | nil =>
+    simp [insertOrd, sortModel]
+  | cons head tail ih =>
+    obtain ⟨ih_compares, ih_inserts⟩ := ih
+    rw [insertOrd]
+    by_cases h_head : le x head
+    · simp [h_head]
+    · simp [h_head]
+      grind
+
+lemma insertOrd_sorted
+    (l : List α) (x : α) (le : α → α → Prop) [DecidableRel le] [Std.Total le] [IsTrans α le] :
+    l.Pairwise le → ((insertOrd x l).eval (sortModel le)).Pairwise le := by
+  rw [insertOrd_eval]
+  exact List.Pairwise.orderedInsert _ _
+
+end Algorithms
+
+end Cslib