Complete lattices

The definitions and instances of the lattice theory: the operations of a complete lattice, the complete lattice of propositions, the embedding ⌜·⌝ of propositions, supremum-preserving maps with their upper adjoints, and Heyting implication ⇨.

Additional operations of a complete lattice

The top element ⊤, the binary meet ⊓ and join ⊔, and the indexed infimum ⨅ and supremum ⨆. The bottom element ⊥ comes from CCPO, which every complete lattice is.

noncomputable def Lean.Order.top {α : Type u} [CompleteLattice α] : α

Top element of a complete lattice (supremum of all elements)

Equations

• Lean.Order.top = Lean.Order.CompleteLattice.sup fun (x : α) => True

def Lean.Order.«term⊤» : ParserDescr

Top element of a complete lattice (supremum of all elements)

Equations

• Lean.Order.«term⊤» = Lean.ParserDescr.node `Lean.Order.«term⊤» 1024 (Lean.ParserDescr.symbol "⊤")

@[instance_reducible]

noncomputable def Lean.Order.instCCPOOfCompleteLattice {α : Type u} [CompleteLattice α] : CCPO α

A complete lattice is a chain-complete partial order.

Equations

• Lean.Order.instCCPOOfCompleteLattice = { toPartialOrder := inst✝.toPartialOrder, has_csup := ⋯ }

noncomputable def Lean.Order.meet {α : Type u} [CompleteLattice α] (x y : α) : α

Binary meet (infimum)

Equations

• Lean.Order.meet x y = Lean.Order.inf fun (z : α) => z = x ∨ z = y

def Lean.Order.«term_⊓_» : TrailingParserDescr

Binary meet (infimum)

Equations

• Lean.Order.«term_⊓_» = Lean.ParserDescr.trailingNode `Lean.Order.«term_⊓_» 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊓ ") (Lean.ParserDescr.cat `term 71))

noncomputable def Lean.Order.join {α : Type u} [CompleteLattice α] (x y : α) : α

Binary join (supremum)

Equations

• Lean.Order.join x y = Lean.Order.CompleteLattice.sup fun (z : α) => z = x ∨ z = y

def Lean.Order.«term_⊔_» : TrailingParserDescr

Binary join (supremum)

Equations

• Lean.Order.«term_⊔_» = Lean.ParserDescr.trailingNode `Lean.Order.«term_⊔_» 65 65 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊔ ") (Lean.ParserDescr.cat `term 66))

noncomputable def Lean.Order.iInf {α : Type u} [CompleteLattice α] {ι : Sort v} (f : ι → α) : α

Indexed infimum

Equations

• Lean.Order.iInf f = Lean.Order.inf fun (x : α) => ∃ (i : ι), f i = x

def Lean.Order.«term⨅_,_» : ParserDescr

Indexed infimum

Equations

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

noncomputable def Lean.Order.iSup {α : Type u} [CompleteLattice α] {ι : Sort v} (f : ι → α) : α

Indexed supremum

Equations

• Lean.Order.iSup f = Lean.Order.CompleteLattice.sup fun (x : α) => ∃ (i : ι), f i = x

def Lean.Order.«term⨆_,_» : ParserDescr

Indexed supremum

Equations

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

The complete lattice of propositions

⊑ is implication and the supremum of a set of propositions is the existential quantifier over it.

The instances are scoped in Std.Internal.Order, outside of Lean.Order. partial_fixpoint and coinductive_fixpoint order Prop by ImplicationOrder and ReverseImplicationOrder, and their monotonicity lemmas live in Lean.Order itself. Open Std.Internal.Order to order Prop by implication.

@[instance_reducible]

def Std.Internal.Order.instPartialOrderProp : Lean.Order.PartialOrder Prop

Equations

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

def Std.Internal.Order.propSup (c : Prop → Prop) : Prop

Supremum for Prop: true iff some element of the set is true

Equations

• Std.Internal.Order.propSup c = ∃ (p : Prop), c p ∧ p

theorem Std.Internal.Order.propSup_is_sup (c : Prop → Prop) : Lean.Order.is_sup c (propSup c)

@[instance_reducible]

