Additional Complete Lattice Operations

Extensions to Lean.Order.CompleteLattice providing additional operations needed for program verification.

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

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

def Lean.Order.«term⊤» : ParserDescr

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

theorem Lean.Order.le_top {α : Type u} [CompleteLattice α] (x : α) : PartialOrder.rel x top

@[implicit_reducible]

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

A complete lattice is a chain-complete partial order.

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

Binary meet (infimum)

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

Binary meet (infimum)

theorem Lean.Order.meet_le_left {α : Type u} [CompleteLattice α] (x y : α) : PartialOrder.rel (meet x y) x

theorem Lean.Order.meet_le_right {α : Type u} [CompleteLattice α] (x y : α) : PartialOrder.rel (meet x y) y

theorem Lean.Order.le_meet {α : Type u} [CompleteLattice α] (x y z : α) : PartialOrder.rel x y → PartialOrder.rel x z → PartialOrder.rel x (meet y z)

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

Binary join (supremum)

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

Binary join (supremum)

theorem Lean.Order.left_le_join {α : Type u} [CompleteLattice α] (x y : α) : PartialOrder.rel x (join x y)

theorem Lean.Order.right_le_join {α : Type u} [CompleteLattice α] (x y : α) : PartialOrder.rel y (join x y)

theorem Lean.Order.join_le {α : Type u} [CompleteLattice α] (x y z : α) : PartialOrder.rel x z → PartialOrder.rel y z → PartialOrder.rel (join x y) z

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

Indexed infimum

theorem Lean.Order.iInf_le {α : Type u} [CompleteLattice α] {ι : Type v} (f : ι → α) (i : ι) : PartialOrder.rel (iInf f) (f i)

theorem Lean.Order.le_iInf {α : Type u} [CompleteLattice α] {ι : Type v} (f : ι → α) (x : α) : (∀ (i : ι), PartialOrder.rel x (f i)) → PartialOrder.rel x (iInf f)

@[simp]

theorem Lean.Order.iInf_fun_apply {ι : Type v} {σ : Type w} {β : Type u} [CompleteLattice β] (f : ι → σ → β) (s : σ) : iInf f s = iInf fun (i : ι) => f i s

Pointwise characterization of indexed infimum on function lattices.

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

Indexed supremum

theorem Lean.Order.le_iSup {α : Type u} [CompleteLattice α] {ι : Type v} (f : ι → α) (i : ι) : PartialOrder.rel (f i) (iSup f)

theorem Lean.Order.iSup_le {α : Type u} [CompleteLattice α] {ι : Type v} (f : ι → α) (x : α) : (∀ (i : ι), PartialOrder.rel (f i) x) → PartialOrder.rel (iSup f) x

theorem Lean.Order.sup_fun_apply {σ : Type v} {β : Type w} [CompleteLattice β] (c : (σ → β) → Prop) (s : σ) : CompleteLattice.sup c s = CompleteLattice.sup fun (y : β) => ∃ (f : σ → β), c f ∧ f s = y

Pointwise characterization of CompleteLattice.sup on function lattices: (sup c) s = sup (fun y => ∃ f, c f ∧ f s = y).

@[simp]

theorem Lean.Order.meet_fun_apply {σ : Type v} {β : Type w} [CompleteLattice β] (a b : σ → β) (s : σ) : meet a b s = meet (a s) (b s)

Pointwise characterization of binary meet on function lattices.

@[simp]

theorem Lean.Order.join_fun_apply {σ : Type v} {β : Type w} [CompleteLattice β] (a b : σ → β) (s : σ) : join a b s = join (a s) (b s)

Pointwise characterization of binary join on function lattices.

Prop Embedding into Partial Order

Embedding propositions into a partial order with top and bottom.

CompleteLattice instance for Prop

We define a CompleteLattice structure on Prop where:

• rel is implication (→)
• sup is existential quantification over the predicate

@[implicit_reducible]

instance Lean.Order.instPartialOrderProp_std : PartialOrder Prop

def Lean.Order.propSup (c : Prop → Prop) : Prop

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

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

@[implicit_reducible]

instance Lean.Order.instCompleteLatticeProp_std : CompleteLattice Prop

theorem Lean.Order.prop_pre_intro (x y : Prop) : (x → PartialOrder.rel True y) → PartialOrder.rel x y

theorem Lean.Order.prop_pre_elim (x : Prop) : x → PartialOrder.rel True x

@[simp]

theorem Lean.Order.iInf_prop_eq_forall {ι : Type u} (f : ι → Prop) : iInf f = ∀ (i : ι), f i

@[simp]

theorem Lean.Order.meet_prop_eq_and (a b : Prop) : meet a b = (a ∧ b)

@[simp]

theorem Lean.Order.join_prop_eq_or (a b : Prop) : join a b = (a ∨ b)

Assertion

The Assertion class and Assertion.ofProp embedding.

class Std.Internal.Do.Assertion (α : Type w) extends Lean.Order.CompleteLattice α : Type w

An assertion type is equipped with a CompleteLattice structure, used as the carrier for pre- and postconditions.

• rel : α → α → Prop
• rel_refl {x : α} : rel x x
• rel_trans {x y z : α} : rel x y → rel y z → rel x z
• rel_antisymm {x y : α} : rel x y → rel y x → x = y
• has_sup (c : α → Prop) : Exists (is_sup c)

@[implicit_reducible]

def Std.Internal.Do.instCCPOOfAssertion {EPred : Type u_1} [Assertion EPred] : Lean.Order.CCPO EPred

An assertion type is a chain-complete partial order.

noncomputable def Std.Internal.Do.Assertion.ofProp {l : Type u_1} [Assertion l] (p : Prop) : l

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

def Std.Internal.Do.«term⌜_⌝» : Lean.ParserDescr

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

@[simp]

theorem Std.Internal.Do.Assertion.ofProp_true (l : Type v) [Assertion l] : ofProp True = Lean.Order.top

@[simp]

theorem Std.Internal.Do.Assertion.ofProp_false (l : Type v) [Assertion l] : ofProp False = Lean.Order.bot

theorem Std.Internal.Do.Assertion.ofProp_imp {l : Type u_1} [Assertion l] (p₁ p₂ : Prop) : (p₁ → p₂) → Lean.Order.PartialOrder.rel (ofProp p₁) (ofProp p₂)

@[simp]

theorem Std.Internal.Do.Assertion.ofProp_intro {l : Type u_1} [Assertion l] (p : Prop) (h : l) : Lean.Order.PartialOrder.rel (ofProp p) h = (p → Lean.Order.PartialOrder.rel Lean.Order.top h)

@[simp]

theorem Std.Internal.Do.Assertion.ofProp_intro_l {l : Type u_1} [Assertion l] (p : Prop) (x y : l) : Lean.Order.PartialOrder.rel (Lean.Order.meet x (ofProp p)) y = (p → Lean.Order.PartialOrder.rel x y)

@[simp]

theorem Std.Internal.Do.Assertion.ofProp_intro_r {l : Type u_1} [Assertion l] (p : Prop) (x y : l) : Lean.Order.PartialOrder.rel (Lean.Order.meet (ofProp p) x) y = (p → Lean.Order.PartialOrder.rel x y)