fix: nontermination while generating equation lemmas for `match`-expressions

leanprover / lean4

Lean 4 programming language and theorem prover

https://lean-lang.org

Apache License 2.0

4.74k stars 427 forks source link

fix: nontermination while generating equation lemmas for `match`-expressions #6180

Closed leodemoura closed 2 days ago

leodemoura commented 3 days ago

This PR fixes a non-termination bug that occurred when generating the match-expression equation theorems. The bug was triggered when the proof automation for the equation theorem repeatedly applied injection( to the same local declaration, as it could not be removed due to forward dependencies. See issue #6067 for an example that reproduces this issue.

closes #6067

leanprover-community-bot commented 2 days ago

Mathlib CI status (docs):

❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 1126407d9b8358248ccf2f6bdc36787633c40887 --onto 6202461a21d2636129cb8950cd9b6549ccf4b185. (2024-11-22 23:56:13)