Else the `case` will now allow introducing all necessary variables.
Induction principles with `let` in the types of the cases will be more
common with #3432.
This implementation no longer reduces the type as it goes, but really
only counts
manifest foralls and lets. I find this more sensible and predictable: If
you have
```
theorem induction₂_symm {P : EReal → EReal → Prop} (symm : Symmetric P) …
```
then previously, writing
```
case symm =>
```
would actually bring a fresh `x` and `y` and variable `h : P x y` into
scope and produce a
goal of `P y x`, because `Symmetric P` happens to be
```
def Symmetric := ∀ ⦃x y⦄, x ≺ y → y ≺ x
```
After this change, after `case symm =>` will leave `Symmetric P` as the
goal.
This gives more control to the author of the induction hypothesis about
the actual
goal of the cases. This shows up in mathlib in two places; fixes in
https://github.com/leanprover-community/mathlib4/pull/11023.
I consider these improvements.
the user can now write `termination_by?` to see the termination argument
inferred by GuessLex, and turn it into `termination_by …` using the “Try
this” widget or a code action.
To be done later, maybe: Avoid writing `sizeOf` if it's not necessary.
When editing core Lean, the `pp.proofs` feature causes goal states to fail to display in the Infoview, instead showing only "error when printing message: unknown constant '«term⋯»'". This PR moves the `⋯` syntax from Init.NotationExtra to Lean.Elab.BuiltinTerm
It also makes it so that `⋯` elaborates as `_` while logging a warning, rather than throwing an error, which should be somewhat more friendly when copy/pasting from the Infoview.
Closes#3476
When using `set_option tactic.skipAssignedInstances false`, `simp` and
`rw` will synthesize instance implicit arguments even if they have
assigned by unification. If the synthesized argument does not match the
assigned one the rewrite is not performed. This option has been added
for backward compatibility.
```
example (a : Nat) :
(((a + (2 ^ 64 - 1)) % 2 ^ 64 + 1) * 8 - 1 - (a + (2 ^ 64 - 1)) % 2 ^ 64 * 8 + 1) = 8 := by
omega
```
used to time out, and now is fast.
(We will probably make separate changes later so the defeq checks would
be fast in any case here.)
During the switch to `.lake`, I overlooked updating the paths in
`LakeInstall`. This fixes that and helps prevent further mistakes by
using the same default definitions as the package configuration itself.
The `decide` tactic produces error messages that users find to be
obscure. Now:
1. If the `Decidable` instance reduces to `isFalse`, it reports that
`decide` failed because the proposition is false.
2. If the `Decidable` instance fails to reduce, it explains what
proposition it failed for, and it shows the reduced `Decidable` instance
rather than the `Decidable.decide` expression. That expression tends to
be less useful since it shows the unreduced `Decidable` argument (plus
it's a lot longer!)
Examples:
```lean
example : 1 ≠ 1 := by decide
/-
tactic 'decide' proved that the proposition
1 ≠ 1
is false
-/
opaque unknownProp : Prop
open scoped Classical in
example : unknownProp := by decide
/-
tactic 'decide' failed for proposition
unknownProp
since its 'Decidable' instance reduced to
Classical.choice ⋯
rather than to the 'isTrue' constructor.
-/
```
When reporting the error, `decide` only shows the whnf of the
`Decidable` instance. In the future we could consider having it reduce
all decidable instances present in the term, which can help with
determining the cause of failure (this was explored in
8cede580690faa5ce18683f168838b08b372bacb).
The elaboration function `Lean.Meta.coerceMonadLift?` inserts these
coercion helper functions into a term and tries to unfolded them with
`expandCoe`, but because that function only unfolds up to
reducible-and-instance transparency, these functions were not being
unfolded. The fix here is to give them the `@[reducible]` attribute.
with this, more functions will be proven terminating automatically,
namely those where after `simp_wf`, lexicographic order handling,
possibly `subst_vars` the remaining goal can be solved by `omega`.
Note that `simp_wf` already does simplification of the goal, so
this adds `omega`, not `(try simp) <;> omega` here.
There are certainly cases where `(try simp) <;> omega` will solve more
goals (e.g. due to the `subst_vars` in `decreasing_with`), and
`(try simp at *) <;> omega` even more. This PR errs on the side of
taking
smaller steps.
Just appending `<;> omega` to the existing
`simp (config := { arith := true, failIfUnchanged := false })` call
doesn’t work nicely, as that leaves forms like `Nat.sub` in the goal
that
`omega` does not seem to recognize.
This does *not* remove any of the existing ad-hoc `decreasing_trivial`
rules based on `apply` and `assumption`, to not regress over the status
quo (these rules may apply in cases where `omega` wouldn't “see”
everything, but `apply` due to defeq works).
Additionally, just extending makes bootstrapping easier; early in `Init`
where
`omega` does not work yet these other tactics can still be used.
(Using a single `omega`-based tactic was tried in #3478 but isn’t quite
possible yet, and will be postponed until we have better automation
including forward reasoning.)
with this, hopefully more obvious array accesses will be handled
automatically.
Just like #3503, this PR does not investiate which of the exitsting
tactics in `get_elem_tactic_trivial` are subsumed now and could be
dropped without (too much) breakage.
Before, app unexpanders would only be applied to entire applications.
However, some notations produce functions, and these functions can be
given additional arguments. The solution so far has been to write app
unexpanders so that they can take an arbitrary number of additional
arguments. However, as reported in [this Zulip
thread](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/pretty.20printer.20bug/near/420662236),
this leads to misleading hover information in the Infoview. For example,
while `HAdd.hAdd f g 1` pretty prints as `(f + g) 1`, hovering over `f +
g` shows `f`. There is no way to fix the situation from within an app
unexpander; the expression position for `HAdd.hAdd f g` is absent, and
app unexpanders cannot register TermInfo.
This commit changes the app delaborator to try running app unexpanders
on every prefix of an application, from longest to shortest prefix. For
efficiency, it is careful to only try this when app delaborators do in
fact exist for the head constant, and it also ensures arguments are only
delaborated once. Then, in `(f + g) 1`, the `f + g` gets TermInfo
registered for that subexpression, making it properly hoverable.
The app delaborator is also refactored, and there are some bug fixes:
- app unexpanders only run when `pp.explicit` is false
- trailing parameters in under-applied applications are now only
considered up to reducible & instance transparency, which lets, for
example, optional arguments for `IO`-valued functions to be omitted.
(`IO` is a reader monad, so it's hiding a pi type)
- app unexpanders will no longer run for delaborators that use
`withOverApp`
- auto parameters now always pretty print, since we are not verifying
that the provided argument equals the result of evaluating the tactic
Furthermore, the `notation` command has been modified to generate an app
unexpander that relies on the app delaborator's new behavior.
The change to app unexpanders is reverse-compatible, but it's
recommended to update `@[app_unexpander]`s in downstream projects so
that they no longer handle overapplication themselves.
