DRS structural API: functorial renaming and merge algebra

[KR93]

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's alphabetic variant (Def. 1.4.7); map_id makes "renaming to the identity is the identity" a free corollary.
• merge algebra — identity (empty) and associativity.

Functorial renaming

def DRT.DRS.map {L : FirstOrder.Language} {V : Type w} {W : Type x} [DecidableEq W] (f : V → W) : DRS L V → DRS L W

Rename discourse referents along f : V → W throughout a DRS.

Equations

• DRT.DRS.map f (DRT.DRS.mk refs conds) = DRT.DRS.mk (Finset.image f refs) (DRT.Condition.mapList f conds)

def DRT.Condition.map {L : FirstOrder.Language} {V : Type w} {W : Type x} [DecidableEq W] (f : V → W) : Condition L V → Condition L W

Rename discourse referents along f throughout a condition.

Equations

• DRT.Condition.map f (DRT.Condition.rel R args) = DRT.Condition.rel R fun (i : Fin n) => f (args i)
• DRT.Condition.map f (DRT.Condition.eq a b) = DRT.Condition.eq (f a) (f b)
• DRT.Condition.map f (DRT.Condition.neg K) = DRT.Condition.neg (DRT.DRS.map f K)
• DRT.Condition.map f (DRT.Condition.imp a c) = DRT.Condition.imp (DRT.DRS.map f a) (DRT.DRS.map f c)
• DRT.Condition.map f (DRT.Condition.dis l r) = DRT.Condition.dis (DRT.DRS.map f l) (DRT.DRS.map f r)

def DRT.Condition.mapList {L : FirstOrder.Language} {V : Type w} {W : Type x} [DecidableEq W] (f : V → W) : List (Condition L V) → List (Condition L W)

Rename along f throughout a list of conditions. A List helper (not conds.map (Condition.map f)) because the higher-order form fails the nested-inductive structural-recursion checker.

Equations

• DRT.Condition.mapList f [] = []
• DRT.Condition.mapList f (c :: cs) = DRT.Condition.map f c :: DRT.Condition.mapList f cs

@[simp]

