Zulip Chat Archive

Stream: maths

Topic: Lemma naming contest


view this post on Zulip Patrick Massot (Sep 28 2020 at 15:07):

Heather and I need help to name lemmas (or find them already named in mathlib).

lemma inf_property' {α : Type*} [ordered_add_comm_group α] {s : set α} {a ε : α}
  (h₁ : is_glb s a) (h₂ : a  s) (h₃ : 0 < ε) :  b, b  s  a < b  ¬ a + ε  b :=
sorry

lemma inf_property {α : Type*} [decidable_linear_ordered_add_comm_group α] {s : set α} {a ε : α}
  (h₁ : is_glb s a) (h₂ : a  s) (h₃ : 0 < ε) :  b, b  s  a < b  b < a + ε :=
by simpa using inf_property' h₁ h₂ h₃

The proof is omitted for brevity, we had no trouble proving this. @Scott Morrison: enjoy the type class mess in these examples, in relation to our previous discussion.

view this post on Zulip Rob Lewis (Sep 28 2020 at 15:12):

is_glb.exists_lt_mem?

view this post on Zulip Patrick Massot (Sep 28 2020 at 15:14):

To me it sounds like a pretty random sampling from the statement, but if you like it then it's good enough for me.

view this post on Zulip Rob Lewis (Sep 28 2020 at 15:16):

It is exactly that, but most options will be unless you spell everything out. is_glb.exists_lt_mem_near?

view this post on Zulip Patrick Massot (Sep 28 2020 at 15:18):

And we have two lemmas to name.

view this post on Zulip Patrick Massot (Sep 28 2020 at 15:18):

TBH I don't expect the first one will get any use, maybe I should remove it.

view this post on Zulip Patrick Massot (Sep 28 2020 at 15:19):

Heather originally stated this for real numbers and I simply picked random type classes to make it look more respectable;

view this post on Zulip Reid Barton (Sep 28 2020 at 15:29):

is_glb.exists_between_self_add?

view this post on Zulip Reid Barton (Sep 28 2020 at 15:29):

Or exists_lt_add

view this post on Zulip Kevin Buzzard (Sep 28 2020 at 15:30):

Life was so much easier when we could just call it lemma 37.

view this post on Zulip Yury G. Kudryashov (Sep 28 2020 at 16:07):

Kevin Buzzard said:

Life was so much easier when we could just call it lemma 37.

Like in some parts of coq stdlib?

view this post on Zulip Kevin Buzzard (Sep 28 2020 at 16:21):

imagine trying to use the API :-) I was skeptical of this naming system at first, believing it simply would not scale. But often I realised one just had to break things down carefully into the right pieces and name them well.

view this post on Zulip Patrick Massot (Sep 28 2020 at 21:13):

Ok, I went with a variation on Reid's proposal. Next challenge is: where should we put:

lemma add_subgroup.int_mul_mem {R : Type*} [ring R] {G : add_subgroup R} (k : ) {g : R} (h : g  G) :
  (k : R) * g  G :=
begin
  convert add_subgroup.gsmul_mem G h k,
  exact (gsmul_eq_mul g k).symm,
end

view this post on Zulip Patrick Massot (Sep 28 2020 at 21:14):

This needs both ring and add_subgroup.

view this post on Zulip Heather Macbeth (Sep 28 2020 at 21:16):

@Patrick Massot Actually, I was wondering if the branch could be rewritten to use only k •ℤ g.

view this post on Zulip Heather Macbeth (Sep 28 2020 at 21:17):

I can try this later if you like the idea.

view this post on Zulip Patrick Massot (Sep 28 2020 at 21:17):

Maybe. I think the lemma is good to have anyway. It's bedtime here, so it's your turn to play with this branch. I think this lemma is the last remaining thing to move.


Last updated: May 12 2021 at 08:14 UTC