feat(library/type_context): unfold lemmas in major premise of acc.rec

[gebner]

See discussion at the bitwise operations issue.

Basically the issue is once again that even though terms such as 4 % 2 definitionally reduce to 0 in the kernel, we can't make use of that fact anywhere else, since the type_context doesn't reduce lemmas.

The type_context.unfold_lemmas option that I added a while back is also problematic, since it is local: consider a definition where the type depends on the definitional equality 4 % 2 = 0. Then whenever you want to use this definition, you have to enable the unfold lemmas option at the use site.

This PR introduces a seemingly cheap workaround for this issue. In the type_context, we iota-reduce acc.rec applications with transparency_mode::All. This makes some well-founded definitions reduce definitionally (and should solve the @digama0's issue). I originally wanted to treat eq.rec and heq.rec in the same way, but this breaks the equation compiler.

@leodemoura Another way to solve this issue is to unfold definitions in the type_context using the equational (rfl-)lemmas. You mentioned a while back that this approach has some issues. Could you elaborate on that, or point to me to previous discussions?

[leodemoura]

@leodemoura Another way to solve this issue is to unfold definitions in the type_context using the equational (rfl-)lemmas. You mentioned a while back that this approach has some issues. Could you elaborate on that, or point to me to previous discussions?

Note that we don't get any rfl-lemmas when using well founded recursion. The equations are only provably equal.

Regarding using rfl-lemmas in the unifier, this is still on the TODO list. We need this feature to address a few issues raised by @Armael. I have tried to implement this approach a few months ago, and it didn't work. I think we are now in a better position to try again. Here are the issues I encountered last time. This is an old note I posted at slack + minor updates.
Remark: the experiment is in the branch https://github.com/leodemoura/lean/tree/type_context_with_refl_lemmas

1. We have to be able to rewrite even when the type context is already in tmp-mode.
   This is an issue because the tmp metavariables in the refl lemma clash with the ones created in the type context. Solution: implemented lift operation for idx metavariables, and custom match.

2. The term being "unfolded" may be stuck. Example:

nat.add n (@one nat ?m)  

will not match the pattern

nat.add ?x_0 (nat.succ ?x_1)

because ?m is not assigned yet.
We cannot assign it during the matching process because it is a regular metavariable and the matching is performed in tmp_mode.

Possible workaround a) try to instanciate type class instances before we try the refl lemmas.
This is a potential performance problem because the term can be arbitrarily big.
The current heuristics we use to speed up the process do not work for the example above.

Possible workaround b) allow regular metavariables be assigned by type class resolution even when we are in tmp-mode.

3. There are many more lazy-delta steps. Before this feature, when we unfold nat.add a (succ ... (succ b) ...), we are done with delta-reduction. It is just iota and beta after that.
   However, with refl-lemmas, the term nat.add a (succ ... (succ b) ...) produces one lazy-delta step per succ. This produces nasty side-effects because of the
   The heuristic (f t =?= f s) ==> (t =?= s).
   Examples such as

(fib 8) =?= 34

will take a very long time because of this heuristic.
Possible workaround: cache failures like we did in Lean2. However, failure are only easy to cache if there are no meta-variables.
UPDATE We now have failure cache in the type_context class. So, this should not be an issue.

4. The type context trace gets very confusing since we use is_def_eq for matching lhs while we are computing is_def_eq. Possible workaround: disable trace when trying refl_lemmas.

5. We must be able to temporarily disable the feature. Example: when proving a refl_lemma for a definition f, we may have to expand the nested definitions (e.g., for match-end blocks)

6. refl/simp lemmas were designed to rewrite elaborated terms. Using them during unification may produce a series of unexpected behaviors since terms contain regular and universe meta-variables.

7. We need to define a notion of "refl stuck application". Right now, a metavar is stuck, a projection is stuck if the structure is stuck, a recursor is stuck is the major premise is stuck. An application (f ...) is refl-lemma stuck if f has refl-lemmas associated with it, AND metavariables occurring in arguments are preventing a refl-lemma from being applied.

[leodemoura]

@gebner Regarding this PR, I'm concerned about using computation for proving lemmas about functions defined by well founded recursion. It is super expensive to compute with them in the kernel. Example:

example : gcd 1000 10 = 10 :=
rfl

That being said, we have a related problem in the current system: we don't have a nice way to unfold functions such as gcd. The equation compiler produces the equation lemma.

gcd.equations._eqn_1 : ∀ (y : ℕ), gcd y = λ (x : ℕ), ite (y = 0) x (gcd (x % y) y)

There is no constructor on the equation lhs. Thus, simp[gcd] will loop since the equation above is applicable to any gcd-application. unfold only supports refl-lemmas (it is actually just sugar for dunfold). We don't support rw [gcd]. Thus, the least ugly solution I found is:

rw [gcd.equations._eqn_1]

This is bad, but we can use it to prove

lemma gcd_zero_right (x : nat) : gcd 0 x = x :=
by rw [gcd.equations._eqn_1]; simp

I see the following possibilities for addressing the unfold-issue.
1- Add support for the notation rw [gcd]. We would be able to prove the lemma above using rw [gcd]; simp.
2- Improve unfold, and make sure it can use non-refl lemmas. The proof above would be unfold gcd; simp.
3- Add flag for non-exhaustive simp. That is, it would perform a single pass, and the result of a simplification step would not be re-simplified. The proof above would be simp [gcd] {exhaustive := ff}; simp.

I think option 2 is the most natural.

[leodemoura]

The following commit implements workaround 3
b9dee04

[leodemoura]

@gebner I'll merge this PR.
As I said above, it is very expensive to compute in the kernel with functions defined by well founded recursion. However, the user should decide whether it is worth it or not. Even if we define something using structured recursion, we may still write very inefficient proofs:

example : 10000000 + 10000000 = 20000000 :=
rfl

[leodemoura]

I'm going to create an issue for the unfold problem described above.