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). It is ω-complete (OmegaCompletePartialOrder), every chain being eventually constant. 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, OmegaCompletePartialOrder, and PartialUnify instances
• Flat.coe_le_coe, Flat.not_coe_le_bot — the order, characterized
• Flat.or — left-biased total merge, with le_or_left/or_le
• Flat.ωSup_mem_range — chains attain their supremum (the domain has height ≤ 2)
• Flat.ωScottContinuous_of_monotone — monotone maps out of Flat are continuous
• Flat.liftEquiv — the free-domain universal property: functions α → D are exactly strict continuous maps Flat α →𝒄 D
• Flat.compat_iff — slot compatibility (Compat), characterized
• Flat.unify_distinct_eq_none — distinct atoms do not unify (the non-distributivity witness)

TODO

The free-domain universal property is now liftEquiv (with its enabling lemma ωScottContinuous_of_monotone). The remaining domain-theoretic program:

• Categorical freeness. Package liftEquiv as a free–forgetful adjunction between Type and the pointed ωCPO category — Flat ⊣ U (template: mathlib's latToBddLatForgetAdjunction, the free bounded lattice via WithBot).
• Lifting monad. Give Flat (= Option) its ω-CPO monad structure — the partiality/lifting monad — whose Kleisli arrows α → Flat β are partial continuous functions; PartialUnify.unify is one, which is why it composes through Option.bind (unify_assoc). (mathlib has this for Part.)
• Algebraicity / bounded-completeness. Every element of Flat α is compact, making it an algebraic (finite-height) bounded-complete domain — the Scott-domain packaging of the partial join PartialUnify provides.
• Three-valued logic. Flat Bool is the knowledge order of Kleene three-valued logic; the strong-Kleene connectives are exactly its continuous maps. Connects this substrate to the trivalence/presupposition layer.
• An inductive Flat.LT in the WithBot.LT mold, for upstreaming.

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

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 := ⋯ }

@[simp]

theorem Flat.le_bot_iff {α : Type u_1} {x : Flat α} : x ≤ ⊥ ↔ x = ⊥

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

theorem Flat.le_coe_iff {α : Type u_1} {b : α} {x : Flat α} : x ≤ ↑b ↔ x = ⊥ ∨ x = ↑b

@[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.ne_bot_of_le {α : Type u_1} {x y : Flat α} (h : x ≤ y) (hx : x ≠ ⊥) : y ≠ ⊥

Definedness persists up the flat order.

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.

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

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 := ⋯ }

The flat domain is ω-complete

A monotone chain in the flat order is eventually constant — ⊥ until it (optionally) commits to a single value, then constant — so it has a supremum. This is the flat domain, the canonical nontrivial example of an OmegaCompletePartialOrder.

@[instance_reducible]

noncomputable instance Flat.instOmegaCompletePartialOrder {α : Type u_1} : OmegaCompletePartialOrder (Flat α)

The flat domain is an OmegaCompletePartialOrder: chains are eventually constant, so their suprema are the eventual value (or ⊥).

Equations

• Flat.instOmegaCompletePartialOrder = { toPartialOrder := Flat.instPartialOrder, ωSup := Flat.ωSupImpl✝, le_ωSup := ⋯, ωSup_le := ⋯ }

theorem Flat.ωSup_mem_range {α : Type u_1} (c : OmegaCompletePartialOrder.Chain (Flat α)) : OmegaCompletePartialOrder.ωSup c ∈ Set.range ⇑c

Chains in the flat domain attain their supremum — ωSup c is some c i: the domain has height ≤ 2.

theorem Flat.ωScottContinuous_of_monotone {α : Type u_1} {D : Type u_2} [OmegaCompletePartialOrder D] {f : Flat α → D} (hf : Monotone f) : OmegaCompletePartialOrder.ωScottContinuous f

Every monotone map out of the flat domain is ωScottContinuous: chains attain their suprema (ωSup_mem_range), so continuity is automatic. This is the key fact behind the universal property liftEquiv.

noncomputable def Flat.liftEquiv {α : Type u_1} {D : Type u_2} [OmegaCompletePartialOrder D] [OrderBot D] : (α → D) ≃ { f : Flat α →𝒄 D // f ⊥ = ⊥ }

The flat domain is free: functions α → D into a pointed domain are exactly the strict continuous maps Flat α →𝒄 D. The forward map extends by ⊥ ↦ ⊥, continuous by ωScottContinuous_of_monotone; the inverse precomposes with ↑.

Equations

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

Unification

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

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

Equations

• Flat.unify none y = some y
• Flat.unify (some a) none = some ↑a
• Flat.unify (some a) (some b) = if a = b then some ↑a else none

@[instance_reducible]

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

Equations

• Flat.instPartialUnifyOfDecidableEq = { unify := Flat.unify, isLUB_of_unify_eq_some := ⋯, isSome_unify_of_bddAbove := ⋯ }

theorem Flat.compat_iff {α : Type u_1} {x y : Flat α} [DecidableEq α] : 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.unify_eq_some_or_of_compat {α : Type u_1} [DecidableEq α] {x y : Flat α} (h : Compat x y) : PartialUnify.unify x y = Option.some (x.or y)

On compatible slots, unification is the priority union: agreeing commitments collapse and ⊥ defers, so the biased and unbiased merges coincide.

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_distinct_eq_none is the witness — distinct atoms have no upper bound, so the join the law would require is undefined.

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