sensible constructor for `add_comm_group`

Stream: Is there code for X?

[Kevin Buzzard]

I'm making a thing, and the thing is an add_comm_group. I am happy to prove add_assoc, add_comm, zero_add and add_left_neg, but I don't really want to prove add_zero because these proofs are a bit tedious and I want to deduce it from what we have already. But I don't know how to rw add_comm where add_comm refers to the field I just filled in a few lines above.

If I could figure out how to do the rewrites here:

def mk'' {G : Type*} [has_add G] [has_zero G] [has_neg G] : add_comm_group G :=
{ add := (+), zero := 0, neg := has_neg.neg,
  add_assoc := sorry, -- happy to prove this
  add_comm := sorry,  -- and this
  zero_add := sorry,  -- and this
  add_left_neg := sorry,  -- and this
  add_zero := λ a, by sorry,-- but now I want to cheat and can't get this to work:
  -- `by{rw add_comm, apply add_left_neg }, -- I mean "the proofs I just did above"`
}

then I guess we don't need another constructor, but I couldn't so I wrote this:

def mk' {G : Type*} [has_add G] [has_zero G] [has_neg G]
  (ax1 : ∀ a b c : G, (a + b) + c = a + (b + c))
  (ax2 : ∀ a b : G, a + b = b + a)
  (ax3 : ∀ a : G, 0 + a = a)
  (ax4 : ∀ a : G, -a + a = 0) : add_comm_group G :=
{ add := (+),
  add_assoc := ax1,
  zero := 0,
  zero_add := ax3,
  add_zero := λ a, by {rw ax2, exact ax3 a},
  neg := has_neg.neg,
  add_left_neg := ax4,
  add_comm := ax2 }

Is that constructor already in mathlib, and if not then should it be?

[Alex J. Best]

I guess this is really a constructor for comm_monoid , which you can use with the .. notation if you want to make a group

[Adam Topaz]

You could do something like

def mk'' {G : Type*} [has_add G] [has_zero G] [has_neg G] : add_comm_group G :=
let h1 : ... := ... in
{ add := (+), zero := 0, neg := has_neg.neg,
  add_assoc := sorry, -- happy to prove this
  add_comm := h1,  -- and this
  zero_add := sorry,  -- and this
  add_left_neg := sorry,  -- and this
  add_zero := λ a, by sorry,-- but now I want to cheat and can't get this to work:
  -- `by{rw h1, apply add_left_neg }, -- I mean "the proofs I just did above"`
}

[Jireh Loreaux]

Is there any reason to worry about bad definitional unfolding (of add) caused by using this let binding? I think I did something like this somewhere but a reviewer advised against it because of definitional unfolding; I can't remember which PR offhand though, so maybe the situation is different.

[Adam Topaz]

The h1 in my suggestion is a proof of a prop so it shouldn't cause any defeq issues

[Adam Topaz]

it may not look to nice if you unfold the add_comm_group instance in a proof (you would see a let ... in ... in the tactic state), but a dsimp should eliminate that let, and one shouldn't really unfold instances to begin with.

[Eric Wieser]

This might not be true in Kevin's case, but most of the time when I find myself proving add_comm_group G I find that add_comm_monoid G is actually true in a more general case, and so you should really just prove that first.

[Kevin Buzzard]

I don't really want to write the statement of add_comm either. Is there any reason not to add the constructor?

[Junyan Xu]

In tactic mode, there is a trick like this, without writing the statement:

begin
  have := _,
  split,
  ...
  { exact this }, /- the `add_left_neg` field -/
  { rw h1, apply this }, /- the `add_zero` field -/
  { /- now prove `this` -/ },
end

This trick can also be used to do wlog. It would be nice if Lean could support it natively.

[Mario Carneiro]

you can do this in lean 4 using ?a in both places

[Junyan Xu]

Oh I forgot: you also still need to prove this in the end. (edited)

[Kevin Buzzard]

ha ha I suspect that this will work in my use case :-)

[Junyan Xu]

Is there a way to translate this proof faithfully into Lean 4? I did it manually in mathlib4#1399 but had to write out the sublemma ∀ b c, r b c → f a c = f a b * f b c. I tried to use ?_ but didn't succeed in the end. Also it seems I get strange error when I write have : ... without following it by :=.

import algebra.group.defs

lemma multiplicative_of_total {α β : Type*} [monoid β] (f : α → α → β)
  (r : α → α → Prop) [t : is_total α r]
  (hswap : ∀ a b, f a b * f b a = 1)
  (hmul : ∀ {a b c}, r a b → r b c → f a c = f a b * f b c)
  (a b c : α) : f a c = f a b * f b c :=
begin
  have := _,
  obtain hbc | hcb := t.total b c,
  { revert b c, exact this },
  { rw [this c b hcb, mul_assoc, hswap c b, mul_one] },
  intros b c hbc,
  obtain hab | hba := t.total a b,
  { exact hmul hab hbc },
  obtain hac | hca := t.total a c,
  { rw [hmul hba hac, ← mul_assoc, hswap a b, one_mul] },
  { rw [← one_mul (f a c), ← hswap a b, hmul hbc hca, mul_assoc, mul_assoc, hswap c a, mul_one] },
end

[Eric Rodriguez]

ah, for easier-to-readness, this is effectively the sort of proof that Junyan wants to work:

example : false :=
begin
  have := _,
  exact this,
  exact sorry,
end

suffices seems to get a bit closer, but Lean still doesn't like it:

image.png

[Junyan Xu]

If this could be made to work, maybe it can cover most of the cases where wlog is used in mathlib3. Since wlog is yet to be ported, some ported files now come with notes to replace proofs once wlog is ported (but swap_var may be working nicely enough).

[Eric Rodriguez]

it may be worth putting this on the lean4 stream

[Eric Rodriguez]

I feel like this may be indicative of a bigger issue that's relevant in all porting. Lean4 seems hesitant to call a metavar a function, and also unify it with stuff given by exact, and when we have tactics that don't work as well as lean3...