The flat order

Flat α is Option α with the flat order: ⊥ below everything, distinct values incomparable. It is the lift of the discrete order on α — the order of partial values under extension — and is mathlib's order on Part α carried on its decidable twin Option (le_iff_ofOption_le), where it supports DecidableEq, DecidableLE, #eval, and constructor pattern-matching. "Flat domain" is the domain-theory name for this poset ([Win93]; the flat class of Isabelle/HOLCF).

The flat order is bounded-complete but not a lattice: meets are total (SemilatticeInf), joins partial (PartialUnify). Linguistically it is one atomic feature slot, ordered by [Shi86]'s and [Car92]'s subsumption; Flat Bool is the knowledge order of Kleene three-valued logic. Feature bundles arise via the Pi PartialUnify instance, with Compat as consistency.

The order skeleton follows the WithBot mold (Mathlib/Order/TypeTags.lean, Mathlib/Order/WithBot.lean) and is an [UPSTREAM] candidate for Mathlib/Order/Flat.lean, coexisting with the namespaced Module.Flat and ConvexCone.Flat. The PartialUnify instance and compat_iff stay here.

Main declarations

• Flat — the order-carrying alias, with coercion ↑ : α → Flat α, and PartialOrder, OrderBot, SemilatticeInf and PartialUnify instances
• Flat.coe_le_coe, Flat.not_coe_le_bot — the order, characterized
• Flat.covBy_iff — the covers, from ⊥ to a committed value: the order has height one
• Flat.coe_inf_coe, Flat.disjoint_coe_coe, Flat.compat_coe_coe — the meet, disjointness and compatibility of committed slots
• Flat.unbotD — the value, or a default at ⊥, as WithBot.unbotD
• Flat.or — left-biased total merge, with le_or_left/or_le
• Flat.compat_iff — slot compatibility (Compat), characterized
• Flat.unify_eq_top_of_ne — distinct atoms do not unify (the non-distributivity witness)

def Flat (α : Type u_1) : Type u_1

Flat α is Option α carrying the flat information order: ⊥ below everything, distinct values incomparable. A def, not an abbrev, so the order instances do not leak onto bare Option.

Equations

• Flat α = Option α

@[match_pattern]

def Flat.some {α : Type u_1} : α → Flat α

The canonical map from α into Flat α.

Equations

• Flat.some = some

@[instance_reducible]

instance Flat.coe {α : Type u_1} : Coe α (Flat α)

Equations

• Flat.coe = { coe := Flat.some }

@[instance_reducible]

instance Flat.bot {α : Type u_1} : Bot (Flat α)

Equations

• Flat.bot = { bot := none }

@[instance_reducible]

instance Flat.inhabited {α : Type u_1} : Inhabited (Flat α)

Equations

• Flat.inhabited = { default := ⊥ }

@[instance_reducible]

instance Flat.instDecidableEq {α : Type u_1} [DecidableEq α] : DecidableEq (Flat α)

Equations

• Flat.instDecidableEq = Flat.instDecidableEq._aux_1

@[instance_reducible]

instance Flat.instBEq {α : Type u_1} [BEq α] : BEq (Flat α)

Equations

• Flat.instBEq = { beq := Flat.instBEq._aux_1 }

instance Flat.instLawfulBEq {α : Type u_1} [BEq α] [LawfulBEq α] : LawfulBEq (Flat α)

@[instance_reducible]

instance Flat.instRepr {α : Type u_1} [Repr α] : Repr (Flat α)

Equations

• Flat.instRepr = { reprPrec := fun (o : Flat α) (x : ℕ) => match o with | none => Std.Format.text "⊥" | some a => Std.Format.text "↑" ++ repr a }

theorem Flat.coe_injective {α : Type u_1} : Function.Injective some

@[simp]

theorem Flat.coe_inj {α : Type u_1} {a b : α} : ↑a = ↑b ↔ a = b

theorem Flat.none_eq_bot {α : Type u_1} : none = ⊥

theorem Flat.some_eq_coe {α : Type u_1} (a : α) : Option.some a = ↑a

@[simp]

theorem Flat.bot_ne_coe {α : Type u_1} {a : α} : ⊥ ≠ ↑a

@[simp]

theorem Flat.coe_ne_bot {α : Type u_1} {a : α} : ↑a ≠ ⊥

def Flat.recBotCoe {α : Type u_1} {C : Flat α → Sort u_2} (bot : C ⊥) (coe : (a : α) → C ↑a) (x : Flat α) : C x

Recursor for Flat using the preferred forms ⊥ and ↑a.

Equations

• Flat.recBotCoe bot coe none = bot
• Flat.recBotCoe bot coe (some a) = coe a

@[simp]

theorem Flat.recBotCoe_bot {α : Type u_1} {C : Flat α → Sort u_2} (d : C ⊥) (f : (a : α) → C ↑a) : recBotCoe d f ⊥ = d

