branch#gsmul_instance

Stream: general

[Johan Commelin]

@Sebastien Gouezel has started a major refactor of mathlib at branch#gsmul_instance. The goal is to get rid of the global instances add_comm_monoid.nat_semimodule, add_comm_group.int_module and algebra_int. So far, it seems to be a lot of work, but also means we get rid of a lot of annoying diamond problems. So it definitely seems worth it. Kudos to @Sebastien Gouezel ! :muscle: :octopus:

I just did a bit of work on this branch, and Lean complained that it couldn't find an instance algebra int (zmod p). Of course this is to be expected. So I went back to the file on zmod, and added that instance. But during breakfast I realised that Lean will also need algebra nat (zmod p). You see where this is going: for every

instance : ring (foo_bar quux) := _

we will now need two extra lines

instance : algebra nat (foo_bar quux) := algebra_nat _

instance : algebra int (foo_bar quux) := algebra_int _

(Actually, algebra nat should already happen for every semiring.)
And we also need instance : module int (xyzzy baz) for every instance : add_comm_group (xyzzy baz).

Is this something that we can automate? Can we change Lean 3.37.42, so that it will trigger extra instance declarations whenever it parses one of

instance : add_comm_monoid
instance : add_comm_group
instance : semiring -- or comm_semiring
instance : ring -- or comm_ring

[Johan Commelin]

cc @Gabriel Ebner @Rob Lewis @Floris van Doorn @Scott Morrison

[Damiano Testa]

Would it be helpful or disrupting to have a nat_semimodule instance on int alone?

[Johan Commelin]

I think we need it on every abelian group.

[Sebastien Gouezel]

I had a crazy idea that should fix all the diamond issues while keeping the $\Z$-module instance on add_comm_groups. I'd like to hear your thoughts about it.

[Johan Commelin]

But you want to disable algebra_int, right?

[Johan Commelin]

If you keep add_comm_group.int_module, how can we make sure that we don't hit diamonds on $\Z$ again?

[Sebastien Gouezel]

The problem: we want every add_comm_group to be a $\Z$-module. For now, this is registered through the instance add_comm_group.int_module, where the multiplication is gsmul, defined by induction over the integer, through the addition. But some add_comm_groups get different module instances. For instance, if M and N are modules over a ring R, then the space of linear maps M →ₗ[R] N has both an add_comm_group and an R-module structure. When R = ℤ, you get two ℤ-module structures on M →ₗ[ℤ] N, the add_comm_group.int_module one, and the one coming from the linear structure. And they are not defeq.

[Sebastien Gouezel]

The solution: a variation on forgetful inheritance. I want to enrich the definition of add_comm_group, by adding data: a ℤ-action with the right axioms. Then the instance from add_comm_group to ℤ-modules would use this data (and we would remove completely add_comm_group.int_module). We would only need to make sure that whenever one can construct a new ℤ-module, the module structure is defeq to the one stored in the add_comm_group.

[Johan Commelin]

But then we can do the same thing with comm_ring and algebra_int, right?

[Johan Commelin]

So we should remove that algebra int (zmod n) instances again?

[Sebastien Gouezel]

An example: when we define M →ₗ[R] N, we have to register an add_comm_group on this space. According to the scheme above, we should be careful about the compatibility. Since the R-action is given by (r • f) (x) = r • (f x), using the action in the target space, we define the ℤ-action in the same way, by (n • f) (x) = n • (f x). Then in the particular case of R = ℤ, everything matches, and there is no diamond.

[Sebastien Gouezel]

Johan Commelin said:

But then we can do the same thing with comm_ring and algebra_int, right?

Since a comm_ring is in particular an add_comm_group, yes, it would carry such a ℤ-action. We can define it to be left-multiplication. And then in the case of R = ℤ, it means that our ℤ-module structure coming from the add_comm_group would be defeq to the ℤ-module structure coming from the ring structure, without having to tweak the definition of ℤ-multiplication.

[Sebastien Gouezel]

Johan Commelin said:

So we should remove that algebra int (zmod n) instances again?

Yes, we would also remove all the manual algebra_int instances, and define a global one that would be completely diamond-free.

[Johan Commelin]

ok, I think I see how this is going to work.

[Johan Commelin]

But we'll need to do the same trick for nat and add_comm_monoid

