Documentation

LeanPool.Lentil.ProofMode.Tactics.Revert

source
theorem TLA.ProofMode.Entails_revert_forall {σ : Type u} {hyps : List (NamedPred σ)} {α : Sort v} {p : α → pred σ} (n : String) :
Entails hyps [tlafml|∀ x, ((TLA.ProofMode.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