Documentation

Loom.LatticeExt

Additional Complete Lattice Operations #

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

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

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

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

    Prop Embedding into Partial Order #

    Embedding propositions into a partial order with top and bottom.

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

    Pure embedding of propositions into a complete lattice.

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

      Pure embedding of propositions into a complete lattice.

      Instances For
        source
        @[simp]
        theorem Lean.Order.trueE (l : Type v) [CompleteLattice l] :
        CompleteLattice.pure True = top
        source
        @[simp]
        theorem Lean.Order.falseE (l : Type v) [CompleteLattice l] :
        CompleteLattice.pure False = latticeBot
        source
        theorem Lean.Order.LE.pure_imp {l : Type u} [CompleteLattice l] (p₁ p₂ : Prop) :
        (p₁ → p₂) → PartialOrder.rel (CompleteLattice.pure p₁) (CompleteLattice.pure p₂)
        source
        @[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 top h)
        source
        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.

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

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

        source
        theorem Lean.Order.bot_fun_apply {σ : Type v} {β : Type w} [CompleteLattice β] (s : σ) :
        latticeBot s = latticeBot
        source
        @[simp]
        theorem Lean.Order.pure_fun_apply {σ : Type v} {β : Type w} [CompleteLattice β] (p : Prop) (s : σ) :
        CompleteLattice.pure p s = CompleteLattice.pure p
        source
        @[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)
        source
        @[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:

        source
        theorem Lean.Order.loom_prop_pre_intro (x y : Prop) :
        (x → PartialOrder.rel True y) → PartialOrder.rel x y
        source
        theorem Lean.Order.loom_prop_pre_elim (x : Prop) :
        x → PartialOrder.rel True x
        source
        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.

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

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