def Std.Internal.Order.instCompleteLatticeProp : Lean.Order.CompleteLattice Prop

Equations

• Std.Internal.Order.instCompleteLatticeProp = { toPartialOrder := Std.Internal.Order.instPartialOrderProp, has_sup := Std.Internal.Order.instCompleteLatticeProp._proof_1 }

Embedding of propositions

⌜p⌝ embeds a proposition p into an assertion lattice as ⊤ if p holds and ⊥ otherwise.

noncomputable def Lean.Order.CompleteLattice.ofProp {l : Type u_1} [CompleteLattice l] (p : Prop) : l

Embedding of propositions into an CompleteLattice type. ⌜p⌝ embeds p : Prop as ⊤ if p holds and ⊥ otherwise.

Equations

• Lean.Order.CompleteLattice.ofProp p = if p then Lean.Order.top else Lean.Order.bot

def Lean.Order.«term⌜_⌝» : ParserDescr

Embedding of propositions into an CompleteLattice type. ⌜p⌝ embeds p : Prop as ⊤ if p holds and ⊥ otherwise.

Equations

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

Supremum-preserving maps and Heyting implication

A supremum-preserving map on a complete lattice is a lower adjoint. Its upper adjoint is the implication belonging to it: Heyting ⇨ for the lattice meet, a magic wand for a separating conjunction.

class Lean.Order.PreservesSup {α : Type u} [CompleteLattice α] (f : α → α) : Prop

f : α → α preserves suprema if it distributes over arbitrary suprema: f (sup s) = sup { f x | x ∈ s }. Equivalently f is a lower adjoint, so it has an upper adjoint PreservesSup.upperAdjoint f.

A frame operator acts by a supremum-preserving map for each resource r: the lattice meet (a ⊓ ·), or a cost combinator (costConj r) for a counter resource. The upper adjoint is the corresponding implication: Heyting ⇨ for the meet, a magic wand for separating conjunction.

• map_sup (s : α → Prop) : f (CompleteLattice.sup s) = CompleteLattice.sup fun (y : α) => ∃ (x : α), s x ∧ y = f x

  f preserves joins.

noncomputable def Lean.Order.PreservesSup.upperAdjoint {α : Type u} [CompleteLattice α] (f : α → α) (b : α) : α

The upper adjoint of f: the join of all x with f x ⊑ b. For f = (a ⊓ ·) this is Heyting implication a ⇨ ·.

Equations

• Lean.Order.PreservesSup.upperAdjoint f b = Lean.Order.CompleteLattice.sup fun (x : α) => Lean.Order.PartialOrder.rel (f x) b

theorem Lean.Order.PreservesSup.le_upperAdjoint {α : Type u} [CompleteLattice α] (f : α → α) {b x : α} (h : PartialOrder.rel (f x) b) : PartialOrder.rel x (upperAdjoint f b)

Unit, free from the definition of upperAdjoint: f x ⊑ b → x ⊑ upperAdjoint f b. Needs only CompleteLattice.

@[reducible, inline]

abbrev Lean.Order.Heyting (α : Type u) [CompleteLattice α] : Prop

A complete lattice whose meets preserve suprema. The Heyting implication ⇨ is then a right adjoint, and ⊓ distributes over suprema of arbitrary families. The literature also calls such a lattice a frame.

Equations

• Lean.Order.Heyting α = ∀ (a : α), Lean.Order.PreservesSup (Lean.Order.meet a)

noncomputable def Lean.Order.himp {α : Type u} [CompleteLattice α] (a b : α) : α

Heyting implication: the upper adjoint of the lattice meet. For Prop it is →.

Equations

• Lean.Order.himp a b = Lean.Order.PreservesSup.upperAdjoint (Lean.Order.meet a) b

def Lean.Order.«term_⇨_» : TrailingParserDescr

Heyting implication: the upper adjoint of the lattice meet. For Prop it is →.

Equations

• Lean.Order.«term_⇨_» = Lean.ParserDescr.trailingNode `Lean.Order.«term_⇨_» 60 61 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⇨ ") (Lean.ParserDescr.cat `term 60))