From b4f20148448d5ce522e4e8080078b621a53eae3e Mon Sep 17 00:00:00 2001
From: Robert Hawkins <hawkrobe@gmail.com>
Date: Fri, 29 May 2026 17:21:18 -0700
Subject: [PATCH] =?UTF-8?q?refactor(Semantics):=20build=20I=E2=82=9A=20and?=
 =?UTF-8?q?=20PostSupp=20on=20mathlib=20LawfulMonad?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 Linglib/Semantics/Composition/MaybeMonad.lean | 71 +++++--------------
 .../Semantics/Dynamic/Connectives/Defs.lean   | 14 ++++
 .../Semantics/Dynamic/Core/DynamicTy2.lean    |  2 +-
 .../Charlow2021/PostSuppositional.lean        | 52 +++++++-------
 Linglib/Studies/Grove2022.lean                |  2 +-
 5 files changed, 60 insertions(+), 81 deletions(-)

diff --git a/Linglib/Semantics/Composition/MaybeMonad.lean b/Linglib/Semantics/Composition/MaybeMonad.lean
index 9c5c69322..7e6934a52 100644
--- a/Linglib/Semantics/Composition/MaybeMonad.lean
+++ b/Linglib/Semantics/Composition/MaybeMonad.lean
@@ -149,23 +149,16 @@ standard intensional types (`i → t` becomes `i → t_#`). -/
 
 section IMonad
 
-variable {I : Type}
-
-/-- `Iₚ I α`: the intensional-presuppositional monad.
-
-    An expression of type `Iₚ I α` reads an index `i` and returns
-    `some v` if defined at `i`, or `none` if presupposition failure
-    occurs at `i`. -/
-abbrev Iₚ (I : Type) (α : Type) := I → Option α
-
-/-- `ηI`: unit for `Iₚ`. Makes a value trivially index-sensitive
-    (ignores the index, always defined). Grove eq. 19, first line. -/
-def ηI {α : Type} (v : α) : Iₚ I α := λ _ => some v
+/-- `Iₚ I α = I → Option α`: the Reader monad transformer over the Maybe
+    monad. An expression of type `Iₚ I α` reads an index `i` (world,
+    world-assignment pair, etc.) and returns `some v` if defined at `i`,
+    or `none` on presupposition failure — Grove §4.1's uniform treatment
+    of intensionality and presupposition (replacing `t` with `t_#` in the
+    intensional type `i → t`).
 
-/-- `bindI`: bind for `Iₚ`. Evaluates `m` at index `i`; if defined,
-    feeds the result to `k` at the same index. Grove eq. 19, second line. -/
-def bindI {α β : Type} (m : Iₚ I α) (k : α → Iₚ I β) : Iₚ I β :=
-  λ i => m i >>= (λ v => k v i)
+    Defining `Iₚ` as `ReaderT I Option` makes `pure`/`>>=` Grove's
+    `η_#`/`⋆_#` and inherits `Monad`/`LawfulMonad` from mathlib. -/
+abbrev Iₚ (I : Type) := ReaderT I Option
 
 end IMonad
 
@@ -175,45 +168,13 @@ end IMonad
 
 /-! ### §3 Monad laws
 
