theorem TLA.ProofMode.Entails_rcases_and_by_idx {σ : Type u} {hyps : List (NamedPred σ)} {goal : pred σ} (name1 name2 : String) {a b : pred σ} (idx : Nat) (heq : Option.map NamedPred.pred hyps[idx]? = some [tlafml|a ∧ b]) : Entails (hyps.eraseIdx idx ++ [{ name := name1, pred := a }, { name := name2, pred := b }]) goal → Entails hyps goal

theorem TLA.ProofMode.Entails_rcases_and_by_name {σ : Type u} {hyps : List (NamedPred σ)} {goal : pred σ} (name1 name2 : String) {a b : pred σ} (chosen : String) (heq : Option.map NamedPred.pred hyps[List.findIdx (fun (h : NamedPred σ) => h.name == chosen) hyps]? = some [tlafml|a ∧ b]) : Entails (hyps.eraseIdx (List.findIdx (fun (h : NamedPred σ) => h.name == chosen) hyps) ++ [{ name := name1, pred := a }, { name := name2, pred := b }]) goal → Entails hyps goal

theorem TLA.ProofMode.Entails_rcases_or_by_idx {σ : Type u} {hyps : List (NamedPred σ)} {goal : pred σ} (name1 name2 : String) {a b : pred σ} (idx : Nat) (heq : Option.map NamedPred.pred hyps[idx]? = some [tlafml|a ∨ b]) : Entails (hyps.eraseIdx idx ++ [{ name := name1, pred := a }]) goal → Entails (hyps.eraseIdx idx ++ [{ name := name2, pred := b }]) goal → Entails hyps goal

theorem TLA.ProofMode.Entails_rcases_or_by_name {σ : Type u} {hyps : List (NamedPred σ)} {goal : pred σ} (name1 name2 : String) {a b : pred σ} (chosen : String) (heq : Option.map NamedPred.pred hyps[List.findIdx (fun (h : NamedPred σ) => h.name == chosen) hyps]? = some [tlafml|a ∨ b]) : Entails (hyps.eraseIdx (List.findIdx (fun (h : NamedPred σ) => h.name == chosen) hyps) ++ [{ name := name1, pred := a }]) goal → Entails (hyps.eraseIdx (List.findIdx (fun (h : NamedPred σ) => h.name == chosen) hyps) ++ [{ name := name2, pred := b }]) goal → Entails hyps goal

theorem TLA.ProofMode.Entails_rcases_exists_by_idx {σ : Type u} {hyps : List (NamedPred σ)} {goal : pred σ} (newName : String) {α : Sort v} {p : α → pred σ} (idx : Nat) (heq : Option.map NamedPred.pred hyps[idx]? = some [tlafml|∃ x, (p x)]) : (∀ (x : α), Entails (hyps.eraseIdx idx ++ [{ name := newName, pred := p x }]) goal) → Entails hyps goal

theorem TLA.ProofMode.Entails_rcases_exists_by_name {σ : Type u} {hyps : List (NamedPred σ)} {goal : pred σ} (newName : String) {α : Sort v} {p : α → pred σ} (chosen : String) (heq : Option.map NamedPred.pred hyps[List.findIdx (fun (h : NamedPred σ) => h.name == chosen) hyps]? = some [tlafml|∃ x, (p x)]) : (∀ (x : α), Entails (hyps.eraseIdx (List.findIdx (fun (h : NamedPred σ) => h.name == chosen) hyps) ++ [{ name := newName, pred := p x }]) goal) → Entails hyps goal

@[irreducible]

def TLA.ProofMode.syntaxNodeCount : Lean.Syntax → Nat

The number of syntax nodes in stx; used as a recursion-fuel bound when destructuring rcasesPat patterns (each sub-pattern is strictly smaller).

Equations

• TLA.ProofMode.syntaxNodeCount (Lean.Syntax.node info kind args) = Array.foldl (fun (acc : Nat) (s : Lean.Syntax) => acc + TLA.ProofMode.syntaxNodeCount s) 1 args
• TLA.ProofMode.syntaxNodeCount x✝ = 1

