Eliminate namedPatterns
from equation, and trivial hypotheses.
Equations
Instances For
Some of the hypotheses added by mkEqnTypes
may not be used by the actual proof (i.e., value
argument).
This method eliminates them.
Alternative solution: improve saveEqn
and make sure it never includes unnecessary hypotheses.
These hypotheses are leftovers from tactics such as splitMatch?
used in mkEqnTypes
.
Equations
Instances For
Equations
Instances For
Delta reduce the equation left-hand-side
Equations
Instances For
Generate equations for declName
.
This unfolds the function application on the LHS (using an unfold theorem, if present, or else by
delta-reduction), calculates the types for the equational theorems using mkEqnTypes
, and then
proves them using mkEqnProof
.
This is currently used for non-recursive functions, well-founded recursion and partial_fixpoint, but not for structural recursion.
Equations
Instances For
Equations
Instances For
Auxiliary method for mkUnfoldEq
. The structure is based on mkEqnTypes
.
mvarId
is the goal to be proved. It is a goal of the form
declName x_1 ... x_n = body[x_1, ..., x_n]
The proof is constructed using the automatically generated equational theorems.
We basically keep splitting the match
and if-then-else
expressions in the right hand side
until one of the equational theorems is applicable.