The `unsafe_change e` tactic is similar to the `change e` tactic, but it
does not check whether `e` is definitionally equal to the current
tactic. It is useful when implementing tactics such as:
```
meta def dunfold : list name → tactic unit :=
λ cs, target >>= dunfold_core transparency.instances default_max_steps cs >>= unsafe_change
```
The tactic `dunfold_core` guarantees that the resultant expression is
definitionally equal to the input one.
This was one of the performance problems at issue #1646.
Here are the runtimes for size 7 in the example described at issue #1646.
Before this commit:
tactic execution took 4.96s
elaboration of some_lifted_lets took 7.6s
type checking time of some_lifted_lets took 31.1ms (aka QED time)
total execution time: 12.785s
After this commit:
tactic execution took 3.78s
elaboration of some_lifted_lets took 5.71s
type checking time of some_lifted_lets took 35.2ms
total execution time: 10.693s
Before this commit they were implemented using C++ and Lean.
A Lean procedure was being invoked for each subterm of the input term.
This is one of the performance problems at issue #1646.
Here are the runtimes for size 7 in the example described at issue #1646.
Before this commit:
tactic execution took 7.48s
elaboration of some_lifted_lets took 11.5s
type checking time of some_lifted_lets took 33.4ms (aka QED time)
total execution time: 16.841s
After this commit:
tactic execution took 4.96s
elaboration of some_lifted_lets took 7.6s
type checking time of some_lifted_lets took 31.1ms (aka QED time)
total execution time: 12.785s
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.
closes#1634
This commit also changes the semantic of `tactic.focus [tac_1, ..., tac_n]`.
It now fails if the number of goals is not `n`.
Before it would only fail if there were more tactics than goals.
@Armael: See tests/lean/run/handthen.lean for examples of the new notation.
@kha @gebner I added the `show_goal` tactic for selecting arbitrary
subgoals. This feature is similar to the one available in Isabelle.
This commit allows us to use the `show` keyword as syntax sugar for
`show_goal`. The test `show_goal.lean` has a small example.
What do you think?
@Armael: you can use `show` to structure your proofs in tactic mode.
See `tests/lean/run/show_goal.lean` for a small example.
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.
