Porting Algebra.Group.Ext

Stream: mathlib4

[Riccardo Brasca]

I am porting Algebra.Group.Ext in #837 and I am stuck at the very beginning. The mathlib3 code is

import algebra.hom.group

universe u

@[ext, to_additive]
lemma monoid.ext {M : Type u} ⦃m₁ m₂ : monoid M⦄ (h_mul : m₁.mul = m₂.mul) : m₁ = m₂ :=
begin
  have h₁ : (@monoid.to_mul_one_class _ m₁).one = (@monoid.to_mul_one_class _ m₂).one,
    from congr_arg (@mul_one_class.one M) (mul_one_class.ext h_mul),
  set f : @monoid_hom M M (@monoid.to_mul_one_class _ m₁) (@monoid.to_mul_one_class _ m₂) :=
    { to_fun := id, map_one' := h₁, map_mul' := λ x y, congr_fun (congr_fun h_mul x) y },
  have hpow : m₁.npow = m₂.npow, by { ext n x, exact @monoid_hom.map_pow M M m₁ m₂ f x n },
  unfreezingI { cases m₁, cases m₂ },
  congr; assumption
end

The mathlib4 is

import Mathlib.Algebra.Hom.Group

universe u

@[ext, to_additive]
theorem Monoid.ext {M : Type u} ⦃m₁ m₂ : Monoid M⦄ (h_mul : m₁.mul = m₂.mul) : m₁ = m₂ := by
  have h₁ : (@Monoid.toMulOneClass _ m₁).one = (@Monoid.toMulOneClass _ m₂).one :=
    congr_arg (MulOneClass.one M) (MulOneClass.ext h_mul)
  let f : @MonoidHom M M (@Monoid.toMulOneClass _ m₁) (@Monoid.toMulOneClass _ m₂) :=
    { toFun := id, map_one' := h₁, map_mul' := fun x y => congr_fun (congr_fun h_mul x) y }
  have hpow : m₁.npow = m₂.npow := by
    ext (n x)
    exact @MonoidHom.map_pow M M m₁ m₂ f x n
  cases m₁
  cases m₂
  congr <;> assumption
#align monoid.ext Monoid.ext

The first error is about @MulOneClass.one M. Why there is no MulOneClass.one? I can fix it with @One.one M, but the mathlib3 way is better in my opinion.

Using @One.one M is get an error at MulOneClass.ext h_mul

application type mismatch
  congr_arg (@One.one M) (MulOneClass.ext ?m.404)
argument
  MulOneClass.ext ?m.404
has type
  ?m.81 = ?m.82 : Prop
but is expected to have type
  MulOneClass.toOne = MulOneClass.toOne : Prop

I don't understand exactly what's wrong here...

[Eric Wieser]

I think this is because of old_structure_cmd

[Eric Wieser]

Does fun (inst : MulOneClass M) => inst.one work?

[Riccardo Brasca]

It moves the error later, so I guess it works... but it's really hard to read

[Eric Wieser]

The problem is that in Lean3/old structures mul_one_class.one is a real field, but in Lean 4/new structures M.one is actualy syntax for M.to_has_one.one but only works when used as field notation

[Eric Wieser]

I think it would be a reasonable feature request to ask that MulOneClass.one be syntax for the lambda function above.

[Floris van Doorn]

This seems like the easiest thing to work around. Note that if the expected type of the function is known (\..one) will work.

[Riccardo Brasca]

OK, not it complains about

  let f : @MonoidHom M M (@Monoid.toMulOneClass _ m₁) (@Monoid.toMulOneClass _ m₂) :=
    { toFun := id, map_one' := h₁, map_mul' := fun x y => congr_fun (congr_fun h_mul x) y }

with

synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
  toMulOneClass
inferred
  toMulOneClass

:rolling_eyes:

[Floris van Doorn]

The proof has to be different anyhow, since the shape of the structure is different because of the new bundling.

[Riccardo Brasca]

