Zulip Chat Archive

Stream: general

Topic: p + q = p * q solves by refl!


view this post on Zulip Eric Wieser (Oct 04 2020 at 11:27):

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

view this post on Zulip Eric Wieser (Oct 04 2020 at 12:08):

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

view this post on Zulip Mario Carneiro (Oct 04 2020 at 12:09):

This is expected behavior

view this post on Zulip Eric Wieser (Oct 04 2020 at 12:10):

Would bad_to_add make sense in mathlib then?

view this post on Zulip Eric Wieser (Oct 04 2020 at 12:10):

With a better name, obviously

view this post on Zulip Mario Carneiro (Oct 04 2020 at 12:10):

absolutely not

view this post on Zulip Eric Wieser (Oct 04 2020 at 12:10):

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

view this post on Zulip Mario Carneiro (Oct 04 2020 at 12:10):

it is pretty obviously not a desirable instance

view this post on Zulip Mario Carneiro (Oct 04 2020 at 12:11):

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

view this post on Zulip Mario Carneiro (Oct 04 2020 at 12:11):

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

view this post on Zulip Eric Wieser (Oct 04 2020 at 12:11):

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

view this post on Zulip Mario Carneiro (Oct 04 2020 at 12:11):

I don't see how that equiv makes sense

view this post on Zulip Mario Carneiro (Oct 04 2020 at 12:12):

are those both rings?

view this post on Zulip Eric Wieser (Oct 04 2020 at 12:12):

Perhaps I need to show a longer example

view this post on Zulip Mario Carneiro (Oct 04 2020 at 12:12):

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

view this post on Zulip Eric Wieser (Oct 04 2020 at 12:13):

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

view this post on Zulip Eric Wieser (Oct 04 2020 at 12:15):

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.

view this post on Zulip Mario Carneiro (Oct 04 2020 at 12:18):

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

view this post on Zulip Mario Carneiro (Oct 04 2020 at 12:18):

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

view this post on Zulip Eric Wieser (Oct 04 2020 at 12:19):

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.

view this post on Zulip Mario Carneiro (Oct 04 2020 at 12:20):

well there you have it

view this post on Zulip Eric Wieser (Oct 04 2020 at 12:21):

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

view this post on Zulip Eric Wieser (Oct 04 2020 at 12:21):

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

view this post on Zulip Mario Carneiro (Oct 04 2020 at 12:21):

the problem is the defeqs are wrong

view this post on Zulip Eric Wieser (Oct 04 2020 at 12:22):

The problem with what and which defeqs?

view this post on Zulip Mario Carneiro (Oct 04 2020 at 12:22):

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

view this post on Zulip Mario Carneiro (Oct 04 2020 at 12:23):

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

view this post on Zulip Eric Wieser (Oct 04 2020 at 12:24):

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

view this post on Zulip Mario Carneiro (Oct 04 2020 at 12:25):

oh I see, it is not the definition

view this post on Zulip Mario Carneiro (Oct 04 2020 at 12:25):

and you want to recover that representation

view this post on Zulip Chris Hughes (Oct 04 2020 at 12:26):

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

view this post on Zulip Eric Wieser (Oct 04 2020 at 12:26):

@Chris, which message is that in response to?

view this post on Zulip Mario Carneiro (Oct 04 2020 at 12:27):

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

view this post on Zulip Mario Carneiro (Oct 04 2020 at 12:28):

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

view this post on Zulip Eric Wieser (Oct 04 2020 at 12:28):

@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

view this post on Zulip Mario Carneiro (Oct 04 2020 at 12:28):

the question is whether the isomorphism itself is well typed

view this post on Zulip Eric Wieser (Oct 04 2020 at 12:28):

There are two isomorphism here - bad_add_to_add and monoid_algebra.to_additive

view this post on Zulip Eric Wieser (Oct 04 2020 at 12:29):

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

view this post on Zulip Eric Wieser (Oct 04 2020 at 12:29):

But the former is a valuable tool for building the latter

view this post on Zulip Mario Carneiro (Oct 04 2020 at 12:29):

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

view this post on Zulip Eric Wieser (Oct 04 2020 at 12:30):

Any to_additive def will inevitably perform an illegal unfolding of multiplicative

view this post on Zulip Mario Carneiro (Oct 04 2020 at 12:30):

yes, but you aren't doing such a def

view this post on Zulip Mario Carneiro (Oct 04 2020 at 12:30):

actually I take that back, to_additive does no unfolding

view this post on Zulip Mario Carneiro (Oct 04 2020 at 12:31):

to_additive does a copy paste job

view this post on Zulip Mario Carneiro (Oct 04 2020 at 12:31):

so there is no leakage

view this post on Zulip Eric Wieser (Oct 04 2020 at 12:31):

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

view this post on Zulip Mario Carneiro (Oct 04 2020 at 12:31):

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

view this post on Zulip Mario Carneiro (Oct 04 2020 at 12:32):

and anything that contains bad_add in its statement is also bad

