From 0e9a217ccaba7355d1a5ec2ed3de817b07e98169 Mon Sep 17 00:00:00 2001 From: Devon Tuma Date: Thu, 3 Sep 2026 12:42:58 -0500 Subject: [PATCH] feat(control): cover the whole `do` fragment in every judgment, with loop rules MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Give each construct core `do`-notation elaborates to a rule in each of PolyFun's judgments, so that reasoning about ordinary monadic code never has to unfold a judgment by hand: - `Control/Monad/Support/Structural.lean`: `CanReturn`, `AllOutputs`, `SomeOutput`, and `NoOutput` through `<*`, `*>`, `if`, `if h :`, `Option.elim`, `Sum.elim`, `<$>`, and `<*>`; the `Option.elim` / `Sum.elim` reachability equations are `@[simp, grind =]`, the rest `@[simp]`, since `grind` refuses `ite` heads and thunked applicative operands as patterns; - `Control/Monad/Support/Loops.lean`: invariant rules for `forIn'` / `forIn` / `foldlM` over lists and `PureForIn` containers, obtained from core's `Spec.*` specifications under the demonic and angelic `WPMonad` instances, plus `forM` by induction — support reasoning about loops without a triple; - `Control/Monad/Algebra.lean`: `wp_seqLeft`, `wp_seqRight`, `wp_ite`, `wp_dite`, `wp_option_elim`, `wp_sum_elim` join the inward-normalizing `@[simp]` set; `Control/Monad/Hom.lean` and `Hom/Loops.lean`: a monad morphism commutes with branching and with every loop combinator; `PFunctor/Free/WP.lean`: the same for `wpFold`; - `Control/Do/Spec.lean`: `@[spec] Spec.forM_list`, the list loop core does not specify, in the tactic tier of the quarantine. `Control/Monad/Support.lean` is split under the 1500-line cap: instances and lift transport move to `Support/Instances.lean`, the per-run support of `StateT` / `ReaderT` to `Support/Indexed.lean`; no declaration changes name. Canaries: `PolyFunTest/Control/SupportStructural.lean` (one-tactic gates), `PolyFunTest/Control/MonadHomLoops.lean`, and, in `PolyFunTest/Do/Support.lean`, a `let mut` accumulator over a `for` loop verified by `vcgen` with a loop invariant through core's `Spec.forIn_list`, converted back to the "always" judgment. The program-logic page gains a coverage table; the landscape memo records the follow-ups (relational loop rules, a `mapM` judgment rule, and `try/catch` through the lifted `ExceptT` instance, where `vcgen` reports no applicable spec). Validated with `./scripts/validate.sh --lint --test --axioms` (zero sorry/axiom taint). Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_01Nb4g3Vxgjhnhsca7BzAsFc --- AGENTS.md | 4 +- PolyFun.lean | 6 + PolyFun/Control/Do/Spec.lean | 61 ++ PolyFun/Control/Monad/Algebra.lean | 40 +- PolyFun/Control/Monad/Hom.lean | 14 + PolyFun/Control/Monad/Hom/Loops.lean | 69 +++ PolyFun/Control/Monad/Support.lean | 546 ------------------ PolyFun/Control/Monad/Support/Indexed.lean | 256 ++++++++ PolyFun/Control/Monad/Support/Instances.lean | 354 ++++++++++++ PolyFun/Control/Monad/Support/Loops.lean | 141 +++++ PolyFun/Control/Monad/Support/Structural.lean | 220 +++++++ PolyFun/PFunctor/Free/Support.lean | 2 +- PolyFun/PFunctor/Free/WP.lean | 56 ++ .../MonadAlgebraRelationalSupport.lean | 1 + PolyFunTest/Control/MonadAttach.lean | 1 + PolyFunTest/Control/MonadHomLoops.lean | 45 ++ PolyFunTest/Control/SupportStructural.lean | 76 +++ PolyFunTest/Do/Support.lean | 22 + docs/reading/program-logic-landscape.md | 7 + docs/wiki/gotchas.md | 8 + docs/wiki/program-logic.md | 32 +- docs/wiki/repo-map.md | 8 +- 22 files changed, 1416 insertions(+), 553 deletions(-) create mode 100644 PolyFun/Control/Do/Spec.lean create mode 100644 PolyFun/Control/Monad/Hom/Loops.lean create mode 100644 PolyFun/Control/Monad/Support/Indexed.lean create mode 100644 PolyFun/Control/Monad/Support/Instances.lean create mode 100644 PolyFun/Control/Monad/Support/Loops.lean create mode 100644 PolyFun/Control/Monad/Support/Structural.lean create mode 100644 PolyFunTest/Control/MonadHomLoops.lean create mode 100644 PolyFunTest/Control/SupportStructural.lean diff --git a/AGENTS.md b/AGENTS.md index 1ad33be0..5970ae46 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -107,7 +107,9 @@ and depend on this library. algebra, monad iter / hom, lawful re-exports), plus the program-logic kernel: ordered monad algebras (`Monad/Algebra`, unary and relational), exact monadic support over core's `MonadAttach` with the - always/some/never judgments (`Monad/Support`), their bridges to core's + always/some/never judgments (`Monad/Support`, with instances, indexed + support, the structural `do`-fragment laws, and loop rules under + `Monad/Support/`), their bridges to core's lattice-generic `Std.Internal.Do` weakest-precondition stack (`Monad/{Algebra,Support,Hom}/WP`: `toWPMonad`, demonic and angelic interpretations, `vcgen`-ready), and the core-`Std.Do` quarantine root diff --git a/PolyFun.lean b/PolyFun.lean index 6d4f7631..3ac07c46 100644 --- a/PolyFun.lean +++ b/PolyFun.lean @@ -6,6 +6,7 @@ public import PolyFun.Control.Coalgebra public import PolyFun.Control.Comonad.Basic public import PolyFun.Control.Comonad.Instances public import PolyFun.Control.Do.Basic +public import PolyFun.Control.Do.Spec public import PolyFun.Control.LTS.Trace public import PolyFun.Control.Lawful.Basic public import PolyFun.Control.Monad.Algebra @@ -15,11 +16,16 @@ public import PolyFun.Control.Monad.Algebra.WP public import PolyFun.Control.Monad.Free public import PolyFun.Control.Monad.FreeCont public import PolyFun.Control.Monad.Hom +public import PolyFun.Control.Monad.Hom.Loops public import PolyFun.Control.Monad.Hom.WP public import PolyFun.Control.Monad.Hom.Writer public import PolyFun.Control.Monad.Indexed public import PolyFun.Control.Monad.Iter public import PolyFun.Control.Monad.Support +public import PolyFun.Control.Monad.Support.Indexed +public import PolyFun.Control.Monad.Support.Instances +public import PolyFun.Control.Monad.Support.Loops +public import PolyFun.Control.Monad.Support.Structural public import PolyFun.Control.Monad.Support.WP public import PolyFun.Control.Trace public import PolyFun.IPFunctor.Basic diff --git a/PolyFun/Control/Do/Spec.lean b/PolyFun/Control/Do/Spec.lean new file mode 100644 index 00000000..d77ab3f7 --- /dev/null +++ b/PolyFun/Control/Do/Spec.lean @@ -0,0 +1,61 @@ +/- +Copyright (c) 2026 PolyFun Contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Devon Tuma +-/ +module + +public import Std.Tactic.Do +public import Std.Internal.Do + +/-! +# Additional Specifications and Normal Forms for `vcgen` + +Core's `Std.Internal.Do.Triple.SpecLemmas` covers `forIn'` / `forIn` / `foldlM` over lists, +ranges, arrays, and iterators; this file adds the `@[spec]` rule for `List.forM`, the one list +loop that core does not specify. The wrappers the `do` elaborator uses to tunnel `return`, +`break`, and `continue` through non-algebraic combinators (`EarlyReturn.runK`, `Break.runK`, +`Continue.runK`) need no rules here: they are `abbrev`s, and both `simp` and `grind` reduce +them on a constructor scrutinee unaided. + +This module imports `Std.Tactic.Do` for the `@[spec]` attribute syntax and is therefore part of +the tactic tier of the `Std.Do` quarantine. +-/ + +@[expose] public section + +universe u v w z + +open Std.Internal.Do + +namespace Std.Internal.Do + +variable {α : Type w} {m : Type u → Type v} {Pred : Type z} {EPred : Type z} + [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] + +/-- Invariant rule for `List.forM`: the invariant relates the elements consumed so far to those +remaining, and each body step advances it by one element. -/ +@[spec] +theorem Spec.forM_list {xs : List α} {f : α → m PUnit} (inv : List α → List α → Pred) + {epost : EPred} + (step : ∀ pref cur suff, xs = pref ++ cur :: suff → + Triple (f cur) (inv pref (cur :: suff)) (fun _ => inv (pref ++ [cur]) suff) epost) : + Triple (xs.forM f) (inv [] xs) (fun _ => inv xs []) epost := by + suffices h : ∀ pref suff, xs = pref ++ suff → + Triple (suff.forM f) (inv pref suff) (fun _ => inv xs []) epost from h [] xs rfl + intro pref suff + induction suff generalizing pref with + | nil => + intro hxs + simp only [List.forM_eq_forM, List.forM_nil] + refine Triple.pure _ ?_ + simp only [List.append_nil] at hxs + subst hxs + exact Lean.Order.PartialOrder.rel_refl + | cons x suff ih => + intro hxs + simp only [List.forM_eq_forM, List.forM_cons] + exact Triple.bind (f x) (fun _ => forM suff f) (fun _ => inv (pref ++ [x]) suff) + (step pref x suff hxs) (fun _ => ih (pref ++ [x]) (by simp [hxs])) + +end Std.Internal.Do diff --git a/PolyFun/Control/Monad/Algebra.lean b/PolyFun/Control/Monad/Algebra.lean index 534a9ef7..2f6db78e 100644 --- a/PolyFun/Control/Monad/Algebra.lean +++ b/PolyFun/Control/Monad/Algebra.lean @@ -29,7 +29,7 @@ Loom's `MonadAlgebras` development. @[expose] public section -universe u v +universe u v w w' /-- An algebra for a monad `m`: a structure map collapsing a monadic value `m α` into a plain value of `α`. -/ @@ -143,6 +143,44 @@ theorem wp_seq [LawfulMonad m] (f : m (α → β)) (x : m α) (post : β → l) funext g simp [wp_map] +/-! ### The rest of the `do` fragment + +`<*`, `*>`, `if`, `if h :`, and `match` on `Option` / `Sum` (through `Option.elim` / +`Sum.elim`) push `wp` inwards like the four rules above; each is an equation on proper +subprograms and joins the same `@[simp]` set. -/ + +@[simp] +theorem wp_seqLeft [LawfulMonad m] (x : m α) (y : m β) (post : α → l) : + wp (x <* y) post = wp x (fun a => wp y fun _ => post a) := by + rw [seqLeft_eq_bind, wp_bind] + simp only [wp_bind, wp_pure] + +@[simp] +theorem wp_seqRight [LawfulMonad m] (x : m α) (y : m β) (post : β → l) : + wp (x *> y) post = wp x (fun _ => wp y post) := by + rw [seqRight_eq_bind, wp_bind] + +@[simp] +theorem wp_ite (c : Prop) [Decidable c] (x y : m α) (post : α → l) : + wp (if c then x else y) post = if c then wp x post else wp y post := by + split <;> rfl + +@[simp] +theorem wp_dite (c : Prop) [Decidable c] (x : c → m α) (y : ¬ c → m α) (post : α → l) : + wp (if h : c then x h else y h) post = if h : c then wp (x h) post else wp (y h) post := by + split <;> rfl + +@[simp] +theorem wp_option_elim {γ : Type w} (o : Option γ) (x : m α) (f : γ → m α) (post : α → l) : + wp (o.elim x f) post = o.elim (wp x post) fun c => wp (f c) post := by + cases o <;> rfl + +@[simp] +theorem wp_sum_elim {γ : Type w} {δ : Type w'} (s : γ ⊕ δ) (f : γ → m α) (g : δ → m α) + (post : α → l) : + wp (s.elim f g) post = s.elim (fun c => wp (f c) post) fun d => wp (g d) post := by + cases s <;> rfl + theorem triple_conseq {pre pre' : l} {x : m α} {post post' : α → l} (hpre : pre' ≤ pre) (hpost : ∀ a, post a ≤ post' a) : Triple pre x post → Triple pre' x post' := by diff --git a/PolyFun/Control/Monad/Hom.lean b/PolyFun/Control/Monad/Hom.lean index 1bf22b05..0e6ca9c5 100644 --- a/PolyFun/Control/Monad/Hom.lean +++ b/PolyFun/Control/Monad/Hom.lean @@ -138,6 +138,20 @@ type are equal. -/ @[simp] lemma mmap_seqRight [LawfulMonad m] [LawfulMonad n] (F : m →ᵐ n) (x : m α) (y : m β) : F (x *> y) = F x *> F y := by simp [seqRight_eq] +@[simp] lemma mmap_ite (F : m →ᵐ n) (c : Prop) [Decidable c] (x y : m α) : + F (if c then x else y) = if c then F x else F y := by split <;> rfl + +@[simp] lemma mmap_dite (F : m →ᵐ n) (c : Prop) [Decidable c] (x : c → m α) + (y : ¬ c → m α) : F (if h : c then x h else y h) = if h : c then F (x h) else F (y h) := by + split <;> rfl + +@[simp] lemma mmap_option_elim {γ : Type x} (F : m →ᵐ n) (o : Option γ) (x : m α) + (f : γ → m α) : F (o.elim x f) = o.elim (F x) fun c => F (f c) := by cases o <;> rfl + +@[simp] lemma mmap_sum_elim {γ : Type x} {δ : Type y} (F : m →ᵐ n) (s : γ ⊕ δ) (f : γ → m α) + (g : δ → m α) : F (s.elim f g) = s.elim (fun c => F (f c)) fun d => F (g d) := by + cases s <;> rfl + /-- Construct a `MonadHom` from a lawful monad lift. -/ def ofLift (m : Type u → Type v) (n : Type u → Type w) [Monad m] [Monad n] [MonadLiftT m n] [LawfulMonadLiftT m n] : m →ᵐ n where diff --git a/PolyFun/Control/Monad/Hom/Loops.lean b/PolyFun/Control/Monad/Hom/Loops.lean new file mode 100644 index 00000000..b9ed3b8b --- /dev/null +++ b/PolyFun/Control/Monad/Hom/Loops.lean @@ -0,0 +1,69 @@ +/- +Copyright (c) 2026 PolyFun Contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Devon Tuma +-/ +module + +public import PolyFun.Control.Monad.Hom +public import ToCslib.Control.Monad.HomTransport + +/-! +# Monad Morphisms Commute with Loops + +The bundled corollaries of `ToCslib.Control.Monad.HomTransport` for `MonadHom`: a monad +morphism commutes with `forIn'`, `forIn`, `forM`, `foldlM`, and `mapM` over lists, and with +`forIn` over any container whose loop is the loop over `ForIn.toList`. Each is an equation +whose left-hand side is the morphism applied to the loop, so `simp` pushes morphisms into loop +bodies the way `mmap_bind` pushes them into binds, and `grind` can index the list forms. +-/ + +@[expose] public section + +universe u v w x y + +namespace MonadHom + +variable {m : Type u → Type v} {n : Type u → Type w} [Monad m] [Monad n] (F : m →ᵐ n) + +@[simp, grind =] +theorem mmap_forIn' {ι : Type x} {β : Type u} (l : List ι) (init : β) + (f : (a : ι) → a ∈ l → β → m (ForInStep β)) : + F (forIn' l init f) = forIn' l init fun a h b => F (f a h b) := + Cslib.map_listForIn' (fun x => F x) F.mmap_pure F.mmap_bind l init f + +/-- Not a `simp` lemma: `simp` already derives it from `mmap_forIn'` through core's +`List.forIn'_eq_forIn`. -/ +@[grind =] +theorem mmap_forIn {ι : Type x} {β : Type u} (l : List ι) (init : β) + (f : ι → β → m (ForInStep β)) : + F (forIn l init f) = forIn l init fun a b => F (f a b) := + Cslib.map_listForIn (fun x => F x) F.mmap_pure F.mmap_bind l init f + +/-- Stated with the class method `forM`, the simp normal form of `List.forM`. -/ +@[simp, grind =] +theorem mmap_forM {ι : Type x} (l : List ι) (f : ι → m PUnit) : + F (forM l f) = forM l fun a => F (f a) := by + simpa only [List.forM_eq_forM, Function.comp_def] using + Cslib.map_listForM (fun x => F x) F.mmap_pure F.mmap_bind l f + +@[simp, grind =] +theorem mmap_foldlM {σ : Type u} {ι : Type x} (f : σ → ι → m σ) (init : σ) (l : List ι) : + F (l.foldlM f init) = l.foldlM (fun s a => F (f s a)) init := + Cslib.map_listFoldlM (fun x => F x) F.mmap_pure F.mmap_bind f init l + +@[simp, grind =] +theorem mmap_mapM [LawfulMonad m] [LawfulMonad n] {ι : Type x} {β : Type u} (f : ι → m β) + (l : List ι) : + F (l.mapM f) = l.mapM fun a => F (f a) := + Cslib.map_listMapM (fun x => F x) F.mmap_pure F.mmap_bind f l + +@[simp] +theorem mmap_forIn_of_pureForIn {ρ : Type y} {ι : Type x} {β : Type u} + [ForIn m ρ ι] [ForIn n ρ ι] [ForIn Id ρ ι] + [Std.Internal.PureForIn m ρ ι] [Std.Internal.PureForIn n ρ ι] + (xs : ρ) (init : β) (f : ι → β → m (ForInStep β)) : + F (forIn xs init f) = forIn xs init fun a b => F (f a b) := + Cslib.map_forIn_of_pureForIn (fun x => F x) F.mmap_pure F.mmap_bind xs init f + +end MonadHom diff --git a/PolyFun/Control/Monad/Support.lean b/PolyFun/Control/Monad/Support.lean index 5c4d33e2..1d1e7342 100644 --- a/PolyFun/Control/Monad/Support.lean +++ b/PolyFun/Control/Monad/Support.lean @@ -542,550 +542,4 @@ end Angelic end PropAlgebra -/-! ## Recovering the `MonadLiftT` presentation - -`MonadAttach` is the canonical interface for reachability here: it is core's, it carries -a lawfulness hierarchy, and core supplies instances for the transformers this library -cares about. The `MonadLiftT m SetM` spelling below is a **compatibility shim for a -downstream still phrased that way**, not the recommended API — register it locally when -migrating, rather than building against it. - -Two things this does *not* say. `SetM` remains perfectly good as a **carrier**: -`support : Set α` is unchanged, and `PFunctor.FreeM.support_eq_liftM_univ` — which -genuinely folds into `SetM` as a monad — stays. What is being demoted is the lift as an -*interface*. And unlike the probability layer's `PMF` retirement, there is no upstream -force here: `SetM` is not being deprecated by Mathlib. This is a project standardizing -on core's vocabulary, nothing more. - -One concrete argument for the direction, which is otherwise recorded nowhere: -`support_eq_liftM_univ` is restricted to `{γ : Type uB}`, because `FreeM.liftM` pins the -payload universe to the *direction* universe. `MonadAttach.support` on `FreeM P` carries -no such restriction. The attach-based presentation is strictly more universe-polymorphic -than the fold. - -The two declarations are deliberately not instances, so that support reasoning does not -perturb monad-lift instance search. -/ - -/-- The support map as a monad lift into `SetM`. Not an instance. -/ -@[instance_reducible] -def toMonadLiftT (m : Type u → Type v) [MonadAttach m] : - MonadLiftT m SetM where - monadLift x := (support x : SetM _) - -/-- The support lift is lawful. Not an instance. -/ -theorem toLawfulMonadLiftT (m : Type u → Type v) [Monad m] [LawfulMonad m] [MonadAttach m] - [ExactMonadAttach m] : - letI := toMonadLiftT m - LawfulMonadLiftT m SetM := - letI := toMonadLiftT m - { monadLift_pure := fun a => support_pure a - monadLift_bind := fun x f => support_bind x f } - -/-! ## Transport along a monad lift - -Core proves the elimination half — lifting cannot *create* possible outputs — so a -lift can only shrink the support, and a demonic obligation therefore transfers along -it for free. - -The introduction half is **not** available generically, and cannot be: nothing in -`MonadLiftT` or its lawfulness class says the lift preserves reachability, and a lift -into a monad whose `CanReturn` is uniformly `False` satisfies every law while losing -every output. A caller that needs `support (liftM x) = support x` must supply that -equation for its particular lift; `FreeM`'s powerset fold -(`PFunctor.FreeM.support_eq_liftM_univ`) is the worked instance. -/ - -section Transport - -variable {m : Type u → Type v} {n : Type u → Type w} {α : Type u} -variable [Monad m] [LawfulMonad m] [MonadAttach m] [LawfulMonadAttach m] -variable [Monad n] [LawfulMonad n] [MonadAttach n] [LawfulMonadAttach n] -variable [MonadLiftT m n] [LawfulMonadLiftT m n] - -/-- Lifting cannot create possible outputs. The set form of core's -`LawfulMonadAttach.canReturn_liftM_imp'`. -/ -theorem support_liftM_subset (x : m α) : support (liftM x : n α) ⊆ support x := - fun _ h => LawfulMonadAttach.canReturn_liftM_imp' h - -/-- A demonic guarantee survives lifting: the lifted computation has no outputs the -original did not have, so a property of all of the original's outputs holds of all of -the lift's. -/ -theorem allOutputs_liftM {p : α → Prop} {x : m α} (h : AllOutputs p x) : - AllOutputs p (liftM x : n α) := - fun a ha => h a (support_liftM_subset x ha) - -/-- Dually, an angelic fact about the lift transfers back to the original. -/ -theorem someOutput_of_someOutput_liftM {p : α → Prop} {x : m α} - (h : SomeOutput p (liftM x : n α)) : SomeOutput p x := - h.imp fun _ ⟨ha, hp⟩ => ⟨support_liftM_subset x ha, hp⟩ - -/-- And a "never" guarantee survives lifting. -/ -theorem noOutput_liftM {p : α → Prop} {x : m α} (h : NoOutput p x) : - NoOutput p (liftM x : n α) := - fun a ha => h a (support_liftM_subset x ha) - -end Transport - -/-! ## Base instances - -Core supplies `MonadAttach` and `LawfulMonadAttach` for `Id`, `Option`, `OptionT`, -`ExceptT`, `StateT`, and `ReaderT`; only the exactness fields are needed here. `Except` and -`SetM` have no core instance and are supplied below. -/ - -section Instances - -/-- Core provides no `MonadAttach (Except ε)` at this pin, only the transformer version; this -mirrors core's `Option` instance. An identical declaration has landed upstream and ships in -Lean v4.35, so delete this instance and the one below it at that toolchain bump. -/ -instance instMonadAttachExcept {ε : Type u} : MonadAttach (Except ε) where - CanReturn x a := x = Except.ok a - attach - | .ok a => .ok ⟨a, rfl⟩ - | .error e => .error e - -instance instLawfulMonadAttachExcept {ε : Type u} : LawfulMonadAttach (Except ε) where - map_attach {_ x} := by cases x <;> rfl - canReturn_map_imp {_ _ x _} h := by - cases x with - | error e => cases h - | ok z => cases h; exact z.2 - -/-- Core's `MonadAttach (ExceptT ε m)` is stated at `max`-joined universes, which blocks -synthesis in a universe-polymorphic context; this alias instantiates it at a single -universe. Delete once the upstream declaration is repaired. -/ -instance instMonadAttachExceptT {ε : Type u} {m : Type u → Type v} [Monad m] - [MonadAttach m] : MonadAttach (ExceptT ε m) := - instMonadAttachExceptTOfMonad.{u, u, v} - -/-- The powerset monad is its own support. -/ -instance instMonadAttachSetM : MonadAttach SetM where - CanReturn s a := a ∈ SetM.run s - attach _ := (Set.univ : Set _) - -instance instLawfulMonadAttachSetM : LawfulMonadAttach SetM where - map_attach {_ x} := by - change Subtype.val '' (Set.univ : Set {a // a ∈ SetM.run x}) = x - ext a - simp [SetM.run] - canReturn_map_imp {_ _ _ _} h := by - obtain ⟨z, -, hz⟩ := h - exact hz ▸ z.2 - -instance instExactMonadAttachId : ExactMonadAttach Id where - canReturn_pure _ := rfl - canReturn_bind h h' := by - simp only [CanReturn, Id.run] at * - subst h - exact h' - -instance instExactMonadAttachOption : ExactMonadAttach Option where - canReturn_pure _ := rfl - canReturn_bind {_ _ _ _ _ _} h h' := by - simp only [CanReturn] at * - subst h - simpa using h' - -instance instExactMonadAttachExcept {ε : Type u} : ExactMonadAttach (Except ε) where - canReturn_pure _ := rfl - canReturn_bind ha hb := by cases ha; exact hb - -instance instExactMonadAttachSetM : ExactMonadAttach SetM where - canReturn_pure _ := rfl - canReturn_bind {_ _ _ _ a _} ha hb := Set.mem_iUnion.mpr ⟨a, Set.mem_iUnion.mpr ⟨ha, hb⟩⟩ - -variable {m : Type u → Type v} [Monad m] [LawfulMonad m] [MonadAttach m] [ExactMonadAttach m] - -instance instExactMonadAttachOptionT : ExactMonadAttach (OptionT m) where - canReturn_pure {α} a := by - change CanReturn ((pure a : OptionT m α)).run (some a) - rw [OptionT.run_pure] - exact ExactMonadAttach.canReturn_pure _ - canReturn_bind {α β x f a b} h h' := by - change CanReturn ((x >>= f : OptionT m β)).run (some b) - have hrun : ((x >>= f : OptionT m β)).run = x.run >>= fun o => - match o with - | some c => (f c).run - | none => pure none := rfl - rw [hrun] - exact ExactMonadAttach.canReturn_bind (a := some a) h h' - -instance instExactMonadAttachExceptT {ε : Type u} : ExactMonadAttach (ExceptT ε m) where - canReturn_pure {α} a := by - change CanReturn ((pure a : ExceptT ε m α)).run (Except.ok a) - rw [ExceptT.run_pure] - exact ExactMonadAttach.canReturn_pure _ - canReturn_bind {α β x f a b} h h' := by - change CanReturn ((x >>= f : ExceptT ε m β)).run (Except.ok b) - have hrun : ((x >>= f : ExceptT ε m β)).run = x.run >>= fun e => - match e with - | Except.ok c => (f c).run - | Except.error e => pure (Except.error e) := rfl - rw [hrun] - exact ExactMonadAttach.canReturn_bind (a := Except.ok a) h h' - -/-! ### Per-monad unfoldings - -Each base monad's `CanReturn` is a concrete predicate, so membership in its support -has a concrete spelling. Every one of these is `Iff.rfl`; naming them keeps callers -from reaching through `support` and `CanReturn` with `change`. -/ - -section Unfoldings - -variable {α : Type u} - -@[simp, grind =] -theorem Id.canReturn_iff {x : Id α} {a : α} : CanReturn x a ↔ x.run = a := - Iff.rfl - -@[simp] -theorem Id.support_eq_singleton (x : Id α) : support x = {x.run} := by - ext a - rw [mem_support, Id.canReturn_iff, Set.mem_singleton_iff] - exact eq_comm - -@[simp, grind =] -theorem Option.canReturn_iff {x : Option α} {a : α} : CanReturn x a ↔ x = some a := - Iff.rfl - -@[simp, grind =] -theorem Option.support_some (a : α) : support (some a) = {a} := by - ext b - rw [mem_support, Option.canReturn_iff, Set.mem_singleton_iff] - exact ⟨fun h => (Option.some.inj h).symm, fun h => by rw [h]⟩ - -@[simp, grind =] -theorem Option.support_none : support (none : Option α) = ∅ := by - ext b - rw [mem_support, Option.canReturn_iff] - simp - -@[simp, grind =] -theorem Except.canReturn_iff {ε : Type u} {x : Except ε α} {a : α} : - CanReturn x a ↔ x = Except.ok a := - Iff.rfl - -@[simp, grind =] -theorem Except.support_ok {ε : Type u} (a : α) : support (Except.ok a : Except ε α) = {a} := by - ext b - rw [mem_support, Except.canReturn_iff, Set.mem_singleton_iff] - exact ⟨fun h => (Except.ok.inj h).symm, fun h => by rw [h]⟩ - -@[simp, grind =] -theorem Except.support_error {ε : Type u} (e : ε) : - support (Except.error e : Except ε α) = ∅ := by - ext b - rw [mem_support, Except.canReturn_iff] - simp - -@[simp, grind =] -theorem SetM.canReturn_iff {x : SetM α} {a : α} : CanReturn x a ↔ a ∈ SetM.run x := - Iff.rfl - -@[simp] -theorem SetM.support_eq_run (x : SetM α) : support x = SetM.run x := - Set.ext fun _ => Iff.rfl - -variable {m : Type u → Type v} [Monad m] [MonadAttach m] - -@[simp, grind =] -theorem OptionT.canReturn_iff {x : OptionT m α} {a : α} : - CanReturn x a ↔ some a ∈ support x.run := - Iff.rfl - -@[simp, grind =] -theorem ExceptT.canReturn_iff {ε : Type u} {x : ExceptT ε m α} {a : α} : - CanReturn x a ↔ Except.ok a ∈ support x.run := - Iff.rfl - -end Unfoldings - -/-! ### The writer transformer - -`WriterT ω m` accumulates an output alongside the value, so the honest reading of its -support is the one that keeps that output: a value is possible exactly when it is -returned *together with some accumulator*. This is the same rule the measure semantics -uses for the same transformer — a writer computation denotes the underlying `m (α × ω)` -rather than discarding `ω` — and unlike `StateT` it costs nothing, because there is no -*input* index to choose. Both introduction rules survive: `pure` writes the unit, and -two composable outputs compose with their accumulators multiplied. -/ - -section WriterT - -variable {ω : Type u} [Monoid ω] - -instance instMonadAttachWriterT : MonadAttach (WriterT ω m) where - CanReturn x a := ∃ w, CanReturn x.run (a, w) - attach x := WriterT.mk <| - (fun p => (⟨p.1.1, ⟨p.1.2, p.2⟩⟩, p.1.2)) <$> MonadAttach.attach x.run - -omit [LawfulMonad m] [ExactMonadAttach m] [Monoid ω] in -theorem mem_support_writerT_iff {x : WriterT ω m α} {a : α} : - a ∈ support x ↔ ∃ w, (a, w) ∈ support x.run := - Iff.rfl - -omit [LawfulMonad m] [ExactMonadAttach m] [Monoid ω] in -theorem mem_support_of_run_writerT {x : WriterT ω m α} {a : α} {w : ω} - (h : (a, w) ∈ support x.run) : a ∈ support x := - ⟨w, h⟩ - -instance instWeaklyLawfulMonadAttachWriterT : - WeaklyLawfulMonadAttach (WriterT ω m) where - map_attach {α x} := by - refine WriterT.ext _ _ ?_ - rw [WriterT.run_map] - have hrun : (MonadAttach.attach x : WriterT ω m (Subtype (CanReturn x))).run - = (fun p : Subtype (CanReturn x.run) => - ((⟨p.1.1, ⟨p.1.2, p.2⟩⟩ : Subtype (CanReturn x)), p.1.2)) - <$> MonadAttach.attach x.run := rfl - rw [hrun, Functor.map_map] - simpa [Function.comp_def] using WeaklyLawfulMonadAttach.map_attach (m := m) (x := x.run) - -instance instLawfulMonadAttachWriterT : LawfulMonadAttach (WriterT ω m) where - canReturn_map_imp {α P x a} h := by - obtain ⟨w, hw⟩ := h - rw [WriterT.run_map] at hw - obtain ⟨q, -, hqa⟩ := LawfulMonadAttach.canReturn_map_imp' hw - obtain ⟨⟨v, hv⟩, w'⟩ := q - cases hqa - exact hv - -/-- Both introduction rules hold: `pure` writes the unit accumulator, and composable -outputs compose with their accumulators multiplied. This is what `StateT` cannot have — -there is no input index to quantify over, so nothing is flattened away. -/ -instance instExactMonadAttachWriterT : ExactMonadAttach (WriterT ω m) where - canReturn_pure {α} a := ⟨1, ExactMonadAttach.canReturn_pure _⟩ - canReturn_bind {α β x f a b} h h' := by - obtain ⟨w₁, hw₁⟩ := h - obtain ⟨w₂, hw₂⟩ := h' - refine ⟨w₁ * w₂, ?_⟩ - change CanReturn (x.run >>= fun p => (fun q => (q.1, p.2 * q.2)) <$> (f p.1).run) (b, w₁ * w₂) - refine ExactMonadAttach.canReturn_bind (a := (a, w₁)) hw₁ ?_ - have hmem : ((b, w₂) : β × ω) ∈ support (f a).run := hw₂ - have himg := Set.mem_image_of_mem (fun q : β × ω => (q.1, w₁ * q.2)) hmem - rwa [← support_map] at himg - -end WriterT - -/-! ### Stateful monads - -`StateT` and `ReaderT` do have core `MonadAttach` instances, existentially quantified over -the initial state or environment, and those supports are canonical. They are *not* -`ExactMonadAttach`: possible outputs do not compose along `bind`, because its flattened -premises may be witnessed at different initial indices. Reason per run instead. -/ - -omit [LawfulMonad m] [ExactMonadAttach m] in -theorem mem_support_stateT_iff {σ : Type u} {x : StateT σ m α} {a : α} : - a ∈ support x ↔ ∃ s s', (a, s') ∈ support (x.run s) := - Iff.rfl - -omit [LawfulMonad m] [ExactMonadAttach m] in -theorem mem_support_readerT_iff {ρ : Type u} {x : ReaderT ρ m α} {a : α} : - a ∈ support x ↔ ∃ r, a ∈ support (x.run r) := - Iff.rfl - -omit [LawfulMonad m] [ExactMonadAttach m] in -theorem mem_support_of_run_stateT {σ : Type u} {x : StateT σ m α} {a : α} {s s' : σ} - (h : (a, s') ∈ support (x.run s)) : a ∈ support x := - ⟨s, s', h⟩ - -omit [LawfulMonad m] [ExactMonadAttach m] in -theorem mem_support_of_run_readerT {ρ : Type u} {x : ReaderT ρ m α} {a : α} {r : ρ} - (h : a ∈ support (x.run r)) : a ∈ support x := - ⟨r, h⟩ - -/-! #### Indexed support - -The flattened support above is canonical but coarse: it quantifies the initial state -existentially, and independently on each side of a `bind`, which is exactly why -`ExactMonadAttach` fails. Indexing repairs that. `supportFrom s x` is the set of -result/final-state pairs reachable *from `s`*, and its bind law is exact — the -continuation is only ever run from states the prefix actually produced — needing no -exactness on the transformer, because nothing is flattened away. - -This is the same move the probabilistic semantics makes for the same transformer: -state-indexed computations denote a `Kernel σ (α × σ)` rather than a measure, because -there is no canonical initial state to integrate over. Kernels are to measures as -indexed support is to support. -/ - -/-- The result/final-state pairs reachable by running `x` from the initial state `s`. -/ -def StateT.supportFrom {σ : Type u} (s : σ) (x : StateT σ m α) : Set (α × σ) := - support (x.run s) - -/-- The outputs reachable by running `x` in the environment `r`. -/ -def ReaderT.supportAt {ρ : Type u} (r : ρ) (x : ReaderT ρ m α) : Set α := - support (x.run r) - -omit [Monad m] [LawfulMonad m] [ExactMonadAttach m] in -theorem StateT.mem_supportFrom_iff {σ : Type u} {s : σ} {x : StateT σ m α} {p : α × σ} : - p ∈ StateT.supportFrom s x ↔ p ∈ support (x.run s) := - Iff.rfl - -omit [Monad m] [LawfulMonad m] [ExactMonadAttach m] in -theorem ReaderT.mem_supportAt_iff {ρ : Type u} {r : ρ} {x : ReaderT ρ m α} {a : α} : - a ∈ ReaderT.supportAt r x ↔ a ∈ support (x.run r) := - Iff.rfl - -omit [LawfulMonad m] [ExactMonadAttach m] in -/-- The flattened support is the union of the indexed ones. Recovers -`mem_support_stateT_iff` and pins that indexing loses nothing. -/ -theorem StateT.mem_support_iff_exists_supportFrom {σ : Type u} {x : StateT σ m α} {a : α} : - a ∈ support x ↔ ∃ s s', (a, s') ∈ StateT.supportFrom s x := - Iff.rfl - -omit [LawfulMonad m] [ExactMonadAttach m] in -theorem ReaderT.mem_support_iff_exists_supportAt {ρ : Type u} {x : ReaderT ρ m α} {a : α} : - a ∈ support x ↔ ∃ r, a ∈ ReaderT.supportAt r x := - Iff.rfl - -@[simp, grind =] -theorem StateT.supportFrom_pure {σ : Type u} (s : σ) (a : α) : - StateT.supportFrom s (pure a : StateT σ m α) = {(a, s)} := by - rw [StateT.supportFrom, StateT.run_pure, support_pure] - -@[simp, grind =] -theorem ReaderT.supportAt_pure {ρ : Type u} (r : ρ) (a : α) : - ReaderT.supportAt r (pure a : ReaderT ρ m α) = {a} := by - rw [ReaderT.supportAt, ReaderT.run_pure, support_pure] - -/-- **The exact bind law.** Unlike the flattened `support`, this composes: the -continuation is run only from states the prefix actually produces, so no witness is -chosen independently on the two sides. Needs only `[ExactMonadAttach m]` on the base -monad — `StateT σ m` itself is deliberately not `ExactMonadAttach`, and does not need -to be. -/ -@[simp] -theorem StateT.supportFrom_bind {σ : Type u} (s : σ) (x : StateT σ m α) - (f : α → StateT σ m β) : - StateT.supportFrom s (x >>= f) - = ⋃ p ∈ StateT.supportFrom s x, StateT.supportFrom p.2 (f p.1) := by - rw [StateT.supportFrom, StateT.run_bind, support_bind] - rfl - -/-- The environment version, where the same `r` is threaded to both sides. -/ -@[simp] -theorem ReaderT.supportAt_bind {ρ : Type u} (r : ρ) (x : ReaderT ρ m α) - (f : α → ReaderT ρ m β) : - ReaderT.supportAt r (x >>= f) - = ⋃ a ∈ ReaderT.supportAt r x, ReaderT.supportAt r (f a) := by - rw [ReaderT.supportAt, ReaderT.run_bind, support_bind] - rfl - -@[simp] -theorem StateT.supportFrom_map {σ : Type u} (s : σ) (g : α → β) (x : StateT σ m α) : - StateT.supportFrom s (g <$> x) - = (fun p => (g p.1, p.2)) '' StateT.supportFrom s x := by - rw [StateT.supportFrom, StateT.run_map, support_map] - rfl - -@[simp] -theorem ReaderT.supportAt_map {ρ : Type u} (r : ρ) (g : α → β) (x : ReaderT ρ m α) : - ReaderT.supportAt r (g <$> x) = g '' ReaderT.supportAt r x := by - rw [ReaderT.supportAt, ReaderT.run_map, support_map] - rfl - -/-! #### Indexed judgments - -The modal pair, indexed. These are the primary indexed notions and `supportFrom` is -their equality instance, exactly as `support` is `SomeOutput`'s in the unindexed case -(`support_eq_setOf_someOutput`). The state-indexed predicate ranges over the *pair*: a -`StateT` computation's outcome is a value together with a final state, and forgetting -the state is what makes the flattened judgments fail to compose. -/ - -/-- Every outcome reachable from `s` satisfies `p`. -/ -def StateT.AllOutputsFrom {σ : Type u} (s : σ) (p : α → σ → Prop) (x : StateT σ m α) : Prop := - ∀ q ∈ StateT.supportFrom s x, p q.1 q.2 - -/-- Some outcome reachable from `s` satisfies `p`. -/ -def StateT.SomeOutputFrom {σ : Type u} (s : σ) (p : α → σ → Prop) (x : StateT σ m α) : Prop := - ∃ q ∈ StateT.supportFrom s x, p q.1 q.2 - -/-- No outcome reachable from `s` satisfies `p`. -/ -def StateT.NoOutputFrom {σ : Type u} (s : σ) (p : α → σ → Prop) (x : StateT σ m α) : Prop := - StateT.AllOutputsFrom s (fun a s' => ¬ p a s') x - -@[inherit_doc StateT.AllOutputsFrom] -scoped notation:50 x:51 " ⊨ₐ[" s "] " p:51 => MonadAttach.StateT.AllOutputsFrom s p x - -@[inherit_doc StateT.SomeOutputFrom] -scoped notation:50 x:51 " ⊨ₛ[" s "] " p:51 => MonadAttach.StateT.SomeOutputFrom s p x - -@[inherit_doc StateT.NoOutputFrom] -scoped notation:50 x:51 " ⊭[" s "] " p:51 => MonadAttach.StateT.NoOutputFrom s p x - -omit [Monad m] [LawfulMonad m] [ExactMonadAttach m] in -/-- `supportFrom` is the equality instance of the indexed angelic judgment — the indexed -counterpart of `support_eq_setOf_someOutput`. -/ -theorem StateT.supportFrom_eq_setOf_someOutputFrom {σ : Type u} (s : σ) (x : StateT σ m α) : - StateT.supportFrom s x = {q | StateT.SomeOutputFrom s (fun a s' => (a, s') = q) x} := - Set.ext fun q => ⟨fun hq => ⟨q, hq, rfl⟩, fun ⟨_, hb, hbq⟩ => hbq ▸ hb⟩ - -@[simp] -theorem StateT.allOutputsFrom_pure {σ : Type u} (s : σ) (p : α → σ → Prop) (a : α) : - StateT.AllOutputsFrom s p (pure a : StateT σ m α) ↔ p a s := by - simp [StateT.AllOutputsFrom] - -@[simp] -theorem StateT.someOutputFrom_pure {σ : Type u} (s : σ) (p : α → σ → Prop) (a : α) : - StateT.SomeOutputFrom s p (pure a : StateT σ m α) ↔ p a s := by - simp [StateT.SomeOutputFrom] - -/-- The indexed demonic bind rule. This is the judgment-level form of -`StateT.supportFrom_bind`, and like it needs no exactness on the transformer. -/ -@[simp] -theorem StateT.allOutputsFrom_bind {σ : Type u} (s : σ) (p : β → σ → Prop) - (x : StateT σ m α) (f : α → StateT σ m β) : - StateT.AllOutputsFrom s p (x >>= f) - ↔ ∀ q ∈ StateT.supportFrom s x, StateT.AllOutputsFrom q.2 p (f q.1) := by - constructor - · intro h q hq a ha - exact h a (by rw [StateT.supportFrom_bind]; exact Set.mem_biUnion hq ha) - · intro h a ha - rw [StateT.supportFrom_bind] at ha - obtain ⟨q, hq, ha'⟩ := Set.mem_iUnion₂.mp ha - exact h q hq a ha' - -/-- The indexed angelic bind rule. -/ -@[simp] -theorem StateT.someOutputFrom_bind {σ : Type u} (s : σ) (p : β → σ → Prop) - (x : StateT σ m α) (f : α → StateT σ m β) : - StateT.SomeOutputFrom s p (x >>= f) - ↔ ∃ q ∈ StateT.supportFrom s x, StateT.SomeOutputFrom q.2 p (f q.1) := by - simp only [StateT.SomeOutputFrom, StateT.supportFrom_bind, Set.mem_iUnion, exists_prop] - tauto - -omit [Monad m] [LawfulMonad m] [ExactMonadAttach m] in -theorem StateT.not_someOutputFrom_iff_noOutputFrom {σ : Type u} (s : σ) (p : α → σ → Prop) - (x : StateT σ m α) : - ¬ StateT.SomeOutputFrom s p x ↔ StateT.NoOutputFrom s p x := by - simp [StateT.SomeOutputFrom, StateT.NoOutputFrom, StateT.AllOutputsFrom] - -omit [Monad m] [LawfulMonad m] [ExactMonadAttach m] in -theorem StateT.allOutputsFrom_mono {σ : Type u} {s : σ} {p q : α → σ → Prop} - (h : ∀ a s', p a s' → q a s') {x : StateT σ m α} - (hx : StateT.AllOutputsFrom s p x) : StateT.AllOutputsFrom s q x := - fun r hr => h r.1 r.2 (hx r hr) - -omit [LawfulMonad m] [ExactMonadAttach m] in -/-- Indexed demonic implies flattened demonic: if a value-only `p` holds of every outcome -from every initial state, it holds of every possible output. -/ -theorem StateT.allOutputs_of_allOutputsFrom {σ : Type u} {p : α → Prop} {x : StateT σ m α} - (h : ∀ s, StateT.AllOutputsFrom s (fun a _ => p a) x) : AllOutputs p x := - fun _ ⟨s, s', hs⟩ => h s (_, s') hs - -omit [LawfulMonad m] [ExactMonadAttach m] in -/-- A flattened value-only guarantee holds at every initial state. Flattening loses the -ability to mention the final state, but it loses nothing for postconditions on values -alone. -/ -theorem StateT.allOutputsFrom_of_allOutputs {σ : Type u} {p : α → Prop} {x : StateT σ m α} - (h : AllOutputs p x) (s : σ) : StateT.AllOutputsFrom s (fun a _ => p a) x := - fun q hq => h q.1 ⟨s, q.2, hq⟩ - -omit [LawfulMonad m] [ExactMonadAttach m] in -/-- For value-only postconditions, flattened demonic support is exactly the universal -closure of the indexed judgment. -/ -theorem StateT.allOutputs_iff_forall_allOutputsFrom {σ : Type u} {p : α → Prop} - {x : StateT σ m α} : - AllOutputs p x ↔ ∀ s, StateT.AllOutputsFrom s (fun a _ => p a) x := - ⟨fun h s => StateT.allOutputsFrom_of_allOutputs h s, StateT.allOutputs_of_allOutputsFrom⟩ - -end Instances - end MonadAttach diff --git a/PolyFun/Control/Monad/Support/Indexed.lean b/PolyFun/Control/Monad/Support/Indexed.lean new file mode 100644 index 00000000..3d3fbbac --- /dev/null +++ b/PolyFun/Control/Monad/Support/Indexed.lean @@ -0,0 +1,256 @@ +/- +Copyright (c) 2026 PolyFun Contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Devon Tuma +-/ +module + +public import PolyFun.Control.Monad.Support.Instances + +/-! +# Exact Support: Indexed Support of Stateful Monads + +`StateT` and `ReaderT` carry core's canonical support, existentially quantified over the initial +state or environment, and are deliberately not `ExactMonadAttach`: possible outputs do not +compose along `bind` when the flattened premises choose unrelated initial indices. This file +reasons per run instead: `StateT.supportFrom s x` and `ReaderT.supportAt r x`, their exact +`pure` / `bind` / `map` laws, and the indexed judgments `⊨ₐ[s]` / `⊨ₛ[s]` / `⊭[s]` with their +bridges to the flattened judgments. +-/ + +@[expose] public section + +universe u v w + +namespace MonadAttach + +variable {m : Type u → Type v} {α β : Type u} + +section Indexed + +variable [Monad m] [LawfulMonad m] [MonadAttach m] [ExactMonadAttach m] + +/-! ### Stateful monads + +`StateT` and `ReaderT` do have core `MonadAttach` instances, existentially quantified over +the initial state or environment, and those supports are canonical. They are *not* +`ExactMonadAttach`: possible outputs do not compose along `bind`, because its flattened +premises may be witnessed at different initial indices. Reason per run instead. -/ + +omit [LawfulMonad m] [ExactMonadAttach m] in +theorem mem_support_stateT_iff {σ : Type u} {x : StateT σ m α} {a : α} : + a ∈ support x ↔ ∃ s s', (a, s') ∈ support (x.run s) := + Iff.rfl + +omit [LawfulMonad m] [ExactMonadAttach m] in +theorem mem_support_readerT_iff {ρ : Type u} {x : ReaderT ρ m α} {a : α} : + a ∈ support x ↔ ∃ r, a ∈ support (x.run r) := + Iff.rfl + +omit [LawfulMonad m] [ExactMonadAttach m] in +theorem mem_support_of_run_stateT {σ : Type u} {x : StateT σ m α} {a : α} {s s' : σ} + (h : (a, s') ∈ support (x.run s)) : a ∈ support x := + ⟨s, s', h⟩ + +omit [LawfulMonad m] [ExactMonadAttach m] in +theorem mem_support_of_run_readerT {ρ : Type u} {x : ReaderT ρ m α} {a : α} {r : ρ} + (h : a ∈ support (x.run r)) : a ∈ support x := + ⟨r, h⟩ + +/-! #### Indexed support + +The flattened support above is canonical but coarse: it quantifies the initial state +existentially, and independently on each side of a `bind`, which is exactly why +`ExactMonadAttach` fails. Indexing repairs that. `supportFrom s x` is the set of +result/final-state pairs reachable *from `s`*, and its bind law is exact — the +continuation is only ever run from states the prefix actually produced — needing no +exactness on the transformer, because nothing is flattened away. + +This is the same move the probabilistic semantics makes for the same transformer: +state-indexed computations denote a `Kernel σ (α × σ)` rather than a measure, because +there is no canonical initial state to integrate over. Kernels are to measures as +indexed support is to support. -/ + +/-- The result/final-state pairs reachable by running `x` from the initial state `s`. -/ +def StateT.supportFrom {σ : Type u} (s : σ) (x : StateT σ m α) : Set (α × σ) := + support (x.run s) + +/-- The outputs reachable by running `x` in the environment `r`. -/ +def ReaderT.supportAt {ρ : Type u} (r : ρ) (x : ReaderT ρ m α) : Set α := + support (x.run r) + +omit [Monad m] [LawfulMonad m] [ExactMonadAttach m] in +theorem StateT.mem_supportFrom_iff {σ : Type u} {s : σ} {x : StateT σ m α} {p : α × σ} : + p ∈ StateT.supportFrom s x ↔ p ∈ support (x.run s) := + Iff.rfl + +omit [Monad m] [LawfulMonad m] [ExactMonadAttach m] in +theorem ReaderT.mem_supportAt_iff {ρ : Type u} {r : ρ} {x : ReaderT ρ m α} {a : α} : + a ∈ ReaderT.supportAt r x ↔ a ∈ support (x.run r) := + Iff.rfl + +omit [LawfulMonad m] [ExactMonadAttach m] in +/-- The flattened support is the union of the indexed ones. Recovers +`mem_support_stateT_iff` and pins that indexing loses nothing. -/ +theorem StateT.mem_support_iff_exists_supportFrom {σ : Type u} {x : StateT σ m α} {a : α} : + a ∈ support x ↔ ∃ s s', (a, s') ∈ StateT.supportFrom s x := + Iff.rfl + +omit [LawfulMonad m] [ExactMonadAttach m] in +theorem ReaderT.mem_support_iff_exists_supportAt {ρ : Type u} {x : ReaderT ρ m α} {a : α} : + a ∈ support x ↔ ∃ r, a ∈ ReaderT.supportAt r x := + Iff.rfl + +@[simp, grind =] +theorem StateT.supportFrom_pure {σ : Type u} (s : σ) (a : α) : + StateT.supportFrom s (pure a : StateT σ m α) = {(a, s)} := by + rw [StateT.supportFrom, StateT.run_pure, support_pure] + +@[simp, grind =] +theorem ReaderT.supportAt_pure {ρ : Type u} (r : ρ) (a : α) : + ReaderT.supportAt r (pure a : ReaderT ρ m α) = {a} := by + rw [ReaderT.supportAt, ReaderT.run_pure, support_pure] + +/-- **The exact bind law.** Unlike the flattened `support`, this composes: the +continuation is run only from states the prefix actually produces, so no witness is +chosen independently on the two sides. Needs only `[ExactMonadAttach m]` on the base +monad — `StateT σ m` itself is deliberately not `ExactMonadAttach`, and does not need +to be. -/ +@[simp] +theorem StateT.supportFrom_bind {σ : Type u} (s : σ) (x : StateT σ m α) + (f : α → StateT σ m β) : + StateT.supportFrom s (x >>= f) + = ⋃ p ∈ StateT.supportFrom s x, StateT.supportFrom p.2 (f p.1) := by + rw [StateT.supportFrom, StateT.run_bind, support_bind] + rfl + +/-- The environment version, where the same `r` is threaded to both sides. -/ +@[simp] +theorem ReaderT.supportAt_bind {ρ : Type u} (r : ρ) (x : ReaderT ρ m α) + (f : α → ReaderT ρ m β) : + ReaderT.supportAt r (x >>= f) + = ⋃ a ∈ ReaderT.supportAt r x, ReaderT.supportAt r (f a) := by + rw [ReaderT.supportAt, ReaderT.run_bind, support_bind] + rfl + +@[simp] +theorem StateT.supportFrom_map {σ : Type u} (s : σ) (g : α → β) (x : StateT σ m α) : + StateT.supportFrom s (g <$> x) + = (fun p => (g p.1, p.2)) '' StateT.supportFrom s x := by + rw [StateT.supportFrom, StateT.run_map, support_map] + rfl + +@[simp] +theorem ReaderT.supportAt_map {ρ : Type u} (r : ρ) (g : α → β) (x : ReaderT ρ m α) : + ReaderT.supportAt r (g <$> x) = g '' ReaderT.supportAt r x := by + rw [ReaderT.supportAt, ReaderT.run_map, support_map] + rfl + +/-! #### Indexed judgments + +The modal pair, indexed. These are the primary indexed notions and `supportFrom` is +their equality instance, exactly as `support` is `SomeOutput`'s in the unindexed case +(`support_eq_setOf_someOutput`). The state-indexed predicate ranges over the *pair*: a +`StateT` computation's outcome is a value together with a final state, and forgetting +the state is what makes the flattened judgments fail to compose. -/ + +/-- Every outcome reachable from `s` satisfies `p`. -/ +def StateT.AllOutputsFrom {σ : Type u} (s : σ) (p : α → σ → Prop) (x : StateT σ m α) : Prop := + ∀ q ∈ StateT.supportFrom s x, p q.1 q.2 + +/-- Some outcome reachable from `s` satisfies `p`. -/ +def StateT.SomeOutputFrom {σ : Type u} (s : σ) (p : α → σ → Prop) (x : StateT σ m α) : Prop := + ∃ q ∈ StateT.supportFrom s x, p q.1 q.2 + +/-- No outcome reachable from `s` satisfies `p`. -/ +def StateT.NoOutputFrom {σ : Type u} (s : σ) (p : α → σ → Prop) (x : StateT σ m α) : Prop := + StateT.AllOutputsFrom s (fun a s' => ¬ p a s') x + +@[inherit_doc StateT.AllOutputsFrom] +scoped notation:50 x:51 " ⊨ₐ[" s "] " p:51 => MonadAttach.StateT.AllOutputsFrom s p x + +@[inherit_doc StateT.SomeOutputFrom] +scoped notation:50 x:51 " ⊨ₛ[" s "] " p:51 => MonadAttach.StateT.SomeOutputFrom s p x + +@[inherit_doc StateT.NoOutputFrom] +scoped notation:50 x:51 " ⊭[" s "] " p:51 => MonadAttach.StateT.NoOutputFrom s p x + +omit [Monad m] [LawfulMonad m] [ExactMonadAttach m] in +/-- `supportFrom` is the equality instance of the indexed angelic judgment — the indexed +counterpart of `support_eq_setOf_someOutput`. -/ +theorem StateT.supportFrom_eq_setOf_someOutputFrom {σ : Type u} (s : σ) (x : StateT σ m α) : + StateT.supportFrom s x = {q | StateT.SomeOutputFrom s (fun a s' => (a, s') = q) x} := + Set.ext fun q => ⟨fun hq => ⟨q, hq, rfl⟩, fun ⟨_, hb, hbq⟩ => hbq ▸ hb⟩ + +@[simp] +theorem StateT.allOutputsFrom_pure {σ : Type u} (s : σ) (p : α → σ → Prop) (a : α) : + StateT.AllOutputsFrom s p (pure a : StateT σ m α) ↔ p a s := by + simp [StateT.AllOutputsFrom] + +@[simp] +theorem StateT.someOutputFrom_pure {σ : Type u} (s : σ) (p : α → σ → Prop) (a : α) : + StateT.SomeOutputFrom s p (pure a : StateT σ m α) ↔ p a s := by + simp [StateT.SomeOutputFrom] + +/-- The indexed demonic bind rule. This is the judgment-level form of +`StateT.supportFrom_bind`, and like it needs no exactness on the transformer. -/ +@[simp] +theorem StateT.allOutputsFrom_bind {σ : Type u} (s : σ) (p : β → σ → Prop) + (x : StateT σ m α) (f : α → StateT σ m β) : + StateT.AllOutputsFrom s p (x >>= f) + ↔ ∀ q ∈ StateT.supportFrom s x, StateT.AllOutputsFrom q.2 p (f q.1) := by + constructor + · intro h q hq a ha + exact h a (by rw [StateT.supportFrom_bind]; exact Set.mem_biUnion hq ha) + · intro h a ha + rw [StateT.supportFrom_bind] at ha + obtain ⟨q, hq, ha'⟩ := Set.mem_iUnion₂.mp ha + exact h q hq a ha' + +/-- The indexed angelic bind rule. -/ +@[simp] +theorem StateT.someOutputFrom_bind {σ : Type u} (s : σ) (p : β → σ → Prop) + (x : StateT σ m α) (f : α → StateT σ m β) : + StateT.SomeOutputFrom s p (x >>= f) + ↔ ∃ q ∈ StateT.supportFrom s x, StateT.SomeOutputFrom q.2 p (f q.1) := by + simp only [StateT.SomeOutputFrom, StateT.supportFrom_bind, Set.mem_iUnion, exists_prop] + tauto + +omit [Monad m] [LawfulMonad m] [ExactMonadAttach m] in +theorem StateT.not_someOutputFrom_iff_noOutputFrom {σ : Type u} (s : σ) (p : α → σ → Prop) + (x : StateT σ m α) : + ¬ StateT.SomeOutputFrom s p x ↔ StateT.NoOutputFrom s p x := by + simp [StateT.SomeOutputFrom, StateT.NoOutputFrom, StateT.AllOutputsFrom] + +omit [Monad m] [LawfulMonad m] [ExactMonadAttach m] in +theorem StateT.allOutputsFrom_mono {σ : Type u} {s : σ} {p q : α → σ → Prop} + (h : ∀ a s', p a s' → q a s') {x : StateT σ m α} + (hx : StateT.AllOutputsFrom s p x) : StateT.AllOutputsFrom s q x := + fun r hr => h r.1 r.2 (hx r hr) + +omit [LawfulMonad m] [ExactMonadAttach m] in +/-- Indexed demonic implies flattened demonic: if a value-only `p` holds of every outcome +from every initial state, it holds of every possible output. -/ +theorem StateT.allOutputs_of_allOutputsFrom {σ : Type u} {p : α → Prop} {x : StateT σ m α} + (h : ∀ s, StateT.AllOutputsFrom s (fun a _ => p a) x) : AllOutputs p x := + fun _ ⟨s, s', hs⟩ => h s (_, s') hs + +omit [LawfulMonad m] [ExactMonadAttach m] in +/-- A flattened value-only guarantee holds at every initial state. Flattening loses the +ability to mention the final state, but it loses nothing for postconditions on values +alone. -/ +theorem StateT.allOutputsFrom_of_allOutputs {σ : Type u} {p : α → Prop} {x : StateT σ m α} + (h : AllOutputs p x) (s : σ) : StateT.AllOutputsFrom s (fun a _ => p a) x := + fun q hq => h q.1 ⟨s, q.2, hq⟩ + +omit [LawfulMonad m] [ExactMonadAttach m] in +/-- For value-only postconditions, flattened demonic support is exactly the universal +closure of the indexed judgment. -/ +theorem StateT.allOutputs_iff_forall_allOutputsFrom {σ : Type u} {p : α → Prop} + {x : StateT σ m α} : + AllOutputs p x ↔ ∀ s, StateT.AllOutputsFrom s (fun a _ => p a) x := + ⟨fun h s => StateT.allOutputsFrom_of_allOutputs h s, StateT.allOutputs_of_allOutputsFrom⟩ + +end Indexed + +end MonadAttach diff --git a/PolyFun/Control/Monad/Support/Instances.lean b/PolyFun/Control/Monad/Support/Instances.lean new file mode 100644 index 00000000..6e00fc56 --- /dev/null +++ b/PolyFun/Control/Monad/Support/Instances.lean @@ -0,0 +1,354 @@ +/- +Copyright (c) 2026 PolyFun Contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Devon Tuma +-/ +module + +public import PolyFun.Control.Monad.Support + +/-! +# Exact Support: Instances and Lift Transport + +The instance side of the exact-support layer: the `MonadLiftT m SetM` compatibility shim, +transport of the judgments along a lawful monad lift, the `MonadAttach` / `ExactMonadAttach` +instances core lacks (`Except`, `SetM`) or leaves inexact (`WriterT`), the exactness instances +for `Id`, `Option`, `OptionT`, and `ExceptT`, and the per-monad `CanReturn` unfoldings. The +judgments and their structural laws live in `PolyFun.Control.Monad.Support`; the per-run +support of `StateT` and `ReaderT` lives in `PolyFun.Control.Monad.Support.Indexed`. +-/ + +@[expose] public section + +universe u v w + +namespace MonadAttach + +variable {m : Type u → Type v} {α β : Type u} + +/-! ## Recovering the `MonadLiftT` presentation + +`MonadAttach` is the canonical interface for reachability here: it is core's, it carries +a lawfulness hierarchy, and core supplies instances for the transformers this library +cares about. The `MonadLiftT m SetM` spelling below is a **compatibility shim for a +downstream still phrased that way**, not the recommended API — register it locally when +migrating, rather than building against it. + +Two things this does *not* say. `SetM` remains perfectly good as a **carrier**: +`support : Set α` is unchanged, and `PFunctor.FreeM.support_eq_liftM_univ` — which +genuinely folds into `SetM` as a monad — stays. What is being demoted is the lift as an +*interface*. And unlike the probability layer's `PMF` retirement, there is no upstream +force here: `SetM` is not being deprecated by Mathlib. This is a project standardizing +on core's vocabulary, nothing more. + +One concrete argument for the direction, which is otherwise recorded nowhere: +`support_eq_liftM_univ` is restricted to `{γ : Type uB}`, because `FreeM.liftM` pins the +payload universe to the *direction* universe. `MonadAttach.support` on `FreeM P` carries +no such restriction. The attach-based presentation is strictly more universe-polymorphic +than the fold. + +The two declarations are deliberately not instances, so that support reasoning does not +perturb monad-lift instance search. -/ + +/-- The support map as a monad lift into `SetM`. Not an instance. -/ +@[instance_reducible] +def toMonadLiftT (m : Type u → Type v) [MonadAttach m] : + MonadLiftT m SetM where + monadLift x := (support x : SetM _) + +/-- The support lift is lawful. Not an instance. -/ +theorem toLawfulMonadLiftT (m : Type u → Type v) [Monad m] [LawfulMonad m] [MonadAttach m] + [ExactMonadAttach m] : + letI := toMonadLiftT m + LawfulMonadLiftT m SetM := + letI := toMonadLiftT m + { monadLift_pure := fun a => support_pure a + monadLift_bind := fun x f => support_bind x f } + +/-! ## Transport along a monad lift + +Core proves the elimination half — lifting cannot *create* possible outputs — so a +lift can only shrink the support, and a demonic obligation therefore transfers along +it for free. + +The introduction half is **not** available generically, and cannot be: nothing in +`MonadLiftT` or its lawfulness class says the lift preserves reachability, and a lift +into a monad whose `CanReturn` is uniformly `False` satisfies every law while losing +every output. A caller that needs `support (liftM x) = support x` must supply that +equation for its particular lift; `FreeM`'s powerset fold +(`PFunctor.FreeM.support_eq_liftM_univ`) is the worked instance. -/ + +section Transport + +variable {m : Type u → Type v} {n : Type u → Type w} {α : Type u} +variable [Monad m] [LawfulMonad m] [MonadAttach m] [LawfulMonadAttach m] +variable [Monad n] [LawfulMonad n] [MonadAttach n] [LawfulMonadAttach n] +variable [MonadLiftT m n] [LawfulMonadLiftT m n] + +/-- Lifting cannot create possible outputs. The set form of core's +`LawfulMonadAttach.canReturn_liftM_imp'`. -/ +theorem support_liftM_subset (x : m α) : support (liftM x : n α) ⊆ support x := + fun _ h => LawfulMonadAttach.canReturn_liftM_imp' h + +/-- A demonic guarantee survives lifting: the lifted computation has no outputs the +original did not have, so a property of all of the original's outputs holds of all of +the lift's. -/ +theorem allOutputs_liftM {p : α → Prop} {x : m α} (h : AllOutputs p x) : + AllOutputs p (liftM x : n α) := + fun a ha => h a (support_liftM_subset x ha) + +/-- Dually, an angelic fact about the lift transfers back to the original. -/ +theorem someOutput_of_someOutput_liftM {p : α → Prop} {x : m α} + (h : SomeOutput p (liftM x : n α)) : SomeOutput p x := + h.imp fun _ ⟨ha, hp⟩ => ⟨support_liftM_subset x ha, hp⟩ + +/-- And a "never" guarantee survives lifting. -/ +theorem noOutput_liftM {p : α → Prop} {x : m α} (h : NoOutput p x) : + NoOutput p (liftM x : n α) := + fun a ha => h a (support_liftM_subset x ha) + +end Transport + +/-! ## Base instances + +Core supplies `MonadAttach` and `LawfulMonadAttach` for `Id`, `Option`, `OptionT`, +`ExceptT`, `StateT`, and `ReaderT`; only the exactness fields are needed here. `Except` and +`SetM` have no core instance and are supplied below. -/ + +section Instances + +/-- Core provides no `MonadAttach (Except ε)` at this pin, only the transformer version; this +mirrors core's `Option` instance. An identical declaration has landed upstream and ships in +Lean v4.35, so delete this instance and the one below it at that toolchain bump. -/ +instance instMonadAttachExcept {ε : Type u} : MonadAttach (Except ε) where + CanReturn x a := x = Except.ok a + attach + | .ok a => .ok ⟨a, rfl⟩ + | .error e => .error e + +instance instLawfulMonadAttachExcept {ε : Type u} : LawfulMonadAttach (Except ε) where + map_attach {_ x} := by cases x <;> rfl + canReturn_map_imp {_ _ x _} h := by + cases x with + | error e => cases h + | ok z => cases h; exact z.2 + +/-- Core's `MonadAttach (ExceptT ε m)` is stated at `max`-joined universes, which blocks +synthesis in a universe-polymorphic context; this alias instantiates it at a single +universe. Delete once the upstream declaration is repaired. -/ +instance instMonadAttachExceptT {ε : Type u} {m : Type u → Type v} [Monad m] + [MonadAttach m] : MonadAttach (ExceptT ε m) := + instMonadAttachExceptTOfMonad.{u, u, v} + +/-- The powerset monad is its own support. -/ +instance instMonadAttachSetM : MonadAttach SetM where + CanReturn s a := a ∈ SetM.run s + attach _ := (Set.univ : Set _) + +instance instLawfulMonadAttachSetM : LawfulMonadAttach SetM where + map_attach {_ x} := by + change Subtype.val '' (Set.univ : Set {a // a ∈ SetM.run x}) = x + ext a + simp [SetM.run] + canReturn_map_imp {_ _ _ _} h := by + obtain ⟨z, -, hz⟩ := h + exact hz ▸ z.2 + +instance instExactMonadAttachId : ExactMonadAttach Id where + canReturn_pure _ := rfl + canReturn_bind h h' := by + simp only [CanReturn, Id.run] at * + subst h + exact h' + +instance instExactMonadAttachOption : ExactMonadAttach Option where + canReturn_pure _ := rfl + canReturn_bind {_ _ _ _ _ _} h h' := by + simp only [CanReturn] at * + subst h + simpa using h' + +instance instExactMonadAttachExcept {ε : Type u} : ExactMonadAttach (Except ε) where + canReturn_pure _ := rfl + canReturn_bind ha hb := by cases ha; exact hb + +instance instExactMonadAttachSetM : ExactMonadAttach SetM where + canReturn_pure _ := rfl + canReturn_bind {_ _ _ _ a _} ha hb := Set.mem_iUnion.mpr ⟨a, Set.mem_iUnion.mpr ⟨ha, hb⟩⟩ + +variable {m : Type u → Type v} [Monad m] [LawfulMonad m] [MonadAttach m] [ExactMonadAttach m] + +instance instExactMonadAttachOptionT : ExactMonadAttach (OptionT m) where + canReturn_pure {α} a := by + change CanReturn ((pure a : OptionT m α)).run (some a) + rw [OptionT.run_pure] + exact ExactMonadAttach.canReturn_pure _ + canReturn_bind {α β x f a b} h h' := by + change CanReturn ((x >>= f : OptionT m β)).run (some b) + have hrun : ((x >>= f : OptionT m β)).run = x.run >>= fun o => + match o with + | some c => (f c).run + | none => pure none := rfl + rw [hrun] + exact ExactMonadAttach.canReturn_bind (a := some a) h h' + +instance instExactMonadAttachExceptT {ε : Type u} : ExactMonadAttach (ExceptT ε m) where + canReturn_pure {α} a := by + change CanReturn ((pure a : ExceptT ε m α)).run (Except.ok a) + rw [ExceptT.run_pure] + exact ExactMonadAttach.canReturn_pure _ + canReturn_bind {α β x f a b} h h' := by + change CanReturn ((x >>= f : ExceptT ε m β)).run (Except.ok b) + have hrun : ((x >>= f : ExceptT ε m β)).run = x.run >>= fun e => + match e with + | Except.ok c => (f c).run + | Except.error e => pure (Except.error e) := rfl + rw [hrun] + exact ExactMonadAttach.canReturn_bind (a := Except.ok a) h h' + +/-! ### Per-monad unfoldings + +Each base monad's `CanReturn` is a concrete predicate, so membership in its support +has a concrete spelling. Every one of these is `Iff.rfl`; naming them keeps callers +from reaching through `support` and `CanReturn` with `change`. -/ + +section Unfoldings + +variable {α : Type u} + +@[simp, grind =] +theorem Id.canReturn_iff {x : Id α} {a : α} : CanReturn x a ↔ x.run = a := + Iff.rfl + +@[simp] +theorem Id.support_eq_singleton (x : Id α) : support x = {x.run} := by + ext a + rw [mem_support, Id.canReturn_iff, Set.mem_singleton_iff] + exact eq_comm + +@[simp, grind =] +theorem Option.canReturn_iff {x : Option α} {a : α} : CanReturn x a ↔ x = some a := + Iff.rfl + +@[simp, grind =] +theorem Option.support_some (a : α) : support (some a) = {a} := by + ext b + rw [mem_support, Option.canReturn_iff, Set.mem_singleton_iff] + exact ⟨fun h => (Option.some.inj h).symm, fun h => by rw [h]⟩ + +@[simp, grind =] +theorem Option.support_none : support (none : Option α) = ∅ := by + ext b + rw [mem_support, Option.canReturn_iff] + simp + +@[simp, grind =] +theorem Except.canReturn_iff {ε : Type u} {x : Except ε α} {a : α} : + CanReturn x a ↔ x = Except.ok a := + Iff.rfl + +@[simp, grind =] +theorem Except.support_ok {ε : Type u} (a : α) : support (Except.ok a : Except ε α) = {a} := by + ext b + rw [mem_support, Except.canReturn_iff, Set.mem_singleton_iff] + exact ⟨fun h => (Except.ok.inj h).symm, fun h => by rw [h]⟩ + +@[simp, grind =] +theorem Except.support_error {ε : Type u} (e : ε) : + support (Except.error e : Except ε α) = ∅ := by + ext b + rw [mem_support, Except.canReturn_iff] + simp + +@[simp, grind =] +theorem SetM.canReturn_iff {x : SetM α} {a : α} : CanReturn x a ↔ a ∈ SetM.run x := + Iff.rfl + +@[simp] +theorem SetM.support_eq_run (x : SetM α) : support x = SetM.run x := + Set.ext fun _ => Iff.rfl + +variable {m : Type u → Type v} [Monad m] [MonadAttach m] + +@[simp, grind =] +theorem OptionT.canReturn_iff {x : OptionT m α} {a : α} : + CanReturn x a ↔ some a ∈ support x.run := + Iff.rfl + +@[simp, grind =] +theorem ExceptT.canReturn_iff {ε : Type u} {x : ExceptT ε m α} {a : α} : + CanReturn x a ↔ Except.ok a ∈ support x.run := + Iff.rfl + +end Unfoldings + +/-! ### The writer transformer + +`WriterT ω m` accumulates an output alongside the value, so the honest reading of its +support is the one that keeps that output: a value is possible exactly when it is +returned *together with some accumulator*. This is the same rule the measure semantics +uses for the same transformer — a writer computation denotes the underlying `m (α × ω)` +rather than discarding `ω` — and unlike `StateT` it costs nothing, because there is no +*input* index to choose. Both introduction rules survive: `pure` writes the unit, and +two composable outputs compose with their accumulators multiplied. -/ + +section WriterT + +variable {ω : Type u} [Monoid ω] + +instance instMonadAttachWriterT : MonadAttach (WriterT ω m) where + CanReturn x a := ∃ w, CanReturn x.run (a, w) + attach x := WriterT.mk <| + (fun p => (⟨p.1.1, ⟨p.1.2, p.2⟩⟩, p.1.2)) <$> MonadAttach.attach x.run + +omit [LawfulMonad m] [ExactMonadAttach m] [Monoid ω] in +theorem mem_support_writerT_iff {x : WriterT ω m α} {a : α} : + a ∈ support x ↔ ∃ w, (a, w) ∈ support x.run := + Iff.rfl + +omit [LawfulMonad m] [ExactMonadAttach m] [Monoid ω] in +theorem mem_support_of_run_writerT {x : WriterT ω m α} {a : α} {w : ω} + (h : (a, w) ∈ support x.run) : a ∈ support x := + ⟨w, h⟩ + +instance instWeaklyLawfulMonadAttachWriterT : + WeaklyLawfulMonadAttach (WriterT ω m) where + map_attach {α x} := by + refine WriterT.ext _ _ ?_ + rw [WriterT.run_map] + have hrun : (MonadAttach.attach x : WriterT ω m (Subtype (CanReturn x))).run + = (fun p : Subtype (CanReturn x.run) => + ((⟨p.1.1, ⟨p.1.2, p.2⟩⟩ : Subtype (CanReturn x)), p.1.2)) + <$> MonadAttach.attach x.run := rfl + rw [hrun, Functor.map_map] + simpa [Function.comp_def] using WeaklyLawfulMonadAttach.map_attach (m := m) (x := x.run) + +instance instLawfulMonadAttachWriterT : LawfulMonadAttach (WriterT ω m) where + canReturn_map_imp {α P x a} h := by + obtain ⟨w, hw⟩ := h + rw [WriterT.run_map] at hw + obtain ⟨q, -, hqa⟩ := LawfulMonadAttach.canReturn_map_imp' hw + obtain ⟨⟨v, hv⟩, w'⟩ := q + cases hqa + exact hv + +/-- Both introduction rules hold: `pure` writes the unit accumulator, and composable +outputs compose with their accumulators multiplied. This is what `StateT` cannot have — +there is no input index to quantify over, so nothing is flattened away. -/ +instance instExactMonadAttachWriterT : ExactMonadAttach (WriterT ω m) where + canReturn_pure {α} a := ⟨1, ExactMonadAttach.canReturn_pure _⟩ + canReturn_bind {α β x f a b} h h' := by + obtain ⟨w₁, hw₁⟩ := h + obtain ⟨w₂, hw₂⟩ := h' + refine ⟨w₁ * w₂, ?_⟩ + change CanReturn (x.run >>= fun p => (fun q => (q.1, p.2 * q.2)) <$> (f p.1).run) (b, w₁ * w₂) + refine ExactMonadAttach.canReturn_bind (a := (a, w₁)) hw₁ ?_ + have hmem : ((b, w₂) : β × ω) ∈ support (f a).run := hw₂ + have himg := Set.mem_image_of_mem (fun q : β × ω => (q.1, w₁ * q.2)) hmem + rwa [← support_map] at himg + +end WriterT + +end Instances + +end MonadAttach diff --git a/PolyFun/Control/Monad/Support/Loops.lean b/PolyFun/Control/Monad/Support/Loops.lean new file mode 100644 index 00000000..eed07dee --- /dev/null +++ b/PolyFun/Control/Monad/Support/Loops.lean @@ -0,0 +1,141 @@ +/- +Copyright (c) 2026 PolyFun Contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Devon Tuma +-/ +module + +public import PolyFun.Control.Monad.Support.WP + +/-! +# Loop Rules for Exact Support + +`for` loops elaborate to `forIn` / `forIn'` over the iterated container, and `forM` / `foldlM` +are their common special cases. Under the demonic interpretation `wp x post = AllOutputs post x` +(`MonadAttach.toWPMonadDemonic`), core's list-loop specifications `Spec.forIn'_list`, +`Spec.forIn_list`, and `Spec.foldlM_list` *are* invariant rules for the "always" judgment, and +the angelic interpretation gives their "sometimes" twins; this file states them in that form so +that support reasoning about loops needs no `vcgen` and no `Triple`. Containers whose loop is +the loop over the list `ForIn.toList` computes (`Std.Internal.PureForIn`: lists, arrays, +ranges, slices, iterators, and `Option` / `Vector` via `ToCslib.Control.ForIn`) reduce to the +list rules. `forM` has no core specification and is proved by induction. + +Invariants follow core's shape: a predicate on the elements consumed so far, the elements +remaining, and the accumulator. The rules are directed reasoning steps, not equations, and are +therefore untagged. +-/ + +@[expose] public section + +universe u v w w' + +open Std.Internal.Do + +namespace MonadAttach + +variable {m : Type u → Type v} [Monad m] [LawfulMonad m] [MonadAttach m] [ExactMonadAttach m] + {ι : Type w} {β : Type u} + +/-! ## Lists -/ + +theorem allOutputs_forIn'_list_of_inv {xs : List ι} {init : β} + {f : (a : ι) → a ∈ xs → β → m (ForInStep β)} (inv : List ι → List ι → β → Prop) + (step : ∀ pref cur suff (h : xs = pref ++ cur :: suff) b, inv pref (cur :: suff) b → + AllOutputs (fun r => match r with + | .yield b' => inv (pref ++ [cur]) suff b' + | .done b' => inv xs [] b') (f cur (by simp [h]) b)) + (hinit : inv [] xs init) : AllOutputs (inv xs []) (forIn' xs init f) := by + let inst := toWPMonadDemonic (m := m) + exact (Spec.forIn'_list (m := m) inv (epost := Lean.Order.bot) + fun pref cur suff h b => ⟨fun hpre => step pref cur suff h b hpre⟩).le_wp hinit + +theorem allOutputs_forIn_list_of_inv {xs : List ι} {init : β} {f : ι → β → m (ForInStep β)} + (inv : List ι → List ι → β → Prop) + (step : ∀ pref cur suff, xs = pref ++ cur :: suff → ∀ b, inv pref (cur :: suff) b → + AllOutputs (fun r => match r with + | .yield b' => inv (pref ++ [cur]) suff b' + | .done b' => inv xs [] b') (f cur b)) + (hinit : inv [] xs init) : AllOutputs (inv xs []) (forIn xs init f) := by + let inst := toWPMonadDemonic (m := m) + exact (Spec.forIn_list (m := m) inv (epost := Lean.Order.bot) + fun pref cur suff h b => ⟨fun hpre => step pref cur suff h b hpre⟩).le_wp hinit + +/-- `allOutputs_forIn_list_of_inv` with an invariant on the accumulator alone. -/ +theorem allOutputs_forIn_list_of_const_inv {xs : List ι} {init : β} {f : ι → β → m (ForInStep β)} + (inv : β → Prop) + (step : ∀ cur ∈ xs, ∀ b, inv b → + AllOutputs (fun r => match r with | .yield b' => inv b' | .done b' => inv b') (f cur b)) + (hinit : inv init) : AllOutputs inv (forIn xs init f) := + allOutputs_forIn_list_of_inv (fun _ _ b => inv b) + (fun _ cur _ h b hb => + step cur (by rw [h]; exact List.mem_append_right _ (List.Mem.head _)) b hb) + hinit + +theorem allOutputs_foldlM_list_of_inv {xs : List ι} {init : β} {f : β → ι → m β} + (inv : List ι → List ι → β → Prop) + (step : ∀ pref cur suff, xs = pref ++ cur :: suff → ∀ b, inv pref (cur :: suff) b → + AllOutputs (fun b' => inv (pref ++ [cur]) suff b') (f b cur)) + (hinit : inv [] xs init) : AllOutputs (inv xs []) (xs.foldlM f init) := by + let inst := toWPMonadDemonic (m := m) + exact (Spec.foldlM_list (m := m) inv (epost := Lean.Order.bot) + fun pref cur suff h b => ⟨fun hpre => step pref cur suff h b hpre⟩).le_wp hinit + +theorem allOutputs_forM_list_of_inv {xs : List ι} {f : ι → m PUnit} + (inv : List ι → List ι → Prop) + (step : ∀ pref cur suff, xs = pref ++ cur :: suff → inv pref (cur :: suff) → + AllOutputs (fun _ => inv (pref ++ [cur]) suff) (f cur)) + (hinit : inv [] xs) : AllOutputs (fun _ => inv xs []) (xs.forM f) := by + suffices h : ∀ pref suff, xs = pref ++ suff → inv pref suff → + AllOutputs (fun _ => inv xs []) (suff.forM f) from h [] xs rfl hinit + intro pref suff + induction suff generalizing pref with + | nil => + intro hxs hinv + simp only [List.forM_eq_forM, List.forM_nil, allOutputs_pure] + simpa [hxs] using hinv + | cons x suff ih => + intro hxs hinv + simp only [List.forM_eq_forM, List.forM_cons, allOutputs_bind] + intro u hu + exact ih (pref ++ [x]) (by simp [hxs]) (step pref x suff hxs hinv u hu) + +/-! ## Angelic twins -/ + +theorem someOutput_forIn'_list_of_inv {xs : List ι} {init : β} + {f : (a : ι) → a ∈ xs → β → m (ForInStep β)} (inv : List ι → List ι → β → Prop) + (step : ∀ pref cur suff (h : xs = pref ++ cur :: suff) b, inv pref (cur :: suff) b → + SomeOutput (fun r => match r with + | .yield b' => inv (pref ++ [cur]) suff b' + | .done b' => inv xs [] b') (f cur (by simp [h]) b)) + (hinit : inv [] xs init) : SomeOutput (inv xs []) (forIn' xs init f) := by + let inst := toWPMonadAngelic (m := m) + exact (Spec.forIn'_list (m := m) inv (epost := Lean.Order.bot) + fun pref cur suff h b => ⟨fun hpre => step pref cur suff h b hpre⟩).le_wp hinit + +theorem someOutput_forIn_list_of_inv {xs : List ι} {init : β} {f : ι → β → m (ForInStep β)} + (inv : List ι → List ι → β → Prop) + (step : ∀ pref cur suff, xs = pref ++ cur :: suff → ∀ b, inv pref (cur :: suff) b → + SomeOutput (fun r => match r with + | .yield b' => inv (pref ++ [cur]) suff b' + | .done b' => inv xs [] b') (f cur b)) + (hinit : inv [] xs init) : SomeOutput (inv xs []) (forIn xs init f) := by + let inst := toWPMonadAngelic (m := m) + exact (Spec.forIn_list (m := m) inv (epost := Lean.Order.bot) + fun pref cur suff h b => ⟨fun hpre => step pref cur suff h b hpre⟩).le_wp hinit + +/-! ## Containers iterating over a list -/ + +theorem allOutputs_forIn_of_pureForIn {ρ : Type w'} [ForIn m ρ ι] [ForIn Id ρ ι] + [Std.Internal.PureForIn m ρ ι] (xs : ρ) {init : β} {f : ι → β → m (ForInStep β)} + (inv : List ι → List ι → β → Prop) + (step : ∀ pref cur suff, ForIn.toList xs = pref ++ cur :: suff → ∀ b, + inv pref (cur :: suff) b → + AllOutputs (fun r => match r with + | .yield b' => inv (pref ++ [cur]) suff b' + | .done b' => inv (ForIn.toList xs) [] b') (f cur b)) + (hinit : inv [] (ForIn.toList xs) init) : + AllOutputs (inv (ForIn.toList xs) []) (forIn xs init f) := by + rw [Std.Internal.PureForIn.forIn_eq] + exact allOutputs_forIn_list_of_inv inv step hinit + +end MonadAttach diff --git a/PolyFun/Control/Monad/Support/Structural.lean b/PolyFun/Control/Monad/Support/Structural.lean new file mode 100644 index 00000000..30437101 --- /dev/null +++ b/PolyFun/Control/Monad/Support/Structural.lean @@ -0,0 +1,220 @@ +/- +Copyright (c) 2026 PolyFun Contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Devon Tuma +-/ +module + +public import PolyFun.Control.Monad.Support + +/-! +# Structural Laws of Exact Support for the `do` Fragment + +`PolyFun.Control.Monad.Support` keys the exact-support laws on `pure` and `bind` and pushes the +set-valued `support` through `map`, `seq`, `ite`, and `dite`. `do`-notation elaborates to more +than that: applicative sequencing `<*` / `*>`, `if` / `if h :`, and `match` on `Option` and `Sum` +(elaborated through `Option.elim` / `Sum.elim`, or left as a `match` that `split` reduces to the +same shapes). This file states each of those for the reachability predicate `CanReturn` and for +the three judgments `AllOutputs` / `SomeOutput` / `NoOutput`, so that a goal about a `do` block +decomposes without unfolding the judgments. + +### Automation contract + +The `CanReturn` equations for `Option.elim` and `Sum.elim` are `@[simp, grind =]`, extending the +`canReturn_pure_iff` / `bind_iff` / `map_iff` chain. Those for `ite` / `dite` and for `<*` / `*>` +are `@[simp]` only: `grind` handles `if` by its own case splitting and refuses `ite` as a pattern +head, and the second operand of `<*` / `*>` sits under the thunk `fun _ => y`, which a pattern +cannot bind. The judgment-level rules are `@[simp]` only, following the root file's contract: +they quantify over outputs, and letting `grind` instantiate quantifier characterizations +saturates it. +-/ + +@[expose] public section + +universe u v w w' + +namespace MonadAttach + +variable {m : Type u → Type v} {α β : Type u} {γ : Type w} {δ : Type w'} + +/-! ## Branching -/ + +section Branching + +variable [MonadAttach m] + +@[simp] +theorem canReturn_ite (c : Prop) [Decidable c] (x y : m α) (a : α) : + CanReturn (if c then x else y) a ↔ if c then CanReturn x a else CanReturn y a := by + split <;> rfl + +@[simp] +theorem canReturn_dite (c : Prop) [Decidable c] (x : c → m α) (y : ¬ c → m α) (a : α) : + CanReturn (if h : c then x h else y h) a ↔ + if h : c then CanReturn (x h) a else CanReturn (y h) a := by + split <;> rfl + +@[simp, grind =] +theorem canReturn_option_elim (o : Option γ) (x : m α) (f : γ → m α) (a : α) : + CanReturn (o.elim x f) a ↔ + (o = none → CanReturn x a) ∧ ∀ c, o = some c → CanReturn (f c) a := by + cases o <;> simp + +@[simp, grind =] +theorem canReturn_sum_elim (s : γ ⊕ δ) (f : γ → m α) (g : δ → m α) (a : α) : + CanReturn (s.elim f g) a ↔ + (∀ c, s = .inl c → CanReturn (f c) a) ∧ ∀ d, s = .inr d → CanReturn (g d) a := by + cases s <;> simp + +@[simp] +theorem allOutputs_ite (c : Prop) [Decidable c] (p : α → Prop) (x y : m α) : + AllOutputs p (if c then x else y) ↔ if c then AllOutputs p x else AllOutputs p y := by + split <;> rfl + +@[simp] +theorem allOutputs_dite (c : Prop) [Decidable c] (p : α → Prop) (x : c → m α) + (y : ¬ c → m α) : + AllOutputs p (if h : c then x h else y h) ↔ + if h : c then AllOutputs p (x h) else AllOutputs p (y h) := by + split <;> rfl + +@[simp] +theorem someOutput_ite (c : Prop) [Decidable c] (p : α → Prop) (x y : m α) : + SomeOutput p (if c then x else y) ↔ if c then SomeOutput p x else SomeOutput p y := by + split <;> rfl + +@[simp] +theorem someOutput_dite (c : Prop) [Decidable c] (p : α → Prop) (x : c → m α) + (y : ¬ c → m α) : + SomeOutput p (if h : c then x h else y h) ↔ + if h : c then SomeOutput p (x h) else SomeOutput p (y h) := by + split <;> rfl + +@[simp] +theorem noOutput_ite (c : Prop) [Decidable c] (p : α → Prop) (x y : m α) : + NoOutput p (if c then x else y) ↔ if c then NoOutput p x else NoOutput p y := by + split <;> rfl + +@[simp] +theorem noOutput_dite (c : Prop) [Decidable c] (p : α → Prop) (x : c → m α) + (y : ¬ c → m α) : + NoOutput p (if h : c then x h else y h) ↔ + if h : c then NoOutput p (x h) else NoOutput p (y h) := by + split <;> rfl + +@[simp] +theorem allOutputs_option_elim (o : Option γ) (p : α → Prop) (x : m α) (f : γ → m α) : + AllOutputs p (o.elim x f) ↔ + (o = none → AllOutputs p x) ∧ ∀ c, o = some c → AllOutputs p (f c) := by + cases o <;> simp + +@[simp] +theorem someOutput_option_elim (o : Option γ) (p : α → Prop) (x : m α) (f : γ → m α) : + SomeOutput p (o.elim x f) ↔ + (o = none → SomeOutput p x) ∧ ∀ c, o = some c → SomeOutput p (f c) := by + cases o <;> simp + +@[simp] +theorem allOutputs_sum_elim (s : γ ⊕ δ) (p : α → Prop) (f : γ → m α) (g : δ → m α) : + AllOutputs p (s.elim f g) ↔ + (∀ c, s = .inl c → AllOutputs p (f c)) ∧ ∀ d, s = .inr d → AllOutputs p (g d) := by + cases s <;> simp + +@[simp] +theorem someOutput_sum_elim (s : γ ⊕ δ) (p : α → Prop) (f : γ → m α) (g : δ → m α) : + SomeOutput p (s.elim f g) ↔ + (∀ c, s = .inl c → SomeOutput p (f c)) ∧ ∀ d, s = .inr d → SomeOutput p (g d) := by + cases s <;> simp + +end Branching + +/-! ## Functor and applicative structure -/ + +section Applicative + +variable [Monad m] [LawfulMonad m] [MonadAttach m] [ExactMonadAttach m] + +@[simp] +theorem allOutputs_map_iff (p : β → Prop) (g : α → β) (x : m α) : + AllOutputs p (g <$> x) ↔ AllOutputs (fun a => p (g a)) x := by + simp only [AllOutputs, canReturn_map_iff] + exact ⟨fun h a ha => h (g a) ⟨a, ha, rfl⟩, fun h _ ⟨a, ha, hab⟩ => hab ▸ h a ha⟩ + +@[simp] +theorem someOutput_map_iff (p : β → Prop) (g : α → β) (x : m α) : + SomeOutput p (g <$> x) ↔ SomeOutput (fun a => p (g a)) x := by + simp only [SomeOutput, canReturn_map_iff] + exact ⟨fun ⟨_, ⟨a, ha, hab⟩, hp⟩ => ⟨a, ha, hab ▸ hp⟩, fun ⟨a, ha, hp⟩ => ⟨g a, ⟨a, ha, rfl⟩, hp⟩⟩ + +@[simp] +theorem noOutput_map_iff (p : β → Prop) (g : α → β) (x : m α) : + NoOutput p (g <$> x) ↔ NoOutput (fun a => p (g a)) x := + allOutputs_map_iff (fun b => ¬ p b) g x + +@[simp] +theorem allOutputs_seq_iff (p : β → Prop) (f : m (α → β)) (x : m α) : + AllOutputs p (f <*> x) ↔ AllOutputs (fun g => AllOutputs (fun a => p (g a)) x) f := by + rw [seq_eq_bind_map, allOutputs_bind] + simp only [allOutputs_map_iff] + exact Iff.rfl + +@[simp] +theorem someOutput_seq_iff (p : β → Prop) (f : m (α → β)) (x : m α) : + SomeOutput p (f <*> x) ↔ SomeOutput (fun g => SomeOutput (fun a => p (g a)) x) f := by + rw [seq_eq_bind_map, someOutput_bind] + simp only [someOutput_map_iff] + exact Iff.rfl + +@[simp] +theorem canReturn_seqLeft_iff {x : m α} {y : m β} {a : α} : + CanReturn (x <* y) a ↔ CanReturn x a ∧ ∃ b, CanReturn y b := by + rw [seqLeft_eq_bind] + simp only [canReturn_bind_iff, canReturn_pure_iff] + exact ⟨fun ⟨_, ha, b, hb, hab⟩ => hab ▸ ⟨ha, b, hb⟩, fun ⟨ha, b, hb⟩ => ⟨a, ha, b, hb, rfl⟩⟩ + +@[simp] +theorem canReturn_seqRight_iff {x : m α} {y : m β} {b : β} : + CanReturn (x *> y) b ↔ (∃ a, CanReturn x a) ∧ CanReturn y b := by + rw [seqRight_eq_bind] + simp only [canReturn_bind_iff] + exact ⟨fun ⟨a, ha, hb⟩ => ⟨⟨a, ha⟩, hb⟩, fun ⟨⟨a, ha⟩, hb⟩ => ⟨a, ha, hb⟩⟩ + +@[simp] +theorem support_seqLeft (x : m α) (y : m β) : + support (x <* y) = {a | a ∈ support x ∧ (support y).Nonempty} := by + ext a + simp [Set.Nonempty] + +@[simp] +theorem support_seqRight (x : m α) (y : m β) : + support (x *> y) = {b | (support x).Nonempty ∧ b ∈ support y} := by + ext b + simp [Set.Nonempty] + +@[simp] +theorem allOutputs_seqLeft_iff (p : α → Prop) (x : m α) (y : m β) : + AllOutputs p (x <* y) ↔ ((∃ b, CanReturn y b) → AllOutputs p x) := by + simp only [AllOutputs, canReturn_seqLeft_iff] + exact ⟨fun h hy a ha => h a ⟨ha, hy⟩, fun h a ⟨ha, hy⟩ => h hy a ha⟩ + +@[simp] +theorem allOutputs_seqRight_iff (p : β → Prop) (x : m α) (y : m β) : + AllOutputs p (x *> y) ↔ ((∃ a, CanReturn x a) → AllOutputs p y) := by + simp only [AllOutputs, canReturn_seqRight_iff] + exact ⟨fun h hx b hb => h b ⟨hx, hb⟩, fun h b ⟨hx, hb⟩ => h hx b hb⟩ + +@[simp] +theorem someOutput_seqLeft_iff (p : α → Prop) (x : m α) (y : m β) : + SomeOutput p (x <* y) ↔ SomeOutput p x ∧ ∃ b, CanReturn y b := by + simp only [SomeOutput, canReturn_seqLeft_iff] + exact ⟨fun ⟨a, ⟨ha, hy⟩, hp⟩ => ⟨⟨a, ha, hp⟩, hy⟩, fun ⟨⟨a, ha, hp⟩, hy⟩ => ⟨a, ⟨ha, hy⟩, hp⟩⟩ + +@[simp] +theorem someOutput_seqRight_iff (p : β → Prop) (x : m α) (y : m β) : + SomeOutput p (x *> y) ↔ (∃ a, CanReturn x a) ∧ SomeOutput p y := by + simp only [SomeOutput, canReturn_seqRight_iff] + exact ⟨fun ⟨b, ⟨hx, hb⟩, hp⟩ => ⟨hx, b, hb, hp⟩, fun ⟨hx, b, hb, hp⟩ => ⟨b, ⟨hx, hb⟩, hp⟩⟩ + +end Applicative + +end MonadAttach diff --git a/PolyFun/PFunctor/Free/Support.lean b/PolyFun/PFunctor/Free/Support.lean index 565614c9..411254c1 100644 --- a/PolyFun/PFunctor/Free/Support.lean +++ b/PolyFun/PFunctor/Free/Support.lean @@ -5,7 +5,7 @@ Authors: Devon Tuma -/ module -public import PolyFun.Control.Monad.Support +public import PolyFun.Control.Monad.Support.Instances public import PolyFun.PFunctor.Free.Path /-! diff --git a/PolyFun/PFunctor/Free/WP.lean b/PolyFun/PFunctor/Free/WP.lean index 926072fa..d04ef8b7 100644 --- a/PolyFun/PFunctor/Free/WP.lean +++ b/PolyFun/PFunctor/Free/WP.lean @@ -125,6 +125,62 @@ theorem wpFold_bind (Φ : OpSpec P l) (x : FreeM P α) (f : α → FreeM P β) | pure x => rfl | lift_bind a r ih => exact congrArg (Φ a) (funext fun b => ih b) +/-! ### The rest of the `do` fragment + +`wpFold` is a fold, so every combinator `do`-notation elaborates to reduces to `wpFold_bind` and +`wpFold_pure`; the equations below state the results directly so `simp` need not rediscover +them. -/ + +@[simp] +theorem wpFold_map (Φ : OpSpec P l) (f : α → β) (x : FreeM P α) (post : β → l) : + wpFold Φ (f <$> x) post = wpFold Φ x fun a => post (f a) := by + induction x with + | pure a => rfl + | lift_bind a r ih => exact congrArg (Φ a) (funext fun b => ih b) + +@[simp] +theorem wpFold_seq (Φ : OpSpec P l) (f : FreeM P (α → β)) (x : FreeM P α) (post : β → l) : + wpFold Φ (f <*> x) post = wpFold Φ f fun g => wpFold Φ x fun a => post (g a) := by + induction f with + | pure g => exact wpFold_map Φ g x post + | lift_bind a r ih => exact congrArg (Φ a) (funext fun b => ih b) + +@[simp] +theorem wpFold_seqLeft (Φ : OpSpec P l) (x : FreeM P α) (y : FreeM P β) (post : α → l) : + wpFold Φ (x <* y) post = wpFold Φ x fun a => wpFold Φ y fun _ => post a := by + rw [seqLeft_eq_bind, wpFold_bind] + simp only [wpFold_bind, wpFold_pure] + +@[simp] +theorem wpFold_seqRight (Φ : OpSpec P l) (x : FreeM P α) (y : FreeM P β) (post : β → l) : + wpFold Φ (x *> y) post = wpFold Φ x fun _ => wpFold Φ y post := by + rw [seqRight_eq_bind, wpFold_bind] + +@[simp] +theorem wpFold_ite (Φ : OpSpec P l) (c : Prop) [Decidable c] (x y : FreeM P α) (post : α → l) : + wpFold Φ (if c then x else y) post = if c then wpFold Φ x post else wpFold Φ y post := by + split <;> rfl + +@[simp] +theorem wpFold_dite (Φ : OpSpec P l) (c : Prop) [Decidable c] (x : c → FreeM P α) + (y : ¬ c → FreeM P α) (post : α → l) : + wpFold Φ (if h : c then x h else y h) post = + if h : c then wpFold Φ (x h) post else wpFold Φ (y h) post := by + split <;> rfl + +@[simp] +theorem wpFold_option_elim {γ : Type uX} (Φ : OpSpec P l) (o : Option γ) (x : FreeM P α) + (f : γ → FreeM P α) (post : α → l) : + wpFold Φ (o.elim x f) post = o.elim (wpFold Φ x post) fun c => wpFold Φ (f c) post := by + cases o <;> rfl + +@[simp] +theorem wpFold_sum_elim {γ : Type uX} {δ : Type uY} (Φ : OpSpec P l) (s : γ ⊕ δ) + (f : γ → FreeM P α) (g : δ → FreeM P α) (post : α → l) : + wpFold Φ (s.elim f g) post = + s.elim (fun c => wpFold Φ (f c) post) fun d => wpFold Φ (g d) post := by + cases s <;> rfl + theorem wpFold_mono [Preorder l] {Φ : OpSpec P l} (hΦ : Φ.Mono) (x : FreeM P α) {post post' : α → l} (h : ∀ a, post a ≤ post' a) : wpFold Φ x post ≤ wpFold Φ x post' := by diff --git a/PolyFunTest/Control/MonadAlgebraRelationalSupport.lean b/PolyFunTest/Control/MonadAlgebraRelationalSupport.lean index d3f55202..a769f202 100644 --- a/PolyFunTest/Control/MonadAlgebraRelationalSupport.lean +++ b/PolyFunTest/Control/MonadAlgebraRelationalSupport.lean @@ -6,6 +6,7 @@ Authors: Quang Dao module public import PolyFun.Control.Monad.Algebra.Relational.Support +public import PolyFun.Control.Monad.Support.Instances /-! # Exact-support relational algebra canaries diff --git a/PolyFunTest/Control/MonadAttach.lean b/PolyFunTest/Control/MonadAttach.lean index c1b54440..3f194e84 100644 --- a/PolyFunTest/Control/MonadAttach.lean +++ b/PolyFunTest/Control/MonadAttach.lean @@ -6,6 +6,7 @@ Authors: Devon Tuma module public import PolyFun.PFunctor.Free.Support +public import PolyFun.Control.Monad.Support.Indexed /-! # Examples for exact monadic support and the always/never judgments diff --git a/PolyFunTest/Control/MonadHomLoops.lean b/PolyFunTest/Control/MonadHomLoops.lean new file mode 100644 index 00000000..927b5f12 --- /dev/null +++ b/PolyFunTest/Control/MonadHomLoops.lean @@ -0,0 +1,45 @@ +/- +Copyright (c) 2026 PolyFun Contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Devon Tuma +-/ + +module + +public import PolyFun.Control.Monad.Hom.Loops +public import PolyFun.Control.Monad.Hom.Writer + +/-! +# Monad morphisms through loops + +`simp` pushes a bundled morphism into the body of every loop combinator, and `grind` closes +goals that need the list forms as rewrite rules. +-/ + +public section + +universe v w + +variable {m : Type → Type v} {n : Type → Type w} [Monad m] [Monad n] + +example (F : m →ᵐ n) (l : List Nat) (init : Nat) (f : Nat → Nat → m (ForInStep Nat)) : + F (forIn l init f) = forIn l init fun a b => F (f a b) := by + simp + +/-- Stated with the class method `forM`, the simp normal form of `List.forM`. -/ +example (F : m →ᵐ n) (l : List Nat) (f : Nat → m PUnit) : + F (forM l f) = forM l fun a => F (f a) := by + grind + +example (F : m →ᵐ n) (l : List Nat) (init : Nat) (f : Nat → Nat → m Nat) : + F (l.foldlM f init) = l.foldlM (fun s a => F (f s a)) init := by + simp + +example [LawfulMonad m] [LawfulMonad n] (F : m →ᵐ n) (l : List Nat) (f : Nat → m Nat) : + F (l.mapM f) = l.mapM fun a => F (f a) := by + simp + +/-- Arrays iterate over their list, so the container lemma applies through `PureForIn`. -/ +example (F : m →ᵐ n) (xs : Array Nat) (init : Nat) (f : Nat → Nat → m (ForInStep Nat)) : + F (forIn xs init f) = forIn xs init fun a b => F (f a b) := by + simp diff --git a/PolyFunTest/Control/SupportStructural.lean b/PolyFunTest/Control/SupportStructural.lean new file mode 100644 index 00000000..a5c86acf --- /dev/null +++ b/PolyFunTest/Control/SupportStructural.lean @@ -0,0 +1,76 @@ +/- +Copyright (c) 2026 PolyFun Contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Devon Tuma +-/ + +module + +public import PolyFun.Control.Monad.Support.Structural +public import PolyFun.Control.Monad.Support.Instances + +/-! +# One-tactic gates for the structural support laws + +Each example is closed by a single call to the automation the corresponding lemma is tagged +for: `simp` for the judgment-level rules and the `CanReturn` rules on `ite` / `dite` / `<*` / +`*>`, `grind` for the `CanReturn` rules on `Option.elim` / `Sum.elim`, which it can index. +-/ + +public section + +open MonadAttach + +universe u v + +variable {m : Type u → Type v} [Monad m] [LawfulMonad m] [MonadAttach m] [ExactMonadAttach m] + +/-- `if` pushes through every judgment. -/ +example (c : Prop) [Decidable c] (x y : Option Nat) (p : Nat → Prop) (hx : AllOutputs p x) + (hy : AllOutputs p y) : AllOutputs p (if c then x else y) := by + simp [hx, hy] + +/-- `if h :` too. -/ +example (c : Prop) [Decidable c] (x : c → Option Nat) (y : ¬ c → Option Nat) (p : Nat → Prop) + (hx : ∀ h, SomeOutput p (x h)) (hy : ∀ h, SomeOutput p (y h)) : + SomeOutput p (if h : c then x h else y h) := by + simp [hx, hy] + +/-- Reachability through `<*` is the conjunction of both sides. -/ +example (x : Option Nat) (y : Option Bool) (a : Nat) (h : CanReturn (x <* y) a) : + CanReturn x a := by + simp only [canReturn_seqLeft_iff] at h + exact h.1 + +/-- `*>` forgets its first operand's value but not its reachability. -/ +example (x : Option Nat) (y : Option Bool) (p : Bool → Prop) (hy : AllOutputs p y) : + AllOutputs p (x *> y) := by + simp [hy] + +/-- Mapping is transparent to the "always" judgment (stated over a generic monad: on `Option`, +`simp` first turns `<$>` into `Option.map`). -/ +example {α β : Type u} (x : m α) (f : α → β) (p : β → Prop) + (h : AllOutputs (fun a => p (f a)) x) : AllOutputs p (f <$> x) := by + simp [h] + +/-- Applicative sequencing nests the judgment. -/ +example {α β : Type u} (f : m (α → β)) (x : m α) (p : β → Prop) + (h : AllOutputs (fun g => AllOutputs (fun a => p (g a)) x) f) : AllOutputs p (f <*> x) := by + simp [h] + +/-- `match` on an option, through `Option.elim`, is indexed by `grind`. -/ +example (o : Option Bool) (x : Option Nat) (f : Bool → Option Nat) (a : Nat) + (hx : o = none → CanReturn x a) (hf : ∀ b, o = some b → CanReturn (f b) a) : + CanReturn (o.elim x f) a := by + grind + +/-- `match` on a sum, through `Sum.elim`, likewise. -/ +example (s : Bool ⊕ Nat) (f : Bool → Option Nat) (g : Nat → Option Nat) (a : Nat) + (hf : ∀ b, s = .inl b → CanReturn (f b) a) (hg : ∀ n, s = .inr n → CanReturn (g n) a) : + CanReturn (s.elim f g) a := by + grind + +/-- The judgment forms of the case splits reduce by `simp` on a concrete scrutinee. -/ +example (x : Option Nat) (f : Bool → Option Nat) (p : Nat → Prop) (h : AllOutputs p (f true)) : + AllOutputs p ((some true).elim x f) := by + simp [h] diff --git a/PolyFunTest/Do/Support.lean b/PolyFunTest/Do/Support.lean index e61d0da4..40e09967 100644 --- a/PolyFunTest/Do/Support.lean +++ b/PolyFunTest/Do/Support.lean @@ -7,6 +7,7 @@ Authors: Devon Tuma module public import PolyFun.Control.Monad.Support.WP +public import PolyFun.Control.Monad.Support.Instances public import Std.Tactic.Do /-! @@ -57,6 +58,27 @@ example : AllOutputs (fun r => r = 2 ∨ r = 3) choose12 := by intro _ simpa only [Lean.Order.ofProp_prop_eq] using choose12_spec.le_wp trivial +/-- A `let mut` accumulator over a `for` loop. -/ +def sumList (xs : List Nat) : SetM Nat := do + let mut s := 0 + for x in xs do + s := s + x + pure s + +/-- `vcgen` reaches the loop through core's `Spec.forIn_list`; the invariant relates the +accumulator to the elements consumed so far. -/ +theorem sumList_spec (xs : List Nat) : ⦃ True ⦄ sumList xs ⦃ fun r => r = xs.sum ⦄ := by + vcgen [sumList] invariants + · fun pref _ s => s = pref.sum + all_goals simp_all + +/-- The loop rule for the "always" judgment, stated without any triple. -/ +example (xs : List Nat) : AllOutputs (fun r => r = xs.sum) (sumList xs) := by + have := toWPMonadDemonic_lawfulWPMonadAttach (m := SetM) + refine allOutputs_of_wp ?_ + intro _ + simpa only [Lean.Order.ofProp_prop_eq] using (sumList_spec xs).le_wp trivial + /-- The demonic interpretation is conjunctive. -/ example (x : SetM Nat) : @WPConjunctive (SetM Nat) Nat Prop EPost.Nil _ _ (instWPMonadSetMDemonic.toWP Nat) x := diff --git a/docs/reading/program-logic-landscape.md b/docs/reading/program-logic-landscape.md index f9aaeba0..4b35fdfc 100644 --- a/docs/reading/program-logic-landscape.md +++ b/docs/reading/program-logic-landscape.md @@ -131,6 +131,13 @@ implemented). ## Open follow-ups +- Relational loop rules: `MAlgRelOrdered` lockstep `forIn` / `forM` / `foldlM` rules under + `StrictBind`, mirroring core's `Spec.forIn'_list` induction; not yet written. +- A `mapM` rule for the judgments (`Hom/Loops.lean` has the morphism form only). +- `try/catch` through core's `ExceptT.instWPMonad` over a PolyFun base: `vcgen` reports + `No spec found for program tryCatch …` although `Spec.tryCatch_ExceptT` exists at the pin; + the instance path needs diagnosing before the canary lands. + - Relational free-monad layer: a two-tree `rwpFold` giving `MAlgRelOrdered (FreeM P) (FreeM Q) l` from a relational op-spec. - `Display`/wp adequacy: `Display.ofPredicates` sections versus `wpFold` of diff --git a/docs/wiki/gotchas.md b/docs/wiki/gotchas.md index 71839584..a411870e 100644 --- a/docs/wiki/gotchas.md +++ b/docs/wiki/gotchas.md @@ -318,6 +318,14 @@ value whose interpretation is a *non-instance* construction (`MAlgOrdered.toWP construction first — `let inst := MAlgOrdered.toWP α` — so it is found as a local instance; `let`, not `have`, so it stays definitionally the term in the statement. +### 11d. `grind =` cannot index `ite`, `dite`, or thunked applicative operands + +`@[grind =]` rejects a lemma whose left-hand side is `f (if c then x else y)` ("invalid +pattern"): `grind` reserves `ite` / `dite` for its own case splitting and will not use them as +pattern heads. Likewise `x <* y` and `x *> y` store `y` under the thunk `fun _ => y`, which a +pattern cannot bind. Such lemmas stay `@[simp]`; `grind` splits the `if` itself and reaches the +applicative forms through `simp`'s normalization to `>>=`. + ### 12. `Std.Do` imports are quarantined Only `PolyFun/Control/Do/Basic.lean`, `PolyFun/PFunctor/Free/Do.lean`, and diff --git a/docs/wiki/program-logic.md b/docs/wiki/program-logic.md index 832e947f..d31cc3ea 100644 --- a/docs/wiki/program-logic.md +++ b/docs/wiki/program-logic.md @@ -13,7 +13,11 @@ migration sketch live in | `PolyFun/Control/Monad/Algebra.lean` | `MAlgOrdered m l`: ordered monad algebras over a complete lattice, with `wp`, `Triple`, the structural rule set, `StateT`/`ReaderT`/`ExceptT`/`OptionT` lifts, and the honest two-postcondition `wpExc`/`wpOpt` | | `PolyFun/Control/Monad/Algebra/Relational.lean` | `MAlgRelOrdered m₁ m₂ l`: relational `rwp`/`RelWP`/`Triple`, asynchronous one-sided bind rules, structural pure rules, explicit named `StateT`/`ReaderT` side lifts, and the `StrictBind` / `Anchored` subclasses (Maillard et al. POPL 2020 shapes) | | `PolyFun/Control/Monad/Algebra/Relational/Support.lean` | Named demonic and angelic exact-support relational algebras; support characterizations; matching `StrictBind` and `Anchored` witnesses | -| `PolyFun/Control/Monad/Support.lean` | `ExactMonadAttach m`: the introduction rules core omits for `MonadAttach.CanReturn`; `MonadAttach.support`; the `AllOutputs`/`SomeOutput`/`NoOutput` judgments and scoped `⊨ₐ`/`⊨ₛ`/`⊭` notation; the named demonic `MAlgOrdered m Prop` choice; instances for `Except`/`SetM` (absent upstream) and the `ExceptT` universe alias | +| `PolyFun/Control/Monad/Support.lean` | `ExactMonadAttach m`: the introduction rules core omits for `MonadAttach.CanReturn`; `MonadAttach.support`; the `AllOutputs`/`SomeOutput`/`NoOutput` judgments and scoped `⊨ₐ`/`⊨ₛ`/`⊭` notation with their `pure`/`bind` laws; the named demonic and angelic `MAlgOrdered m Prop` choices | +| `PolyFun/Control/Monad/Support/Instances.lean` | The `MonadLiftT m SetM` shim, transport along lawful lifts, the `MonadAttach` instances core lacks (`Except`, `SetM`) or leaves inexact (`WriterT`), exactness instances for `Id`/`Option`/`OptionT`/`ExceptT`, per-monad `CanReturn` unfoldings | +| `PolyFun/Control/Monad/Support/Indexed.lean` | Per-run support of `StateT`/`ReaderT` (`supportFrom`, `supportAt`) with exact laws and the indexed judgments `⊨ₐ[s]`/`⊨ₛ[s]`/`⊭[s]` | +| `PolyFun/Control/Monad/Support/Structural.lean` | The rest of the `do` fragment for `CanReturn` and the judgments: `<*`, `*>`, `if`, `if h :`, `Option.elim`, `Sum.elim`, `<$>`, `<*>` | +| `PolyFun/Control/Monad/Support/Loops.lean` | Invariant rules for `forIn'`/`forIn`/`foldlM`/`forM` over lists and `PureForIn` containers, for `AllOutputs` (from core's `Spec.*` under the demonic instance) and `SomeOutput` (angelic) | | `PolyFun/PFunctor/Free/Support.lean` | `MonadAttach`/`ExactMonadAttach` for `FreeM P` with a computable, axiom-free `attach`; structural equations by `rfl`; coherence with `Free/Path.lean` (`support_eq_range_output`) and with the powerset fold (`support_eq_liftM_univ`) | | `PolyFun/PFunctor/Free/WP.lean` | `OpSpec P l` per-operation specs; syntactic `FreeM.wpFold` (with `demonic`/`angelic`); `OpSpec.toMAlgOrdered`; semantic `FreeM.wpVia` through a `Handler`; soundness `wpFold_le_wpVia`/`wpFold_eq_wpVia` | | `PolyFun/Control/Do/Basic.lean` | Legacy core-`Std.Do` transports: `MonadHom.transportSPredWP(Monad)` along a monad morphism, `MonadAttach.toWP(Monad)` demonically at `.pure`, `toWPSound` for core-sense soundness, and `support_subset_of_wpSPred`/`allOutputs_of_wpSPred` turning any `WPSound` triple into a support fact | @@ -22,6 +26,8 @@ migration sketch live in | `PolyFun/Control/Monad/Algebra/WP.lean` | `MAlgOrdered.toWP` / `toWPMonad`: an ordered monad algebra as a core `Std.Internal.Do.WPMonad m l EPost.Nil` (through the `ToCslib.Order.LeanOrder` bridge), `wp` agreement by `rfl`, `toWP_triple_iff`, `wpConjunctiveOf`, and the transfer lemmas `top_eq_top` / `meet_eq_inf` / `join_eq_sup` between core's and Mathlib's lattice operations | | `PolyFun/Control/Monad/Support/WP.lean` | `MonadAttach.toWPMonadDemonic` / `toWPMonadAngelic`: the always/some judgments as `WPMonad m Prop EPost.Nil`; conjunctivity of the demonic reading; the `LawfulWPMonadAttach` mirror of Lean master's soundness class with its demonic instance; `support_subset_of_wp` / `allOutputs_of_wp` | | `PolyFun/Control/Monad/Hom/WP.lean` | `MonadHom.transportWP` / `transportWPMonad` / `transportWPMonadOf`: pulling a core `WPMonad` back along a (bundled or unbundled) monad morphism | +| `PolyFun/Control/Monad/Hom/Loops.lean` | A monad morphism commutes with `forIn'`/`forIn`/`forM`/`foldlM`/`mapM` and with `forIn` over `PureForIn` containers (`@[simp, grind =]`) | +| `PolyFun/Control/Do/Spec.lean` | `@[spec] Spec.forM_list`, the list loop core does not specify, for `vcgen` (tactic tier) | Worked examples: `PolyFunTest/Control/MonadAttach.lean` (judgments, notation, `Iff.rfl` transfer contract) and `PolyFunTest/Do/FreeM.lean` (`mvcgen` smoke @@ -121,6 +127,30 @@ The migration contract for a downstream — what bridges exist, and the two real obstructions — is in [`docs/reading/program-logic-landscape.md`](../reading/program-logic-landscape.md). +## Coverage of the `do` fragment + +What `do`-notation elaborates to, and where each construct has a rule. "free" means the rule is +core's `Spec.*` lemma applied through the `WPMonad` instances of the bridges, with no PolyFun +proof. + +| Construct | core `wp` / `Triple` (`vcgen`) | `AllOutputs` / `SomeOutput` / `support` | `MAlgOrdered.wp` | `MonadHom` | `wpFold` | +|---|---|---|---|---|---| +| `pure`, `>>=`, `<$>`, `<*>` | free | `Support.lean`, `Support/Structural.lean` | `Algebra.lean` | `Hom.lean` | `Free/WP.lean` | +| `<*`, `*>` | free | `Support/Structural.lean` | `Algebra.lean` (`wp_seqLeft`/`wp_seqRight`) | `Hom.lean` | `Free/WP.lean` | +| `if`, `if h :` | `vcgen` splits | `Support/Structural.lean` | `wp_ite`/`wp_dite` | `mmap_ite`/`mmap_dite` | `wpFold_ite`/`wpFold_dite` | +| `match` on `Option`/`Sum` | `vcgen` splits | `*_option_elim`/`*_sum_elim` | `wp_option_elim`/`wp_sum_elim` | `mmap_option_elim`/`mmap_sum_elim` | `wpFold_option_elim`/`wpFold_sum_elim` | +| `for` over `List`/`Array`/ranges/`Option`/`Vector` | free (`Spec.forIn'_list`, `forIn_pure` + `PureForIn`) | `Support/Loops.lean` | via the instance | `Hom/Loops.lean` | via `OpSpec.toWPMonad` (next PR) | +| `forM`, `foldlM` | `Spec.foldlM_list` free, `Spec.forM_list` in `Do/Spec.lean` | `Support/Loops.lean` | via the instance | `Hom/Loops.lean` | — | +| `mapM` | — | — | — | `Hom/Loops.lean` | — | +| early `return`/`break`/`continue` | `Invariant.withEarlyReturnNewDo` (core) | via the instance | — | — | — | +| `throw`/`tryCatch` on `ExceptT`/`OptionT` | core's lifted instances (`Spec.tryCatch_ExceptT`) | via the instance | — | `ExceptT.mapHom`/`OptionT.mapHom` | — | +| `get`/`set`/`read` | core's lifted instances | `Support/Indexed.lean` (`supportFrom`, `supportAt`) | — | `StateT.mapHom`/`ReaderT.mapHom` | — | +| `while`/`repeat` | `ITree` only (`ITree/Do.lean`); no rule on finite `FreeM` | — | — | — | — | + +Open in this table: the relational (`MAlgRelOrdered`) loop rules, a `mapM` judgment rule, and +`try/catch` through the lifted `ExceptT` instance over a PolyFun base, where `vcgen` currently +reports no applicable spec (see the landscape memo's follow-ups). + ## The `Std.Do` quarantine Only `PolyFun/Control/Do/Basic.lean` and `PolyFun/PFunctor/Free/Do.lean` (and diff --git a/docs/wiki/repo-map.md b/docs/wiki/repo-map.md index 140b1e4c..0172d8cd 100644 --- a/docs/wiki/repo-map.md +++ b/docs/wiki/repo-map.md @@ -29,9 +29,11 @@ PolyFun/ Control/ monad/comonad and LTS infrastructure (Coalgebra, Comonad, Lawful, Free, Iter, Bisimulation, LTS/Trace), including the program-logic kernel - (Monad/{Algebra, Support}), its bridges to core's - lattice-generic WP stack (Monad/{Algebra, Support, Hom}/WP) - and the core-Std.Do quarantine root (Do/Basic) + (Monad/{Algebra, Support}, Support/{Instances, Indexed, + Structural, Loops}, Hom/Loops), its bridges to core's + lattice-generic WP stack (Monad/{Algebra, Support, Hom}/WP), + the vcgen spec tier (Do/Spec) and the core-Std.Do + quarantine root (Do/Basic) Logic/ small logic helpers (HEq) ToCslib/ lowest production layer, staging what PolyFun upstreams: