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.
After this commit, `(+)` is notation for (add) instead of `(fun x y, add x y)`.
This change is relevant when defining type class instances such as
```lean
instance semigroup_to_is_associative [semigroup α] : is_associative α (*) :=
⟨mul_assoc⟩
```
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
