As suggested by @kmill, removing an unnecessary `let` (possibly only
there in the first place for copy/paste reasons) seems to fix the
included test.
This makes `~q()` matching in quote4 noticeably more useful in things
like `norm_num` (as it fixes
https://github.com/leanprover-community/quote4/issues/29)
It also makes a quote4 bug slightly more visible
(https://github.com/leanprover-community/quote4/issues/30), but the bug
there already existed anyway, and isn't caused by this patch.
Fixes#3065
Consider
```
import Std.Tactic.ShowTerm
opaque a : Nat
opaque b : Nat
axiom a_eq_b : a = b
opaque P : Nat → Prop
set_option pp.explicit true
-- Using rw
example (h : P b) : P a := by show_term rw [a_eq_b]; assumption
```
Before, a typical proof term for `rewrite` looked like this:
```
-- Using the proof term that rw produces
example (h : P b) : P a :=
@Eq.mpr (P a) (P b)
(@id (@Eq Prop (P a) (P b))
(@Eq.ndrec Nat a (fun _a => @Eq Prop (P a) (P _a))
(@Eq.refl Prop (P a)) b a_eq_b))
h
```
which is rather round-about, applying `ndrec` to `refl`. It would be
more direct to write
```
example (h : P b) : P a :=
@Eq.mpr (P a) (P b)
(@id (@Eq Prop (P a) (P b))
(@congrArg Nat Prop a b (fun _a => (P _a)) a_eq_b))
h
```
which this change does.
This makes proof terms smaller, causing mild general speed up throughout
the code; if the brenchmarks don’t lie the highlights are
* olean size -2.034 %
* lint wall-clock -3.401 %
* buildtactic execution s -10.462 %
H'T to @digama0 for advice and help.
NB: One might even expect the even simpler
```
-- Using the proof term that I would have expected
example (h : P b) : P a :=
@Eq.ndrec Nat b (fun _a => P _a) h a a_eq_b.symm
```
but that would require non-local changes to the source code, so one step
at a time.
The `checkTargets` function introduced in 4a0f8bf2 as
```
checkTargets (targets : Array Expr) : MetaM Unit := do
let mut foundFVars : FVarIdSet := {}
for target in targets do
unless target.isFVar do
throwError "index in target's type is not a variable (consider using the `cases` tactic instead){indentExpr target}"
if foundFVars.contains target.fvarId! then
throwError "target (or one of its indices) occurs more than once{indentExpr target}"
```
looks like it tries to check for duplicate indices, but it doesn’t
actually, as `foundFVars` is never written to.
This adds
```
foundFVars := foundFVars.insert target.fvarId!
```
and a test case.
Maybe a linter that warns about `let mut` that are never writen to would
be useful?
there was a check
if !Structural.recArgHasLooseBVarsAt recFnName fixedPrefixSize e then
that would avoid going through `.refineThrough`/`.addArg` for
matcher/casesOn applications. It seems it tries to detect when refining
the motive/param is pointless, but it was too eager, and cause confusion
with, for example, this reasonably reasonable function:
def foo : (n : Nat) → (i : Fin n) → Bool
| 0, _ => false
| 1, _ => false
| _+2, _ => foo 1 ⟨0, Nat.zero_lt_one⟩
decreasing_by simp_wf; simp_arith
In particular, the `GuessLex` code later expects that the (implict)
`PProd.casesOn` in the implementation of `foo._unary` will refine the
paramter, because else the (rather picky) `unpackArg` fails. But it also
prevents this from being provable.
So let's try without this shortcut.
Fixing this also revealed that `withRecApps` wasn’t looking in all
corners
of a matcherApp/casesOnApp.
Fixes#3175
This change
* moves `termination_by` and `decreasing_by` next to the function they
apply to
* simplify the syntax of `termination_by`
* apply the `decreasing_by` goal to all goals at once, for better
interactive use.
See the section in `RELEASES.md` for more details and migration advise.
This is a hard breaking change, requiring developers to touch every
`termination_by` in their code base. We decided to still do it as a
hard-breaking change, because supporting both old and new syntax at the
same time would be non-trivial, and not save that much. Moreover, this
requires changes to some metaprograms that developers might have
written, and supporting both syntaxes at the same time would make
_their_ migration harder.
This introduces `FilePath.addExtension` to take a path that we know has
no prior extension, and append a new extension to it.
As this function is simpler than `FilePath.withExtension`, this change
eagerly replaces uses of the latter with the former, except in a few
cases where stripping the extension really is the right thing to do.
This should fix the bug described at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Import.20file.20with.20multiple.20dots.20in.20file.20name/near/404508048,
where `import «A.B».«C.D.lean»` is needed to import `A.B/C.D.lean`.
Closes#2999
---------
Co-authored-by: Mac Malone <tydeu@hatpress.net>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
To handle delaborating notations that are functions that can be applied
to arguments, extracts the core function application delaborator as a
separate function that accepts the number of arguments to process and a
delaborator to apply to the "head" of the expression.
Defines `withOverApp`, which has the same interface as the combinator of
the same name from std4, but it uses this core function application
delaborator.
Uses `withOverApp` to improve a number of application delaborators,
notably projections. This means Mathlib can stop using `pp_dot` for
structure fields that have function types.
Incidentally fixes `getParamKinds` to specialize default values to use
supplied arguments, which impacts how default arguments are delaborated.
---------
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Allow `simproc`s to be declared without setting the `[simproc]`
attribute. A `simproc` declaration is function + pattern.
Motivation: allow them to be provided as arguments to `simp` **and** `simp only`.
TODO: track their use in `simp`.
TODO: builtin simprocs
See new test for example that takes exponential time without new simp
theorems.
TODO: replace auxiliary theorems with simprocs as soon as we implement them.
The pattern
```
for h : i in [:xs.size] do
let x := xs[i]'h.2
```
is occassionally useful to iterate over an array with the index in
hand. This PR extends the `get_elem_tactic_trivial` so that one can
simply write
```
for h : i in [:xs.size] do
let x := xs[i]
```
fixes#3032.
This makes hover info, go to definition, etc work for the `h` in `cases
h : e`. The implementation is similar to that used for the `generalize h
: e = x` tactic.
#2966 was the `@[extern]` bug that prompted development of the
`test_extern` command, but then we merged the fix to #2966 without
updating the tests to use `test_extern`.
There were no `quot_precheck` instances registered for the expression
tree elaborators, which prevented them from being usable in a `notation`
expansion without turning off the quotation prechecker.
Users can evaluate whether `set_option quotPrecheck false` is still
necessary for their `notation` definitions.
Switches from encoding `let_fun` using an annotated `(fun x : t => b) v`
expression to a function application `letFun v (fun x : t => b)`.
---------
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Fixes reference implementation of `ByteArray.copySlice`, as reported
https://github.com/leanprover/lean4/issues/2966.
Adds tests.
---------
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
This adds a `test_extern` command.
Usage:
```
import Lean.Util.TestExtern
test_extern Nat.add 17 37
```
This:
* Checks that the head symbol has an `@[extern]` attribute.
* Writes down `t == t'`, where `t` is the term provided, and `t'` is the
reference implementation (specifically, `t` with the head symbol
unfolded).
* Tries to reduce this to `true`, and complains if this fails.
Note that the type of the term must have a `BEq` instance for this to
work: there's a self-explanatory error message if it isn't available.
