See Section "Other goodies" at
https://github.com/leanprover/lean/wiki/Refactoring-structures
This commit also improves the support for projections in the
unifier/matcher.
Now, we consider the extra case-split for projections.
Given a projection `proj`, and the constraint `proj s =?= proj t`, we need to try first `s =?= t` and if it fails, then try to reduce.
This is needed in the standard library because we now have constraints such as:
```
@has_le.le ?A ?s ?a ?b =?= @has_le.le nat nat.has_add x y
```
If we reduce the right hand side, we get the unsolvable constraint
```
@has_le.le ?A ?s ?a ?b =?= nat.le x y
```
Before this change, the constraint was `@le ?A ?s ?a ?b =?= @le nat nat.has_add x y`, and we already perform a case-split in this case.
Moreover, projections were eagerly reduced whenever possible.
The extra case-split generates a performance problem in several tests. For example `fib 8 = 34` was timing out.
I worked around this issue by performing the case-split only when the constraint contains meta-variables.
There are also minor issues. Example. `<` is notation for `has_lt.lt`, but `>` is for `gt`.
We need this improvement to be able to finish Section "Other goodies" described at
https://github.com/leanprover/lean/wiki/Refactoring-structures
Before this commit, Lean would not be able to solve constraints such as
```lean
@has_add.add nat nat.has_add a b =?= @had_add.add ?A ?inst a b
```
The problem is that projections were being reduced eagerly, and the
constraint would be reduced to
```lean
nat.add a b =?= @had_add.add ?A ?inst a b
```
The new test proj_uniy.lean contains similar unification problems.
Motivation: see "Other goodies" section at
https://github.com/leanprover/lean/wiki/Refactoring-structures
We had to add a new transparency mode: Instances at type_context.
In this mode, instances and reducible definitions are considered
transparent.
The new mode is used in the defeq_canonizer, code generator,
and sizeof lemma generation at inductive_compiler.
We also use the new mode in the unfold tactics.
Moreover, we process the implicit arguments using at least the Semireducible
transparency mode. The idea is to make sure to reduce counterintuitive
behavior in rw and simp where the user believes a lemma is applicable
but it does not work because the implicit part fails to unify.
The modification above fixes the simplifier issues found by @kha when proving the
monadic laws.
This commit also improves constraints of the form
n =?= m
where n and m are big distinct numerals. The type_context fails quickly
for this kind of constraint even using transparency mode Semireducible.
We need this feature otherwise we timeout at
@eq char a b =?= @eq unsigned ?x ?y
Recall that
char := fin char_sz
unsigned := fin unsigned_sz
@leodemoura The forced zeta-expansion in mk_aux_definition might
cause problems if we use tactic.abstract without zeta-reduction.
However, we never use the non-zeta mode, and it already fails right now
if you accidentally use zeta-expansion in the proof we want to abstract.
See #1480
@semorrison We can now use the following commands to trace the rewrite
tactic
```lean
set_option trace.rewrite true
set_option trace.kabstract true
```
When these options are used, Lean will pretty print the subterm selected
by the rewrite tactic. That is, the subterm that will be rewritten.
This option may help you diagnose what is going on.