-The three laws from Figure 7 hold for `Iₚ`. Left Identity and
-Associativity are the key properties for scope-taking: Left Identity
-ensures that `η` + `⋆` = reconstruction (no scope), and Associativity
-ensures that cyclic scope-taking (roll-up pied-piping) works. -/
-
-section MonadLaws
-
-variable {I α β γ : Type}
-
-/-- **Left Identity**: lifting a value into the monad and immediately
-    binding is the same as applying the continuation directly.
-
-    This is why global scope for a presupposition trigger that has been
-    locally `η`-shifted reconstructs to the local meaning (Grove fn. 13). -/
-theorem left_identity (v : α) (k : α → Iₚ I β) :
-    bindI (ηI v) k = k v := rfl
-
-/-- **Right Identity**: binding with `ηI` is a no-op. -/
-theorem right_identity (m : Iₚ I α) : bindI m ηI = m := by
-  funext i; simp [bindI, ηI]
-
-/-- **Associativity**: sequential scope-taking = direct wide scope.
-
-    This is the presuppositional analog of @cite{charlow-2020}'s
-    ASSOCIATIVITY theorem for the set monad. It guarantees that
-    roll-up pied-piping (taking scope at an island edge, then further)
-    yields the same result as direct scope-taking. -/
-theorem assoc (m : Iₚ I α) (f : α → Iₚ I β) (g : β → Iₚ I γ) :
-    bindI (bindI m f) g = bindI m (λ x => bindI (f x) g) := by
-  funext i; simp [bindI]; cases m i <;> rfl
-
-/-- **Backward compatibility**: non-presuppositional expressions (those
-    wrapped in `some`) compose the same way they do without the monad.
-    This means traditional satisfaction-theoretic analyses that use only
-    defined values are preserved inside the monadic setting (Grove §5). -/
-theorem backward_compat (f : α → β) (v : α) :
-    bindI (ηI v) (λ x => ηI (f x)) = (ηI (f v) : Iₚ I β) := rfl
-
-end MonadLaws
+`Iₚ = ReaderT I Option` is a `LawfulMonad`, so the three laws of Grove's
+Figure 7 hold via `pure_bind`, `bind_pure`, and `bind_assoc` rather than
+standalone `rfl` theorems. Left Identity and Associativity are the
+scope-taking properties: Left Identity gives reconstruction (`η` + `⋆` =
+no scope; Grove fn. 13), and Associativity makes cyclic scope-taking
+(roll-up pied-piping) sound (the presuppositional analog of
+@cite{charlow-2020}'s ASSOCIATIVITY theorem for the set monad). -/
 
 -- ════════════════════════════════════════════════════════════════
 -- §4 Semantic Operations
diff --git a/Linglib/Semantics/Dynamic/Connectives/Defs.lean b/Linglib/Semantics/Dynamic/Connectives/Defs.lean
index 5469867cc..59caf8632 100644
--- a/Linglib/Semantics/Dynamic/Connectives/Defs.lean
+++ b/Linglib/Semantics/Dynamic/Connectives/Defs.lean
@@ -216,6 +216,20 @@ theorem test_dseq (C : Condition S) (D : DRS S) (hC : ∀ i, C i) :
   · intro hD
     exact ⟨i, ⟨rfl, hC i⟩, hD⟩
 
+/-- Test is right identity for sequencing (when condition holds everywhere).
+Together with `test_dseq` and `dseq_assoc`, this makes `(DRS S, ⨟, test ⊤)`
+a monoid. -/
+theorem dseq_test (D : DRS S) (C : Condition S) (hC : ∀ i, C i) :
+    D ⨟ test C = D := by
+  funext i j
+  simp only [dseq, test, eq_iff_iff]
+  constructor
+  · intro ⟨h, hD, hhj, _⟩
+    subst hhj
+    exact hD
+  · intro hD
+    exact ⟨j, hD, rfl, hC j⟩
+
 /-- Double negation for tests. -/
 theorem dneg_dneg_test (C : Condition S) :
     dneg (test (dneg (test C))) = C := by
diff --git a/Linglib/Semantics/Dynamic/Core/DynamicTy2.lean b/Linglib/Semantics/Dynamic/Core/DynamicTy2.lean
index 2fc38959e..15e88f584 100644
--- a/Linglib/Semantics/Dynamic/Core/DynamicTy2.lean
+++ b/Linglib/Semantics/Dynamic/Core/DynamicTy2.lean
@@ -42,7 +42,7 @@ namespace Semantics.Dynamic.Core
 export DynProp (DRS Condition
   dseq test dneg dimpl ddisj closure
   trueAt valid entails
-  dseq_assoc test_dseq dneg_dneg_test closure_closure dseq_closure)
+  dseq_assoc test_dseq dseq_test dneg_dneg_test closure_closure dseq_closure)
 
 /-!
 Dynamic Ty2 is parameterized by:
diff --git a/Linglib/Studies/Charlow2021/PostSuppositional.lean b/Linglib/Studies/Charlow2021/PostSuppositional.lean
index 674f16547..cc006dbf9 100644
--- a/Linglib/Studies/Charlow2021/PostSuppositional.lean
+++ b/Linglib/Studies/Charlow2021/PostSuppositional.lean
@@ -31,20 +31,14 @@ structure PostSupp (S : Type*) (A : Type*) where
   /-- Accumulated post-suppositional content -/
   postsup : DRS S
 
