Smart unfolding support #
Forward declaration. It is defined in the module
It is possible to avoid this hack if we move
to this module.
Helper methods #
Helper functions for reducing recursors #
major. It tries to use the auto-generated projection functions if available. Otherwise falls back
Helper functions for reducing Quot.lift and Quot.ind #
Helper function for extracting "stuck term" #
Weak Head Normal Form auxiliary combinators #
The "match" compiler uses
if-then-else expressions and other auxiliary declarations to compile match-expressions such as
match v with | 'a' => 1 | 'b' => 2 | _ => 3
because it is more efficient than using
reduceMatcher? fails if these auxiliary definitions (e.g.,
ite) cannot be unfolded in the current
transparency setting. This is problematic because tactics such as
most users assume that expressions such as
match 0 with | 0 => 1 | 100 => 2 | _ => 3
should reduce in any transparency mode.
Thus, we define a custom
canUnfoldAtMatcher predicate for
This solution is not very modular because modifications at the
match compiler require changes here.
We claim this is defensible because it is reducing the auxiliary declaration defined by the
Alternative solution: tactics that use
TransparencyMode.reducible should rely on the equations we generated for match-expressions.
This solution is also not perfect because the match-expression above will not reduce during type checking when we are not using
Apply beta-reduction, zeta-reduction (i.e., unfold let local-decls), iota-reduction, expand let-expressions, expand assigned meta-variables.
deltaAtProj controls how to reduce projections
deltaAtProj == true,
then delta reduction is used to reduce
whnf is used), otherwise
iota and projection reduction are not performed.
Note that the value of
deltaAtProj is irrelevant if
simpleReduceOnly = true.
def r (i j : Nat) : Nat := i + match j with | Nat.zero => 1 | Nat.succ j => i + match j with | Nat.zero => 2 | Nat.succ j => r i j
produces the following
_sunfold auxiliary definition with the markers
def r._sunfold (i j : Nat) : Nat := i + (*) match j with | Nat.zero => (**) 1 | Nat.succ j => i + (*) match j with | Nat.zero => (**) 2 | Nat.succ j => (**) r i j
match expressions marked with
markSmartUnfoldingMatch (*) must be reduced, otherwise the resulting term is not definitionally
equal to the given expression. The recursion may be interrupted as soon as the annotation
markSmartUnfoldingAlt (**) is reached.
For example, the term
r i j.succ.succ reduces to the definitionally equal term
i + i * r i j
Auxiliary method for unfolding a class projection. when transparency is set to
Recall that class instance projections are not marked with
[reducible] because we want them to be
in "reducible canonical form".