HelpCodeProofTactics

This module provides auxiliary helpers for the MRiscX code-proof tactics.

def tacticSimpCurrInstr : Lean.ParserDescr

Tries to solve a s.currInstr = instr goal. Requires the s.cdoe and s.pc being introduced as h_code' and h_pc respectively as hypothesis

Equations

• tacticSimpCurrInstr = Lean.ParserDescr.node `tacticSimpCurrInstr 1024 (Lean.ParserDescr.nonReservedSymbol "simpCurrInstr" false)

def tacticSimpTUpdate : Lean.ParserDescr

Simplify total-map updates appearing in the goal.

Equations

• tacticSimpTUpdate = Lean.ParserDescr.node `tacticSimpTUpdate 1024 (Lean.ParserDescr.nonReservedSymbol "simpTUpdate" false)

def tacticPrepareSecondSeq : Lean.ParserDescr

Prepare the goal for the second branch of a sequencing proof.

Equations

• tacticPrepareSecondSeq = Lean.ParserDescr.node `tacticPrepareSecondSeq 1024 (Lean.ParserDescr.nonReservedSymbol "prepareSecondSeq" false)

def RCasesPatt.alts' (ref : Lean.Syntax) : List Lean.Elab.Tactic.RCases.RCasesPatt → Lean.Elab.Tactic.RCases.RCasesPatt

Collapse a list of rcases alternatives into a single pattern, using the lone pattern directly when there is exactly one. Adapted from Lean.Elab.Tactic.RCases.

Equations

• RCasesPatt.alts' ref [p] = p
• RCasesPatt.alts' ref x✝ = Lean.Elab.Tactic.RCases.RCasesPatt.alts ref x✝

def RCasesPatt.parse (stx : Lean.Syntax) : Lean.MetaM Lean.Elab.Tactic.RCases.RCasesPatt

Parses a Syntax into the RCasesPatt type used by the RCases tactic.

Equations

• RCasesPatt.parse stx = RCasesPatt.parseAux✝ (patternSyntaxSize✝ stx) stx

def tacticSplitCondisIn_ : Lean.ParserDescr

Split the conjunctions and disjunctions in the given hypothesis.

Equations

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