feat(control): cover the whole do fragment in every judgment, with loop rules

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

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

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

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

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

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