[Sebastien Gouezel]

And we should also do the same for nat and add_comm_monoid, yes.

[Sebastien Gouezel]

I say this is a crazy idea because this would be a huge refactor.

[Sebastien Gouezel]

But this ℤ-module thing has been a major painpoint several times, so I think it would probably be worth it.

[Sebastien Gouezel]

I have a few questions abouth this idea:

[Johan Commelin]

And then there is https://github.com/leanprover-community/mathlib/blob/master/src/data/zmod/basic.lean#L337

instance (R : Type*) [comm_ring R] [char_p R n] : algebra (zmod n) R :=
(zmod.cast_hom (dvd_refl n) R).to_algebra

[Johan Commelin]

So we can now get two instances of algebra (zmod n) (zmod n)

[Sebastien Gouezel]

1) would it really solve all diamond problems in this area one can think of (@Eric Wieser has thought a lot about it, so maybe he could think of other examples I have overlooked).

[Johan Commelin]

One from :up: and another from algebra.id

[Sebastien Gouezel]

2) For the implementation, I expect that we could add a default field and defaults arguments for the prop fields, so hopefully this shouldn't make to much of a difference in definitions where we don't care about the defeqness, and we would only change things where they matter. But I wonder about things like to_additive or the additive/multiplicative tricks, especially since the fields in add_comm_group and comm_group would not match any more.

[Sebastien Gouezel]

3) Performancewise, we would be adding data fields to a lot of structures we use all the time in mathlib, so how bad would it be?

[Sebastien Gouezel]

4) This seems directly related to the issue of numerics in Lean 4. With the above design, we should probably essentially never use any more int.cast, and replace it with the field in the add_comm_group structure applied to 1, or something like that. If we do such a refactor, we'd better plan it to be compatible with the implementation of numerics we want in Lean 4 (which I haven't really followed). @Mario Carneiro, do you have thoughts about this?

[Sebastien Gouezel]

This would mean ditching my branch branch#gsmul_instance, but I don't care, this seems like a much better solution. I'm done with my rant, and I'm going to the sea because it's our last day of freedom before yet another lockdown, but I'll be happy to read what you think of it when I'm back this evening :-)

[Mario Carneiro]

The idea for numerics in lean 4 was to add a field ofNat to the base structures like semiring. From such a structure you get a natural interpretation of nsmul, although not gsmul (unless we extend the field to ofInt)

[Mario Carneiro]

That is, nat.cast would become a projection

[Mario Carneiro]

That's not quite the same as what you are proposing, which is to add n * x as a field of the structure. Perhaps we want both?

[Mario Carneiro]

Well at least on semirings there is a natural definition of n * x as ofNat n * x

[Johan Commelin]

Right, but we also need something that works for groups

[Eric Wieser]

What's the advantage of adding fields to add_comm_group here, vs just remembering to add a few explicit nat_semimodule instances?

[Eric Wieser]

I suspect we would actually need very few

[Eric Wieser]

There don't seem to be many "primitive" types, my impression is that most are compound types like linear_map which inherit the module structure

[Eric Wieser]

Ah, the argument is it combines [add_comm_monoid A] [semimodule nat A] into a single parameter

[Johan Commelin]

Not the same, but related, I think:

import data.polynomial.algebra_map

noncomputable theory

variables {R A : Type*} [comm_ring R] [comm_ring A] [algebra R A]

example : algebra R (polynomial R) := polynomial.algebra_of_algebra

-- it seems that this is not yet in mathlib
instance polynomial.map_algebra : algebra (polynomial R) (polynomial A) :=
(polynomial.map_ring_hom (algebra_map R A)).to_algebra

lemma «problem?» :
  @eq (algebra (polynomial R) (polynomial (polynomial R)))
  polynomial.algebra_of_algebra
  polynomial.map_algebra
  :=
rfl -- fails

[Kevin Buzzard]

Why stop at add_comm_group? Why not register some kind of action of nat on all monoids and add_monoids, and an action of int on all groups and add_groups? We have this already, it's just monoid.pow etc. The axiom $(gh)^n=g^nh^n$ doesn't hold in general but we could just throw this in later with the commutativity assumptions. We could at the same time try to solve the problem that to_additive can't handle power stuff because the order of the inputs is wrong, by making g^n mean n bub g.

