# Zulip Chat Archive

## Stream: general

### Topic: branch#gsmul_instance

#### Johan Commelin (Apr 03 2021 at 06:31):

@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 (Apr 03 2021 at 06:42):

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

#### Damiano Testa (Apr 03 2021 at 06:44):

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

#### Johan Commelin (Apr 03 2021 at 06:49):

I think we need it on every abelian group.

#### Sebastien Gouezel (Apr 03 2021 at 07:10):

I had a crazy idea that should fix all the diamond issues while keeping the $\Z$-module instance on `add_comm_group`

s. I'd like to hear your thoughts about it.

#### Johan Commelin (Apr 03 2021 at 07:12):

But you want to disable `algebra_int`

, right?

#### Johan Commelin (Apr 03 2021 at 07:13):

If you keep `add_comm_group.int_module`

, how can we make sure that we don't hit diamonds on $\Z$ again?

#### Sebastien Gouezel (Apr 03 2021 at 07:13):

*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_group`

s 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 (Apr 03 2021 at 07:16):

*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 (Apr 03 2021 at 07:18):

But then we can do the same thing with `comm_ring`

and `algebra_int`

, right?

#### Johan Commelin (Apr 03 2021 at 07:18):

So we should remove that `algebra int (zmod n)`

instances again?

#### Sebastien Gouezel (Apr 03 2021 at 07:19):

*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 (Apr 03 2021 at 07:22):

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 (Apr 03 2021 at 07:22):

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 (Apr 03 2021 at 07:23):

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

#### Johan Commelin (Apr 03 2021 at 07:23):

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

and `add_comm_monoid`

#### Sebastien Gouezel (Apr 03 2021 at 07:23):

And we should also do the same for `nat`

and `add_comm_monoid`

, yes.

#### Sebastien Gouezel (Apr 03 2021 at 07:23):

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

#### Sebastien Gouezel (Apr 03 2021 at 07:24):

But this `ℤ`

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

#### Sebastien Gouezel (Apr 03 2021 at 07:24):

I have a few questions abouth this idea:

#### Johan Commelin (Apr 03 2021 at 07:25):

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 (Apr 03 2021 at 07:25):

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

#### Sebastien Gouezel (Apr 03 2021 at 07:25):

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 (Apr 03 2021 at 07:25):

One from :up: and another from `algebra.id`

#### Sebastien Gouezel (Apr 03 2021 at 07:27):

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 (Apr 03 2021 at 07:28):

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 (Apr 03 2021 at 07:30):

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 (Apr 03 2021 at 07:32):

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 (Apr 03 2021 at 07:41):

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 (Apr 03 2021 at 07:41):

That is, `nat.cast`

would become a projection

#### Mario Carneiro (Apr 03 2021 at 07:43):

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 (Apr 03 2021 at 07:44):

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

as `ofNat n * x`

#### Johan Commelin (Apr 03 2021 at 07:48):

Right, but we also need something that works for groups

#### Eric Wieser (Apr 03 2021 at 07:53):

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 (Apr 03 2021 at 07:53):

I suspect we would actually need very few

#### Eric Wieser (Apr 03 2021 at 07:54):

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 (Apr 03 2021 at 08:27):

Ah, the argument is it combines `[add_comm_monoid A] [semimodule nat A]`

into a single parameter

#### Johan Commelin (Apr 03 2021 at 09:07):

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 (Apr 03 2021 at 09:27):

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 (Apr 03 2021 at 10:52):

@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 (Apr 03 2021 at 11:19):

#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 (Apr 03 2021 at 19:12):

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 (Apr 03 2021 at 19:15):

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 (Apr 03 2021 at 19:16):

@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 (Apr 03 2021 at 19:17):

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 (Apr 03 2021 at 19:25):

How does the proposed `nsmul`

field end up mapped to an `has_scalar`

instance?

#### Sebastien Gouezel (Apr 03 2021 at 19:29):

Later on, we will declare a `has_scalar ℕ M`

instance on all `add_comm_group`

s 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 (Apr 03 2021 at 19:35):

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 (Apr 03 2021 at 19:49):

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 (Apr 03 2021 at 19:51):

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

#### Sebastien Gouezel (Apr 03 2021 at 20:14):

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 (Apr 03 2021 at 22:04):

```
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 (Apr 03 2021 at 22:12):

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 `mul`

s 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 (Apr 03 2021 at 22:28):

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 (Apr 03 2021 at 22:33):

(deleted)

#### Kevin Buzzard (Apr 03 2021 at 22:49):

(deleted)

#### Kevin Buzzard (Apr 03 2021 at 22:56):

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 (Apr 03 2021 at 22:58):

Isn't the axiomatization of `nspow`

incomplete? It's not possible to prove `nspow 0 x = 1`

#### Mario Carneiro (Apr 03 2021 at 22:59):

(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 (Apr 03 2021 at 23:05):

```
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 (Apr 03 2021 at 23:14):

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 (Apr 04 2021 at 07:05):

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 (Apr 04 2021 at 07:11):

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 (Apr 04 2021 at 07:17):

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 (Apr 04 2021 at 07:25):

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 (Apr 04 2021 at 07:31):

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 (Apr 04 2021 at 07:34):

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 (Apr 04 2021 at 07:35):

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 (Apr 04 2021 at 07:36):

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 (Apr 04 2021 at 07:37):

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

#### Mario Carneiro (Apr 04 2021 at 07:37):

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

#### Sebastien Gouezel (Apr 04 2021 at 07:37):

And I suspect the answer is no.

#### Mario Carneiro (Apr 04 2021 at 07:37):

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

#### Mario Carneiro (Apr 04 2021 at 07:38):

but this seems like a tautology

#### Sebastien Gouezel (Apr 04 2021 at 07:38):

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

#### Sebastien Gouezel (Apr 04 2021 at 07:39):

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

line"?

#### Sebastien Gouezel (Apr 04 2021 at 07:40):

(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 (Apr 04 2021 at 07:43):

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 (Apr 04 2021 at 07:44):

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 (Apr 04 2021 at 07:45):

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 (Apr 04 2021 at 07:47):

are you sure it found `mul_one_class`

? It probably just got it by unification

#### Sebastien Gouezel (Apr 04 2021 at 07:48):

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

#### Sebastien Gouezel (Apr 04 2021 at 07:50):

(and then try it again by filling the `nspow`

field by hand instead of with the automatic block, to see the difference).

#### Eric Wieser (Apr 04 2021 at 07:52):

What's the goal state at the failing mul_comm?

#### Mario Carneiro (Apr 04 2021 at 07:59):

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 (Apr 04 2021 at 08:02):

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 (Apr 04 2021 at 08:03):

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 (Apr 04 2021 at 08:04):

ok, thanks a lot!

#### Mario Carneiro (Apr 04 2021 at 08:06):

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 (Apr 04 2021 at 08:06):

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 (Apr 04 2021 at 08:07):

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 (Apr 04 2021 at 08:08):

you just got lucky here with `mul_one_class`

, most instances can't be found this way

#### Mario Carneiro (Apr 04 2021 at 08:10):

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 (Apr 04 2021 at 09:01):

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!

Last updated: May 15 2021 at 23:13 UTC