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

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

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

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_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

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

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

@[simp]

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

Pointwise characterization of indexed supremum on function lattices.

theorem Lean.Order.sup_apply {σ : Type v} {β : σ → Type w} [(s : σ) → CompleteLattice (β s)] (c : ((s : σ) → β s) → Prop) (s : σ) : CompleteLattice.sup c s = CompleteLattice.sup fun (y : β s) => ∃ (f : (s : σ) → β s), 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_apply {σ : Type v} {β : σ → Type w} [(s : σ) → CompleteLattice (β s)] (a b : (s : σ) → β s) (s : σ) : meet a b s = meet (a s) (b s)

Pointwise characterization of binary meet on function lattices.

@[simp]

theorem Lean.Order.join_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.

@[simp]

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

Pointwise characterization of ⊤ on a function lattice.

@[simp]

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

Pointwise characterization of ⊥ on a function lattice.

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

@[instance_reducible]

instance Lean.Order.instPartialOrderProp_std : PartialOrder Prop

@[simp]

theorem Lean.Order.le_prop_eq_imp (p q : Prop) : PartialOrder.rel p q = (p → q)

theorem Lean.Order.le_pi_eq_forall {σ : Type v} {β : σ → Type w} [(s : σ) → PartialOrder (β s)] (a b : (s : σ) → β s) : PartialOrder.rel a b = ∀ (s : σ), PartialOrder.rel (a s) (b s)

Entailment on a function lattice is pointwise. β is recoverable from the operands' types, so unlike a carrier-only parameter this is a usable @[grind =] trigger; it lets grind push ⊑ through a state argument down to the base lattice.

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)

@[instance_reducible]

instance Lean.Order.instCompleteLatticeProp_std : CompleteLattice Prop

theorem Lean.Order.le_of_imp_top_le (x y : Prop) : (x → PartialOrder.rel top y) → PartialOrder.rel x y

theorem Lean.Order.top_le_prop (x : Prop) : x → PartialOrder.rel top x

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

theorem Lean.Order.of_top_le_prop {x : Prop} : PartialOrder.rel top x → x

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

@[simp]

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

theorem Lean.Order.le_forall {α : Sort u} (p : Prop) (q : α → Prop) (h : ∀ (x : α), PartialOrder.rel p (q x)) : PartialOrder.rel p (∀ (x : α), q x)

Introduction rule for a ∀ on the RHS of a Prop entailment.

@[simp]

theorem Lean.Order.iSup_prop_eq_exists {ι : Type u} (f : ι → Prop) : iSup 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)

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.

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

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

@[simp]

theorem Lean.Order.CompleteLattice.ofProp_true (l : Type v) [CompleteLattice l] : ofProp True = top

@[simp]

theorem Lean.Order.CompleteLattice.ofProp_false (l : Type v) [CompleteLattice l] : ofProp False = bot

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Lean.Order.CompleteLattice.ofProp_apply {σ : Type v} {β : Type u} [CompleteLattice β] (p : Prop) (s : σ) : ofProp p s = ofProp p

Pointwise characterization of CompleteLattice.ofProp on a function lattice.

theorem Lean.Order.top_le_ofProp {l : Type u_1} [CompleteLattice l] (p : Prop) : p → PartialOrder.rel top (CompleteLattice.ofProp p)

theorem Lean.Order.le_ofProp {l : Type u_1} [CompleteLattice l] (x : l) (p : Prop) : p → PartialOrder.rel x (CompleteLattice.ofProp p)

x ⊑ ⌜p⌝ whenever p holds.

theorem Lean.Order.ofProp_le {l : Type u_1} [CompleteLattice l] (p : Prop) (rhs : l) : (p → PartialOrder.rel top rhs) → PartialOrder.rel (CompleteLattice.ofProp p) rhs

⌜p⌝ ⊑ rhs reduces to assuming p and proving ⊤ ⊑ rhs.

