SpecificationTactics

This module provides tactics proving the per-instruction specifications.

def tacticHoareSimpSpecification : Lean.ParserDescr

Unfold and simplify the Hoare specification in the goal.

Equations

• tacticHoareSimpSpecification = Lean.ParserDescr.node `tacticHoareSimpSpecification 1024 (Lean.ParserDescr.nonReservedSymbol "hoareSimpSpecification" false)

def tacticSimpJumpSpecFalse : Lean.ParserDescr

Simplify a jump specification whose branch condition is false.

Equations

• tacticSimpJumpSpecFalse = Lean.ParserDescr.node `tacticSimpJumpSpecFalse 1024 (Lean.ParserDescr.nonReservedSymbol "simpJumpSpecFalse" false)

def tacticSimpJumpSpecTrue : Lean.ParserDescr

Simplify a jump specification whose branch condition is true.

Equations

• tacticSimpJumpSpecTrue = Lean.ParserDescr.node `tacticSimpJumpSpecTrue 1024 (Lean.ParserDescr.nonReservedSymbol "simpJumpSpecTrue" false)

def tacticSimpJumpSpec : Lean.ParserDescr

Simplify a jump specification in the goal.

Equations

• tacticSimpJumpSpec = Lean.ParserDescr.node `tacticSimpJumpSpec 1024 (Lean.ParserDescr.nonReservedSymbol "simpJumpSpec" false)