refactor: Array.feraseIdx: avoid have in definition

leanprover / lean4

Lean 4 programming language and theorem prover

https://lean-lang.org

Apache License 2.0

3.82k stars 325 forks source link

refactor: Array.feraseIdx: avoid have in definition #4074

Closed nomeata closed 1 week ago

nomeata commented 1 week ago

otherwise it remains in the equational theorem and may cause the “unused have linter” to trigger. By moving the proof into decreasing_by, the equational theorems are unencumbered by termination arguments.

leanprover-community-mathlib4-bot commented 1 week ago

Mathlib CI status (docs):

❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e0c1afd12d4fc6b0e520774959aed06bf122aba9 --onto e362b50fa95d6823e59dd706803a93c25e888535. (2024-05-06 08:10:45)

digama0 commented 1 week ago

What are the chances that this is fixed in the equation compiler so that it doesn't generate terms that violate the unused have linter?

nomeata commented 1 week ago

That's plausible; it would entail removing unused have there. Didn't check yet how hard it would be.

The induction principle generator should then also remove them from the minor premises.

Do you see a case where the user might genuinely want then to be there in the equations? In some cases it maybe might be nice to have them in the goal to intro them conveniently? But that sounds obscure, generating nicer equation lemmas is probably the better trade off.