Discourse representation structures

This file defines discourse representation structures (DRSs) over a mathlib FirstOrder.Language, following [KR93]. A DRS is a pair of a finite set of discourse referents (the textbook's universe U) and a list of conditions (Def. 1.4.1); a condition is atomic (rel, eq) or complex (neg, with imp/dis from the Chapter 2 extension), and sub-DRSs occur only inside complex conditions. In the literature a DRS is also drawn as a box, [Mus96]'s [u₁ … uₙ | γ₁ … γₘ].

Verification and truth are model-theoretic and live in DRS/Verification.lean; the structural theory is in DRS/Basic.lean.

Main declarations

• Condition, DRS: conditions and DRSs over a language L and referent type V; DRS L V is the generic container Box (DRS/Box.lean) instantiated at Condition L V.
• DRS.merge: the merge ⊕ — union the referents, append the conditions ([Mus96]).
• DirectlySubordinate, Subordinate, WeakSubordinate: immediate subordination and its transitive and reflexive-transitive closures (Def. 1.4.10, Def. 2.1.2). Accessibility is host-relative and lives in DRS/Basic.lean (AccessibleTo, accessibleFrom).

Main statements

• WeakSubordinate.antisymm: weak subordination is a partial order.

Implementation notes

• referents is the textbook U; universe is a Lean keyword and univ collides with Finset.univ.
• Box is a container structure the condition syntax nests through, and DRS its instantiation at Condition L V — Def. 1.4.1's simultaneous recursion without a mutual block, keeping the structure API.
• conditions is a List, since an inductive cannot nest through Finset/Multiset; set semantics is recovered by the interpretation (Embedding.verifies_perm, DRS/Verification.lean).
• DRT is the owning namespace, on the FirstOrder.Language pattern.

inductive DRT.Condition (L : FirstOrder.Language) (V : Type w) : Type (max v w)

A DRS-condition: atomic (rel, eq) or complex — neg per Def. 1.4.1, imp/dis per its Chapter 2 extension. Sub-DRSs occur only inside complex conditions.

• rel {L : FirstOrder.Language} {V : Type w} {n : ℕ} (R : L.Relations n) (args : Fin n → V) : Condition L V

  Atomic condition: n-ary relation symbol R applied to referents args.

• eq {L : FirstOrder.Language} {V : Type w} (u v : V) : Condition L V

  Atomic equality condition u = v.

• neg {L : FirstOrder.Language} {V : Type w} (K : Box V (Condition L V)) : Condition L V

  Complex condition ¬K.

• imp {L : FirstOrder.Language} {V : Type w} (ante cons : Box V (Condition L V)) : Condition L V

  Complex condition K₁ ⇒ K₂ (antecedent ⇒ consequent).

• dis {L : FirstOrder.Language} {V : Type w} (left right : Box V (Condition L V)) : Condition L V

  Complex condition K₁ ∨ K₂.

@[reducible, inline]

abbrev DRT.DRS (L : FirstOrder.Language) (V : Type w) : Type (max w w v)

A discourse representation structure consists of two parts: a universe of discourse referents, which represent the objects under discussion, and the DRS-conditions, which encode the information that has accumulated on them (Def. 1.4.1).

Equations

• DRT.DRS L V = DRT.Box V (DRT.Condition L V)

@[simp]

theorem DRT.DRS.referents_mk {L : FirstOrder.Language} {V : Type w} (u : Finset V) (c : List (Condition L V)) : { referents := u, conditions := c }.referents = u

@[simp]

theorem DRT.DRS.conditions_mk {L : FirstOrder.Language} {V : Type w} (u : Finset V) (c : List (Condition L V)) : { referents := u, conditions := c }.conditions = c

def DRT.DRS.empty {L : FirstOrder.Language} {V : Type w} : DRS L V

The empty DRS ⟨∅, []⟩.

Equations

• DRT.DRS.empty = { referents := ∅, conditions := [] }

@[instance_reducible]

instance DRT.DRS.instInhabited {L : FirstOrder.Language} {V : Type w} : Inhabited (DRS L V)

Equations

• DRT.DRS.instInhabited = { default := DRT.DRS.empty }

def DRT.DRS.merge {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (K₁ K₂ : DRS L V) : DRS L V

The merge K₁ ⊕ K₂ unions the referents and appends the conditions — [Mus96]'s compositional operation (Kamp & Reyle combine DRSs incrementally via the construction algorithm instead). An operation, not a syntactic constructor.

Equations

• K₁.merge K₂ = { referents := K₁.referents ∪ K₂.referents, conditions := K₁.conditions ++ K₂.conditions }

@[simp]

theorem DRT.DRS.referents_merge {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (K₁ K₂ : DRS L V) : (K₁.merge K₂).referents = K₁.referents ∪ K₂.referents

@[simp]

theorem DRT.DRS.conditions_merge {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (K₁ K₂ : DRS L V) : (K₁.merge K₂).conditions = K₁.conditions ++ K₂.conditions

theorem DRT.Condition.induction {L : FirstOrder.Language} {V : Type w} {motive : Condition L V → Prop} (rel : ∀ {n : ℕ} (R : L.Relations n) (args : Fin n → V), motive (rel R args)) (eq : ∀ (u v : V), motive (eq u v)) (neg : ∀ (K : Box V (Condition L V)), (∀ c ∈ K.conditions, motive c) → motive (neg K)) (imp : ∀ (a c : Box V (Condition L V)), (∀ d ∈ a.conditions, motive d) → (∀ d ∈ c.conditions, motive d) → motive (imp a c)) (dis : ∀ (l r : Box V (Condition L V)), (∀ d ∈ l.conditions, motive d) → (∀ d ∈ r.conditions, motive d) → motive (dis l r)) (c : Condition L V) : motive c

Induction on conditions, descending into sub-boxes: to prove motive c for every condition, handle each constructor given the motive for every condition of its sub-boxes.

Subordination

inductive DRT.DirectlySubordinate {L : FirstOrder.Language} {V : Type w} : DRS L V → DRS L V → Prop

DirectlySubordinate K' K says K' is a sub-box of one of K's conditions — the neg case per Def. 1.4.10(i), the ⇒/∨ cases per its Chapter 2 extension (Def. 2.1.2, which subordinates both components of a conditional to the containing DRS). A relation on DRS values, where the textbook's is on box occurrences. Every clause pins the containing box in its conclusion: an unpinned clause (such as consequent-below-antecedent) would hold of every pair of DRSs via a manufactured container, collapsing the relation. The ⇒ visibility asymmetry is not subordination but accessibility (AccessibleTo, DRS/Basic.lean).

• neg {L : FirstOrder.Language} {V : Type w} {D K : DRS L V} : Condition.neg K ∈ D.conditions → DirectlySubordinate K D

  The body of a ¬ is directly subordinate to the containing DRS.

• impAnte {L : FirstOrder.Language} {V : Type w} {D a c : DRS L V} : Condition.imp a c ∈ D.conditions → DirectlySubordinate a D

  The antecedent of a ⇒ is directly subordinate to the containing DRS.

• impCons {L : FirstOrder.Language} {V : Type w} {D a c : DRS L V} : Condition.imp a c ∈ D.conditions → DirectlySubordinate c D

  The consequent of a ⇒ is directly subordinate to the containing DRS.

• disL {L : FirstOrder.Language} {V : Type w} {D l r : DRS L V} : Condition.dis l r ∈ D.conditions → DirectlySubordinate l D

  The left disjunct of a ∨ is directly subordinate to the containing DRS.

• disR {L : FirstOrder.Language} {V : Type w} {D l r : DRS L V} : Condition.dis l r ∈ D.conditions → DirectlySubordinate r D

  The right disjunct of a ∨ is directly subordinate to the containing DRS.

@[reducible, inline]

abbrev DRT.Subordinate {L : FirstOrder.Language} {V : Type w} : DRS L V → DRS L V → Prop

The < of Def. 1.4.10(ii): the transitive closure of DirectlySubordinate.

Equations

• DRT.Subordinate = Relation.TransGen DRT.DirectlySubordinate

@[reducible, inline]

abbrev DRT.WeakSubordinate {L : FirstOrder.Language} {V : Type w} : DRS L V → DRS L V → Prop

The ≤ of Def. 1.4.10(ii): the reflexive-transitive closure of DirectlySubordinate.

Equations

• DRT.WeakSubordinate = Relation.ReflTransGen DRT.DirectlySubordinate

theorem DRT.DirectlySubordinate.sizeOf_lt {L : FirstOrder.Language} {V : Type w} {K' K : DRS L V} (h : DirectlySubordinate K' K) : sizeOf K' < sizeOf K

A directly subordinate DRS is a structurally smaller value.

theorem DRT.Subordinate.sizeOf_lt {L : FirstOrder.Language} {V : Type w} {K' K : DRS L V} (h : Subordinate K' K) : sizeOf K' < sizeOf K

Subordinate DRSs are structurally smaller; subordination chains terminate.

theorem DRT.Subordinate.irrefl {L : FirstOrder.Language} {V : Type w} (K : DRS L V) : ¬Subordinate K K

theorem DRT.WeakSubordinate.antisymm {L : FirstOrder.Language} {V : Type w} {K' K : DRS L V} (h : WeakSubordinate K' K) (h' : WeakSubordinate K K') : K' = K

Weak subordination is a partial order on DRS values.