Embedding of propositions into a complete lattice

⌜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.

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

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

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

theorem Lean.Order.ofProp_elim {l : Type u} [CompleteLattice l] {Q R : l} {φ : Prop} (h1 : PartialOrder.rel Q (CompleteLattice.ofProp φ)) (h2 : φ → PartialOrder.rel Q R) : PartialOrder.rel Q R

theorem Lean.Order.ofProp_mono {l : Type u} [CompleteLattice l] {φ₁ φ₂ : Prop} (h : φ₁ → φ₂) : PartialOrder.rel (CompleteLattice.ofProp φ₁) (CompleteLattice.ofProp φ₂)

theorem Lean.Order.ofProp_congr {l : Type u} [CompleteLattice l] {φ₁ φ₂ : Prop} (h : φ₁ ↔ φ₂) : CompleteLattice.ofProp φ₁ = CompleteLattice.ofProp φ₂

theorem Lean.Order.ofProp_meet_le_left {l : Type u} [CompleteLattice l] {Q R : l} {φ : Prop} (h : φ → PartialOrder.rel Q R) : PartialOrder.rel (meet (CompleteLattice.ofProp φ) Q) R

theorem Lean.Order.ofProp_meet_le_right {l : Type u} [CompleteLattice l] {Q R : l} {φ : Prop} (h : φ → PartialOrder.rel Q R) : PartialOrder.rel (meet Q (CompleteLattice.ofProp φ)) R

theorem Lean.Order.ofProp_eq_top {l : Type u} [CompleteLattice l] {φ : Prop} (h : φ) : CompleteLattice.ofProp φ = top

theorem Lean.Order.ofProp_and {l : Type u} [CompleteLattice l] {φ₁ φ₂ : Prop} : meet (CompleteLattice.ofProp φ₁) (CompleteLattice.ofProp φ₂) = CompleteLattice.ofProp (φ₁ ∧ φ₂)

theorem Lean.Order.ofProp_or {l : Type u} [CompleteLattice l] {φ₁ φ₂ : Prop} : join (CompleteLattice.ofProp φ₁) (CompleteLattice.ofProp φ₂) = CompleteLattice.ofProp (φ₁ ∨ φ₂)

theorem Lean.Order.ofProp_forall_le {l : Type u} [CompleteLattice l] {β : Type u_1} {Φ : β → Prop} : PartialOrder.rel (CompleteLattice.ofProp (∀ (x : β), Φ x)) (iInf fun (x : β) => CompleteLattice.ofProp (Φ x))

theorem Lean.Order.ofProp_exists {l : Type u} [CompleteLattice l] {β : Type u_1} {Φ : β → Prop} : (iSup fun (x : β) => CompleteLattice.ofProp (Φ x)) = CompleteLattice.ofProp (∃ (x : β), Φ x)

theorem Lean.Order.ofProp_forall {l : Type u} [CompleteLattice l] {β : Type u_1} {Φ : β → Prop} : (iInf fun (x : β) => CompleteLattice.ofProp (Φ x)) = CompleteLattice.ofProp (∀ (x : β), Φ x)

theorem Lean.Order.le_apply_of_point_meet_le {σ : Type u} {β : Type v} [CompleteLattice β] (s : σ) (pre : β) (Q : σ → β) (h : PartialOrder.rel (fun (u : σ) => meet (CompleteLattice.ofProp (u = s)) pre) Q) : PartialOrder.rel pre (Q s)

Frame a single state coordinate: from the function-order premise (fun u => ⌜u = s⌝ ⊓ pre) ⊑ Q conclude the point entailment pre ⊑ Q s. Instantiating the premise at u := s collapses ⌜s = s⌝ ⊓ pre to pre. Iterating it over a state chain point-frames pre ⊑ Q s₁ … sₙ to the function-order goal (fun u⃗ => ⌜u⃗ = s⃗⌝ ⊓ pre) ⊑ Q.