Instances For
Equations
- Lean.Elab.Eqns.splitMatch? mvarId declNames = Lean.commitWhenSome? do let target ← mvarId.getType' Lean.Elab.Eqns.splitMatch?.go mvarId declNames target ∅
Eliminate namedPatterns
from equation, and trivial hypotheses.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
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
- One or more equations did not get rendered due to their size.
Delta reduce the equation left-hand-side
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.Elab.Eqns.tryContradiction mvarId = mvarId.contradictionCore { useDecide := true, emptyType := true, searchFuel := 16, genDiseq := true }
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
- One or more equations did not get rendered due to their size.
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.
Equations
- One or more equations did not get rendered due to their size.
Generate the "unfold" lemma for declName
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.Elab.Eqns.getUnfoldFor? declName getInfo? = match getInfo? () with | some info => do let __do_lift ← Lean.Elab.Eqns.mkUnfoldEq declName info pure (some __do_lift) | x => pure none