Partial unification

PartialUnify α equips a partial order with a partial join: unify a b is the least upper bound of {a, b} when the pair is bounded above, and ⊤ otherwise. This is the pairwise face of bounded completeness, Carpenter's setting for unification domains, in which an inheritance hierarchy is a finite bounded complete partial order and joins are unifications. Adjoining a top element, the inconsistent description, makes the join total, as Aït-Kaci and Smolka do in Carpenter's account: WithTop α is a join-semilattice whose join of two coerced elements is their unification, and the laws of unification, idempotence, commutativity, associativity with failure propagating, ⊥ as identity and monotonicity, are the semilattice laws read through the coercion. A carrier supplies only unify and the two axioms. The semilattice is a scoped instance, since a carrier that is already a semilattice would otherwise give WithTop α a second join.

Main declarations

• PartialUnify: the class.
• PartialUnify.isLUB_unify: unify a b is the join of ↑a and ↑b in WithTop α.
• PartialUnify.semilatticeSup: the scoped join-semilattice on WithTop α.
• PartialUnify.unify_eq_coe_iff_isLUB, PartialUnify.unify_eq_top_iff: success and failure, characterized.
• PartialUnify.unify_comm, PartialUnify.unify_assoc, PartialUnify.unify_self, PartialUnify.bot_unify, PartialUnify.unify_mono: the unification laws.
• Compat: the consistency relation, a common upper bound.
• The Pi instance: pointwise unification over a Fintype index.

Implementation notes

mem_upperBounds_pair, WithTop.decidableEqTop, WithTop.isLUB_image_coe_iff and WithTop.isLUB_image_coe_top_iff are rungs of mathlib's bounds and WithTop API that the class needs and mathlib lacks. [UPSTREAM]

References

• [Car92]
• [Shi86]

Bounds of pairs and of coerced sets

theorem mem_upperBounds_pair {α : Type u_1} [Preorder α] {u a b : α} : u ∈ upperBounds {a, b} ↔ a ≤ u ∧ b ≤ u

@[instance_reducible]

instance WithTop.decidableEqTop {α : Type u_1} (x : WithTop α) : Decidable (x = ⊤)

Whether an element of WithTop α is ⊤ is decidable without decidable equality on α.

Equations

• x.decidableEqTop = WithTop.recTopCoe (isTrue ⋯) (fun (x : α) => isFalse ⋯) x

theorem WithTop.coe_mem_upperBounds_image_coe {α : Type u_1} [Preorder α] {s : Set α} {u : α} : ↑u ∈ upperBounds (some '' s) ↔ u ∈ upperBounds s

theorem WithTop.isLUB_image_coe_iff {α : Type u_1} [Preorder α] {s : Set α} {u : α} : IsLUB (some '' s) ↑u ↔ IsLUB s u

A coerced element is the least upper bound of a set of coerced elements iff it is the least upper bound of the set.

theorem WithTop.isLUB_image_coe_top_iff {α : Type u_1} [Preorder α] {s : Set α} : IsLUB (some '' s) ⊤ ↔ ¬BddAbove s

⊤ is the least upper bound of a set of coerced elements iff the set is unbounded.

The class

class PartialUnify (α : Type u_1) [PartialOrder α] : Type u_1

A partial join on a partial order, where unify a b is the least upper bound of {a, b} when the pair is bounded above and ⊤ otherwise.

• unify : α → α → WithTop α

  The partial join, ⊤ on an unbounded pair.

• isLUB_of_unify_eq_coe {a b c : α} : unify a b = ↑c → IsLUB {a, b} c

  A successful unification is a least upper bound.

• unify_ne_top_of_bddAbove {a b : α} : BddAbove {a, b} → unify a b ≠ ⊤

  Unification succeeds on bounded pairs.

theorem PartialUnify.isLUB_unify {α : Type u_1} [PartialOrder α] [PartialUnify α] (a b : α) : IsLUB {↑a, ↑b} (unify a b)

unify a b is the join of ↑a and ↑b in WithTop α.

theorem PartialUnify.unify_eq_coe_iff_isLUB {α : Type u_1} [PartialOrder α] [PartialUnify α] {a b c : α} : unify a b = ↑c ↔ IsLUB {a, b} c

theorem PartialUnify.unify_eq_top_iff {α : Type u_1} [PartialOrder α] [PartialUnify α] {a b : α} : unify a b = ⊤ ↔ ¬BddAbove {a, b}

theorem PartialUnify.unify_ne_top_iff_bddAbove {α : Type u_1} [PartialOrder α] [PartialUnify α] {a b : α} : unify a b ≠ ⊤ ↔ BddAbove {a, b}

The join-semilattice with failure adjoined

def PartialUnify.sup {α : Type u_1} [PartialOrder α] [PartialUnify α] : WithTop α → WithTop α → WithTop α

The join on WithTop α that unification computes, ⊤ absorbing.

Equations

• PartialUnify.sup (some a) (some b) = PartialUnify.unify a b
• PartialUnify.sup x✝¹ x✝ = ⊤

theorem PartialUnify.isLUB_sup {α : Type u_1} [PartialOrder α] [PartialUnify α] (x y : WithTop α) : IsLUB {x, y} (PartialUnify.sup x y)

@[instance_reducible]

def PartialUnify.semilatticeSup {α : Type u_1} [PartialOrder α] [PartialUnify α] : SemilatticeSup (WithTop α)

Unification presents WithTop α as a join-semilattice with ⊤ as the failure of unification. The instance is scoped: a carrier that is already a semilattice would otherwise give WithTop α a second join.

Equations

• PartialUnify.semilatticeSup = SemilatticeSup.ofIsLUB PartialUnify.sup ⋯

@[simp]

