In Lean4, we will not generate non dependent recursors for inductive
predicates. The main goal is to make the shape of the automatically
generated recursors more uniform. The non uniform representation is
leftover from Lean2. In Lean2, we wanted to support different kernels
with different features. For example: we could create proof relevant
kernels, no impredicative universe, etc.
Recall that, in a kernel with an impredicative Prop and no proof
irrelevance, inductive predicates without dependent elimination are
weaker that inductive predicates with dependent elimination.
When proof irrelevance is enabled, we can generate the dependent
recursor from the non dependent one. Actually, the module drec.cpp
generates the dependent recursor.
Now, we only support one kind of kernel, and it doesn't make sense
anymore to generate non dependent recursors for inductive predicates.
This would only produce an unnecessary asymmetry on the inductive
datatype module.
Remark: we had to create non dependent recursors to help the elaborator.
This can be avoid if we improve the elaborator. I will do that in the
new elaborator implemented in Lean.
Remark: equation lemmas are broken for definitions that pattern match on
nested inductive datatypes. The problem is the super messy
`prove_eq_rec_invertible_aux` function. This function will not be needed
after I finish the new inductive datatype support in the kernel.
cc @kha
We replace them with a new kind of (delayed) assignment at `metavar_context`
```
mvar := (lctx, locals, v)
```
where `lctx` is a local context, `locals` is a list of local
constants, and `v` is an expression.
When all metavariables in `v` are assigned, this assignment is replaced with
```
mvar := Fun(locals, v)
```
We added for the following reasons:
1- It should mimic the behavior of `visit_lambda` and `visit_pi`.
2- It minimizes the number of auxiliary metavariables that need to be
created when we execute `locals.mk_lambda(new_body)`. In Lean3,
it would minimize the number of delayed abstractions.
@kha The runtime folder includes what is needed to link a
standalone Lean program. It is still contains some unnecessary files.
We will be able to remove them after we release Lean4.
Now, the elaborator only uses the quasi-pattern unifier approximation
for inferring the implicit motive in recursor-like applications.
This change was motivated by counterintuitive behavior associated with
this approximation. For example, before this commit
```
variables {δ σ : Type}
def ex1 : state_t δ (state_t σ id) σ :=
monad_lift (get : state_t σ id σ) -- doesn't work
def ex2 : state_t δ (state_t σ id) σ :=
do s ← monad_lift (get : state_t σ id σ), -- works
return s
```
The first one doesn't work because when we elaborate
`@monad_lift ?m ?n ?c ?α (get : state_t σ id σ) : ?n ?α`
with expected type `state_t δ (state_t σ id) σ`
It first produces the following unification problem by processing
matching the inferred type with the expected one.
```
?n ?α =?= state_t δ (state_t σ id) σ
==> (approximate using first-order unification)
?n := state_t δ (state_t σ id)
?α := σ
```
Then we try to solve
```
?m ?α =?= state_t σ id σ
==> instantiate metavars
?m σ =?= state_t σ id σ
==> (approximate since it is a quasi-pattern unification constraint)
?m := λ σ, state_t σ id σ
```
Remark: the constraint is not a Milner pattern because `σ` is in
the local context of `?m`. By assuming it is a Milner pattern,
we are ignoring the other possible solutions:
```
?m := λ σ', state_t σ id σ
?m := λ σ', state_t σ' id σ
?m := λ σ', state_t σ id σ'
```
We need the quasi-pattern approximation for elaborating recursors.
So, this commit enable this kind of approximation only when
elaborating recursors and executing induction-like tactics.
If we had used first-order unification, then we would have produced
the right answer: `?m := state_t σ id`
Haskell would solve this example since it always uses
first-order unification during elaboration.
The second one works because when we elaborate
`monad_lift (get : state_t σ id σ)`, the expected type is `state_t δ (state_t σ id) ?α`.
So, `?m ?α =?= state_t σ id σ` will not considered to be a quasi-pattern
since `?α` is not yet assigned to a local constant.
We are not fully confident this commit produces a better user
experience. We know that
- Full higher-order unification (used in Lean2) produces a combinatoric
explosion, and generates a lot of non-termination in complex type class
hierarchies (monad library, has_coe, etc). The problem is that
higher-order unification manages to create new solutions that we
cannot find using first-order unification.
- Lean3 is more reliable than Lean2 for elaborating monadic code because
it does not use higher-order unification.
- For elaborating recursor-like applications, we need at least the
quasi-patterns. We need it when trying to infer the implicit
motive. First-order unification works poorly in this case. Note that
the lack of higher-order unification in Lean3 forces us to provide the
motive explicitly for terms that Lean2 can elaborate.
- We need quasi-patterns for solving unification constraints in the
induction-like tactics. Similar to the previous item. We use it to infer
the motive. (edited) I will try to disable the quasi-pattern
approximation when elaborating regular applications. At least, we will
behave like Haskell for this kind of application.
It just adds extra complexity and is in conflict for our plans for
Lean4. Moreover, in our experiments it impacts negatively on
performance: master and lean4 branches. The negative impact has been
confirmed by @kha too.
Remark: so far, caching, in the tactic framework, only makes a difference for the `simp` tactic.
This is not surprising since the simplifier tries to apply rewriting
lemmas over and over again.
@kha the following idiom is not safe
```
while (is_pi(t)) {
t = whnf(binding_body(t));
}
```
`whnf(e)` assumes that `e` does not have dangling deBruijn variables.
We should use (the more expensive):
```
while (is_pi(t)) {
t = whnf(instantiate(binding_body(t), locals.push_local_from_binding(t)));
}
```
BTW, this problem is not related to the assertion violation at #1930
I just stumbled on it when fixing the violation.