theorem Lean.Order.ofProp_meet_le {l : Type u_1} [CompleteLattice l] (p : Prop) (x rhs : l) : (p → PartialOrder.rel x rhs) → PartialOrder.rel (meet (CompleteLattice.ofProp p) x) rhs

⌜p⌝ ⊓ x ⊑ rhs reduces to assuming p and proving x ⊑ rhs.

theorem Lean.Order.le_iff_forall_le {σ : Type u} {α : Type v} [PartialOrder α] {f g : σ → α} : PartialOrder.rel f g ↔ ∀ (s : σ), PartialOrder.rel (f s) (g s)

Entailment between functions is pointwise.

theorem Lean.Order.le_of_forall_le {σ : Type u} {α : Type v} [PartialOrder α] {f g : σ → α} : (∀ (s : σ), PartialOrder.rel (f s) (g s)) → PartialOrder.rel f g

Entailment between functions follows from pointwise entailment.

theorem Lean.Order.top_le_of_forall_top_le {σ : Type u} {α : Type v} [CompleteLattice α] {g : σ → α} : (∀ (s : σ), PartialOrder.rel top (g s)) → PartialOrder.rel top g

⊤ ⊑ g for a function g follows from pointwise ⊤ ⊑ g s.

@[simp]

theorem Lean.Order.top_prop_eq : top = True

The top element of the Prop lattice is True. Not a global @[simp] lemma: collapsing the lattice ⊤/⊥/⌜·⌝ to True/False/p would change how mvcgen discharge lattice goals. Tagged @[grind =] for use under grind.

@[simp]

theorem Lean.Order.bot_prop_eq : bot = False

The bottom element of the Prop lattice is False. See top_prop_eq for why this is not @[simp].

@[simp]

theorem Lean.Order.ofProp_prop_eq (p : Prop) : CompleteLattice.ofProp p = p

Embedding a proposition into the Prop lattice (⌜p⌝) is the proposition itself. See top_prop_eq for why this is not @[simp].

Prop-valued, fixed-arity specializations of CompleteLattice.ofProp_apply: ⌜p⌝ at a state-indexed Prop lattice, applied to its states, is p. Fixing the carrier to Prop (a ground instance) leaves every parameter recoverable from the trigger, so these are usable @[grind =] lemmas where the general ofProp_apply is not. They reduce a guard straight to its Prop in one step, avoiding the intermediate (⌜p⌝ : Prop) whose instance ofProp_prop_eq fails to match.

theorem Lean.Order.CompleteLattice.ofProp_apply_1 {σ₁ : Type u_1} (p : Prop) (s₁ : σ₁) : ofProp p s₁ = p

theorem Lean.Order.CompleteLattice.ofProp_apply_2 {σ₁ : Type u_1} {σ₂ : Type u_2} (p : Prop) (s₁ : σ₁) (s₂ : σ₂) : ofProp p s₁ s₂ = p

theorem Lean.Order.CompleteLattice.ofProp_apply_3 {σ₁ : Type u_1} {σ₂ : Type u_2} {σ₃ : Type u_3} (p : Prop) (s₁ : σ₁) (s₂ : σ₂) (s₃ : σ₃) : ofProp p s₁ s₂ s₃ = p

theorem Lean.Order.CompleteLattice.ofProp_apply_4 {σ₁ : Type u_1} {σ₂ : Type u_2} {σ₃ : Type u_3} {σ₄ : Type u_4} (p : Prop) (s₁ : σ₁) (s₂ : σ₂) (s₃ : σ₃) (s₄ : σ₄) : ofProp p s₁ s₂ s₃ s₄ = p

theorem Lean.Order.CompleteLattice.ofProp_apply_5 {σ₁ : Type u_1} {σ₂ : Type u_2} {σ₃ : Type u_3} {σ₄ : Type u_4} {σ₅ : Type u_5} (p : Prop) (s₁ : σ₁) (s₂ : σ₂) (s₃ : σ₃) (s₄ : σ₄) (s₅ : σ₅) : ofProp p s₁ s₂ s₃ s₄ s₅ = p