Would this mean that we would not have to persuade Leo to change the definition of natural multiplication in Lean 4 or is that another thing?

[Eric Wieser]

@Johan Commelin, are you convinced that statement is true?

import data.polynomial.algebra_map

noncomputable theory

variables {R A : Type*} [comm_ring R] [comm_ring A] [algebra R A]

example : algebra R (polynomial R) := polynomial.algebra_of_algebra

-- it seems that this is not yet in mathlib
instance polynomial.map_algebra : algebra (polynomial R) (polynomial A) :=
(polynomial.map_ring_hom (algebra_map R A)).to_algebra

lemma map_algebra_smul (pr : polynomial R) (pa : polynomial A) :
  pr • pa = polynomial.map_ring_hom (algebra_map R A) pr * pa := rfl

lemma algebra_of_algebra_smul (r : R) (pa : polynomial A) :
  r • pa = finsupp.map_range (λ x, r • x) (smul_zero _) pa := rfl

lemma «problem?» :
  @eq (algebra (polynomial R) (polynomial (polynomial R)))
  polynomial.algebra_of_algebra
  polynomial.map_algebra
  :=
begin
  ext1,
  rw [map_algebra_smul, algebra_of_algebra_smul],
  simp,
  sorry,
end

[Eric Wieser]

#7019 adds a lemma that might make that sorry easier to prove, as then we can write

@[simp]
lemma polynomial.map_algebra_self_algebra_map :
  (algebra_map (polynomial R) (polynomial R)) = ring_hom.id _ := polynomial.map_ring_hom_id

[Sebastien Gouezel]

I've started looking at this. There is something that is a mystery for me, maybe it will look obvious to some of you. Suppose that I have changed the definition of comm_monoid to add a field with data. As follows:

import algebra.group.inj_surj

set_option old_structure_cmd true

universe u

/-- The power operation in a monoid. `a^n = a*a*...*a` n times. -/
def monoid.pow_rec (M : Type u) [has_mul M] [has_one M] : ℕ → M → M
| 0     a := 1
| (n+1) a := a * monoid.pow_rec n a