theorem DRT.DRS.map_id {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (K : DRS L V) : map id K = K

Renaming along the identity is the identity.

@[simp]

theorem DRT.Condition.map_id {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (c : Condition L V) : map id c = c

Renaming a condition along the identity is the identity.

theorem DRT.Condition.mapList_id {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (cs : List (Condition L V)) : mapList id cs = cs

Merge algebra

@[simp]

theorem DRT.DRS.empty_merge {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (K : DRS L V) : empty.merge K = K

@[simp]

theorem DRT.DRS.merge_empty {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (K : DRS L V) : K.merge empty = K

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

Properness (no free discourse referent)

def DRT.DRS.Bound {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (b : Finset V) : DRS L V → Prop

Bound b K: every discourse referent occurring in K is bound — present in b or introduced by K's universe or by an ancestor reachable "left and up" (the antecedent of a ⇒ threads its referents into the consequent).

Equations

• DRT.DRS.Bound b (DRT.DRS.mk refs conds) = DRT.Condition.BoundAll (b ∪ refs) conds

def DRT.Condition.Bound {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (b : Finset V) : Condition L V → Prop

b-boundedness of a condition.

Equations

• DRT.Condition.Bound b (DRT.Condition.rel R args) = ∀ (i : Fin n), args i ∈ b
• DRT.Condition.Bound b (DRT.Condition.eq a b_1) = (a ∈ b ∧ b_1 ∈ b)
• DRT.Condition.Bound b (DRT.Condition.neg K) = DRT.DRS.Bound b K
• DRT.Condition.Bound b (DRT.Condition.imp a c) = (DRT.DRS.Bound b a ∧ DRT.DRS.Bound (b ∪ a.referents) c)
• DRT.Condition.Bound b (DRT.Condition.dis l r) = (DRT.DRS.Bound b l ∧ DRT.DRS.Bound b r)

def DRT.Condition.BoundAll {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (b : Finset V) : List (Condition L V) → Prop

b-boundedness of a list of conditions. A List helper (not List.Forall (Condition.Bound b)) — the higher-order form fails the nested-inductive structural-recursion checker.

Equations

• DRT.Condition.BoundAll b [] = True
• DRT.Condition.BoundAll b (c :: cs) = (DRT.Condition.Bound b c ∧ DRT.Condition.BoundAll b cs)

def DRT.DRS.IsProper {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (K : DRS L V) : Prop

A DRS is proper iff it has no free discourse referent ([KR93], Def. 1.4.2–1.4.3): every occurring referent is bound at its position.

Equations

• K.IsProper = DRT.DRS.Bound ∅ K

Occurring referents

def DRT.Condition.occ {L : FirstOrder.Language} {V : Type w} [DecidableEq V] : Condition L V → Finset V

Occurring referents (free or bound) in a condition, as a Finset — the DRS analogue of mathlib's Term.varFinset. Membership x ∈ occ c is decidable, so downstream consumers get decidable occurrence for free.

Equations

• (DRT.Condition.rel R args).occ = Finset.image args Finset.univ
• (DRT.Condition.eq a b).occ = {a, b}
• (DRT.Condition.neg K).occ = K.occ
• (DRT.Condition.imp a c).occ = a.occ ∪ c.occ
• (DRT.Condition.dis l r).occ = l.occ ∪ r.occ

def DRT.DRS.occ {L : FirstOrder.Language} {V : Type w} [DecidableEq V] : DRS L V → Finset V

Occurring referents in a DRS (its universe and those of its conditions).

Equations

• (DRT.DRS.mk refs conds).occ = refs ∪ DRT.Condition.occL conds

def DRT.Condition.occL {L : FirstOrder.Language} {V : Type w} [DecidableEq V] : List (Condition L V) → Finset V

Occurring referents in a list of conditions.

Equations

• DRT.Condition.occL [] = ∅
• DRT.Condition.occL (c :: cs) = c.occ ∪ DRT.Condition.occL cs

Accessibility (decidable, host-relative)

Accessibility ([KR93], Def. 1.4.11) is intrinsically relative to a host DRS: "u accessible at box B" means u lies in the universe of B or of a box on the path from the host down to B. A host-free ∃ D, WeakSubordinate K D ∧ u ∈ D.referents is vacuous — a superordinate D introducing any referent can always be manufactured. So accessibility is computed top-down, threading the in-scope referents (the same threading as DRS.Bound), which is also decidable.

def DRT.DRS.accScope {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (s : Finset V) : DRS L V → V → Option (Finset V)

Descend T, accumulating in-scope referents s ("left and up"); on reaching the box introducing x, return that box's in-scope set s ∪ U. The ⇒-consequent additionally sees the antecedent's universe.

Equations

• DRT.DRS.accScope s (DRT.DRS.mk U conds) x✝ = if x✝ ∈ U then some (s ∪ U) else DRT.Condition.accScopeL (s ∪ U) conds x✝

def DRT.Condition.accScope {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (s : Finset V) : Condition L V → V → Option (Finset V)

Accessibility threading through a condition.

Equations

• DRT.Condition.accScope s (DRT.Condition.rel R args) x✝ = none
• DRT.Condition.accScope s (DRT.Condition.eq u v) x✝ = none
• DRT.Condition.accScope s (DRT.Condition.neg K) x✝ = DRT.DRS.accScope s K x✝
• DRT.Condition.accScope s (DRT.Condition.imp a c) x✝ = match DRT.DRS.accScope s a x✝ with | some r => some r | none => DRT.DRS.accScope (s ∪ a.referents) c x✝
• DRT.Condition.accScope s (DRT.Condition.dis l r) x✝ = match DRT.DRS.accScope s l x✝ with | some r => some r | none => DRT.DRS.accScope s r x✝

def DRT.Condition.accScopeL {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (s : Finset V) : List (Condition L V) → V → Option (Finset V)

Accessibility threading through a list of conditions (mutual helper).

Equations

• DRT.Condition.accScopeL s [] x✝ = none
• DRT.Condition.accScopeL s (c :: cs) x✝ = match DRT.Condition.accScope s c x✝ with | some r => some r | none => DRT.Condition.accScopeL s cs x✝

def DRT.DRS.accessibleFrom {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (T : DRS L V) (u : V) : Finset V

The referents accessible from u's introduction in T ([KR93], Def. 1.4.11), as a decidable Finset; ∅ if u is not introduced in T.

Equations

• T.accessibleFrom u = (DRT.DRS.accScope ∅ T u).getD ∅

def DRT.DRS.Accessible {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (T : DRS L V) (u v : V) : Prop

v is accessible from u's position in T. Decidable (Finset membership).

Equations

• T.Accessible u v = (v ∈ T.accessibleFrom u)

@[implicit_reducible]

instance DRT.instDecidableAccessible {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (T : DRS L V) (u v : V) : Decidable (T.Accessible u v)

Equations

• DRT.instDecidableAccessible T u v = DRT.instDecidableAccessible._aux_1 T u v