Zulip Chat Archive
Stream: mathlib4
Topic: dsimp and Iff.rfl
Johan Commelin (Mar 22 2023 at 13:25):
See https://github.com/leanprover-community/mathlib4/pull/2891#discussion_r1137173310
can
dsimpuseIff.rfllemmas in Lean 4?
Kyle Miller (Mar 22 2023 at 14:23):
Looks like no:
@[simp]
theorem my_id_apply : my_id p ↔ p := Iff.rfl
example : my_id p ↔ p := by
dsimp
-- goal is still my_id p ↔ p
sorry
Johan Commelin (Mar 22 2023 at 14:25):
Is that a "bug"? (Also, sorry for being so lame that I didn't test this myself. That should've been the obvious thing to do.)
Reid Barton (Mar 22 2023 at 14:27):
I think this was added in the community fork of Lean 3, so, unsurprising that it is not supported in Lean 4
Kyle Miller (Mar 22 2023 at 14:30):
Maybe a workaround for now is to give both the iff and rfl lemmas with a porting note?
Kyle Miller (Mar 22 2023 at 14:34):
By the way, do we have something like this somewhere?
theorem Eq.iff {p q : Prop} (h : p = q) : p ↔ q := h ▸ Iff.rfl
It'd make it very slightly easier to use Eq lemmas in proof terms (thm.iff.mp and thm.iff.mpr), but maybe we don't want to encourage having Eq lemmas for propositions.
Kyle Miller (Mar 22 2023 at 14:39):
Found the rfl theorem check: https://github.com/leanprover/lean4/blob/a4acf084c85d8f1a4a3ec0f5d20f90799c27d46f/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean#L106
It accepts more than just rfl, but it doesn't look at Iffs at all.
Eric Wieser (Mar 22 2023 at 15:13):
Reid Barton said:
I think this was added in the community fork of Lean 3, so, unsurprising that it is not supported in Lean 4
Yes, I added this recently. I would hope it would be reasonable to request it be added to Lean 4 too.
Eric Wieser (Mar 22 2023 at 15:14):
but maybe we don't want to encourage having Eq lemmas for propositions.
This was the main motivation; to allow us to retire using docs#set.mem_set_of_eq in favor of the more reasonable docs#set.mem_set_of
Johan Commelin (Mar 22 2023 at 15:15):
Recently? I think dsimp has used iff.rfl lemmas for ages? At least that is how I've always experienced Lean 3.
Eric Wieser (Mar 22 2023 at 15:16):
https://github.com/leanprover-community/lean/pull/723 was the PR
Eric Wieser (Mar 22 2023 at 15:16):
2022-06-26 was about when it went live
Johan Commelin (Mar 22 2023 at 15:20):
huh! That shows how well I understood the system that I was using to work on LTE :rofl:
Last updated: Dec 20 2023 at 11:08 UTC