theorem PartialUnify.coe_sup_coe {α : Type u_1} [PartialOrder α] [PartialUnify α] (a b : α) : ↑a ⊔ ↑b = unify a b

theorem PartialUnify.unify_comm {α : Type u_1} [PartialOrder α] [PartialUnify α] (a b : α) : unify a b = unify b a

@[simp]

theorem PartialUnify.unify_self {α : Type u_1} [PartialOrder α] [PartialUnify α] (a : α) : unify a a = ↑a

theorem PartialUnify.unify_assoc {α : Type u_1} [PartialOrder α] [PartialUnify α] (a b c : α) : unify a b ⊔ ↑c = ↑a ⊔ unify b c

Unification is associative, with failure propagating.

theorem PartialUnify.unify_le_coe_iff {α : Type u_1} [PartialOrder α] [PartialUnify α] {a b c : α} : unify a b ≤ ↑c ↔ a ≤ c ∧ b ≤ c

theorem PartialUnify.unify_eq_left {α : Type u_1} [PartialOrder α] [PartialUnify α] {a b : α} : unify a b = ↑a ↔ b ≤ a

theorem PartialUnify.unify_eq_right {α : Type u_1} [PartialOrder α] [PartialUnify α] {a b : α} : unify a b = ↑b ↔ a ≤ b

theorem PartialUnify.sup_coe_eq_coe_iff {α : Type u_1} [PartialOrder α] [PartialUnify α] {a c : α} {x : WithTop α} : x ⊔ ↑c = ↑a ↔ ∃ (y : α), x = ↑y ∧ unify y c = ↑a

theorem PartialUnify.coe_sup_eq_coe_iff {α : Type u_1} [PartialOrder α] [PartialUnify α] {a c : α} {x : WithTop α} : ↑a ⊔ x = ↑c ↔ ∃ (y : α), x = ↑y ∧ unify a y = ↑c

theorem PartialUnify.unify_mono {α : Type u_1} [PartialOrder α] [PartialUnify α] {a₁ a₂ b₁ b₂ u₂ : α} (ha : a₁ ≤ a₂) (hb : b₁ ≤ b₂) (h₂ : unify a₂ b₂ = ↑u₂) : ∃ (u₁ : α), unify a₁ b₁ = ↑u₁ ∧ u₁ ≤ u₂

Unification is monotone where defined, so shrinking both inputs preserves success and shrinks the output.

@[simp]

theorem PartialUnify.bot_unify {α : Type u_1} [PartialOrder α] [PartialUnify α] [OrderBot α] (a : α) : unify ⊥ a = ↑a

@[simp]

theorem PartialUnify.unify_bot {α : Type u_1} [PartialOrder α] [PartialUnify α] [OrderBot α] (a : α) : unify a ⊥ = ↑a

Pointwise unification on Pi types

@[instance_reducible]

instance PartialUnify.instForall {F : Type u_2} {S : F → Type u_3} [(t : F) → PartialOrder (S t)] [(t : F) → PartialUnify (S t)] [Fintype F] : PartialUnify ((t : F) → S t)

Unification is pointwise, so a bundle unifies when every coordinate does.

Equations

• One or more equations did not get rendered due to their size.

Compatibility

The consistency relation of unification: two elements are compatible when they have a common upper bound, equivalently when they unify. On feature carriers this is the agreement relation of Carpenter and Shieber.

@[reducible, inline]

abbrev Compat {α : Type u_1} [Preorder α] (a b : α) : Prop

Two elements are compatible when they are bounded above, the consistency relation of unification. An abbrev, so the BddAbove API applies.

Equations

• Compat a b = BddAbove {a, b}

theorem Compat.of_le {α : Type u_1} [Preorder α] {a b u : α} (ha : a ≤ u) (hb : b ≤ u) : Compat a b

A common upper bound witnesses compatibility.

theorem Compat.symm {α : Type u_1} [Preorder α] {a b : α} (h : Compat a b) : Compat b a

theorem Compat.mono {α : Type u_1} [Preorder α] {a b c d : α} (h₁ : a ≤ b) (h₂ : c ≤ d) (h : Compat b d) : Compat a c

Compatibility persists downward.

theorem compat_self {α : Type u_1} [Preorder α] (a : α) : Compat a a

theorem compat_pi_iff {F : Type u_2} {S : F → Type u_3} [(t : F) → Preorder (S t)] {f g : (t : F) → S t} : Compat f g ↔ ∀ (t : F), Compat (f t) (g t)

Compatibility on a Pi type is pointwise.

theorem Compat.apply {F : Type u_2} {S : F → Type u_3} [(t : F) → Preorder (S t)] {f g : (t : F) → S t} (h : Compat f g) (t : F) : Compat (f t) (g t)

Compatibility of functions is pointwise.

theorem bot_compat {α : Type u_1} [Preorder α] [OrderBot α] (a : α) : Compat ⊥ a

⊥ is a wildcard, compatible with everything.

theorem compat_bot {α : Type u_1} [Preorder α] [OrderBot α] (a : α) : Compat a ⊥

theorem not_compat_iff_of_forall_isMax {α : Type u_1} [PartialOrder α] [OrderBot α] (h : ∀ (a : α), a ≠ ⊥ → IsMax a) {a b : α} : ¬Compat a b ↔ a ≠ ⊥ ∧ b ≠ ⊥ ∧ a ≠ b

Where every element other than ⊥ is maximal, two elements are incompatible exactly when both are present and distinct.

@[instance_reducible]

instance instDecidableCompatOfPartialUnify {α : Type u_1} [PartialOrder α] [PartialUnify α] (a b : α) : Decidable (Compat a b)

Equations

• instDecidableCompatOfPartialUnify a b = decidable_of_iff (PartialUnify.unify a b ≠ ⊤) ⋯