div_inv_monoid

Stream: general

[Yaël Dillies]

I feel like div_inv_monoid does not quite fulfill its purpose of common ancestor of group and group_with_zero because div and inv are currently lawless. We still have a fair share of lemmas which are duplicated between both. For example,

• docs#inv_one vs docs#one_inv
• docs#one_zpow vs docs#one_zpow₀
• docs#group.to_has_involutive_inv vs docs#group_with_zero.to_has_involutive_inv

What do people think of making div_inv_monoid stronger and thus potentially more useful for deduplicating lemmas?

[Eric Wieser]

The original motivation was div_eq_mul_inv, so it's not entirely lawless

[Yaël Dillies]

Okay so I will make div_inv_monoid extend has_involutive_inv. While I'm at it, shouldn't we have div_inv_comm_monoid?

[Yaël Dillies]

I am thinking of lemmas like docs#div_eq_inv_mul

[Yaël Dillies]

Let me also add another motivation to my original message: Pointwise operations (set, finset, filter) make a group except for a / a = 1. This means that we currently

• duplicate the instances: docs#set.div_inv_monoid, docs#set.div_inv_monoid' (same for the other two). This is rather minor
• lack almost all lemmas relating division and inversion. For example, when s t : finset α and α is a group, it is true that (t / s)⁻¹ = s / t but it is a pain to prove.

[Yaël Dillies]

div_inv_monoid/div_inv_comm_monoid could help here by being "a group (with zero), except that division doesn't have to bring you back to 1".

[Yaël Dillies]

I went through all instances of div_inv_monoid and it seems that nothing relies on the current precise implementation.

[Eric Wieser]

I agree that div_eq_inv_mul and similar lemmas look like sufficient justification for div_inv_comm_monoid

[Eric Wieser]

Do we already have the group versions of those lemmas?

[Yaël Dillies]

docs#div_eq_inv_mul' ?

[Yaël Dillies]

Some thoughts over at branch#stronger_div_inv_monoid. I am still figuring whichgroup /group_with_zero lemmas should be turned into axioms of div_inv_monoid. So far I've gone with inv_inv : a⁻¹⁻¹ = a and inv_mul_rev : (a * b)⁻¹ = b⁻¹ * a⁻¹` and it seems to work well.

[Yaël Dillies]

Okay I'm hitting a problem with docs#matrix.div_inv_monoid. Inversion of matrices isn't involutive.

[Yaël Dillies]

@Yakov Pechersky, is there any way to make this work?

[Eric Wieser]

I'd encourage you to do the div_inv_comm_monoid change first before going too deep into this second can of worms

[Yaël Dillies]

I mean, are you happy with me nuking matrix.div_inv_monoid into pieces?

[Yaël Dillies]

Given that data.matrix.zpow is a leaf file, this should be fine.

[Eric Wieser]

It might be worth waiting for @Anne Baanen's opinion on that kind of thing; originally div_inv_monoid was intended purely to unify the two notations, but with your suggested change it's now not able to do that any more (in this case, for matrices)

[Yaël Dillies]

Maybe the solution is to have both div_inv_class (for the notation) and div_inv_monoid (for the lemma deduplication).

[Eric Wieser]

I'm not sure about the names, but an additional typeclass would alleviate my specific concern above.

[Yaël Dillies]

If you look at branch#stronger_div_inv_monoid, you will also see that I had to manually copy the new fields from div_inv_monoid to a bunch of structures because extending div_inv_monoid would make them have many two redundant fields. Having this notation typeclass would fix this.

[Yaël Dillies]

What about has_lawful_div?

[Eric Wieser]

For the stronger or weaker notion?

[Yaël Dillies]

The weaker one.

[Yakov Pechersky]

Involution of inverse is too strong for matrices. But as we have it defined, inv thrice is inv.

[Yakov Pechersky]

Ask Anne, they made the matrix inv work. The zpow is just making its commutation make sense with npow.

