theorem TLA.ProofMode.Entails_add_new {σ : Type u} {hyps : List (NamedPred σ)} {goal : pred σ} (subHyps : List (pred σ)) (hinc : subHyps ⊆ List.map NamedPred.pred hyps) (newHypName : String) (newHyp : pred σ) : ((repeatedAnd subHyps)) |-tla- (newHyp) → Entails (hyps ++ [{ name := newHypName, pred := newHyp }]) goal → Entails hyps goal

The general thing used in apply, have and suffices.

def TLA.ProofMode.replaceChosenPred {σ : Type u} (hyps : List (NamedPred σ)) (chosen : String) (newHyp : pred σ) : List (NamedPred σ)

Replace the chosen hypothesis predicate with a new one.

Equations

• TLA.ProofMode.replaceChosenPred hyps chosen newHyp = TLA.ProofMode.modifyHypByName hyps chosen fun (h : TLA.ProofMode.NamedPred σ) => { name := h.name, pred := newHyp }

theorem TLA.ProofMode.Entails_specialize_forall_by_name {σ : Type u} {hyps : List (NamedPred σ)} {goal : pred σ} {α : Sort v} {p : α → pred σ} (witness : α) (chosen : String) (hpred : List.find? (fun (h : NamedPred σ) => h.name == chosen) hyps = some { name := chosen, pred := [tlafml|∀ x, (p x)] }) : Entails (replaceChosenPred hyps chosen (p witness)) goal → Entails hyps goal

theorem TLA.ProofMode.Entails_specialize_forall_by_idx {σ : Type u} {hyps : List (NamedPred σ)} {goal : pred σ} {α : Sort v} {p : α → pred σ} (witness : α) (idx : Nat) (hpred : Option.map NamedPred.pred hyps[idx]? = some [tlafml|∀ x, (p x)]) : Entails (hyps.modify idx fun (x : NamedPred σ) => match x with | { name := name, pred := pred } => { name := name, pred := p witness }) goal → Entails hyps goal

theorem TLA.ProofMode.Entails_specialize_pure_by_name {σ : Type u} {hyps : List (NamedPred σ)} {goal rhs : pred σ} {q : Prop} (hq : q) (chosen : String) (hpred : List.find? (fun (h : NamedPred σ) => h.name == chosen) hyps = some { name := chosen, pred := [tlafml|⌞ q ⌟ → rhs] }) : Entails (replaceChosenPred hyps chosen rhs) goal → Entails hyps goal

theorem TLA.ProofMode.Entails_specialize_pure_by_idx {σ : Type u} {hyps : List (NamedPred σ)} {goal rhs : pred σ} {q : Prop} (hq : q) (idx : Nat) (hpred : Option.map NamedPred.pred hyps[idx]? = some [tlafml|⌞ q ⌟ → rhs]) : Entails (hyps.modify idx fun (x : NamedPred σ) => match x with | { name := name, pred := pred } => { name := name, pred := rhs }) goal → Entails hyps goal

theorem TLA.ProofMode.Entails_specialize_valid_by_name {σ : Type u} {hyps : List (NamedPred σ)} {goal lhs rhs : pred σ} (hlhs : |-tla- (lhs)) (chosen : String) (hpred : List.find? (fun (h : NamedPred σ) => h.name == chosen) hyps = some { name := chosen, pred := [tlafml|lhs → rhs] }) : Entails (replaceChosenPred hyps chosen rhs) goal → Entails hyps goal

theorem TLA.ProofMode.Entails_specialize_valid_by_idx {σ : Type u} {hyps : List (NamedPred σ)} {goal lhs rhs : pred σ} (hlhs : |-tla- (lhs)) (idx : Nat) (hpred : Option.map NamedPred.pred hyps[idx]? = some [tlafml|lhs → rhs]) : Entails (hyps.modify idx fun (x : NamedPred σ) => match x with | { name := name, pred := pred } => { name := name, pred := rhs }) goal → Entails hyps goal

theorem TLA.ProofMode.Entails_specialize_temporal_by_name {σ : Type u} {hyps : List (NamedPred σ)} {goal rhs : pred σ} {lhss : List (pred σ)} (premises : List String) (hprem : List.filterMap (fun (premise : String) => Option.map NamedPred.pred (List.find? (fun (h : NamedPred σ) => h.name == premise) hyps)) premises = lhss) (chosen : String) (hpred : List.find? (fun (h : NamedPred σ) => h.name == chosen) hyps = some { name := chosen, pred := [tlafml|(repeatedAnd lhss) → rhs] }) : Entails (replaceChosenPred hyps chosen rhs) goal → Entails hyps goal

theorem TLA.ProofMode.Entails_specialize_temporal_by_idx {σ : Type u} {hyps : List (NamedPred σ)} {goal rhs : pred σ} {lhss : List (pred σ)} (premises : List String) (hprem : List.filterMap (fun (premise : String) => Option.map NamedPred.pred (List.find? (fun (h : NamedPred σ) => h.name == premise) hyps)) premises = lhss) (idx : Nat) (hpred : Option.map NamedPred.pred hyps[idx]? = some [tlafml|(repeatedAnd lhss) → rhs]) : Entails (hyps.modify idx fun (x : NamedPred σ) => match x with | { name := name, pred := pred } => { name := name, pred := rhs }) goal → Entails hyps goal

def TLA.ProofMode.tlaSpecializeStep (pos : TemporalHypLoc) (arg : Lean.TSyntax `term) : Lean.Elab.Tactic.TacticM Unit

Specialize one temporal hypothesis once, then simplify the reflected hypothesis list back to the literal proof-mode context. Callers build repeated specialization by invoking this after each argument, so each step sees the predicate produced by the previous step.

def TLA.ProofMode.tlaSpecializeStep.specializeTargetBadShapeMsg (pred : Lean.Expr) : TemporalHypLoc → Lean.MessageData

Error message for a specialize target of an unsupported shape.

Equations

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

def TLA.ProofMode.tlaSpecializeTac : Lean.ParserDescr

tla_specialize h arg₁ arg₂ ... specializes a proof-mode temporal hypothesis in place.

If h : ∀ n, P n, then

tla_specialize h 0

changes h to P 0. If h : p → q and hp : p is a temporal hypothesis, then

tla_specialize h hp

changes h to q and keeps hp in the context. Numeric hypothesis indices may be used in place of names.

Equations

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