Zulip Chat Archive

Stream: maths

Topic: Defining instances


view this post on Zulip Sebastien Gouezel (Oct 13 2018 at 16:11):

I am trying to define an instance of a normed space starting from a norm satisfying the right axioms, but I would need some help. Here is the situation:

def normed_group_of_norm {α : Type} [a: add_comm_group α] [b: has_norm α]
(norm_triangle : x y: α, norm (x + y)  norm x + norm y)
(norm_zero : norm (0 : α) = 0)
(eq_of_norm_eq_zero : (x:α), norm x = 0  x = 0)
(norm_neg : (x:α), norm (-x) = norm x) : normed_group α :=
have A: metric_space α := metric_space.mk''
{ dist := λx y, norm (x - y),
  dist_self := by simp [norm_zero],
  eq_of_dist_eq_zero := λx y hxy, sub_eq_zero.1 (eq_of_norm_eq_zero _ hxy),
  dist_comm := λx y, begin have A := norm_neg (x-y), simp at A, simp [A.symm] end,
  dist_triangle :=λx y z, by simpa using norm_triangle (x-y) (y-z)
},
{
   dist_eq := sorry,
    ..a, ..b, ..A
}

A normed group is an abelian group together with a norm, with the property that the distance should be given by dist x y = norm(x-y). It extends metric spaces, so I first define the metric space structure I want (A above), and then I just have to check this equality, which is by definition of A. But I do not see how to get access to the formula in the definition of A, so I am stuck...

view this post on Zulip Kenny Lau (Oct 13 2018 at 16:11):

don't we already have this?

view this post on Zulip Sebastien Gouezel (Oct 13 2018 at 16:13):

No, I don't think so. Normed groups are defined in analysis/normed_space.lean, but there is no constructor just in terms of a norm.

view this post on Zulip Kenny Lau (Oct 13 2018 at 16:15):

is there anything about abs?

view this post on Zulip Sebastien Gouezel (Oct 13 2018 at 16:16):

My question is not specifically about this situation, it is rather that there is something I don't know about the syntax or the way to access fields.

view this post on Zulip Kenny Lau (Oct 13 2018 at 16:18):

(maybe unrelated) I recall there's no wrapper for norm_mul

view this post on Zulip Sebastien Gouezel (Oct 13 2018 at 16:31):

Here is the same question in a completely basic setting:

structure my_test := (f :   )

lemma foo : true :=
have A : my_test := {f := λx, x},
have B: x, A.f x = x := begin intros x, sorry end,
trivial

I just want to get access to the definition of the field f in the structure I have constructed.

view this post on Zulip Kenny Lau (Oct 13 2018 at 16:32):

that isn't possible because have doesn't store data

view this post on Zulip Johannes Hölzl (Oct 13 2018 at 16:32):

Yes: you need to use let m : metric_space A := ... instead of the have

view this post on Zulip Sebastien Gouezel (Oct 13 2018 at 16:32):

Thanks!

view this post on Zulip Patrick Massot (Oct 13 2018 at 16:42):

Sébastien, I'm not sure I understand your question, but https://github.com/leanprover/mathlib/blob/master/analysis/normed_space.lean#L276 does define a normed stuff instance explicitly

view this post on Zulip Sebastien Gouezel (Oct 13 2018 at 16:50):

Yes, but the metric space structure had already been defined before on \R. I am maximally lazy here: starting just from the norm, I want to define simultaneously the metric space and the normed space. In the same way, when you have a distance, you don't want to define by hand the topological structure, then the uniform structure, then the metric space structure: you want a constructor that does all this for you.

view this post on Zulip Sebastien Gouezel (Oct 13 2018 at 16:52):

And it works perfectly thanks to the hints of Kenny and Johannes:

structure normed_group.core (α : Type) [add_comm_group α] [has_norm α] :=
(norm_triangle : x y: α, norm (x + y)  norm x + norm y)
(norm_zero : norm (0 : α) = 0)
(eq_of_norm_eq_zero : (x:α), norm x = 0  x = 0)
(norm_neg : (x:α), norm (-x) = norm x)

def normed_group_of_norm {α : Type} [a: add_comm_group α] [b: has_norm α]
(m : normed_group.core α) : normed_group α :=
let A : metric_space α := metric_space.mk''
{ dist := λx y, norm (x - y),
  dist_self := by simp [m.norm_zero],
  eq_of_dist_eq_zero := λx y hxy, sub_eq_zero.1 (m.eq_of_norm_eq_zero _ hxy),
  dist_comm := λx y, begin have A := m.norm_neg (x-y), simp at A, simp [A.symm] end,
  dist_triangle :=λx y z, by simpa using m.norm_triangle (x-y) (y-z)
} in
{ dist_eq := λx y, rfl,
  ..a, ..b, ..A
}

(Don't try this, it depends on my emetric spaces pull request for the metric space constructor)

view this post on Zulip Kenny Lau (Oct 13 2018 at 16:53):

I would define the metric space separately first

view this post on Zulip Kenny Lau (Oct 13 2018 at 16:53):

and avoid let

view this post on Zulip Kenny Lau (Oct 13 2018 at 16:54):

if you still want to keep it, I would add set_option zeta.compiler true

view this post on Zulip Johan Commelin (Oct 13 2018 at 16:55):

@Sebastien Gouezel The let statements aren't parsed away, they go all the way down to the kernel. Sometimes I wish there was a "syntactic sugar" variant, maybe called where.

view this post on Zulip Johan Commelin (Oct 13 2018 at 16:55):

But like Kenny suggests, you might want to split it up any way.

view this post on Zulip Sebastien Gouezel (Oct 13 2018 at 16:57):

How would you avoid the let? I insist on having one single constructor that takes a normed_group.core and gives a normed group, that's really the point here.

view this post on Zulip Johan Commelin (Oct 13 2018 at 17:03):

This constructor could call another one, right?

view this post on Zulip Johan Commelin (Oct 13 2018 at 17:04):

If you just factor out the let-statement into a separate instance. Or am I missing something?

view this post on Zulip Johan Commelin (Oct 13 2018 at 17:04):

Maybe some refine_struct magic could also help. But I'm not an expert on this.


Last updated: May 12 2021 at 08:14 UTC