dsimp and iff.rfl

Stream: general

[Sebastien Gouezel]

In #6935, Yury discusses the following set of lemmas:

lemma mem_image2_eq : c ∈ image2 f s t = ∃ a b, a ∈ s ∧ b ∈ t ∧ f a b = c := rfl

@[simp]  lemma mem_image2 : c ∈ image2 f s t ↔ ∃ a b, a ∈ s ∧ b ∈ t ∧ f a b = c := iff.rfl

They are currently like that in data/set/basic.lean. Yury suggests to move the simp attribute to the other lemma, to make sure that it can be used by dsimp. I don't have an opinion on this, except that eq lemmas on Prop like this seem a little odd. I am wondering why we have these two lemmas, and why dsimp is designed to not use iff.rfl lemmas. Comments welcome!

[Yury G. Kudryashov]

I don't know why dsimp can't use iff.rfl lemmas and if it's hard to make it work.

[Mario Carneiro]

dsimp will only use lemmas proved by the literal string rfl

[Mario Carneiro]

not by refl or eq.refl _ or @rfl _ _

[Mario Carneiro]

This is a magic word that triggers the @[_refl_lemma] attribute

[Gabriel Ebner]

You can also set the _refl_lemma attribute yourself. :smile:

[Gabriel Ebner]

There's no fundamental reason why iff.rfl isn't accepted. A PR in that direction would be accepted (est. effort ~10 lines + 5 lines test).

[Mario Carneiro]

oh wow, dsimp just doesn't care

@[_refl_lemma] -- sure, why not?
theorem foo (x y z : ℕ) : x + y + z = x + (y + z) := add_assoc _ _ _

example (x y z : ℕ) : x + y + z = x + (y + z) :=
begin
  dsimp [foo], -- no problem
  -- ⊢ x + (y + z) = x + (y + z)
  refl, -- goals accomplished!
end -- wait a minute...

[Johan Commelin]

w00t

[Yury G. Kudryashov]

Will lemmas proved by iff.rfl cause failures in situations when dsimp vs simp is really important?

[Yury G. Kudryashov]

E.g., in some complex goal with dependent types etc.

[Kevin Buzzard]

This is great -- all our motive is not type correct problems are now solved, right?

[Yury G. Kudryashov]

Not yet. We have a proposed solution. It was neither implemented, nor tested.

[Kevin Buzzard]

I think Mario tested it already :-/ (not at lean right now but I have a bad feeling based on his comments...)

[Eric Wieser]

I tried a PR for this at leanprover-community/lean#723