-/-- Pure: trivial post-supposition (equation 120).
-    The post-suppositional DRS is the identity (test True). -/
-def PostSupp.pure {S A : Type*} (a : A) : PostSupp S A :=
-  ⟨a, test (λ _ => True)⟩
-
-/-- Bind: sequence post-suppositions via dseq (equation 121).
-    Post-suppositional content accumulates via dynamic conjunction. -/
-def PostSupp.bind {S A B : Type*} (m : PostSupp S A) (f : A → PostSupp S B) : PostSupp S B :=
-  let result := f m.val
-  ⟨result.val, dseq m.postsup result.postsup⟩
-
-/-- Map: apply a function to the at-issue value, preserving post-suppositions. -/
-def PostSupp.map {S A B : Type*} (f : A → B) (m : PostSupp S A) : PostSupp S B :=
-  ⟨f m.val, m.postsup⟩
+/-- `PostSupp S` is the Writer monad over the monoid `(DRS S, ⨟, test ⊤)`
+    (@cite{charlow-2021} equations 120–121): `pure` carries the trivial
+    post-supposition (the `True`-test identity) and `bind` sequences
+    post-suppositional content via dynamic conjunction (`dseq`). Independent
+    composition of post-suppositions is what yields cumulative readings. -/
+instance : Monad (PostSupp S) where
+  pure a := ⟨a, test (λ _ => True)⟩
+  bind m f := ⟨(f m.val).val, dseq m.postsup (f m.val).postsup⟩
 
 /-- Reify (bullet operator, equation 58): conjoin value and post-supposition.
     For a `PostSupp S (DRS S)`, this produces a single DRS by sequencing
@@ -72,20 +66,30 @@ def exactlyN_postsup {S E : Type*} [AssignmentStructure S E] [PartialOrder E] [F
 -- § Monad Laws
 -- ════════════════════════════════════════════════════
 
-/-- Left identity for PostSupp bind. -/
-theorem PostSupp.bind_left_id {S A B : Type*} (a : A) (f : A → PostSupp S B) :
-    PostSupp.bind (PostSupp.pure a) f = f a := by
-  simp only [PostSupp.bind, PostSupp.pure]
-  -- dseq (test fun _ => True) (f a).postsup = (f a).postsup
-  -- because ∃ h, (i = h ∧ True) ∧ D h j  ↔  D i j
-  have : dseq (test λ _ => True) (f a).postsup = (f a).postsup := by
-    funext i j; simp [dseq, test]
-  simp [this]
+/-- The monad laws are exactly the monoid laws of `(DRS S, ⨟, test ⊤)`
+    (`test_dseq`, `dseq_test`, `dseq_assoc`), so we register `PostSupp S`
+    as a lawful monad rather than re-proving them standalone. -/
+instance : LawfulMonad (PostSupp S) := LawfulMonad.mk' (PostSupp S)
+  (id_map := by
+    rintro α ⟨a, d⟩
+    show (⟨a, dseq d (test (λ _ => True))⟩ : PostSupp S α) = ⟨a, d⟩
+    rw [dseq_test d (λ _ => True) (λ _ => trivial)])
+  (pure_bind := by
+    intro α β x f
+    show (⟨(f x).val, dseq (test (λ _ => True)) (f x).postsup⟩ : PostSupp S β) = f x
+    rw [test_dseq (λ _ => True) (f x).postsup (λ _ => trivial)])
+  (bind_assoc := by
+    intro α β γ x f g
+    show (⟨(g (f x.val).val).val,
+          dseq (dseq x.postsup (f x.val).postsup) (g (f x.val).val).postsup⟩ : PostSupp S γ)
+       = ⟨(g (f x.val).val).val,
+          dseq x.postsup (dseq (f x.val).postsup (g (f x.val).val).postsup)⟩
+    rw [dseq_assoc])
 
 /-- Reify of a pure post-supposition recovers the original DRS
     (modulo the trivial True test). -/
 theorem PostSupp.reify_pure {S : Type*} (D : DRS S) :
-    PostSupp.reify (PostSupp.pure D) = dseq D (test (λ _ => True)) := by
+    PostSupp.reify (pure D) = dseq D (test (λ _ => True)) := by
   rfl
 
 /-- Post-suppositional combination yields cumulative readings.
diff --git a/Linglib/Studies/Grove2022.lean b/Linglib/Studies/Grove2022.lean
index da8ad2e72..da53bb7a8 100644
--- a/Linglib/Studies/Grove2022.lean
+++ b/Linglib/Studies/Grove2022.lean
@@ -280,7 +280,7 @@ theorem believe_local_always_defined (w : AttWorld) :
 def believeGlobal : Iₚ AttWorld Bool :=
   λ i => lostWetsuit i >>= (λ b =>
     believe (λ _ => believesRBool) [AttWorld.actual, AttWorld.believed]
-      (ηI b) () i)
+      (pure b) () i)
 
 /-- Global reading at `actual`: complement is undefined → `none`.