|
| 1 | +/- |
| 2 | +Copyright (c) 2026 Lean FRO, LLC. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Kim Morrison, Sebastian Graf |
| 5 | +-/ |
| 6 | +module |
| 7 | + |
| 8 | +public import Cslib.Algorithms.Lean.Query.Bounds |
| 9 | +public import Cslib.Algorithms.Lean.Query.Sort.IsSort |
| 10 | +public import Cslib.Algorithms.Lean.Query.Sort.Insertion.Defs |
| 11 | +import Mathlib.Data.List.Sort |
| 12 | +import Mathlib.Tactic.Ring |
| 13 | +public import Mathlib.Algebra.Group.Defs |
| 14 | + |
| 15 | +/-! # Insertion Sort: Correctness and Upper Bound |
| 16 | +
|
| 17 | +Proofs that `insertionSort` is a correct comparison sort and uses at most `n²` queries. |
| 18 | +All proofs are by plain equational reasoning on `Prog.eval` and `Prog.queriesOn`. |
| 19 | +-/ |
| 20 | + |
| 21 | +open Cslib.Query |
| 22 | + |
| 23 | +public section |
| 24 | + |
| 25 | +namespace Cslib.Query |
| 26 | + |
| 27 | +variable {α : Type} |
| 28 | + |
| 29 | +-- ## Evaluation simp lemmas for orderedInsert |
| 30 | + |
| 31 | +@[simp] theorem eval_orderedInsert_nil (oracle : {ι : Type} → LEQuery α ι → ι) (x : α) : |
| 32 | + (orderedInsert x ([] : List α)).eval oracle = [x] := by |
| 33 | + simp [orderedInsert] |
| 34 | + |
| 35 | +@[simp] theorem eval_orderedInsert_cons (oracle : {ι : Type} → LEQuery α ι → ι) (x y : α) |
| 36 | + (ys : List α) : |
| 37 | + (orderedInsert x (y :: ys)).eval oracle = |
| 38 | + if oracle (.le x y) then x :: y :: ys |
| 39 | + else y :: (orderedInsert x ys).eval oracle := by |
| 40 | + simp [orderedInsert, LEQuery.ask] |
| 41 | + split <;> simp_all |
| 42 | + |
| 43 | +-- ## Evaluation simp lemmas for insertionSort |
| 44 | + |
| 45 | +@[simp] theorem eval_insertionSort_nil (oracle : {ι : Type} → LEQuery α ι → ι) : |
| 46 | + (insertionSort (α := α) []).eval oracle = [] := by |
| 47 | + simp [insertionSort] |
| 48 | + |
| 49 | +@[simp] theorem eval_insertionSort_cons (oracle : {ι : Type} → LEQuery α ι → ι) |
| 50 | + (x : α) (xs : List α) : |
| 51 | + (insertionSort (x :: xs)).eval oracle = |
| 52 | + (orderedInsert x ((insertionSort xs).eval oracle)).eval oracle := by |
| 53 | + simp [insertionSort] |
| 54 | + |
| 55 | +-- ## Permutation proofs |
| 56 | + |
| 57 | +theorem orderedInsert_perm (oracle : {ι : Type} → LEQuery α ι → ι) (x : α) (xs : List α) : |
| 58 | + ((orderedInsert x xs).eval oracle).Perm (x :: xs) := by |
| 59 | + induction xs with |
| 60 | + | nil => simp |
| 61 | + | cons y ys ih => |
| 62 | + simp only [eval_orderedInsert_cons] |
| 63 | + split |
| 64 | + · exact List.Perm.refl _ |
| 65 | + · exact (List.Perm.cons _ ih).trans (List.Perm.swap _ _ _) |
| 66 | + |
| 67 | +theorem insertionSort_perm (oracle : {ι : Type} → LEQuery α ι → ι) (xs : List α) : |
| 68 | + ((insertionSort xs).eval oracle).Perm xs := by |
| 69 | + induction xs with |
| 70 | + | nil => simp |
| 71 | + | cons x xs ih => |
| 72 | + simp only [eval_insertionSort_cons] |
| 73 | + exact (orderedInsert_perm oracle x _).trans (List.Perm.cons _ ih) |
| 74 | + |
| 75 | +-- ## Sortedness proofs |
| 76 | + |
| 77 | +theorem orderedInsert_sorted |
| 78 | + (r : α → α → Prop) [DecidableRel r] [Std.Total r] [IsTrans α r] |
| 79 | + (oracle : {ι : Type} → LEQuery α ι → ι) |
| 80 | + (horacle : ∀ a b, oracle (.le a b) = decide (r a b)) |
| 81 | + (x : α) (xs : List α) (hxs : xs.Pairwise r) : |
| 82 | + ((orderedInsert x xs).eval oracle).Pairwise r := by |
| 83 | + induction xs with |
| 84 | + | nil => simp |
| 85 | + | cons y ys ih => |
| 86 | + simp only [eval_orderedInsert_cons, horacle] |
| 87 | + split |
| 88 | + next h => |
| 89 | + have hle : r x y := by simpa [decide_eq_true_eq] using h |
| 90 | + exact List.pairwise_cons.mpr ⟨fun z hz => |
| 91 | + match List.mem_cons.mp hz with |
| 92 | + | .inl h => h ▸ hle |
| 93 | + | .inr h => _root_.trans hle (List.rel_of_pairwise_cons hxs h), hxs⟩ |
| 94 | + next h => |
| 95 | + have hle : ¬ r x y := by simpa [decide_eq_true_eq] using h |
| 96 | + have hyx : r y x := (Std.Total.total y x).resolve_right hle |
| 97 | + have ih' := ih hxs.of_cons |
| 98 | + have hperm := orderedInsert_perm oracle x ys |
| 99 | + exact List.pairwise_cons.mpr ⟨fun z hz => |
| 100 | + match List.mem_cons.mp (hperm.mem_iff.mp hz) with |
| 101 | + | .inl h => h ▸ hyx |
| 102 | + | .inr h => List.rel_of_pairwise_cons hxs h, ih'⟩ |
| 103 | + |
| 104 | +theorem insertionSort_sorted |
| 105 | + (r : α → α → Prop) [DecidableRel r] [Std.Total r] [IsTrans α r] |
| 106 | + (oracle : {ι : Type} → LEQuery α ι → ι) |
| 107 | + (horacle : ∀ a b, oracle (.le a b) = decide (r a b)) |
| 108 | + (xs : List α) : |
| 109 | + ((insertionSort xs).eval oracle).Pairwise r := by |
| 110 | + induction xs with |
| 111 | + | nil => simp |
| 112 | + | cons x xs ih => |
| 113 | + simp only [eval_insertionSort_cons] |
| 114 | + exact orderedInsert_sorted r oracle horacle x _ ih |
| 115 | + |
| 116 | +-- ## Query count proofs |
| 117 | + |
| 118 | +theorem orderedInsert_queriesOn_le (oracle : {ι : Type} → LEQuery α ι → ι) |
| 119 | + (x : α) (xs : List α) : |
| 120 | + (orderedInsert x xs).queriesOn oracle ≤ xs.length := by |
| 121 | + induction xs with |
| 122 | + | nil => simp [orderedInsert] |
| 123 | + | cons y ys ih => |
| 124 | + unfold orderedInsert LEQuery.ask |
| 125 | + simp |
| 126 | + split |
| 127 | + · simp_all |
| 128 | + · simp_all; omega |
| 129 | + |
| 130 | +theorem insertionSort_queriesOn_le (oracle : {ι : Type} → LEQuery α ι → ι) |
| 131 | + (xs : List α) : |
| 132 | + (insertionSort xs).queriesOn oracle ≤ xs.length ^ 2 := by |
| 133 | + induction xs with |
| 134 | + | nil => simp [insertionSort] |
| 135 | + | cons x xs ih => |
| 136 | + have hq : (insertionSort (x :: xs)).queriesOn oracle = |
| 137 | + (insertionSort xs).queriesOn oracle + |
| 138 | + (orderedInsert x ((insertionSort xs).eval oracle)).queriesOn oracle := by |
| 139 | + simp [insertionSort] |
| 140 | + rw [hq] |
| 141 | + have hlen : ((insertionSort xs).eval oracle).length = xs.length := |
| 142 | + (insertionSort_perm oracle xs).length_eq |
| 143 | + have hord := orderedInsert_queriesOn_le oracle x ((insertionSort xs).eval oracle) |
| 144 | + rw [hlen] at hord |
| 145 | + have h1 := Nat.add_le_add ih hord |
| 146 | + have hpow : xs.length ^ 2 + xs.length ≤ (xs.length + 1) ^ 2 := by |
| 147 | + have : (xs.length + 1) ^ 2 = xs.length ^ 2 + 2 * xs.length + 1 := by ring |
| 148 | + omega |
| 149 | + simp only [List.length_cons] |
| 150 | + exact Nat.le_trans h1 hpow |
| 151 | + |
| 152 | +-- ## UpperBound and IsSort instances |
| 153 | + |
| 154 | +public theorem insertionSort_upperBound : |
| 155 | + UpperBound (insertionSort (α := α)) List.length (· ^ 2) := by |
| 156 | + intro oracle n x hle |
| 157 | + exact Nat.le_trans (insertionSort_queriesOn_le oracle x) |
| 158 | + (Nat.pow_le_pow_left hle 2) |
| 159 | + |
| 160 | +public theorem insertionSort_isSort : IsSort (insertionSort (α := α)) where |
| 161 | + perm xs oracle := insertionSort_perm oracle xs |
| 162 | + sorted := by |
| 163 | + intro xs oracle r _ _ _ horacle |
| 164 | + exact insertionSort_sorted r oracle horacle xs |
| 165 | + |
| 166 | +end Cslib.Query |
| 167 | + |
| 168 | +end -- public section |
0 commit comments