view this post on Zulip Kevin Buzzard (Oct 04 2020 at 12:33):

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

view this post on Zulip Eric Wieser (Oct 04 2020 at 12:33):

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

view this post on Zulip Mario Carneiro (Oct 04 2020 at 12:33):

which includes bad_add_to_add

view this post on Zulip Mario Carneiro (Oct 04 2020 at 12:33):

what to_additive are you talking about?

view this post on Zulip Eric Wieser (Oct 04 2020 at 12:33):

Ah, sorry - add_monoid_algebra.to_multiplicative

view this post on Zulip Eric Wieser (Oct 04 2020 at 12:34):

I meant that throughout

view this post on Zulip Mario Carneiro (Oct 04 2020 at 12:34):

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

view this post on Zulip Eric Wieser (Oct 04 2020 at 12:34):

I pasted it above

view this post on Zulip Eric Wieser (Oct 04 2020 at 12:35):

It's my proposed isomorphism

view this post on Zulip Mario Carneiro (Oct 04 2020 at 12:35):

I mean the full statement

view this post on Zulip Eric Wieser (Oct 04 2020 at 12:35):

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?

view this post on Zulip Mario Carneiro (Oct 04 2020 at 12:36):

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

view this post on Zulip Kevin Buzzard (Oct 04 2020 at 12:36):

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

view this post on Zulip Mario Carneiro (Oct 04 2020 at 12:36):

There are implicit arguments

view this post on Zulip Mario Carneiro (Oct 04 2020 at 12:36):

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

view this post on Zulip Kevin Buzzard (Oct 04 2020 at 12:36):

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

view this post on Zulip Mario Carneiro (Oct 04 2020 at 12:37):

aha

view this post on Zulip Mario Carneiro (Oct 04 2020 at 12:37):

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

view this post on Zulip Eric Wieser (Oct 04 2020 at 12:38):

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)

view this post on Zulip Eric Wieser (Oct 04 2020 at 12:38):

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

view this post on Zulip Mario Carneiro (Oct 04 2020 at 12:42):

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

view this post on Zulip Kevin Buzzard (Oct 04 2020 at 12:43):

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

view this post on Zulip Kevin Buzzard (Oct 04 2020 at 12:46):

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.

view this post on Zulip Kevin Buzzard (Oct 04 2020 at 12:47):

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

view this post on Zulip Kevin Buzzard (Oct 04 2020 at 12:48):

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.

view this post on Zulip Kevin Buzzard (Oct 04 2020 at 12:50):

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?

view this post on Zulip Eric Wieser (Oct 04 2020 at 12:59):

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

view this post on Zulip Eric Wieser (Oct 04 2020 at 13:10):

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.

view this post on Zulip Eric Wieser (Oct 04 2020 at 13:28):

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

view this post on Zulip Reid Barton (Oct 04 2020 at 14:15):

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.

view this post on Zulip Eric Wieser (Oct 04 2020 at 15:06):

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.

view this post on Zulip Adam Topaz (Oct 04 2020 at 16:23):

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.

view this post on Zulip Adam Topaz (Oct 04 2020 at 16:26):

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

view this post on Zulip Reid Barton (Oct 04 2020 at 16:46):

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?

view this post on Zulip Reid Barton (Oct 04 2020 at 16:47):

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

view this post on Zulip Reid Barton (Oct 04 2020 at 16:49):

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

view this post on Zulip Adam Topaz (Oct 04 2020 at 17:28):

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

view this post on Zulip Adam Topaz (Oct 04 2020 at 17:28):

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

view this post on Zulip Eric Wieser (Oct 04 2020 at 17:42):

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 (*)

view this post on Zulip Adam Topaz (Oct 04 2020 at 17:47):

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

view this post on Zulip Mario Carneiro (Oct 04 2020 at 23:32):

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

view this post on Zulip Adam Topaz (Oct 05 2020 at 00:33):

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

view this post on Zulip Yury G. Kudryashov (Oct 05 2020 at 01:06):

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

view this post on Zulip Adam Topaz (Oct 05 2020 at 01:09):

You use a type alias

view this post on Zulip Yury G. Kudryashov (Oct 05 2020 at 01:19):

And loose lots of lemmas.

view this post on Zulip Yury G. Kudryashov (Oct 05 2020 at 01:19):

This is not better than adding a new type.

view this post on Zulip Adam Topaz (Oct 05 2020 at 01:20):

Yeah, you're right.

view this post on Zulip Adam Topaz (Oct 05 2020 at 01:20):

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

view this post on Zulip Mario Carneiro (Oct 05 2020 at 01:22):

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

view this post on Zulip Kevin Buzzard (Oct 05 2020 at 06:09):

How about a new type formultiplicative int?

view this post on Zulip Chris Hughes (Oct 05 2020 at 06:41):

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

view this post on Zulip Eric Wieser (Oct 05 2020 at 15:16):

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


Last updated: May 11 2021 at 00:31 UTC