p + q = p * q solves by refl!

Stream: general

[Eric Wieser]

Something seems wrong either with the pretty-printer or with type-class resolution here:

example {G : Type u} [add_monoid G] (p q : multiplicative G) :
  (p * q) = (@has_add.add (multiplicative G) (@add_semigroup.to_has_add G (add_monoid.to_add_semigroup G))
             p q) :=
begin
  /-
  p q : multiplicative G
  ⊢ p * q = p + q
  -/
  refl,
end

Obviously the RHS of my lemma is contrived, but it's what extract_goal produced mid-proof

[Eric Wieser]

This lets me make a rather strange (multiplicative G) ≃+ G object

import algebra.algebra.basic

def bad_add (G : Type) [add_monoid G] : has_add (multiplicative G) :=
(@add_semigroup.to_has_add (multiplicative G) (@add_monoid.to_add_semigroup (multiplicative G) _inst_1))

lemma bad_map_add {G : Type} [add_monoid G] (x y : multiplicative G) :
  by haveI := bad_add G; exact
    multiplicative.to_add x + multiplicative.to_add y = multiplicative.to_add (x + y) :=
rfl

def bad_to_add {G : Type} [add_monoid G] :
  by haveI := bad_add; exact
    (multiplicative G) ≃+ G :=
{add_equiv.
  map_add' := λ x y, by {simp only [equiv.to_fun_as_coe, bad_map_add x y]},
  ..@multiplicative.to_add G
}

#check bad_to_add

[Mario Carneiro]

This is expected behavior

[Eric Wieser]

Would bad_to_add make sense in mathlib then?

[Eric Wieser]

With a better name, obviously

[Mario Carneiro]

absolutely not

[Eric Wieser]

Perhaps some more context - I'm trying to implement add_monoid_algebra k G ≃+* monoid_algebra k (multiplicative G)

[Mario Carneiro]

it is pretty obviously not a desirable instance

[Mario Carneiro]

You can locally override instances, as you are doing in these examples

[Mario Carneiro]

but they cause problems down the line so you should keep it to a minimum

[Eric Wieser]

Sorry, I'm not suggesting bad_add should be a global instance

[Mario Carneiro]

I don't see how that equiv makes sense

[Mario Carneiro]

are those both rings?

[Eric Wieser]

Perhaps I need to show a longer example

[Mario Carneiro]

I'm pretty sure ≃+* works on rings and ringish things

[Eric Wieser]

Both add_monoid_algebra k G and monoid_algebra k (multiplicative G) are semirings, yes

[Eric Wieser]

I was able to prove this lemma:

lemma add_monoid_algebra.map_domain_mul {α : Type*} {β : Type*} {α₂ : Type*} [semiring β] [add_monoid α] [add_monoid α₂] {x y : add_monoid_algebra β α}
  {f : α → α₂} (f_map_mul : ∀ x y, f x + f y = f (x + y)):
  (map_domain f (x * y : add_monoid_algebra β α) : add_monoid_algebra β α₂) =
    (map_domain f x * map_domain f y : add_monoid_algebra β α₂) := sorry

and I can then use it to construct the ring isomorphism as

def add_monoid_algebra.to_multiplicative :
  add_monoid_algebra k G ≃+* monoid_algebra k (multiplicative G) :=
{ map_mul' := λ x y, by {
    unfold finsupp.dom_congr,
    simp,
    rw map_domain_mul _,
    extract_goal, -- this is where the weird goal appears
    intros p q,
    simp [← to_add_mul],
    refl, },
  map_add' := λ x y, by {
    simp [finsupp.dom_congr, map_domain_add],
  },
  ..finsupp.dom_congr multiplicative.to_add }

What I'd like to do is bundle fand f_map_mul into a α →+ α₂. The →+ object I need is exactly bad_to_add.

[Mario Carneiro]

I'm asking a more basic question, I think. What kind of object is monoid_algebra k (multiplicative G)? What operations does it support?

[Mario Carneiro]

