Zulip Chat Archive

Stream: general

Topic: Structure fields

Sebastien Gouezel (Nov 07 2018 at 15:22):

Is there a quick way to unfold something defined in a class? Let me be more specific. The product of metric spaces starts with

instance prod.metric_space_max [metric_space β] : metric_space (α × β) :=
{ dist := λ x y, max (dist x.1 y.1) (dist x.2 y.2),

Now, in a proof, I have dist x y where x and y are in a product metric space, and I would like to unfold it to max (dist x.1 y.1) (dist x.2 y.2).
I can change it, or use show, or prove a lemma giving the formula for the distance (with rfl) and then unfold this lemma. But I am wondering if I am missing something and if there is something I can just unfold, like prod.metric_space_max._secret_access_to_dist_ or something like that.

Johannes Hölzl (Nov 07 2018 at 15:51):

I don't think so. you can unfold prod.metric_space_max, and then call dsimp to unfold the projection. But this will not work in general. The best thing to do is to add the lemma as a simp-rule (which we should have anyway)

Sebastian Ullrich (Nov 07 2018 at 16:13):

Does simp [dist] not work? Or do you want to unfold only this specific dist?

Sebastien Gouezel (Nov 07 2018 at 16:20):

No, simp does not work here:

lemma prod.dist_eq {α : Type u} {β : Type v} [metric_space α] [metric_space β] {x y : α × β} :
  dist x y = max (dist x.1 y.1) (dist x.2 y.2) := by simp

fails with

simplify tactic failed to simplify

I have proved the lemma using rfl, and then used it explicitly later. This seems to be the canonical way to proceed. By the way, this is not the kind of thing I would want to unfold all the time, so I don't think it is a good simp lemma (but it is definitely useful to have it in explicit form like this)

Sebastian Ullrich (Nov 07 2018 at 16:23):

You have to pass the projection explicitly: simp [dist]

Sebastien Gouezel (Nov 07 2018 at 16:25):

Sorry, I should learn to read. Yes, simp [dist] works. Can you explain why?

Sebastian Ullrich (Nov 07 2018 at 16:27):

simp accepts not just rewrite lemmas but also function and projection names, which tell it to unfold usages of them

Sebastien Gouezel (Nov 07 2018 at 16:34):

OK, thanks (and this is very useful, I don't know why I never noticed this)

Kevin Buzzard (Nov 07 2018 at 16:41):

Oh nice trick Sebastian! I thought that the philosophy was to always prove these lemmas and give them names. Wait -- maybe that is the philosophy anyway.

Floris van Doorn (Nov 07 2018 at 16:45):

I also didn't know this. This is very useful!

Last updated: Aug 03 2023 at 10:10 UTC