This is one of the performance problems at issue #1646.
The method `local_context::erase_user_name(local_decl const & d)` was
inefficient when there are many locals with the same user facing name.
For size 7 in the example described at issue #1646, the average size of the
declaration list was 400. Here are the runtimes for size 7
Before: 19.021 secs
After: 16.433 secs
There are more performance issues.
They can be used to store user state in the tactic_state object.
@Armael @jroesch: The new file tests/lean/run/tactic_ref.lean contains a few examples.
We were getting the following error non deterministically:
```
library/init/data/nat/bitwise.lean:131:6: error: exact tactic failed, type mismatch, given expression has type
z = f ff 0 z
but is expected to have type
eq.rec z e = f ff 0 (binary_rec f z 0)
state:
C : ℕ → Sort u,
f : Π (b : bool) (n : ℕ), C n → C (bit b n),
z : C 0,
h : f ff 0 z = z,
b : bool,
n : ℕ,
b0 : bit b n = 0,
bf : bodd 0 = b,
n0 : shiftr 0 1 = n,
e : 0 = bit ff 0
⊢ eq.rec z e = f ff 0 (binary_rec f z 0)
```
This error was happening because of the type_context.unfold_lemmas new
flag. The type context thread local cache must be flushed whenever the
value of type_context.unfold_lemmas has changed.
This commit fixes issue #1631. However, it is not a perfect solution.
This commit improves the predicate that checks whether a definition is
noncomputable or not. This predicate was implemented before we had
a code generator.
We should refactor the code and use the code generator to check
whether a definition is noncomputable or not. Otherwise, we will
keep finding mismatches between the predicate at noncomputable.cpp
and what the code generator implements.
Older gcc compilers generate a warning when the attribute is used.
I found out that GCC 7 will not produce a warning if comments
such as /* fall-thru */ or /* FALLTHRU */ are used instead of the
attribute [[fallthrough]]
rel_tac is a tactic used for synthesizing a well founded relation.
The default implementation just uses type class resolution.
More sophisticated strategies may need to access the set of recursive
equations. This commit addresses this need.
@dselsam You have assumed that the left-hand-side (t) and
right-hand-side (s) of (t = s) and (t == s) are the last two arguments.
This is a reasonable assumption, and it is correct for eq, but it is
incorrect for heq.
The type of heq is
```
Π {α : Sort u_1}, α → Π {β : Sort u_1}, β → Prop
```
Do you recall other places where we may have made this assumption?
@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.
