structure TLA.ProofMode.NamedPred (σ : Type u) : Type u

A named proof-mode hypothesis.

• name : String

  The hypothesis name.

• pred : TLA.pred σ

  The hypothesis predicate.

def TLA.ProofMode.repeatedAnd {σ : Type u_1} (ps : List (pred σ)) : pred σ

Right-fold a list of predicates into a single conjunction.

Equations

• TLA.ProofMode.repeatedAnd ps = LentilLib.List.foldrD TLA.tlaAnd [tlafml|⊤] ps

def TLA.ProofMode.repeatedImplies {σ : Type u_1} (ps : List (pred σ)) (q : pred σ) : pred σ

Right-fold a list of predicates into a chain of implications to q.

Equations

• TLA.ProofMode.repeatedImplies ps q = List.foldr TLA.tlaImplies q ps

theorem TLA.ProofMode.repeatedAnd_eq_bigwedge {σ : Type u_1} (ps : List (pred σ)) : ((repeatedAnd ps)) =tla= (⋀ x ∈ ps, x)

theorem TLA.ProofMode.repeatedAnd_eq_in_iff {σ : Type u_1} (ps1 ps2 : List (pred σ)) (h : ∀ (p : pred σ), p ∈ ps1 ↔ p ∈ ps2) : repeatedAnd ps1 = repeatedAnd ps2

theorem TLA.ProofMode.repeatedAnd_singleton {σ : Type u_1} (p : pred σ) : repeatedAnd [p] = p

theorem TLA.ProofMode.repeatedAnd_append {σ : Type u_1} (ps1 ps2 : List (pred σ)) : ((repeatedAnd (ps1 ++ ps2))) =tla= ((repeatedAnd ps1) ∧ (repeatedAnd ps2))

theorem TLA.ProofMode.repeatedAnd_cons {σ : Type u_1} (p : pred σ) (ps : List (pred σ)) : ((repeatedAnd (p :: ps))) =tla= (p ∧ (repeatedAnd ps))

theorem TLA.ProofMode.repeatedAnd_add_duplicate {σ : Type u_1} {ps : List (pred σ)} {p : pred σ} (h : p ∈ ps) : ((repeatedAnd ps)) =tla= ((repeatedAnd ps) ∧ p)

theorem TLA.ProofMode.repeatedAnd_subset_implies {σ : Type u_1} (ps1 ps2 : List (pred σ)) : ps1 ⊆ ps2 → ((repeatedAnd ps2)) |-tla- ((repeatedAnd ps1))

theorem TLA.ProofMode.repeatedImplies_apply {σ : Type u} {hs : List (pred σ)} {goal : pred σ} : ((repeatedAnd hs) ∧ (repeatedImplies hs goal)) |-tla- (goal)

def TLA.ProofMode.Entails {σ : Type u_1} (hyps : List (NamedPred σ)) (goal : pred σ) : Prop

The proof-mode entailment: the conjunction of hypotheses entails the goal.

Equations

• TLA.ProofMode.Entails hyps goal = ((TLA.ProofMode.repeatedAnd (List.map TLA.ProofMode.NamedPred.pred hyps))) |-tla- (goal)

theorem TLA.ProofMode.repeatedAnd_modifyHyp_reorder {σ : Type u} (hyps : List (NamedPred σ)) (idx : Nat) (h : idx < hyps.length) (f : NamedPred σ → NamedPred σ) : ((repeatedAnd (List.map NamedPred.pred hyps)) ∧ (f hyps[idx]).pred) =tla= ((repeatedAnd (List.map NamedPred.pred (hyps.modify idx f))) ∧ hyps[idx].pred)

theorem TLA.ProofMode.repeatedAnd_map_comm {σ : Type u} (hyps : List (pred σ)) (f : pred σ → pred σ) (htrue : (⊤) =tla= ((f [tlafml|⊤]))) (h : ∀ (p q : pred σ), ((f p) ∧ (f q)) =tla= ((f [tlafml|p ∧ q]))) : repeatedAnd (List.map f hyps) = f (repeatedAnd hyps)