[Yakov Pechersky]

I think the div_eq_inv_mul is a powerful law, because it implies statements about associativity of various operators. The fact that the matrix semiring admits an inverse that respects this structure is to me, reason enough to have it.

[Yaël Dillies]

It doesn't buy you much, though. You can take an arbitrary inv and derive div from it. Sure, we do get a few lemmas about the interaction of div and mul but that's it.

[Yaël Dillies]

matrix actually respects docs#matrix.mul_inv_rev, which is a pretty crucial lemma.

[Yaël Dillies]

Just look at the sheer amount of lemmas I can deduplicate/generalize and convince yourself: branch#stronger_div_inv_monoid

[Eric Wieser]

Removing an existing typeclass is an orthogonal discussion to adding a new one

[Eric Wieser]

(making a typeclass stronger to the point that existing instances are no longer true amounts to removing it and adding a new one with the same name)

[Yaël Dillies]

Okay so I have three propositions, modulo naming:

• Have a class which just contains the bare minimum for division and inversion and use it in extends clause to avoid copying over all the zpow fields, and add a stronger typeclass
  • div_inv_class = the current div_inv_monoid
  • div_inv_monoid = div_inv_class + has_involutive_inv
• Moderately strengthen div_inv_monoid and add a stronger typeclass
  • div_inv_class = the current div_inv_monoid + (a * b)⁻¹ = b⁻¹ * a⁻¹
  • div_inv_monoid = div_inv_class + has_involutive_inv. I did not yet manage to prove a * b = 1 → a⁻¹ = b from this, even though all candidate types (yes, even set) in mathlib respect it. If it doesn't hold generally, we might consider adding it as well.
• Strengthen div_inv_monoid and make the weaker one a mixin typeclass
  • div_inv_class = mixin for a / b = a * b⁻¹ and eventually the zpow fields. Does that work diamond-wise?
  • div_inv_monoid = the current div_inv_monoid + has_involutive_inv.