@[simp]

theorem Flat.recBotCoe_coe {α : Type u_1} {C : Flat α → Sort u_2} (d : C ⊥) (f : (a : α) → C ↑a) (x : α) : recBotCoe d f ↑x = f x

theorem Flat.ne_bot_iff_exists {α : Type u_1} {x : Flat α} : x ≠ ⊥ ↔ ∃ (a : α), x = ↑a

def Flat.unbotD {α : Type u_1} (d : α) (x : Flat α) : α

The value of an element, or the default d at ⊥, as WithBot.unbotD.

Equations

• Flat.unbotD d x = Flat.recBotCoe d id x

@[simp]

theorem Flat.unbotD_bot {α : Type u_1} (d : α) : unbotD d ⊥ = d

@[simp]

theorem Flat.unbotD_coe {α : Type u_1} (d b : α) : unbotD d ↑b = b

def Flat.get {α : Type u_1} (x : Flat α) (h : x ≠ ⊥) : α

The value of a committed slot.

Equations

• x.get h = Option.get x ⋯

@[simp]

theorem Flat.coe_get {α : Type u_1} (x : Flat α) (h : x ≠ ⊥) : ↑(x.get h) = x

@[simp]

theorem Flat.get_coe {α : Type u_1} (a : α) (h : ↑a ≠ ⊥) : (↑a).get h = a

The flat order

inductive Flat.LE {α : Type u_1} : Flat α → Flat α → Prop

Auxiliary definition for the order on Flat.

• bot_le {α : Type u_1} (x : Flat α) : ⊥.LE x
• refl {α : Type u_1} (a : α) : (↑a).LE ↑a

theorem Flat.le_def_aux {α : Type u_1} (a✝ a✝¹ : Flat α) : a✝.LE a✝¹ ↔ a✝ = ⊥ ∨ ∃ (a : α), a✝ = ↑a ∧ a✝¹ = ↑a

@[instance_reducible, instance 10]

instance Flat.instLE {α : Type u_1} : LE (Flat α)

The flat order on Flat α, defined by ⊥ ≤ x and ↑a ≤ ↑a. The definition as an inductive predicate follows WithBot.LE; it cannot be accidentally unfolded too far.

Equations

• Flat.instLE = { le := Flat.LE }

theorem Flat.le_def {α : Type u_1} {x y : Flat α} : x ≤ y ↔ x = ⊥ ∨ ∃ (a : α), x = ↑a ∧ y = ↑a

@[simp]

theorem Flat.coe_le_coe {α : Type u_1} {a b : α} : ↑a ≤ ↑b ↔ a = b

@[simp]

theorem Flat.not_coe_le_bot {α : Type u_1} (a : α) : ¬↑a ≤ ⊥

@[instance_reducible]

instance Flat.instOrderBot {α : Type u_1} : OrderBot (Flat α)

Equations

• Flat.instOrderBot = { toBot := Flat.bot, bot_le := ⋯ }

@[instance_reducible]

instance Flat.instPartialOrder {α : Type u_1} : PartialOrder (Flat α)

Equations

• Flat.instPartialOrder = { toLE := Flat.instLE, lt := fun (a b : Flat α) => a ≤ b ∧ ¬b ≤ a, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯ }

theorem Flat.coe_le_iff {α : Type u_1} {a : α} {y : Flat α} : ↑a ≤ y ↔ y = ↑a

theorem Flat.isMax_coe {α : Type u_1} (a : α) : IsMax ↑a

A value is maximal: nothing lies above it but itself.

theorem Flat.isMax_of_ne_bot {α : Type u_1} {x : Flat α} (hx : x ≠ ⊥) : IsMax x

Every value other than ⊥ is maximal.

@[instance_reducible]

instance Flat.instDecidableLEOfDecidableEq {α : Type u_1} [DecidableEq α] : DecidableLE (Flat α)

Equations

• Flat.instDecidableLEOfDecidableEq none x✝ = isTrue ⋯
• Flat.instDecidableLEOfDecidableEq (some a) none = isFalse ⋯
• Flat.instDecidableLEOfDecidableEq (some a) (some b) = decidable_of_iff' (a = b) ⋯

theorem Flat.eq_of_le {α : Type u_1} {x y : Flat α} (h : x ≤ y) (hyx : y ≠ ⊥ → x ≠ ⊥) : x = y

A flat inequality with no definedness gain is an equality.

Covering

theorem Flat.covBy_iff {α : Type u_1} {x y : Flat α} : x ⋖ y ↔ x = ⊥ ∧ y ≠ ⊥

The flat order has height one: its covers are the steps from ⊥ to a committed value.

@[simp]

theorem Flat.bot_covBy_coe {α : Type u_1} (a : α) : ⊥ ⋖ ↑a