Does it have an addition and multiplication, and do they make sense

[Eric Wieser]

Perhaps it helps to note that the implementation notes for add_monoid_algebra say

Similarly, I attempted to just define add_monoid_algebra k G := monoid_algebra k (multiplicative G),
but the definitional equality multiplicative G = G leaks through everywhere, and
seems impossible to use.

[Mario Carneiro]

well there you have it

[Eric Wieser]

Right - and IMO the thing that makes it impossible to use is the absence of add_monoid_algebra.to_multiplicative above

[Eric Wieser]

With that in place I can (hopefully) replace all the add_monoid_algebra theorems with

1. Apply the iso
2. use the proof for monoid_algebra

[Mario Carneiro]

the problem is the defeqs are wrong

[Eric Wieser]

The problem with what and which defeqs?

[Mario Carneiro]

The iso is trivial, I guess, because they are equal objects

[Mario Carneiro]

To fix the defeqs, the definition should be changed to something like

def add_monoid_algebra k G :=
{ add := something reasonable,
  mul := something reasonable,
  ..monoid_algebra k (multiplicative G) } -- use the unreasonable equalities to do the proof obligations

[Eric Wieser]

I don't quite get that example - today it's defined as def add_monoid_algebra := G →₀ k

[Mario Carneiro]

oh I see, it is not the definition

[Mario Carneiro]

and you want to recover that representation

[Chris Hughes]

The idiomatic way to use multiplicatuve is to use the to_add function, and others like it.

[Eric Wieser]

@Chris, which message is that in response to?

[Mario Carneiro]

somewhere in your definition is an "illegal" unfolding of multiplicative

[Mario Carneiro]

you could try making multiplicative irreducible to see if that pinpoints the issue, but I don't have your code to test

[Eric Wieser]

@Mario Carneiro, I think what you're recommending is already what I'm planning to do:

• Keep the definition of add_monoid_algebra
• Keep the definition of add_monoid_algebra.has_add
• Keep the definition of add_monoid_algebra.has_mul
• Transfer the ring structure of add_monoid_algebra over the isomorphism

[Mario Carneiro]

the question is whether the isomorphism itself is well typed

[Eric Wieser]

There are two isomorphism here - bad_add_to_add and monoid_algebra.to_additive

[Eric Wieser]

The former is obviously badly typed, IMO the latter is totally safe

[Eric Wieser]

But the former is a valuable tool for building the latter

[Mario Carneiro]

A ~=+* isomorphism comes with the assumption that both sides have reasonable addition/multiplication structures

[Eric Wieser]

Any to_additive def will inevitably perform an illegal unfolding of multiplicative

[Mario Carneiro]

yes, but you aren't doing such a def

[Mario Carneiro]

actually I take that back, to_additive does no unfolding

[Mario Carneiro]

to_additive does a copy paste job

[Mario Carneiro]

so there is no leakage

[Eric Wieser]

My claim is bad_add_to_add is a utility function to perform that unfolding / copy paste

[Mario Carneiro]

bad_add is aptly named, because multiplicative G isn't supposed to have an add

[Mario Carneiro]

and anything that contains bad_add in its statement is also bad

[Kevin Buzzard]

I had problems with leakage when using with_zero and I fixed it by making with_zero irreducible and approaching everything in a principled way, never using definitional equality apart from when I was setting up the API

[Eric Wieser]

The statement of bad_add_to_add is exactly an intermediate goal state in add_monoid_algebra.to_multiplicative (edited)

[Mario Carneiro]

which includes bad_add_to_add

[Mario Carneiro]

what to_additive are you talking about?

[Eric Wieser]

Ah, sorry - add_monoid_algebra.to_multiplicative

[Eric Wieser]

I meant that throughout

[Mario Carneiro]

I don't know what the statement of add_monoid_algebra.to_multiplicative is but it seems highly likely that some bad_add stuff is in there

[Eric Wieser]

I pasted it above

[Eric Wieser]