All three versions do not break any current instance of div_inv_monoid, and actually only one of them (namely docs#matrix.div_inv_monoid) can't be upgraded to the new version of div_inv_monoid.

[Yaël Dillies]

Another possibility for the names is div_inv_monoid and division_monoid.

[Eric Wieser]

Another name that may or may not be useful is has_distrib_inv to somewhat match docs#has_distrib_neg (although the type of distributivity is quite different)

[Reid Barton]

I wouldn't regard these as similar, distributivity is about the interaction of multiplication and addition, but here there is only multiplicative structure. You can see also the form of the axiom neg_mul is different from (a * b)⁻¹ = b⁻¹ * a⁻¹ because in neg_mul only one side is negated. It is like $g.xy = (g.x)y$ versus $g.xy = (g.x)(g.y)$ again.

[Yaël Dillies]

It's rather left or right commutativity of a unary and a binary functions.

[Yaël Dillies]

... which means that has_distrib_neg might be a misnomer.

[Reid Barton]

The name has_distrib_neg seems fine to me, it's the part of distributivity/bilinearity that has to do with negation in each argument.

[Reid Barton]

I mean it's not neg itself that is distributive, but otherwise it's fine.

[Reid Barton]

Oh it depends on whether you think of neg as part of the additive structure or as multiplication by $-1$; maybe that's what you meant?

[Yaël Dillies]

Yes, kind of

[Reid Barton]

Like $-(a + b) = (-1) * (a + b) = (-1) * a + (-1) * b = - a - b$ which now looks like div_inv stuff and not neg_mul yet I used the distributive law to get it

[Eric Wieser]

has_distrib_inv was a dumb suggestion because we need a name for the additive concept -(a + b) = -b + -a, sorry for the distraction.

[Eric Wieser]

And the additive name is obviously already taken

[Yaël Dillies]

Technically, it's not distributivity, but antidistributivity.

[Yaël Dillies]

I'm hitting something weird... Making docs#linear_ordered_add_comm_group_with_top extend has_sub and has_neg instead of sub_neg_monoid and copying over the fields makes Lean reject the default value for sub.

[Yaël Dillies]

Okay so I managed to make version 1 compile. The diff is rather huge, so I will first PR the definition of division_monoid, then the lemma generalizations.

[Anne Baanen]

It's been a while, hopefully my comments don't lead to too much wasted work!

The definition of div_inv_monoid had the following main motivation: group_with_zero used to assume div would be defined in terms of inv but for fractional_ideal it's the other way around. So we should replace the definitional equality a / b = a * b⁻¹ with a propositional one. Since group might have the same issue in the future, I made a superclass of both group and group_with_zero div_inv_monoid carrying a definition of div and inv and a proof div_eq_mul_inv. A few results nicely generalized from group(_with_zero) to div_inv_monoid but the motivation was to remove a technical obstruction to a specific instance, rather than generalizing as many lemmas as possible.

Having said that, I think it's a valuable project to generalize as much as reasonable, so indeed a stronger subclass of group and group_with_zero does make sense.

[Yaël Dillies]

If you could have a look at branch#stronger_div_inv_monoid and tell me what you think, I would be grateful!

[Anne Baanen]

Alright, here's my thoughts on the implementation:

• Mixins can be useful in specific cases, but they do have a tendency to hurt performance. In particular, the fully unfolded term size of a type determines the worst-case typechecking behaviour. So a long inheritance chain including mixins on a group G instance can really hurt typechecking on s : submonoid G, and even worse on typechecking x : s. Also, we probably don't need to switch often in applications between assuming that inverses are very lawful and only a bit lawful, so mixins probably don't help either.
• Naïvely I would assume "monoid with a (partial) inverse operator" is one with a strong specification on the inverse of inv_spec : ∀ a b, a * b = 1 → a⁻¹ = b. As far as I can tell, your code puts that in group still, and in the thread you noted that everything currently already satisfies this axiom. (An example of a division_monoid in your branch that doesn't satisfy inv_spec would be a comm_monoid where inv = id.)
• I think we should keep a class isomorphic to div_inv_monoid, since its syntactic role means it can be easily applied to any type with division and inverses, even if those inverses aren't neatly involutive (like matrix (pseudo)inverses).

[Anne Baanen]

So overall I think your branch is going in the right direction, except I would like the inv_spec axiom to be a part of the new class. The name division_monoid I'm not totally convinced of (since mathematicians tend to care more about inverses than division) but I guess it works since it's essentially the meet of group and division_ring.

[Yaël Dillies]

• division_monoid is not a mixin, though?
• If you think this axiom is justified, I will add it. The question now is whether this implies any of inv_mul_rev : ∀ a b, (a * b)⁻¹ = b⁻¹ * a⁻¹ or inv_inv : ∀ a, a⁻¹⁻¹ = a. I believe matrix is a counterexample for inv_inv, and I can't see how we could derive inv_mul_rev because we would need some cancellation property to prove (a * b) * (b⁻¹ * a⁻¹) = 1. One thing I also have to check is whether filter respects inv_spec.
• Does that mean you do not want to have both div_inv_monoid and division_monoid? because this is a problem for classes currently extending div_inv_monoid as we do not want to clutter their declarations with the redundant inv_mul_rev and inv_inv.
• I also thought about inversion_monoid, but I quite like the parallel with division_ring indeed.

[Anne Baanen]

• Indeed! I was trying to respond to some questions on mixins upthread.
• I agree that neither follows from inv_spec, for example if you take the naturals then neg_spec only says - 0 = 0 and leaves neg totally unspecified otherwise. But if filter also satisfies inv_spec then I don't see that adding it as a new axiom (alongside inv_inv and inv_mul_rev) will cause any problems, while providing a better base for the group axioms.
• I wanted to say that keeping div_inv_monoid as it is, like you have done, seems like the correct approach to me. Sorry if that was unclear.

[Yaël Dillies]

Fancy! I will figure out the filter conundrum and add inv_spec then! (do you think there's a better name for it?)

[Anne Baanen]

For groups it's called docs#eq_inv_of_mul_eq_one so let's use that.

[Yaël Dillies]

Okay so I managed to prove that inv_eq_of_mul_eq_one on α implies inv_eq_of_mul_eq_one on set α/finset α, but it was harder than I thought! When multiplication is cancellable, you can show that s and t are singletons and then s⁻¹ = t is pretty obvious, but of course a group_with_zero isn't cancellative.

example (h : s * t = 1) : s⁻¹ = t :=
begin
  ext a,
  rw mem_inv,
  have H : ∀ {a b}, a ∈ s → b ∈ t → a⁻¹ = b :=
    λ a b ha hb, inv_eq_of_mul_eq_one (h.subset $ mem_image2_of_mem ha hb),
  have hst : (s * t).nonempty := h.symm.subst one_nonempty,
  refine ⟨λ ha, _, λ ha, _⟩,
  { obtain ⟨b, hb⟩ := hst.of_image2_right,
    rwa [←inv_inv a, H ha hb] },
  { obtain ⟨b, hb⟩ := hst.of_image2_left,
    rwa [←H hb ha, inv_inv] }
end

[Floris van Doorn]

But H together with hst still are telling you that s and t are singletons, right?

[Yaël Dillies]

Hmm... You're right. I will try proving the earlier lemma without using cancellability.

[Yaël Dillies]

Update: filter is a division_monoid! I will now open the PR.

[Yaël Dillies]

#13860

[Yaël Dillies]

Here's the second bit of the refactor: #14000. It introduces new division_monoid lemmas to replace the group and group_with_zero ones (but leaves the deletion of those to the next PR).

[Yaël Dillies]

I tried my best to make it as straightforward as possible.

[Yaël Dillies]

I crunched the numbers for an upcoming paper and found out that division monoids allowed us to generalise 483 lemmas! 293 (manually generated) lemmas mention docs#division_monoid, and 190 mention docs#division_comm_monoid.

Source

import all

open tactic

def countp {α : Type*} (p : α → bool) : list α → ℕ
| []        := 0
| (x :: xs) := match p x with
  | ff := countp xs
  | tt := (countp xs).succ
  end

meta def is_division_monoid : expr → bool
| (expr.app (expr.const `division_monoid l) ty) := tt
| _ := ff

meta def is_comm_division_monoid : expr → bool
| (expr.app (expr.const `division_comm_monoid l) ty) := tt
| _ := ff

meta def contains_division_monoid : expr → bool
| (expr.pi n bi ty la) := is_division_monoid ty || contains_division_monoid la
| _ := ff

meta def contains_comm_division_monoid : expr → bool
| (expr.pi n bi ty la) := is_comm_division_monoid ty || contains_comm_division_monoid la
| _ := ff

meta def count_division_monoid : command := do
  env ← get_env,
  let l := declaration.type <$> env.get_decls.filter (λ decl, ¬ decl.is_auto_generated env),
  tactic.trace ("division_monoid: " ++ to_string (countp contains_division_monoid l)),
  tactic.trace ("division_comm_monoid: " ++ to_string (countp contains_comm_division_monoid l))

#eval count_division_monoid
/-
division_monoid: 293
division_comm_monoid: 190
-/

[Floris van Doorn]

You're counting all declarations - not just lemmas - right? I'm not sure whether declarations like docs#group.to_division_monoid and docs#prod.division_monoid should count towards the usefulness of division monoids.

[Yaël Dillies]

The limitations of my metaprogramming skills have been uncovered :grinning_face_with_smiling_eyes: How do I filter out instances?

[Floris van Doorn]

An easy check is to use docs#declaration.is_theorem if you only want to count lemmas (I'm quite sure all instances are not theorems, even if they are propositional instances). You can use docs#tactic.is_instance to check for instances.