def TLA.ProofMode.ModifyHypSpecWithIndex {σ : Type u_1} (hyps hyps' : List (NamedPred σ)) (f : NamedPred σ → NamedPred σ) (idx : Nat) : Prop

Specification relating a hypothesis list to its modification at a given index.

Equations

• TLA.ProofMode.ModifyHypSpecWithIndex hyps hyps' f idx = (hyps = hyps' ∨ idx < hyps.length ∧ hyps' = hyps.modify idx f)

theorem TLA.ProofMode.ModifyHypSpecWithIndex_modify {σ : Type u} (hyps : List (NamedPred σ)) (f : NamedPred σ → NamedPred σ) (idx : Nat) : ModifyHypSpecWithIndex hyps (hyps.modify idx f) f idx

def TLA.ProofMode.ModifyHypSpec {σ : Type u_1} (hyps hyps' : List (NamedPred σ)) (f : NamedPred σ → NamedPred σ) : Prop

Specification relating a hypothesis list to its modification at some index.

Equations

• TLA.ProofMode.ModifyHypSpec hyps hyps' f = (hyps = hyps' ∨ ∃ (idx : Nat), ∃ (x : idx < hyps.length), hyps' = hyps.modify idx f)

theorem TLA.ProofMode.ModifyHypSpecWithIndex_implies_ModifyHypSpec {σ : Type u_1} {hyps hyps' : List (NamedPred σ)} {f : NamedPred σ → NamedPred σ} {idx : Nat} : ModifyHypSpecWithIndex hyps hyps' f idx → ModifyHypSpec hyps hyps' f

theorem TLA.ProofMode.ModifyHypSpec_implies_ModifyHypSpecWithIndex {σ : Type u_1} {hyps hyps' : List (NamedPred σ)} {f : NamedPred σ → NamedPred σ} : ModifyHypSpec hyps hyps' f → ∃ (idx : Nat), ModifyHypSpecWithIndex hyps hyps' f idx

def TLA.ProofMode.modifyHypByName {σ : Type u} (hyps : List (NamedPred σ)) (name : String) (f : NamedPred σ → NamedPred σ) : List (NamedPred σ)

Modify the hypothesis with the given name by applying f.

Equations

• TLA.ProofMode.modifyHypByName hyps name f = (List.findIdx? (fun (h : TLA.ProofMode.NamedPred σ) => h.name == name) hyps).elim hyps fun (idx : Nat) => hyps.modify idx f

theorem TLA.ProofMode.modifyHypByName_spec {σ : Type u} (hyps : List (NamedPred σ)) (name : String) (f : NamedPred σ → NamedPred σ) : ModifyHypSpec hyps (modifyHypByName hyps name f) f

def TLA.ProofMode.parseStringLitOpt : Lean.Expr → Option String

Like Expr.isStringLit, but returns the string.

Equations

• TLA.ProofMode.parseStringLitOpt (Lean.Expr.lit (Lean.Literal.strVal s)) = some s
• TLA.ProofMode.parseStringLitOpt x✝ = none

def TLA.ProofMode.cleanupAnnotAndMore (e : Lean.Expr) : Lean.MetaM Lean.Expr

Obtain a cleaned-up version of e.

Equations

• TLA.ProofMode.cleanupAnnotAndMore e = do let __do_lift ← Lean.instantiateMVars e pure __do_lift.headBeta.cleanupAnnotations

def TLA.ProofMode.postDSimpAfterApplyingReflectionTheorem (l : Array Lean.Name) : Lean.Elab.Tactic.TacticM Unit

Run dsimp with the reflection lemmas after applying a proof-mode theorem.

Equations

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

def TLA.ProofMode.recognizeHypsList (hyps : Lean.Expr) : Lean.MetaM (Option (Lean.Expr × List (String × Lean.Expr)))

Recognize a literal list of named hypotheses from an Expr.

Equations

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

def TLA.ProofMode.recognizeEntailsHyps (e : Lean.Expr) : Lean.MetaM (Option (Lean.Expr × List (String × Lean.Expr)))

Recognize the hypothesis list of an Entails goal Expr.

Equations

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

def TLA.ProofMode.recognizeEntailsHypsFromGoal : Lean.Elab.Tactic.TacticM (Option (Lean.Expr × List (String × Lean.Expr)))

Recognize the hypothesis list of the current Entails goal.

Equations

• TLA.ProofMode.recognizeEntailsHypsFromGoal = do let g ← Lean.Elab.Tactic.getMainTarget have g : Lean.Expr := g.headBeta.cleanupAnnotations liftM (TLA.ProofMode.recognizeEntailsHyps g)

def TLA.ProofMode.toHypsList (hypTy : Lean.Expr) (hyps : List (String × Lean.Expr)) : Lean.MetaM Lean.Expr

Build the Expr of a literal list of named hypotheses.

Equations

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

def TLA.ProofMode.goalHypsLength : Lean.Elab.Tactic.TacticM (Option Nat)

The number of hypotheses in the current proof-mode goal.

Equations

• TLA.ProofMode.goalHypsLength = do let __x ← TLA.ProofMode.recognizeEntailsHypsFromGoal match __x with | some (fst, hyps) => pure (some hyps.length) | x => pure none