Zulip Chat Archive

Stream: general

Topic: branch#gsmul_instance


view this post on Zulip 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

view this post on Zulip Johan Commelin (Apr 03 2021 at 06:42):

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

view this post on Zulip Damiano Testa (Apr 03 2021 at 06:44):

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

view this post on Zulip Johan Commelin (Apr 03 2021 at 06:49):

I think we need it on every abelian group.

view this post on Zulip Sebastien Gouezel (Apr 03 2021 at 07:10):

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

view this post on Zulip Johan Commelin (Apr 03 2021 at 07:12):

But you want to disable algebra_int, right?

view this post on Zulip 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\Z again?

view this post on Zulip Sebastien Gouezel (Apr 03 2021 at 07:13):

The problem: we want every add_comm_group to be a Z\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.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Apr 03 2021 at 07:18):

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

view this post on Zulip Johan Commelin (Apr 03 2021 at 07:18):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Apr 03 2021 at 07:23):

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

view this post on Zulip Johan Commelin (Apr 03 2021 at 07:23):

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

view this post on Zulip Sebastien Gouezel (Apr 03 2021 at 07:23):

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

view this post on Zulip Sebastien Gouezel (Apr 03 2021 at 07:23):

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

view this post on Zulip 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.

view this post on Zulip Sebastien Gouezel (Apr 03 2021 at 07:24):

I have a few questions abouth this idea:

view this post on Zulip 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

view this post on Zulip Johan Commelin (Apr 03 2021 at 07:25):

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

view this post on Zulip 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).

view this post on Zulip Johan Commelin (Apr 03 2021 at 07:25):

One from :up: and another from algebra.id

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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 :-)

view this post on Zulip 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)

view this post on Zulip Mario Carneiro (Apr 03 2021 at 07:41):

That is, nat.cast would become a projection

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Johan Commelin (Apr 03 2021 at 07:48):

Right, but we also need something that works for groups

view this post on Zulip 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?

view this post on Zulip Eric Wieser (Apr 03 2021 at 07:53):

I suspect we would actually need very few

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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=gnhn(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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Eric Wieser (Apr 03 2021 at 19:25):

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

view this post on Zulip Sebastien Gouezel (Apr 03 2021 at 19:29):

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.

view this post on Zulip 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...

view this post on Zulip 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?

view this post on Zulip Sebastien Gouezel (Apr 03 2021 at 19:51):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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 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).

view this post on Zulip 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!
     },
...

view this post on Zulip Kevin Buzzard (Apr 03 2021 at 22:33):

(deleted)

view this post on Zulip Kevin Buzzard (Apr 03 2021 at 22:49):

(deleted)

view this post on Zulip 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 }

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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 }

view this post on Zulip 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 }

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip 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 :-)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Sebastien Gouezel (Apr 04 2021 at 07:37):

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

view this post on Zulip Mario Carneiro (Apr 04 2021 at 07:37):

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

view this post on Zulip Sebastien Gouezel (Apr 04 2021 at 07:37):

And I suspect the answer is no.

view this post on Zulip Mario Carneiro (Apr 04 2021 at 07:37):

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

view this post on Zulip Mario Carneiro (Apr 04 2021 at 07:38):

but this seems like a tautology

view this post on Zulip 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"?

view this post on Zulip 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"?

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Apr 04 2021 at 07:47):

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

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip Eric Wieser (Apr 04 2021 at 07:52):

What's the goal state at the failing mul_comm?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Sebastien Gouezel (Apr 04 2021 at 08:04):

ok, thanks a lot!

view this post on Zulip 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₁
...

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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