Same-except relations

Two items over a shared position space are the same except at a set S of positions when they agree everywhere outside S ([CJ12]; [JA20] §3.7). This is literally Set.EqOn on the complement, so the relation inherits mathlib's equal-on API. William James' observation that comparison presupposes a common frame is the domain-general root; the shared position type Pos encodes the Gentner-Sagi structural-alignment presupposition — the two items are already put into correspondence.

What happens at the except-positions classifies the relation. In an elaboration, one side is decorated and the other empty (⊥): the same as the other plus something else. In a contrast, both sides are decorated and differ. [JA20] add a third reading for the schema-to-instance case, where the item strictly dominates the schema (Instantiation); they hedge what to call it, and strict order is one settled reading, not William James' or [CJ12]'s. The three cases are intentionally non-exhaustive — double contrasts and elaborations in different places satisfy none.

A schema itself expresses a same-except relation to its instances (Instantiation.instantiates): the instantiation case entails Schema.Instantiates.

Main declarations

• SameExcept — agreement off a position set (Set.EqOn on the complement)
• SameExcept.symm, SameExcept.mono, SameExcept.trans — the equal-on API
• Elaboration, Contrast, Instantiation — the classification at the except-positions
• Contrast.symm — contrast is symmetric
• Instantiation.instantiates — the schema-instance relation is a same-except relation

@[reducible, inline]

abbrev Morphology.Construction.SameExcept {Pos : Type u_1} {α : Type u_2} (f g : Pos → α) (S : Set Pos) : Prop

Two items are the same except at S when they agree off S: Set.EqOn on the complement.

Equations

• Morphology.Construction.SameExcept f g S = Set.EqOn f g Sᶜ

theorem Morphology.Construction.SameExcept.symm {Pos : Type u_1} {α : Type u_2} {f g : Pos → α} {S : Set Pos} (h : SameExcept f g S) : SameExcept g f S

Same-except is symmetric.

theorem Morphology.Construction.SameExcept.mono {Pos : Type u_1} {α : Type u_2} {f g : Pos → α} {S T : Set Pos} (hST : S ⊆ T) (h : SameExcept f g S) : SameExcept f g T

Same-except is monotone in the except-set: agreeing off a smaller set implies agreeing off a larger one.

theorem Morphology.Construction.SameExcept.trans {Pos : Type u_1} {α : Type u_2} {f g k : Pos → α} {S : Set Pos} (h₁ : SameExcept f g S) (h₂ : SameExcept g k S) : SameExcept f k S

Same-except is transitive at a fixed except-set.

def Morphology.Construction.Instantiation {Pos : Type u_1} {α : Type u_2} [PartialOrder α] (f g : Pos → α) (S : Set Pos) : Prop

The schema-to-instance case: same except at S, where the second strictly dominates the first — [JA20]'s added third reading.

Equations

• Morphology.Construction.Instantiation f g S = (Morphology.Construction.SameExcept f g S ∧ ∀ p ∈ S, f p < g p)

theorem Morphology.Construction.Instantiation.instantiates {Pos : Type u_1} {α : Type u_2} [PartialOrder α] {s : Schema Pos α} {w : Pos → α} {S : Set Pos} (h : Instantiation s.body w S) : s.Instantiates w

The schema-instance relation is a same-except relation: an instantiation of a schema's description entails Schema.Instantiates.

def Morphology.Construction.Elaboration {Pos : Type u_1} {α : Type u_2} [PartialOrder α] [OrderBot α] (f g : Pos → α) (S : Set Pos) : Prop

An elaboration: same except at S, where the first side is present and the second empty — the same as the other plus something else.

Equations

• Morphology.Construction.Elaboration f g S = (Morphology.Construction.SameExcept f g S ∧ ∀ p ∈ S, f p ≠ ⊥ ∧ g p = ⊥)

def Morphology.Construction.Contrast {Pos : Type u_1} {α : Type u_2} [PartialOrder α] [OrderBot α] (f g : Pos → α) (S : Set Pos) : Prop

A contrast: same except at S, where both sides are present and distinct.

Equations

• Morphology.Construction.Contrast f g S = (Morphology.Construction.SameExcept f g S ∧ ∀ p ∈ S, f p ≠ ⊥ ∧ g p ≠ ⊥ ∧ f p ≠ g p)

theorem Morphology.Construction.Contrast.symm {Pos : Type u_1} {α : Type u_2} [PartialOrder α] [OrderBot α] {f g : Pos → α} {S : Set Pos} (h : Contrast f g S) : Contrast g f S

Contrast is symmetric.