theorem Flat.le_iff_ofOption_le {α : Type u_1} {x y : Flat α} : x ≤ y ↔ ↑x ≤ ↑y

The flat order is Part's order, along Part.ofOption.

Left-biased merge

def Flat.or {α : Type u_1} (x y : Flat α) : Flat α

The left-biased total merge of two slots, keeping the first committed value; the total companion of the partial join Flat.unify.

Equations

• x.or y = Option.or x y

@[simp]

theorem Flat.bot_or {α : Type u_1} (y : Flat α) : ⊥.or y = y

@[simp]

theorem Flat.coe_or {α : Type u_1} (a : α) (y : Flat α) : (↑a).or y = ↑a

@[simp]

theorem Flat.or_bot {α : Type u_1} (x : Flat α) : x.or ⊥ = x

theorem Flat.or_assoc {α : Type u_1} (x y z : Flat α) : (x.or y).or z = x.or (y.or z)

theorem Flat.le_or_left {α : Type u_1} (x y : Flat α) : x ≤ x.or y

theorem Flat.or_le {α : Type u_1} {x y z : Flat α} (hx : x ≤ z) (hy : y ≤ z) : x.or y ≤ z

@[simp]

theorem Flat.or_self {α : Type u_1} (x : Flat α) : x.or x = x

Meets

def Flat.inf {α : Type u_1} [DecidableEq α] (x y : Flat α) : Flat α

The meet of two slots is their agreement, or ⊥ — the generalization (anti-unification) of the two, order-dual to the partial join PartialUnify.

Equations

• x.inf y = if x = y then x else ⊥

@[instance_reducible]

instance Flat.instSemilatticeInfOfDecidableEq {α : Type u_1} [DecidableEq α] : SemilatticeInf (Flat α)

Equations

• Flat.instSemilatticeInfOfDecidableEq = { toPartialOrder := Flat.instPartialOrder, inf := Flat.inf, inf_le_left := ⋯, inf_le_right := ⋯, le_inf := ⋯ }

theorem Flat.inf_def {α : Type u_1} [DecidableEq α] (x y : Flat α) : x ⊓ y = if x = y then x else ⊥

@[simp]

theorem Flat.coe_inf_coe {α : Type u_1} [DecidableEq α] (a b : α) : ↑a ⊓ ↑b = if a = b then ↑a else ⊥

@[simp]

theorem Flat.disjoint_coe_coe {α : Type u_1} {a b : α} : Disjoint ↑a ↑b ↔ a ≠ b

Two committed slots are disjoint exactly when they disagree.

@[simp]

theorem Flat.compat_coe_coe {α : Type u_1} {a b : α} : Compat ↑a ↑b ↔ a = b

Two committed slots are compatible exactly when they agree.

@[instance_reducible]

instance Flat.instDecidableDisjointOfDecidableEq {α : Type u_1} {x y : Flat α} [DecidableEq α] : Decidable (Disjoint x y)

Equations

• Flat.instDecidableDisjointOfDecidableEq = decidable_of_iff (x ⊓ y = ⊥) ⋯

Unification

def Flat.unify {α : Type u_1} [DecidableEq α] : Flat α → Flat α → WithTop (Flat α)

Unification of two slots merges equal commitments, treats ⊥ as identity, and fails on distinct commitments.

Equations

• Flat.unify none x✝ = ↑x✝
• Flat.unify (some a) none = ↑↑a
• Flat.unify (some a) (some b) = if a = b then ↑↑a else ⊤

@[instance_reducible]

instance Flat.instPartialUnifyOfDecidableEq {α : Type u_1} [DecidableEq α] : PartialUnify (Flat α)

Equations

• Flat.instPartialUnifyOfDecidableEq = { unify := Flat.unify, isLUB_of_unify_eq_coe := ⋯, unify_ne_top_of_bddAbove := ⋯ }

theorem Flat.compat_iff {α : Type u_1} {x y : Flat α} : Compat x y ↔ ∀ (a : α), x = ↑a → ∀ (b : α), y = ↑b → a = b

Two slots are compatible exactly when their committed values coincide; an uncommitted slot is a wildcard.

theorem Flat.le_or_right {α : Type u_1} {x y : Flat α} (h : Compat x y) : y ≤ x.or y

On compatible slots the right slot also lies below the left-biased merge.

Non-distributivity

The flat order is not distributive: three distinct atoms (with a top adjoined) form the diamond M₃ — [Car92] takes subsumption orders to be neither distributive nor modular in general. Flat carries only the partial join (PartialUnify), so the distributive law cannot even be stated on it directly; unify_eq_top_of_ne is the witness — distinct atoms have no upper bound, so the join the law would require is undefined.

theorem Flat.unify_eq_top_of_ne {α : Type u_1} {a b : α} [DecidableEq α] (h : a ≠ b) : (↑a).unify ↑b = ⊤