theorem TLA.ProofMode.Entails_of_false_in_hyps {σ : Type u} {hyps : List (NamedPred σ)} {goal : pred σ} (idx : Nat) (h : Option.map NamedPred.pred hyps[idx]? = some [tlafml|⊥]) : Entails hyps goal

If the proof-mode context contains tlaFalse, every goal follows vacuously.

theorem TLA.ProofMode.Entails_of_contradicting_hyps {σ : Type u} {hyps : List (NamedPred σ)} {goal p : pred σ} (idx1 idx2 : Nat) (h1 : Option.map NamedPred.pred hyps[idx1]? = some p) (h2 : Option.map NamedPred.pred hyps[idx2]? = some [tlafml|¬p]) : Entails hyps goal

If the proof-mode context contains both p and ¬ p, every goal follows.

def TLA.ProofMode.tlaContradictionTac : Lean.ParserDescr

tla_contradiction closes any proof-mode goal whose context contains an explicit contradiction:

• a temporal hypothesis with predicate ⊥ (i.e. tlaFalse), or
• a pair of temporal hypotheses with predicates p and ¬ p.

It fails if neither pattern is found.

Equations

• TLA.ProofMode.tlaContradictionTac = Lean.ParserDescr.node `TLA.ProofMode.tlaContradictionTac 1024 (Lean.ParserDescr.nonReservedSymbol "tla_contradiction" false)