From 2295c8a90d642954e950d88202188bcc5b523afc Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Fri, 7 Aug 2026 12:56:15 -0700 Subject: [PATCH 01/15] =?UTF-8?q?refactor(Semantics/Dynamic/DRS):=20Realiz?= =?UTF-8?q?e=20=E2=86=92=20Verifies,=20embedding-first?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Linglib/Semantics/Dynamic/DRS/Basic.lean | 2 +- Linglib/Semantics/Dynamic/DRS/Dynamics.lean | 57 +++--- Linglib/Semantics/Dynamic/DRS/Reduction.lean | 24 +-- .../Semantics/Dynamic/DRS/Verification.lean | 179 +++++++++--------- Linglib/Studies/KampReyle1993.lean | 2 +- 5 files changed, 136 insertions(+), 128 deletions(-) diff --git a/Linglib/Semantics/Dynamic/DRS/Basic.lean b/Linglib/Semantics/Dynamic/DRS/Basic.lean index 697517d35f..7ff15d43fb 100644 --- a/Linglib/Semantics/Dynamic/DRS/Basic.lean +++ b/Linglib/Semantics/Dynamic/DRS/Basic.lean @@ -9,7 +9,7 @@ Structural operations and lemmas over the faithful `DRS` core (`DRS/Defs.lean`): * `DRS.map` / `Condition.map` — functorial renaming of discourse referents along `f : V → W`. When `f` is a bijection this is [kamp-reyle-1993]'s *alphabetic variant* (the prose preceding Def. 1.4.8); `map_id` makes "renaming to the - identity is the identity" a free corollary, and `DRS.realize_map` + identity is the identity" a free corollary, and `DRS.verifies_map` (`DRS/Verification.lean`) shows variants have the same semantics. * `merge` algebra — identity (`empty`) and associativity. * `DRS.Extends` — K&R's extension relation `f [K] g` between embeddings. diff --git a/Linglib/Semantics/Dynamic/DRS/Dynamics.lean b/Linglib/Semantics/Dynamic/DRS/Dynamics.lean index f604679b1d..c98a47f2a6 100644 --- a/Linglib/Semantics/Dynamic/DRS/Dynamics.lean +++ b/Linglib/Semantics/Dynamic/DRS/Dynamics.lean @@ -9,7 +9,7 @@ import Linglib.Semantics.Dynamic.Update boxes denote *binary relations* between embeddings (SEM3, input → output, the format of [groenendijk-stokhof-1991]); a box is true under an input embedding `a` iff some output `a'` is related to it (p. 148). This is the dynamic / CCP -face of DRT, dual to the static verifying-embedding semantics `DRS.Realize` — +face of DRT, dual to the static verifying-embedding semantics `DRS.Verifies` — the total-assignment rendering of [kamp-reyle-1993]'s verification (see the deviation note in `DRS/Verification.lean`). @@ -19,19 +19,19 @@ verifying-embedding one (his fn. 4 scopes the remark: both sides here are the total-assignment variant). The equivalence is a theorem, not a definitional identification: -* `DRS.toRel_iff_realize` — the relation `toRel K a a'` holds iff `a'` extends `a` +* `DRS.toRel_iff_verifies` — the relation `toRel K a a'` holds iff `a'` extends `a` over `K`'s universe and verifies `K` (the keystone bridge). * `DRS.trueRel_iff_realize_toFormula` — the dynamic truth of a DRS equals its first-order translation's `Realize`, closing the triangle with `Reduction` - (`Realize` — `toFormula` — `toRel`, each pair related by a proven theorem). + (`Verifies` — `toFormula` — `toRel`, each pair related by a proven theorem). ## Main declarations * `DRS.toRel` / `Condition.holds` — the relational (SEM3) and set (SEM1/2) denotations. * `DRS.trueRel` — relational truth: some output embedding is related to the input. -* `DRS.toRel_iff_realize` / `Condition.holds_iff_realize` — equivalence with the - static `DRS.Realize` semantics. +* `DRS.toRel_iff_verifies` / `Condition.holds_iff_verifies` — equivalence with the + static `DRS.Verifies` semantics. * `DRS.trueRel_congr` — the coincidence lemma: denotation depends only on the occurring referents (`DRS.occ`, from `DRS/Basic.lean`). * `DRS.toRel_merge` — the Merging Lemma: under freshness, `merge` denotes the @@ -41,7 +41,8 @@ identification: Naming: the dynamic face (`toRel`, `holds`, `trueRel`) follows the spine's lowerCamel operation names (`neg`, `seq`, `closure`); the static face -(`DRS.Realize`, `DRS/Verification.lean`) follows mathlib's `Formula.Realize`. +(`DRS.Verifies`, `DRS/Verification.lean`) uses the field's own verb, and the +first-order reduction (`DRS/Reduction.lean`) speaks mathlib's `Formula.Realize`. -/ open FirstOrder FirstOrder.Language @@ -122,39 +123,39 @@ mutual agrees with the static verifying-embedding semantics — `toRel K a a'` holds iff the output `a'` extends the input `a` over `K`'s universe and verifies `K`. (Both sides are the total-assignment variant; see `DRS/Verification.lean`.) -/ -theorem DRS.toRel_iff_realize (K : DRS L V) (a a' : V → M) : - DRS.toRel K a a' ↔ K.Extends a a' ∧ K.Realize a' := by +theorem DRS.toRel_iff_verifies (K : DRS L V) (a a' : V → M) : + DRS.toRel K a a' ↔ K.Extends a a' ∧ DRS.Verifies a' K := by match K with | .mk U conds => - simp only [DRS.toRel, DRS.referents_mk, DRS.realize_mk, DRS.Extends] - exact and_congr_right (fun _ => Condition.holdsAll_iff_realizeAll conds a') -/-- A condition's set denotation agrees with its static `Realize`. -/ -theorem Condition.holds_iff_realize (c : Condition L V) (a : V → M) : - c.holds a ↔ c.Realize a := by + simp only [DRS.toRel, DRS.referents_mk, DRS.verifies_mk, DRS.Extends] + exact and_congr_right (fun _ => Condition.holdsAll_iff_verifies conds a') +/-- A condition's set denotation agrees with its static `Verifies`. -/ +theorem Condition.holds_iff_verifies (c : Condition L V) (a : V → M) : + c.holds a ↔ Condition.Verifies a c := by match c with - | .rel R args => simp only [Condition.holds_rel, Condition.realize_rel] - | .eq u v => simp only [Condition.holds_eq, Condition.realize_eq] + | .rel R args => simp only [Condition.holds_rel, Condition.verifies_rel] + | .eq u v => simp only [Condition.holds_eq, Condition.verifies_eq] | .neg K => - simp only [Condition.holds_neg, Condition.realize_neg] - exact not_congr (exists_congr (fun a' => DRS.toRel_iff_realize K a a')) + simp only [Condition.holds_neg, Condition.verifies_neg] + exact not_congr (exists_congr (fun a' => DRS.toRel_iff_verifies K a a')) | .imp ante cons => - simp only [Condition.holds_imp, Condition.realize_imp] + simp only [Condition.holds_imp, Condition.verifies_imp] refine forall_congr' (fun a' => ?_) - rw [DRS.toRel_iff_realize ante a a', and_imp] + rw [DRS.toRel_iff_verifies ante a a', and_imp] refine imp_congr_right (fun _ => imp_congr_right (fun _ => ?_)) - exact exists_congr (fun a'' => DRS.toRel_iff_realize cons a' a'') + exact exists_congr (fun a'' => DRS.toRel_iff_verifies cons a' a'') | .dis l r => - simp only [Condition.holds_dis, Condition.realize_dis, exists_or] - exact or_congr (exists_congr (fun a' => DRS.toRel_iff_realize l a a')) - (exists_congr (fun a' => DRS.toRel_iff_realize r a a')) -/-- The list analogue of `Condition.holds_iff_realize`. -/ -theorem Condition.holdsAll_iff_realizeAll (cs : List (Condition L V)) (a : V → M) : - Condition.holdsAll cs a ↔ ∀ c ∈ cs, c.Realize a := by + simp only [Condition.holds_dis, Condition.verifies_dis, exists_or] + exact or_congr (exists_congr (fun a' => DRS.toRel_iff_verifies l a a')) + (exists_congr (fun a' => DRS.toRel_iff_verifies r a a')) +/-- The list analogue of `Condition.holds_iff_verifies`. -/ +theorem Condition.holdsAll_iff_verifies (cs : List (Condition L V)) (a : V → M) : + Condition.holdsAll cs a ↔ ∀ c ∈ cs, Condition.Verifies a c := by match cs with | [] => simp | c :: cs => simp only [Condition.holdsAll_cons, List.forall_mem_cons] - exact and_congr (Condition.holds_iff_realize c a) (Condition.holdsAll_iff_realizeAll cs a) + exact and_congr (Condition.holds_iff_verifies c a) (Condition.holdsAll_iff_verifies cs a) end /-- The dynamic truth of a DRS equals its first-order translation's `Realize` @@ -162,7 +163,7 @@ end theorem DRS.trueRel_iff_realize_toFormula [DecidableEq V] (K : DRS L V) (a : V → M) : DRS.trueRel K a ↔ (K.toFormula).Realize a := by rw [DRS.trueRel_iff, DRS.realize_toFormula K a] - exact exists_congr (fun a' => DRS.toRel_iff_realize K a a') + exact exists_congr (fun a' => DRS.toRel_iff_verifies K a a') /-! ### The coincidence lemma -/ diff --git a/Linglib/Semantics/Dynamic/DRS/Reduction.lean b/Linglib/Semantics/Dynamic/DRS/Reduction.lean index a2c77d0657..8bcab996d9 100644 --- a/Linglib/Semantics/Dynamic/DRS/Reduction.lean +++ b/Linglib/Semantics/Dynamic/DRS/Reduction.lean @@ -7,7 +7,7 @@ import Mathlib.ModelTheory.Semantics The bespoke DRS box language is *equivalent to ordinary first-order logic*. We translate each DRS into a mathlib `FirstOrder.Language.Formula` and prove its `Realize` coincides with the -bespoke `DRS.Realize` — [kamp-reyle-1993]'s §1.5 ("From DRT to Predicate +bespoke `DRS.Verifies` — [kamp-reyle-1993]'s §1.5 ("From DRT to Predicate Logic") and [muskens-1996]'s "DRSs are already present in classical logic", now a Lean theorem (`DRS.realize_toFormula`) rather than an assertion. @@ -142,47 +142,47 @@ theorem realize_closeForall [DecidableEq V] (U : Finset V) (φ : L.Formula V) (v mutual /-- **DRT ⊆ FOL** (§1.5): the -translated formula's `Realize` coincides with the bespoke `DRS.Realize`. As +translated formula's `Realize` coincides with the bespoke `DRS.Verifies`. As `toFormula` existentially closes the universe, the correspondence is with an embedding `v'` extending `v` over `K.referents`. -/ theorem DRS.realize_toFormula [DecidableEq V] (K : DRS L V) (v : V → M) : - (K.toFormula).Realize v ↔ ∃ v', K.Extends v v' ∧ K.Realize v' := by + (K.toFormula).Realize v ↔ ∃ v', K.Extends v v' ∧ DRS.Verifies v' K := by match K with | .mk U conds => rw [DRS.toFormula, realize_closeExists] - simp only [DRS.referents_mk, DRS.realize_mk, DRS.Extends] + simp only [DRS.referents_mk, DRS.verifies_mk, DRS.Extends] exact exists_congr fun v' => and_congr_right fun _ => Condition.realize_toFormulaAll conds v' /-- The open body of a DRS (its conditions, no universe closure) realizes as -`DRS.Realize` (used for the antecedent of `⇒`). -/ +`DRS.Verifies` (used for the antecedent of `⇒`). -/ theorem DRS.realize_bodyFormula [DecidableEq V] (K : DRS L V) (v : V → M) : - (DRS.bodyFormula K).Realize v ↔ K.Realize v := by + (DRS.bodyFormula K).Realize v ↔ DRS.Verifies v K := by match K with | .mk _ conds => exact Condition.realize_toFormulaAll conds v -/-- A single condition's translation realizes as `Condition.Realize`. -/ +/-- A single condition's translation realizes as `Condition.Verifies`. -/ theorem Condition.realize_toFormula [DecidableEq V] (c : Condition L V) (v : V → M) : - (Condition.toFormula c).Realize v ↔ c.Realize v := by + (Condition.toFormula c).Realize v ↔ Condition.Verifies v c := by match c with | .rel R args => simp [Condition.toFormula, Relations.formula, Formula.Realize, BoundedFormula.realize_rel, Term.realize_var] | .eq a b => simp [Condition.toFormula, Formula.realize_equal] | .neg K => - simp only [Condition.toFormula, Condition.realize_neg, Formula.realize_not] + simp only [Condition.toFormula, Condition.verifies_neg, Formula.realize_not] rw [DRS.realize_toFormula K v] | .imp a c => - simp only [Condition.toFormula, Condition.realize_imp] + simp only [Condition.toFormula, Condition.verifies_imp] rw [realize_closeForall] simp only [Formula.realize_imp] refine forall_congr' (fun v' => imp_congr_right (fun _ => ?_)) rw [DRS.realize_bodyFormula a v', DRS.realize_toFormula c v'] | .dis l r => - simp only [Condition.toFormula, Condition.realize_dis, Formula.realize_sup] + simp only [Condition.toFormula, Condition.verifies_dis, Formula.realize_sup] rw [DRS.realize_toFormula l v, DRS.realize_toFormula r v] /-- A list of conditions' conjoined translation realizes as the conjunction of their realizations. -/ theorem Condition.realize_toFormulaAll [DecidableEq V] (cs : List (Condition L V)) (v : V → M) : - (Condition.toFormulaAll cs).Realize v ↔ ∀ c ∈ cs, c.Realize v := by + (Condition.toFormulaAll cs).Realize v ↔ ∀ c ∈ cs, Condition.Verifies v c := by match cs with | [] => simp [Condition.toFormulaAll, Formula.realize_top] | c :: cs => diff --git a/Linglib/Semantics/Dynamic/DRS/Verification.lean b/Linglib/Semantics/Dynamic/DRS/Verification.lean index 34a07b5433..a488dff38b 100644 --- a/Linglib/Semantics/Dynamic/DRS/Verification.lean +++ b/Linglib/Semantics/Dynamic/DRS/Verification.lean @@ -6,16 +6,16 @@ import Linglib.Semantics.Dynamic.DRS.Basic DRS verification via *embeddings* into a mathlib `FirstOrder.Language.Structure` — [kamp-reyle-1993]'s Def. 1.4.4 in the *total-assignment* rendering. An embedding is an assignment `f : V → M` of discourse referents to the model -domain; `DRS.Extends K f g` is K&R's extension relation `f [K] g` — the -output `g` differs from `f` at most on `K`'s universe — and a sub-DRS is -entered by existentially (re)assigning along it. For `imp`, the consequent -witness extends the *antecedent* embedding, not the host one — antecedent -referents stay visible in the consequent, the `⇒` accessibility asymmetry. -The atomic and `¬` clauses are Def. 1.4.4(ii); the `⇒`/`∨` clauses are the -Chapter 2 conditional and disjunction semantics. Truth (Def. 1.4.5) is the -existential closure of verification over the outer universe; it is delivered -downstream as `DRS.trueRel` (`DRS/Dynamics.lean`) and as the first-order -translation's realization (`DRS/Reduction.lean`). +domain; `DRS.Extends K f g` is K&R's extension relation `f [K] g` +(`DRS/Basic.lean`), and a sub-DRS is entered by existentially (re)assigning +along it. For `imp`, the consequent witness extends the *antecedent* +embedding, not the host one — antecedent referents stay visible in the +consequent, the `⇒` accessibility asymmetry. The atomic and `¬` clauses are +Def. 1.4.4(ii); the `⇒`/`∨` clauses are the Chapter 2 conditional and +disjunction semantics. Truth (Def. 1.4.5) is the existential closure of +verification over the outer universe; it is delivered downstream as +`DRS.trueRel` (`DRS/Dynamics.lean`) and as the first-order translation's +realization (`DRS/Reduction.lean`). **Deviation** ([muskens-1996], fn. 4): K&R's embeddings are *partial* functions that sub-DRSs strictly *extend*, so a re-declared referent keeps its value; here @@ -26,21 +26,23 @@ says "every man is mortal" for K&R, "if there is a man there is a mortal" here. ## Main declarations -* `DRS.Realize` / `Condition.Realize` — the verifying-embedding relation. A DRS - is verified when every condition is (`∀ c ∈ K.conditions`, the `Theory.Model` - idiom), so there is no mutual recursion and no list helper. -* `DRS.realize_perm` — verification reads the condition list as a set, cashing +* `DRS.Verifies` / `Condition.Verifies` — `Verifies f K` is the field's + "`f` verifies `K`": every condition of `K` holds under `f` + (`∀ c ∈ K.conditions`, the `Theory.Model` idiom — no mutual recursion, no + list helper). +* `DRS.verifies_perm` — verification reads the condition list as a set, cashing the `List`-representation note in `DRS/Defs.lean`. -* `DRS.realize_map` — renaming along a bijection transports verification: +* `DRS.verifies_map` — renaming along a bijection transports verification: alphabetic variants (Def. 1.4.8, via `DRS.map` in `DRS/Basic.lean`) have the same semantics. ## Implementation notes -`Condition.Realize` recurses into sub-DRSs through the nested +`Condition.Verifies` recurses into sub-DRSs through the nested `List (Condition L V)` by well-founded recursion on `sizeOf`, so its clause -characterizations (`realize_neg`, …) are equation-lemma rewrites rather than -`Iff.rfl`. +characterizations (`verifies_neg`, …) are equation-lemma rewrites rather than +`Iff.rfl`; they restate the clauses with `DRS.Verifies`, as the textbook +states them. -/ open FirstOrder FirstOrder.Language @@ -51,64 +53,66 @@ universe u v w x variable {L : Language.{u, v}} {V : Type w} {M : Type x} [L.Structure M] -/-- `c.Realize f`: the embedding `f` *verifies* the condition `c` +/-- `Condition.Verifies f c`: the embedding `f` *verifies* the condition `c` (Def. 1.4.4(ii)); a sub-DRS is entered by existentially (re)assigning along its extension relation and verifying each of its conditions. -/ -def Condition.Realize : Condition L V → (V → M) → Prop - | .rel R args, f => Structure.RelMap R (fun i => f (args i)) - | .eq a b, f => f a = f b - | .neg K, f => ¬ ∃ g, K.Extends f g ∧ ∀ c ∈ K.conditions, c.Realize g - | .imp a c, f => - ∀ g, a.Extends f g → (∀ d ∈ a.conditions, d.Realize g) → - ∃ h, c.Extends g h ∧ ∀ d ∈ c.conditions, d.Realize h - | .dis l r, f => - (∃ g, l.Extends f g ∧ ∀ c ∈ l.conditions, c.Realize g) ∨ - (∃ g, r.Extends f g ∧ ∀ c ∈ r.conditions, c.Realize g) +def Condition.Verifies : (V → M) → Condition L V → Prop + | f, .rel R args => Structure.RelMap R (fun i => f (args i)) + | f, .eq a b => f a = f b + | f, .neg K => ¬ ∃ g, K.Extends f g ∧ ∀ c ∈ K.conditions, Condition.Verifies g c + | f, .imp a c => + ∀ g, a.Extends f g → (∀ d ∈ a.conditions, Condition.Verifies g d) → + ∃ h, c.Extends g h ∧ ∀ d ∈ c.conditions, Condition.Verifies h d + | f, .dis l r => + (∃ g, l.Extends f g ∧ ∀ c ∈ l.conditions, Condition.Verifies g c) ∨ + (∃ g, r.Extends f g ∧ ∀ c ∈ r.conditions, Condition.Verifies g c) +termination_by f c => sizeOf c decreasing_by all_goals have := DRS.sizeOf_lt_of_mem_conditions (by assumption) simp_wf omega -/-- `K.Realize f`: the embedding `f` *verifies* `K` — every condition of `K` -holds under `f` (Def. 1.4.4). -/ -def DRS.Realize (K : DRS L V) (f : V → M) : Prop := ∀ c ∈ K.conditions, c.Realize f +/-- `DRS.Verifies f K`: the embedding `f` *verifies* `K` — `f` verifies every +condition of `K` (Def. 1.4.4). -/ +def DRS.Verifies (f : V → M) (K : DRS L V) : Prop := + ∀ c ∈ K.conditions, Condition.Verifies f c /-! ### Structural simp API -/ variable {f : V → M} -@[simp] theorem DRS.realize_mk (U : Finset V) (conds : List (Condition L V)) : - (DRS.mk U conds).Realize f ↔ ∀ c ∈ conds, c.Realize f := Iff.rfl +@[simp] theorem DRS.verifies_mk (U : Finset V) (conds : List (Condition L V)) : + DRS.Verifies f (.mk U conds) ↔ ∀ c ∈ conds, Condition.Verifies f c := Iff.rfl -@[simp] theorem Condition.realize_rel {n : ℕ} (R : L.Relations n) (args : Fin n → V) : - (Condition.rel R args).Realize f ↔ Structure.RelMap R (fun i => f (args i)) := by - simp only [Condition.Realize] +@[simp] theorem Condition.verifies_rel {n : ℕ} (R : L.Relations n) (args : Fin n → V) : + Condition.Verifies f (.rel R args) ↔ Structure.RelMap R (fun i => f (args i)) := by + simp only [Condition.Verifies] -@[simp] theorem Condition.realize_eq (a b : V) : - (Condition.eq a b : Condition L V).Realize f ↔ f a = f b := by - simp only [Condition.Realize] +@[simp] theorem Condition.verifies_eq (a b : V) : + Condition.Verifies f (.eq a b : Condition L V) ↔ f a = f b := by + simp only [Condition.Verifies] -@[simp] theorem Condition.realize_neg (K : DRS L V) : - (Condition.neg K).Realize f ↔ ¬ ∃ g, K.Extends f g ∧ K.Realize g := by - simp only [Condition.Realize, DRS.Realize] +@[simp] theorem Condition.verifies_neg (K : DRS L V) : + Condition.Verifies f (.neg K) ↔ ¬ ∃ g, K.Extends f g ∧ DRS.Verifies g K := by + simp only [Condition.Verifies, DRS.Verifies] -@[simp] theorem Condition.realize_imp (a c : DRS L V) : - (Condition.imp a c).Realize f ↔ - ∀ g, a.Extends f g → a.Realize g → - ∃ h, c.Extends g h ∧ c.Realize h := by - simp only [Condition.Realize, DRS.Realize] +@[simp] theorem Condition.verifies_imp (a c : DRS L V) : + Condition.Verifies f (.imp a c) ↔ + ∀ g, a.Extends f g → DRS.Verifies g a → + ∃ h, c.Extends g h ∧ DRS.Verifies h c := by + simp only [Condition.Verifies, DRS.Verifies] -@[simp] theorem Condition.realize_dis (l r : DRS L V) : - (Condition.dis l r).Realize f ↔ - (∃ g, l.Extends f g ∧ l.Realize g) ∨ - (∃ g, r.Extends f g ∧ r.Realize g) := by - simp only [Condition.Realize, DRS.Realize] +@[simp] theorem Condition.verifies_dis (l r : DRS L V) : + Condition.Verifies f (.dis l r) ↔ + (∃ g, l.Extends f g ∧ DRS.Verifies g l) ∨ + (∃ g, r.Extends f g ∧ DRS.Verifies g r) := by + simp only [Condition.Verifies, DRS.Verifies] /-- Verification is invariant under permutation of the conditions — the set semantics the `List`-valued `conditions` field promises (`DRS/Defs.lean`). -/ -theorem DRS.realize_perm {U : Finset V} {cs ds : List (Condition L V)} (h : cs.Perm ds) : - (DRS.mk U cs).Realize f ↔ (DRS.mk U ds).Realize f := by - simp only [DRS.realize_mk, h.mem_iff] +theorem DRS.verifies_perm {U : Finset V} {cs ds : List (Condition L V)} (h : cs.Perm ds) : + DRS.Verifies f (.mk U cs) ↔ DRS.Verifies f (.mk U ds) := by + simp only [DRS.verifies_mk, h.mem_iff] /-! ### Alphabetic variants -/ @@ -146,50 +150,53 @@ private theorem forall_precomp_extend_iff (e : V ≃ W) (U : Finset V) (f : W · intro H g h exact H (g ∘ e) fun x hx => h (e x) (by simpa using hx) -/-- A renamed DRS is verified iff the original is under the precomposed -embedding, given the transport for each of its conditions. -/ -private theorem realize_map_all (e : V ≃ W) (K : DRS L V) (g : W → M) - (ih : ∀ c ∈ K.conditions, ∀ u : W → M, (c.map e).Realize u ↔ c.Realize (u ∘ e)) : - (K.map e).Realize g ↔ K.Realize (g ∘ e) := by - simp only [DRS.Realize, DRS.conditions_map, Condition.mapList_eq_map, List.forall_mem_map] +/-- An embedding verifies a renamed DRS iff its precomposition verifies the +original, given the transport for each of the DRS's conditions. -/ +private theorem verifies_map_all (e : V ≃ W) (K : DRS L V) (g : W → M) + (ih : ∀ c ∈ K.conditions, ∀ u : W → M, + Condition.Verifies u (c.map e) ↔ Condition.Verifies (u ∘ e) c) : + DRS.Verifies g (K.map e) ↔ DRS.Verifies (g ∘ e) K := by + simp only [DRS.Verifies, DRS.conditions_map, Condition.mapList_eq_map, List.forall_mem_map] exact forall_congr' fun c => imp_congr_right fun hc => ih c hc g /-- Renaming along a bijection transports verification (the condition form of -`DRS.realize_map`). -/ -theorem Condition.realize_map (e : V ≃ W) : ∀ (c : Condition L V) (f : W → M), - (c.map e).Realize f ↔ c.Realize (f ∘ e) - | .rel R args, f => by +`DRS.verifies_map`). -/ +theorem Condition.verifies_map (e : V ≃ W) : ∀ (f : W → M) (c : Condition L V), + Condition.Verifies f (c.map e) ↔ Condition.Verifies (f ∘ e) c + | f, .rel R args => by simp [Condition.map, Function.comp] - | .eq a b, f => by + | f, .eq a b => by simp [Condition.map, Function.comp] - | .neg K, f => by + | f, .neg K => by have hK := fun g : W → M => - realize_map_all e K g (fun d hd u => Condition.realize_map e d u) - simp only [Condition.map, Condition.realize_neg, DRS.Extends, DRS.referents_map] + verifies_map_all e K g (fun d hd u => Condition.verifies_map e u d) + simp only [Condition.map, Condition.verifies_neg, DRS.Extends, DRS.referents_map] exact not_congr ((exists_congr fun g => and_congr_right fun _ => hK g).trans - (exists_precomp_extend_iff e K.referents f K.Realize)) - | .imp a c, f => by + (exists_precomp_extend_iff e K.referents f (DRS.Verifies · K))) + | f, .imp a c => by have hA := fun g : W → M => - realize_map_all e a g (fun d hd u => Condition.realize_map e d u) + verifies_map_all e a g (fun d hd u => Condition.verifies_map e u d) have hC := fun g : W → M => - realize_map_all e c g (fun d hd u => Condition.realize_map e d u) - simp only [Condition.map, Condition.realize_imp, DRS.Extends, DRS.referents_map] + verifies_map_all e c g (fun d hd u => Condition.verifies_map e u d) + simp only [Condition.map, Condition.verifies_imp, DRS.Extends, DRS.referents_map] refine Iff.trans (forall_congr' fun g => imp_congr_right fun _ => imp_congr (hA g) ((exists_congr fun h => and_congr_right fun _ => hC h).trans - (exists_precomp_extend_iff e c.referents g c.Realize))) ?_ + (exists_precomp_extend_iff e c.referents g (DRS.Verifies · c)))) ?_ exact forall_precomp_extend_iff e a.referents f - (fun u => a.Realize u → ∃ w'', (∀ x ∉ c.referents, w'' x = u x) ∧ c.Realize w'') - | .dis l r, f => by + (fun u => DRS.Verifies u a → + ∃ w'', (∀ x ∉ c.referents, w'' x = u x) ∧ DRS.Verifies w'' c) + | f, .dis l r => by have hL := fun g : W → M => - realize_map_all e l g (fun d hd u => Condition.realize_map e d u) + verifies_map_all e l g (fun d hd u => Condition.verifies_map e u d) have hR := fun g : W → M => - realize_map_all e r g (fun d hd u => Condition.realize_map e d u) - simp only [Condition.map, Condition.realize_dis, DRS.Extends, DRS.referents_map] + verifies_map_all e r g (fun d hd u => Condition.verifies_map e u d) + simp only [Condition.map, Condition.verifies_dis, DRS.Extends, DRS.referents_map] exact or_congr ((exists_congr fun g => and_congr_right fun _ => hL g).trans - (exists_precomp_extend_iff e l.referents f l.Realize)) + (exists_precomp_extend_iff e l.referents f (DRS.Verifies · l))) ((exists_congr fun g => and_congr_right fun _ => hR g).trans - (exists_precomp_extend_iff e r.referents f r.Realize)) + (exists_precomp_extend_iff e r.referents f (DRS.Verifies · r))) +termination_by f c => sizeOf c decreasing_by all_goals have := DRS.sizeOf_lt_of_mem_conditions (by assumption) simp_wf @@ -197,9 +204,9 @@ decreasing_by all_goals /-- Renaming along a bijection transports verification: `f` verifies `K.map e` iff `f ∘ e` verifies `K` — alphabetic variants have the same semantics. -/ -theorem DRS.realize_map (e : V ≃ W) (K : DRS L V) (f : W → M) : - (K.map e).Realize f ↔ K.Realize (f ∘ e) := - realize_map_all e K f (fun c _ u => Condition.realize_map e c u) +theorem DRS.verifies_map (e : V ≃ W) (f : W → M) (K : DRS L V) : + DRS.Verifies f (K.map e) ↔ DRS.Verifies (f ∘ e) K := + verifies_map_all e K f (fun c _ u => Condition.verifies_map e u c) end Map diff --git a/Linglib/Studies/KampReyle1993.lean b/Linglib/Studies/KampReyle1993.lean index 52e1c43e67..bfd4dfdd3c 100644 --- a/Linglib/Studies/KampReyle1993.lean +++ b/Linglib/Studies/KampReyle1993.lean @@ -7,7 +7,7 @@ import Mathlib.Data.Fin.VecNotation K&R's worked examples, evaluated through the faithful model-theoretic DRS core (`Semantics/Dynamic/DRS/`). Each truth-condition is a theorem about the substrate -denotation `DRS.trueRel` (Muskens's relational truth, equivalently `DRS.Realize`), +denotation `DRS.trueRel` (Muskens's relational truth, equivalently `DRS.Verifies`), not a local re-implementation. ## Examples From b82ef09875258a3ec02b9ec032719445b792646d Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Fri, 7 Aug 2026 13:05:57 -0700 Subject: [PATCH 02/15] refactor(Semantics/Dynamic/DRS): Embedding abbrev, bare Verifies via export --- Linglib/Semantics/Dynamic/DRS/Basic.lean | 14 +- Linglib/Semantics/Dynamic/DRS/Dynamics.lean | 18 +-- Linglib/Semantics/Dynamic/DRS/Reduction.lean | 16 +-- .../Semantics/Dynamic/DRS/Verification.lean | 123 +++++++++--------- 4 files changed, 91 insertions(+), 80 deletions(-) diff --git a/Linglib/Semantics/Dynamic/DRS/Basic.lean b/Linglib/Semantics/Dynamic/DRS/Basic.lean index 7ff15d43fb..a08f69d15d 100644 --- a/Linglib/Semantics/Dynamic/DRS/Basic.lean +++ b/Linglib/Semantics/Dynamic/DRS/Basic.lean @@ -9,10 +9,11 @@ Structural operations and lemmas over the faithful `DRS` core (`DRS/Defs.lean`): * `DRS.map` / `Condition.map` — functorial renaming of discourse referents along `f : V → W`. When `f` is a bijection this is [kamp-reyle-1993]'s *alphabetic variant* (the prose preceding Def. 1.4.8); `map_id` makes "renaming to the - identity is the identity" a free corollary, and `DRS.verifies_map` + identity is the identity" a free corollary, and `verifies_map` (`DRS/Verification.lean`) shows variants have the same semantics. * `merge` algebra — identity (`empty`) and associativity. -* `DRS.Extends` — K&R's extension relation `f [K] g` between embeddings. +* `Embedding` and `DRS.Extends` — embedding functions and K&R's extension + relation `f [K] g` between them. * `DRS.fv` / `DRS.IsProper` — free discourse referents (as a `Finset`) and properness (`fv K = ∅`, Def. 1.4.2–1.4.3). * `Condition.occ` / `DRS.occ` — occurring referents, as a decidable `Finset`. @@ -109,13 +110,18 @@ theorem merge_assoc (K₁ K₂ K₃ : DRS L V) : end DRS -/-! ### The extension relation -/ +/-! ### Embeddings and the extension relation -/ + +/-- An *embedding function*: an assignment of discourse referents to +individuals in a model — in the total-assignment rendering (deviation note in +`DRS/Verification.lean`). -/ +abbrev Embedding (V : Type w) (M : Type*) := V → M variable {M : Type*} in /-- `K.Extends f g` (K&R's `f [K] g`): the output embedding `g` differs from the input `f` at most on `K`'s universe — the total-assignment rendering of "`f ⊆ g` and `Dom g = Dom f ∪ U_K`". -/ -def DRS.Extends (K : DRS L V) (f g : V → M) : Prop := ∀ x ∉ K.referents, g x = f x +def DRS.Extends (K : DRS L V) (f g : Embedding V M) : Prop := ∀ x ∉ K.referents, g x = f x /-! ### Occurring referents -/ diff --git a/Linglib/Semantics/Dynamic/DRS/Dynamics.lean b/Linglib/Semantics/Dynamic/DRS/Dynamics.lean index c98a47f2a6..28203b36bb 100644 --- a/Linglib/Semantics/Dynamic/DRS/Dynamics.lean +++ b/Linglib/Semantics/Dynamic/DRS/Dynamics.lean @@ -124,33 +124,33 @@ agrees with the static verifying-embedding semantics — `toRel K a a'` holds if the output `a'` extends the input `a` over `K`'s universe and verifies `K`. (Both sides are the total-assignment variant; see `DRS/Verification.lean`.) -/ theorem DRS.toRel_iff_verifies (K : DRS L V) (a a' : V → M) : - DRS.toRel K a a' ↔ K.Extends a a' ∧ DRS.Verifies a' K := by + DRS.toRel K a a' ↔ K.Extends a a' ∧ Verifies a' K := by match K with | .mk U conds => - simp only [DRS.toRel, DRS.referents_mk, DRS.verifies_mk, DRS.Extends] + simp only [DRS.toRel, DRS.referents_mk, verifies_mk, DRS.Extends] exact and_congr_right (fun _ => Condition.holdsAll_iff_verifies conds a') /-- A condition's set denotation agrees with its static `Verifies`. -/ theorem Condition.holds_iff_verifies (c : Condition L V) (a : V → M) : - c.holds a ↔ Condition.Verifies a c := by + c.holds a ↔ Verifies a c := by match c with - | .rel R args => simp only [Condition.holds_rel, Condition.verifies_rel] - | .eq u v => simp only [Condition.holds_eq, Condition.verifies_eq] + | .rel R args => simp only [Condition.holds_rel, verifies_rel] + | .eq u v => simp only [Condition.holds_eq, verifies_eq] | .neg K => - simp only [Condition.holds_neg, Condition.verifies_neg] + simp only [Condition.holds_neg, verifies_neg] exact not_congr (exists_congr (fun a' => DRS.toRel_iff_verifies K a a')) | .imp ante cons => - simp only [Condition.holds_imp, Condition.verifies_imp] + simp only [Condition.holds_imp, verifies_imp] refine forall_congr' (fun a' => ?_) rw [DRS.toRel_iff_verifies ante a a', and_imp] refine imp_congr_right (fun _ => imp_congr_right (fun _ => ?_)) exact exists_congr (fun a'' => DRS.toRel_iff_verifies cons a' a'') | .dis l r => - simp only [Condition.holds_dis, Condition.verifies_dis, exists_or] + simp only [Condition.holds_dis, verifies_dis, exists_or] exact or_congr (exists_congr (fun a' => DRS.toRel_iff_verifies l a a')) (exists_congr (fun a' => DRS.toRel_iff_verifies r a a')) /-- The list analogue of `Condition.holds_iff_verifies`. -/ theorem Condition.holdsAll_iff_verifies (cs : List (Condition L V)) (a : V → M) : - Condition.holdsAll cs a ↔ ∀ c ∈ cs, Condition.Verifies a c := by + Condition.holdsAll cs a ↔ ∀ c ∈ cs, Verifies a c := by match cs with | [] => simp | c :: cs => diff --git a/Linglib/Semantics/Dynamic/DRS/Reduction.lean b/Linglib/Semantics/Dynamic/DRS/Reduction.lean index 8bcab996d9..8064a02fef 100644 --- a/Linglib/Semantics/Dynamic/DRS/Reduction.lean +++ b/Linglib/Semantics/Dynamic/DRS/Reduction.lean @@ -146,43 +146,43 @@ translated formula's `Realize` coincides with the bespoke `DRS.Verifies`. As `toFormula` existentially closes the universe, the correspondence is with an embedding `v'` extending `v` over `K.referents`. -/ theorem DRS.realize_toFormula [DecidableEq V] (K : DRS L V) (v : V → M) : - (K.toFormula).Realize v ↔ ∃ v', K.Extends v v' ∧ DRS.Verifies v' K := by + (K.toFormula).Realize v ↔ ∃ v', K.Extends v v' ∧ Verifies v' K := by match K with | .mk U conds => rw [DRS.toFormula, realize_closeExists] - simp only [DRS.referents_mk, DRS.verifies_mk, DRS.Extends] + simp only [DRS.referents_mk, verifies_mk, DRS.Extends] exact exists_congr fun v' => and_congr_right fun _ => Condition.realize_toFormulaAll conds v' /-- The open body of a DRS (its conditions, no universe closure) realizes as `DRS.Verifies` (used for the antecedent of `⇒`). -/ theorem DRS.realize_bodyFormula [DecidableEq V] (K : DRS L V) (v : V → M) : - (DRS.bodyFormula K).Realize v ↔ DRS.Verifies v K := by + (DRS.bodyFormula K).Realize v ↔ Verifies v K := by match K with | .mk _ conds => exact Condition.realize_toFormulaAll conds v /-- A single condition's translation realizes as `Condition.Verifies`. -/ theorem Condition.realize_toFormula [DecidableEq V] (c : Condition L V) (v : V → M) : - (Condition.toFormula c).Realize v ↔ Condition.Verifies v c := by + (Condition.toFormula c).Realize v ↔ Verifies v c := by match c with | .rel R args => simp [Condition.toFormula, Relations.formula, Formula.Realize, BoundedFormula.realize_rel, Term.realize_var] | .eq a b => simp [Condition.toFormula, Formula.realize_equal] | .neg K => - simp only [Condition.toFormula, Condition.verifies_neg, Formula.realize_not] + simp only [Condition.toFormula, verifies_neg, Formula.realize_not] rw [DRS.realize_toFormula K v] | .imp a c => - simp only [Condition.toFormula, Condition.verifies_imp] + simp only [Condition.toFormula, verifies_imp] rw [realize_closeForall] simp only [Formula.realize_imp] refine forall_congr' (fun v' => imp_congr_right (fun _ => ?_)) rw [DRS.realize_bodyFormula a v', DRS.realize_toFormula c v'] | .dis l r => - simp only [Condition.toFormula, Condition.verifies_dis, Formula.realize_sup] + simp only [Condition.toFormula, verifies_dis, Formula.realize_sup] rw [DRS.realize_toFormula l v, DRS.realize_toFormula r v] /-- A list of conditions' conjoined translation realizes as the conjunction of their realizations. -/ theorem Condition.realize_toFormulaAll [DecidableEq V] (cs : List (Condition L V)) (v : V → M) : - (Condition.toFormulaAll cs).Realize v ↔ ∀ c ∈ cs, Condition.Verifies v c := by + (Condition.toFormulaAll cs).Realize v ↔ ∀ c ∈ cs, Verifies v c := by match cs with | [] => simp [Condition.toFormulaAll, Formula.realize_top] | c :: cs => diff --git a/Linglib/Semantics/Dynamic/DRS/Verification.lean b/Linglib/Semantics/Dynamic/DRS/Verification.lean index a488dff38b..810a3b6df3 100644 --- a/Linglib/Semantics/Dynamic/DRS/Verification.lean +++ b/Linglib/Semantics/Dynamic/DRS/Verification.lean @@ -3,12 +3,13 @@ import Linglib.Semantics.Dynamic.DRS.Basic /-! # Verifying embeddings for DRSs -DRS verification via *embeddings* into a mathlib `FirstOrder.Language.Structure` -— [kamp-reyle-1993]'s Def. 1.4.4 in the *total-assignment* rendering. An -embedding is an assignment `f : V → M` of discourse referents to the model -domain; `DRS.Extends K f g` is K&R's extension relation `f [K] g` -(`DRS/Basic.lean`), and a sub-DRS is entered by existentially (re)assigning -along it. For `imp`, the consequent witness extends the *antecedent* +[kamp-reyle-1993]'s Def. 1.4.4 in the *total-assignment* rendering, over a +mathlib `FirstOrder.Language.Structure`. An *embedding function* +`f : Embedding V M` assigns discourse referents to individuals in the model; +`DRS.Extends K f g` is K&R's extension relation `f [K] g` (both in +`DRS/Basic.lean`); and `Verifies f K` says the embedding `f` *verifies* the +DRS `K`. A sub-DRS is entered by existentially (re)assigning along its +extension relation. For `imp`, the consequent witness extends the *antecedent* embedding, not the host one — antecedent referents stay visible in the consequent, the `⇒` accessibility asymmetry. The atomic and `¬` clauses are Def. 1.4.4(ii); the `⇒`/`∨` clauses are the Chapter 2 conditional and @@ -30,9 +31,9 @@ says "every man is mortal" for K&R, "if there is a man there is a mortal" here. "`f` verifies `K`": every condition of `K` holds under `f` (`∀ c ∈ K.conditions`, the `Theory.Model` idiom — no mutual recursion, no list helper). -* `DRS.verifies_perm` — verification reads the condition list as a set, cashing +* `verifies_perm` — verification reads the condition list as a set, cashing the `List`-representation note in `DRS/Defs.lean`. -* `DRS.verifies_map` — renaming along a bijection transports verification: +* `verifies_map` — renaming along a bijection transports verification: alphabetic variants (Def. 1.4.8, via `DRS.map` in `DRS/Basic.lean`) have the same semantics. @@ -41,7 +42,7 @@ says "every man is mortal" for K&R, "if there is a man there is a mortal" here. `Condition.Verifies` recurses into sub-DRSs through the nested `List (Condition L V)` by well-founded recursion on `sizeOf`, so its clause characterizations (`verifies_neg`, …) are equation-lemma rewrites rather than -`Iff.rfl`; they restate the clauses with `DRS.Verifies`, as the textbook +`Iff.rfl`; they restate the clauses with `Verifies` of the sub-DRS, as the textbook states them. -/ @@ -56,7 +57,7 @@ variable {L : Language.{u, v}} {V : Type w} {M : Type x} [L.Structure M] /-- `Condition.Verifies f c`: the embedding `f` *verifies* the condition `c` (Def. 1.4.4(ii)); a sub-DRS is entered by existentially (re)assigning along its extension relation and verifying each of its conditions. -/ -def Condition.Verifies : (V → M) → Condition L V → Prop +def Condition.Verifies : Embedding V M → Condition L V → Prop | f, .rel R args => Structure.RelMap R (fun i => f (args i)) | f, .eq a b => f a = f b | f, .neg K => ¬ ∃ g, K.Extends f g ∧ ∀ c ∈ K.conditions, Condition.Verifies g c @@ -66,53 +67,57 @@ def Condition.Verifies : (V → M) → Condition L V → Prop | f, .dis l r => (∃ g, l.Extends f g ∧ ∀ c ∈ l.conditions, Condition.Verifies g c) ∨ (∃ g, r.Extends f g ∧ ∀ c ∈ r.conditions, Condition.Verifies g c) -termination_by f c => sizeOf c +termination_by _ c => sizeOf c decreasing_by all_goals have := DRS.sizeOf_lt_of_mem_conditions (by assumption) simp_wf omega -/-- `DRS.Verifies f K`: the embedding `f` *verifies* `K` — `f` verifies every +export Condition (Verifies) + +/-- `Verifies f K`: the embedding `f` *verifies* `K` — `f` verifies every condition of `K` (Def. 1.4.4). -/ -def DRS.Verifies (f : V → M) (K : DRS L V) : Prop := +def DRS.Verifies (f : Embedding V M) (K : DRS L V) : Prop := ∀ c ∈ K.conditions, Condition.Verifies f c +export DRS (Verifies) + /-! ### Structural simp API -/ -variable {f : V → M} +variable {f : Embedding V M} -@[simp] theorem DRS.verifies_mk (U : Finset V) (conds : List (Condition L V)) : - DRS.Verifies f (.mk U conds) ↔ ∀ c ∈ conds, Condition.Verifies f c := Iff.rfl +@[simp] theorem verifies_mk (U : Finset V) (conds : List (Condition L V)) : + Verifies f (.mk U conds) ↔ ∀ c ∈ conds, Verifies f c := Iff.rfl -@[simp] theorem Condition.verifies_rel {n : ℕ} (R : L.Relations n) (args : Fin n → V) : - Condition.Verifies f (.rel R args) ↔ Structure.RelMap R (fun i => f (args i)) := by +@[simp] theorem verifies_rel {n : ℕ} (R : L.Relations n) (args : Fin n → V) : + Verifies f (.rel R args) ↔ Structure.RelMap R (fun i => f (args i)) := by simp only [Condition.Verifies] -@[simp] theorem Condition.verifies_eq (a b : V) : - Condition.Verifies f (.eq a b : Condition L V) ↔ f a = f b := by +@[simp] theorem verifies_eq (a b : V) : + Verifies f (.eq a b : Condition L V) ↔ f a = f b := by simp only [Condition.Verifies] -@[simp] theorem Condition.verifies_neg (K : DRS L V) : - Condition.Verifies f (.neg K) ↔ ¬ ∃ g, K.Extends f g ∧ DRS.Verifies g K := by +@[simp] theorem verifies_neg (K : DRS L V) : + Verifies f (.neg K) ↔ ¬ ∃ g, K.Extends f g ∧ Verifies g K := by simp only [Condition.Verifies, DRS.Verifies] -@[simp] theorem Condition.verifies_imp (a c : DRS L V) : - Condition.Verifies f (.imp a c) ↔ - ∀ g, a.Extends f g → DRS.Verifies g a → - ∃ h, c.Extends g h ∧ DRS.Verifies h c := by +@[simp] theorem verifies_imp (a c : DRS L V) : + Verifies f (.imp a c) ↔ + ∀ g, a.Extends f g → Verifies g a → + ∃ h, c.Extends g h ∧ Verifies h c := by simp only [Condition.Verifies, DRS.Verifies] -@[simp] theorem Condition.verifies_dis (l r : DRS L V) : - Condition.Verifies f (.dis l r) ↔ - (∃ g, l.Extends f g ∧ DRS.Verifies g l) ∨ - (∃ g, r.Extends f g ∧ DRS.Verifies g r) := by +@[simp] theorem verifies_dis (l r : DRS L V) : + Verifies f (.dis l r) ↔ + (∃ g, l.Extends f g ∧ Verifies g l) ∨ + (∃ g, r.Extends f g ∧ Verifies g r) := by simp only [Condition.Verifies, DRS.Verifies] /-- Verification is invariant under permutation of the conditions — the set semantics the `List`-valued `conditions` field promises (`DRS/Defs.lean`). -/ -theorem DRS.verifies_perm {U : Finset V} {cs ds : List (Condition L V)} (h : cs.Perm ds) : - DRS.Verifies f (.mk U cs) ↔ DRS.Verifies f (.mk U ds) := by - simp only [DRS.verifies_mk, h.mem_iff] +theorem verifies_perm {U : Finset V} {cs ds : List (Condition L V)} (h : cs.Perm ds) : + Verifies f (.mk U cs) ↔ Verifies f (.mk U ds) := by + simp only [verifies_mk, h.mem_iff] /-! ### Alphabetic variants -/ @@ -122,10 +127,10 @@ variable {W : Type*} [DecidableEq W] /-- Precomposition with `e` is a bijection between the embeddings extending `f` on `U.image e` and those extending `f ∘ e` on `U`. -/ -private theorem exists_precomp_extend_iff (e : V ≃ W) (U : Finset V) (f : W → M) - (P : (V → M) → Prop) : - (∃ g : W → M, (∀ y ∉ U.image e, g y = f y) ∧ P (g ∘ e)) ↔ - ∃ w' : V → M, (∀ x ∉ U, w' x = f (e x)) ∧ P w' := by +private theorem exists_precomp_extend_iff (e : V ≃ W) (U : Finset V) (f : Embedding W M) + (P : (Embedding V M) → Prop) : + (∃ g : Embedding W M, (∀ y ∉ U.image e, g y = f y) ∧ P (g ∘ e)) ↔ + ∃ w' : Embedding V M, (∀ x ∉ U, w' x = f (e x)) ∧ P w' := by constructor · rintro ⟨g, h, hp⟩ exact ⟨g ∘ e, fun x hx => h (e x) (by simpa using hx), hp⟩ @@ -137,10 +142,10 @@ private theorem exists_precomp_extend_iff (e : V ≃ W) (U : Finset V) (f : W exact key.symm ▸ hp /-- The `∀` analogue of `exists_precomp_extend_iff`. -/ -private theorem forall_precomp_extend_iff (e : V ≃ W) (U : Finset V) (f : W → M) - (P : (V → M) → Prop) : - (∀ g : W → M, (∀ y ∉ U.image e, g y = f y) → P (g ∘ e)) ↔ - ∀ w' : V → M, (∀ x ∉ U, w' x = f (e x)) → P w' := by +private theorem forall_precomp_extend_iff (e : V ≃ W) (U : Finset V) (f : Embedding W M) + (P : (Embedding V M) → Prop) : + (∀ g : Embedding W M, (∀ y ∉ U.image e, g y = f y) → P (g ∘ e)) ↔ + ∀ w' : Embedding V M, (∀ x ∉ U, w' x = f (e x)) → P w' := by constructor · intro H w' h have key : (w' ∘ e.symm) ∘ e = w' := by funext x; simp @@ -152,33 +157,33 @@ private theorem forall_precomp_extend_iff (e : V ≃ W) (U : Finset V) (f : W /-- An embedding verifies a renamed DRS iff its precomposition verifies the original, given the transport for each of the DRS's conditions. -/ -private theorem verifies_map_all (e : V ≃ W) (K : DRS L V) (g : W → M) - (ih : ∀ c ∈ K.conditions, ∀ u : W → M, - Condition.Verifies u (c.map e) ↔ Condition.Verifies (u ∘ e) c) : - DRS.Verifies g (K.map e) ↔ DRS.Verifies (g ∘ e) K := by +private theorem verifies_map_all (e : V ≃ W) (K : DRS L V) (g : Embedding W M) + (ih : ∀ c ∈ K.conditions, ∀ u : Embedding W M, + Verifies u (c.map e) ↔ Verifies (u ∘ e) c) : + Verifies g (K.map e) ↔ Verifies (g ∘ e) K := by simp only [DRS.Verifies, DRS.conditions_map, Condition.mapList_eq_map, List.forall_mem_map] exact forall_congr' fun c => imp_congr_right fun hc => ih c hc g /-- Renaming along a bijection transports verification (the condition form of -`DRS.verifies_map`). -/ -theorem Condition.verifies_map (e : V ≃ W) : ∀ (f : W → M) (c : Condition L V), - Condition.Verifies f (c.map e) ↔ Condition.Verifies (f ∘ e) c +`verifies_map`). -/ +theorem Condition.verifies_map (e : V ≃ W) : ∀ (f : Embedding W M) (c : Condition L V), + Verifies f (c.map e) ↔ Verifies (f ∘ e) c | f, .rel R args => by simp [Condition.map, Function.comp] | f, .eq a b => by simp [Condition.map, Function.comp] | f, .neg K => by - have hK := fun g : W → M => + have hK := fun g : Embedding W M => verifies_map_all e K g (fun d hd u => Condition.verifies_map e u d) - simp only [Condition.map, Condition.verifies_neg, DRS.Extends, DRS.referents_map] + simp only [Condition.map, verifies_neg, DRS.Extends, DRS.referents_map] exact not_congr ((exists_congr fun g => and_congr_right fun _ => hK g).trans (exists_precomp_extend_iff e K.referents f (DRS.Verifies · K))) | f, .imp a c => by - have hA := fun g : W → M => + have hA := fun g : Embedding W M => verifies_map_all e a g (fun d hd u => Condition.verifies_map e u d) - have hC := fun g : W → M => + have hC := fun g : Embedding W M => verifies_map_all e c g (fun d hd u => Condition.verifies_map e u d) - simp only [Condition.map, Condition.verifies_imp, DRS.Extends, DRS.referents_map] + simp only [Condition.map, verifies_imp, DRS.Extends, DRS.referents_map] refine Iff.trans (forall_congr' fun g => imp_congr_right fun _ => imp_congr (hA g) ((exists_congr fun h => and_congr_right fun _ => hC h).trans (exists_precomp_extend_iff e c.referents g (DRS.Verifies · c)))) ?_ @@ -186,17 +191,17 @@ theorem Condition.verifies_map (e : V ≃ W) : ∀ (f : W → M) (c : Condition (fun u => DRS.Verifies u a → ∃ w'', (∀ x ∉ c.referents, w'' x = u x) ∧ DRS.Verifies w'' c) | f, .dis l r => by - have hL := fun g : W → M => + have hL := fun g : Embedding W M => verifies_map_all e l g (fun d hd u => Condition.verifies_map e u d) - have hR := fun g : W → M => + have hR := fun g : Embedding W M => verifies_map_all e r g (fun d hd u => Condition.verifies_map e u d) - simp only [Condition.map, Condition.verifies_dis, DRS.Extends, DRS.referents_map] + simp only [Condition.map, verifies_dis, DRS.Extends, DRS.referents_map] exact or_congr ((exists_congr fun g => and_congr_right fun _ => hL g).trans (exists_precomp_extend_iff e l.referents f (DRS.Verifies · l))) ((exists_congr fun g => and_congr_right fun _ => hR g).trans (exists_precomp_extend_iff e r.referents f (DRS.Verifies · r))) -termination_by f c => sizeOf c +termination_by _ c => sizeOf c decreasing_by all_goals have := DRS.sizeOf_lt_of_mem_conditions (by assumption) simp_wf @@ -204,8 +209,8 @@ decreasing_by all_goals /-- Renaming along a bijection transports verification: `f` verifies `K.map e` iff `f ∘ e` verifies `K` — alphabetic variants have the same semantics. -/ -theorem DRS.verifies_map (e : V ≃ W) (f : W → M) (K : DRS L V) : - DRS.Verifies f (K.map e) ↔ DRS.Verifies (f ∘ e) K := +theorem verifies_map (e : V ≃ W) (f : Embedding W M) (K : DRS L V) : + Verifies f (K.map e) ↔ Verifies (f ∘ e) K := verifies_map_all e K f (fun c _ u => Condition.verifies_map e u c) end Map From 81ede3f2c966ac971a63a929cb47b0787c3158b0 Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Fri, 7 Aug 2026 13:15:56 -0700 Subject: [PATCH 03/15] refactor(Semantics/Dynamic/DRS): Verifies owned by Embedding, class dispatch --- Linglib/Semantics/Dynamic/DRS/Basic.lean | 2 +- Linglib/Semantics/Dynamic/DRS/Dynamics.lean | 12 +- Linglib/Semantics/Dynamic/DRS/Reduction.lean | 8 +- .../Semantics/Dynamic/DRS/Verification.lean | 149 ++++++++++-------- Linglib/Studies/KampReyle1993.lean | 2 +- 5 files changed, 97 insertions(+), 76 deletions(-) diff --git a/Linglib/Semantics/Dynamic/DRS/Basic.lean b/Linglib/Semantics/Dynamic/DRS/Basic.lean index a08f69d15d..d5b016a8cb 100644 --- a/Linglib/Semantics/Dynamic/DRS/Basic.lean +++ b/Linglib/Semantics/Dynamic/DRS/Basic.lean @@ -9,7 +9,7 @@ Structural operations and lemmas over the faithful `DRS` core (`DRS/Defs.lean`): * `DRS.map` / `Condition.map` — functorial renaming of discourse referents along `f : V → W`. When `f` is a bijection this is [kamp-reyle-1993]'s *alphabetic variant* (the prose preceding Def. 1.4.8); `map_id` makes "renaming to the - identity is the identity" a free corollary, and `verifies_map` + identity is the identity" a free corollary, and `Embedding.verifies_map` (`DRS/Verification.lean`) shows variants have the same semantics. * `merge` algebra — identity (`empty`) and associativity. * `Embedding` and `DRS.Extends` — embedding functions and K&R's extension diff --git a/Linglib/Semantics/Dynamic/DRS/Dynamics.lean b/Linglib/Semantics/Dynamic/DRS/Dynamics.lean index 28203b36bb..d4a4571ee7 100644 --- a/Linglib/Semantics/Dynamic/DRS/Dynamics.lean +++ b/Linglib/Semantics/Dynamic/DRS/Dynamics.lean @@ -127,25 +127,25 @@ theorem DRS.toRel_iff_verifies (K : DRS L V) (a a' : V → M) : DRS.toRel K a a' ↔ K.Extends a a' ∧ Verifies a' K := by match K with | .mk U conds => - simp only [DRS.toRel, DRS.referents_mk, verifies_mk, DRS.Extends] + simp only [DRS.toRel, DRS.referents_mk, Embedding.verifies_mk, DRS.Extends] exact and_congr_right (fun _ => Condition.holdsAll_iff_verifies conds a') /-- A condition's set denotation agrees with its static `Verifies`. -/ theorem Condition.holds_iff_verifies (c : Condition L V) (a : V → M) : c.holds a ↔ Verifies a c := by match c with - | .rel R args => simp only [Condition.holds_rel, verifies_rel] - | .eq u v => simp only [Condition.holds_eq, verifies_eq] + | .rel R args => simp only [Condition.holds_rel, Embedding.verifies_rel] + | .eq u v => simp only [Condition.holds_eq, Embedding.verifies_eq] | .neg K => - simp only [Condition.holds_neg, verifies_neg] + simp only [Condition.holds_neg, Embedding.verifies_neg] exact not_congr (exists_congr (fun a' => DRS.toRel_iff_verifies K a a')) | .imp ante cons => - simp only [Condition.holds_imp, verifies_imp] + simp only [Condition.holds_imp, Embedding.verifies_imp] refine forall_congr' (fun a' => ?_) rw [DRS.toRel_iff_verifies ante a a', and_imp] refine imp_congr_right (fun _ => imp_congr_right (fun _ => ?_)) exact exists_congr (fun a'' => DRS.toRel_iff_verifies cons a' a'') | .dis l r => - simp only [Condition.holds_dis, verifies_dis, exists_or] + simp only [Condition.holds_dis, Embedding.verifies_dis, exists_or] exact or_congr (exists_congr (fun a' => DRS.toRel_iff_verifies l a a')) (exists_congr (fun a' => DRS.toRel_iff_verifies r a a')) /-- The list analogue of `Condition.holds_iff_verifies`. -/ diff --git a/Linglib/Semantics/Dynamic/DRS/Reduction.lean b/Linglib/Semantics/Dynamic/DRS/Reduction.lean index 8064a02fef..99266803e1 100644 --- a/Linglib/Semantics/Dynamic/DRS/Reduction.lean +++ b/Linglib/Semantics/Dynamic/DRS/Reduction.lean @@ -150,7 +150,7 @@ theorem DRS.realize_toFormula [DecidableEq V] (K : DRS L V) (v : V → M) : match K with | .mk U conds => rw [DRS.toFormula, realize_closeExists] - simp only [DRS.referents_mk, verifies_mk, DRS.Extends] + simp only [DRS.referents_mk, Embedding.verifies_mk, DRS.Extends] exact exists_congr fun v' => and_congr_right fun _ => Condition.realize_toFormulaAll conds v' /-- The open body of a DRS (its conditions, no universe closure) realizes as @@ -168,16 +168,16 @@ theorem Condition.realize_toFormula [DecidableEq V] (c : Condition L V) (v : V BoundedFormula.realize_rel, Term.realize_var] | .eq a b => simp [Condition.toFormula, Formula.realize_equal] | .neg K => - simp only [Condition.toFormula, verifies_neg, Formula.realize_not] + simp only [Condition.toFormula, Embedding.verifies_neg, Formula.realize_not] rw [DRS.realize_toFormula K v] | .imp a c => - simp only [Condition.toFormula, verifies_imp] + simp only [Condition.toFormula, Embedding.verifies_imp] rw [realize_closeForall] simp only [Formula.realize_imp] refine forall_congr' (fun v' => imp_congr_right (fun _ => ?_)) rw [DRS.realize_bodyFormula a v', DRS.realize_toFormula c v'] | .dis l r => - simp only [Condition.toFormula, verifies_dis, Formula.realize_sup] + simp only [Condition.toFormula, Embedding.verifies_dis, Formula.realize_sup] rw [DRS.realize_toFormula l v, DRS.realize_toFormula r v] /-- A list of conditions' conjoined translation realizes as the conjunction of their realizations. -/ diff --git a/Linglib/Semantics/Dynamic/DRS/Verification.lean b/Linglib/Semantics/Dynamic/DRS/Verification.lean index 810a3b6df3..d0220a1d07 100644 --- a/Linglib/Semantics/Dynamic/DRS/Verification.lean +++ b/Linglib/Semantics/Dynamic/DRS/Verification.lean @@ -7,12 +7,15 @@ import Linglib.Semantics.Dynamic.DRS.Basic mathlib `FirstOrder.Language.Structure`. An *embedding function* `f : Embedding V M` assigns discourse referents to individuals in the model; `DRS.Extends K f g` is K&R's extension relation `f [K] g` (both in -`DRS/Basic.lean`); and `Verifies f K` says the embedding `f` *verifies* the -DRS `K`. A sub-DRS is entered by existentially (re)assigning along its -extension relation. For `imp`, the consequent witness extends the *antecedent* -embedding, not the host one — antecedent referents stay visible in the -consequent, the `⇒` accessibility asymmetry. The atomic and `¬` clauses are -Def. 1.4.4(ii); the `⇒`/`∨` clauses are the Chapter 2 conditional and +`DRS/Basic.lean`); and `f.Verifies K` says the embedding `f` *verifies* the +DRS `K`. Verification is the embedding's relation — `Verifies` dispatches over +what is verified (a DRS or a DRS-condition) the way `∈` dispatches over +carriers, so both `f.Verifies K` and `f.Verifies c` are the one +`Embedding.Verifies`. A sub-DRS is entered by existentially (re)assigning +along its extension relation. For `imp`, the consequent witness extends the +*antecedent* embedding, not the host one — antecedent referents stay visible +in the consequent, the `⇒` accessibility asymmetry. The atomic and `¬` clauses +are Def. 1.4.4(ii); the `⇒`/`∨` clauses are the Chapter 2 conditional and disjunction semantics. Truth (Def. 1.4.5) is the existential closure of verification over the outer universe; it is delivered downstream as `DRS.trueRel` (`DRS/Dynamics.lean`) and as the first-order translation's @@ -27,23 +30,23 @@ says "every man is mortal" for K&R, "if there is a man there is a mortal" here. ## Main declarations -* `DRS.Verifies` / `Condition.Verifies` — `Verifies f K` is the field's - "`f` verifies `K`": every condition of `K` holds under `f` +* `Verifiable` / `Embedding.Verifies` — `f.Verifies K` is the field's + "`f` verifies `K`": `f` verifies every condition of `K` (`∀ c ∈ K.conditions`, the `Theory.Model` idiom — no mutual recursion, no list helper). -* `verifies_perm` — verification reads the condition list as a set, cashing - the `List`-representation note in `DRS/Defs.lean`. -* `verifies_map` — renaming along a bijection transports verification: - alphabetic variants (Def. 1.4.8, via `DRS.map` in `DRS/Basic.lean`) have the - same semantics. +* `Embedding.verifies_perm` — verification reads the condition list as a set, + cashing the `List`-representation note in `DRS/Defs.lean`. +* `Embedding.verifies_map` — renaming along a bijection transports + verification: alphabetic variants (Def. 1.4.8, via `DRS.map` in + `DRS/Basic.lean`) have the same semantics. ## Implementation notes -`Condition.Verifies` recurses into sub-DRSs through the nested -`List (Condition L V)` by well-founded recursion on `sizeOf`, so its clause +The clause-wise recursion descends into sub-DRSs through the nested +`List (Condition L V)` by well-founded recursion on `sizeOf`, so the clause characterizations (`verifies_neg`, …) are equation-lemma rewrites rather than -`Iff.rfl`; they restate the clauses with `Verifies` of the sub-DRS, as the textbook -states them. +`Iff.rfl`; they restate the clauses with `Verifies` of the sub-DRS, as the +textbook states them. -/ open FirstOrder FirstOrder.Language @@ -54,69 +57,84 @@ universe u v w x variable {L : Language.{u, v}} {V : Type w} {M : Type x} [L.Structure M] -/-- `Condition.Verifies f c`: the embedding `f` *verifies* the condition `c` -(Def. 1.4.4(ii)); a sub-DRS is entered by existentially (re)assigning along -its extension relation and verifying each of its conditions. -/ -def Condition.Verifies : Embedding V M → Condition L V → Prop +private def verifiesCond : Embedding V M → Condition L V → Prop | f, .rel R args => Structure.RelMap R (fun i => f (args i)) | f, .eq a b => f a = f b - | f, .neg K => ¬ ∃ g, K.Extends f g ∧ ∀ c ∈ K.conditions, Condition.Verifies g c + | f, .neg K => ¬ ∃ g, K.Extends f g ∧ ∀ c ∈ K.conditions, verifiesCond g c | f, .imp a c => - ∀ g, a.Extends f g → (∀ d ∈ a.conditions, Condition.Verifies g d) → - ∃ h, c.Extends g h ∧ ∀ d ∈ c.conditions, Condition.Verifies h d + ∀ g, a.Extends f g → (∀ d ∈ a.conditions, verifiesCond g d) → + ∃ h, c.Extends g h ∧ ∀ d ∈ c.conditions, verifiesCond h d | f, .dis l r => - (∃ g, l.Extends f g ∧ ∀ c ∈ l.conditions, Condition.Verifies g c) ∨ - (∃ g, r.Extends f g ∧ ∀ c ∈ r.conditions, Condition.Verifies g c) + (∃ g, l.Extends f g ∧ ∀ c ∈ l.conditions, verifiesCond g c) ∨ + (∃ g, r.Extends f g ∧ ∀ c ∈ r.conditions, verifiesCond g c) termination_by _ c => sizeOf c decreasing_by all_goals have := DRS.sizeOf_lt_of_mem_conditions (by assumption) simp_wf omega -export Condition (Verifies) +/-- What an embedding can verify: a DRS or a DRS-condition. The dispatch +class behind `Embedding.Verifies` (the `Membership` pattern — one verb, two +carriers). -/ +class Verifiable (α : Type*) (V : Type w) (M : Type x) where + /-- The embedding `f` verifies `x`. -/ + Verifies : Embedding V M → α → Prop -/-- `Verifies f K`: the embedding `f` *verifies* `K` — `f` verifies every -condition of `K` (Def. 1.4.4). -/ -def DRS.Verifies (f : Embedding V M) (K : DRS L V) : Prop := - ∀ c ∈ K.conditions, Condition.Verifies f c +/-- `f.Verifies x`: the embedding `f` *verifies* `x` — a DRS-condition +(Def. 1.4.4(ii)) or a DRS (Def. 1.4.4: `f` verifies every condition of it). -/ +abbrev Embedding.Verifies {α : Type*} [Verifiable α V M] (f : Embedding V M) (x : α) : Prop := + Verifiable.Verifies f x -export DRS (Verifies) +instance instVerifiableCondition : Verifiable (Condition L V) V M := ⟨verifiesCond⟩ + +instance instVerifiableDRS : Verifiable (DRS L V) V M := + ⟨fun f K => ∀ c ∈ K.conditions, f.Verifies c⟩ + +export Embedding (Verifies) + +private theorem verifies_cond_def (f : Embedding V M) (c : Condition L V) : + f.Verifies c = verifiesCond f c := rfl + +private theorem verifies_drs_def (f : Embedding V M) (K : DRS L V) : + f.Verifies K = ∀ c ∈ K.conditions, f.Verifies c := rfl + +namespace Embedding /-! ### Structural simp API -/ variable {f : Embedding V M} @[simp] theorem verifies_mk (U : Finset V) (conds : List (Condition L V)) : - Verifies f (.mk U conds) ↔ ∀ c ∈ conds, Verifies f c := Iff.rfl + f.Verifies (DRS.mk U conds) ↔ ∀ c ∈ conds, f.Verifies c := Iff.rfl @[simp] theorem verifies_rel {n : ℕ} (R : L.Relations n) (args : Fin n → V) : - Verifies f (.rel R args) ↔ Structure.RelMap R (fun i => f (args i)) := by - simp only [Condition.Verifies] + f.Verifies (Condition.rel R args) ↔ Structure.RelMap R (fun i => f (args i)) := by + simp only [verifies_cond_def, verifiesCond] @[simp] theorem verifies_eq (a b : V) : - Verifies f (.eq a b : Condition L V) ↔ f a = f b := by - simp only [Condition.Verifies] + f.Verifies (Condition.eq a b : Condition L V) ↔ f a = f b := by + simp only [verifies_cond_def, verifiesCond] @[simp] theorem verifies_neg (K : DRS L V) : - Verifies f (.neg K) ↔ ¬ ∃ g, K.Extends f g ∧ Verifies g K := by - simp only [Condition.Verifies, DRS.Verifies] + f.Verifies (Condition.neg K) ↔ ¬ ∃ g, K.Extends f g ∧ g.Verifies K := by + simp only [verifies_cond_def, verifies_drs_def, verifiesCond] @[simp] theorem verifies_imp (a c : DRS L V) : - Verifies f (.imp a c) ↔ - ∀ g, a.Extends f g → Verifies g a → - ∃ h, c.Extends g h ∧ Verifies h c := by - simp only [Condition.Verifies, DRS.Verifies] + f.Verifies (Condition.imp a c) ↔ + ∀ g, a.Extends f g → g.Verifies a → + ∃ h, c.Extends g h ∧ h.Verifies c := by + simp only [verifies_cond_def, verifies_drs_def, verifiesCond] @[simp] theorem verifies_dis (l r : DRS L V) : - Verifies f (.dis l r) ↔ - (∃ g, l.Extends f g ∧ Verifies g l) ∨ - (∃ g, r.Extends f g ∧ Verifies g r) := by - simp only [Condition.Verifies, DRS.Verifies] + f.Verifies (Condition.dis l r) ↔ + (∃ g, l.Extends f g ∧ g.Verifies l) ∨ + (∃ g, r.Extends f g ∧ g.Verifies r) := by + simp only [verifies_cond_def, verifies_drs_def, verifiesCond] /-- Verification is invariant under permutation of the conditions — the set semantics the `List`-valued `conditions` field promises (`DRS/Defs.lean`). -/ theorem verifies_perm {U : Finset V} {cs ds : List (Condition L V)} (h : cs.Perm ds) : - Verifies f (.mk U cs) ↔ Verifies f (.mk U ds) := by + f.Verifies (DRS.mk U cs) ↔ f.Verifies (DRS.mk U ds) := by simp only [verifies_mk, h.mem_iff] /-! ### Alphabetic variants -/ @@ -128,7 +146,7 @@ variable {W : Type*} [DecidableEq W] /-- Precomposition with `e` is a bijection between the embeddings extending `f` on `U.image e` and those extending `f ∘ e` on `U`. -/ private theorem exists_precomp_extend_iff (e : V ≃ W) (U : Finset V) (f : Embedding W M) - (P : (Embedding V M) → Prop) : + (P : Embedding V M → Prop) : (∃ g : Embedding W M, (∀ y ∉ U.image e, g y = f y) ∧ P (g ∘ e)) ↔ ∃ w' : Embedding V M, (∀ x ∉ U, w' x = f (e x)) ∧ P w' := by constructor @@ -143,7 +161,7 @@ private theorem exists_precomp_extend_iff (e : V ≃ W) (U : Finset V) (f : Embe /-- The `∀` analogue of `exists_precomp_extend_iff`. -/ private theorem forall_precomp_extend_iff (e : V ≃ W) (U : Finset V) (f : Embedding W M) - (P : (Embedding V M) → Prop) : + (P : Embedding V M → Prop) : (∀ g : Embedding W M, (∀ y ∉ U.image e, g y = f y) → P (g ∘ e)) ↔ ∀ w' : Embedding V M, (∀ x ∉ U, w' x = f (e x)) → P w' := by constructor @@ -161,12 +179,13 @@ private theorem verifies_map_all (e : V ≃ W) (K : DRS L V) (g : Embedding W M) (ih : ∀ c ∈ K.conditions, ∀ u : Embedding W M, Verifies u (c.map e) ↔ Verifies (u ∘ e) c) : Verifies g (K.map e) ↔ Verifies (g ∘ e) K := by - simp only [DRS.Verifies, DRS.conditions_map, Condition.mapList_eq_map, List.forall_mem_map] + simp only [verifies_drs_def, DRS.conditions_map, Condition.mapList_eq_map, + List.forall_mem_map] exact forall_congr' fun c => imp_congr_right fun hc => ih c hc g /-- Renaming along a bijection transports verification (the condition form of `verifies_map`). -/ -theorem Condition.verifies_map (e : V ≃ W) : ∀ (f : Embedding W M) (c : Condition L V), +theorem verifies_map_cond (e : V ≃ W) : ∀ (f : Embedding W M) (c : Condition L V), Verifies f (c.map e) ↔ Verifies (f ∘ e) c | f, .rel R args => by simp [Condition.map, Function.comp] @@ -174,33 +193,33 @@ theorem Condition.verifies_map (e : V ≃ W) : ∀ (f : Embedding W M) (c : Cond simp [Condition.map, Function.comp] | f, .neg K => by have hK := fun g : Embedding W M => - verifies_map_all e K g (fun d hd u => Condition.verifies_map e u d) + verifies_map_all e K g (fun d hd u => verifies_map_cond e u d) simp only [Condition.map, verifies_neg, DRS.Extends, DRS.referents_map] exact not_congr ((exists_congr fun g => and_congr_right fun _ => hK g).trans - (exists_precomp_extend_iff e K.referents f (DRS.Verifies · K))) + (exists_precomp_extend_iff e K.referents f (Verifies · K))) | f, .imp a c => by have hA := fun g : Embedding W M => - verifies_map_all e a g (fun d hd u => Condition.verifies_map e u d) + verifies_map_all e a g (fun d hd u => verifies_map_cond e u d) have hC := fun g : Embedding W M => - verifies_map_all e c g (fun d hd u => Condition.verifies_map e u d) + verifies_map_all e c g (fun d hd u => verifies_map_cond e u d) simp only [Condition.map, verifies_imp, DRS.Extends, DRS.referents_map] refine Iff.trans (forall_congr' fun g => imp_congr_right fun _ => imp_congr (hA g) ((exists_congr fun h => and_congr_right fun _ => hC h).trans - (exists_precomp_extend_iff e c.referents g (DRS.Verifies · c)))) ?_ + (exists_precomp_extend_iff e c.referents g (Verifies · c)))) ?_ exact forall_precomp_extend_iff e a.referents f - (fun u => DRS.Verifies u a → - ∃ w'', (∀ x ∉ c.referents, w'' x = u x) ∧ DRS.Verifies w'' c) + (fun u => Verifies u a → + ∃ w'', (∀ x ∉ c.referents, w'' x = u x) ∧ Verifies w'' c) | f, .dis l r => by have hL := fun g : Embedding W M => - verifies_map_all e l g (fun d hd u => Condition.verifies_map e u d) + verifies_map_all e l g (fun d hd u => verifies_map_cond e u d) have hR := fun g : Embedding W M => - verifies_map_all e r g (fun d hd u => Condition.verifies_map e u d) + verifies_map_all e r g (fun d hd u => verifies_map_cond e u d) simp only [Condition.map, verifies_dis, DRS.Extends, DRS.referents_map] exact or_congr ((exists_congr fun g => and_congr_right fun _ => hL g).trans - (exists_precomp_extend_iff e l.referents f (DRS.Verifies · l))) + (exists_precomp_extend_iff e l.referents f (Verifies · l))) ((exists_congr fun g => and_congr_right fun _ => hR g).trans - (exists_precomp_extend_iff e r.referents f (DRS.Verifies · r))) + (exists_precomp_extend_iff e r.referents f (Verifies · r))) termination_by _ c => sizeOf c decreasing_by all_goals have := DRS.sizeOf_lt_of_mem_conditions (by assumption) @@ -211,8 +230,10 @@ decreasing_by all_goals iff `f ∘ e` verifies `K` — alphabetic variants have the same semantics. -/ theorem verifies_map (e : V ≃ W) (f : Embedding W M) (K : DRS L V) : Verifies f (K.map e) ↔ Verifies (f ∘ e) K := - verifies_map_all e K f (fun c _ u => Condition.verifies_map e u c) + verifies_map_all e K f (fun c _ u => verifies_map_cond e u c) end Map +end Embedding + end DRT diff --git a/Linglib/Studies/KampReyle1993.lean b/Linglib/Studies/KampReyle1993.lean index bfd4dfdd3c..f116a4a92e 100644 --- a/Linglib/Studies/KampReyle1993.lean +++ b/Linglib/Studies/KampReyle1993.lean @@ -7,7 +7,7 @@ import Mathlib.Data.Fin.VecNotation K&R's worked examples, evaluated through the faithful model-theoretic DRS core (`Semantics/Dynamic/DRS/`). Each truth-condition is a theorem about the substrate -denotation `DRS.trueRel` (Muskens's relational truth, equivalently `DRS.Verifies`), +denotation `DRS.trueRel` (Muskens's relational truth, equivalently `Embedding.Verifies`), not a local re-implementation. ## Examples From 3ff2113cfc36169a52ebbf8d5c0e2ae900924891 Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Fri, 7 Aug 2026 13:16:27 -0700 Subject: [PATCH 04/15] docs(Semantics/Dynamic/DRS): fix stale DRS.Verifies mentions --- Linglib/Semantics/Dynamic/DRS/Reduction.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Linglib/Semantics/Dynamic/DRS/Reduction.lean b/Linglib/Semantics/Dynamic/DRS/Reduction.lean index 99266803e1..a19b2050e5 100644 --- a/Linglib/Semantics/Dynamic/DRS/Reduction.lean +++ b/Linglib/Semantics/Dynamic/DRS/Reduction.lean @@ -7,7 +7,7 @@ import Mathlib.ModelTheory.Semantics The bespoke DRS box language is *equivalent to ordinary first-order logic*. We translate each DRS into a mathlib `FirstOrder.Language.Formula` and prove its `Realize` coincides with the -bespoke `DRS.Verifies` — [kamp-reyle-1993]'s §1.5 ("From DRT to Predicate +bespoke `Embedding.Verifies` — [kamp-reyle-1993]'s §1.5 ("From DRT to Predicate Logic") and [muskens-1996]'s "DRSs are already present in classical logic", now a Lean theorem (`DRS.realize_toFormula`) rather than an assertion. @@ -142,7 +142,7 @@ theorem realize_closeForall [DecidableEq V] (U : Finset V) (φ : L.Formula V) (v mutual /-- **DRT ⊆ FOL** (§1.5): the -translated formula's `Realize` coincides with the bespoke `DRS.Verifies`. As +translated formula's `Realize` coincides with the bespoke `Embedding.Verifies`. As `toFormula` existentially closes the universe, the correspondence is with an embedding `v'` extending `v` over `K.referents`. -/ theorem DRS.realize_toFormula [DecidableEq V] (K : DRS L V) (v : V → M) : @@ -154,7 +154,7 @@ theorem DRS.realize_toFormula [DecidableEq V] (K : DRS L V) (v : V → M) : exact exists_congr fun v' => and_congr_right fun _ => Condition.realize_toFormulaAll conds v' /-- The open body of a DRS (its conditions, no universe closure) realizes as -`DRS.Verifies` (used for the antecedent of `⇒`). -/ +`Verifies` of the DRS (used for the antecedent of `⇒`). -/ theorem DRS.realize_bodyFormula [DecidableEq V] (K : DRS L V) (v : V → M) : (DRS.bodyFormula K).Realize v ↔ Verifies v K := by match K with From b94d470c7d4ec2c7a1df4b27736264fe6a5b6981 Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Fri, 7 Aug 2026 13:20:37 -0700 Subject: [PATCH 05/15] refactor(Semantics/Dynamic/DRS): drop Verifiable class; two plain defs --- Linglib/Semantics/Dynamic/DRS/Dynamics.lean | 4 +- Linglib/Semantics/Dynamic/DRS/Reduction.lean | 6 +- .../Semantics/Dynamic/DRS/Verification.lean | 104 ++++++++---------- 3 files changed, 48 insertions(+), 66 deletions(-) diff --git a/Linglib/Semantics/Dynamic/DRS/Dynamics.lean b/Linglib/Semantics/Dynamic/DRS/Dynamics.lean index d4a4571ee7..88b64f1e7d 100644 --- a/Linglib/Semantics/Dynamic/DRS/Dynamics.lean +++ b/Linglib/Semantics/Dynamic/DRS/Dynamics.lean @@ -131,7 +131,7 @@ theorem DRS.toRel_iff_verifies (K : DRS L V) (a a' : V → M) : exact and_congr_right (fun _ => Condition.holdsAll_iff_verifies conds a') /-- A condition's set denotation agrees with its static `Verifies`. -/ theorem Condition.holds_iff_verifies (c : Condition L V) (a : V → M) : - c.holds a ↔ Verifies a c := by + c.holds a ↔ VerifiesCond a c := by match c with | .rel R args => simp only [Condition.holds_rel, Embedding.verifies_rel] | .eq u v => simp only [Condition.holds_eq, Embedding.verifies_eq] @@ -150,7 +150,7 @@ theorem Condition.holds_iff_verifies (c : Condition L V) (a : V → M) : (exists_congr (fun a' => DRS.toRel_iff_verifies r a a')) /-- The list analogue of `Condition.holds_iff_verifies`. -/ theorem Condition.holdsAll_iff_verifies (cs : List (Condition L V)) (a : V → M) : - Condition.holdsAll cs a ↔ ∀ c ∈ cs, Verifies a c := by + Condition.holdsAll cs a ↔ ∀ c ∈ cs, VerifiesCond a c := by match cs with | [] => simp | c :: cs => diff --git a/Linglib/Semantics/Dynamic/DRS/Reduction.lean b/Linglib/Semantics/Dynamic/DRS/Reduction.lean index a19b2050e5..78bd17cccb 100644 --- a/Linglib/Semantics/Dynamic/DRS/Reduction.lean +++ b/Linglib/Semantics/Dynamic/DRS/Reduction.lean @@ -159,9 +159,9 @@ theorem DRS.realize_bodyFormula [DecidableEq V] (K : DRS L V) (v : V → M) : (DRS.bodyFormula K).Realize v ↔ Verifies v K := by match K with | .mk _ conds => exact Condition.realize_toFormulaAll conds v -/-- A single condition's translation realizes as `Condition.Verifies`. -/ +/-- A single condition's translation realizes as `VerifiesCond`. -/ theorem Condition.realize_toFormula [DecidableEq V] (c : Condition L V) (v : V → M) : - (Condition.toFormula c).Realize v ↔ Verifies v c := by + (Condition.toFormula c).Realize v ↔ VerifiesCond v c := by match c with | .rel R args => simp [Condition.toFormula, Relations.formula, Formula.Realize, @@ -182,7 +182,7 @@ theorem Condition.realize_toFormula [DecidableEq V] (c : Condition L V) (v : V /-- A list of conditions' conjoined translation realizes as the conjunction of their realizations. -/ theorem Condition.realize_toFormulaAll [DecidableEq V] (cs : List (Condition L V)) (v : V → M) : - (Condition.toFormulaAll cs).Realize v ↔ ∀ c ∈ cs, Verifies v c := by + (Condition.toFormulaAll cs).Realize v ↔ ∀ c ∈ cs, VerifiesCond v c := by match cs with | [] => simp [Condition.toFormulaAll, Formula.realize_top] | c :: cs => diff --git a/Linglib/Semantics/Dynamic/DRS/Verification.lean b/Linglib/Semantics/Dynamic/DRS/Verification.lean index d0220a1d07..248831fb29 100644 --- a/Linglib/Semantics/Dynamic/DRS/Verification.lean +++ b/Linglib/Semantics/Dynamic/DRS/Verification.lean @@ -7,18 +7,16 @@ import Linglib.Semantics.Dynamic.DRS.Basic mathlib `FirstOrder.Language.Structure`. An *embedding function* `f : Embedding V M` assigns discourse referents to individuals in the model; `DRS.Extends K f g` is K&R's extension relation `f [K] g` (both in -`DRS/Basic.lean`); and `f.Verifies K` says the embedding `f` *verifies* the -DRS `K`. Verification is the embedding's relation — `Verifies` dispatches over -what is verified (a DRS or a DRS-condition) the way `∈` dispatches over -carriers, so both `f.Verifies K` and `f.Verifies c` are the one -`Embedding.Verifies`. A sub-DRS is entered by existentially (re)assigning -along its extension relation. For `imp`, the consequent witness extends the -*antecedent* embedding, not the host one — antecedent referents stay visible -in the consequent, the `⇒` accessibility asymmetry. The atomic and `¬` clauses -are Def. 1.4.4(ii); the `⇒`/`∨` clauses are the Chapter 2 conditional and -disjunction semantics. Truth (Def. 1.4.5) is the existential closure of -verification over the outer universe; it is delivered downstream as -`DRS.trueRel` (`DRS/Dynamics.lean`) and as the first-order translation's +`DRS/Basic.lean`); `f.Verifies K` says the embedding `f` *verifies* the DRS +`K` — it verifies every condition of `K` — and `f.VerifiesCond c` that it +verifies the DRS-condition `c`. A sub-DRS is entered by existentially +(re)assigning along its extension relation. For `imp`, the consequent witness +extends the *antecedent* embedding, not the host one — antecedent referents +stay visible in the consequent, the `⇒` accessibility asymmetry. The atomic +and `¬` clauses are Def. 1.4.4(ii); the `⇒`/`∨` clauses are the Chapter 2 +conditional and disjunction semantics. Truth (Def. 1.4.5) is the existential +closure of verification over the outer universe; it is delivered downstream +as `DRS.trueRel` (`DRS/Dynamics.lean`) and as the first-order translation's realization (`DRS/Reduction.lean`). **Deviation** ([muskens-1996], fn. 4): K&R's embeddings are *partial* functions @@ -30,8 +28,8 @@ says "every man is mortal" for K&R, "if there is a man there is a mortal" here. ## Main declarations -* `Verifiable` / `Embedding.Verifies` — `f.Verifies K` is the field's - "`f` verifies `K`": `f` verifies every condition of `K` +* `Embedding.Verifies` / `Embedding.VerifiesCond` — `f.Verifies K` is the + field's "`f` verifies `K`": `f` verifies every condition of `K` (`∀ c ∈ K.conditions`, the `Theory.Model` idiom — no mutual recursion, no list helper). * `Embedding.verifies_perm` — verification reads the condition list as a set, @@ -42,8 +40,8 @@ says "every man is mortal" for K&R, "if there is a man there is a mortal" here. ## Implementation notes -The clause-wise recursion descends into sub-DRSs through the nested -`List (Condition L V)` by well-founded recursion on `sizeOf`, so the clause +`VerifiesCond` descends into sub-DRSs through the nested +`List (Condition L V)` by well-founded recursion on `sizeOf`, so its clause characterizations (`verifies_neg`, …) are equation-lemma rewrites rather than `Iff.rfl`; they restate the clauses with `Verifies` of the sub-DRS, as the textbook states them. @@ -57,46 +55,31 @@ universe u v w x variable {L : Language.{u, v}} {V : Type w} {M : Type x} [L.Structure M] -private def verifiesCond : Embedding V M → Condition L V → Prop +/-- `f.VerifiesCond c`: the embedding `f` *verifies* the DRS-condition `c` +(Def. 1.4.4(ii)); a sub-DRS is entered by existentially (re)assigning along +its extension relation and verifying each of its conditions. -/ +def Embedding.VerifiesCond : Embedding V M → Condition L V → Prop | f, .rel R args => Structure.RelMap R (fun i => f (args i)) | f, .eq a b => f a = f b - | f, .neg K => ¬ ∃ g, K.Extends f g ∧ ∀ c ∈ K.conditions, verifiesCond g c + | f, .neg K => ¬ ∃ g, K.Extends f g ∧ ∀ c ∈ K.conditions, g.VerifiesCond c | f, .imp a c => - ∀ g, a.Extends f g → (∀ d ∈ a.conditions, verifiesCond g d) → - ∃ h, c.Extends g h ∧ ∀ d ∈ c.conditions, verifiesCond h d + ∀ g, a.Extends f g → (∀ d ∈ a.conditions, g.VerifiesCond d) → + ∃ h, c.Extends g h ∧ ∀ d ∈ c.conditions, h.VerifiesCond d | f, .dis l r => - (∃ g, l.Extends f g ∧ ∀ c ∈ l.conditions, verifiesCond g c) ∨ - (∃ g, r.Extends f g ∧ ∀ c ∈ r.conditions, verifiesCond g c) + (∃ g, l.Extends f g ∧ ∀ c ∈ l.conditions, g.VerifiesCond c) ∨ + (∃ g, r.Extends f g ∧ ∀ c ∈ r.conditions, g.VerifiesCond c) termination_by _ c => sizeOf c decreasing_by all_goals have := DRS.sizeOf_lt_of_mem_conditions (by assumption) simp_wf omega -/-- What an embedding can verify: a DRS or a DRS-condition. The dispatch -class behind `Embedding.Verifies` (the `Membership` pattern — one verb, two -carriers). -/ -class Verifiable (α : Type*) (V : Type w) (M : Type x) where - /-- The embedding `f` verifies `x`. -/ - Verifies : Embedding V M → α → Prop +/-- `f.Verifies K`: the embedding `f` *verifies* the DRS `K` — `f` verifies +every condition of `K` (Def. 1.4.4). -/ +def Embedding.Verifies (f : Embedding V M) (K : DRS L V) : Prop := + ∀ c ∈ K.conditions, f.VerifiesCond c -/-- `f.Verifies x`: the embedding `f` *verifies* `x` — a DRS-condition -(Def. 1.4.4(ii)) or a DRS (Def. 1.4.4: `f` verifies every condition of it). -/ -abbrev Embedding.Verifies {α : Type*} [Verifiable α V M] (f : Embedding V M) (x : α) : Prop := - Verifiable.Verifies f x - -instance instVerifiableCondition : Verifiable (Condition L V) V M := ⟨verifiesCond⟩ - -instance instVerifiableDRS : Verifiable (DRS L V) V M := - ⟨fun f K => ∀ c ∈ K.conditions, f.Verifies c⟩ - -export Embedding (Verifies) - -private theorem verifies_cond_def (f : Embedding V M) (c : Condition L V) : - f.Verifies c = verifiesCond f c := rfl - -private theorem verifies_drs_def (f : Embedding V M) (K : DRS L V) : - f.Verifies K = ∀ c ∈ K.conditions, f.Verifies c := rfl +export Embedding (Verifies VerifiesCond) namespace Embedding @@ -105,36 +88,36 @@ namespace Embedding variable {f : Embedding V M} @[simp] theorem verifies_mk (U : Finset V) (conds : List (Condition L V)) : - f.Verifies (DRS.mk U conds) ↔ ∀ c ∈ conds, f.Verifies c := Iff.rfl + f.Verifies (.mk U conds) ↔ ∀ c ∈ conds, f.VerifiesCond c := Iff.rfl @[simp] theorem verifies_rel {n : ℕ} (R : L.Relations n) (args : Fin n → V) : - f.Verifies (Condition.rel R args) ↔ Structure.RelMap R (fun i => f (args i)) := by - simp only [verifies_cond_def, verifiesCond] + f.VerifiesCond (.rel R args) ↔ Structure.RelMap R (fun i => f (args i)) := by + simp only [VerifiesCond] @[simp] theorem verifies_eq (a b : V) : - f.Verifies (Condition.eq a b : Condition L V) ↔ f a = f b := by - simp only [verifies_cond_def, verifiesCond] + f.VerifiesCond (.eq a b : Condition L V) ↔ f a = f b := by + simp only [VerifiesCond] @[simp] theorem verifies_neg (K : DRS L V) : - f.Verifies (Condition.neg K) ↔ ¬ ∃ g, K.Extends f g ∧ g.Verifies K := by - simp only [verifies_cond_def, verifies_drs_def, verifiesCond] + f.VerifiesCond (.neg K) ↔ ¬ ∃ g, K.Extends f g ∧ g.Verifies K := by + simp only [VerifiesCond, Verifies] @[simp] theorem verifies_imp (a c : DRS L V) : - f.Verifies (Condition.imp a c) ↔ + f.VerifiesCond (.imp a c) ↔ ∀ g, a.Extends f g → g.Verifies a → ∃ h, c.Extends g h ∧ h.Verifies c := by - simp only [verifies_cond_def, verifies_drs_def, verifiesCond] + simp only [VerifiesCond, Verifies] @[simp] theorem verifies_dis (l r : DRS L V) : - f.Verifies (Condition.dis l r) ↔ + f.VerifiesCond (.dis l r) ↔ (∃ g, l.Extends f g ∧ g.Verifies l) ∨ (∃ g, r.Extends f g ∧ g.Verifies r) := by - simp only [verifies_cond_def, verifies_drs_def, verifiesCond] + simp only [VerifiesCond, Verifies] /-- Verification is invariant under permutation of the conditions — the set semantics the `List`-valued `conditions` field promises (`DRS/Defs.lean`). -/ theorem verifies_perm {U : Finset V} {cs ds : List (Condition L V)} (h : cs.Perm ds) : - f.Verifies (DRS.mk U cs) ↔ f.Verifies (DRS.mk U ds) := by + f.Verifies (.mk U cs) ↔ f.Verifies (.mk U ds) := by simp only [verifies_mk, h.mem_iff] /-! ### Alphabetic variants -/ @@ -177,16 +160,15 @@ private theorem forall_precomp_extend_iff (e : V ≃ W) (U : Finset V) (f : Embe original, given the transport for each of the DRS's conditions. -/ private theorem verifies_map_all (e : V ≃ W) (K : DRS L V) (g : Embedding W M) (ih : ∀ c ∈ K.conditions, ∀ u : Embedding W M, - Verifies u (c.map e) ↔ Verifies (u ∘ e) c) : + VerifiesCond u (c.map e) ↔ VerifiesCond (u ∘ e) c) : Verifies g (K.map e) ↔ Verifies (g ∘ e) K := by - simp only [verifies_drs_def, DRS.conditions_map, Condition.mapList_eq_map, - List.forall_mem_map] + simp only [Verifies, DRS.conditions_map, Condition.mapList_eq_map, List.forall_mem_map] exact forall_congr' fun c => imp_congr_right fun hc => ih c hc g /-- Renaming along a bijection transports verification (the condition form of `verifies_map`). -/ theorem verifies_map_cond (e : V ≃ W) : ∀ (f : Embedding W M) (c : Condition L V), - Verifies f (c.map e) ↔ Verifies (f ∘ e) c + VerifiesCond f (c.map e) ↔ VerifiesCond (f ∘ e) c | f, .rel R args => by simp [Condition.map, Function.comp] | f, .eq a b => by From 38cc36e0a3850fd82327196e328f1ab305a686ef Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Fri, 7 Aug 2026 13:24:55 -0700 Subject: [PATCH 06/15] docs(Semantics/Dynamic/DRS): Embedding docstring, model-relativity split --- Linglib/Semantics/Dynamic/DRS/Basic.lean | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/Linglib/Semantics/Dynamic/DRS/Basic.lean b/Linglib/Semantics/Dynamic/DRS/Basic.lean index d5b016a8cb..1b6c9ff435 100644 --- a/Linglib/Semantics/Dynamic/DRS/Basic.lean +++ b/Linglib/Semantics/Dynamic/DRS/Basic.lean @@ -113,8 +113,12 @@ end DRS /-! ### Embeddings and the extension relation -/ /-- An *embedding function*: an assignment of discourse referents to -individuals in a model — in the total-assignment rendering (deviation note in -`DRS/Verification.lean`). -/ +individuals in a given model, in the total-assignment rendering (deviation +note in `DRS/Verification.lean`). `M` is the model's domain of individuals; +the model itself — `M` together with an interpretation of the relation +symbols — is the `L.Structure M` instance that verification +(`Embedding.Verifies`) requires, so embeddings and the extension relation +need no model theory, while `f.Verifies K` only exists in a given model. -/ abbrev Embedding (V : Type w) (M : Type*) := V → M variable {M : Type*} in From 980a331e700fe0bb66c82b707eb71245926ad381 Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Fri, 7 Aug 2026 13:37:05 -0700 Subject: [PATCH 07/15] refactor(Semantics/Dynamic/DRS): drop export, dot-form consumers, merge API --- Linglib/Semantics/Dynamic/DRS/Dynamics.lean | 12 +++++------ Linglib/Semantics/Dynamic/DRS/Reduction.lean | 17 ++++++++-------- .../Semantics/Dynamic/DRS/Verification.lean | 20 +++++++++++++------ 3 files changed, 29 insertions(+), 20 deletions(-) diff --git a/Linglib/Semantics/Dynamic/DRS/Dynamics.lean b/Linglib/Semantics/Dynamic/DRS/Dynamics.lean index 88b64f1e7d..ec32e93ad8 100644 --- a/Linglib/Semantics/Dynamic/DRS/Dynamics.lean +++ b/Linglib/Semantics/Dynamic/DRS/Dynamics.lean @@ -123,15 +123,15 @@ mutual agrees with the static verifying-embedding semantics — `toRel K a a'` holds iff the output `a'` extends the input `a` over `K`'s universe and verifies `K`. (Both sides are the total-assignment variant; see `DRS/Verification.lean`.) -/ -theorem DRS.toRel_iff_verifies (K : DRS L V) (a a' : V → M) : - DRS.toRel K a a' ↔ K.Extends a a' ∧ Verifies a' K := by +theorem DRS.toRel_iff_verifies (K : DRS L V) (a a' : Embedding V M) : + DRS.toRel K a a' ↔ K.Extends a a' ∧ a'.Verifies K := by match K with | .mk U conds => simp only [DRS.toRel, DRS.referents_mk, Embedding.verifies_mk, DRS.Extends] exact and_congr_right (fun _ => Condition.holdsAll_iff_verifies conds a') /-- A condition's set denotation agrees with its static `Verifies`. -/ -theorem Condition.holds_iff_verifies (c : Condition L V) (a : V → M) : - c.holds a ↔ VerifiesCond a c := by +theorem Condition.holds_iff_verifies (c : Condition L V) (a : Embedding V M) : + c.holds a ↔ a.VerifiesCond c := by match c with | .rel R args => simp only [Condition.holds_rel, Embedding.verifies_rel] | .eq u v => simp only [Condition.holds_eq, Embedding.verifies_eq] @@ -149,8 +149,8 @@ theorem Condition.holds_iff_verifies (c : Condition L V) (a : V → M) : exact or_congr (exists_congr (fun a' => DRS.toRel_iff_verifies l a a')) (exists_congr (fun a' => DRS.toRel_iff_verifies r a a')) /-- The list analogue of `Condition.holds_iff_verifies`. -/ -theorem Condition.holdsAll_iff_verifies (cs : List (Condition L V)) (a : V → M) : - Condition.holdsAll cs a ↔ ∀ c ∈ cs, VerifiesCond a c := by +theorem Condition.holdsAll_iff_verifies (cs : List (Condition L V)) (a : Embedding V M) : + Condition.holdsAll cs a ↔ ∀ c ∈ cs, a.VerifiesCond c := by match cs with | [] => simp | c :: cs => diff --git a/Linglib/Semantics/Dynamic/DRS/Reduction.lean b/Linglib/Semantics/Dynamic/DRS/Reduction.lean index 78bd17cccb..4d7713a992 100644 --- a/Linglib/Semantics/Dynamic/DRS/Reduction.lean +++ b/Linglib/Semantics/Dynamic/DRS/Reduction.lean @@ -145,8 +145,8 @@ mutual translated formula's `Realize` coincides with the bespoke `Embedding.Verifies`. As `toFormula` existentially closes the universe, the correspondence is with an embedding `v'` extending `v` over `K.referents`. -/ -theorem DRS.realize_toFormula [DecidableEq V] (K : DRS L V) (v : V → M) : - (K.toFormula).Realize v ↔ ∃ v', K.Extends v v' ∧ Verifies v' K := by +theorem DRS.realize_toFormula [DecidableEq V] (K : DRS L V) (v : Embedding V M) : + (K.toFormula).Realize v ↔ ∃ v', K.Extends v v' ∧ v'.Verifies K := by match K with | .mk U conds => rw [DRS.toFormula, realize_closeExists] @@ -155,13 +155,13 @@ theorem DRS.realize_toFormula [DecidableEq V] (K : DRS L V) (v : V → M) : and_congr_right fun _ => Condition.realize_toFormulaAll conds v' /-- The open body of a DRS (its conditions, no universe closure) realizes as `Verifies` of the DRS (used for the antecedent of `⇒`). -/ -theorem DRS.realize_bodyFormula [DecidableEq V] (K : DRS L V) (v : V → M) : - (DRS.bodyFormula K).Realize v ↔ Verifies v K := by +theorem DRS.realize_bodyFormula [DecidableEq V] (K : DRS L V) (v : Embedding V M) : + (DRS.bodyFormula K).Realize v ↔ v.Verifies K := by match K with | .mk _ conds => exact Condition.realize_toFormulaAll conds v /-- A single condition's translation realizes as `VerifiesCond`. -/ -theorem Condition.realize_toFormula [DecidableEq V] (c : Condition L V) (v : V → M) : - (Condition.toFormula c).Realize v ↔ VerifiesCond v c := by +theorem Condition.realize_toFormula [DecidableEq V] (c : Condition L V) (v : Embedding V M) : + (Condition.toFormula c).Realize v ↔ v.VerifiesCond c := by match c with | .rel R args => simp [Condition.toFormula, Relations.formula, Formula.Realize, @@ -181,8 +181,9 @@ theorem Condition.realize_toFormula [DecidableEq V] (c : Condition L V) (v : V rw [DRS.realize_toFormula l v, DRS.realize_toFormula r v] /-- A list of conditions' conjoined translation realizes as the conjunction of their realizations. -/ -theorem Condition.realize_toFormulaAll [DecidableEq V] (cs : List (Condition L V)) (v : V → M) : - (Condition.toFormulaAll cs).Realize v ↔ ∀ c ∈ cs, VerifiesCond v c := by +theorem Condition.realize_toFormulaAll [DecidableEq V] (cs : List (Condition L V)) + (v : Embedding V M) : + (Condition.toFormulaAll cs).Realize v ↔ ∀ c ∈ cs, v.VerifiesCond c := by match cs with | [] => simp [Condition.toFormulaAll, Formula.realize_top] | c :: cs => diff --git a/Linglib/Semantics/Dynamic/DRS/Verification.lean b/Linglib/Semantics/Dynamic/DRS/Verification.lean index 248831fb29..c74f661ebb 100644 --- a/Linglib/Semantics/Dynamic/DRS/Verification.lean +++ b/Linglib/Semantics/Dynamic/DRS/Verification.lean @@ -79,8 +79,6 @@ every condition of `K` (Def. 1.4.4). -/ def Embedding.Verifies (f : Embedding V M) (K : DRS L V) : Prop := ∀ c ∈ K.conditions, f.VerifiesCond c -export Embedding (Verifies VerifiesCond) - namespace Embedding /-! ### Structural simp API -/ @@ -90,6 +88,16 @@ variable {f : Embedding V M} @[simp] theorem verifies_mk (U : Finset V) (conds : List (Condition L V)) : f.Verifies (.mk U conds) ↔ ∀ c ∈ conds, f.VerifiesCond c := Iff.rfl +theorem verifies_iff {K : DRS L V} : + f.Verifies K ↔ ∀ c ∈ K.conditions, f.VerifiesCond c := Iff.rfl + +@[simp] theorem verifies_empty : f.Verifies (.empty : DRS L V) := by + simp [DRS.empty] + +@[simp] theorem verifies_merge [DecidableEq V] (K₁ K₂ : DRS L V) : + f.Verifies (K₁.merge K₂) ↔ f.Verifies K₁ ∧ f.Verifies K₂ := by + simp only [verifies_iff, DRS.conditions_merge, List.forall_mem_append] + @[simp] theorem verifies_rel {n : ℕ} (R : L.Relations n) (args : Fin n → V) : f.VerifiesCond (.rel R args) ↔ Structure.RelMap R (fun i => f (args i)) := by simp only [VerifiesCond] @@ -160,15 +168,15 @@ private theorem forall_precomp_extend_iff (e : V ≃ W) (U : Finset V) (f : Embe original, given the transport for each of the DRS's conditions. -/ private theorem verifies_map_all (e : V ≃ W) (K : DRS L V) (g : Embedding W M) (ih : ∀ c ∈ K.conditions, ∀ u : Embedding W M, - VerifiesCond u (c.map e) ↔ VerifiesCond (u ∘ e) c) : - Verifies g (K.map e) ↔ Verifies (g ∘ e) K := by + u.VerifiesCond (c.map e) ↔ VerifiesCond (u ∘ e) c) : + g.Verifies (K.map e) ↔ Verifies (g ∘ e) K := by simp only [Verifies, DRS.conditions_map, Condition.mapList_eq_map, List.forall_mem_map] exact forall_congr' fun c => imp_congr_right fun hc => ih c hc g /-- Renaming along a bijection transports verification (the condition form of `verifies_map`). -/ theorem verifies_map_cond (e : V ≃ W) : ∀ (f : Embedding W M) (c : Condition L V), - VerifiesCond f (c.map e) ↔ VerifiesCond (f ∘ e) c + f.VerifiesCond (c.map e) ↔ VerifiesCond (f ∘ e) c | f, .rel R args => by simp [Condition.map, Function.comp] | f, .eq a b => by @@ -211,7 +219,7 @@ decreasing_by all_goals /-- Renaming along a bijection transports verification: `f` verifies `K.map e` iff `f ∘ e` verifies `K` — alphabetic variants have the same semantics. -/ theorem verifies_map (e : V ≃ W) (f : Embedding W M) (K : DRS L V) : - Verifies f (K.map e) ↔ Verifies (f ∘ e) K := + f.Verifies (K.map e) ↔ Verifies (f ∘ e) K := verifies_map_all e K f (fun c _ u => verifies_map_cond e u c) end Map From 1f7f6e13197069ba65bebbd903fcedc510ab19a5 Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Fri, 7 Aug 2026 13:54:51 -0700 Subject: [PATCH 08/15] =?UTF-8?q?style(Semantics/Dynamic/DRS):=20VerifiesC?= =?UTF-8?q?ond=20=E2=86=92=20VerifiesCondition?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Linglib/Semantics/Dynamic/DRS/Dynamics.lean | 4 +- Linglib/Semantics/Dynamic/DRS/Reduction.lean | 6 +- .../Semantics/Dynamic/DRS/Verification.lean | 64 +++++++++---------- 3 files changed, 37 insertions(+), 37 deletions(-) diff --git a/Linglib/Semantics/Dynamic/DRS/Dynamics.lean b/Linglib/Semantics/Dynamic/DRS/Dynamics.lean index ec32e93ad8..0870eaa28d 100644 --- a/Linglib/Semantics/Dynamic/DRS/Dynamics.lean +++ b/Linglib/Semantics/Dynamic/DRS/Dynamics.lean @@ -131,7 +131,7 @@ theorem DRS.toRel_iff_verifies (K : DRS L V) (a a' : Embedding V M) : exact and_congr_right (fun _ => Condition.holdsAll_iff_verifies conds a') /-- A condition's set denotation agrees with its static `Verifies`. -/ theorem Condition.holds_iff_verifies (c : Condition L V) (a : Embedding V M) : - c.holds a ↔ a.VerifiesCond c := by + c.holds a ↔ a.VerifiesCondition c := by match c with | .rel R args => simp only [Condition.holds_rel, Embedding.verifies_rel] | .eq u v => simp only [Condition.holds_eq, Embedding.verifies_eq] @@ -150,7 +150,7 @@ theorem Condition.holds_iff_verifies (c : Condition L V) (a : Embedding V M) : (exists_congr (fun a' => DRS.toRel_iff_verifies r a a')) /-- The list analogue of `Condition.holds_iff_verifies`. -/ theorem Condition.holdsAll_iff_verifies (cs : List (Condition L V)) (a : Embedding V M) : - Condition.holdsAll cs a ↔ ∀ c ∈ cs, a.VerifiesCond c := by + Condition.holdsAll cs a ↔ ∀ c ∈ cs, a.VerifiesCondition c := by match cs with | [] => simp | c :: cs => diff --git a/Linglib/Semantics/Dynamic/DRS/Reduction.lean b/Linglib/Semantics/Dynamic/DRS/Reduction.lean index 4d7713a992..cc111caedc 100644 --- a/Linglib/Semantics/Dynamic/DRS/Reduction.lean +++ b/Linglib/Semantics/Dynamic/DRS/Reduction.lean @@ -159,9 +159,9 @@ theorem DRS.realize_bodyFormula [DecidableEq V] (K : DRS L V) (v : Embedding V M (DRS.bodyFormula K).Realize v ↔ v.Verifies K := by match K with | .mk _ conds => exact Condition.realize_toFormulaAll conds v -/-- A single condition's translation realizes as `VerifiesCond`. -/ +/-- A single condition's translation realizes as `VerifiesCondition`. -/ theorem Condition.realize_toFormula [DecidableEq V] (c : Condition L V) (v : Embedding V M) : - (Condition.toFormula c).Realize v ↔ v.VerifiesCond c := by + (Condition.toFormula c).Realize v ↔ v.VerifiesCondition c := by match c with | .rel R args => simp [Condition.toFormula, Relations.formula, Formula.Realize, @@ -183,7 +183,7 @@ theorem Condition.realize_toFormula [DecidableEq V] (c : Condition L V) (v : Emb their realizations. -/ theorem Condition.realize_toFormulaAll [DecidableEq V] (cs : List (Condition L V)) (v : Embedding V M) : - (Condition.toFormulaAll cs).Realize v ↔ ∀ c ∈ cs, v.VerifiesCond c := by + (Condition.toFormulaAll cs).Realize v ↔ ∀ c ∈ cs, v.VerifiesCondition c := by match cs with | [] => simp [Condition.toFormulaAll, Formula.realize_top] | c :: cs => diff --git a/Linglib/Semantics/Dynamic/DRS/Verification.lean b/Linglib/Semantics/Dynamic/DRS/Verification.lean index c74f661ebb..d1ee2070e4 100644 --- a/Linglib/Semantics/Dynamic/DRS/Verification.lean +++ b/Linglib/Semantics/Dynamic/DRS/Verification.lean @@ -8,7 +8,7 @@ mathlib `FirstOrder.Language.Structure`. An *embedding function* `f : Embedding V M` assigns discourse referents to individuals in the model; `DRS.Extends K f g` is K&R's extension relation `f [K] g` (both in `DRS/Basic.lean`); `f.Verifies K` says the embedding `f` *verifies* the DRS -`K` — it verifies every condition of `K` — and `f.VerifiesCond c` that it +`K` — it verifies every condition of `K` — and `f.VerifiesCondition c` that it verifies the DRS-condition `c`. A sub-DRS is entered by existentially (re)assigning along its extension relation. For `imp`, the consequent witness extends the *antecedent* embedding, not the host one — antecedent referents @@ -28,7 +28,7 @@ says "every man is mortal" for K&R, "if there is a man there is a mortal" here. ## Main declarations -* `Embedding.Verifies` / `Embedding.VerifiesCond` — `f.Verifies K` is the +* `Embedding.Verifies` / `Embedding.VerifiesCondition` — `f.Verifies K` is the field's "`f` verifies `K`": `f` verifies every condition of `K` (`∀ c ∈ K.conditions`, the `Theory.Model` idiom — no mutual recursion, no list helper). @@ -40,7 +40,7 @@ says "every man is mortal" for K&R, "if there is a man there is a mortal" here. ## Implementation notes -`VerifiesCond` descends into sub-DRSs through the nested +`VerifiesCondition` descends into sub-DRSs through the nested `List (Condition L V)` by well-founded recursion on `sizeOf`, so its clause characterizations (`verifies_neg`, …) are equation-lemma rewrites rather than `Iff.rfl`; they restate the clauses with `Verifies` of the sub-DRS, as the @@ -55,19 +55,19 @@ universe u v w x variable {L : Language.{u, v}} {V : Type w} {M : Type x} [L.Structure M] -/-- `f.VerifiesCond c`: the embedding `f` *verifies* the DRS-condition `c` +/-- `f.VerifiesCondition c`: the embedding `f` *verifies* the DRS-condition `c` (Def. 1.4.4(ii)); a sub-DRS is entered by existentially (re)assigning along its extension relation and verifying each of its conditions. -/ -def Embedding.VerifiesCond : Embedding V M → Condition L V → Prop +def Embedding.VerifiesCondition : Embedding V M → Condition L V → Prop | f, .rel R args => Structure.RelMap R (fun i => f (args i)) | f, .eq a b => f a = f b - | f, .neg K => ¬ ∃ g, K.Extends f g ∧ ∀ c ∈ K.conditions, g.VerifiesCond c + | f, .neg K => ¬ ∃ g, K.Extends f g ∧ ∀ c ∈ K.conditions, g.VerifiesCondition c | f, .imp a c => - ∀ g, a.Extends f g → (∀ d ∈ a.conditions, g.VerifiesCond d) → - ∃ h, c.Extends g h ∧ ∀ d ∈ c.conditions, h.VerifiesCond d + ∀ g, a.Extends f g → (∀ d ∈ a.conditions, g.VerifiesCondition d) → + ∃ h, c.Extends g h ∧ ∀ d ∈ c.conditions, h.VerifiesCondition d | f, .dis l r => - (∃ g, l.Extends f g ∧ ∀ c ∈ l.conditions, g.VerifiesCond c) ∨ - (∃ g, r.Extends f g ∧ ∀ c ∈ r.conditions, g.VerifiesCond c) + (∃ g, l.Extends f g ∧ ∀ c ∈ l.conditions, g.VerifiesCondition c) ∨ + (∃ g, r.Extends f g ∧ ∀ c ∈ r.conditions, g.VerifiesCondition c) termination_by _ c => sizeOf c decreasing_by all_goals have := DRS.sizeOf_lt_of_mem_conditions (by assumption) @@ -77,7 +77,7 @@ decreasing_by all_goals /-- `f.Verifies K`: the embedding `f` *verifies* the DRS `K` — `f` verifies every condition of `K` (Def. 1.4.4). -/ def Embedding.Verifies (f : Embedding V M) (K : DRS L V) : Prop := - ∀ c ∈ K.conditions, f.VerifiesCond c + ∀ c ∈ K.conditions, f.VerifiesCondition c namespace Embedding @@ -86,10 +86,10 @@ namespace Embedding variable {f : Embedding V M} @[simp] theorem verifies_mk (U : Finset V) (conds : List (Condition L V)) : - f.Verifies (.mk U conds) ↔ ∀ c ∈ conds, f.VerifiesCond c := Iff.rfl + f.Verifies (.mk U conds) ↔ ∀ c ∈ conds, f.VerifiesCondition c := Iff.rfl theorem verifies_iff {K : DRS L V} : - f.Verifies K ↔ ∀ c ∈ K.conditions, f.VerifiesCond c := Iff.rfl + f.Verifies K ↔ ∀ c ∈ K.conditions, f.VerifiesCondition c := Iff.rfl @[simp] theorem verifies_empty : f.Verifies (.empty : DRS L V) := by simp [DRS.empty] @@ -99,28 +99,28 @@ theorem verifies_iff {K : DRS L V} : simp only [verifies_iff, DRS.conditions_merge, List.forall_mem_append] @[simp] theorem verifies_rel {n : ℕ} (R : L.Relations n) (args : Fin n → V) : - f.VerifiesCond (.rel R args) ↔ Structure.RelMap R (fun i => f (args i)) := by - simp only [VerifiesCond] + f.VerifiesCondition (.rel R args) ↔ Structure.RelMap R (fun i => f (args i)) := by + simp only [VerifiesCondition] @[simp] theorem verifies_eq (a b : V) : - f.VerifiesCond (.eq a b : Condition L V) ↔ f a = f b := by - simp only [VerifiesCond] + f.VerifiesCondition (.eq a b : Condition L V) ↔ f a = f b := by + simp only [VerifiesCondition] @[simp] theorem verifies_neg (K : DRS L V) : - f.VerifiesCond (.neg K) ↔ ¬ ∃ g, K.Extends f g ∧ g.Verifies K := by - simp only [VerifiesCond, Verifies] + f.VerifiesCondition (.neg K) ↔ ¬ ∃ g, K.Extends f g ∧ g.Verifies K := by + simp only [VerifiesCondition, Verifies] @[simp] theorem verifies_imp (a c : DRS L V) : - f.VerifiesCond (.imp a c) ↔ + f.VerifiesCondition (.imp a c) ↔ ∀ g, a.Extends f g → g.Verifies a → ∃ h, c.Extends g h ∧ h.Verifies c := by - simp only [VerifiesCond, Verifies] + simp only [VerifiesCondition, Verifies] @[simp] theorem verifies_dis (l r : DRS L V) : - f.VerifiesCond (.dis l r) ↔ + f.VerifiesCondition (.dis l r) ↔ (∃ g, l.Extends f g ∧ g.Verifies l) ∨ (∃ g, r.Extends f g ∧ g.Verifies r) := by - simp only [VerifiesCond, Verifies] + simp only [VerifiesCondition, Verifies] /-- Verification is invariant under permutation of the conditions — the set semantics the `List`-valued `conditions` field promises (`DRS/Defs.lean`). -/ @@ -168,30 +168,30 @@ private theorem forall_precomp_extend_iff (e : V ≃ W) (U : Finset V) (f : Embe original, given the transport for each of the DRS's conditions. -/ private theorem verifies_map_all (e : V ≃ W) (K : DRS L V) (g : Embedding W M) (ih : ∀ c ∈ K.conditions, ∀ u : Embedding W M, - u.VerifiesCond (c.map e) ↔ VerifiesCond (u ∘ e) c) : + u.VerifiesCondition (c.map e) ↔ VerifiesCondition (u ∘ e) c) : g.Verifies (K.map e) ↔ Verifies (g ∘ e) K := by simp only [Verifies, DRS.conditions_map, Condition.mapList_eq_map, List.forall_mem_map] exact forall_congr' fun c => imp_congr_right fun hc => ih c hc g /-- Renaming along a bijection transports verification (the condition form of `verifies_map`). -/ -theorem verifies_map_cond (e : V ≃ W) : ∀ (f : Embedding W M) (c : Condition L V), - f.VerifiesCond (c.map e) ↔ VerifiesCond (f ∘ e) c +theorem verifies_map_condition (e : V ≃ W) : ∀ (f : Embedding W M) (c : Condition L V), + f.VerifiesCondition (c.map e) ↔ VerifiesCondition (f ∘ e) c | f, .rel R args => by simp [Condition.map, Function.comp] | f, .eq a b => by simp [Condition.map, Function.comp] | f, .neg K => by have hK := fun g : Embedding W M => - verifies_map_all e K g (fun d hd u => verifies_map_cond e u d) + verifies_map_all e K g (fun d hd u => verifies_map_condition e u d) simp only [Condition.map, verifies_neg, DRS.Extends, DRS.referents_map] exact not_congr ((exists_congr fun g => and_congr_right fun _ => hK g).trans (exists_precomp_extend_iff e K.referents f (Verifies · K))) | f, .imp a c => by have hA := fun g : Embedding W M => - verifies_map_all e a g (fun d hd u => verifies_map_cond e u d) + verifies_map_all e a g (fun d hd u => verifies_map_condition e u d) have hC := fun g : Embedding W M => - verifies_map_all e c g (fun d hd u => verifies_map_cond e u d) + verifies_map_all e c g (fun d hd u => verifies_map_condition e u d) simp only [Condition.map, verifies_imp, DRS.Extends, DRS.referents_map] refine Iff.trans (forall_congr' fun g => imp_congr_right fun _ => imp_congr (hA g) ((exists_congr fun h => and_congr_right fun _ => hC h).trans @@ -201,9 +201,9 @@ theorem verifies_map_cond (e : V ≃ W) : ∀ (f : Embedding W M) (c : Condition ∃ w'', (∀ x ∉ c.referents, w'' x = u x) ∧ Verifies w'' c) | f, .dis l r => by have hL := fun g : Embedding W M => - verifies_map_all e l g (fun d hd u => verifies_map_cond e u d) + verifies_map_all e l g (fun d hd u => verifies_map_condition e u d) have hR := fun g : Embedding W M => - verifies_map_all e r g (fun d hd u => verifies_map_cond e u d) + verifies_map_all e r g (fun d hd u => verifies_map_condition e u d) simp only [Condition.map, verifies_dis, DRS.Extends, DRS.referents_map] exact or_congr ((exists_congr fun g => and_congr_right fun _ => hL g).trans @@ -220,7 +220,7 @@ decreasing_by all_goals iff `f ∘ e` verifies `K` — alphabetic variants have the same semantics. -/ theorem verifies_map (e : V ≃ W) (f : Embedding W M) (K : DRS L V) : f.Verifies (K.map e) ↔ Verifies (f ∘ e) K := - verifies_map_all e K f (fun c _ u => verifies_map_cond e u c) + verifies_map_all e K f (fun c _ u => verifies_map_condition e u c) end Map From fbdb2cba31db78d1949a4044a2cc5069a327991a Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Fri, 7 Aug 2026 13:58:49 -0700 Subject: [PATCH 09/15] style(Semantics/Dynamic/DRS): hoist namespace Embedding above the defs --- Linglib/Semantics/Dynamic/DRS/Verification.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Linglib/Semantics/Dynamic/DRS/Verification.lean b/Linglib/Semantics/Dynamic/DRS/Verification.lean index d1ee2070e4..5ec5f9df43 100644 --- a/Linglib/Semantics/Dynamic/DRS/Verification.lean +++ b/Linglib/Semantics/Dynamic/DRS/Verification.lean @@ -55,10 +55,12 @@ universe u v w x variable {L : Language.{u, v}} {V : Type w} {M : Type x} [L.Structure M] +namespace Embedding + /-- `f.VerifiesCondition c`: the embedding `f` *verifies* the DRS-condition `c` (Def. 1.4.4(ii)); a sub-DRS is entered by existentially (re)assigning along its extension relation and verifying each of its conditions. -/ -def Embedding.VerifiesCondition : Embedding V M → Condition L V → Prop +def VerifiesCondition : Embedding V M → Condition L V → Prop | f, .rel R args => Structure.RelMap R (fun i => f (args i)) | f, .eq a b => f a = f b | f, .neg K => ¬ ∃ g, K.Extends f g ∧ ∀ c ∈ K.conditions, g.VerifiesCondition c @@ -76,11 +78,9 @@ decreasing_by all_goals /-- `f.Verifies K`: the embedding `f` *verifies* the DRS `K` — `f` verifies every condition of `K` (Def. 1.4.4). -/ -def Embedding.Verifies (f : Embedding V M) (K : DRS L V) : Prop := +def Verifies (f : Embedding V M) (K : DRS L V) : Prop := ∀ c ∈ K.conditions, f.VerifiesCondition c -namespace Embedding - /-! ### Structural simp API -/ variable {f : Embedding V M} From ecb019410041a0357880f91f72516ed41646b87d Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Fri, 7 Aug 2026 15:32:29 -0700 Subject: [PATCH 10/15] refactor(Semantics/Dynamic/DRS): extends_map API; Map section at Extends level --- Linglib/Semantics/Dynamic/DRS/Basic.lean | 44 ++++++++++++++++- .../Semantics/Dynamic/DRS/Verification.lean | 49 ++++--------------- 2 files changed, 52 insertions(+), 41 deletions(-) diff --git a/Linglib/Semantics/Dynamic/DRS/Basic.lean b/Linglib/Semantics/Dynamic/DRS/Basic.lean index 1b6c9ff435..afa618cee1 100644 --- a/Linglib/Semantics/Dynamic/DRS/Basic.lean +++ b/Linglib/Semantics/Dynamic/DRS/Basic.lean @@ -121,12 +121,54 @@ symbols — is the `L.Structure M` instance that verification need no model theory, while `f.Verifies K` only exists in a given model. -/ abbrev Embedding (V : Type w) (M : Type*) := V → M -variable {M : Type*} in +section Extends + +variable {M : Type*} + /-- `K.Extends f g` (K&R's `f [K] g`): the output embedding `g` differs from the input `f` at most on `K`'s universe — the total-assignment rendering of "`f ⊆ g` and `Dom g = Dom f ∪ U_K`". -/ def DRS.Extends (K : DRS L V) (f g : Embedding V M) : Prop := ∀ x ∉ K.referents, g x = f x +/-- Extension along a renamed DRS is extension of the precompositions. -/ +theorem DRS.extends_map [DecidableEq W] (e : V ≃ W) (K : DRS L V) (f g : Embedding W M) : + (K.map e).Extends f g ↔ K.Extends (f ∘ e) (g ∘ e) := by + simp only [DRS.Extends, DRS.referents_map, Function.comp_apply] + constructor + · intro h x hx + exact h (e x) (by simpa using hx) + · intro h y hy + have hx : e.symm y ∉ K.referents := fun hm => + hy (by simpa using Finset.mem_image_of_mem e hm) + simpa using h (e.symm y) hx + +/-- The extensions of `f` at `K.map e` are the extensions of `f ∘ e` at `K`, +via precomposition. -/ +theorem DRS.exists_extends_map [DecidableEq W] (e : V ≃ W) (K : DRS L V) (f : Embedding W M) + (P : Embedding V M → Prop) : + (∃ g, (K.map e).Extends f g ∧ P (g ∘ e)) ↔ ∃ g, K.Extends (f ∘ e) g ∧ P g := by + simp only [DRS.extends_map] + constructor + · rintro ⟨g, hg, hp⟩ + exact ⟨g ∘ e, hg, hp⟩ + · rintro ⟨g, hg, hp⟩ + have key : (g ∘ e.symm) ∘ e = g := by funext x; simp + exact ⟨g ∘ e.symm, key.symm ▸ hg, key.symm ▸ hp⟩ + +/-- The `∀` analogue of `DRS.exists_extends_map`. -/ +theorem DRS.forall_extends_map [DecidableEq W] (e : V ≃ W) (K : DRS L V) (f : Embedding W M) + (P : Embedding V M → Prop) : + (∀ g, (K.map e).Extends f g → P (g ∘ e)) ↔ ∀ g, K.Extends (f ∘ e) g → P g := by + simp only [DRS.extends_map] + constructor + · intro H g hg + have key : (g ∘ e.symm) ∘ e = g := by funext x; simp + exact key ▸ H (g ∘ e.symm) (key.symm ▸ hg) + · intro H g hg + exact H (g ∘ e) hg + +end Extends + /-! ### Occurring referents -/ section Occ diff --git a/Linglib/Semantics/Dynamic/DRS/Verification.lean b/Linglib/Semantics/Dynamic/DRS/Verification.lean index 5ec5f9df43..cd0969e1b5 100644 --- a/Linglib/Semantics/Dynamic/DRS/Verification.lean +++ b/Linglib/Semantics/Dynamic/DRS/Verification.lean @@ -134,36 +134,6 @@ section Map variable {W : Type*} [DecidableEq W] -/-- Precomposition with `e` is a bijection between the embeddings extending `f` -on `U.image e` and those extending `f ∘ e` on `U`. -/ -private theorem exists_precomp_extend_iff (e : V ≃ W) (U : Finset V) (f : Embedding W M) - (P : Embedding V M → Prop) : - (∃ g : Embedding W M, (∀ y ∉ U.image e, g y = f y) ∧ P (g ∘ e)) ↔ - ∃ w' : Embedding V M, (∀ x ∉ U, w' x = f (e x)) ∧ P w' := by - constructor - · rintro ⟨g, h, hp⟩ - exact ⟨g ∘ e, fun x hx => h (e x) (by simpa using hx), hp⟩ - · rintro ⟨w', h, hp⟩ - refine ⟨w' ∘ e.symm, fun y hy => ?_, ?_⟩ - · have hx : e.symm y ∉ U := fun hmem => hy (by simpa using Finset.mem_image_of_mem e hmem) - simpa using h _ hx - · have key : (w' ∘ e.symm) ∘ e = w' := by funext x; simp - exact key.symm ▸ hp - -/-- The `∀` analogue of `exists_precomp_extend_iff`. -/ -private theorem forall_precomp_extend_iff (e : V ≃ W) (U : Finset V) (f : Embedding W M) - (P : Embedding V M → Prop) : - (∀ g : Embedding W M, (∀ y ∉ U.image e, g y = f y) → P (g ∘ e)) ↔ - ∀ w' : Embedding V M, (∀ x ∉ U, w' x = f (e x)) → P w' := by - constructor - · intro H w' h - have key : (w' ∘ e.symm) ∘ e = w' := by funext x; simp - refine key ▸ H (w' ∘ e.symm) fun y hy => ?_ - have hx : e.symm y ∉ U := fun hmem => hy (by simpa using Finset.mem_image_of_mem e hmem) - simpa using h _ hx - · intro H g h - exact H (g ∘ e) fun x hx => h (e x) (by simpa using hx) - /-- An embedding verifies a renamed DRS iff its precomposition verifies the original, given the transport for each of the DRS's conditions. -/ private theorem verifies_map_all (e : V ≃ W) (K : DRS L V) (g : Embedding W M) @@ -184,32 +154,31 @@ theorem verifies_map_condition (e : V ≃ W) : ∀ (f : Embedding W M) (c : Cond | f, .neg K => by have hK := fun g : Embedding W M => verifies_map_all e K g (fun d hd u => verifies_map_condition e u d) - simp only [Condition.map, verifies_neg, DRS.Extends, DRS.referents_map] + simp only [Condition.map, verifies_neg] exact not_congr ((exists_congr fun g => and_congr_right fun _ => hK g).trans - (exists_precomp_extend_iff e K.referents f (Verifies · K))) + (DRS.exists_extends_map e K f (Verifies · K))) | f, .imp a c => by have hA := fun g : Embedding W M => verifies_map_all e a g (fun d hd u => verifies_map_condition e u d) have hC := fun g : Embedding W M => verifies_map_all e c g (fun d hd u => verifies_map_condition e u d) - simp only [Condition.map, verifies_imp, DRS.Extends, DRS.referents_map] + simp only [Condition.map, verifies_imp] refine Iff.trans (forall_congr' fun g => imp_congr_right fun _ => imp_congr (hA g) ((exists_congr fun h => and_congr_right fun _ => hC h).trans - (exists_precomp_extend_iff e c.referents g (Verifies · c)))) ?_ - exact forall_precomp_extend_iff e a.referents f - (fun u => Verifies u a → - ∃ w'', (∀ x ∉ c.referents, w'' x = u x) ∧ Verifies w'' c) + (DRS.exists_extends_map e c g (Verifies · c)))) ?_ + exact DRS.forall_extends_map e a f + (fun u => Verifies u a → ∃ h', c.Extends u h' ∧ Verifies h' c) | f, .dis l r => by have hL := fun g : Embedding W M => verifies_map_all e l g (fun d hd u => verifies_map_condition e u d) have hR := fun g : Embedding W M => verifies_map_all e r g (fun d hd u => verifies_map_condition e u d) - simp only [Condition.map, verifies_dis, DRS.Extends, DRS.referents_map] + simp only [Condition.map, verifies_dis] exact or_congr ((exists_congr fun g => and_congr_right fun _ => hL g).trans - (exists_precomp_extend_iff e l.referents f (Verifies · l))) + (DRS.exists_extends_map e l f (Verifies · l))) ((exists_congr fun g => and_congr_right fun _ => hR g).trans - (exists_precomp_extend_iff e r.referents f (Verifies · r))) + (DRS.exists_extends_map e r f (Verifies · r))) termination_by _ c => sizeOf c decreasing_by all_goals have := DRS.sizeOf_lt_of_mem_conditions (by assumption) From 5b57c79f5740a4aab36bb2ea044f1ef237dc7a06 Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Fri, 7 Aug 2026 15:37:48 -0700 Subject: [PATCH 11/15] style(Semantics/Dynamic/DRS): fuse have-wall into one transport lemma --- .../Semantics/Dynamic/DRS/Verification.lean | 36 +++++++++---------- 1 file changed, 17 insertions(+), 19 deletions(-) diff --git a/Linglib/Semantics/Dynamic/DRS/Verification.lean b/Linglib/Semantics/Dynamic/DRS/Verification.lean index cd0969e1b5..6ad31fe89b 100644 --- a/Linglib/Semantics/Dynamic/DRS/Verification.lean +++ b/Linglib/Semantics/Dynamic/DRS/Verification.lean @@ -143,6 +143,16 @@ private theorem verifies_map_all (e : V ≃ W) (K : DRS L V) (g : Embedding W M) simp only [Verifies, DRS.conditions_map, Condition.mapList_eq_map, List.forall_mem_map] exact forall_congr' fun c => imp_congr_right fun hc => ih c hc g +/-- "Some extension of `f` verifies `K`" transported along renaming, given the +transport for each condition of `K`. -/ +private theorem exists_extends_verifies_map (e : V ≃ W) (K : DRS L V) (f : Embedding W M) + (ih : ∀ c ∈ K.conditions, ∀ u : Embedding W M, + u.VerifiesCondition (c.map e) ↔ VerifiesCondition (u ∘ e) c) : + (∃ g, (K.map e).Extends f g ∧ g.Verifies (K.map e)) ↔ + ∃ g, K.Extends (f ∘ e) g ∧ g.Verifies K := + (exists_congr fun g => and_congr_right fun _ => verifies_map_all e K g ih).trans + (DRS.exists_extends_map e K f (Verifies · K)) + /-- Renaming along a bijection transports verification (the condition form of `verifies_map`). -/ theorem verifies_map_condition (e : V ≃ W) : ∀ (f : Embedding W M) (c : Condition L V), @@ -152,33 +162,21 @@ theorem verifies_map_condition (e : V ≃ W) : ∀ (f : Embedding W M) (c : Cond | f, .eq a b => by simp [Condition.map, Function.comp] | f, .neg K => by - have hK := fun g : Embedding W M => - verifies_map_all e K g (fun d hd u => verifies_map_condition e u d) simp only [Condition.map, verifies_neg] - exact not_congr ((exists_congr fun g => and_congr_right fun _ => hK g).trans - (DRS.exists_extends_map e K f (Verifies · K))) + exact not_congr + (exists_extends_verifies_map e K f fun d _ u => verifies_map_condition e u d) | f, .imp a c => by - have hA := fun g : Embedding W M => - verifies_map_all e a g (fun d hd u => verifies_map_condition e u d) - have hC := fun g : Embedding W M => - verifies_map_all e c g (fun d hd u => verifies_map_condition e u d) simp only [Condition.map, verifies_imp] - refine Iff.trans (forall_congr' fun g => imp_congr_right fun _ => imp_congr (hA g) - ((exists_congr fun h => and_congr_right fun _ => hC h).trans - (DRS.exists_extends_map e c g (Verifies · c)))) ?_ + refine Iff.trans (forall_congr' fun g => imp_congr_right fun _ => imp_congr + (verifies_map_all e a g fun d _ u => verifies_map_condition e u d) + (exists_extends_verifies_map e c g fun d _ u => verifies_map_condition e u d)) ?_ exact DRS.forall_extends_map e a f (fun u => Verifies u a → ∃ h', c.Extends u h' ∧ Verifies h' c) | f, .dis l r => by - have hL := fun g : Embedding W M => - verifies_map_all e l g (fun d hd u => verifies_map_condition e u d) - have hR := fun g : Embedding W M => - verifies_map_all e r g (fun d hd u => verifies_map_condition e u d) simp only [Condition.map, verifies_dis] exact or_congr - ((exists_congr fun g => and_congr_right fun _ => hL g).trans - (DRS.exists_extends_map e l f (Verifies · l))) - ((exists_congr fun g => and_congr_right fun _ => hR g).trans - (DRS.exists_extends_map e r f (Verifies · r))) + (exists_extends_verifies_map e l f fun d _ u => verifies_map_condition e u d) + (exists_extends_verifies_map e r f fun d _ u => verifies_map_condition e u d) termination_by _ c => sizeOf c decreasing_by all_goals have := DRS.sizeOf_lt_of_mem_conditions (by assumption) From 21e484e8dfbc9b1596a69c1e73872eb4b29266e0 Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Fri, 7 Aug 2026 15:40:18 -0700 Subject: [PATCH 12/15] feat(Semantics/Dynamic/DRS): trueRel_map, truth invariance of variants --- Linglib/Semantics/Dynamic/DRS/Dynamics.lean | 11 +++++++++++ Linglib/Semantics/Dynamic/DRS/Verification.lean | 17 ++++++++++++----- 2 files changed, 23 insertions(+), 5 deletions(-) diff --git a/Linglib/Semantics/Dynamic/DRS/Dynamics.lean b/Linglib/Semantics/Dynamic/DRS/Dynamics.lean index 0870eaa28d..17b265b819 100644 --- a/Linglib/Semantics/Dynamic/DRS/Dynamics.lean +++ b/Linglib/Semantics/Dynamic/DRS/Dynamics.lean @@ -36,6 +36,7 @@ identification: occurring referents (`DRS.occ`, from `DRS/Basic.lean`). * `DRS.toRel_merge` — the Merging Lemma: under freshness, `merge` denotes the spine sequencing `Update.seq` (relational composition) of the two box relations. +* `DRS.trueRel_map` — alphabetic variants have the same dynamic truth. ## Implementation notes @@ -165,6 +166,16 @@ theorem DRS.trueRel_iff_realize_toFormula [DecidableEq V] (K : DRS L V) (a : V rw [DRS.trueRel_iff, DRS.realize_toFormula K a] exact exists_congr (fun a' => DRS.toRel_iff_verifies K a a') +/-- Renaming along a bijection transports dynamic truth: alphabetic variants +have the same truth conditions. -/ +theorem DRS.trueRel_map {W : Type*} [DecidableEq V] [DecidableEq W] (e : V ≃ W) + (K : DRS L V) (a : Embedding W M) : + DRS.trueRel (K.map e) a ↔ DRS.trueRel K (a ∘ e) := by + simp only [DRS.trueRel_iff] + exact (exists_congr fun a' => DRS.toRel_iff_verifies (K.map e) a a').trans + ((Embedding.exists_extends_verifies_map e a K).trans + (exists_congr fun a' => (DRS.toRel_iff_verifies K (a ∘ e) a').symm)) + /-! ### The coincidence lemma -/ mutual diff --git a/Linglib/Semantics/Dynamic/DRS/Verification.lean b/Linglib/Semantics/Dynamic/DRS/Verification.lean index 6ad31fe89b..55500d5b2e 100644 --- a/Linglib/Semantics/Dynamic/DRS/Verification.lean +++ b/Linglib/Semantics/Dynamic/DRS/Verification.lean @@ -145,7 +145,7 @@ private theorem verifies_map_all (e : V ≃ W) (K : DRS L V) (g : Embedding W M) /-- "Some extension of `f` verifies `K`" transported along renaming, given the transport for each condition of `K`. -/ -private theorem exists_extends_verifies_map (e : V ≃ W) (K : DRS L V) (f : Embedding W M) +private theorem exists_extends_verifies_map_aux (e : V ≃ W) (K : DRS L V) (f : Embedding W M) (ih : ∀ c ∈ K.conditions, ∀ u : Embedding W M, u.VerifiesCondition (c.map e) ↔ VerifiesCondition (u ∘ e) c) : (∃ g, (K.map e).Extends f g ∧ g.Verifies (K.map e)) ↔ @@ -164,19 +164,19 @@ theorem verifies_map_condition (e : V ≃ W) : ∀ (f : Embedding W M) (c : Cond | f, .neg K => by simp only [Condition.map, verifies_neg] exact not_congr - (exists_extends_verifies_map e K f fun d _ u => verifies_map_condition e u d) + (exists_extends_verifies_map_aux e K f fun d _ u => verifies_map_condition e u d) | f, .imp a c => by simp only [Condition.map, verifies_imp] refine Iff.trans (forall_congr' fun g => imp_congr_right fun _ => imp_congr (verifies_map_all e a g fun d _ u => verifies_map_condition e u d) - (exists_extends_verifies_map e c g fun d _ u => verifies_map_condition e u d)) ?_ + (exists_extends_verifies_map_aux e c g fun d _ u => verifies_map_condition e u d)) ?_ exact DRS.forall_extends_map e a f (fun u => Verifies u a → ∃ h', c.Extends u h' ∧ Verifies h' c) | f, .dis l r => by simp only [Condition.map, verifies_dis] exact or_congr - (exists_extends_verifies_map e l f fun d _ u => verifies_map_condition e u d) - (exists_extends_verifies_map e r f fun d _ u => verifies_map_condition e u d) + (exists_extends_verifies_map_aux e l f fun d _ u => verifies_map_condition e u d) + (exists_extends_verifies_map_aux e r f fun d _ u => verifies_map_condition e u d) termination_by _ c => sizeOf c decreasing_by all_goals have := DRS.sizeOf_lt_of_mem_conditions (by assumption) @@ -189,6 +189,13 @@ theorem verifies_map (e : V ≃ W) (f : Embedding W M) (K : DRS L V) : f.Verifies (K.map e) ↔ Verifies (f ∘ e) K := verifies_map_all e K f (fun c _ u => verifies_map_condition e u c) +/-- "Some extension verifies", transported along renaming: `f` has a verifying +`K.map e`-extension iff `f ∘ e` has a verifying `K`-extension. -/ +theorem exists_extends_verifies_map (e : V ≃ W) (f : Embedding W M) (K : DRS L V) : + (∃ g, (K.map e).Extends f g ∧ g.Verifies (K.map e)) ↔ + ∃ g, K.Extends (f ∘ e) g ∧ g.Verifies K := + exists_extends_verifies_map_aux e K f fun c _ u => verifies_map_condition e u c + end Map end Embedding From 58833f58fbc5ddca57a5c50942cecef396f15571 Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Fri, 7 Aug 2026 15:41:41 -0700 Subject: [PATCH 13/15] style(Semantics/Dynamic/DRS): one-line atomic cases --- Linglib/Semantics/Dynamic/DRS/Verification.lean | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/Linglib/Semantics/Dynamic/DRS/Verification.lean b/Linglib/Semantics/Dynamic/DRS/Verification.lean index 55500d5b2e..809c007bd2 100644 --- a/Linglib/Semantics/Dynamic/DRS/Verification.lean +++ b/Linglib/Semantics/Dynamic/DRS/Verification.lean @@ -157,10 +157,8 @@ private theorem exists_extends_verifies_map_aux (e : V ≃ W) (K : DRS L V) (f : `verifies_map`). -/ theorem verifies_map_condition (e : V ≃ W) : ∀ (f : Embedding W M) (c : Condition L V), f.VerifiesCondition (c.map e) ↔ VerifiesCondition (f ∘ e) c - | f, .rel R args => by - simp [Condition.map, Function.comp] - | f, .eq a b => by - simp [Condition.map, Function.comp] + | f, .rel R args => by simp [Condition.map, Function.comp] + | f, .eq a b => by simp [Condition.map, Function.comp] | f, .neg K => by simp only [Condition.map, verifies_neg] exact not_congr From ca286e5a6ee4d93839d401fe0bc190a8cd3c3410 Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Fri, 7 Aug 2026 15:45:02 -0700 Subject: [PATCH 14/15] =?UTF-8?q?style(Semantics/Dynamic/DRS):=20derive=20?= =?UTF-8?q?=E2=88=83-corollary=20from=20the=20hom=20laws?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Linglib/Semantics/Dynamic/DRS/Verification.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Linglib/Semantics/Dynamic/DRS/Verification.lean b/Linglib/Semantics/Dynamic/DRS/Verification.lean index 809c007bd2..c9845c0308 100644 --- a/Linglib/Semantics/Dynamic/DRS/Verification.lean +++ b/Linglib/Semantics/Dynamic/DRS/Verification.lean @@ -192,7 +192,8 @@ theorem verifies_map (e : V ≃ W) (f : Embedding W M) (K : DRS L V) : theorem exists_extends_verifies_map (e : V ≃ W) (f : Embedding W M) (K : DRS L V) : (∃ g, (K.map e).Extends f g ∧ g.Verifies (K.map e)) ↔ ∃ g, K.Extends (f ∘ e) g ∧ g.Verifies K := - exists_extends_verifies_map_aux e K f fun c _ u => verifies_map_condition e u c + (exists_congr fun g => and_congr_right fun _ => verifies_map e g K).trans + (DRS.exists_extends_map e K f (Verifies · K)) end Map From a6c8448824859af4252ded158e7bb2c2b88cf419 Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Fri, 7 Aug 2026 16:11:35 -0700 Subject: [PATCH 15/15] refactor(Semantics/Dynamic/DRS): unify on SEP verification; toRel derived --- Linglib/Semantics/Dynamic/DRS/Basic.lean | 14 + Linglib/Semantics/Dynamic/DRS/Dynamics.lean | 336 ++++-------------- Linglib/Semantics/Dynamic/DRS/Indexed.lean | 69 ++-- .../Semantics/Dynamic/DRS/Verification.lean | 116 ++++++ Linglib/Studies/KampReyle1993.lean | 27 +- Linglib/Studies/Muskens1996.lean | 15 +- 6 files changed, 270 insertions(+), 307 deletions(-) diff --git a/Linglib/Semantics/Dynamic/DRS/Basic.lean b/Linglib/Semantics/Dynamic/DRS/Basic.lean index afa618cee1..f76617df43 100644 --- a/Linglib/Semantics/Dynamic/DRS/Basic.lean +++ b/Linglib/Semantics/Dynamic/DRS/Basic.lean @@ -199,6 +199,20 @@ end | nil => simp [Condition.occL] | cons c cs ih => simp [Condition.occL, ih, Finset.union_assoc] +/-- A DRS's conditions' occurring referents are among the DRS's. -/ +theorem DRS.occL_subset_occ (K : DRS L V) : Condition.occL K.conditions ⊆ K.occ := by + cases K; exact Finset.subset_union_right + +/-- A condition's occurring referents are among its list's. -/ +theorem Condition.occ_subset_occL {c : Condition L V} {cs : List (Condition L V)} + (hc : c ∈ cs) : c.occ ⊆ Condition.occL cs := by + induction cs with + | nil => cases hc + | cons d ds ih => + rcases List.mem_cons.mp hc with h | h + · exact h ▸ Finset.subset_union_left + · exact (ih h).trans Finset.subset_union_right + end Occ /-! ### Free discourse referents and properness -/ diff --git a/Linglib/Semantics/Dynamic/DRS/Dynamics.lean b/Linglib/Semantics/Dynamic/DRS/Dynamics.lean index 17b265b819..470905e87b 100644 --- a/Linglib/Semantics/Dynamic/DRS/Dynamics.lean +++ b/Linglib/Semantics/Dynamic/DRS/Dynamics.lean @@ -1,49 +1,45 @@ -import Linglib.Semantics.Dynamic.DRS.Basic +import Linglib.Semantics.Dynamic.DRS.Verification import Linglib.Semantics.Dynamic.DRS.Reduction import Linglib.Semantics.Dynamic.Update /-! -# Relational (dynamic) semantics of DRSs, and its equivalence with verifying embeddings - -[muskens-1996]'s reformulation of DRT. Conditions denote *sets* of embeddings (SEM1/2); -boxes denote *binary relations* between embeddings (SEM3, input → output, the -format of [groenendijk-stokhof-1991]); a box is true under an input embedding -`a` iff some output `a'` is related to it (p. 148). This is the dynamic / CCP -face of DRT, dual to the static verifying-embedding semantics `DRS.Verifies` — -the total-assignment rendering of [kamp-reyle-1993]'s verification (see the -deviation note in `DRS/Verification.lean`). - -The two semantics are *defined independently* and proved equivalent — Muskens's -remark that the relational interpretation "is in fact equivalent" to the -verifying-embedding one (his fn. 4 scopes the remark: both sides here are the -total-assignment variant). The equivalence is a theorem, not a definitional -identification: - -* `DRS.toRel_iff_verifies` — the relation `toRel K a a'` holds iff `a'` extends `a` - over `K`'s universe and verifies `K` (the keystone bridge). -* `DRS.trueRel_iff_realize_toFormula` — the dynamic truth of a DRS equals its - first-order translation's `Realize`, closing the triangle with `Reduction` - (`Verifies` — `toFormula` — `toRel`, each pair related by a proven theorem). +# The box relation: dynamic face of DRS verification + +The relational (input–output) face of the unified verification semantics +(`DRS/Verification.lean`): the *box relation* `K.toRel a a'` holds when the +output `a'` extends the input `a` across `K` and verifies `K`, and a DRS is +*true* under an input iff some output is related to it (the spine's anaphoric +`closure`). This is [muskens-1996]'s SEM3 format (input → output, the format +of [groenendijk-stokhof-1991]), definable in one line from verification — +Muskens's remark that his relational interpretation "is in fact equivalent" +to the standard one (his fn. 3–4 scope it: constant-free constructs, and both +sides in the total-assignment rendering; see the deviation note in +`DRS/Verification.lean`). His SEM1/2 clauses — complex conditions as the +spine connectives `neg`/`impl`/`disj` on box relations — are derived +characterizations (`verifies_neg_toRel`, …), connecting DRS verification to +the connective algebra shared across the dynamic-semantics spine. ## Main declarations -* `DRS.toRel` / `Condition.holds` — the relational (SEM3) and set (SEM1/2) - denotations. -* `DRS.trueRel` — relational truth: some output embedding is related to the input. -* `DRS.toRel_iff_verifies` / `Condition.holds_iff_verifies` — equivalence with the - static `DRS.Verifies` semantics. -* `DRS.trueRel_congr` — the coincidence lemma: denotation depends only on the - occurring referents (`DRS.occ`, from `DRS/Basic.lean`). +* `DRS.toRel` — the box relation; `DRS.trueRel` — relational truth, its + `closure`. +* `Embedding.verifies_neg_toRel` (`_imp_`, `_dis_`) — complex conditions are + the spine connectives on box relations (SEM1/2). +* `DRS.trueRel_iff_realize_toFormula` — dynamic truth equals the first-order + translation's `Realize` (`DRS/Reduction.lean`). +* `DRS.trueRel_congr` — coincidence: truth reads the input only at the + occurring referents. * `DRS.toRel_merge` — the Merging Lemma: under freshness, `merge` denotes the - spine sequencing `Update.seq` (relational composition) of the two box relations. -* `DRS.trueRel_map` — alphabetic variants have the same dynamic truth. + spine sequencing `Update.seq` of the two box relations. +* `DRS.trueRel_map` — alphabetic variants have the same truth conditions. ## Implementation notes -Naming: the dynamic face (`toRel`, `holds`, `trueRel`) follows the spine's -lowerCamel operation names (`neg`, `seq`, `closure`); the static face -(`DRS.Verifies`, `DRS/Verification.lean`) uses the field's own verb, and the -first-order reduction (`DRS/Reduction.lean`) speaks mathlib's `Formula.Realize`. +Naming: the relational face (`toRel`, `trueRel`) follows the spine's +lowerCamel operation names (`neg`, `seq`, `closure`); verification +(`Embedding.Verifies`, `DRS/Verification.lean`) uses the field's own verb, and +the first-order reduction (`DRS/Reduction.lean`) speaks mathlib's +`Formula.Realize`. -/ open FirstOrder FirstOrder.Language @@ -56,242 +52,65 @@ universe u v w x variable {L : Language.{u, v}} {V : Type w} {M : Type x} [L.Structure M] -/-! ### The relational denotation -/ +/-! ### The box relation -/ -mutual -/-- The relational (dynamic) denotation of a DRS (SEM3): the input-output -relation `⟨a, a'⟩` where `a'` differs from `a` at most on the universe and -verifies every condition. -/ -def DRS.toRel : DRS L V → Update (V → M) - | .mk U conds => fun a a' => (∀ x ∉ U, a' x = a x) ∧ Condition.holdsAll conds a' -/-- The set denotation of a condition (SEM1/2): the set of embeddings at which -it holds. Complex conditions apply the spine connectives `neg`/`impl`/`disj` -to the box relations of their sub-DRSs. -/ -def Condition.holds : Condition L V → (V → M) → Prop - | .rel R args => fun a => Structure.RelMap R (fun i => a (args i)) - | .eq u v => fun a => a u = a v - | .neg K => neg (DRS.toRel K) - | .imp ante cons => impl (DRS.toRel ante) (DRS.toRel cons) - | .dis l r => disj (DRS.toRel l) (DRS.toRel r) -/-- Every condition in the list holds at `a`. A `List` helper — the higher-order -form fails the nested-inductive structural-recursion checker. -/ -def Condition.holdsAll : List (Condition L V) → (V → M) → Prop - | [] => fun _ => True - | c :: cs => fun a => Condition.holds c a ∧ Condition.holdsAll cs a -end +/-- The box relation (SEM3): the output `a'` extends the input `a` across `K` +and verifies `K`. -/ +def DRS.toRel (K : DRS L V) : Update (V → M) := + fun a a' => K.Extends a a' ∧ Embedding.Verifies a' K + +@[simp] theorem DRS.toRel_iff (K : DRS L V) (a a' : Embedding V M) : + DRS.toRel K a a' ↔ K.Extends a a' ∧ a'.Verifies K := Iff.rfl /-- A DRS is *true* under an input embedding `a` iff some output embedding is -related to it (p. 148) — the spine's anaphoric `closure`. -/ +related to it — the spine's anaphoric `closure`. -/ def DRS.trueRel (K : DRS L V) (a : V → M) : Prop := closure (DRS.toRel K) a -/-! ### Structural simp API -/ - -@[simp] theorem DRS.toRel_mk (U : Finset V) (conds : List (Condition L V)) (a a' : V → M) : - DRS.toRel (.mk U conds) a a' ↔ - (∀ x ∉ U, a' x = a x) ∧ Condition.holdsAll conds a' := Iff.rfl - -@[simp] theorem Condition.holds_rel {n : ℕ} (R : L.Relations n) (args : Fin n → V) (a : V → M) : - (Condition.rel R args).holds a ↔ Structure.RelMap R (fun i => a (args i)) := Iff.rfl - -@[simp] theorem Condition.holds_eq (u v : V) (a : V → M) : - (Condition.eq u v : Condition L V).holds a ↔ a u = a v := Iff.rfl - -@[simp] theorem Condition.holds_neg (K : DRS L V) (a : V → M) : - (Condition.neg K).holds a ↔ ¬ ∃ a', DRS.toRel K a a' := Iff.rfl - -@[simp] theorem Condition.holds_imp (ante cons : DRS L V) (a : V → M) : - (Condition.imp ante cons).holds a ↔ - ∀ a', DRS.toRel ante a a' → ∃ a'', DRS.toRel cons a' a'' := Iff.rfl - -@[simp] theorem Condition.holds_dis (l r : DRS L V) (a : V → M) : - (Condition.dis l r).holds a ↔ ∃ a', DRS.toRel l a a' ∨ DRS.toRel r a a' := Iff.rfl - -@[simp] theorem Condition.holdsAll_nil (a : V → M) : - Condition.holdsAll ([] : List (Condition L V)) a := trivial - -@[simp] theorem Condition.holdsAll_cons (c : Condition L V) (cs : List (Condition L V)) - (a : V → M) : - Condition.holdsAll (c :: cs) a ↔ Condition.holds c a ∧ Condition.holdsAll cs a := Iff.rfl - /-- `trueRel` unfolded: some output embedding is related to the input. -/ theorem DRS.trueRel_iff (K : DRS L V) (a : V → M) : DRS.trueRel K a ↔ ∃ a', DRS.toRel K a a' := Iff.rfl -/-! ### Equivalence with the verifying-embedding semantics -/ +/-! ### The spine connectives (SEM1/2) -/ + +/-- A negated sub-DRS is the spine's `neg` of its box relation. -/ +theorem Embedding.verifies_neg_toRel (K : DRS L V) (f : Embedding V M) : + f.VerifiesCondition (.neg K) ↔ neg (DRS.toRel K) f := by + simp only [Embedding.verifies_neg]; rfl + +/-- A conditional is the spine's `impl` of the boxes' relations. -/ +theorem Embedding.verifies_imp_toRel (a c : DRS L V) (f : Embedding V M) : + f.VerifiesCondition (.imp a c) ↔ impl (DRS.toRel a) (DRS.toRel c) f := by + simp only [Embedding.verifies_imp, impl, DRS.toRel, and_imp] -mutual -/-- **SEM3 ≡ verification semantics**: the relational denotation -agrees with the static verifying-embedding semantics — `toRel K a a'` holds iff -the output `a'` extends the input `a` over `K`'s universe and verifies `K`. -(Both sides are the total-assignment variant; see `DRS/Verification.lean`.) -/ -theorem DRS.toRel_iff_verifies (K : DRS L V) (a a' : Embedding V M) : - DRS.toRel K a a' ↔ K.Extends a a' ∧ a'.Verifies K := by - match K with - | .mk U conds => - simp only [DRS.toRel, DRS.referents_mk, Embedding.verifies_mk, DRS.Extends] - exact and_congr_right (fun _ => Condition.holdsAll_iff_verifies conds a') -/-- A condition's set denotation agrees with its static `Verifies`. -/ -theorem Condition.holds_iff_verifies (c : Condition L V) (a : Embedding V M) : - c.holds a ↔ a.VerifiesCondition c := by - match c with - | .rel R args => simp only [Condition.holds_rel, Embedding.verifies_rel] - | .eq u v => simp only [Condition.holds_eq, Embedding.verifies_eq] - | .neg K => - simp only [Condition.holds_neg, Embedding.verifies_neg] - exact not_congr (exists_congr (fun a' => DRS.toRel_iff_verifies K a a')) - | .imp ante cons => - simp only [Condition.holds_imp, Embedding.verifies_imp] - refine forall_congr' (fun a' => ?_) - rw [DRS.toRel_iff_verifies ante a a', and_imp] - refine imp_congr_right (fun _ => imp_congr_right (fun _ => ?_)) - exact exists_congr (fun a'' => DRS.toRel_iff_verifies cons a' a'') - | .dis l r => - simp only [Condition.holds_dis, Embedding.verifies_dis, exists_or] - exact or_congr (exists_congr (fun a' => DRS.toRel_iff_verifies l a a')) - (exists_congr (fun a' => DRS.toRel_iff_verifies r a a')) -/-- The list analogue of `Condition.holds_iff_verifies`. -/ -theorem Condition.holdsAll_iff_verifies (cs : List (Condition L V)) (a : Embedding V M) : - Condition.holdsAll cs a ↔ ∀ c ∈ cs, a.VerifiesCondition c := by - match cs with - | [] => simp - | c :: cs => - simp only [Condition.holdsAll_cons, List.forall_mem_cons] - exact and_congr (Condition.holds_iff_verifies c a) (Condition.holdsAll_iff_verifies cs a) -end +/-- A disjunction is the spine's `disj` of the boxes' relations. -/ +theorem Embedding.verifies_dis_toRel (l r : DRS L V) (f : Embedding V M) : + f.VerifiesCondition (.dis l r) ↔ disj (DRS.toRel l) (DRS.toRel r) f := by + simp only [Embedding.verifies_dis, disj] + exact exists_or.symm + +/-! ### Truth: the triangle, coincidence, and alphabetic variants -/ /-- The dynamic truth of a DRS equals its first-order translation's `Realize` -— the third edge of the `Realize`/`toFormula`/`toRel` triangle. -/ +— the third edge of the `Verifies`/`toFormula`/`toRel` triangle. -/ theorem DRS.trueRel_iff_realize_toFormula [DecidableEq V] (K : DRS L V) (a : V → M) : - DRS.trueRel K a ↔ (K.toFormula).Realize a := by - rw [DRS.trueRel_iff, DRS.realize_toFormula K a] - exact exists_congr (fun a' => DRS.toRel_iff_verifies K a a') + DRS.trueRel K a ↔ (K.toFormula).Realize a := + (DRS.realize_toFormula K a).symm + +/-- **Coincidence**: truth reads the input embedding only at the occurring +referents. -/ +theorem DRS.trueRel_congr [DecidableEq V] {K : DRS L V} {a₁ a₂ : V → M} + (h : Set.EqOn a₁ a₂ ↑(DRS.occ K)) : DRS.trueRel K a₁ ↔ DRS.trueRel K a₂ := + Embedding.exists_extends_verifies_congr h /-- Renaming along a bijection transports dynamic truth: alphabetic variants have the same truth conditions. -/ -theorem DRS.trueRel_map {W : Type*} [DecidableEq V] [DecidableEq W] (e : V ≃ W) +theorem DRS.trueRel_map {W : Type*} [DecidableEq W] (e : V ≃ W) (K : DRS L V) (a : Embedding W M) : - DRS.trueRel (K.map e) a ↔ DRS.trueRel K (a ∘ e) := by - simp only [DRS.trueRel_iff] - exact (exists_congr fun a' => DRS.toRel_iff_verifies (K.map e) a a').trans - ((Embedding.exists_extends_verifies_map e a K).trans - (exists_congr fun a' => (DRS.toRel_iff_verifies K (a ∘ e) a').symm)) - -/-! ### The coincidence lemma -/ - -mutual -/-- **Coincidence**: a DRS's relational truth depends only on the input -embedding's values at its occurring referents. Proved by surgery on the output -witness, the load-bearing case being the `imp` clause of `Condition.holds_congr`. -/ -theorem DRS.trueRel_congr [DecidableEq V] (K : DRS L V) (a₁ a₂ : V → M) - (h : Set.EqOn a₁ a₂ ↑(DRS.occ K)) : DRS.trueRel K a₁ ↔ DRS.trueRel K a₂ := by - match K with - | .mk U conds => - simp only [DRS.trueRel_iff, DRS.toRel_mk] - have key : ∀ (b₁ b₂ : V → M), Set.EqOn b₁ b₂ ↑(DRS.occ (DRS.mk U conds)) → - (∃ a', (∀ x ∉ U, a' x = b₁ x) ∧ Condition.holdsAll conds a') → - (∃ a', (∀ x ∉ U, a' x = b₂ x) ∧ Condition.holdsAll conds a') := by - rintro b₁ b₂ hb ⟨a', hag, hh⟩ - refine ⟨(Condition.occL conds).piecewise a' b₂, ?_, ?_⟩ - · intro x hx - by_cases hxc : x ∈ Condition.occL conds - · rw [Finset.piecewise_eq_of_mem _ _ _ hxc, hag x hx] - refine hb ?_ - simp only [DRS.occ, Finset.coe_union] - exact Or.inr (Finset.mem_coe.mpr hxc) - · rw [Finset.piecewise_eq_of_notMem _ _ _ hxc] - · refine (Condition.holdsAll_congr conds _ a' ?_).mpr hh - intro x hx - exact Finset.piecewise_eq_of_mem _ _ _ (Finset.mem_coe.mp hx) - exact ⟨key a₁ a₂ h, key a₂ a₁ h.symm⟩ -/-- A condition's set denotation depends only on its occurring referents. -/ -theorem Condition.holds_congr [DecidableEq V] (c : Condition L V) (a₁ a₂ : V → M) - (h : Set.EqOn a₁ a₂ ↑(Condition.occ c)) : Condition.holds c a₁ ↔ Condition.holds c a₂ := by - match c with - | .rel R args => - simp only [Condition.holds] - have : (fun i => a₁ (args i)) = (fun i => a₂ (args i)) := by - funext i; refine h ?_; simp [Condition.occ] - rw [this] - | .eq u v => - simp only [Condition.holds] - rw [h (show u ∈ ↑(Condition.occ (Condition.eq u v)) by simp [Condition.occ]), - h (show v ∈ ↑(Condition.occ (Condition.eq u v)) by simp [Condition.occ])] - | .neg K => - simp only [Condition.holds_neg] - have hk := DRS.trueRel_congr K a₁ a₂ h - simp only [DRS.trueRel_iff] at hk - rw [hk] - | .imp ante cons => - simp only [Condition.holds_imp] - have hante : ∀ (b₁ b₂ : V → M), Set.EqOn b₁ b₂ ↑(Condition.occ (Condition.imp ante cons)) → - (∀ a', DRS.toRel ante b₁ a' → ∃ a'', DRS.toRel cons a' a'') → - (∀ a', DRS.toRel ante b₂ a' → ∃ a'', DRS.toRel cons a' a'') := by - rintro b₁ b₂ hb hL a' ha' - cases ante with - | mk Ua condsa => - obtain ⟨hag, hh⟩ := ha' - have hset : DRS.occ (DRS.mk Ua condsa) ∪ DRS.occ cons = - Condition.occ (Condition.imp (DRS.mk Ua condsa) cons) := by - simp [Condition.occ] - have hagree : Set.EqOn - ((DRS.occ (DRS.mk Ua condsa) ∪ DRS.occ cons).piecewise a' b₁) a' - ↑(DRS.occ cons) := by - intro x hx - exact Finset.piecewise_eq_of_mem _ _ _ - (Finset.mem_union_right _ (Finset.mem_coe.mp hx)) - have hr₁ : DRS.toRel (DRS.mk Ua condsa) b₁ - ((DRS.occ (DRS.mk Ua condsa) ∪ DRS.occ cons).piecewise a' b₁) := by - refine ⟨?_, ?_⟩ - · intro x hx - by_cases hxS : x ∈ DRS.occ (DRS.mk Ua condsa) ∪ DRS.occ cons - · rw [Finset.piecewise_eq_of_mem _ _ _ hxS, hag x hx] - exact (hb (Finset.mem_coe.mpr (hset ▸ hxS))).symm - · rw [Finset.piecewise_eq_of_notMem _ _ _ hxS] - · refine (Condition.holdsAll_congr condsa _ a' ?_).mpr hh - intro x hx - refine Finset.piecewise_eq_of_mem _ _ _ (Finset.mem_union_left _ ?_) - simp only [DRS.occ] - exact Finset.mem_union_right _ (Finset.mem_coe.mp hx) - obtain ⟨a₄, ha₄⟩ := hL _ hr₁ - have hcc := DRS.trueRel_congr cons _ a' hagree - simp only [DRS.trueRel_iff] at hcc - exact hcc.mp ⟨a₄, ha₄⟩ - exact ⟨hante a₁ a₂ h, hante a₂ a₁ h.symm⟩ - | .dis l r => - simp only [Condition.holds_dis, exists_or] - have hsub : ↑(DRS.occ l) ⊆ ↑(Condition.occ (Condition.dis l r)) := - Finset.coe_subset.mpr Finset.subset_union_left - have hsubr : ↑(DRS.occ r) ⊆ ↑(Condition.occ (Condition.dis l r)) := - Finset.coe_subset.mpr Finset.subset_union_right - have hl := DRS.trueRel_congr l a₁ a₂ (h.mono hsub) - have hr := DRS.trueRel_congr r a₁ a₂ (h.mono hsubr) - simp only [DRS.trueRel_iff] at hl hr - rw [hl, hr] -/-- The list analogue of `Condition.holds_congr`. -/ -theorem Condition.holdsAll_congr [DecidableEq V] (cs : List (Condition L V)) (a₁ a₂ : V → M) - (h : Set.EqOn a₁ a₂ ↑(Condition.occL cs)) : - Condition.holdsAll cs a₁ ↔ Condition.holdsAll cs a₂ := by - match cs with - | [] => exact Iff.rfl - | c :: cs => - simp only [Condition.holdsAll_cons] - have hsub : ↑(Condition.occ c) ⊆ ↑(Condition.occL (c :: cs)) := - Finset.coe_subset.mpr Finset.subset_union_left - have hsubr : ↑(Condition.occL cs) ⊆ ↑(Condition.occL (c :: cs)) := - Finset.coe_subset.mpr Finset.subset_union_right - exact and_congr (Condition.holds_congr c a₁ a₂ (h.mono hsub)) - (Condition.holdsAll_congr cs a₁ a₂ (h.mono hsubr)) -end + DRS.trueRel (K.map e) a ↔ DRS.trueRel K (a ∘ e) := + Embedding.exists_extends_verifies_map e a K /-! ### The merging lemma: sequencing is merge, under freshness -/ -/-- The conjunction of conditions distributes over list append. -/ -@[simp] theorem Condition.holdsAll_append (cs ds : List (Condition L V)) (a : V → M) : - Condition.holdsAll (cs ++ ds) a ↔ Condition.holdsAll cs a ∧ Condition.holdsAll ds a := by - induction cs with - | nil => simp [Condition.holdsAll] - | cons c cs ih => simp only [List.cons_append, Condition.holdsAll, ih, and_assoc] - /-- **Merging Lemma** (§II.2): when `K₂`'s universe is fresh for `K₁`'s conditions, the merge `K₁ ⊕ K₂` denotes the spine sequencing (relational composition) of the two box relations — `‖K₁ ⊕ K₂‖ = seq ‖K₁‖ ‖K₂‖`. @@ -304,8 +123,8 @@ theorem DRS.toRel_merge [DecidableEq V] (K₁ K₂ : DRS L V) simp only [DRS.referents_mk, DRS.conditions_mk, Finset.disjoint_left] at hfresh funext a a' apply propext - simp only [DRS.merge, DRS.referents_mk, DRS.conditions_mk, DRS.toRel, - Condition.holdsAll_append, seq, Relation.Comp] + simp only [DRS.toRel, DRS.Extends, DRS.merge, DRS.referents_mk, DRS.conditions_mk, + Embedding.verifies_mk, List.forall_mem_append, seq, Relation.Comp] constructor · rintro ⟨hag, hh₁, hh₂⟩ refine ⟨U₂.piecewise a a', ⟨?_, ?_⟩, ?_, ?_⟩ @@ -316,10 +135,10 @@ theorem DRS.toRel_merge [DecidableEq V] (K₁ K₂ : DRS L V) refine hag x ?_ rw [Finset.mem_union, not_or] exact ⟨hx, hxU2⟩ - · refine (Condition.holdsAll_congr conds₁ _ a' ?_).mpr hh₁ - intro x hx + · intro c hc + refine (Embedding.verifiesCondition_congr c fun x hx => ?_).mpr (hh₁ c hc) exact Finset.piecewise_eq_of_notMem _ _ _ - (fun h => hfresh h (Finset.mem_coe.mp hx)) + (fun hU => hfresh hU (Condition.occ_subset_occL hc (Finset.mem_coe.mp hx))) · intro x hx exact (Finset.piecewise_eq_of_notMem _ _ _ hx).symm · exact hh₂ @@ -328,7 +147,8 @@ theorem DRS.toRel_merge [DecidableEq V] (K₁ K₂ : DRS L V) · intro x hx rw [Finset.mem_union, not_or] at hx rw [hag2 x hx.2, hag1 x hx.1] - · exact (Condition.holdsAll_congr conds₁ a' a'' - (fun x hx => hag2 x (fun hu => hfresh hu (Finset.mem_coe.mp hx)))).mpr hh1 + · intro c hc + refine (Embedding.verifiesCondition_congr c fun x hx => ?_).mpr (hh1 c hc) + exact hag2 x fun hU => hfresh hU (Condition.occ_subset_occL hc (Finset.mem_coe.mp hx)) end DRT diff --git a/Linglib/Semantics/Dynamic/DRS/Indexed.lean b/Linglib/Semantics/Dynamic/DRS/Indexed.lean index 85f0de0e09..c21f7293ae 100644 --- a/Linglib/Semantics/Dynamic/DRS/Indexed.lean +++ b/Linglib/Semantics/Dynamic/DRS/Indexed.lean @@ -509,7 +509,8 @@ diverge (Muskens's fn. 4; witness in `Studies/Muskens1996.lean`). -/ to agreement on a disjoint base. -/ private theorem DRS.toRelAt_of_toRel' {X U : Finset V} {conds : List (Condition L V)} (hXU : Disjoint X U) - (hIH : ∀ k : V → M, Condition.holdsAll conds k ↔ Condition.holdsAllAt (X ∪ U) conds k) + (hIH : ∀ k : V → M, (∀ c ∈ conds, Embedding.VerifiesCondition k c) ↔ + Condition.holdsAllAt (X ∪ U) conds k) {g g' : V → M} (h : DRS.toRel (.mk U conds) g g') : DRS.toRelAt X (.mk U conds) g g' := by obtain ⟨hag, hh⟩ := h @@ -520,7 +521,8 @@ private theorem DRS.toRelAt_of_toRel' {X U : Finset V} {conds : List (Condition the input's values. -/ private theorem DRS.toRel_of_toRelAt' {X U : Finset V} {conds : List (Condition L V)} (hfvc : Condition.fvL conds ⊆ X ∪ U) - (hIH : ∀ k : V → M, Condition.holdsAll conds k ↔ Condition.holdsAllAt (X ∪ U) conds k) + (hIH : ∀ k : V → M, (∀ c ∈ conds, Embedding.VerifiesCondition k c) ↔ + Condition.holdsAllAt (X ∪ U) conds k) {g g' : V → M} (h : DRS.toRelAt X (.mk U conds) g g') : DRS.toRel (.mk U conds) g (fun x => if x ∈ U then g' x else g x) ∧ Set.EqOn (fun x => if x ∈ U then g' x else g x) g' ↑(X ∪ U) := by @@ -541,21 +543,21 @@ private theorem DRS.toRel_of_toRelAt' {X U : Finset V} {conds : List (Condition mutual /-- On a reuse-free condition with free referents in the base, the flat set denotation and the indexed one coincide. -/ -theorem Condition.holds_iff_holdsAt {X : Finset V} (c : Condition L V) +theorem Condition.verifies_iff_holdsAt {X : Finset V} (c : Condition L V) (hrf : Condition.ReuseFreeAt X c) (hfv : c.fv ⊆ X) (g : V → M) : - Condition.holds c g ↔ Condition.holdsAt X c g := by + Embedding.VerifiesCondition g c ↔ Condition.holdsAt X c g := by match c with - | .rel R args => exact Iff.rfl - | .eq u v => exact Iff.rfl + | .rel R args => simp only [Embedding.verifies_rel, Condition.holdsAt_rel] + | .eq u v => simp only [Embedding.verifies_eq, Condition.holdsAt_eq] | .neg K => obtain ⟨U, conds⟩ := K simp only [Condition.reuseFreeAt_neg, DRS.reuseFreeAt_mk] at hrf rw [Condition.fv_neg] at hfv have hfvc := DRS.fv_subset_iff.mp hfv - have hIH : ∀ k : V → M, Condition.holdsAll conds k ↔ + have hIH : ∀ k : V → M, (∀ c ∈ conds, Embedding.VerifiesCondition k c) ↔ Condition.holdsAllAt (X ∪ U) conds k := - fun k => Condition.holdsAll_iff_holdsAllAt conds hrf.2 hfvc k - simp only [Condition.holds_neg, Condition.holdsAt_neg] + fun k => Condition.verifiesAll_iff_holdsAllAt conds hrf.2 hfvc k + simp only [Embedding.verifies_neg, Condition.holdsAt_neg] exact not_congr ⟨fun ⟨k, hk⟩ => ⟨k, DRS.toRelAt_of_toRel' hrf.1 hIH hk⟩, fun ⟨k, hk⟩ => ⟨_, (DRS.toRel_of_toRelAt' hfvc hIH hk).1⟩⟩ | .imp a c' => @@ -575,21 +577,21 @@ theorem Condition.holds_iff_holdsAt {X : Finset V} (c : Condition L V) · refine Finset.mem_union_left _ (Finset.mem_union_left _ (hfvc' ?_)) rw [DRS.fv_mk, DRS.referents_mk, Finset.mem_sdiff, Finset.mem_sdiff] exact ⟨⟨hx, hxUc⟩, hxUa⟩ - have hIHa : ∀ k : V → M, Condition.holdsAll ca k ↔ + have hIHa : ∀ k : V → M, (∀ c ∈ ca, Embedding.VerifiesCondition k c) ↔ Condition.holdsAllAt (X ∪ Ua) ca k := - fun k => Condition.holdsAll_iff_holdsAllAt ca hrfa hfvca k - have hIHc : ∀ k : V → M, Condition.holdsAll cc k ↔ + fun k => Condition.verifiesAll_iff_holdsAllAt ca hrfa hfvca k + have hIHc : ∀ k : V → M, (∀ c ∈ cc, Embedding.VerifiesCondition k c) ↔ Condition.holdsAllAt ((X ∪ Ua) ∪ Uc) cc k := - fun k => Condition.holdsAll_iff_holdsAllAt cc hrfc hfvcc k - simp only [Condition.holds_imp, Condition.holdsAt_imp, DRS.referents_mk] + fun k => Condition.verifiesAll_iff_holdsAllAt cc hrfc hfvcc k + simp only [Embedding.verifies_imp, Condition.holdsAt_imp, DRS.referents_mk] constructor · intro hL g₁ hg₁ obtain ⟨hflat, heq⟩ := DRS.toRel_of_toRelAt' hfvca hIHa hg₁ - obtain ⟨g₂, hg₂⟩ := hL _ hflat + obtain ⟨g₂, hg₂⟩ := hL _ hflat.1 hflat.2 exact ⟨g₂, (DRS.toRelAt_congr_left (X ∪ Ua) _ heq).mp (DRS.toRelAt_of_toRel' hXUc hIHc hg₂)⟩ - · intro hR g₁ hg₁ - obtain ⟨g₂, hg₂⟩ := hR g₁ (DRS.toRelAt_of_toRel' hXUa hIHa hg₁) + · intro hR g₁ hg₁ hv₁ + obtain ⟨g₂, hg₂⟩ := hR g₁ (DRS.toRelAt_of_toRel' hXUa hIHa ⟨hg₁, hv₁⟩) exact ⟨_, (DRS.toRel_of_toRelAt' hfvcc hIHc hg₂).1⟩ | .dis l r => obtain ⟨Ul, cl⟩ := l @@ -599,31 +601,32 @@ theorem Condition.holds_iff_holdsAt {X : Finset V} (c : Condition L V) rw [Condition.fv_dis, Finset.union_subset_iff] at hfv have hfvcl : Condition.fvL cl ⊆ X ∪ Ul := DRS.fv_subset_iff.mp hfv.1 have hfvcr : Condition.fvL cr ⊆ X ∪ Ur := DRS.fv_subset_iff.mp hfv.2 - have hIHl : ∀ k : V → M, Condition.holdsAll cl k ↔ + have hIHl : ∀ k : V → M, (∀ c ∈ cl, Embedding.VerifiesCondition k c) ↔ Condition.holdsAllAt (X ∪ Ul) cl k := - fun k => Condition.holdsAll_iff_holdsAllAt cl hrfl hfvcl k - have hIHr : ∀ k : V → M, Condition.holdsAll cr k ↔ + fun k => Condition.verifiesAll_iff_holdsAllAt cl hrfl hfvcl k + have hIHr : ∀ k : V → M, (∀ c ∈ cr, Embedding.VerifiesCondition k c) ↔ Condition.holdsAllAt (X ∪ Ur) cr k := - fun k => Condition.holdsAll_iff_holdsAllAt cr hrfr hfvcr k - simp only [Condition.holds_dis, Condition.holdsAt_dis] + fun k => Condition.verifiesAll_iff_holdsAllAt cr hrfr hfvcr k + simp only [Embedding.verifies_dis, Condition.holdsAt_dis] constructor - · rintro ⟨k, hk | hk⟩ + · rintro (⟨k, hk⟩ | ⟨k, hk⟩) · exact ⟨k, Or.inl (DRS.toRelAt_of_toRel' hXUl hIHl hk)⟩ · exact ⟨k, Or.inr (DRS.toRelAt_of_toRel' hXUr hIHr hk)⟩ · rintro ⟨k, hk | hk⟩ - · exact ⟨_, Or.inl (DRS.toRel_of_toRelAt' hfvcl hIHl hk).1⟩ - · exact ⟨_, Or.inr (DRS.toRel_of_toRelAt' hfvcr hIHr hk).1⟩ -/-- The list analogue of `Condition.holds_iff_holdsAt`. -/ -theorem Condition.holdsAll_iff_holdsAllAt {X : Finset V} (cs : List (Condition L V)) + · exact Or.inl ⟨_, (DRS.toRel_of_toRelAt' hfvcl hIHl hk).1⟩ + · exact Or.inr ⟨_, (DRS.toRel_of_toRelAt' hfvcr hIHr hk).1⟩ +/-- The list analogue of `Condition.verifies_iff_holdsAt`. -/ +theorem Condition.verifiesAll_iff_holdsAllAt {X : Finset V} (cs : List (Condition L V)) (hrf : Condition.ReuseFreeAllAt X cs) (hfv : Condition.fvL cs ⊆ X) (g : V → M) : - Condition.holdsAll cs g ↔ Condition.holdsAllAt X cs g := by + (∀ c ∈ cs, Embedding.VerifiesCondition g c) ↔ Condition.holdsAllAt X cs g := by match cs with - | [] => exact Iff.rfl + | [] => simp | c :: cs => simp only [Condition.reuseFreeAllAt_cons] at hrf rw [Condition.fvL_cons, Finset.union_subset_iff] at hfv - exact and_congr (Condition.holds_iff_holdsAt c hrf.1 hfv.1 g) - (Condition.holdsAll_iff_holdsAllAt cs hrf.2 hfv.2 g) + simp only [List.forall_mem_cons, Condition.holdsAllAt_cons] + exact and_congr (Condition.verifies_iff_holdsAt c hrf.1 hfv.1 g) + (Condition.verifiesAll_iff_holdsAllAt cs hrf.2 hfv.2 g) end /-- Flat-to-indexed: on a reuse-free DRS every flat output is a indexed output. -/ @@ -632,7 +635,7 @@ theorem DRS.toRelAt_of_toRel {X : Finset V} {K : DRS L V} (hrf : DRS.ReuseFreeAt obtain ⟨U, conds⟩ := K simp only [DRS.reuseFreeAt_mk] at hrf exact DRS.toRelAt_of_toRel' hrf.1 - (fun k => Condition.holdsAll_iff_holdsAllAt conds hrf.2 (DRS.fv_subset_iff.mp hfv) k) h + (fun k => Condition.verifiesAll_iff_holdsAllAt conds hrf.2 (DRS.fv_subset_iff.mp hfv) k) h /-- Indexed-to-flat: on a reuse-free DRS a indexed output repairs, off the grown base, into a flat output. -/ @@ -642,7 +645,7 @@ theorem DRS.toRel_of_toRelAt {X : Finset V} {K : DRS L V} (hrf : DRS.ReuseFreeAt obtain ⟨U, conds⟩ := K simp only [DRS.reuseFreeAt_mk] at hrf exact ⟨_, DRS.toRel_of_toRelAt' (DRS.fv_subset_iff.mp hfv) - (fun k => Condition.holdsAll_iff_holdsAllAt conds hrf.2 (DRS.fv_subset_iff.mp hfv) k) h⟩ + (fun k => Condition.verifiesAll_iff_holdsAllAt conds hrf.2 (DRS.fv_subset_iff.mp hfv) k) h⟩ /-- **Truth-level reconciliation** (Muskens's fn. 4): on a reuse-free DRS the flat total-assignment semantics and the indexed persistence semantics diff --git a/Linglib/Semantics/Dynamic/DRS/Verification.lean b/Linglib/Semantics/Dynamic/DRS/Verification.lean index c9845c0308..dfc2e1515e 100644 --- a/Linglib/Semantics/Dynamic/DRS/Verification.lean +++ b/Linglib/Semantics/Dynamic/DRS/Verification.lean @@ -197,6 +197,122 @@ theorem exists_extends_verifies_map (e : V ≃ W) (f : Embedding W M) (K : DRS L end Map +/-! ### Coincidence -/ + +section Coincidence + +variable [DecidableEq V] + +/-- "Some extension of `f₁` verifies `K`" survives changing `f₁` at +non-occurring referents, given coincidence for each condition of `K`. -/ +private theorem exists_extends_verifies_congr_aux (K : DRS L V) {f₁ f₂ : Embedding V M} + (h : Set.EqOn f₁ f₂ ↑K.occ) + (ih : ∀ c ∈ K.conditions, ∀ g₁ g₂ : Embedding V M, + Set.EqOn g₁ g₂ ↑(Condition.occ c) → (g₁.VerifiesCondition c ↔ g₂.VerifiesCondition c)) : + (∃ g, K.Extends f₁ g ∧ g.Verifies K) → ∃ g, K.Extends f₂ g ∧ g.Verifies K := by + obtain ⟨U, conds⟩ := K + rintro ⟨g, hag, hh⟩ + refine ⟨(Condition.occL conds).piecewise g f₂, ?_, ?_⟩ + · intro x hx + by_cases hxc : x ∈ Condition.occL conds + · rw [Finset.piecewise_eq_of_mem _ _ _ hxc, hag x hx] + refine h ?_ + simp only [DRS.occ, Finset.coe_union] + exact Or.inr (Finset.mem_coe.mpr hxc) + · rw [Finset.piecewise_eq_of_notMem _ _ _ hxc] + · intro c hc + refine (ih c hc _ g fun x hx => ?_).mpr (hh c hc) + exact Finset.piecewise_eq_of_mem _ _ _ + (Condition.occ_subset_occL hc (Finset.mem_coe.mp hx)) + +/-- Verification of a condition reads the embedding only at its occurring +referents. -/ +theorem verifiesCondition_congr : ∀ (c : Condition L V) {f₁ f₂ : Embedding V M}, + Set.EqOn f₁ f₂ ↑(Condition.occ c) → (f₁.VerifiesCondition c ↔ f₂.VerifiesCondition c) + | .rel R args, f₁, f₂, h => by + simp only [verifies_rel] + rw [show (fun i => f₁ (args i)) = fun i => f₂ (args i) from + funext fun i => h (by simp [Condition.occ])] + | .eq a b, f₁, f₂, h => by + simp only [verifies_eq] + rw [h (show a ∈ ↑(Condition.occ (.eq a b : Condition L V)) by simp [Condition.occ]), + h (show b ∈ ↑(Condition.occ (.eq a b : Condition L V)) by simp [Condition.occ])] + | .neg K, f₁, f₂, h => by + simp only [verifies_neg] + exact not_congr + ⟨exists_extends_verifies_congr_aux K h + fun d _ g₁ g₂ hg => verifiesCondition_congr d hg, + exists_extends_verifies_congr_aux K h.symm + fun d _ g₁ g₂ hg => verifiesCondition_congr d hg⟩ + | .imp a c, f₁, f₂, h => by + simp only [verifies_imp] + have key : ∀ b₁ b₂ : Embedding V M, + Set.EqOn b₁ b₂ ↑(Condition.occ (.imp a c)) → + (∀ g, a.Extends b₁ g → g.Verifies a → + ∃ h', c.Extends g h' ∧ h'.Verifies c) → + ∀ g, a.Extends b₂ g → g.Verifies a → + ∃ h', c.Extends g h' ∧ h'.Verifies c := by + rintro b₁ b₂ hb hL g hag hv + have hpg : Set.EqOn ((DRS.occ a ∪ DRS.occ c).piecewise g b₁) g ↑(DRS.occ a) := + fun x hx => + Finset.piecewise_eq_of_mem _ _ _ (Finset.mem_union_left _ (Finset.mem_coe.mp hx)) + have hExt : a.Extends b₁ ((DRS.occ a ∪ DRS.occ c).piecewise g b₁) := by + intro x hx + by_cases hxS : x ∈ DRS.occ a ∪ DRS.occ c + · rw [Finset.piecewise_eq_of_mem _ _ _ hxS, hag x hx] + exact (hb (Finset.mem_coe.mpr hxS)).symm + · rw [Finset.piecewise_eq_of_notMem _ _ _ hxS] + have hVer : Verifies ((DRS.occ a ∪ DRS.occ c).piecewise g b₁) a := fun d hd => + (verifiesCondition_congr d (hpg.mono (Finset.coe_subset.mpr + ((Condition.occ_subset_occL hd).trans (DRS.occL_subset_occ a))))).mpr (hv d hd) + obtain ⟨h', hch', hvh'⟩ := hL _ hExt hVer + have hpc : Set.EqOn ((DRS.occ a ∪ DRS.occ c).piecewise g b₁) g ↑(DRS.occ c) := + fun x hx => + Finset.piecewise_eq_of_mem _ _ _ (Finset.mem_union_right _ (Finset.mem_coe.mp hx)) + exact exists_extends_verifies_congr_aux c hpc + (fun d _ g₁ g₂ hg => verifiesCondition_congr d hg) ⟨h', hch', hvh'⟩ + exact ⟨key f₁ f₂ h, key f₂ f₁ h.symm⟩ + | .dis l r, f₁, f₂, h => by + simp only [verifies_dis] + have hl : Set.EqOn f₁ f₂ ↑(DRS.occ l) := + h.mono (by simp only [Condition.occ, Finset.coe_union]; exact Set.subset_union_left) + have hr : Set.EqOn f₁ f₂ ↑(DRS.occ r) := + h.mono (by simp only [Condition.occ, Finset.coe_union]; exact Set.subset_union_right) + exact or_congr + ⟨exists_extends_verifies_congr_aux l hl + fun d _ g₁ g₂ hg => verifiesCondition_congr d hg, + exists_extends_verifies_congr_aux l hl.symm + fun d _ g₁ g₂ hg => verifiesCondition_congr d hg⟩ + ⟨exists_extends_verifies_congr_aux r hr + fun d _ g₁ g₂ hg => verifiesCondition_congr d hg, + exists_extends_verifies_congr_aux r hr.symm + fun d _ g₁ g₂ hg => verifiesCondition_congr d hg⟩ +termination_by c => sizeOf c +decreasing_by all_goals + have := DRS.sizeOf_lt_of_mem_conditions (by assumption) + simp_wf + omega + +/-- Verification reads the embedding only at the DRS's occurring referents. -/ +theorem verifies_congr {K : DRS L V} {f₁ f₂ : Embedding V M} + (h : Set.EqOn f₁ f₂ ↑K.occ) : f₁.Verifies K ↔ f₂.Verifies K := by + simp only [verifies_iff] + exact forall_congr' fun c => imp_congr_right fun hc => + verifiesCondition_congr c (h.mono (Finset.coe_subset.mpr + ((Condition.occ_subset_occL hc).trans (DRS.occL_subset_occ K)))) + +/-- "Some extension verifies" reads the input embedding only at the occurring +referents. -/ +theorem exists_extends_verifies_congr {K : DRS L V} {f₁ f₂ : Embedding V M} + (h : Set.EqOn f₁ f₂ ↑K.occ) : + (∃ g, K.Extends f₁ g ∧ g.Verifies K) ↔ ∃ g, K.Extends f₂ g ∧ g.Verifies K := + ⟨exists_extends_verifies_congr_aux K h + fun c _ _ _ hg => verifiesCondition_congr c hg, + exists_extends_verifies_congr_aux K h.symm + fun c _ _ _ hg => verifiesCondition_congr c hg⟩ + +end Coincidence + end Embedding end DRT diff --git a/Linglib/Studies/KampReyle1993.lean b/Linglib/Studies/KampReyle1993.lean index f116a4a92e..f1057fe3e8 100644 --- a/Linglib/Studies/KampReyle1993.lean +++ b/Linglib/Studies/KampReyle1993.lean @@ -59,7 +59,7 @@ abbrev rm {n} (R : krLang.Relations n) (x : Fin n → M) : Prop := Structure.Rel /-- Reindex a composed vector argument componentwise: with `comp_vecEmpty`, folds `fun i => v (![k₁, …] i)` to `![v k₁, …]`, so truth-condition proofs work with the -atoms' assigned values directly. Point-ful because `Condition.holds_rel` produces +atoms' assigned values directly. Point-ful because `Embedding.verifies_rel` produces the eta-expanded form, which the point-free mathlib lemmas (`Fin.comp_cons`, `FinVec.map_eq`) do not match. -/ private theorem comp_vecCons {α β : Type*} (v : α → β) (k : α) {n : ℕ} (t : Fin n → α) : @@ -83,8 +83,9 @@ def persistence : DRS krLang ℕ := that is a man, walked in, and sat down. -/ theorem persistence_tc (a : ℕ → M) : DRS.trueRel persistence a ↔ ∃ e : M, rm .man ![e] ∧ rm .walkedIn ![e] ∧ rm .satDown ![e] := by - simp only [DRS.trueRel_iff, persistence, DRS.toRel_mk, Condition.holdsAll_cons, - Condition.holdsAll_nil, Condition.holds_rel, comp_vecCons, comp_vecEmpty, and_true] + simp only [DRS.trueRel_iff, persistence, DRS.toRel_iff, DRS.Extends, DRS.referents_mk, + Embedding.verifies_mk, List.forall_mem_cons, List.not_mem_nil, false_implies, + implies_true, Embedding.verifies_rel, comp_vecCons, comp_vecEmpty, and_true] constructor · rintro ⟨a', _, hm, hw, hs⟩; exact ⟨a' 1, hm, hw, hs⟩ · rintro ⟨e, hm, hw, hs⟩ @@ -112,21 +113,22 @@ theorem donkey_universal_reading (a : ℕ → M) : DRS.trueRel donkey a ↔ ∀ e₁ e₂ : M, (rm .farmer ![e₁] ∧ rm .donkey ![e₂] ∧ rm .owns ![e₁, e₂]) → rm .beats ![e₁, e₂] := by - simp only [DRS.trueRel_iff, donkey, donkeyAnte, donkeyCons, DRS.toRel_mk, - Condition.holdsAll_cons, Condition.holdsAll_nil, Condition.holds_imp, Condition.holds_rel, + simp only [DRS.trueRel_iff, donkey, donkeyAnte, donkeyCons, DRS.toRel_iff, DRS.Extends, + DRS.referents_mk, Embedding.verifies_mk, List.forall_mem_cons, List.not_mem_nil, + false_implies, implies_true, Embedding.verifies_imp, Embedding.verifies_rel, comp_vecCons, comp_vecEmpty, and_true] constructor · rintro ⟨a', _, himp⟩ e₁ e₂ ⟨hf, hd, ho⟩ set v' := Function.update (Function.update a' 1 e₁) 2 e₂ with hv' have h1 : v' 1 = e₁ := by simp [hv', Function.update_of_ne, Function.update_self] have h2 : v' 2 = e₂ := by simp [hv', Function.update_self] - obtain ⟨v'', hag, hb⟩ := himp v' ⟨fun x hx => by + obtain ⟨v'', hag, hb⟩ := himp v' (fun x hx => by simp only [Finset.mem_insert, Finset.mem_singleton, not_or] at hx - simp [hv', Function.update_of_ne hx.1, Function.update_of_ne hx.2], - by rw [h1]; exact hf, by rw [h2]; exact hd, by rw [h1, h2]; exact ho⟩ + simp [hv', Function.update_of_ne hx.1, Function.update_of_ne hx.2]) + ⟨by rw [h1]; exact hf, by rw [h2]; exact hd, by rw [h1, h2]; exact ho⟩ simpa [hag 1 (by simp), hag 2 (by simp), h1, h2] using hb · intro hall - exact ⟨a, fun _ _ => rfl, fun v' ⟨_, hf, hd, ho⟩ => + exact ⟨a, fun _ _ => rfl, fun v' _ ⟨hf, hd, ho⟩ => ⟨v', fun _ _ => rfl, hall (v' 1) (v' 2) ⟨hf, hd, ho⟩⟩⟩ /-! ### Negation blocks anaphora -/ @@ -139,9 +141,10 @@ def negation : DRS krLang ℕ := .mk ∅ [.neg negInner] is bound inside the negation and inaccessible to any continuation. -/ theorem negation_tc (a : ℕ → M) : DRS.trueRel negation a ↔ ¬ ∃ e : M, rm .man ![e] ∧ rm .walkedIn ![e] := by - simp only [DRS.trueRel_iff, negation, negInner, DRS.toRel_mk, Condition.holdsAll_cons, - Condition.holdsAll_nil, Condition.holds_neg, Condition.holds_rel, comp_vecCons, - comp_vecEmpty, and_true] + simp only [DRS.trueRel_iff, negation, negInner, DRS.toRel_iff, DRS.Extends, + DRS.referents_mk, Embedding.verifies_mk, List.forall_mem_cons, List.not_mem_nil, + false_implies, implies_true, Embedding.verifies_neg, Embedding.verifies_rel, + comp_vecCons, comp_vecEmpty, and_true] constructor · rintro ⟨a', _, hneg⟩ ⟨e, hm, hw⟩ exact hneg ⟨Function.update a' 1 e, fun x hx => by diff --git a/Linglib/Studies/Muskens1996.lean b/Linglib/Studies/Muskens1996.lean index facd3877cf..9495d203c5 100644 --- a/Linglib/Studies/Muskens1996.lean +++ b/Linglib/Studies/Muskens1996.lean @@ -380,11 +380,18 @@ theorem fn4_not_reuseFreeAt : ¬ DRS.ReuseFreeAt ∅ fn4 := by /-- Flat truth: every input verifies the witness — the re-declared referent may be reassigned, so it suffices that some mortal exist. -/ theorem fn4_trueRel (g : ℕ → Fin 2) : DRS.trueRel fn4 g := by - refine ⟨g, fun x _ => rfl, ?_, trivial⟩ - rw [Condition.holds_imp] - intro g₁ _ + refine ⟨g, fun x _ => rfl, ?_⟩ + intro c hc + simp only [fn4, DRS.conditions_mk, List.mem_singleton] at hc + subst hc + rw [Embedding.verifies_imp] + intro g₁ _ _ refine ⟨Function.update g₁ 0 1, - fun x hx => by rw [Function.update_apply, if_neg (by simpa [fn4Cons] using hx)], ?_, trivial⟩ + fun x hx => by rw [Function.update_apply, if_neg (by simpa [fn4Cons] using hx)], ?_⟩ + intro c hc + simp only [fn4Cons, DRS.conditions_mk, List.mem_singleton] at hc + subst hc + rw [Embedding.verifies_rel] show Function.update g₁ 0 1 0 = 1 simp