It's my proposed isomorphism

[Mario Carneiro]

I mean the full statement

[Eric Wieser]

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/p.20.2B.20q.20.3D.20p.20*.20q.20solves.20by.20refl!/near/212220659 is the full statement?

[Mario Carneiro]

I just don't understand how you can have a add_monoid_algebra on one side and a monoid_algebra on the other and they are the same type of object

[Kevin Buzzard]

There are maps from G to multiplicative G which could be used at all times. Does this solve the problems you have Eric? In my mind the fix for the leakage mentioned in the docs is to make multiplicative irreducible after the API has been set up

[Mario Carneiro]

There are implicit arguments

[Mario Carneiro]

and all the interesting stuff in this discussion is only visible if you look at the implicit arguments

[Kevin Buzzard]

An add_monoid_algebra and a monoid_algebra are just both semirings, they can be isomorphic

[Mario Carneiro]

aha

[Mario Carneiro]

so is it the finsupp lemmas then that are exposing the defeqs?

[Eric Wieser]

Perhaps the easiest way to see is:

• add_monoid_algebra: single a1 b1 * single a2 b2 = single (a1 + a2) (b2 * b2)
• monoid_algebra: single a1 b1 * single a2 b2 = single (a1 * a2) (b2 * b2)

[Eric Wieser]

So this is an obvious candidate for the type of map that Kevin is talking about - all I want to do is extend the existing maps to preserve additional structure

[Mario Carneiro]

Aha:

lemma add_monoid_algebra.map_domain_mul {α : Type*} {β : Type*} {α₂ : Type*} [semiring β] [add_monoid α] [add_monoid α₂] {x y : add_monoid_algebra β α}
  {f : α → α₂} (f_map_mul : ∀ x y, f x + f y = f (x + y)):
  (map_domain f (x * y : add_monoid_algebra β α) : add_monoid_algebra β α₂) =
    (map_domain f x * map_domain f y : add_monoid_algebra β α₂) := sorry

In your definition, the function f is multiplicative.to_add, so it should not be type correct for f_map_mul

[Kevin Buzzard]

I think that if you want to relate the two structures you could go further and define a group homomorphism between an add_group and a group, give it a nice notation, prove that this induces a morphism of semirings from add_monoid_alg and monoid_alg, do things the other way, prove that isomorphisms get sent to isomorphisms etc

[Kevin Buzzard]

We have spent two years running from the fact that we have two kinds of groups; usually it works fine because mathematicians use multiplication and addition in quite different ways, but with valuations I ran into problems because we didn't have eg any API for an infinite cyclic group. Valuations are both additive and multiplicative in the literature and lean's eccentric approach to keeping them separate has had advantages (eg the crystallisation of the monoid with 0 idea) but it also has disadvantages, and one we're seeing now is that it's difficult to pass from one world to the other.

[Kevin Buzzard]

But I think that one reason it's difficult is that nobody cared enough to write the API yet

[Kevin Buzzard]

I need an additive valuation on a multiplicative object to continue with discrete valuation rings and it's not there. Maybe it's time to put these things there? We've as yet seen no issues with people wanting to use ten different notations for groups and this idea not scaling.

[Kevin Buzzard]

I think that defining the structure which is a group hom from an additive to a multiplicative object and making a proper API would be the correct way to get the morphisms you want. Or are there other problems I've not foreseen?

[Eric Wieser]

We already have the group homs between additive and multiplicative objects - the case in question is dependent types D X and D (multiplicative Y), where the monoid on X is used internally by D X

[Eric Wieser]

Anyway, I've put the first lemma I need (finsupp.dom_add_congr) up as #4398.

I think that alone is enough to demonstrate the issue, without complicating things with monoid_algebra.

The simplified question is, given monoid α how do I construct the canonical isomorphism finsupp α β ≃+ finsupp (additive α) β? I can construct finsupp α β ≃ finsupp (additive α) β easily with finsupp.dom_congr, but I can't use finsupp.dom_add_congr without the "illegal" α ≃+ additive αobject discussed above.

