leanprover
feat: mark `rfl` proofs of `Iff` for use by `dsimp`
This PR modifies the behavior of dsimp to allow it to use rfl proofs of Iff statements. It does so by marking Iff theorems that have proofs which consist of Iff.rfl, Iff.refl, Iff.symm, propext, or any combination thereof as rfl theorems via isRflProof.
- [X] Put an X in this bracket to confirm you have read the External Contribution Guidelines.
Fixes #2678.
Note: this PR is currently experimental, and CI is being used for debugging; this branch will likely be rebased for a cleaner commit history.
⚠️ Various issues arise from adding lemmas to the dsimp set. See zulip for more details.
![github-actions[bot] avatar](https://avatars.githubusercontent.com/in/15368?v=4 "Published by a pub.dev verified publisher"){kind=small}
@thorimur, could you run !bench on the Mathlib branch? You will need to make a PR out of the branch lean-pr-testing-2679.
Here are the benchmark results for commit 8f732903af2959c1584ebd50e99d40f0d206b3c7. There were no significant changes against commit 99b78bcc23d759ed9af55a3cccae15da51c0730b.
@thorimur, could you run
!benchon the Mathlib branch? You will need to make a PR out of the branch lean-pr-testing-2679.
Will do—as soon as I make sure this is working! :) Turns out I needed to account for simp's preprocessing adding propext to these lemmas. (I also plan to add some tests.) Depending on how long it takes to compile and produce a toolchain, I might not have a chance to test and bench until tomorrow.
Will do—as soon as I make sure this is working! :) Turns out I needed to account for
simp's preprocessing addingpropextto these lemmas.
What do you mean by this? IIRC, the strategy I implemented in lean 3 was just to recreate a copy of the lemma with = instead of Iff, to avoid needing propext. The motivation is not to avoid the axiom per se, but to ensure everything goes through definitionally, which avoids problems with dependent rewrites.
Will do—as soon as I make sure this is working! :) Turns out I needed to account for
simp's preprocessing addingpropextto these lemmas.What do you mean by this? IIRC, the strategy I implemented in lean 3 was just to recreate a copy of the lemma with
=instead ofIff, to avoid needingpropext. The motivation is not to avoid the axiom per se, but to ensure everything goes through definitionally, which avoids problems with dependent rewrites.
@eric-wieser The reasons lie in the code of mkSimpTheoremsFromConst in Lean.Meta.Tactic.Simp.SimpTheorems. This calls preprocess on the type and value, and in the case of Iff, attaches propext to the value. Here's the relevant code in preprocess (in that same file):
...
else if let some (lhs, rhs) := type.iff? then
...
let type ← mkEq lhs rhs
let e ← mkPropExt e
return [(e, type)]
It is this e and type which is used to create an auxLemma, which is in turn fed to mkSimpTheoremCore—which in turn calls isRflProof to set the dsimp flag. At that stage, we therefore need isRflProof to unwrap the propext to check if it's dsimp-worthy. (I was reluctant to change the flow and wanted to keep my changes minimal, but one could imagine e.g. including the output of isRflProof in the preprocess result.)
I want to be clear, though, that isRflProof already unwraps this auxLemma anyway, and unwraps constants it encounters recursively (as long as they're applied to something, for some reason). This isn't something I introduced; I just added an if branch to handle the propext case.
What sorts of problems with dependent rewrites might we worry about here?
@thorimur, you might want to rebase this onto master; I think we won't be able to get the Mathlib testing to work otherwise, as other things have moved on in the meantime! :-)
- 💥 Mathlib branch lean-pr-testing-2679 build failed against this PR. (2023-11-06 15:21:05) View Log
- 💥 Mathlib branch lean-pr-testing-2679 build failed against this PR. (2023-11-13 13:46:55) View Log
