Beginner question about typeclass constraints

Stream: lean4

[Andrija D.]

I wanted to try proving something about groups and I have

class Invertable (a : Type) where
  inv : a -> a

class GroupOp (a : Type) where
  op : a -> a -> a

infixl:70 " ⬝ " => GroupOp.op
notation:100 lhs:100 "⁻¹" => Invertable.inv lhs

class Group (a : Type) extends GroupOp a, Invertable a where
  e : a
  assoc : ∀ x y z : a, x ⬝ y ⬝ z = x ⬝ (y ⬝ z)
  mul_one : ∀ x : a, x ⬝ e = x
  left_inv : ∀ x : a, x⁻¹ ⬝ x = e

theorem right_inv [Group a] (a : Type) : ∀ (x : a), x ⬝ x⁻¹ = e :=
  _

But the x ⬝ x⁻¹ part is highlighted with "failed to synthesize instance" for GroupOp and Invertable. Both of those should be entailed by the [Group a] as far as I understand it, but I tried adding them explicitly just in case, yet the same error remains. This led me to ask, how do you even specify typeclass constraints in Lean 4? And ultimately of course, how do I go about solving this issue?

[Kevin Buzzard]

(Not that this is relevant to your question, but I think your axioms do not define a group, eg x^-1:=e and x.y:=x are a model, so your theorem is not provable)

[Mario Carneiro]

You introduced a after the typeclass [Group a], meaning you shadowed the auto-bound a with another a which is not a group

[Kevin Buzzard]

Possibly more relevant to your question: what happens if you switch the order of [Group a] and (a : Type) in the theorem? Right now the order doesn't make sense to me and I'm wondering if you have two as.

[Mario Carneiro]

It should probably be an error to shadow an auto-bound variable since that's almost certainly a typo

[Andrija D.]

It does work, although there's type mismatch on e, I probably should qualify it somehow.

As for the axioms, maybe haha, classically at least you can prove it with those afaik, and I was going to prove it in Lean to get a hang of some basic tactics

[Kevin Buzzard]

Yeah if you don't set up notation for e I guess you'll have to write a.e. You can take a look at mathlib4 for how they do it there, they use 1 and set up notation for it. I disagree with your claim that classically you can prove it. If I've not made a mistake then my original post explains why. If you make right_inv the axiom instead of left_inv you're ok (you can prove left_inv).

[Andrija D.]

@Kevin Buzzard

to prove e*x = x for all x
assume e*x =/= x
then
e*x = y, x =/= y
y^-1 * (e * x) = y^-1 * y
y^-1 * (e * x) = e (left inverse)
(y^-1 * e) * x = e (assoc)
y^-1 * x = e (right identity)
y^-1 * y = e (def of inverse)
y^-1 * y = y^-1 * x
x = y (contradiction to original assumption)

to prove x * x^-1 = e for all x
x^-1 * (x * x^-1) = x^-1 * e
x^-1 * (x * x^-1) = x^-1 (right identity)
(x^-1 * x) * x^-1 = x^-1 (assoc)
e * x^-1 = x^-1 (left inverse)
this is true based on that lemma above

Does this not prove it? I wrote the steps I took in the parens just to make sure I am not using any axioms I haven't defined, and it seems to work out. Or if I made a mistake somewhere along the way please correct me :pray:

[Ruben Van de Velde]

I don't follow your proof of x * x^-1 = e.

(It is known that associativity + left inverse + left identity or associativity + right inverse + right identity are sufficient to be a group, but I do think the sides need to match)

[Ruben Van de Velde]

And Kevin's counterexample does seem to work

[Ruben Van de Velde]

Confirmed in lean 3:

import group_theory.abelianization

class Group (a : Type) extends has_mul a, has_inv a :=
(e : a)
(assoc : ∀ x y z : a, x * y * z = x * (y * z))
(mul_one : ∀ x : a, x * e = x)
(left_inv : ∀ x : a, x⁻¹ * x = e)

inductive counter
| One
| Two

open counter
instance : Group counter :=
{ mul := λ x y, x,
  inv := λ x, One,
  e := One,
  assoc := λ x y z, rfl,
  mul_one := λ x, rfl,
  left_inv := λ x, rfl }

lemma no_right_inv : ¬(∀ (x : counter), x * x⁻¹ = One) :=
begin
  push_neg,
  refine ⟨Two, _⟩,
  trivial,
end