[Eric Wieser]

Mario Carneiro said:

Aha: <snip>
In your definition, the function f is multiplicative.to_add, so it should not be type correct for f_map_mul

Right, so I just called rw on that definition, and lean created the nonsense goal for me automatically

[Reid Barton]

The moral is with these different instances on plain def B := A definitions, you really should avoid doing anything that would be ill-typed if B wasn't defeq to A. At some point, it becomes easier to just not have them be defeq in the first place.

[Eric Wieser]

I ended up not using bad_add_to_add, as I forgot that I did not need that f 0 = 0. #4402 still has the nonsense intermediate goal state that started this thread.

[Adam Topaz]

Does mathlib have something like a monoid morphism from a multiplicative monoid to an additive monoid (or vice versa)? If not, should we add it? We can call one a logarithmand the other an exponential.

[Adam Topaz]

(Oh, I now see Kevin's comments about this.)

[Reid Barton]

The combinatorial explosion of lemmas in all the variants sounds a bit scary, but maybe this is the logical conclusion of having add_monoid and monoid in the first place?

[Reid Barton]

Also, we can call to_add the "universal logarithm" on multiplicative α, which sounds very sophisticated.

[Reid Barton]

For notation: +→* for exponentials and *→+ for logarithms?

[Adam Topaz]

What about this approach:

import algebra

class has_binop (α : Type*) :=
(op : α → α → α)

class has_const (α : Type*) :=
(const : α)

structure widget (α β : Type*) [has_binop α] [has_binop β] [has_const α] [has_const β] :=
(to_fun : α → β)
(map_const : to_fun has_const.const = has_const.const)
(map_binop {x y : α} : to_fun (has_binop.op x y) = has_binop.op (to_fun x) (to_fun y))

instance add_to_op {α} [has_add α] : has_binop α := ⟨(+)⟩
instance zero_to_const {α} [has_zero α] : has_const α := ⟨0⟩
instance mul_to_op {α} [has_mul α] : has_binop α := ⟨(*)⟩
instance one_to_const {α} [has_one α] : has_const α := ⟨1⟩

variables {M N : Type*} [monoid M] [add_monoid N]
#check widget M N
#check widget N M

[Adam Topaz]

I guess this is a problem if M is a ring.

[Eric Wieser]

I was also wondering about the similar:

class base_monoid {T : Type} (identity : T) (op: T -> T -> T)
:=
(op_identity : ...) -- etc

abbreviation add_monoid = base_monoid 0 (+)

abbreviation monoid = base_monoid 1 (*)

[Adam Topaz]

@Eric Wieser check out how these things work in Agda. It's similar to what you suggest.

[Mario Carneiro]

In the interest of avoiding combinatorial explosions, to what extent can we get away with using G ->* multiplicative H for "logarithmic homs"?

[Adam Topaz]

I guess most things should work out if we define the the has_coe_to_fun correctly, no?

[Yury G. Kudryashov]

I think that we can't redefine has_coe_to_fun for this subcase.

[Adam Topaz]

You use a type alias

[Yury G. Kudryashov]

And loose lots of lemmas.

[Yury G. Kudryashov]

This is not better than adding a new type.

[Adam Topaz]

Yeah, you're right.

[Adam Topaz]

Is there some @[derive] magic that can be used?

[Mario Carneiro]

My suggestion is not to create a new type at all, just live with the fact that the codomain of the hom is multiplicative H and use multiplicative lemmas to convert the statements to things about addition in H

[Kevin Buzzard]

How about a new type formultiplicative int?

[Chris Hughes]

I've been using multiplicative int a lot lately. I just made notation for it. C∞ for the infinite cyclic group.

[Eric Wieser]

Eric Wieser said:

I was also wondering about the similar: <snip>

Turns out this is already discussed here: https://github.com/leanprover/lean/wiki/Refactoring-structures#encoding-the-algebraic-hierarchy-1