Structural operations on DRSs

This file develops the structural theory of the DRSs of DRS/Defs.lean, namely the renaming of discourse referents, the merge algebra, the transport of the extension relation along renaming, and occurring and free referents. Renaming along a bijection gives Kamp and Reyle's alphabetic variants (the prose preceding Def. 1.4.8).

Main declarations

• DRS.map: renaming along f : V → W, functorial.
• DRS.varFinset, DRS.freeVarFinset: occurring and free referents.
• DRS.IsProper: no free referent (Def. 1.4.2–1.4.3); decidable.
• DRS.ReuseFreeAt: no referent declared twice along a nesting path.

Main statements

• DRS.isProper_merge: merging a proper DRS with an increment whose free referents it declares is proper.

Implementation notes

Renaming, occurring and free referents, and reuse-freeness are each three mutually recursive functions, on DRSs, conditions and condition lists, by structural recursion through the nesting, so the kernel evaluates them and decide settles them on concrete DRSs.

References

• [KR93]

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

K.map f renames the discourse referents of K along f.

Equations

• DRT.DRS.map f { referents := U, conditions := cs } = { referents := Finset.image f U, conditions := DRT.Condition.mapList f cs }

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

c.map f renames the discourse referents of c along f.

Equations

• DRT.Condition.map f (DRT.Condition.atom a) = DRT.Condition.atom (FirstOrder.Language.Atom.map f a)
• 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)

Condition.mapList f cs renames each condition of cs along f.

Equations

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

@[simp]

theorem DRT.Condition.mapList_eq_map {L : FirstOrder.Language} {V : Type w} {W : Type x} [DecidableEq W] (f : V → W) (cs : List (Condition L V)) : mapList f cs = List.map (map f) cs

@[simp]

theorem DRT.DRS.referents_map {L : FirstOrder.Language} {V : Type w} {W : Type x} [DecidableEq W] (f : V → W) (K : DRS L V) : (map f K).referents = Finset.image f K.referents

@[simp]

theorem DRT.DRS.conditions_map {L : FirstOrder.Language} {V : Type w} {W : Type x} [DecidableEq W] (f : V → W) (K : DRS L V) : (map f K).conditions = List.map (Condition.map f) K.conditions

