This feature is needed when we declare an inductive predicate/type
which is indexed by a mutual and/or nested inductive datatype.
See tests/lean/run/term_pred.lean for an example.
@Armael: this commit should fix the issue with the `cases` tactic that
you reported today.
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
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.
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.
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`.
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
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.
