Documentation

LeanPool.Lentil.Gadgets.TheoremDeriving

Gadgets for providing different variants of a proven theorem.

source
def TLA.Deriving.assembleUnderCommonContextShape (σ : Lean.Expr) (ps : List Lean.Expr) (q : Lean.Expr) :
Lean.MetaM Lean.Expr

Assemble premises and a conclusion under a shared context Γ.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def TLA.Deriving.assembleSeparatedPredImplications (ps : List Lean.Expr) (q : Lean.Expr) :
    Lean.MetaM Lean.Expr

    Assemble a list of premise predicates and a conclusion into the arrow chain of separated predImplies/valid statements used by tla_derive.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def TLA.Deriving.assembleSeparatedPredImplications.simplify (ps : List Lean.Expr) (q : Lean.Expr) :
      Lean.MetaM (List Lean.Expr × Lean.Expr)

      Simplify a premise list and conclusion before assembling the implication chain.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def TLA.Deriving.deriveForPredImpliesOrValid (nm : Lean.Name) :
        Lean.CoreM Unit

        For a TLA theorem whose conclusion is a single TLA.predImplies or TLA.valid, this function automatically derives its several equivalent or weakened versions, which might be easier to use elsewhere.

        For example, consider the following statement:

        |-tla- ((p' ⇒ p) → (q ⇒ q') → (p ↝ q) ⇒ (p' ↝ q'))

        One useful, but weaker version is:

        (p') |-tla- (p) → (q) |-tla- (q') → (p ↝ q) |-tla- (p' ↝ q')

        which is derived by repeatly applying impl_decouple, impl_intro and always_intro.

        Another useful and equivalent version is:

        ∀ Γ, (Γ) |-tla- (p' ⇒ p) → (Γ) |-tla- (q ⇒ q') → (Γ) |-tla- ((p ↝ q) ⇒ (p' ↝ q'))

        which can be used in case we want to keep the context Γ.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def tlaDerive :
          Lean.ParserDescr

          For a TLA theorem with this attribute in the form of a single TLA.predImplies or TLA.valid, its different variants will be derived. See the docstring of TLA.Deriving.deriveForPredImpliesOrValid for more details.

          Equations
          Instances For