@[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.map_map {L : FirstOrder.Language} {V : Type w} {W : Type x} {X : Type u_2} [DecidableEq W] [DecidableEq X] (g : W → X) (f : V → W) (c : Condition L V) : map g (map f c) = map (g ∘ f) c

Renaming a condition along a composite is the composite of the renamings.

Renaming and extension

theorem DRT.DRS.extends_map {L : FirstOrder.Language} {V : Type w} {W : Type x} {M : Type u_1} [DecidableEq W] (e : V ≃ W) (K : DRS L V) (f g : W → M) : Box.Extends (map (⇑e) K) f g ↔ Box.Extends K (f ∘ ⇑e) (g ∘ ⇑e)

Extension along a renamed DRS is extension of the precompositions.

theorem DRT.DRS.exists_extends_map {L : FirstOrder.Language} {V : Type w} {W : Type x} {M : Type u_1} [DecidableEq W] (e : V ≃ W) (K : DRS L V) (f : W → M) (P : (V → M) → Prop) : (∃ (g : W → M), Box.Extends (map (⇑e) K) f g ∧ P (g ∘ ⇑e)) ↔ ∃ (g : V → M), Box.Extends K (f ∘ ⇑e) g ∧ P g

The extensions of f at K.map e are the extensions of f ∘ e at K, via precomposition.

theorem DRT.DRS.forall_extends_map {L : FirstOrder.Language} {V : Type w} {W : Type x} {M : Type u_1} [DecidableEq W] (e : V ≃ W) (K : DRS L V) (f : W → M) (P : (V → M) → Prop) : (∀ (g : W → M), Box.Extends (map (⇑e) K) f g → P (g ∘ ⇑e)) ↔ ∀ (g : V → M), Box.Extends K (f ∘ ⇑e) g → P g

The ∀ analogue of DRS.exists_extends_map.

@[simp]

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

Renaming a DRS along the identity is the identity.

theorem DRT.DRS.map_map {L : FirstOrder.Language} {V : Type w} {W : Type x} {X : Type u_2} [DecidableEq W] [DecidableEq X] (g : W → X) (f : V → W) (K : DRS L V) : map g (map f K) = map (g ∘ f) K

Renaming a DRS along a composite is the composite of the renamings.

Occurring and free referents

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

The occurring referents of a DRS are its universe and those of its conditions.

Equations

• DRT.DRS.varFinset { referents := U, conditions := cs } = U ∪ DRT.Condition.varFinsetL cs

def DRT.Condition.varFinset {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.

Equations

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

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

Occurring referents in a list of conditions.

Equations

• DRT.Condition.varFinsetL [] = ∅
• DRT.Condition.varFinsetL (c :: cs) = c.varFinset ∪ DRT.Condition.varFinsetL cs

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

The free discourse referents of a DRS occur in its conditions and are bound neither by its universe nor by an ancestor reachable "left and up" (the antecedent of a ⇒ threads its referents into the consequent). K.freeVarFinset ⊆ b says every referent of K is bound in context b.

Equations

• DRT.DRS.freeVarFinset { referents := U, conditions := cs } = DRT.Condition.freeVarFinsetL cs \ U

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

The free discourse referents of a condition (Def. 1.4.2); the consequent of a ⇒ also has the antecedent's universe bound.

Equations

• (DRT.Condition.atom a).freeVarFinset = Finset.image a.args Finset.univ
• (DRT.Condition.eq a b).freeVarFinset = {a, b}
• (DRT.Condition.neg K).freeVarFinset = DRT.DRS.freeVarFinset K
• (DRT.Condition.imp a c).freeVarFinset = DRT.DRS.freeVarFinset a ∪ DRT.DRS.freeVarFinset c \ a.referents
• (DRT.Condition.dis l r).freeVarFinset = DRT.DRS.freeVarFinset l ∪ DRT.DRS.freeVarFinset r

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

Free referents of a list of conditions.

Equations

• DRT.Condition.freeVarFinsetL [] = ∅
• DRT.Condition.freeVarFinsetL (c :: cs) = c.freeVarFinset ∪ DRT.Condition.freeVarFinsetL cs

@[simp]

theorem DRT.Condition.varFinsetL_nil {L : FirstOrder.Language} {V : Type w} [DecidableEq V] : varFinsetL [] = ∅

@[simp]

theorem DRT.Condition.varFinsetL_cons {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (c : Condition L V) (cs : List (Condition L V)) : varFinsetL (c :: cs) = c.varFinset ∪ varFinsetL cs

@[simp]

theorem DRT.Condition.varFinset_atom {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (a : L.Atom V) : (atom a).varFinset = Finset.image a.args Finset.univ

@[simp]

theorem DRT.Condition.varFinset_eq {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (u v : V) : (eq u v).varFinset = {u, v}

@[simp]

theorem DRT.Condition.varFinset_neg {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (K : DRS L V) : (neg K).varFinset = K.varFinset

@[simp]

theorem DRT.Condition.varFinset_imp {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (a c : DRS L V) : (imp a c).varFinset = a.varFinset ∪ c.varFinset

@[simp]

theorem DRT.Condition.varFinset_dis {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (l r : DRS L V) : (dis l r).varFinset = l.varFinset ∪ r.varFinset

@[simp]

theorem DRT.Condition.varFinsetL_append {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (cs ds : List (Condition L V)) : varFinsetL (cs ++ ds) = varFinsetL cs ∪ varFinsetL ds

theorem DRT.Condition.varFinset_subset_varFinsetL {L : FirstOrder.Language} {V : Type w} [DecidableEq V] {c : Condition L V} {cs : List (Condition L V)} (hc : c ∈ cs) : c.varFinset ⊆ varFinsetL cs

A condition's occurring referents are among its list's.

@[simp]

theorem DRT.Condition.freeVarFinsetL_nil {L : FirstOrder.Language} {V : Type w} [DecidableEq V] : freeVarFinsetL [] = ∅

@[simp]

theorem DRT.Condition.freeVarFinsetL_cons {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (c : Condition L V) (cs : List (Condition L V)) : freeVarFinsetL (c :: cs) = c.freeVarFinset ∪ freeVarFinsetL cs

@[simp]

theorem DRT.Condition.freeVarFinset_atom {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (a : L.Atom V) : (atom a).freeVarFinset = Finset.image a.args Finset.univ

@[simp]

theorem DRT.Condition.freeVarFinset_eq {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (u v : V) : (eq u v).freeVarFinset = {u, v}

@[simp]

theorem DRT.Condition.freeVarFinset_neg {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (K : DRS L V) : (neg K).freeVarFinset = K.freeVarFinset

@[simp]

theorem DRT.Condition.freeVarFinset_imp {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (a c : DRS L V) : (imp a c).freeVarFinset = a.freeVarFinset ∪ c.freeVarFinset \ a.referents

@[simp]

theorem DRT.Condition.freeVarFinset_dis {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (l r : DRS L V) : (dis l r).freeVarFinset = l.freeVarFinset ∪ r.freeVarFinset

@[simp]

theorem DRT.Condition.freeVarFinsetL_append {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (cs ds : List (Condition L V)) : freeVarFinsetL (cs ++ ds) = freeVarFinsetL cs ∪ freeVarFinsetL ds

theorem DRT.Condition.freeVarFinset_subset_freeVarFinsetL {L : FirstOrder.Language} {V : Type w} [DecidableEq V] {c : Condition L V} {cs : List (Condition L V)} (hc : c ∈ cs) : c.freeVarFinset ⊆ freeVarFinsetL cs

A condition's free referents are among its list's.

@[simp]

theorem DRT.DRS.varFinset_mk {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (U : Finset V) (conds : List (Condition L V)) : varFinset { referents := U, conditions := conds } = U ∪ Condition.varFinsetL conds

theorem DRT.DRS.varFinset_eq {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (K : DRS L V) : K.varFinset = K.referents ∪ Condition.varFinsetL K.conditions

theorem DRT.DRS.varFinsetL_subset_varFinset {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (K : DRS L V) : Condition.varFinsetL K.conditions ⊆ K.varFinset

A DRS's conditions' occurring referents are among the DRS's.

@[simp]

theorem DRT.DRS.freeVarFinset_mk {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (U : Finset V) (conds : List (Condition L V)) : freeVarFinset { referents := U, conditions := conds } = Condition.freeVarFinsetL conds \ U

theorem DRT.DRS.freeVarFinset_eq {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (K : DRS L V) : K.freeVarFinset = Condition.freeVarFinsetL K.conditions \ K.referents

theorem DRT.DRS.coe_freeVarFinset {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (K : DRS L V) : ↑K.freeVarFinset = ↑(Condition.freeVarFinsetL K.conditions) \ ↑K.referents

theorem DRT.DRS.freeVarFinset_subset_iff {L : FirstOrder.Language} {V : Type w} [DecidableEq V] {U X : Finset V} {conds : List (Condition L V)} : freeVarFinset { referents := U, conditions := conds } ⊆ X ↔ Condition.freeVarFinsetL conds ⊆ X ∪ U

A box's free referents are supplied by X iff its conditions' are supplied by the grown base, the characteristic form of the referential presupposition.

theorem DRT.Condition.freeVarFinset_subset_varFinset {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (c : Condition L V) : c.freeVarFinset ⊆ c.varFinset

Free referents of a condition occur.

theorem DRT.DRS.freeVarFinset_subset_varFinset {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (K : DRS L V) : K.freeVarFinset ⊆ K.varFinset

Free referents occur.

theorem DRT.Condition.freeVarFinsetL_subset_varFinsetL {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (cs : List (Condition L V)) : freeVarFinsetL cs ⊆ varFinsetL cs

The list analogue of Condition.freeVarFinset_subset_varFinset.

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₃)

theorem DRT.DRS.freeVarFinset_merge_subset {L : FirstOrder.Language} {V : Type w} [DecidableEq V] {X : Finset V} {K₁ K₂ : DRS L V} (h₁ : K₁.freeVarFinset ⊆ X) (h₂ : K₂.freeVarFinset ⊆ X ∪ K₁.referents) : (K₁.merge K₂).freeVarFinset ⊆ X

A merge's free referents are supplied by X when the context's are and the increment's are supplied by the grown base.

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 (Def. 1.4.2–1.4.3).

Equations

• K.IsProper = (K.freeVarFinset = ∅)

@[instance_reducible]

instance DRT.DRS.instDecidableIsProper {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (K : DRS L V) : Decidable K.IsProper

Equations

• K.instDecidableIsProper = decidable_of_iff (K.freeVarFinset = ∅) ⋯

theorem DRT.DRS.isProper_merge {L : FirstOrder.Language} {V : Type w} [DecidableEq V] {K₁ K₂ : DRS L V} (h₁ : K₁.IsProper) (h₂ : K₂.freeVarFinset ⊆ K₁.referents) : (K₁.merge K₂).IsProper

Merging preserves properness when the increment's free referents are supplied by the context DRS's universe.

Reuse-freeness

No discourse referent is declared twice along a nesting path: each universe is fresh for the ambient declarations, threaded through sub-boxes the way verification threads the base (the antecedent of a ⇒ feeds its referents into the consequent). This is the hypothesis under which the total agree-off-universe semantics and the persistence semantics coincide (DRS.trueRel_iff_toRelAt in DRS/Indexed.lean).

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

A DRS is reuse-free at ambient declarations X when its universe avoids X and its conditions are reuse-free at the grown set.

Equations

• DRT.DRS.ReuseFreeAt X { referents := U, conditions := cs } = (Disjoint X U ∧ DRT.Condition.ReuseFreeAllAt (X ∪ U) cs)

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

A condition is reuse-free at ambient declarations X when each sub-box is, the consequent of a ⇒ at the declarations grown by the antecedent's universe.

Equations

• DRT.Condition.ReuseFreeAt X (DRT.Condition.atom a) = True
• DRT.Condition.ReuseFreeAt X (DRT.Condition.eq a b) = True
• DRT.Condition.ReuseFreeAt X (DRT.Condition.neg K) = DRT.DRS.ReuseFreeAt X K
• DRT.Condition.ReuseFreeAt X (DRT.Condition.imp a c) = (DRT.DRS.ReuseFreeAt X a ∧ DRT.DRS.ReuseFreeAt (X ∪ a.referents) c)
• DRT.Condition.ReuseFreeAt X (DRT.Condition.dis l r) = (DRT.DRS.ReuseFreeAt X l ∧ DRT.DRS.ReuseFreeAt X r)

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

Every condition of the list is reuse-free at X.

Equations

• DRT.Condition.ReuseFreeAllAt X [] = True
• DRT.Condition.ReuseFreeAllAt X (c :: cs) = (DRT.Condition.ReuseFreeAt X c ∧ DRT.Condition.ReuseFreeAllAt X cs)

@[simp]

theorem DRT.Condition.reuseFreeAt_atom {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (X : Finset V) (a : L.Atom V) : ReuseFreeAt X (atom a)

@[simp]

theorem DRT.Condition.reuseFreeAt_eq {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (X : Finset V) (u v : V) : ReuseFreeAt X (eq u v)

@[simp]

theorem DRT.Condition.reuseFreeAt_neg {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (X : Finset V) (K : DRS L V) : ReuseFreeAt X (neg K) ↔ DRS.ReuseFreeAt X K

@[simp]

theorem DRT.Condition.reuseFreeAt_imp {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (X : Finset V) (a c : DRS L V) : ReuseFreeAt X (imp a c) ↔ DRS.ReuseFreeAt X a ∧ DRS.ReuseFreeAt (X ∪ a.referents) c

@[simp]

theorem DRT.Condition.reuseFreeAt_dis {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (X : Finset V) (l r : DRS L V) : ReuseFreeAt X (dis l r) ↔ DRS.ReuseFreeAt X l ∧ DRS.ReuseFreeAt X r

@[simp]

theorem DRT.Condition.reuseFreeAllAt_nil {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (X : Finset V) : ReuseFreeAllAt X []

@[simp]

theorem DRT.Condition.reuseFreeAllAt_cons {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (X : Finset V) (c : Condition L V) (cs : List (Condition L V)) : ReuseFreeAllAt X (c :: cs) ↔ ReuseFreeAt X c ∧ ReuseFreeAllAt X cs

@[simp]

theorem DRT.DRS.reuseFreeAt_mk {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (X U : Finset V) (conds : List (Condition L V)) : ReuseFreeAt X { referents := U, conditions := conds } ↔ Disjoint X U ∧ Condition.ReuseFreeAllAt (X ∪ U) conds

@[instance_reducible]

instance DRT.DRS.decidableReuseFreeAt {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (X : Finset V) (K : DRS L V) : Decidable (ReuseFreeAt X K)

Reuse-freeness of a DRS is decidable.

Equations

• DRT.DRS.decidableReuseFreeAt X { referents := U, conditions := cs } = instDecidableAnd

@[instance_reducible]

instance DRT.Condition.decidableReuseFreeAt {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (X : Finset V) (c : Condition L V) : Decidable (ReuseFreeAt X c)

Reuse-freeness of a condition is decidable.

Equations

• DRT.Condition.decidableReuseFreeAt X (DRT.Condition.atom a) = instDecidableTrue
• DRT.Condition.decidableReuseFreeAt X (DRT.Condition.eq a b) = instDecidableTrue
• DRT.Condition.decidableReuseFreeAt X (DRT.Condition.neg K) = DRT.DRS.decidableReuseFreeAt X K
• DRT.Condition.decidableReuseFreeAt X (DRT.Condition.imp a c) = instDecidableAnd
• DRT.Condition.decidableReuseFreeAt X (DRT.Condition.dis l r) = instDecidableAnd

@[instance_reducible]

instance DRT.Condition.decidableReuseFreeAllAt {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (X : Finset V) (cs : List (Condition L V)) : Decidable (ReuseFreeAllAt X cs)

Reuse-freeness of a list of conditions is decidable.

Equations

• DRT.Condition.decidableReuseFreeAllAt X [] = instDecidableTrue
• DRT.Condition.decidableReuseFreeAllAt X (c :: cs) = instDecidableAnd