Trouble with old structures

Stream: general

[Scott Morrison]

I've run into trouble with apparently duplicated copies of ancestor fields for an old structure, and would like some help!

I've been experimenting with strengthening the definition of div_inv_monoid, to add the requirement that "division is sensible when it can be", that is, adding a field:

(div_eq : ∀ a b c : G, c * b = a → a / b = c)

(Notice this is true for all groups, for all groups-with-zero, and for nat. Leave aside the question of whether adding this field is a good idea.)

In fact, as this doesn't have anything to do with inv, I broke this out as an ancestor of div_inv_monoid:

class div_monoid (G : Type u) extends monoid G, has_div G :=
(div_eq : ∀ a b c : G, c * b = a → a / b = c)

With a few tweaks, which you can see on branch#div_monoid, we can make src/algebra/group/defs.lean compile.
However, I would really like to add a default field for group that provides the proof of div_eq.

When doing so, however, we find ourselves with a context that contains (besides much else):

a: div_inv_monoid G
mul: G → G → G
mul_left_inv: ∀ (a_1 : G), a_1⁻¹ * a_1 = 1
h: z * y = x

and the terrifying thing is that the multiplication in mul_left_inv refers to a, while the multiplication in h refers to mul, but we have no way of saying they are related!

[Scott Morrison]

(diff at https://github.com/leanprover-community/mathlib/compare/master..div_monoid if that's easier to read)

[Eric Wieser]

I think I saw something like this when providing a default for one of the ordered algebra classes. I think the goal view might be lying to you, and you should ignore a entirely

[Scott Morrison]

But I can't, because my hypothesis mul_left_inv is using it!

[Scott Morrison]

When I try to write the sensible proof I get unification errors between the two different multiplications.

[Scott Morrison]

I suspect it may be a Lean bug here.

[Scott Morrison]

So I guess I should be trying to minimise...

[Eric Wieser]

I'll see if I can find my previous thread...

[Eric Wieser]

Found it, https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Parent.20instance.20arguments.20in.20auto_param.20.2F.20opt_param/near/221832405

[Eric Wieser]

And the workaround I needed:

https://github.com/leanprover-community/mathlib/blob/e0fcb15c88cfed8e2a69a71e41725a0b0b0c2f15/src/algebra/ordered_monoid.lean#L52-L64

[Scott Morrison]

Is that on a branch? I'm having trouble checking it out.

[Scott Morrison]

I agree it looks similar!

[Scott Morrison]

Oh! I see, I deleted that proof recently, when I fixed the definition of ordered_monoid. :-)

[Scott Morrison]

In any case, I think I see what's going on now, and hopefully can imitate your solution. How on earth did you realise that this would solve the problem?

[Scott Morrison]

Actually, no, this isn't going to solve the problem.

[Scott Morrison]

The current situation is worse than the one you encountered: the field mul_left_inv, which we're absolutely going to need to complete the proof, already refers to the inaccessible a hypothesis.

[Eric Wieser]

It's not relevant to your problem, but I don't really understand why you want div_monoid here (vs just adding the field to div_inv_monoid); do you have a type in mind that is a div_monoid but not also a div_inv_monoid?

[Eric Wieser]

Ah of course, nat would be a sub_monoid

[Scott Morrison]

There are lots of interesting sub_add_monoids. I've been thinking a lot about fin n \to \nat recently. :-)

[Scott Morrison]

I think I've found one work-around: define group_aux, in which we add the (mul_left_inv : ∀ a : G, a⁻¹ * a = 1) field, and then extend that with group in which we fill in the default value of div_eq. I haven't actually written out the proof, but the instances now match up.

[Scott Morrison]

It's a bit unpleasant to have to add an extra intermediate typeclass to achieve this.

[Eric Wieser]

You could probably make the intermediate step a structure so that it doesn't make typeclass terms longer

[Scott Morrison]

Ah, good call!

[Scott Morrison]

And I found a hack that avoids introducing the intermediate structure:

[Scott Morrison]

use your letI trick in the mul_left_inv field as well.

[Scott Morrison]

That is, in the type of that field.

[Scott Morrison]

It feels a little ugly to break into tactic mode to specify the type of a field. (Particularly when we're defining something as fundamental as a group...)

[Kevin Buzzard]

If you look at mathlib's definition of a group right now it's already far far more complicated than one might guess, for technical reasons involving definitional equality. Nowadays I just show people the API rather than the internals

[Eric Wieser]

I get the feeling there _is_ a bug here, and the bug is that the context contains a: div_inv_monoid G and not a: div_inv_monoid G := {mul := mul, ...}.

[Scott Morrison]

Sounds very plausible. Perhaps @Gabriel Ebner will be able to tell us if it could be changed to work that way.

[Scott Morrison]

In any case, after some more playing with adding the field directly to div_inv_monoid (or an ancestor) I'm losing enthusiasm. Even when I can provide the default value at group, it is very fragile and often breaks when instantiating a group.

I think I'll try a lawful_div mixin typeclass with (div_eq : ∀ a b c : G, c * b = a → a / b = c) instead.

[Yaël Dillies]

Are you working on adding has_ordered_div : a / b ≤ c ↔ a ≤ c * b?

[Scott Morrison]

No.

[Yaël Dillies]

Oh oops :sweat_smile:

[Johan Commelin]

I guess nat is an example of div_monoid that is not a div_inv_monoid?

[Johan Commelin]

But using lawful_div as a mixin might indeed be a lot smoother.

[Scott Morrison]

Yes, \nat and fin n \to \nat are the main applications.

[Eric Wieser]

This class will let us eliminate docs#finsupp.nat_sub_self in favor of docs#sub_self, right?