fix: nontermination when generating the match-expression splitter theorem

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 when generating the match-expression splitter theorem #6146

Closed leodemoura closed 4 days ago

leodemoura commented 4 days ago

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

closes #6065

leanprover-community-bot commented 4 days ago

Mathlib CI status (docs):

✅ Mathlib branch lean-pr-testing-6146 has successfully built against this PR. (2024-11-21 03:00:40) View Log