[Kyle Miller]

Kevin Buzzard said:

Yeah if you don't set up notation for e

The quick way to use an unqualified e for the identity is

export Group (e)

Then this works:

theorem right_inv [Group a] : ∀ (x : a), x ⬝ x⁻¹ = e :=
  _

[Andrija D.]

@Ruben Van de Velde
Correct me if I'm wrong, but I think we have
x = y <-> z*x = z*y, for all z

Then I'll just rewrite the proof as:
Assume x * x^-1 =/= e
Then:

1. x^-1 * (x * x^-1) =/= x^-1 * e (rewrite based on that assumption above)
2. x^-1 * (x * x^-1) =/= x^-1 (rewrite rhs based on right identity)
3. (x^-1 * x) * x^-1 =/= x^-1 (rewrite based on associativity)
4. e * x^-1 =/= x^1 (simplify based on left inverse)

This contradicts that mini lemma from before, and as far as I see I used only my own axioms (specific steps written between parens)

[Ruben Van de Velde]

Andrija D. said:

Ruben Van de Velde
Correct me if I'm wrong, but I think we have
x = y <-> z*x = z*y, for all z

I'm afraid I do have to correct you :)
With the same setup as above

lemma no_cancel : ¬(∀ (x y z: counter), z * x = z * y → x = y) :=
begin
  push_neg,
  refine ⟨Two, One, One, rfl, _⟩,
  trivial,
end

[Andrija D.]

But don't we have

1. z*x = z*y
2. z^-1 * (z * x) = z^-1 * (z * y) (apply the one sided implication x = y -> z*x = z*y)
3. (z^-1 * z) * x = (z^1 * z) * y (assoc)
4. e * x = e * y (left inverse)
5. e * x = x = e * y (lemma)
6. e*y = x (drop leftmost, eq reflex)
7. e*y = y = x (lemma)
8. x = y (drop leftmost, eq reflex)

Since you've proven this wrong in Lean I'm confused, but I can't find the mistake in my own steps :joy:

[Ruben Van de Velde]

Remember that you have assumed that x*e = x, not that e*x = x, so step 5 goes wrong

[Ruben Van de Velde]

(It turns out that assuming left-cancellativity is indeed sufficient, so the rest of your argument does work. Not sure if that's surprising.)

class Group' (a : Type) extends has_mul a, has_inv a :=
(e : a)
(assoc : ∀ x y z : a, x * y * z = x * (y * z))
(mul_one : ∀ x : a, x * e = x)
(left_inv : ∀ x : a, x⁻¹ * x = e)
(cancel : ∀ (x y z: a), z * x = z * y → x = y)
namespace Group'
lemma one_mul (a) [Group' a] (x : a) : e * x = x :=
begin
  apply cancel _ _ (e * x)⁻¹,
  have : ((e * x)⁻¹ * e) * x = e,
  { rw [assoc, left_inv], },
  rw mul_one at this,
  apply eq.trans _ this.symm,
  rw left_inv,
end
end Group'

[Andrija D.]

But e*x = x was my first lemma thingy, the first part in the message you originally replied to

[Ruben Van de Velde]

z * x = z * y → x = y and e * x = x appear to be equivalent given your other axioms - you can prove each by using the other

[Ruben Van de Velde]

Andrija D. said:

y^-1 * y = y^-1 * x (true up to here)
x = y (does not follow without assuming cancellativity)

[Andrija D.]

I forgot to write it, but doesn't it follow from uniqueness of the inverse?

Let a = y^-1, then we have

1. a * a^-1 = a * x
2. e = a*x
3. x = a^-1 = y

Steps 1 and 3 use (y^-1)^-1 = y which also uses the uniqueness of the inverse

[Ruben Van de Velde]

It's really easy to lose track of what you have and haven't proved at this early point :)

[Ruben Van de Velde]

(y^-1)^-1 = y is not true given your axioms

[Ruben Van de Velde]

(better: "does not follow from your axioms")

[Ruben Van de Velde]

Anyway, it really is a nice exercise to write this proof, but you will need to change your mul_one axiom to one_mul

[Ruben Van de Velde]

(I have a proof in lean3 I can link to once you've tried yourself)

[Andrija D.]

Ah you're right, that was the problem, I'll write the proof when I get some time. I guess the whole purpose of proof assistants is to avoid mistakes like these

[Patrick Massot]

It's definitely not the whole purpose, but it's part of it.