Synthesizing typeclass instances for definitions

Stream: new members

[Giovanni Mascellani]

Hi, I don't understand why this code doesn't work:

import data.real.basic
import data.real.nnreal
import analysis.calculus.fderiv.basic

open_locale nnreal

-- Add a definition to simplify later code
def ℝ3 := fin 3 → ℝ

-- I need to add instances to the definition, so that fderiv will typecheck
instance : normed_add_comm_group ℝ3 := begin
  unfold ℝ3,
  apply_instance,
end

-- Why doesn't this work?!?
instance : normed_space ℝ ℝ3 := begin
  unfold ℝ3,  -- ERROR: "simplify tactic failed to simplify"
  apply_instance,
end

def zero_deriv (u : ℝ3 → ℝ) :=
∀ x, fderiv ℝ u x = 0

#check zero_deriv

Specifically, I am puzzled by the fact that the first instance has no problem unfolding my definition, while the second one fails. What's the formal difference between normed_add_comm_group and normed_space that causes this difference?

[Eric Wieser]

normed_space mentions ℝ3 twice (use set_option pp.implicit true to see where)

[Eric Wieser]

Does dunfold ℝ3 work?

[Eric Wieser]

Note that the real answer here is probably @[reducible] def ℝ3 := _ or even notation `ℝ3` := _

[Eric Wieser]

Also, this is your obligatory reminder that metric.ball (c : fin 3 → ℝ) r is the cube around c of side length 2r; not the round ball you were hoping for!

[Eric Wieser]

So my recommendation would be that you actually use notation `ℝ3` := euclidean_space ℝ (fin 3) unless you want your sphere to be cubes!

[Giovanni Mascellani]

Hi, thanks for your useful answers. Yes, dunfold works. I'm curious about the difference, but I guess it's something related to the tactic internal implementation, so I am not sure it's a good idea to dive too much into that while I'm still struggling with the basics.

[Giovanni Mascellani]

Eric Wieser said:

Note that the real answer here is probably @[reducible] def ℝ3 := _ or even notation `ℝ3` := _

What's the difference between the two alternatives?

[Eric Wieser]

I'm curious about the difference

I never really understood these tactics, but unfold is basically rw, and dunfold is basically dsimp. rw doesn't like rewriting dependent types (it's hard in general, though simp_rw knows how to do it). dsimp is very happy to, because all it ever has to do is say "the new state equals the old one by definition".

[Yakov Pechersky]

Handwavy explanation:
Regular def -- you aren't setting an alias, you want a new object that will have separate API, the fact of how it is defined it meant to be an implementation detaiL
Reducible def --- it's a new object, sure, but for many proofs and automation, you want things to automatically see through the implementation to the underlying object
Notation -- no new object whatsoever, it is just keystroke shorthand for the precise object you are referencing.

[Giovanni Mascellani]

Eric Wieser said:

So my recommendation would be that you actually use notation `ℝ3` := euclidean_space ℝ (fin 3) unless you want your sphere to be cubes!

Thanks for that too. For the moment I'm not sure I'm already caring about balls, but it's good to know. I guess that fin 3 → ℝ by default uses the sup metric, is that true?

[Eric Wieser]

What's the difference between the two alternatives?

A rough mental model is "notation is completely transparent and Lean can't tell the difference between it and the original at all", whereas reducible is "lean can tell the difference but promises to ignore it most of the time"

If it helps, ℝ is a notation not a @[reducible] def.

[Eric Wieser]

Yes exactly, it uses the sup metric

[Eric Wieser]

If that's what you expected, then fin 3 → ℝ is fine.

[Giovanni Mascellani]

Yakov Pechersky said:

Handwavy explanation:
Regular def -- you aren't setting an alias, you want a new object that will have separate API, the fact of how it is defined it meant to be an implementation detaiL
Reducible def --- it's a new object, sure, but for many proofs and automation, you want things to automatically see through the implementation to the underlying object
Notation -- no new object whatsoever, it is just keystroke shorthand for the precise object you are referencing.

Thanks. Some explanation along these lines would make for a nice addition to TPIL 10.5, which is what I was reading when trying to write my code.

[Eric Wieser]

To add to the mix, there's abbreviation ℝ3 := which means @[reducible] def but "oops I forgot to generate the equation lemma"