Documentation

LeanPool.Lentil.ProofMode.Tactics.Revert

source
def TLA.ProofMode.binderNameHintAsString {α : Sort u_1} {β : Sort u_2} (_n : String) (p : α → β) :
α → β

Attach a binder-name hint without changing the underlying function.

Equations
Instances For
    source
    theorem TLA.ProofMode.Entails_revert_forall {σ : Type u} {hyps : List (NamedPred σ)} {α : Sort v} {p : α → pred σ} (n : String) :
    Entails hyps [tlafml|∀ x, ((binderNameHintAsString n p) x)] → ∀ (x : α), Entails hyps (p x)
    source
    theorem TLA.ProofMode.Entails_revert_by_idx {σ : Type u} {hyps : List (NamedPred σ)} {goal : pred σ} (idx : Nat) :
    Entails (hyps.eraseIdx idx) ((hyps.get?Internal idx).elim goal fun (r : NamedPred σ) => [tlafml|r.pred → goal]) → Entails hyps goal
    source
    theorem TLA.ProofMode.Entails_revert_by_name {σ : Type u} {hyps : List (NamedPred σ)} {goal : pred σ} (toRevert : String) :
    Entails (hyps.eraseIdx (List.findIdx (fun (h : NamedPred σ) => h.name == toRevert) hyps)) ((hyps.get?Internal (List.findIdx (fun (h : NamedPred σ) => h.name == toRevert) hyps)).elim goal fun (r : NamedPred σ) => [tlafml|r.pred → goal]) → Entails hyps goal
    source
    theorem TLA.ProofMode.Entails_revert_all {σ : Type u} {hyps : List (NamedPred σ)} {goal : pred σ} :
    Entails [] (repeatedImplies (List.map NamedPred.pred hyps) goal) → Entails hyps goal
    source
    def TLA.ProofMode.tlaRevertTac :
    Lean.ParserDescr

    tla_revert h₁ h₂ ... moves assumptions back into the proof-mode goal.

    If hp : p is a temporal hypothesis and the current goal is q, then

    tla_revert hp

    removes hp from the proof-mode context and changes the goal to p → q.

    Lean locals can also be reverted: a proof hP : P becomes a pure implication ⌞P⌟ → q, while a non-Prop local such as n : Nat becomes a universal quantifier in the goal.

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

      tla_revert_all moves every temporal hypothesis back into the proof-mode goal.

      For example, if the proof-mode context contains hp : p, hq : q, and the goal is r, then

      tla_revert_all

      leaves an empty temporal context and changes the goal to p → q → r. Lean-local variables and pure assumptions are not reverted; use tla_revert with explicit names for those.

      Equations
      Instances For