theorem TLA.ProofMode.Entails_pull_pure {σ : Type u} {hyps : List (NamedPred σ)} {goal : pred σ} (toPull : String) {q : Prop} : Option.map NamedPred.pred hyps[List.findIdx (fun (h : NamedPred σ) => h.name == toPull) hyps]? = some [tlafml|⌞ q ⌟] → (q → Entails (hyps.eraseIdx (List.findIdx (fun (h : NamedPred σ) => h.name == toPull) hyps)) goal) → Entails hyps goal

Pull a pure-fact hypothesis ⟨h, ⌞q⌟⟩ from the temporal context into Lean's local context.

The dedicated soundness theorem is built by composing the soundness of tla_revert (which moves the temporal hyp into a ⌞q⌟ → goal antecedent) and tla_intro's Entails_pure_fact_intro (which converts a Entails Γ (⌞q⌟ → goal) to a Lean-level q → Entails Γ goal). Inlining the composition here keeps the proof term short.

def TLA.ProofMode.tlaPullPureTac : Lean.ParserDescr

tla_pull_pure h₁ h₂ ... moves pure temporal hypotheses into Lean's local context.

For example, if the proof-mode context contains hP : ⌞P⌟, then

tla_pull_pure hP

removes hP from the temporal context and introduces a Lean local hP : P.

Equations

• One or more equations did not get rendered due to their size.

def TLA.ProofMode.tacticTlaProvePure : Lean.ParserDescr

tlaProvePure proves a pure TLA entailment by reducing it to an ordinary Lean proposition.

For example, on a goal whose temporal conclusion is ⌞P⌟,

tlaProvePure

changes the remaining obligation to the Lean proposition P.

Equations

• TLA.ProofMode.tacticTlaProvePure = Lean.ParserDescr.node `TLA.ProofMode.tacticTlaProvePure 1024 (Lean.ParserDescr.nonReservedSymbol "tlaProvePure" false)