def TLA.ProofMode.tlaRcasesCoreFocused (fuel : Nat) (currentHyp : TemporalHypLoc) (pat : Lean.TSyntax `rcasesPat) : Lean.Elab.Tactic.TacticM Unit

Destructure the proof-mode hypothesis at currentHyp against pat. Precondition: the goal list contains exactly one goal — every caller enforces this by running through focus or Tactic.run. fuel bounds the pattern-nesting depth.

A tuple ⟨..⟩ destructures tlaAnd / tlaExists; a parenthesized alternation (.. | ..) case-splits a tlaOr, producing two subgoals.

def TLA.ProofMode.tlaRcasesCoreAllGoals (fuel : Nat) (currentHyp : TemporalHypLoc) (pat : Lean.TSyntax `rcasesPat) : Lean.Elab.Tactic.TacticM Unit

Run tlaRcasesCoreFocused on every current goal, collecting all resulting goals. Needed because an or-split multiplies goals, and sibling or subsequent patterns must then be applied to each of them.

Equations

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

def TLA.ProofMode.tlaRcasesCore (currentHyp : TemporalHypLoc) (pat : Lean.TSyntax `rcasesPat) : Lean.Elab.Tactic.TacticM Unit

Destructure the proof-mode hypothesis at currentHyp against pat, acting on the main goal and leaving any other goals untouched. This is the entry point; the recursive work happens in tlaRcasesCoreFocused.

Equations

• TLA.ProofMode.tlaRcasesCore currentHyp pat = Lean.Elab.Tactic.focus (TLA.ProofMode.tlaRcasesCoreFocused (TLA.ProofMode.syntaxNodeCount pat.raw + 1) currentHyp pat)

def TLA.ProofMode.tlaRcasesTac : Lean.ParserDescr

tla_rcases h with pat destructures a temporal hypothesis in the proof-mode context.

If h : p ∧ q, then

tla_rcases h with ⟨hp, hq⟩

removes h and adds hp : p and hq : q. If h : ∃ x, P x, then

tla_rcases h with ⟨x, hx⟩

introduces a Lean witness x and a temporal hypothesis hx : P x. If h : p ∨ q, then

tla_rcases h with (hp | hq)

case-splits into two subgoals, with hp : p in the first and hq : q in the second. A - pattern clears the targeted hypothesis:

tla_rcases h with -
tla_rcases h with ⟨ha, -⟩  -- destructure and discard the second conjunct

A numeric index can be used instead of a name:

tla_rcases 0 with ⟨hp, hq⟩

Equations

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

def TLA.ProofMode.tlaObtainTac : Lean.ParserDescr

tla_obtain pat := t adds the temporal fact proved by t and immediately destructures it with pat.

For example, if h : |-tla- (p ∧ q), then

tla_obtain ⟨hp, hq⟩ := h

adds hp : p and hq : q to the proof-mode context. If t proves an existential predicate, the pattern may introduce a Lean witness together with the temporal hypothesis for its body. A bare proof-mode hypothesis is destructured in place; other terms are first added as a new temporal hypothesis.

Equations

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

def TLA.ProofMode.tlaByCasesTac : Lean.ParserDescr

tla_by_cases h : p splits a proof-mode goal into the cases h : p and h : ¬ p.

For example,

tla_by_cases hp : p

creates two goals. The first has the temporal hypothesis hp : p; the second has hp : ¬ p.

Equations

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

def TLA.ProofMode.tlaRintroTac : Lean.ParserDescr

tla_rintro pat₁ pat₂ ... introduces proof-mode goal binders like tla_intro, but each introduced item may be immediately destructured.

For Lean binders and pure antecedents, the pattern is handled by Lean's rintro. For a temporal implication, the antecedent is introduced as a new temporal hypothesis and then destructured by tla_rcases.

For example, if the goal is (p ∧ q) → r, then

tla_rintro ⟨hp, hq⟩

adds hp : p and hq : q to the proof-mode context and changes the goal to r. If the goal is ∀ x, P x, then

tla_rintro x

introduces x as a Lean local and changes the goal to P x. A temporal antecedent p ∨ q can be case-split with a parenthesized alternation:

tla_rintro (hp | hq)

introduces the antecedent and splits into two subgoals.

Equations

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