From c2381cca28fe89fefc0b7c3d8e71e0a970a69900 Mon Sep 17 00:00:00 2001 From: Tanner Duve Date: Tue, 2 Jun 2026 13:58:42 -0700 Subject: [PATCH 1/7] feat(FreeWP): weakest preconditions for FreeM via Std.Do Port of cslib feat/free-logic: logical handlers (LHandler) into PredTrans, wpH as the unique monad morphism from FreeM, adequacy theorem, HasHandler instances plugging FreeM into Std.Do's WP/WPMonad/Triple infrastructure, plus state/reader handlers with @[spec] lemmas and tests. Follows Vistrup, Sammler, Jung. Program Logics a la Carte. POPL 2025. --- Algolean.lean | 2 + Algolean/FreeWP/Effects.lean | 86 ++++++++++++ Algolean/FreeWP/WP.lean | 128 ++++++++++++++++++ AlgoleanTests.lean | 1 + AlgoleanTests/FreeMonadWP.lean | 234 +++++++++++++++++++++++++++++++++ 5 files changed, 451 insertions(+) create mode 100644 Algolean/FreeWP/Effects.lean create mode 100644 Algolean/FreeWP/WP.lean create mode 100644 AlgoleanTests/FreeMonadWP.lean diff --git a/Algolean.lean b/Algolean.lean index 013a5ba..0db1429 100644 --- a/Algolean.lean +++ b/Algolean.lean @@ -11,6 +11,8 @@ public import Algolean.Algorithms.NaivePatternSearch public import Algolean.Algorithms.VecSearch public import Algolean.Complexity.Basic public import Algolean.Complexity.PolytimeBasicClasses +public import Algolean.FreeWP.Effects +public import Algolean.FreeWP.WP public import Algolean.LowerBounds.ComparisonSort public import Algolean.Models.Circuits public import Algolean.Models.Comparison diff --git a/Algolean/FreeWP/Effects.lean b/Algolean/FreeWP/Effects.lean new file mode 100644 index 0000000..38a21c6 --- /dev/null +++ b/Algolean/FreeWP/Effects.lean @@ -0,0 +1,86 @@ +/- +Copyright (c) 2025 Tanner Duve (Logical Intelligence). All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Tanner Duve +-/ + +module + +public import Cslib.Foundations.Control.Monad.Free.Effects +public import Algolean.FreeWP.WP + +/-! +# Logical handlers for the standard `FreeM` effects + +Logical handlers and `HasHandler` instances for the state and reader effects from +`Cslib.Foundations.Control.Monad.Free.Effects`, each induced by the canonical interpreter +into the corresponding Lean monad (`StateM`, `ReaderM`) via `Std.Do`'s `WP` instances. +Adequacy theorems relate the `FreeM`-level WP to the WP of the interpretation, and `@[spec]` +Hoare triples for the primitive operations enable `mvcgen` reasoning. +-/ + +@[expose] public section + +set_option mvcgen.warning false + +namespace Cslib + +namespace FreeM + +open Std.Do + +universe u + +/-! ### State -/ + +/-- Logical handler for the state effect, induced by `Std.Do`'s `WP (StateM σ)`. -/ +def StateF.handler {σ : Type u} : LHandler (StateF σ) (.arg σ .pure) := + LHandler.ofInterp (m := StateM σ) (fun _ op => FreeState.stateInterp op) + +instance StateF.instHasHandler {σ : Type u} : + HasHandler (StateF σ) (.arg σ .pure) where + handler := StateF.handler + +/-- WP of a `FreeState` program matches WP of its `StateM` interpretation. -/ +theorem StateF.wp_FreeState_eq_wp_toStateM {σ α : Type u} (comp : FreeState σ α) : + wp comp = wp (FreeState.toStateM comp) := + wpH_ofInterp_eq_wp_liftM (m := StateM σ) + (fun _ op => FreeState.stateInterp op) comp + +/-- Hoare spec for `get` on `FreeState`. -/ +@[spec] +theorem Spec.get_FreeState {σ : Type u} {Q : PostCond σ (.arg σ .pure)} : + Triple (MonadStateOf.get : FreeState σ σ) (spred(fun s => Q.1 s s)) Q := by + mvcgen + +/-- Hoare spec for `set` on `FreeState`. -/ +@[spec] +theorem Spec.set_FreeState {σ : Type u} (s : σ) {Q : PostCond PUnit (.arg σ .pure)} : + Triple (MonadStateOf.set s : FreeState σ PUnit) (spred(fun _ => Q.1 ⟨⟩ s)) Q := by + mvcgen + +/-! ### Reader -/ + +/-- Logical handler for the reader effect, induced by `Std.Do`'s `WP (ReaderM σ)`. -/ +def ReaderF.handler {σ : Type u} : LHandler (ReaderF σ) (.arg σ .pure) := + LHandler.ofInterp (m := ReaderM σ) (fun _ op => FreeReader.readInterp op) + +instance ReaderF.instHasHandler {σ : Type u} : + HasHandler (ReaderF σ) (.arg σ .pure) where + handler := ReaderF.handler + +/-- WP of a `FreeReader` program matches WP of its `ReaderM` interpretation. -/ +theorem ReaderF.wp_FreeReader_eq_wp_toReaderM {σ α : Type u} (comp : FreeReader σ α) : + wp comp = wp (FreeReader.toReaderM comp) := + wpH_ofInterp_eq_wp_liftM (m := ReaderM σ) + (fun _ op => FreeReader.readInterp op) comp + +/-- Hoare spec for `read` on `FreeReader`. -/ +@[spec] +theorem Spec.read_FreeReader {ρ : Type u} {Q : PostCond ρ (.arg ρ .pure)} : + Triple (MonadReaderOf.read : FreeReader ρ ρ) (spred(fun r => Q.1 r r)) Q := by + mvcgen + +end FreeM + +end Cslib diff --git a/Algolean/FreeWP/WP.lean b/Algolean/FreeWP/WP.lean new file mode 100644 index 0000000..7dcdc6c --- /dev/null +++ b/Algolean/FreeWP/WP.lean @@ -0,0 +1,128 @@ +/- +Copyright (c) 2025 Tanner Duve (Logical Intelligence). All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Tanner Duve +-/ + +module + +public import Cslib.Foundations.Control.Monad.Free +public import Std.Do.PredTrans +public import Std.Do.WP.Basic +public import Std.Do.WP.Monad +public import Std.Do.Triple + +/-! +# Weakest preconditions for `FreeM` programs + +Weakest-precondition interpretation of `FreeM F` programs through `Std.Do`'s +predicate-transformer monad `PredTrans ps`. The universal property of `FreeM` lifts any +effect handler `F ι → PredTrans ps ι` to a unique monad morphism `wpH H = liftM H`, +so weakest preconditions are compositional in `FreeM`'s monadic structure. A +`[HasHandler F ps]` instance plugs `FreeM F` into `Std.Do`'s `WP`/`WPMonad`/`Triple` +infrastructure. + +The WP's structural rules (`wpH_pure`, `wpH_bind`, …) are immediate from `liftM` being a monad +morphism; the adequacy theorem `wpH_ofInterp_eq_wp_liftM` — that WP-via-handler agrees with +`Std.Do`'s WP of the `liftM` interpretation — is the same statement of uniqueness. + +The design follows [Vistrup, Sammler, Jung. *Program Logics à la Carte.* POPL 2025], adapted +from coinductive ITrees to inductive `FreeM` and from Iris to `Std.Do`. +-/ + +@[expose] public section + +set_option mvcgen.warning false + +namespace Cslib + +open Std.Do + +namespace FreeM + +universe u v w + +variable {F G : Type u → Type v} {ps : PostShape.{u}} {α β : Type u} + +/-- A logical handler: an effect handler from `F` into the predicate-transformer monad +`PredTrans ps`. -/ +abbrev LHandler (F : Type u → Type v) (ps : PostShape.{u}) : Type (max (u + 1) v) := + ∀ {ι : Type u}, F ι → PredTrans ps ι + +namespace LHandler + +/-- Sum of handlers; the counterpart of the paper's `H₁ ⊕ H₂`. -/ +def sum (H₁ : LHandler F ps) (H₂ : LHandler G ps) : + LHandler (fun α => F α ⊕ G α) ps := + fun op => Sum.elim H₁ H₂ op + +@[simp] theorem sum_inl (H₁ : LHandler F ps) (H₂ : LHandler G ps) + {ι : Type u} (x : F ι) : + LHandler.sum H₁ H₂ (Sum.inl x : F ι ⊕ G ι) = H₁ x := rfl + +@[simp] theorem sum_inr (H₁ : LHandler F ps) (H₂ : LHandler G ps) + {ι : Type u} (y : G ι) : + LHandler.sum H₁ H₂ (Sum.inr y : F ι ⊕ G ι) = H₂ y := rfl + +/-- Derive a logical handler from an effect handler into any `[WP m ps]` monad, by composing +with `m`'s WP. -/ +def ofInterp {m : Type u → Type w} [WP m ps] + (interp : ∀ ι : Type u, F ι → m ι) : LHandler F ps := + fun {ι} op => wp (interp ι op) + +@[simp] theorem ofInterp_apply {m : Type u → Type w} [WP m ps] + (interp : ∀ ι : Type u, F ι → m ι) {ι : Type u} (op : F ι) : + LHandler.ofInterp interp op = wp (interp ι op) := rfl + +end LHandler + +/-- Weakest-precondition interpretation of a `FreeM F α` program against a logical handler `H`. +Defined as `FreeM.liftM` instantiated at `PredTrans ps`, the unique monad morphism +`FreeM F → PredTrans ps` extending `H` per the universal property of `FreeM`. -/ +def wpH (H : LHandler F ps) (x : FreeM F α) : PredTrans ps α := + x.liftM H + +@[simp] theorem wpH_pure (H : LHandler F ps) (a : α) : + wpH H (pure a : FreeM F α) = Pure.pure a := rfl + +@[simp] theorem wpH_liftBind (H : LHandler F ps) {ι : Type u} + (op : F ι) (k : ι → FreeM F α) : + wpH H (lift op >>= k) = H op >>= fun x => wpH H (k x) := rfl + +@[simp] theorem wpH_lift (H : LHandler F ps) {ι : Type u} (op : F ι) : + wpH H (lift op : FreeM F ι) = H op := + liftM_lift _ op + +@[simp] theorem wpH_bind (H : LHandler F ps) (x : FreeM F α) (f : α → FreeM F β) : + wpH H (x >>= f) = wpH H x >>= fun a => wpH H (f a) := + liftM_bind _ x f + +/-- Adequacy theorem: WP via `FreeM` against an `ofInterp`-derived handler agrees with +`Std.Do`'s WP of the `liftM` interpretation. Equivalently, two monad morphisms +`FreeM F → PredTrans ps` extending the same handler are equal. -/ +theorem wpH_ofInterp_eq_wp_liftM + {m : Type u → Type w} [Monad m] [LawfulMonad m] [WPMonad m ps] + (interp : ∀ ι : Type u, F ι → m ι) (x : FreeM F α) : + wpH (LHandler.ofInterp interp) x = wp (x.liftM (fun {_} => interp _)) := by + induction x with + | pure a => simp [wpH, FreeM.liftM, WPMonad.wp_pure] + | liftBind op k ih => + simp only [wpH] at ih ⊢ + simp [liftM_liftBind, WPMonad.wp_bind, ih] + +/-- Records a default logical handler for `F` at shape `ps`, enabling the global +`WP (FreeM F) ps` instance and any `Triple`/`mvcgen` reasoning over `FreeM F`. -/ +class HasHandler (F : Type u → Type v) (ps : outParam (PostShape.{u})) where + /-- The default logical handler for `F`. -/ + handler {ι : Type u} : F ι → PredTrans ps ι + +instance instWPFreeM [HasHandler F ps] : WP (FreeM F) ps where + wp := wpH HasHandler.handler + +instance instWPMonadFreeM [HasHandler F ps] : WPMonad (FreeM F) ps where + wp_pure _ := rfl + wp_bind x f := wpH_bind _ x f + +end FreeM + +end Cslib diff --git a/AlgoleanTests.lean b/AlgoleanTests.lean index 87c80c8..523359e 100644 --- a/AlgoleanTests.lean +++ b/AlgoleanTests.lean @@ -1,6 +1,7 @@ module -- shake: keep-all public import AlgoleanTests.CircuitExamples +public import AlgoleanTests.FreeMonadWP public import AlgoleanTests.KMPExamples public import AlgoleanTests.NaivePatternSearchExamples public import AlgoleanTests.ProgExamples diff --git a/AlgoleanTests/FreeMonadWP.lean b/AlgoleanTests/FreeMonadWP.lean new file mode 100644 index 0000000..76f5bf1 --- /dev/null +++ b/AlgoleanTests/FreeMonadWP.lean @@ -0,0 +1,234 @@ +/- +Copyright (c) 2025 Tanner Duve (Logical Intelligence). All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Tanner Duve +-/ + +module + +public import Algolean.FreeWP.Effects +public import Std.Tactic.Do + +/-! +Examples for WP in `Algolean.FreeWP.WP`: instance resolution, +a `Triple` on a `FreeState` program discharged by `mvcgen`, and a custom `CounterF` effect with +its own logical handler. +-/ + +@[expose] public section + +set_option mvcgen.warning false + +namespace AlgoleanTests.FreeMonadWP + +open Cslib Cslib.FreeM Std.Do + +example : WP (FreeState Nat) (.arg Nat .pure) := inferInstance +example : WPMonad (FreeState Nat) (.arg Nat .pure) := inferInstance +example : WP (FreeReader Nat) (.arg Nat .pure) := inferInstance +example : HasHandler (StateF Nat) (.arg Nat .pure) := inferInstance + +/-- Increment the natural-number state by 1. -/ +def incr : FreeState Nat Unit := do + let n ← MonadStateOf.get + MonadStateOf.set (n + 1) + +example : wp incr = wp (FreeState.toStateM incr) := + StateF.wp_FreeState_eq_wp_toStateM incr + +/-- Starting in state `n`, `incr` ends in state `n + 1`. `mvcgen` picks up the `@[spec]` lemmas +for `MonadStateOf.get`/`set` on `FreeState` and discharges the resulting arithmetic VC. -/ +example (n : Nat) : + ⦃fun s => ⌜s = n⌝⦄ (incr : FreeState Nat Unit) ⦃⇓ _ s' => ⌜s' = n + 1⌝⦄ := by + mvcgen + intro s heq + subst heq + rfl + +/-- A counter effect with two operations. -/ +inductive CounterF : Type → Type where + /-- Increment the counter by one. -/ + | tick : CounterF Unit + /-- Read the counter's value. -/ + | read : CounterF Nat + +/-- Counter programs built from `CounterF`. -/ +abbrev FreeCounter := FreeM CounterF + +namespace CounterF + +/-- Effect handler for `CounterF` into `StateM Nat`, used to seed both the executable +semantics and the logical handler. -/ +def interp : ∀ ι : Type, CounterF ι → StateM Nat ι + | _, .tick => modify (· + 1) + | _, .read => MonadStateOf.get + +/-- Logical handler for `CounterF` induced by `interp` and `Std.Do`'s `WP (StateM Nat)` +instance. -/ +def handler : LHandler CounterF (.arg Nat .pure) := + LHandler.ofInterp CounterF.interp + +instance : HasHandler CounterF (.arg Nat .pure) where + handler := CounterF.handler + +/-- Interpret counter programs as `StateM Nat` programs. -/ +abbrev toStateM {α : Type} (comp : FreeCounter α) : StateM Nat α := + comp.liftM (fun {ι} => CounterF.interp ι) + +/-- Adequacy theorem specialized to `CounterF`. -/ +theorem wp_FreeCounter_eq_wp_toStateM {α : Type} (comp : FreeCounter α) : + wp comp = wp (CounterF.toStateM comp) := + wpH_ofInterp_eq_wp_liftM (m := StateM Nat) CounterF.interp comp + +end CounterF + +/-- Smart constructor: tick the counter as a `FreeCounter` action. -/ +abbrev tick : FreeCounter Unit := lift CounterF.tick + +/-- Smart constructor: read the counter as a `FreeCounter` action. -/ +abbrev readCounter : FreeCounter Nat := lift CounterF.read + +/-- Tick three times, then read out the counter. -/ +def threeTicks : FreeCounter Nat := do + tick; tick; tick + readCounter + +/-- +Triple about the counter program: starting at `0`, the final value is `3` and the final state +is `3`. Proven by the same bridge-then-`mvcgen` pattern as `incr`. +-/ +example : + ⦃fun s => ⌜s = 0⌝⦄ threeTicks ⦃⇓ v s => ⌜v = 3 ∧ s = 3⌝⦄ := by + mvcgen + intro s seq0 + subst seq0 + exact ⟨rfl, rfl⟩ + +/-- A failure effect with one operation `fail` of empty answer type. -/ +inductive FailF : Type → Type where + /-- Abort the computation. -/ + | fail : FailF PEmpty.{1} + +/-- Logical handler for `FailF`: `fail` has precondition `⌜False⌝`, so it is only provable in +unreachable branches. -/ +def FailF.handler {ps : PostShape} : LHandler FailF ps := + fun op => match op with + | .fail => PredTrans.const spred(⌜False⌝) + +/-- A combined state + failure signature, sequencing `StateF Nat` with `FailF`. -/ +abbrev StateFail := fun α => StateF Nat α ⊕ FailF α + +/-- Handler for the combined signature: the sum of the component handlers — the paper's +`H₁ ⊕ H₂` composition. -/ +instance : HasHandler StateFail (.arg Nat .pure) where + handler := StateF.handler.sum FailF.handler + +/-- Smart constructor for state-read in the combined signature. -/ +abbrev sfGet : FreeM StateFail Nat := lift (Sum.inl StateF.get) + +/-- Smart constructor for state-write in the combined signature. -/ +abbrev sfSet (n : Nat) : FreeM StateFail PUnit := lift (Sum.inl (StateF.set n)) + +/-- Smart constructor for failure in the combined signature, eliminated to any return type via +`PEmpty.elim`. -/ +abbrev sfFail {α : Type} : FreeM StateFail α := + lift (Sum.inr FailF.fail) >>= PEmpty.elim + +/-- Hoare spec for the sum-lifted state-read. -/ +@[spec] +theorem Spec.sfGet {Q : PostCond Nat (.arg Nat .pure)} : + Triple sfGet (spred(fun s => Q.1 s s)) Q := by + mvcgen + +/-- Hoare spec for the sum-lifted state-write. -/ +@[spec] +theorem Spec.sfSet (n : Nat) {Q : PostCond PUnit (.arg Nat .pure)} : + Triple (sfSet n) (spred(fun _ => Q.1 ⟨⟩ n)) Q := by + mvcgen + +/-- Hoare spec for sum-lifted failure: requires `False` to verify. -/ +@[spec] +theorem Spec.sfFail {α : Type} {Q : PostCond α (.arg Nat .pure)} : + Triple (sfFail : FreeM StateFail α) (spred(⌜False⌝)) Q := by + mvcgen + +/-- A non-branching program in the combined signature: read the state, then write +`state + 1`. Shows that the sum handler composes the StateF and FailF specs cleanly. -/ +def getAndBump : FreeM StateFail Unit := do + let n ← sfGet + sfSet (n + 1) + +/-- `getAndBump` advances the state by 1, proven through the sum handler. -/ +example (n : Nat) : + ⦃fun s => ⌜s = n⌝⦄ (getAndBump : FreeM StateFail Unit) + ⦃⇓ _ s => ⌜s = n + 1⌝⦄ := by + mvcgen + intro s a + subst a + rfl + +/-- Increment the state if it's strictly below `limit`, otherwise fail. Branches on the state's +value and uses `sfFail` in the else branch. -/ +def bumpUnder (limit : Nat) : FreeM StateFail Unit := do + let n ← sfGet + if n < limit then sfSet (n + 1) else sfFail + +/-- Starting in a state below `limit`, `bumpUnder` increments without failing — the failure +branch is unreachable because the precondition rules it out. -/ +example (limit n : Nat) (hlt : n < limit) : + ⦃fun s => ⌜s = n⌝⦄ (bumpUnder limit : FreeM StateFail Unit) + ⦃⇓ _ s => ⌜s = n + 1⌝⦄ := by + unfold bumpUnder + mvcgen <;> aesop + +/-- Demonic non-determinism: a single operation `choice α` that abstractly returns an arbitrary +`a : α`. Verification must consider all possible values of `a`. -/ +inductive DemonicF : Type → Type 1 where + /-- Choose an element of `α`. -/ + | choice (α : Type) : DemonicF α + +/-- Logical handler for `DemonicF`: the predicate transformer for `choice α` is universal +quantification over `α`. Conjunctivity of `∀` (i.e. `∀ a, P a ∧ Q a ⊣⊢ (∀ a, P a) ∧ (∀ a, Q a)`) +is what makes this admissible in `PredTrans`. -/ +def DemonicF.handler {ps : PostShape} : LHandler DemonicF ps := + fun op => match op with + | .choice _ => + { trans := fun Q => SPred.forall (fun a => Q.1 a) + conjunctiveRaw := by + intro Q₁ Q₂ + apply SPred.bientails.iff.mpr + refine ⟨?_, ?_⟩ + · apply SPred.and_intro + · apply SPred.forall_intro + intro a + exact (SPred.forall_elim a).trans SPred.and_elim_l + · apply SPred.forall_intro + intro a + exact (SPred.forall_elim a).trans SPred.and_elim_r + · apply SPred.forall_intro + intro a + apply SPred.and_intro + · exact SPred.and_elim_l.trans (SPred.forall_elim a) + · exact SPred.and_elim_r.trans (SPred.forall_elim a) } + +instance : HasHandler DemonicF .pure where + handler := DemonicF.handler + +/-- Smart constructor for demonic choice over `α`. -/ +abbrev demonic (α : Type) : FreeM DemonicF α := lift (DemonicF.choice α) + +/-- Triple for `demonic α`: the precondition must imply the postcondition for *every* `a : α`. -/ +@[spec] +theorem Spec.demonic {α : Type} {Q : PostCond α .pure} : + Triple (demonic α) (SPred.forall (fun a : α => Q.1 a)) Q := + Triple.iff.mpr SPred.entails.rfl + +/-- A demonic Bool: the precondition must hold for both `true` and `false`. -/ +example {Q : PostCond Bool .pure} : + Triple (demonic Bool) (SPred.and (Q.1 true) (Q.1 false)) Q := + fun ⟨ht, hf⟩ b => + match b with + | true => ht + | false => hf + +end AlgoleanTests.FreeMonadWP From 2f956bd2732538e772870c785349d82d67360710 Mon Sep 17 00:00:00 2001 From: Tanner Duve Date: Tue, 2 Jun 2026 14:11:01 -0700 Subject: [PATCH 2/7] fix(FreeWP): state simp lemmas in simp-normal form, drop unused LawfulMonad Restate wpH_pure/wpH_liftBind/wpH_bind on the FreeM constructor forms that Cslib's simp set normalizes to, un-simp wpH_lift (mirroring liftM_lift), and remove the LawfulMonad instance unused by the adequacy proof. --- Algolean/FreeWP/WP.lean | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/Algolean/FreeWP/WP.lean b/Algolean/FreeWP/WP.lean index 7dcdc6c..7782f65 100644 --- a/Algolean/FreeWP/WP.lean +++ b/Algolean/FreeWP/WP.lean @@ -83,25 +83,25 @@ def wpH (H : LHandler F ps) (x : FreeM F α) : PredTrans ps α := x.liftM H @[simp] theorem wpH_pure (H : LHandler F ps) (a : α) : - wpH H (pure a : FreeM F α) = Pure.pure a := rfl + wpH H (.pure a : FreeM F α) = Pure.pure a := rfl @[simp] theorem wpH_liftBind (H : LHandler F ps) {ι : Type u} (op : F ι) (k : ι → FreeM F α) : - wpH H (lift op >>= k) = H op >>= fun x => wpH H (k x) := rfl + wpH H (liftBind op k) = H op >>= fun x => wpH H (k x) := rfl -@[simp] theorem wpH_lift (H : LHandler F ps) {ι : Type u} (op : F ι) : +theorem wpH_lift (H : LHandler F ps) {ι : Type u} (op : F ι) : wpH H (lift op : FreeM F ι) = H op := liftM_lift _ op @[simp] theorem wpH_bind (H : LHandler F ps) (x : FreeM F α) (f : α → FreeM F β) : - wpH H (x >>= f) = wpH H x >>= fun a => wpH H (f a) := + wpH H (x.bind f) = wpH H x >>= fun a => wpH H (f a) := liftM_bind _ x f /-- Adequacy theorem: WP via `FreeM` against an `ofInterp`-derived handler agrees with `Std.Do`'s WP of the `liftM` interpretation. Equivalently, two monad morphisms `FreeM F → PredTrans ps` extending the same handler are equal. -/ theorem wpH_ofInterp_eq_wp_liftM - {m : Type u → Type w} [Monad m] [LawfulMonad m] [WPMonad m ps] + {m : Type u → Type w} [Monad m] [WPMonad m ps] (interp : ∀ ι : Type u, F ι → m ι) (x : FreeM F α) : wpH (LHandler.ofInterp interp) x = wp (x.liftM (fun {_} => interp _)) := by induction x with From efbf619cbaba2485a529a772534e203d2b505c7a Mon Sep 17 00:00:00 2001 From: Tanner Duve Date: Wed, 3 Jun 2026 11:05:02 -0700 Subject: [PATCH 3/7] test(FreeWP): add query-model WP examples on ReadOnlyVec MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Connect the FreeM weakest-precondition framework to the repo's query model (Prog Q α := FreeM Q α): derive a logical handler from a Model Q Cost via evalQuery, register it for ReadOnlyVec, and prove an adequacy theorem plus mvcgen-discharged Hoare triples over query programs. --- AlgoleanTests/FreeMonadWP.lean | 70 +++++++++++++++++++++++++++++++++- 1 file changed, 68 insertions(+), 2 deletions(-) diff --git a/AlgoleanTests/FreeMonadWP.lean b/AlgoleanTests/FreeMonadWP.lean index 76f5bf1..c8d326b 100644 --- a/AlgoleanTests/FreeMonadWP.lean +++ b/AlgoleanTests/FreeMonadWP.lean @@ -7,12 +7,15 @@ Authors: Tanner Duve module public import Algolean.FreeWP.Effects +public import Algolean.Models.ReadOnlyVec public import Std.Tactic.Do /-! Examples for WP in `Algolean.FreeWP.WP`: instance resolution, -a `Triple` on a `FreeState` program discharged by `mvcgen`, and a custom `CounterF` effect with -its own logical handler. +a `Triple` on a `FreeState` program discharged by `mvcgen`, a custom `CounterF` effect with +its own logical handler, sum/failure/demonic effects, and — connecting the WP framework to this +repository's query model — Hoare triples about query-model programs `Prog Q α` against a handler +derived from a `Model Q Cost` (illustrated on `ReadOnlyVec`). -/ @[expose] public section @@ -231,4 +234,67 @@ example {Q : PostCond Bool .pure} : | true => ht | false => hf +/-! ### Query-model programs + +The repository's query model defines `Prog Q α := FreeM Q α`, so the WP framework applies to +query-model algorithms verbatim — `Prog` *is* a `FreeM` program. The missing piece is a logical +handler: a `Model Q Cost` already carries an interpreter `evalQuery : Q ι → ι`, and reading it +as an interpreter into `Id` gives a handler at the pure post-shape `.pure`, against which we can +state Hoare triples about the *result value* a query program computes under that model. + +We illustrate with `ReadOnlyVec`, the query type for read-only vector access, and its canonical +cost model `ReadOnlyVec.natCost`. -/ + +open Algolean Algolean.Algorithms + +/-- The logical handler induced by a `Model Q Cost`: interpret each query through the model's +`evalQuery` into `Id` (where `pure` is the identity), then take its WP at the pure post-shape. +This is the bridge that turns the query model into a `Std.Do` effect, so `mvcgen`/`Triple` +reasoning works on any `Prog Q α`. -/ +def modelHandler {Q : Type → Type} {Cost : Type} (M : Model Q Cost) : LHandler Q .pure := + LHandler.ofInterp (m := Id) (fun _ q => M.evalQuery q) + +/-- Register `ReadOnlyVec.natCost` as the default handler for read-only-vector programs, so the +global `WP (Prog (ReadOnlyVec α)) .pure` instance fires. -/ +instance instHasHandlerReadOnlyVec {α : Type} : HasHandler (ReadOnlyVec α) .pure where + handler := modelHandler ReadOnlyVec.natCost + +/-- Adequacy for the query model: the WP of a `ReadOnlyVec` program agrees with the WP of its +`Id`-interpretation under `natCost`, i.e. with what the program actually `eval`uates to. -/ +theorem ReadOnlyVec.wp_eq_wp_interp {α β : Type} (P : Prog (ReadOnlyVec α) β) : + wp P = wp (P.liftM (fun {_} q => (ReadOnlyVec.natCost.evalQuery q : Id _))) := + wpH_ofInterp_eq_wp_liftM (m := Id) + (fun _ q => ReadOnlyVec.natCost.evalQuery q) P + +/-- Hoare spec for a single read: to establish postcondition `Q` after `read a i`, it suffices +that `Q` holds of the value `a[i]` that the model returns. -/ +@[spec] +theorem Spec.read_ReadOnlyVec {α : Type} {n : Nat} (a : Vector α n) (i : Fin n) + {Q : PostCond α .pure} : + Triple (ReadOnlyVec.read a i : Prog (ReadOnlyVec α) α) + (Q.1 a[i]) Q := + Triple.iff.mpr SPred.entails.rfl + +/-- Read indices `i` then `j` of a vector and return the pair of values. Queries lift into `Prog` +automatically through the `CoeOut` coercion, so no explicit `lift` is needed. -/ +def readTwo {α : Type} {n : Nat} (a : Vector α n) (i j : Fin n) : + Prog (ReadOnlyVec α) (α × α) := do + let x ← ReadOnlyVec.read a i + let y ← ReadOnlyVec.read a j + pure (x, y) + +/-- Functional correctness of `readTwo`: it returns exactly `(a[i], a[j])`. The two `read` +specs compose through the `bind` rule, and `mvcgen` discharges the program. -/ +example {α : Type} {n : Nat} (a : Vector α n) (i j : Fin n) : + ⦃⌜True⌝⦄ (readTwo a i j) ⦃⇓ r => ⌜r = (a[i], a[j])⌝⦄ := by + mvcgen + +/-- A read program whose result depends on the data: read index `i`, and if the value equals +`x`, the answer is `true`. The triple shows the verifier sees the concrete element `a[i]`. -/ +example {n : Nat} (a : Vector Nat n) (i : Fin n) (x : Nat) : + ⦃⌜True⌝⦄ + (do let v ← ReadOnlyVec.read a i; pure (v == x) : Prog (ReadOnlyVec Nat) Bool) + ⦃⇓ r => ⌜r = (a[i] == x)⌝⦄ := by + mvcgen + end AlgoleanTests.FreeMonadWP From 9e1b49ebbdad2204182c228af0350ebdfccab311 Mon Sep 17 00:00:00 2001 From: Tanner Duve Date: Thu, 4 Jun 2026 15:09:47 -0700 Subject: [PATCH 4/7] =?UTF-8?q?feat(QueryModel):=20generic=20Model?= =?UTF-8?q?=E2=86=92WP=20bridge=20+=20verified=20bubble=20sort=20demo?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Move the weakest-precondition bridge out of the test file and generalize it in QueryModel.lean: `Model.handler`, a `HasModel` class with a single generic `HasHandler` instance, the `Spec.query` rule, adequacy (`Model.wp_eq_wp_interp`), and `eval_of_triple`. Register `HasModel` for `ReadOnlyVec`/`Vec`. The handler reasons about the result value only (`.pure`), so it needs no algebra on `Cost`. Add Algolean/Algorithms/VecBubbleSort.lean: bubble sort in `Prog (Vec α)` using read/write, proved fully correct via `mvcgen` (`bubbleSort_perm`, `bubbleSort_sorted`). Split into `bubblePass` + `bubbleSort`, each a single-loop mvcgen proof composed through `bubblePass_spec` — the worked non-trivial mvcgen example for the query model. Slim FreeMonadWP.lean down to the ReadOnlyVec examples using the generalized infra. --- Algolean.lean | 1 + Algolean/Algorithms/VecBubbleSort.lean | 247 +++++++++++++++++++++++++ Algolean/Models/ReadOnlyVec.lean | 6 + Algolean/Models/ReadWriteVec.lean | 11 ++ Algolean/QueryModel.lean | 69 +++++++ AlgoleanTests/FreeMonadWP.lean | 50 ++--- 6 files changed, 351 insertions(+), 33 deletions(-) create mode 100644 Algolean/Algorithms/VecBubbleSort.lean diff --git a/Algolean.lean b/Algolean.lean index 0db1429..b4fa103 100644 --- a/Algolean.lean +++ b/Algolean.lean @@ -8,6 +8,7 @@ public import Algolean.Algorithms.ListLinearSearch public import Algolean.Algorithms.ListOrderedInsert public import Algolean.Algorithms.MergeSort public import Algolean.Algorithms.NaivePatternSearch +public import Algolean.Algorithms.VecBubbleSort public import Algolean.Algorithms.VecSearch public import Algolean.Complexity.Basic public import Algolean.Complexity.PolytimeBasicClasses diff --git a/Algolean/Algorithms/VecBubbleSort.lean b/Algolean/Algorithms/VecBubbleSort.lean new file mode 100644 index 0000000..c6cc3cd --- /dev/null +++ b/Algolean/Algorithms/VecBubbleSort.lean @@ -0,0 +1,247 @@ +/- +Copyright (c) 2026 Tanner Duve (Logical Intelligence). All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Tanner Duve +-/ + +module + +public import Algolean.Models.ReadWriteVec +public import Mathlib.Data.List.Sort +public import Std.Tactic.Do + +@[expose] public section + +/-! +# Bubble sort in the read/write vector query model + +Bubble sort written as a program in the `Vec` query model (`Prog (Vec α)`), using `read` and +`write` queries against a mutable vector threaded through `for` loops. This is the worked example +the query-model WP framework is built for: a *non-trivial* `mvcgen` development establishing full +functional correctness — both that the output is a permutation of the input and that it is sorted. + +The algorithm is split into two pieces, each verified with its own single-loop `mvcgen` proof and +composed through a Hoare-triple spec (`bubblePass_spec`), which is the idiomatic way to keep loop +reasoning modular: + +- `bubblePass` makes one left-to-right sweep over `[0, bound]`, bubbling the largest element of + that range up to position `bound`. +- `bubbleSort` runs `n` such passes with shrinking bounds `n-1, n-2, …`, growing a sorted suffix. + +## Main definitions + +- `bubblePass` : one bubbling sweep in the `Vec` query model. +- `bubbleSort` : bubble sort in the `Vec` query model. + +## Main results + +- `bubbleSort_perm` : `bubbleSort` returns a permutation of its input. +- `bubbleSort_sorted` : `bubbleSort` returns a sorted vector (for a total, transitive `le`). +-/ + +namespace Algolean + +namespace Algorithms + +open Cslib Prog Std.Do + +set_option mvcgen.warning false + +/-- +One bubbling sweep in the `Vec` query model: for each adjacent pair `v[j], v[j+1]` with +`j < bound`, read both and, if out of order under `le`, write them back swapped. After the sweep +the largest element of `[0, bound]` sits at position `bound`. +-/ +def bubblePass (le : α → α → Bool) (bound : Nat) (hb : bound < n) (v : Vector α n) : + Prog (Vec α) (Vector α n) := do + let mut v := v + for j in List.finRange bound do + let a ← (Vec.read v ⟨j, by omega⟩ : Prog (Vec α) α) + let b ← (Vec.read v ⟨j + 1, by omega⟩ : Prog (Vec α) α) + if !le a b then + v ← (Vec.write v ⟨j, by omega⟩ b : Prog (Vec α) (Vector α n)) + v ← (Vec.write v ⟨j + 1, by omega⟩ a : Prog (Vec α) (Vector α n)) + return v + +/-- +Bubble sort in the `Vec` query model: run `n` bubbling passes with shrinking bounds. After the +`k`-th pass the last `k` positions hold the `k` largest elements in sorted order. +-/ +def bubbleSort (le : α → α → Bool) (v : Vector α n) : Prog (Vec α) (Vector α n) := do + let mut v := v + for i in List.finRange n do + v ← bubblePass le (n - 1 - i) (by omega) v + return v + +/-! ### Invariants and pointwise lemmas + +`MaxAt le w m` says `w[m]` dominates the prefix `[0, m]`; `SortedFrom le w b` says positions +`[b, n)` are sorted and dominated by the whole prefix. These are the loop invariants, with the +pointwise lemmas below feeding `mvcgen`'s verification conditions. -/ + +variable {α : Type} {n : Nat} + +/-- `w[m]` is `≥` everything in the prefix `[0, m]`. -/ +def MaxAt (le : α → α → Bool) (w : Vector α n) (m : Nat) : Prop := + ∀ p q : Fin n, (p : Nat) ≤ m → (q : Nat) = m → le w[p] w[q] = true + +/-- Positions `[b, n)` are sorted and dominated by the whole prefix. -/ +def SortedFrom (le : α → α → Bool) (w : Vector α n) (b : Nat) : Prop := + ∀ p q : Fin n, (p : Nat) ≤ (q : Nat) → b ≤ (q : Nat) → le w[p] w[q] = true + +/-- In a `finRange` split, the cursor element sits at the prefix length. -/ +private theorem fin_cur_eq {pref suff : List (Fin n)} {cur : Fin n} + (h : List.finRange n = pref ++ cur :: suff) : (cur : Nat) = pref.length := by + have hlt : pref.length < n := by have := congrArg List.length h; simp at this; omega + have h2 := congrArg (fun l => l[pref.length]?) h + simp only [List.getElem?_append_right (Nat.le_refl pref.length), Nat.sub_self, + List.getElem?_cons_zero, List.getElem_finRange, + List.getElem?_eq_getElem (show pref.length < (List.finRange n).length by simpa using hlt)] at h2 + exact (congrArg Fin.val (Option.some.inj h2)).symm + +/-- Swapping two entries permutes the underlying list. -/ +private lemma set_set_toList_perm (w : Vector α n) (i j : Nat) (hi : i < n) (hj : j < n) : + ((w.set i (w[j]'hj) hi).set j (w[i]'hi) hj).toList.Perm w.toList := by + simpa [Vector.toList_set, Vector.getElem_toList] using + List.set_set_perm (as := w.toList) (by simpa using hi) (by simpa using hj) + +/-- After swapping out-of-order `w[m], w[m+1]`, the prefix maximum moves to `m+1`. -/ +private lemma maxAt_swap (le : α → α → Bool) (htot : ∀ a b : α, le a b = true ∨ le b a = true) + (w : Vector α n) (m : Nat) (hm : m + 1 < n) (hmax : MaxAt le w m) + (hsw : le (w[m]'(by omega)) (w[m + 1]'hm) = false) : + MaxAt le ((w.set m (w[m + 1]'hm) (by omega)).set (m + 1) (w[m]'(by omega)) hm) (m + 1) := by + intro p q hp hq + have hcmp := (htot (w[m]'(by omega)) (w[m + 1]'hm)).resolve_left (by simp [hsw]) + have key : ∀ r : Fin n, (r : Nat) ≤ m → le w[r] (w[m]'(by omega)) = true := + fun r hr => hmax r ⟨m, by omega⟩ hr rfl + grind + +/-- When the pair is already in order, the prefix maximum still extends to `m+1`. -/ +private lemma maxAt_noswap (le : α → α → Bool) (htot : ∀ a b : α, le a b = true ∨ le b a = true) + (htr : ∀ a b c : α, le a b = true → le b c = true → le a c = true) + (w : Vector α n) (m : Nat) (hm : m + 1 < n) (hmax : MaxAt le w m) + (hns : le (w[m]'(by omega)) (w[m + 1]'hm) = true) : MaxAt le w (m + 1) := by + intro p q hp hq + have key : ∀ r : Fin n, (r : Nat) ≤ m → le w[r] (w[m]'(by omega)) = true := + fun r hr => hmax r ⟨m, by omega⟩ hr rfl + grind + +/-- A swap strictly below the boundary `b` preserves the sorted suffix `[b, n)`. -/ +private lemma sortedFrom_swap (le : α → α → Bool) (w : Vector α n) (m b : Nat) + (hm : m + 1 < n) (hmb : m + 1 < b) (hsort : SortedFrom le w b) : + SortedFrom le ((w.set m (w[m + 1]'hm) (by omega)).set (m + 1) (w[m]'(by omega)) hm) b := by + intro p q hp hq + have e_m := hsort ⟨m, by omega⟩ q (show m ≤ (q : Nat) by omega) hq + have e_m1 := hsort ⟨m + 1, hm⟩ q (show m + 1 ≤ (q : Nat) by omega) hq + have hpq := hsort p q hp hq + grind + +/-- The prefix maximum at `k` extends a sorted suffix `[k+1, n)` to `[k, n)`. -/ +private lemma sortedFrom_of_maxAt (le : α → α → Bool) (w : Vector α n) (k : Nat) + (hmax : MaxAt le w k) (hsort : SortedFrom le w (k + 1)) : SortedFrom le w k := by + intro p q hp hq + rcases Nat.lt_or_ge (q : Nat) (k + 1) with h | h + · exact hmax p q (by omega) (by omega) + · exact hsort p q hp h + +/-- The prefix maximum at `0` is trivial: `w[0] ≥ w[0]`. -/ +private lemma maxAt_zero (le : α → α → Bool) (hrefl : ∀ a, le a a = true) (w : Vector α n) : + MaxAt le w 0 := fun p q hp hq => by obtain rfl : p = q := by ext; omega + exact hrefl _ + +/-- `SortedFrom le w 0` is exactly sortedness of the underlying list. -/ +private lemma sortedFrom_zero_pairwise {le : α → α → Bool} {w : Vector α n} + (h : SortedFrom le w 0) : w.toList.Pairwise (fun a b => le a b = true) := by + rw [List.pairwise_iff_getElem] + intro i j hi hj _ + simpa [Vector.getElem_toList] using + h ⟨i, by simpa using hi⟩ ⟨j, by simpa using hj⟩ (by simp; omega) (Nat.zero_le _) + +private lemma sub_one_sub_add (k : Nat) (h : k < n) : n - 1 - k + 1 = n - k := by omega +private lemma sub_succ (k : Nat) : n - (k + 1) = n - 1 - k := by omega + +/-! ### Hoare specs via `mvcgen` + +The two single-loop proofs that carry the work: each calls `mvcgen` with one hand-supplied loop +invariant, then discharges the (concrete, `grind`-friendly) verification conditions. -/ + +set_option mvcgen.warning false in +/-- One pass deposits the maximum of `[0, bound]` at `bound`, preserves the sorted suffix above, +and permutes the vector. -/ +theorem bubblePass_spec (le : α → α → Bool) (htot : ∀ a b : α, le a b = true ∨ le b a = true) + (htr : ∀ a b c : α, le a b = true → le b c = true → le a c = true) + (bound : Nat) (hb : bound < n) (v : Vector α n) (hpre : SortedFrom le v (bound + 1)) : + ⦃⌜True⌝⦄ bubblePass le bound hb v + ⦃⇓w => ⌜MaxAt le w bound ∧ SortedFrom le w (bound + 1) ∧ w.toList.Perm v.toList⌝⦄ := by + have hrefl : ∀ a, le a a = true := fun a => (htot a a).elim id id + mvcgen [bubblePass] invariants + · ⇓⟨xs, w⟩ => ⌜MaxAt le w xs.prefix.length ∧ SortedFrom le w (bound + 1) + ∧ w.toList.Perm v.toList⌝ + case vc3.pre => + simp only [List.length_nil] + exact ⟨maxAt_zero le hrefl v, hpre, List.Perm.refl _⟩ + case vc4.post.success => + obtain ⟨h1, h2, h3⟩ := ‹MaxAt le _ _ ∧ SortedFrom le _ _ ∧ List.Perm _ _› + rw [List.length_finRange] at h1 + exact ⟨h1, h2, h3⟩ + case vc1.step.isTrue => + obtain ⟨hmax, hsort, hperm⟩ := ‹MaxAt le _ _ ∧ SortedFrom le _ _ ∧ List.Perm _ _› + have hc := fin_cur_eq ‹List.finRange bound = _ ++ _ :: _› + have hcb := (‹Fin bound› : Fin bound).isLt + have hcmp := ‹(!le _ _) = true› + simp only [Vec.hasModel_model, Bool.not_eq_true', + List.length_append, List.length_cons, List.length_nil, ← hc] at hmax hcmp hcb ⊢ + exact ⟨maxAt_swap le htot _ _ (by grind) hmax hcmp, + sortedFrom_swap le _ _ _ (by grind) (by grind) hsort, + (set_set_toList_perm _ _ _ (by grind) (by grind)).trans hperm⟩ + case vc2.step.isFalse => + obtain ⟨hmax, hsort, hperm⟩ := ‹MaxAt le _ _ ∧ SortedFrom le _ _ ∧ List.Perm _ _› + have hc := fin_cur_eq ‹List.finRange bound = _ ++ _ :: _› + have hcb := (‹Fin bound› : Fin bound).isLt + have hns := ‹¬(!le _ _) = true› + simp only [Vec.hasModel_model, Bool.not_eq_true, + Bool.not_eq_false', List.length_append, List.length_cons, List.length_nil, ← hc] + at hmax hns hcb ⊢ + exact ⟨maxAt_noswap le htot htr _ _ (by omega) hmax hns, hsort, hperm⟩ + +set_option mvcgen.warning false in +/-- `bubbleSort` is correct: it sorts and permutes its input (for a total, transitive `le`). -/ +theorem bubbleSort_spec (le : α → α → Bool) (htot : ∀ a b : α, le a b = true ∨ le b a = true) + (htr : ∀ a b c : α, le a b = true → le b c = true → le a c = true) (v : Vector α n) : + ⦃⌜True⌝⦄ bubbleSort le v ⦃⇓w => ⌜SortedFrom le w 0 ∧ w.toList.Perm v.toList⌝⦄ := by + mvcgen [bubbleSort, bubblePass_spec] invariants + · ⇓⟨xs, w⟩ => ⌜SortedFrom le w (n - xs.prefix.length) ∧ w.toList.Perm v.toList⌝ + case vc3.hpre => + have hsort := (‹SortedFrom le _ _ ∧ List.Perm _ _›).1 + have hcb := (‹Fin n› : Fin n).isLt + rw [fin_cur_eq ‹List.finRange n = _ ++ _ :: _›] at hcb ⊢ + rwa [sub_one_sub_add _ hcb] + case vc4.step.success => + obtain ⟨hmax, hsort, hperm⟩ := ‹MaxAt le _ _ ∧ SortedFrom le _ _ ∧ List.Perm _ _› + have hperm0 := (‹SortedFrom le _ _ ∧ List.Perm _ _›).2 + have key := sortedFrom_of_maxAt le _ _ hmax hsort + rw [fin_cur_eq ‹List.finRange n = _ ++ _ :: _›] at key + exact ⟨by simp only [List.length_append, List.length_cons, List.length_nil]; rwa [sub_succ], + hperm.trans hperm0⟩ + case vc5.pre => + exact ⟨fun p q _ hq => absurd (by simpa using hq) (by have := q.isLt; omega), List.Perm.refl _⟩ + case vc6.post.success => + obtain ⟨h1, h2⟩ := ‹SortedFrom le _ _ ∧ List.Perm _ _› + rw [List.length_finRange, Nat.sub_self] at h1 + exact ⟨h1, h2⟩ + +/-- `bubbleSort` returns a permutation of its input. -/ +theorem bubbleSort_perm (le : α → α → Bool) (htot : ∀ a b : α, le a b = true ∨ le b a = true) + (htr : ∀ a b c : α, le a b = true → le b c = true → le a c = true) (v : Vector α n) : + ((bubbleSort le v).eval Vec.natCost).toList.Perm v.toList := + (eval_of_triple (bubbleSort_spec le htot htr v)).2 + +/-- `bubbleSort` returns a sorted vector, for a total and transitive `le`. -/ +theorem bubbleSort_sorted (le : α → α → Bool) (htot : ∀ a b : α, le a b = true ∨ le b a = true) + (htr : ∀ a b c : α, le a b = true → le b c = true → le a c = true) (v : Vector α n) : + ((bubbleSort le v).eval Vec.natCost).toList.Pairwise (fun a b => le a b = true) := + sortedFrom_zero_pairwise (eval_of_triple (bubbleSort_spec le htot htr v)).1 + +end Algorithms + +end Algolean diff --git a/Algolean/Models/ReadOnlyVec.lean b/Algolean/Models/ReadOnlyVec.lean index be911d8..3684da7 100644 --- a/Algolean/Models/ReadOnlyVec.lean +++ b/Algolean/Models/ReadOnlyVec.lean @@ -44,6 +44,12 @@ def ReadOnlyVec.natCost : Model (ReadOnlyVec α) ℕ where | .read a i => a[i] cost _ := 1 +/-- Register `natCost` as the default model for `ReadOnlyVec`, so the global +`WP (Prog (ReadOnlyVec α)) .pure` / `HasHandler` instances fire and `Triple`/`mvcgen` reasoning +works on read-only-vector programs out of the box. -/ +instance : HasModel (ReadOnlyVec α) ℕ where + model := ReadOnlyVec.natCost + end Algorithms end Algolean diff --git a/Algolean/Models/ReadWriteVec.lean b/Algolean/Models/ReadWriteVec.lean index 007b81e..ad2e431 100644 --- a/Algolean/Models/ReadWriteVec.lean +++ b/Algolean/Models/ReadWriteVec.lean @@ -49,6 +49,17 @@ def Vec.natCost : Model (Vec α) ℕ where | .write a i x => a.set i x cost _ := 1 +/-- Register `natCost` as the default model for `Vec`, so the global +`WP (Prog (Vec α)) .pure` / `HasHandler` instances fire and `Triple`/`mvcgen` reasoning works on +read/write-vector programs out of the box. Both `Vec` cost models share the same `evalQuery`, so +this choice fixes only the functional semantics used by the weakest-precondition handler. -/ +instance : HasModel (Vec α) ℕ where + model := Vec.natCost + +/-- The default `Vec` model unfolds to `natCost`; lets `mvcgen` reduce `evalQuery` on `Vec` +programs to concrete `read`/`write` semantics. -/ +@[simp] theorem Vec.hasModel_model : (HasModel.model : Model (Vec α) ℕ) = Vec.natCost := rfl + section VecModel diff --git a/Algolean/QueryModel.lean b/Algolean/QueryModel.lean index 991563b..b307b07 100644 --- a/Algolean/QueryModel.lean +++ b/Algolean/QueryModel.lean @@ -9,6 +9,7 @@ module public import Cslib public import Cslib.Foundations.Control.Monad.Free public import Algolean.AddWriter.Basic +public import Algolean.FreeWP.WP @[expose] public section @@ -206,6 +207,74 @@ theorem FreeM.bind_eq_bind {α β : Type w} end FreeMExtras +section WeakestPrecondition +/-! +## Weakest preconditions for query programs + +A `Prog Q α` is by definition a `FreeM Q α`, so the weakest-precondition framework of +`Algolean.FreeWP.WP` applies to query-model algorithms verbatim. The bridge is a *logical handler* +read off a model: a `Model Q Cost` already carries an interpreter `evalQuery : Q ι → ι`, and viewing +that as an interpreter into `Id` produces a handler at the pure post-shape `.pure`, against which +we can state Hoare triples about the *result value* a program computes under the model. + +The cost field plays no role here — `.pure` tracks only the returned value — so the construction +works for a model over *any* cost type, with no algebraic structure required. To register a query +type's canonical model as the default for `mvcgen`/`Triple` reasoning, provide a `HasModel` +instance; the global `WP (Prog Q) .pure` instance then fires automatically. +-/ + +open Cslib Cslib.FreeM Std.Do + +variable {Q : Type u → Type v} {Cost : Type w} {ι α : Type u} + +/-- The logical handler induced by a model `M : Model Q Cost`: interpret each query through +`M.evalQuery` into `Id` (where `pure` is the identity), then take its weakest precondition at the +pure post-shape. This is the bridge that turns a query model into a `Std.Do` effect, so +`mvcgen`/`Triple` reasoning works on any `Prog Q α`. -/ +def Model.handler (M : Model Q Cost) : LHandler Q .pure := + LHandler.ofInterp (m := Id) (fun _ q => M.evalQuery q) + +/-- A query type equipped with a designated default cost model. Registering an instance lets the +generic `HasHandler`/`WP (Prog Q) .pure` instances fire, so query programs plug into +`Std.Do`'s `Triple`/`mvcgen` infrastructure with no per-type boilerplate. -/ +class HasModel (Q : Type u → Type v) (Cost : outParam (Type w)) where + /-- The designated default model for `Q`. -/ + model : Model Q Cost + +/-- Generic handler instance: every query type with a default `HasModel` gets the WP framework at +the pure post-shape, induced by that model. This is the single instance that "generates" a handler +for an arbitrary model. -/ +instance instHasHandlerOfModel [HasModel Q Cost] : HasHandler Q .pure where + handler := (HasModel.model (Cost := Cost)).handler + +/-- Adequacy for the query model: the WP of a query program against a model's handler agrees with +`Std.Do`'s WP of its `Id`-interpretation under that model — i.e. with what the program +`eval`uates to. -/ +theorem Model.wp_eq_wp_interp (M : Model Q Cost) (P : Prog Q α) : + wpH M.handler P = wp (P.liftM (fun {_} q => (M.evalQuery q : Id _))) := + wpH_ofInterp_eq_wp_liftM (m := Id) (fun _ q => M.evalQuery q) P + +/-- The single-query Hoare spec, generic over any registered model: to establish postcondition `Q'` +after running a query `q`, it suffices that `Q'` holds of the value `HasModel.model.evalQuery q` +that the model returns. Tagged `@[spec]` so `mvcgen` discharges every lifted query automatically. -/ +@[spec] +theorem Spec.query [HasModel Q Cost] (q : Q ι) {Q' : PostCond ι .pure} : + Triple (FreeM.lift q : Prog Q ι) + (Q'.1 ((HasModel.model : Model Q Cost).evalQuery q)) Q' := + Triple.iff.mpr SPred.entails.rfl + +/-- Adequacy bridge: a pure-shape Hoare triple with trivial precondition yields a fact about the +value the program `eval`uates to under the registered model. This turns an `mvcgen` proof about a +`Prog Q` program directly into a statement about `Prog.eval`. -/ +theorem eval_of_triple [HasModel Q Cost] {prog : Prog Q α} {φ : α → Prop} + (h : ⦃⌜True⌝⦄ prog ⦃⇓r => ⌜φ r⌝⦄) : + φ (prog.eval (HasModel.model : Model Q Cost)) := + Id.of_wp_run_eq + (prog := prog.liftM (fun {_} q => ((HasModel.model : Model Q Cost).evalQuery q : Id _))) + rfl φ (by rw [← (HasModel.model : Model Q Cost).wp_eq_wp_interp prog]; exact h) + +end WeakestPrecondition + end Algorithms end Algolean diff --git a/AlgoleanTests/FreeMonadWP.lean b/AlgoleanTests/FreeMonadWP.lean index c8d326b..7ea6364 100644 --- a/AlgoleanTests/FreeMonadWP.lean +++ b/AlgoleanTests/FreeMonadWP.lean @@ -236,44 +236,28 @@ example {Q : PostCond Bool .pure} : /-! ### Query-model programs -The repository's query model defines `Prog Q α := FreeM Q α`, so the WP framework applies to -query-model algorithms verbatim — `Prog` *is* a `FreeM` program. The missing piece is a logical -handler: a `Model Q Cost` already carries an interpreter `evalQuery : Q ι → ι`, and reading it -as an interpreter into `Id` gives a handler at the pure post-shape `.pure`, against which we can -state Hoare triples about the *result value* a query program computes under that model. +The repository's query model defines `Prog Q α := FreeM Q α`, and `Algolean.QueryModel` wires every +query model into this WP framework: `Model.handler` reads a logical handler off a model's +`evalQuery` at the pure post-shape, a `HasModel` instance registers a query type's default model, +and the generic `Spec.query` discharges single queries under `mvcgen`. So Hoare triples about the +*result value* a query program computes are available with no per-example setup. -We illustrate with `ReadOnlyVec`, the query type for read-only vector access, and its canonical -cost model `ReadOnlyVec.natCost`. -/ +We illustrate with `ReadOnlyVec`, whose `HasModel (ReadOnlyVec α) ℕ` instance (via +`ReadOnlyVec.natCost`, in `Algolean.Models.ReadOnlyVec`) makes the global +`WP (Prog (ReadOnlyVec α)) .pure` instance fire automatically. -/ open Algolean Algolean.Algorithms -/-- The logical handler induced by a `Model Q Cost`: interpret each query through the model's -`evalQuery` into `Id` (where `pure` is the identity), then take its WP at the pure post-shape. -This is the bridge that turns the query model into a `Std.Do` effect, so `mvcgen`/`Triple` -reasoning works on any `Prog Q α`. -/ -def modelHandler {Q : Type → Type} {Cost : Type} (M : Model Q Cost) : LHandler Q .pure := - LHandler.ofInterp (m := Id) (fun _ q => M.evalQuery q) - -/-- Register `ReadOnlyVec.natCost` as the default handler for read-only-vector programs, so the -global `WP (Prog (ReadOnlyVec α)) .pure` instance fires. -/ -instance instHasHandlerReadOnlyVec {α : Type} : HasHandler (ReadOnlyVec α) .pure where - handler := modelHandler ReadOnlyVec.natCost - -/-- Adequacy for the query model: the WP of a `ReadOnlyVec` program agrees with the WP of its -`Id`-interpretation under `natCost`, i.e. with what the program actually `eval`uates to. -/ -theorem ReadOnlyVec.wp_eq_wp_interp {α β : Type} (P : Prog (ReadOnlyVec α) β) : - wp P = wp (P.liftM (fun {_} q => (ReadOnlyVec.natCost.evalQuery q : Id _))) := - wpH_ofInterp_eq_wp_liftM (m := Id) - (fun _ q => ReadOnlyVec.natCost.evalQuery q) P +/-- The WP framework is available on query programs with no local setup — the handler instance is +generated from the registered model. -/ +example {α : Type} : WP (Prog (ReadOnlyVec α)) .pure := inferInstance -/-- Hoare spec for a single read: to establish postcondition `Q` after `read a i`, it suffices -that `Q` holds of the value `a[i]` that the model returns. -/ -@[spec] -theorem Spec.read_ReadOnlyVec {α : Type} {n : Nat} (a : Vector α n) (i : Fin n) - {Q : PostCond α .pure} : - Triple (ReadOnlyVec.read a i : Prog (ReadOnlyVec α) α) - (Q.1 a[i]) Q := - Triple.iff.mpr SPred.entails.rfl +/-- Adequacy, specialized to `ReadOnlyVec` from the generic `Model.wp_eq_wp_interp`: the WP of a +program agrees with the WP of its `Id`-interpretation under `natCost`, i.e. with what the program +actually `eval`uates to. -/ +example {α β : Type} (P : Prog (ReadOnlyVec α) β) : + wp P = wp (P.liftM (fun {_} q => (ReadOnlyVec.natCost.evalQuery q : Id _))) := + ReadOnlyVec.natCost.wp_eq_wp_interp P /-- Read indices `i` then `j` of a vector and return the pair of values. Queries lift into `Prog` automatically through the `CoeOut` coercion, so no explicit `lift` is needed. -/ From f2716186fbf4874599d527a2b7615432a2046a80 Mon Sep 17 00:00:00 2001 From: Tanner Duve Date: Thu, 4 Jun 2026 16:43:04 -0700 Subject: [PATCH 5/7] refactor(VecBubbleSort): use Std order typeclasses; module docstring before section MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Address review: replace the explicit totality/transitivity hypotheses on the public `bubblePass_spec`/`bubbleSort_spec`/`bubbleSort_perm`/`bubbleSort_sorted` with `[Std.Total (fun a b => le a b = true)]` / `[IsTrans α (fun a b => le a b = true)]`, matching `mergeSort`/`insertionSort`. The `∀`-form facts are derived once inside `bubblePass_spec` for the (private, grind-friendly) pointwise helpers. Also move `@[expose] public section` to after the module docstring. --- Algolean/Algorithms/VecBubbleSort.lean | 36 ++++++++++++++------------ 1 file changed, 20 insertions(+), 16 deletions(-) diff --git a/Algolean/Algorithms/VecBubbleSort.lean b/Algolean/Algorithms/VecBubbleSort.lean index c6cc3cd..09d9c9a 100644 --- a/Algolean/Algorithms/VecBubbleSort.lean +++ b/Algolean/Algorithms/VecBubbleSort.lean @@ -10,8 +10,6 @@ public import Algolean.Models.ReadWriteVec public import Mathlib.Data.List.Sort public import Std.Tactic.Do -@[expose] public section - /-! # Bubble sort in the read/write vector query model @@ -39,6 +37,8 @@ reasoning modular: - `bubbleSort_sorted` : `bubbleSort` returns a sorted vector (for a total, transitive `le`). -/ +@[expose] public section + namespace Algolean namespace Algorithms @@ -168,11 +168,15 @@ invariant, then discharges the (concrete, `grind`-friendly) verification conditi set_option mvcgen.warning false in /-- One pass deposits the maximum of `[0, bound]` at `bound`, preserves the sorted suffix above, and permutes the vector. -/ -theorem bubblePass_spec (le : α → α → Bool) (htot : ∀ a b : α, le a b = true ∨ le b a = true) - (htr : ∀ a b c : α, le a b = true → le b c = true → le a c = true) +theorem bubblePass_spec (le : α → α → Bool) [Std.Total (fun a b : α => le a b = true)] + [IsTrans α (fun a b => le a b = true)] (bound : Nat) (hb : bound < n) (v : Vector α n) (hpre : SortedFrom le v (bound + 1)) : ⦃⌜True⌝⦄ bubblePass le bound hb v ⦃⇓w => ⌜MaxAt le w bound ∧ SortedFrom le w (bound + 1) ∧ w.toList.Perm v.toList⌝⦄ := by + have htot : ∀ a b : α, le a b = true ∨ le b a = true := + fun a b => Std.Total.total (r := fun a b : α => le a b = true) a b + have htr : ∀ a b c : α, le a b = true → le b c = true → le a c = true := + fun a b c => IsTrans.trans (r := fun a b => le a b = true) a b c have hrefl : ∀ a, le a a = true := fun a => (htot a a).elim id id mvcgen [bubblePass] invariants · ⇓⟨xs, w⟩ => ⌜MaxAt le w xs.prefix.length ∧ SortedFrom le w (bound + 1) @@ -206,41 +210,41 @@ theorem bubblePass_spec (le : α → α → Bool) (htot : ∀ a b : α, le a b = set_option mvcgen.warning false in /-- `bubbleSort` is correct: it sorts and permutes its input (for a total, transitive `le`). -/ -theorem bubbleSort_spec (le : α → α → Bool) (htot : ∀ a b : α, le a b = true ∨ le b a = true) - (htr : ∀ a b c : α, le a b = true → le b c = true → le a c = true) (v : Vector α n) : +theorem bubbleSort_spec (le : α → α → Bool) [Std.Total (fun a b : α => le a b = true)] + [IsTrans α (fun a b => le a b = true)] (v : Vector α n) : ⦃⌜True⌝⦄ bubbleSort le v ⦃⇓w => ⌜SortedFrom le w 0 ∧ w.toList.Perm v.toList⌝⦄ := by mvcgen [bubbleSort, bubblePass_spec] invariants · ⇓⟨xs, w⟩ => ⌜SortedFrom le w (n - xs.prefix.length) ∧ w.toList.Perm v.toList⌝ - case vc3.hpre => + case vc1.hpre => have hsort := (‹SortedFrom le _ _ ∧ List.Perm _ _›).1 have hcb := (‹Fin n› : Fin n).isLt rw [fin_cur_eq ‹List.finRange n = _ ++ _ :: _›] at hcb ⊢ rwa [sub_one_sub_add _ hcb] - case vc4.step.success => + case vc2.step.success => obtain ⟨hmax, hsort, hperm⟩ := ‹MaxAt le _ _ ∧ SortedFrom le _ _ ∧ List.Perm _ _› have hperm0 := (‹SortedFrom le _ _ ∧ List.Perm _ _›).2 have key := sortedFrom_of_maxAt le _ _ hmax hsort rw [fin_cur_eq ‹List.finRange n = _ ++ _ :: _›] at key exact ⟨by simp only [List.length_append, List.length_cons, List.length_nil]; rwa [sub_succ], hperm.trans hperm0⟩ - case vc5.pre => + case vc3.pre => exact ⟨fun p q _ hq => absurd (by simpa using hq) (by have := q.isLt; omega), List.Perm.refl _⟩ - case vc6.post.success => + case vc4.post.success => obtain ⟨h1, h2⟩ := ‹SortedFrom le _ _ ∧ List.Perm _ _› rw [List.length_finRange, Nat.sub_self] at h1 exact ⟨h1, h2⟩ /-- `bubbleSort` returns a permutation of its input. -/ -theorem bubbleSort_perm (le : α → α → Bool) (htot : ∀ a b : α, le a b = true ∨ le b a = true) - (htr : ∀ a b c : α, le a b = true → le b c = true → le a c = true) (v : Vector α n) : +theorem bubbleSort_perm (le : α → α → Bool) [Std.Total (fun a b : α => le a b = true)] + [IsTrans α (fun a b => le a b = true)] (v : Vector α n) : ((bubbleSort le v).eval Vec.natCost).toList.Perm v.toList := - (eval_of_triple (bubbleSort_spec le htot htr v)).2 + (eval_of_triple (bubbleSort_spec le v)).2 /-- `bubbleSort` returns a sorted vector, for a total and transitive `le`. -/ -theorem bubbleSort_sorted (le : α → α → Bool) (htot : ∀ a b : α, le a b = true ∨ le b a = true) - (htr : ∀ a b c : α, le a b = true → le b c = true → le a c = true) (v : Vector α n) : +theorem bubbleSort_sorted (le : α → α → Bool) [Std.Total (fun a b : α => le a b = true)] + [IsTrans α (fun a b => le a b = true)] (v : Vector α n) : ((bubbleSort le v).eval Vec.natCost).toList.Pairwise (fun a b => le a b = true) := - sortedFrom_zero_pairwise (eval_of_triple (bubbleSort_spec le htot htr v)).1 + sortedFrom_zero_pairwise (eval_of_triple (bubbleSort_spec le v)).1 end Algorithms From 3bd28590ff883ce84c157ea316f66d9977fdd707 Mon Sep 17 00:00:00 2001 From: Tanner Duve Date: Fri, 5 Jun 2026 08:50:55 -0700 Subject: [PATCH 6/7] refactor(VecBubbleSort): prefer lia over omega; drop derivation haves Address review: - Replace `omega` with `lia` for the Nat-arithmetic side goals (the `grind` calls that need `Fin.val_mk` reduction are left as `grind`). - Remove the `htot`/`htr`/`hrefl` `have`s from `bubblePass_spec`: the private pointwise helpers (`maxAt_swap`/`maxAt_noswap`/`maxAt_zero`) now take the `[Std.Total]`/`[IsTrans]` instances directly and materialize the facts they need locally, so the spec just lets the instances flow through. --- Algolean/Algorithms/VecBubbleSort.lean | 75 +++++++++++++------------- 1 file changed, 39 insertions(+), 36 deletions(-) diff --git a/Algolean/Algorithms/VecBubbleSort.lean b/Algolean/Algorithms/VecBubbleSort.lean index 09d9c9a..6db12e5 100644 --- a/Algolean/Algorithms/VecBubbleSort.lean +++ b/Algolean/Algorithms/VecBubbleSort.lean @@ -56,11 +56,11 @@ def bubblePass (le : α → α → Bool) (bound : Nat) (hb : bound < n) (v : Vec Prog (Vec α) (Vector α n) := do let mut v := v for j in List.finRange bound do - let a ← (Vec.read v ⟨j, by omega⟩ : Prog (Vec α) α) - let b ← (Vec.read v ⟨j + 1, by omega⟩ : Prog (Vec α) α) + let a ← (Vec.read v ⟨j, by lia⟩ : Prog (Vec α) α) + let b ← (Vec.read v ⟨j + 1, by lia⟩ : Prog (Vec α) α) if !le a b then - v ← (Vec.write v ⟨j, by omega⟩ b : Prog (Vec α) (Vector α n)) - v ← (Vec.write v ⟨j + 1, by omega⟩ a : Prog (Vec α) (Vector α n)) + v ← (Vec.write v ⟨j, by lia⟩ b : Prog (Vec α) (Vector α n)) + v ← (Vec.write v ⟨j + 1, by lia⟩ a : Prog (Vec α) (Vector α n)) return v /-- @@ -70,7 +70,7 @@ Bubble sort in the `Vec` query model: run `n` bubbling passes with shrinking bou def bubbleSort (le : α → α → Bool) (v : Vector α n) : Prog (Vec α) (Vector α n) := do let mut v := v for i in List.finRange n do - v ← bubblePass le (n - 1 - i) (by omega) v + v ← bubblePass le (n - 1 - i) (by lia) v return v /-! ### Invariants and pointwise lemmas @@ -92,7 +92,7 @@ def SortedFrom (le : α → α → Bool) (w : Vector α n) (b : Nat) : Prop := /-- In a `finRange` split, the cursor element sits at the prefix length. -/ private theorem fin_cur_eq {pref suff : List (Fin n)} {cur : Fin n} (h : List.finRange n = pref ++ cur :: suff) : (cur : Nat) = pref.length := by - have hlt : pref.length < n := by have := congrArg List.length h; simp at this; omega + have hlt : pref.length < n := by have := congrArg List.length h; simp at this; lia have h2 := congrArg (fun l => l[pref.length]?) h simp only [List.getElem?_append_right (Nat.le_refl pref.length), Nat.sub_self, List.getElem?_cons_zero, List.getElem_finRange, @@ -106,33 +106,39 @@ private lemma set_set_toList_perm (w : Vector α n) (i j : Nat) (hi : i < n) (hj List.set_set_perm (as := w.toList) (by simpa using hi) (by simpa using hj) /-- After swapping out-of-order `w[m], w[m+1]`, the prefix maximum moves to `m+1`. -/ -private lemma maxAt_swap (le : α → α → Bool) (htot : ∀ a b : α, le a b = true ∨ le b a = true) +private lemma maxAt_swap (le : α → α → Bool) [Std.Total (fun a b : α => le a b = true)] (w : Vector α n) (m : Nat) (hm : m + 1 < n) (hmax : MaxAt le w m) - (hsw : le (w[m]'(by omega)) (w[m + 1]'hm) = false) : - MaxAt le ((w.set m (w[m + 1]'hm) (by omega)).set (m + 1) (w[m]'(by omega)) hm) (m + 1) := by + (hsw : le (w[m]'(by lia)) (w[m + 1]'hm) = false) : + MaxAt le ((w.set m (w[m + 1]'hm) (by lia)).set (m + 1) (w[m]'(by lia)) hm) (m + 1) := by intro p q hp hq - have hcmp := (htot (w[m]'(by omega)) (w[m + 1]'hm)).resolve_left (by simp [hsw]) - have key : ∀ r : Fin n, (r : Nat) ≤ m → le w[r] (w[m]'(by omega)) = true := - fun r hr => hmax r ⟨m, by omega⟩ hr rfl + have htot : ∀ a b : α, le a b = true ∨ le b a = true := + Std.Total.total (r := fun a b : α => le a b = true) + have hcmp := (htot (w[m]'(by lia)) (w[m + 1]'hm)).resolve_left (by simp [hsw]) + have key : ∀ r : Fin n, (r : Nat) ≤ m → le w[r] (w[m]'(by lia)) = true := + fun r hr => hmax r ⟨m, by lia⟩ hr rfl grind /-- When the pair is already in order, the prefix maximum still extends to `m+1`. -/ -private lemma maxAt_noswap (le : α → α → Bool) (htot : ∀ a b : α, le a b = true ∨ le b a = true) - (htr : ∀ a b c : α, le a b = true → le b c = true → le a c = true) +private lemma maxAt_noswap (le : α → α → Bool) [Std.Total (fun a b : α => le a b = true)] + [IsTrans α (fun a b => le a b = true)] (w : Vector α n) (m : Nat) (hm : m + 1 < n) (hmax : MaxAt le w m) - (hns : le (w[m]'(by omega)) (w[m + 1]'hm) = true) : MaxAt le w (m + 1) := by + (hns : le (w[m]'(by lia)) (w[m + 1]'hm) = true) : MaxAt le w (m + 1) := by intro p q hp hq - have key : ∀ r : Fin n, (r : Nat) ≤ m → le w[r] (w[m]'(by omega)) = true := - fun r hr => hmax r ⟨m, by omega⟩ hr rfl + have htot : ∀ a b : α, le a b = true ∨ le b a = true := + Std.Total.total (r := fun a b : α => le a b = true) + have htr : ∀ a b c : α, le a b = true → le b c = true → le a c = true := + fun a b c => IsTrans.trans (r := fun a b : α => le a b = true) a b c + have key : ∀ r : Fin n, (r : Nat) ≤ m → le w[r] (w[m]'(by lia)) = true := + fun r hr => hmax r ⟨m, by lia⟩ hr rfl grind /-- A swap strictly below the boundary `b` preserves the sorted suffix `[b, n)`. -/ private lemma sortedFrom_swap (le : α → α → Bool) (w : Vector α n) (m b : Nat) (hm : m + 1 < n) (hmb : m + 1 < b) (hsort : SortedFrom le w b) : - SortedFrom le ((w.set m (w[m + 1]'hm) (by omega)).set (m + 1) (w[m]'(by omega)) hm) b := by + SortedFrom le ((w.set m (w[m + 1]'hm) (by lia)).set (m + 1) (w[m]'(by lia)) hm) b := by intro p q hp hq - have e_m := hsort ⟨m, by omega⟩ q (show m ≤ (q : Nat) by omega) hq - have e_m1 := hsort ⟨m + 1, hm⟩ q (show m + 1 ≤ (q : Nat) by omega) hq + have e_m := hsort ⟨m, by lia⟩ q (show m ≤ (q : Nat) by lia) hq + have e_m1 := hsort ⟨m + 1, hm⟩ q (show m + 1 ≤ (q : Nat) by lia) hq have hpq := hsort p q hp hq grind @@ -141,13 +147,15 @@ private lemma sortedFrom_of_maxAt (le : α → α → Bool) (w : Vector α n) (k (hmax : MaxAt le w k) (hsort : SortedFrom le w (k + 1)) : SortedFrom le w k := by intro p q hp hq rcases Nat.lt_or_ge (q : Nat) (k + 1) with h | h - · exact hmax p q (by omega) (by omega) + · exact hmax p q (by lia) (by lia) · exact hsort p q hp h /-- The prefix maximum at `0` is trivial: `w[0] ≥ w[0]`. -/ -private lemma maxAt_zero (le : α → α → Bool) (hrefl : ∀ a, le a a = true) (w : Vector α n) : - MaxAt le w 0 := fun p q hp hq => by obtain rfl : p = q := by ext; omega - exact hrefl _ +private lemma maxAt_zero (le : α → α → Bool) [Std.Total (fun a b : α => le a b = true)] + (w : Vector α n) : MaxAt le w 0 := by + intro p q hp hq + obtain rfl : p = q := by ext; lia + exact (Std.Total.total (r := fun a b : α => le a b = true) w[p] w[p]).elim id id /-- `SortedFrom le w 0` is exactly sortedness of the underlying list. -/ private lemma sortedFrom_zero_pairwise {le : α → α → Bool} {w : Vector α n} @@ -155,10 +163,10 @@ private lemma sortedFrom_zero_pairwise {le : α → α → Bool} {w : Vector α rw [List.pairwise_iff_getElem] intro i j hi hj _ simpa [Vector.getElem_toList] using - h ⟨i, by simpa using hi⟩ ⟨j, by simpa using hj⟩ (by simp; omega) (Nat.zero_le _) + h ⟨i, by simpa using hi⟩ ⟨j, by simpa using hj⟩ (by simp; lia) (Nat.zero_le _) -private lemma sub_one_sub_add (k : Nat) (h : k < n) : n - 1 - k + 1 = n - k := by omega -private lemma sub_succ (k : Nat) : n - (k + 1) = n - 1 - k := by omega +private lemma sub_one_sub_add (k : Nat) (h : k < n) : n - 1 - k + 1 = n - k := by lia +private lemma sub_succ (k : Nat) : n - (k + 1) = n - 1 - k := by lia /-! ### Hoare specs via `mvcgen` @@ -173,17 +181,12 @@ theorem bubblePass_spec (le : α → α → Bool) [Std.Total (fun a b : α => le (bound : Nat) (hb : bound < n) (v : Vector α n) (hpre : SortedFrom le v (bound + 1)) : ⦃⌜True⌝⦄ bubblePass le bound hb v ⦃⇓w => ⌜MaxAt le w bound ∧ SortedFrom le w (bound + 1) ∧ w.toList.Perm v.toList⌝⦄ := by - have htot : ∀ a b : α, le a b = true ∨ le b a = true := - fun a b => Std.Total.total (r := fun a b : α => le a b = true) a b - have htr : ∀ a b c : α, le a b = true → le b c = true → le a c = true := - fun a b c => IsTrans.trans (r := fun a b => le a b = true) a b c - have hrefl : ∀ a, le a a = true := fun a => (htot a a).elim id id mvcgen [bubblePass] invariants · ⇓⟨xs, w⟩ => ⌜MaxAt le w xs.prefix.length ∧ SortedFrom le w (bound + 1) ∧ w.toList.Perm v.toList⌝ case vc3.pre => simp only [List.length_nil] - exact ⟨maxAt_zero le hrefl v, hpre, List.Perm.refl _⟩ + exact ⟨maxAt_zero le v, hpre, List.Perm.refl _⟩ case vc4.post.success => obtain ⟨h1, h2, h3⟩ := ‹MaxAt le _ _ ∧ SortedFrom le _ _ ∧ List.Perm _ _› rw [List.length_finRange] at h1 @@ -195,7 +198,7 @@ theorem bubblePass_spec (le : α → α → Bool) [Std.Total (fun a b : α => le have hcmp := ‹(!le _ _) = true› simp only [Vec.hasModel_model, Bool.not_eq_true', List.length_append, List.length_cons, List.length_nil, ← hc] at hmax hcmp hcb ⊢ - exact ⟨maxAt_swap le htot _ _ (by grind) hmax hcmp, + exact ⟨maxAt_swap le _ _ (by grind) hmax hcmp, sortedFrom_swap le _ _ _ (by grind) (by grind) hsort, (set_set_toList_perm _ _ _ (by grind) (by grind)).trans hperm⟩ case vc2.step.isFalse => @@ -206,7 +209,7 @@ theorem bubblePass_spec (le : α → α → Bool) [Std.Total (fun a b : α => le simp only [Vec.hasModel_model, Bool.not_eq_true, Bool.not_eq_false', List.length_append, List.length_cons, List.length_nil, ← hc] at hmax hns hcb ⊢ - exact ⟨maxAt_noswap le htot htr _ _ (by omega) hmax hns, hsort, hperm⟩ + exact ⟨maxAt_noswap le _ _ (by lia) hmax hns, hsort, hperm⟩ set_option mvcgen.warning false in /-- `bubbleSort` is correct: it sorts and permutes its input (for a total, transitive `le`). -/ @@ -228,7 +231,7 @@ theorem bubbleSort_spec (le : α → α → Bool) [Std.Total (fun a b : α => le exact ⟨by simp only [List.length_append, List.length_cons, List.length_nil]; rwa [sub_succ], hperm.trans hperm0⟩ case vc3.pre => - exact ⟨fun p q _ hq => absurd (by simpa using hq) (by have := q.isLt; omega), List.Perm.refl _⟩ + exact ⟨fun p q _ hq => absurd (by simpa using hq) (by have := q.isLt; lia), List.Perm.refl _⟩ case vc4.post.success => obtain ⟨h1, h2⟩ := ‹SortedFrom le _ _ ∧ List.Perm _ _› rw [List.length_finRange, Nat.sub_self] at h1 From 6cb10f9e3c0bd6ee9b73594a8c9252c0a8cb33ab Mon Sep 17 00:00:00 2001 From: Tanner Duve Date: Fri, 5 Jun 2026 09:51:54 -0700 Subject: [PATCH 7/7] refactor(VecBubbleSort): inline the order-fact haves at call sites MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Drop the `htot`/`htr`/`hrefl` `have` aliases entirely. The private pointwise helpers take the order facts as plain arguments (so `grind` reads them as local hypotheses — it can't consume a typeclass instance directly), and `bubblePass_spec` passes the terms inline: `Std.Total.total` / `IsTrans.trans` resolve the relation from each argument's expected type, and `Std.Refl.refl` (free from the Total→Refl instance) supplies reflexivity. The public theorems keep their `[Std.Total]` / `[IsTrans]` instances. --- Algolean/Algorithms/VecBubbleSort.lean | 25 ++++++++++--------------- 1 file changed, 10 insertions(+), 15 deletions(-) diff --git a/Algolean/Algorithms/VecBubbleSort.lean b/Algolean/Algorithms/VecBubbleSort.lean index 6db12e5..19af78b 100644 --- a/Algolean/Algorithms/VecBubbleSort.lean +++ b/Algolean/Algorithms/VecBubbleSort.lean @@ -106,28 +106,22 @@ private lemma set_set_toList_perm (w : Vector α n) (i j : Nat) (hi : i < n) (hj List.set_set_perm (as := w.toList) (by simpa using hi) (by simpa using hj) /-- After swapping out-of-order `w[m], w[m+1]`, the prefix maximum moves to `m+1`. -/ -private lemma maxAt_swap (le : α → α → Bool) [Std.Total (fun a b : α => le a b = true)] +private lemma maxAt_swap (le : α → α → Bool) (htot : ∀ a b : α, le a b = true ∨ le b a = true) (w : Vector α n) (m : Nat) (hm : m + 1 < n) (hmax : MaxAt le w m) (hsw : le (w[m]'(by lia)) (w[m + 1]'hm) = false) : MaxAt le ((w.set m (w[m + 1]'hm) (by lia)).set (m + 1) (w[m]'(by lia)) hm) (m + 1) := by intro p q hp hq - have htot : ∀ a b : α, le a b = true ∨ le b a = true := - Std.Total.total (r := fun a b : α => le a b = true) have hcmp := (htot (w[m]'(by lia)) (w[m + 1]'hm)).resolve_left (by simp [hsw]) have key : ∀ r : Fin n, (r : Nat) ≤ m → le w[r] (w[m]'(by lia)) = true := fun r hr => hmax r ⟨m, by lia⟩ hr rfl grind /-- When the pair is already in order, the prefix maximum still extends to `m+1`. -/ -private lemma maxAt_noswap (le : α → α → Bool) [Std.Total (fun a b : α => le a b = true)] - [IsTrans α (fun a b => le a b = true)] +private lemma maxAt_noswap (le : α → α → Bool) (htot : ∀ a b : α, le a b = true ∨ le b a = true) + (htr : ∀ a b c : α, le a b = true → le b c = true → le a c = true) (w : Vector α n) (m : Nat) (hm : m + 1 < n) (hmax : MaxAt le w m) (hns : le (w[m]'(by lia)) (w[m + 1]'hm) = true) : MaxAt le w (m + 1) := by intro p q hp hq - have htot : ∀ a b : α, le a b = true ∨ le b a = true := - Std.Total.total (r := fun a b : α => le a b = true) - have htr : ∀ a b c : α, le a b = true → le b c = true → le a c = true := - fun a b c => IsTrans.trans (r := fun a b : α => le a b = true) a b c have key : ∀ r : Fin n, (r : Nat) ≤ m → le w[r] (w[m]'(by lia)) = true := fun r hr => hmax r ⟨m, by lia⟩ hr rfl grind @@ -151,11 +145,11 @@ private lemma sortedFrom_of_maxAt (le : α → α → Bool) (w : Vector α n) (k · exact hsort p q hp h /-- The prefix maximum at `0` is trivial: `w[0] ≥ w[0]`. -/ -private lemma maxAt_zero (le : α → α → Bool) [Std.Total (fun a b : α => le a b = true)] - (w : Vector α n) : MaxAt le w 0 := by +private lemma maxAt_zero (le : α → α → Bool) (hrefl : ∀ a, le a a = true) (w : Vector α n) : + MaxAt le w 0 := by intro p q hp hq obtain rfl : p = q := by ext; lia - exact (Std.Total.total (r := fun a b : α => le a b = true) w[p] w[p]).elim id id + exact hrefl _ /-- `SortedFrom le w 0` is exactly sortedness of the underlying list. -/ private lemma sortedFrom_zero_pairwise {le : α → α → Bool} {w : Vector α n} @@ -186,7 +180,8 @@ theorem bubblePass_spec (le : α → α → Bool) [Std.Total (fun a b : α => le ∧ w.toList.Perm v.toList⌝ case vc3.pre => simp only [List.length_nil] - exact ⟨maxAt_zero le v, hpre, List.Perm.refl _⟩ + exact ⟨maxAt_zero le (Std.Refl.refl (r := fun a b : α => le a b = true)) v, + hpre, List.Perm.refl _⟩ case vc4.post.success => obtain ⟨h1, h2, h3⟩ := ‹MaxAt le _ _ ∧ SortedFrom le _ _ ∧ List.Perm _ _› rw [List.length_finRange] at h1 @@ -198,7 +193,7 @@ theorem bubblePass_spec (le : α → α → Bool) [Std.Total (fun a b : α => le have hcmp := ‹(!le _ _) = true› simp only [Vec.hasModel_model, Bool.not_eq_true', List.length_append, List.length_cons, List.length_nil, ← hc] at hmax hcmp hcb ⊢ - exact ⟨maxAt_swap le _ _ (by grind) hmax hcmp, + exact ⟨maxAt_swap le Std.Total.total _ _ (by grind) hmax hcmp, sortedFrom_swap le _ _ _ (by grind) (by grind) hsort, (set_set_toList_perm _ _ _ (by grind) (by grind)).trans hperm⟩ case vc2.step.isFalse => @@ -209,7 +204,7 @@ theorem bubblePass_spec (le : α → α → Bool) [Std.Total (fun a b : α => le simp only [Vec.hasModel_model, Bool.not_eq_true, Bool.not_eq_false', List.length_append, List.length_cons, List.length_nil, ← hc] at hmax hns hcb ⊢ - exact ⟨maxAt_noswap le _ _ (by lia) hmax hns, hsort, hperm⟩ + exact ⟨maxAt_noswap le Std.Total.total IsTrans.trans _ _ (by lia) hmax hns, hsort, hperm⟩ set_option mvcgen.warning false in /-- `bubbleSort` is correct: it sorts and permutes its input (for a total, transitive `le`). -/