@[ancestor monoid comm_semigroup]
class my_comm_monoid (M : Type u) extends monoid M, comm_semigroup M :=
(nspow : ℕ → M → M := monoid.pow_rec M)
(nspow_add' : ∀ (n m : ℕ) (x : M), nspow (m + n) x = nspow m x * nspow n x)

I will want to fill the last field with a tactic to do it automatically, but before that let's do by hand the first breaking example, in inj_surj.lean.

protected def my_comm_monoid_of_injective {M₁ : Type*} {M₂ : Type*}
  [has_mul M₁] [has_one M₁] [comm_monoid M₂] (f : M₁ → M₂) (hf : function.injective f)
  (one : f 1 = 1) (mul : ∀ x y, f (x * y) = f x * f y) :
  my_comm_monoid M₁ :=
{ nspow_add' := begin
  assume n m a,
    induction n with n ih,
    { rw [nat.add_zero, monoid.pow_rec, mul_one] },
    { rw [nat.add_succ, monoid.pow_rec, ih, monoid.pow_rec, ← mul_assoc, ← mul_assoc],
      rw mul_comm a _ } -- fails
  end
  .. hf.comm_semigroup f mul, .. hf.monoid f one mul }

Here, the rw mul_one in the first step of the induction succeeds, which means it is able to somehow find the mul_one_class instance, which is probably coming from the last line with .. hf.monoid f one mul, .. hf.comm_semigroup f mul. Then, in the second step of the induction, it can rewrite mul_assoc, so it finds the semigroup instance. Unfortunately, the rw mul_comm a _ fails, which means it doesn't find the comm_semigroup instance, which should follow from the same line.

Do you understand what is going on, and if there is a generic enough fix?

[Johan Commelin]

Unrelated to the above: but if this refactor means that add_monoid_hom will be defeq (for groups?) to Z-linear module homs, that would would be insanely cool.

[Johan Commelin]

@Sebastien Gouezel Can you prove the pow_add lemma for monoid.pow_rec in a separate lemma? Does that help at the location of the error?

[Sebastien Gouezel]

Yes, I can prove it, and the proof I have given works fine. The question here is really about which instances are available when doing proofs inside fields of a structure.

[Eric Wieser]

How does the proposed nsmul field end up mapped to an has_scalar instance?

[Sebastien Gouezel]

Later on, we will declare a has_scalar ℕ M instance on all add_comm_groups using this field. But for now, I am only starting with the simplest stuff, i.e., adding the fields, making sure that they are populated when creating the structure, but not using them yet. If I can't do this properly, I won't be able to go any further.

[Sebastien Gouezel]

A good joke in my mwe: if instead of the automatically populated field nspow you fill it by hand, then you get an error at a different place:

protected def my_comm_monoid_of_injective {M₁ : Type*} {M₂ : Type*}
  [has_mul M₁] [has_one M₁] [comm_monoid M₂] (f : M₁ → M₂) (hf : function.injective f)
  (one : f 1 = 1) (mul : ∀ x y, f (x * y) = f x * f y) :
  my_comm_monoid M₁ :=
{ nspow := monoid.pow_rec M₁,
  nspow_add' := begin
  assume n m a,
    induction n with n ih,
    { rw [nat.add_zero, monoid.pow_rec, mul_one] }, -- already fails
    { rw [nat.add_succ, monoid.pow_rec, ih, monoid.pow_rec, ← mul_assoc, ← mul_assoc],
      rw mul_comm a _ }
  end,
  .. hf.comm_semigroup f mul, .. hf.monoid f one mul }

Really weird...

[Eric Wieser]

The idea here is that, for example, prod.add_comm_group.nsmul would be designed such that it's defeq to prod.has_scalar.smul?

[Sebastien Gouezel]

Yes, exactly. Just like it's done for metric spaces and uniform spaces.

[Sebastien Gouezel]

A workaround to my problem is to change my prop field, using instead nspow_eq_rec : ∀ (n : ℕ) (x : M), nspow n x = monoid.pow_rec n x, which can be proved by rfl when using the default field, so no need to activate other classes. This solves my issue (though it will need some tweaks down the road with alternate constructors, but nothing bad), but still I'd be interested to understand what is going on here.

[Kevin Buzzard]

protected def my_comm_monoid_of_injective {M₁ : Type*} {M₂ : Type*}
  [has_mul M₁] [has_one M₁] [comm_monoid M₂] (f : M₁ → M₂) (hf : function.injective f)
  (one : f 1 = 1) (mul : ∀ x y, f (x * y) = f x * f y) :
  my_comm_monoid M₁ :=
{ nspow_add' := begin
    letI : comm_semigroup M₁ := hf.comm_semigroup f mul,
    letI : monoid M₁ := hf.monoid f one mul,
  assume n m a,
    induction n with n ih,
    { rw [nat.add_zero, monoid.pow_rec],
      symmetry,
      -- monoid.pow_rec M₁ m a * 1 = monoid.pow_rec M₁ m a
      exact mul_one (monoid.pow_rec M₁ m a) }, -- fails <---------------------------------------------------------------------
    { rw [nat.add_succ, monoid.pow_rec, ih, monoid.pow_rec, ← mul_assoc, ← mul_assoc],
      rw mul_comm a _ } -- fails
  end
  .. hf.comm_semigroup f mul, .. hf.monoid f one mul }

gives

unexpected argument at application
  @mul_one M₁ _inst_4 (@monoid.pow_rec M₁ _inst_1 _inst_2 m a)
given argument
  @monoid.pow_rec M₁ _inst_1 _inst_2 m a
expected argument
  @monoid.pow_rec M₁
    (@semigroup.to_has_mul M₁
       (@monoid.to_semigroup M₁
          (@monoid.mk M₁
             (@comm_semigroup.mul M₁
                (@function.injective.comm_semigroup M₁ M₂ _inst_1 (@comm_monoid.to_comm_semigroup M₂ _inst_3) f hf
                   mul))
             _
             (@monoid.one M₁
                (@function.injective.monoid M₁ M₂ _inst_1 _inst_2 (@comm_monoid.to_monoid M₂ _inst_3) f hf one
                   mul))
             _
             _)))
    (@monoid.to_has_one M₁
       (@monoid.mk M₁
          (@comm_semigroup.mul M₁
             (@function.injective.comm_semigroup M₁ M₂ _inst_1 (@comm_monoid.to_comm_semigroup M₂ _inst_3) f hf
                mul))
          _
          (@monoid.one M₁
             (@function.injective.monoid M₁ M₂ _inst_1 _inst_2 (@comm_monoid.to_monoid M₂ _inst_3) f hf one mul))
          _
          _))
    m
    a

[Kevin Buzzard]

Aah, convert instead of exact gives the goals ⊢ semigroup.to_has_mul M₁ = _inst_1 and ⊢ monoid.to_has_one M₁ = _inst_2. So this is probably your problem: you have two non-defeq muls on M_1, one coming from the [has_mul M_1] and one coming from pulling back multiplication on M_2 and your mul axiom is not definitional (and similarly you have non-definitional 1s).

[Kevin Buzzard]

OK so this is beyond my pay grade. If we look at the code you originally posted, as you say the rw mul_one in the first step of the induction succeeds. For the rewrite to succeed, Lean must be inferring an instance of monoid M1 somehow, and you would imagine that the type class inference system is doing this, but it is not! Indeed letI : monoid M₁ := by apply_instance, on the line before fails! So Lean is doing some kind of magic which happens when creating structures where it looks at the .. stuff but this is somehow not in the type class inference cache at the point where I am trying to infer an instance?

protected def my_comm_monoid_of_injective {M₁ : Type*} {M₂ : Type*}
  [has_mul M₁] [has_one M₁] [comm_monoid M₂] (f : M₁ → M₂) (hf : function.injective f)
  (one : f 1 = 1) (mul : ∀ x y, f (x * y) = f x * f y) :
  my_comm_monoid M₁ :=
{ nspow_add' := begin
  assume n m a,
    induction n with n ih,
    { rw [nat.add_zero, monoid.pow_rec],
      -- ⊢ monoid.pow_rec M₁ m a = monoid.pow_rec M₁ m a * 1
      -- letI : monoid M₁ := by apply_instance, -- this FAILS
      -- and the next line will only work if Lean can find a monoid structure on M₁
      rw mul_one, -- but it works anyway!
     },
...

[Kevin Buzzard]

(deleted)

[Kevin Buzzard]

(deleted)

[Kevin Buzzard]

This works:

protected def my_comm_monoid_of_injective {M₁ : Type*} {M₂ : Type*}
  [has_mul M₁] [has_one M₁] [comm_monoid M₂] (f : M₁ → M₂) (hf : function.injective f)
  (one : f 1 = 1) (mul : ∀ x y, f (x * y) = f x * f y) :
  my_comm_monoid M₁ :=
{ nspow_add' := begin
  assume n m a,
    letI : comm_semigroup M₁ := hf.comm_semigroup f mul,
    induction n with n ih,
    { rw [nat.add_zero, monoid.pow_rec, mul_one] },
    { rw [nat.add_succ, monoid.pow_rec, ih, monoid.pow_rec, ← mul_assoc, ← mul_assoc],
      rw mul_comm a _ }
  end,
  .. hf.comm_semigroup f mul, .. hf.monoid f one mul }

[Mario Carneiro]

Isn't the axiomatization of nspow incomplete? It's not possible to prove nspow 0 x = 1

[Mario Carneiro]

(you can prove it is idempotent but I don't think that's good enough to conclude it is 1 in a monoid)

[Mario Carneiro]

protected def my_comm_monoid_of_injective {M₁ : Type*} {M₂ : Type*}
  [has_mul M₁] [has_one M₁] [my_comm_monoid M₂]
  (f : M₁ → M₂) (hf : function.injective f)
  (one : f 1 = 1) (mul : ∀ x y, f (x * y) = f x * f y)
  (nspow₁ : ℕ → M₁ → M₁ := monoid.pow_rec M₁)
  (nsm : ∀ n x, f (nspow₁ n x) = my_comm_monoid.nspow n (f x)) :
  my_comm_monoid M₁ :=
{ nspow := nspow₁,
  nspow_add' := λ n m x, begin
    change nspow₁ (m + n) x = nspow₁ m x * nspow₁ n x,
    apply hf,
    rw [nsm, mul, nsm, nsm, my_comm_monoid.nspow_add'],
  end,
  .. hf.comm_semigroup f mul, .. hf.monoid f one mul }

[Mario Carneiro]

or

@[ancestor monoid comm_semigroup]
class my_comm_monoid (M : Type u) extends monoid M, comm_semigroup M :=
(nspow : ℕ → M → M := monoid.pow_rec M)
(nspow_eq' : nspow = monoid.pow_rec M . control_laws_tac)

protected def my_comm_monoid_of_injective {M₁ : Type*} {M₂ : Type*}
  [has_mul M₁] [has_one M₁] [my_comm_monoid M₂]
  (f : M₁ → M₂) (hf : function.injective f)
  (one : f 1 = 1) (mul : ∀ x y, f (x * y) = f x * f y)
  (nspow : ℕ → M₁ → M₁ := monoid.pow_rec M₁)
  (nsm : ∀ n x, f (nspow n x) = my_comm_monoid.nspow n (f x)) :
  my_comm_monoid M₁ :=
{ nspow := nspow,
  nspow_eq' := begin
    funext n x,
    apply hf,
    rw [nsm, show _=_, from my_comm_monoid.nspow_eq'],
    induction n,
    { exact one.symm },
    { rw [monoid.pow_rec, n_ih, ← mul], refl }
  end,
  .. hf.comm_semigroup f mul, .. hf.monoid f one mul }

[Sebastien Gouezel]

Mario Carneiro said:

Isn't the axiomatization of nspow incomplete? It's not possible to prove nspow 0 x = 1

Sure, it was just for the mwe but I also have the other axioms in my files.

[Sebastien Gouezel]

Mario and Kevin, your solutions work, but they are specific to the problem at hand. My goal was really to do the following: endow a type with the power monoid.pow_rec (not another one) and prove with a universal tactic block that it satisfies the axioms, so that this tactic block can be used in all situations and then automated. The pullback comm_monoid was just an example of a situation where my universal tactic block, which most often works, failed because of Lean not finding the right instance. I can absolutely do it by hand or by modifying the definition like you did, but I was looking for a more principled solution which would always work automatically. Anyway, the solution to change the axioms by requiring instead equality with monoid.pow_rec works (the automatic proof is just by rfl and always works), so I'll go this route.

[Mario Carneiro]

I would suggest avoiding a full tactic block in an auto param unless you actually need to do something tactic-like such as inspecting the kind of definition that the user gave. If it's just a theorem parametric on values provided by the user then you should prove a lemma and the auto_param tactic should be essentially apply my_lemma

[Sebastien Gouezel]

That's what I did first, but the my_lemma needs some typeclasses that are not found, for the same reason as in my #mwe (that I minimized by removing the lemma and the tactic to get to the heart of the issue).

[Mario Carneiro]

you may have to supply the typeclasses manually, since as kevin observed there is a bit of magic to construct the typeclass argument for extends structures inside a structure literal

[Sebastien Gouezel]

Yes, my question was precisely about this magic bit, and if I could make it even a little bit more magical to just work in all situations :-)

[Mario Carneiro]

The fix in the tactic example is to add letI := hf.comm_semigroup f mul but I think I'm missing the actual question

[Mario Carneiro]

The tactic state inside structure fields is a bit of a mess since there are a bunch of typeclasses inside things like has_mul.mul that aren't actually in the context, so some theorems will work by unification and others will fail because the typeclass isn't available

[Sebastien Gouezel]

The actual question is "is there a way to not need a fix"?

[Mario Carneiro]

Well there's an error in the provided tactic block, so no?

[Sebastien Gouezel]

And I suspect the answer is no.

[Mario Carneiro]

of course the tactic block or statement has to change to make it work

[Mario Carneiro]

but this seems like a tautology

[Sebastien Gouezel]

Or maybe the question is "is there a way to fix Lean to not need a fix in this kind of situation"?

[Sebastien Gouezel]

Or "is there a magic instruction I could add in my tactic block to infer the instances I need from the .. line"?

[Sebastien Gouezel]

(Without adding it by hand, because by hand it would depend on the specific situation and I want a fix that always works)

[Mario Carneiro]

Well part of the issue is that this uses old_structure_cmd. When you use { .. hf.comm_semigroup f mul }, it has to splat out the projections into the structure, so it's not like letI : comm_semigroup M₁ := hf.comm_semigroup f mul was actually added to the context. If you had comm_semigroup M₁ available to the typeclass system, then in the new structure command it would pick that instance up since it would be a typeclass argument to my_comm_monoid.mk. With the old structure command it can't be, it is splatted out into fields, so you have to specify it in both places

[Mario Carneiro]

One way to write it without repetition is

begin
  letI := hf.comm_semigroup f mul,
  refine { nspow_add' := begin
    assume n m a,
      induction n with n ih,
      { rw [nat.add_zero, monoid.pow_rec, mul_one] },
      { rw [nat.add_succ, monoid.pow_rec, ih, monoid.pow_rec, ← mul_assoc, ← mul_assoc],
        rw mul_comm a _ }
    end
    .. (by apply_instance : comm_semigroup M₁),
    .. hf.monoid f one mul }
end

but that's not exactly shorter

[Sebastien Gouezel]

The mystery to me is that it finds some instances, like mul_one_class. And it doesn't find the same ones if the nspow field is populated by hand or with the tactic.

[Mario Carneiro]

are you sure it found mul_one_class? It probably just got it by unification

[Sebastien Gouezel]

You can try the example in https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/branch.23gsmul_instance/near/233026073

[Sebastien Gouezel]

(and then try it again by filling the nspow field by hand instead of with the automatic block, to see the difference).

[Eric Wieser]

What's the goal state at the failing mul_comm?

[Mario Carneiro]

Indeed, if you provide nspow := monoid.pow_rec M₁ (that is, @monoid.pow_rec M₁ _inst_1 _inst_2), then at the failing mul_one application the goal is

_ = has_mul.mul M₁ (mul_one_class.to_has_mul M₁) _ (has_one.one M₁ _inst_2)

and if you don't provide it and let it fill in automatically monoid.pow_rec M₁ (that is, @monoid.pow_rec M₁ (mul_one_class.to_has_mul M₁) (mul_one_class.to_has_one M₁)), then the goal is

_ = has_mul.mul M₁ (mul_one_class.to_has_mul M₁) _ (has_one.one M₁ (mul_one_class.to_has_one M₁))

and so mul_one_class.mul_one actually matches by unification, not by typeclass inference.

[Sebastien Gouezel]

Ah, thanks for explaining the mystery! I am still wondering why filling it with the tactic block uses has_mul.mul M₁ (mul_one_class.to_has_mul M₁) _ (has_one.one M₁ (mul_one_class.to_has_one M₁)), and especially where the tactic block is finding this mul_one_class instance.

[Mario Carneiro]

You might wonder why the automatic instantiation of nspow has mul_one_class all over it, and that's because of a trick that lean uses while elaborating the monoid.pow_rec M in the opt_param inside the structure definition of my_comm_monoid. The context at that point doesn't actually have a monoid instance in it, it has a bunch of fields, but lean will actually add the equivalent of letI := <mul, one, mul_one, one_mul> to typeclass inference (it's not actually using letI since this is part of core lean) in order to elaborate it, so you end up with these explicit monoid.mk things inside typeclass args

[Sebastien Gouezel]

ok, thanks a lot!

[Mario Carneiro]

if you replace the field with (nspow : ℕ → M → M := by show_term {exact monoid.pow_rec M}) with pp.all you will see that it is actually

(@monoid.pow_rec M₁
            (@mul_one_class.to_has_mul M₁
               (@monoid.to_mul_one_class M₁
                  (@monoid.mk M₁
...

[Sebastien Gouezel]

Does it mean that if I defined my pow_rec to also take an instance [comm_semi_group G], then core Lean would also find it and add it here, and then it would be available by unification in the tactic block proof?

[Mario Carneiro]

Unfortunately, you are pretty limited when it comes to using unification to find things, because that depends on the actual sequence of things in the hierarchy of typeclasses leading to the projections that were used

[Mario Carneiro]

you just got lucky here with mul_one_class, most instances can't be found this way

[Mario Carneiro]

If there are any defeq diamonds like A -> B -> D and A -> C -> D and typeclass inference finds the first path (in a context where you have A and need D), then theorems about B will trigger but not theorems about C

[Sebastien Gouezel]

Just to summarize the discussion: there is a magical tactic "pull an instance out of thin air" that is used by Lean core C++ when filling in opt_param fields of structures. Unfortunately, it is not accessible to mere mortal users. Thanks Mario for the explanations!