OK, I seems more complicated than I thought. I am closing my WIP PR (where I basically didn't do anything) to "free" the file to anyone else interested, since I don't have much time this weekend.

[Richard Osborn]

So is something like the following even possible to write in lean4?

import Mathlib.Algebra.Hom.Group

variable (M) (m₁ m₂ : Monoid M)

#check @MonoidHom M M (@Monoid.toMulOneClass M m₁) (@Monoid.toMulOneClass M m₂) -- M →* M : Type u_1

def f : @MonoidHom M M (@Monoid.toMulOneClass M m₁) (@Monoid.toMulOneClass M m₂) where
  toFun := id
  map_one' := sorry
  map_mul' := sorry

[Scott Morrison]

I mean, it is impossible to fill in the sorries in any version of Lean, so I guess not?

[Richard Osborn]

So I had a crack at porting the file. I managed to fix the proof of Monoid.ext and fix the proofs of injectivity, but was unable to fix the proofs for DivInvMonoid.ext and Group.ext. I've created a PR mathlib4#850, so if anyone has any insights, please feel free to work on it.

[Richard Osborn]

My main issue was that lean4 forgets that m₁ is a DivInvMonoid when deconstructing the instance, so I don't have access to theorems that require a DivInvMonoid instance.

[Richard Osborn]

I also couldn't figure out how to tell lean that the div in DivInvMonoid was the same as the hDiv in div_eq_mul_inv.

[Richard Osborn]

So I managed to fix the first issue with deconstructing a class by delaying it in the proof giving me access to theorems for DivInvMonoid and Group. I feel like the main issue preventing me from completing the proofs is that lean is converting (·*·) and (·/·) into an hMul and hDiv and I can't quite wrap my head around how to give lean the information to apply lemmas using (·*·) and (·/·). I've pushed updated versions of the proofs. Hopefully, the finishing touches to them is fairly trivial.

[Eric Wieser]

Scott Morrison said:

I mean, it is impossible to fill in the sorries in any version of Lean, so I guess not?

I think this question was asked poorly; in the real context, there are hypotheses available that say the one and mul agree

[Eric Wieser]

I think the problem is the new-style classes interfering with

  let f : @MonoidHom M M (@Monoid.toMulOneClass _ m₁) (@Monoid.toMulOneClass _ m₂) :=
    { toFun := id, map_one' := h₁, map_mul' := fun x y => congr_fun (congr_fun h_mul x) y }

In particular, this calls MonoidHom.mk and OneHom.mk, and seems to pass the wrong typeclass arguments into these

[Eric Wieser]

This works:

  let f : @MonoidHom M M m₁.toMulOneClass m₂.toMulOneClass :=
    @MonoidHom.mk _ _ (_) _ (@OneHom.mk _ _ (_) _ id h₁)
      (fun x y => congr_fun (congr_fun h_mul x) y)

[Eric Wieser]

I'm very new to Lean4; what does (_) mean compared to _?

[Eric Wieser]

Also, this feels like a place where the opaqueness of inferInstance is causing a problem (swapping m₁.toMulOneClass for the suggested by letI := m₁ <;> infer_instance fails)

[Eric Wieser]

I was able to copy across the mathlib3 proof

lemma div_inv_monoid.ext {M : Type*} ⦃m₁ m₂ : div_inv_monoid M⦄ (h_mul : m₁.mul = m₂.mul)
  (h_inv : m₁.inv = m₂.inv) : m₁ = m₂ :=
begin
  have h₁ : (@div_inv_monoid.to_monoid _ m₁).one = (@div_inv_monoid.to_monoid _ m₂).one,
    from congr_arg (@monoid.one M) (monoid.ext h_mul),
  set f : @monoid_hom M M (by letI := m₁; apply_instance) (by letI := m₂; apply_instance) :=
    { to_fun := id, map_one' := h₁, map_mul' := λ x y, congr_fun (congr_fun h_mul x) y },
  have hpow : (@div_inv_monoid.to_monoid _ m₁).npow = (@div_inv_monoid.to_monoid _ m₂).npow :=
    congr_arg (@monoid.npow M) (monoid.ext h_mul),
  have hzpow : m₁.zpow = m₂.zpow,
  { ext m x,
    exact @monoid_hom.map_zpow' M M m₁ m₂ f (congr_fun h_inv) x m },
  have hdiv : m₁.div = m₂.div,
  { ext a b,
    exact @map_div' M M _ m₁ m₂ _ f (congr_fun h_inv) a b },
  unfreezingI { cases m₁, cases m₂ },
  congr, exacts [h_mul, h₁, hpow, h_inv, hdiv, hzpow]
end

as

theorem DivInvMonoid.ext {M : Type _} ⦃m₁ m₂ : DivInvMonoid M⦄ (h_mul : m₁.mul = m₂.mul)
  (h_inv : m₁.inv = m₂.inv) : m₁ = m₂ := by
  have := Monoid.ext h_mul
  have h₁ : m₁.one = m₂.one := congr_arg (·.one) this
  let f : @MonoidHom M M m₁.toMulOneClass m₂.toMulOneClass :=
    @MonoidHom.mk _ _ (_) _ (@OneHom.mk _ _ (_) _ id h₁)
      (fun x y => congr_fun (congr_fun h_mul x) y)
  have hpow : m₁.npow = m₂.npow := congr_arg (·.npow) (Monoid.ext h_mul)
  have hzpow : m₁.zpow = m₂.zpow := by
    ext (m x)
    exact @MonoidHom.map_zpow' _ _ (_) _ f (congr_fun h_inv) x m
  have hdiv : m₁.div = m₂.div := by
    ext (a b)
    exact @map_div' _ _ (_) (_) _
      (@MonoidHom.monoidHomClass _ _ (_) _) f (congr_fun h_inv) a b
  rcases m₁ with @⟨_, ⟨inv₁⟩, ⟨div₁⟩, _, zpow₁⟩
  rcases m₂ with @⟨_, ⟨inv₂⟩, ⟨div₂⟩, _, zpow₂⟩
  congr

[Eric Wieser]

It seems that @ and (_) is ultimately the trick here

[Eric Wieser]

Maybe it would be best to restart from the mathport output for the other instances now that we know that?

[Richard Osborn]

Whatever ends up being the most readable/maintainable. The original mathport output is also in a block comment for Group.ext. Now that you have the MonoidHom working, it should be a similar proof. Are you planning on working on that one? I can probably figure it out, following this method.
I am still slightly concerned that (·*·) and (·/·) are hMuls and hDivs. And it seems as though Mul and Div don't extend the classes, which seems weird to me. I'm assuming there's a good reason.

[Richard Osborn]

Ok, I've fixed up all the proofs and have emulated the mathlib3 versions. Thank you for the help!
Btw, is the extra destructuring that is happening at the end of these proofs something that congr should be able to figure out on its own?

[Riccardo Brasca]

Do you mind adding to the porting wiki what you had to do?

[Richard Osborn]

As far as I understand it, to create a MonoidHom (or OneHom) with ambiguous instances, you need to use the mk constructor and then use (_) to delay the TC inference on the input type (or more generally any type in the 'contravariant' position?).

[Eric Wieser]

It's not delaying it, it's disabling it entirely

[Eric Wieser]

It's forcing it to use unification instead of typeclass search

[Eric Wieser]

Lean3 did that automatically for {...} notation