We need this procedure otherwise it takes forever to prove equation lemmas
for definitions such as:
```
def macros : name → option macro
| `lambda := some lambda_macro
| `intro_x := some intro_x_macro
| _ := none
```
We never experienced this problem in Lean3 because we used `name`
literals only occurred in patterns of *meta* definitions. So, no
equation lemma was generated.
@kha `def macros` was taking more than 1 second to elaborate on my
machine. It is now instantaneous.
We use the auxiliary procedure pull_nested_rec_fn to pull recursive
application in nested match expressions. This is needed because the
nested match expression is compiled before we process the recursive
procedure that contains it. This transformation may produce
performance problems if the recursive application does not depend on
the data being matched. Here is an example from the new test:
```
def tst : tree → nat
| (tree.leaf v) := v
| (tree.node v l r) :=
match f v with
| tt := tst l
| ff := tst r
end
```
pull_nested_rec_fn will convert it into
```
def tst : tree → nat
| (tree.leaf v) := v
| (tree.node v l r) := tst._match_1 (f v) (tst l) (tst r)
```
Since our interpreter uses eager evaluation, both `(tst l)` and `(tst r)`
are executed. This commit fixes this issue by expanding `tst._match_1`
during code generation.
We need this feature for:
1) Defining nonlinear search patterns. Example: (?m <= ?m + 1)
2) Preprocessing recursive equations and support the pattern
refinement approach used in Agda. Example: in Agda, they accept
```
def append {A : Type} : Π (m n : nat), Vec A m -> Vec A n -> Vec A (m + n)
| m n nil ys := ys
| m n (cons m' x xs) ys := cons x (append m' n xs ys)
```
These equations have to be refined. For example, `m` has to be
replaced with `0` (in the first equation), and `succ m'` in the
second. To implement this kind of refinement, we need to convert
the pattern variables (local constants) into metavariables during
elaboration. Then, the unassigned metavariables become local constants
again. This preprocessing step will fix some of the issues on #1594.
To completely fix#1594, we will need yet another preprocessing step
which will implement "complete transition" used in the equation
compiler before we start elim_match.cpp
@dselsam You have used a function similar to prove_eq_rec_invertible in
the inductive compiler.
I'm wondering if this bug (missing case) may also occur in the inductive
compiler.
This step packs a collection of mutually recursive functions into a
single one. We use `psum` to combine the different domains, and
`psum.cases_on` to combine the codomains.
The equational compiler was failing to generate equational lemmas for
equations such as:
def f : nat → nat → nat
| (x+1) (y+1) := f (x+10) y
| _ _ := 1
It would fail when trying to prove the following equation:
forall x, f 0 x = 1
using a "refl" proof. This equation does not hold definitionally.
It is not blocked by the internal pattern matching based on the
cases_on recursor, but it is blocked by the outer most brec_on
used to implement structural recursion. The solution is to
"complete" the set of equations. So, the structural_rec
module will replace the equation above with
def f : nat → nat → nat
| (x+1) (y+1) := f (x+10) y
| _ 0 := 1
| _ (y+1) := 1
and then (as before)
def f : Pi (x y : nat), below y → nat
| (x+1) (y+1) F := F^.fst^.fst (x+10)
| _ 0 F := 1
| _ (y+1) F := 1
There were two performance bottlenecks in the recursive equation
compiler. Both bottlenecks were due to conversion checking.
1- We allow patterns such as (x+1) in the left-hand-side of a
recursive equation. This is kind of pattern has to be reduced
since it is not a constructor. Moreover, when we are trying to
compile using structural recursion, we need to find an element
that is structurally smaller in recursive applications.
Again, we need to use reduction since the pattern may be (x+2),
and in the recursive application we have (x+1). Now, consider
the following equation
f (x+1) (y+1) := f complex_term y
It will first check whether complex_term is structurally smaller
than (x+1), and the compiler will timeout trying to reduce
complex_term.
This commit adds the following workaround. The structural
recursion module from now on will only unfold reducible constants
and constants marked as patterns. This is not a complete
solution. It will timeout in the following equation:
f (x+1) (y+1) := f (x+1000000000000) y
For this one, we need to add a whnf "fuel" option to type_context
2- Equational lemma generation was producing lemmas that are too
expensive to check. Suppose we the following two definitions
| f x 0 := 1
| f x (y+1) := f complex_term y
and
| g 0 y := 1
| g (x+1) y := g x complex_term
Before this commit, we would generate the following proofs for
the second equation of each definition:
eq.refl (f complex_term y)
eq.refl (g x complex_term)
This proof triggers the following definitionally equality test:
f x (y+1) =?= f complex_term y
g (x+1) y =?= g x complex_term
Since, we have f/g on both sides, the type checker will try
first to unify the arguments, and may timeout trying to solve
x =?= complex_term
y =?= complex_term
since it may take a long time to reduce `complex_term`.
We workaround this problem by creating a slightly different
proof.
eq.refl (unfold_of(f x (y+1)))
eq.refl (unfold_of(g (x+1) y))
where unfold_of(t) is the result of applying one delta reduction
step.
@johoelzl We now produce a better message for your example:
inductive R : ℕ → Prop
| pos : ∀p n, R (p + n)
lemma R_id : ∀n, R n → R n
| (.p + .n) (R.pos p n) := R.pos p n
The new error is:
file.lean:5:2: error: invalid function application in pattern, it cannot be reduced to a constructor (possible solution, mark term as inaccessible using '.( )')
.p + .n
