Control: Basic Lemmas

Basic lemmas about the control vocabulary of Syntax/Control/Defs.lean: the exhaustive-control lemma family (refinement, composition, exclusion of partial readings and split antecedents), the localization of a partial reading to a leg of a composite dependency, the phenomenology of saturation, and the occupant-mismatch refutation engine of the overt-copy diagnostics ([PP06]).

Exhaustive control

theorem Control.IsExhaustive.eq {Pos : Type u_1} {Ref : Type u_2} {val : Pos → Ref} {ante : SetRel Pos Pos} {a b : Pos} (hs : IsExhaustive val ante) (h : (a, b) ∈ ante) : val a = val b

Related positions of an exhaustive dependency are co-valued.

theorem Control.IsExhaustive.mono {Pos : Type u_1} {Ref : Type u_2} {val : Pos → Ref} {ante bind : SetRel Pos Pos} (h : ante ⊆ bind) (hs : IsExhaustive val bind) : IsExhaustive val ante

A refinement of an exhaustive dependency is exhaustive.

theorem Control.IsExhaustive.comp {Pos : Type u_1} {Ref : Type u_2} {val : Pos → Ref} {bind pred : SetRel Pos Pos} (hb : IsExhaustive val bind) (hp : IsExhaustive val pred) : IsExhaustive val (bind.comp pred)

Exhaustivity composes through the mediating position.

theorem Control.IsExhaustive.not_lt {Pos : Type u_1} {Ref : Type u_2} {val : Pos → Ref} {ante : SetRel Pos Pos} {a b : Pos} [Preorder Ref] (hs : IsExhaustive val ante) (h : (a, b) ∈ ante) : ¬val a < val b

Exhaustive control excludes partial readings: no strict growth of the referent along the dependency ([Lan00a]).

theorem Control.IsExhaustive.eq_of_two {Pos : Type u_1} {Ref : Type u_2} {val : Pos → Ref} {ante : SetRel Pos Pos} {a b p : Pos} (hs : IsExhaustive val ante) (ha : (a, p) ∈ ante) (hb : (b, p) ∈ ante) : val a = val b

Under exhaustive control, joint antecedents are co-valued — split control needs a non-exhaustive leg.

theorem Control.IsExhaustive.not_isPartial {Pos : Type u_1} {Ref : Type u_2} {val : Pos → Ref} {d : SetRel Pos Pos} [Preorder Ref] (h : IsExhaustive val d) : ¬IsPartial val d

An exhaustive dependency admits no partial reading.

theorem Control.exists_lt_of_comp_lt {Pos : Type u_1} {Ref : Type u_2} {val : Pos → Ref} {bind pred : SetRel Pos Pos} {a c : Pos} [PartialOrder Ref] (hb : ∀ ⦃x m : Pos⦄, (x, m) ∈ bind → val x ≤ val m) (h : (a, c) ∈ bind.comp pred) (hlt : val a < val c) : (∃ (x : Pos), ∃ (m : Pos), (x, m) ∈ bind ∧ val x < val m) ∨ ∃ (m : Pos), ∃ (x : Pos), (m, x) ∈ pred ∧ val m < val x

A partial reading in a composite localizes to a leg: if referents grow monotonely along the first leg and strictly across the composite, one of the two legs already grows strictly.

Saturation

theorem Control.IsSaturating.not_isPartial {Pos : Type u_1} {Ref : Type u_2} {val : Pos → Ref} {d : SetRel Pos Pos} [Preorder Ref] (h : IsSaturating val d) : ¬IsPartial val d

A saturating dependency admits no partial reading.

theorem Control.IsSaturating.eq_of_controllers {Pos : Type u_1} {Ref : Type u_2} {val : Pos → Ref} {d : SetRel Pos Pos} {a b p : Pos} (h : IsSaturating val d) (ha : (a, p) ∈ d) (hb : (b, p) ∈ d) : a = b

A saturating dependency admits no split: joint controllers coincide.

theorem Control.IsSaturating.not_isSplit {Pos : Type u_1} {Ref : Type u_2} {val : Pos → Ref} {d : SetRel Pos Pos} (h : IsSaturating val d) : ¬IsSplit d

A saturating dependency admits no split antecedents.

theorem Control.IsSaturating.eq_of_controlled {Pos : Type u_1} {Ref : Type u_2} {val : Pos → Ref} {d : SetRel Pos Pos} {a p q : Pos} (h : IsSaturating val d) (hp : (a, p) ∈ d) (hq : (a, q) ∈ d) : p = q

A saturating controller saturates a single slot: its dependents coincide.

Enforcement

Which assignment a dependency exhaustively shares distinguishes the enforcement species ([Bre82]): functional control shares the occupant assignment itself (structure sharing — movement chains, LFG control equations), anaphoric control only the referent valuation. Occupant sharing is the stronger: a shared assignment transports along every map of it (IsExhaustive.map), so every occupant property transports across the dependency (IsExhaustive.iff_of_rel) — and one observed mismatch refutes it (not_isExhaustive_of_mismatch), the engine of the overt-copy diagnostics ([PP06]).

theorem Control.IsExhaustive.map {Pos : Type u_1} {Ref : Type u_2} {ante : SetRel Pos Pos} {Item : Type u_3} {occ : Pos → Item} (hs : IsExhaustive occ ante) (f : Item → Ref) : IsExhaustive (f ∘ occ) ante

Sharing an assignment transports along any map of it: token identity yields referential co-valuation for every referent map.

theorem Control.IsExhaustive.iff_of_rel {Pos : Type u_1} {ante : SetRel Pos Pos} {a b : Pos} {Item : Type u_3} {occ : Pos → Item} (hs : IsExhaustive occ ante) (h : (a, b) ∈ ante) (P : Item → Prop) : P (occ a) ↔ P (occ b)

Under a shared assignment, every property of the assigned value transports across the dependency: copies are indistinguishable.

theorem Control.not_isExhaustive_of_mismatch {Pos : Type u_1} {ante : SetRel Pos Pos} {a b : Pos} {Item : Type u_3} {occ : Pos → Item} {P : Item → Prop} (h : (a, b) ∈ ante) (hPa : P (occ a)) (hPb : ¬P (occ b)) : ¬IsExhaustive occ ante

One observed mismatch refutes a shared assignment — the refutation engine of the copy-control diagnostics.