This modification improves the performance of the example in issue
#4861. It no longer times out but is still expensive.
Here is the analysis of the performance issue: Given `(x : Int)`, to
elaborate `x ^ 1`, a few default instances have to be tried.
First, the homogeneous instance is tried and fails since `Int` does not
implement `Pow Int`. Then, the `NatPow` instance is tried, and it also
fails. The same process is performed for each term of the form `p ^ 1`.
There are seveal of them at #4861. After all of these fail, the lower
priority default instance for numerals is tried, and `x ^ 1` becomes `x
^ (1 : Nat)`. Then, `HPow Int Nat Int` can be applied, and the
elaboration succeeds. However, this process has to be repeated for every
single term of the form `p ^ 1`. The elaborator tries all homogeneous
`HPow` and `NatPow` instances for all `p ^ 1` terms before trying the
lower priority default instance `OfNat`.
This commit ensures `Int` has a `NatPow` instance instead of `HPow Int
Nat Int`. This change shortcuts the process, but it still first tries
the homogeneous `HPow` instance, fails, and then tries `NatPow`. The
elaboration can be made much more efficient by writing `p ^ (1 : Nat)`.
Those represent ~13% of the time spent in `save_result`,
even though `r` is a temporary in all cases but one.
See #4698 for details.
---------
Co-authored-by: Leonardo de Moura <leomoura@amazon.com>
…rators
Right now those constructors result in a copy instead of the desired
move. We've measured that expr copying and assignment by itself uses
around 10% of total runtime on our workloads.
See #4698 for details.
Initial options are now re-parsed and validated after importing. Cmdline
option assignments prefixed with `weak.` are silently discarded if the
option name without the prefix does not exist.
Fixes#3403
This allows bitblasting `BitVec.replicate`.
I changed the definition of `BitVec.replicate` to use `BitVec.cast` in
order to make the proof smoother, since it's an easier time simplifying
away terms with `BitVec.cast`.
---------
Co-authored-by: Tobias Grosser <tobias@grosser.es>
This message is often incorporated into source files via `#guard_msgs`.
This change ensures it won't go over the 100 character ruler, and I
think is equally grammatical. :-)
It is confusing that the message suggesting to use the `diagnostics`
option is given even when the option is already set. This PR makes use
of lazy message data to make the message contingent on the option being
false.
It also tones down the promise that there is any diagonostic information
available, since sometimes there is nothing to report.
Suggested by Johan Commelin.
now that we support structural mutual recursion, I expect that every
`DecidableEq` instance be implemented using structural recursion, so
let's be explicit about it.
Some eliminators (such as `False.rec`) have an explicit motive argument.
The `elabAsElim` elaborator assumed that all motives are implicit.
If the explicit motive argument is `_`, then it uses the elab-as-elim
procedure, and otherwise it falls back to the standard app elaborator.
Furthermore, if an explicit elaborator is not provided, it falls back to
treating the elaborator as being implicit, which is convenient for
writing `h.rec` rather than `h.rec _`. Rationale: for `False.rec`, this
simulates it having an implicit motive, and also motives are generally
not going to be available in the expected type.
Closes#4347
Before, the delaborator was conservative about omitting optional
arguments, only omitting the very last one. Now it can omit arbitrarily
long sequences of optional arguments from the end.
For simplicity of implementation, every optional argument is delaborated
and then potentially discarded. It could save state and lazily
delaborate, but we're running under the hypothesis that most optional
arguments are for very simple values (like `true`, `false`, or a numeric
literal), so it is unlikely that efficiency gains, if any, are worth it.
In particular, in the future structure constructors will have optional
arguments, but `unexpandStructureInstance` assumes none of the optional
fields are omitted.
Closes#4812
when transforming the `match` statements in `IndPredBelow`, given a
local variable `x : T`, we need to search for `hx : T.below x`.
Previously this was done using the custom `backwardsChaining` method,
although my hypothesis is that we don’t need to chain anything here, and
can use `apply_assumption`.
this improves support for structural recursion over inductive
*predicates* when there are reflexive arguments.
Consider
```lean
inductive F: Prop where
| base
| step (fn: Nat → F)
-- set_option trace.Meta.IndPredBelow.search true
set_option pp.proofs true
def F.asdf1 : (f : F) → True
| base => trivial
| step f => F.asdf1 (f 0)
termination_by structural f => f`
```
Previously the search for the right induction hypothesis would fail with
```
could not solve using backwards chaining x✝¹ : F
x✝ : x✝¹.below
f : Nat → F
a✝¹ : ∀ (a : Nat), (f a).below
a✝ : Nat → True
⊢ True
```
The backchaining process will try to use `a✝ : Nat → True`, but then has
no idea what to use for `Nat`.
There are three steps here to fix this.
1. We let-bind the function's type before the whole process. Now the
goal is
```
funType : F → Prop := fun x => True
x✝ : x✝¹.below
f : Nat → F
a✝¹ : ∀ (a : Nat), (f a).below
a✝ : ∀ (a : Nat), funType (f a)
⊢ funType (f 0)
```
2. Instead of using the general purpose backchaining proof search, which
is more
powerful than we need here (we need on recursive search and no
backtracking),
we have a custom search that looks for local assumptions that
provide evidence of `funType`, and extracts the arguments from that
“type” application to construct the recursive call.
Above, it will thus unify `f a =?= f 0`.
3. In order to make progress here, we also turn on use
`withoutProofIrrelevance`,
because else `isDefEq` is happy to say “they are equal” without actually
looking
at the terms and thus assigning `?a := 0`.
This idea of let-binding the function's motive may also be useful for
the other recursion compilers, as it may simplify the FunInd
construction. This is to be investigated.
fixes#4751
