Additional Complete Lattice Operations

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

noncomputable def Lean.Order.latticeTop {α : 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 latticeTop

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

Bottom element of a complete lattice (infimum of all elements)

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

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.

noncomputable def Lean.Order.CompleteLattice.pure {l : Type u} [CompleteLattice l] : Prop → l

Pure embedding of propositions into a complete lattice.

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

Pure embedding of propositions into a complete lattice.

@[simp]

theorem Lean.Order.trueE (l : Type v) [CompleteLattice l] : CompleteLattice.pure True = latticeTop

@[simp]

theorem Lean.Order.falseE (l : Type v) [CompleteLattice l] : CompleteLattice.pure False = latticeBot

theorem Lean.Order.LE.pure_imp {l : Type u} [CompleteLattice l] (p₁ p₂ : Prop) : (p₁ → p₂) → PartialOrder.rel (CompleteLattice.pure p₁) (CompleteLattice.pure p₂)

@[simp]

theorem Lean.Order.LE.pure_intro {l : Type u} [CompleteLattice l] (p : Prop) (h : l) : PartialOrder.rel (CompleteLattice.pure p) h = (p → PartialOrder.rel latticeTop h)

theorem Lean.Order.le_pure {l : Type u} [CompleteLattice l] (x : l) (p : Prop) : p → PartialOrder.rel x (CompleteLattice.pure p)

Proving pre ⊑ ⌜p⌝ reduces to proving p.

theorem Lean.Order.top_fun_apply {σ : Type v} {β : Type w} [CompleteLattice β] (s : σ) : latticeTop s = latticeTop

Pointwise characterization of ⌜p⌝ on function lattices: (⌜p⌝ : σ → β) s = (⌜p⌝ : β).

theorem Lean.Order.bot_fun_apply {σ : Type v} {β : Type w} [CompleteLattice β] (s : σ) : latticeBot s = latticeBot

@[simp]

theorem Lean.Order.pure_fun_apply {σ : Type v} {β : Type w} [CompleteLattice β] (p : Prop) (s : σ) : CompleteLattice.pure p s = CompleteLattice.pure p

@[simp]

theorem Lean.Order.pure_intro_l {l : Type u} [CompleteLattice l] (p : Prop) (x y : l) : PartialOrder.rel (meet x (CompleteLattice.pure p)) y = (p → PartialOrder.rel x y)

@[simp]

theorem Lean.Order.pure_intro_r {l : Type u} [CompleteLattice l] (p : Prop) (x y : l) : PartialOrder.rel (meet (CompleteLattice.pure p) x) y = (p → PartialOrder.rel x y)

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_loom : 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_loom : 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

theorem Lean.Order.meet_pre_intro (a b c : Prop) : (a → PartialOrder.rel b c) → PartialOrder.rel (meet a b) c

Intro the left component of a meet precondition: a ⊓ b ⊑ c becomes a → b ⊑ c.

theorem Lean.Order.meet_pre_intro' (a b c : Prop) : (b → PartialOrder.rel a c) → PartialOrder.rel (meet a b) c

Intro the right component of a meet precondition: a ⊓ b ⊑ c becomes a → b ⊑ c.

theorem Lean.Order.true_meet_pre_elim (b c : Prop) : PartialOrder.rel b c → PartialOrder.rel (meet True b) c

Eliminate True from the left of a meet precondition.

@[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)