Zulip Chat Archive

Stream: maths

Topic: bundling mul_homs


view this post on Zulip Kevin Buzzard (Jul 18 2019 at 04:21):

Mathlib has the unbundled is_mul_hom class (a Prop), and then it has mul_equiv which references this unbundled is_mul_hom. If we were to bundle mul_homs, how would we define mul_equiv?

import data.equiv.basic algebra.group
import data.equiv.algebra

variables {α : Type*} {β : Type*} {γ : Type*}
[has_mul α] [has_mul β] [has_mul γ]
(M : Type*) (N : Type*) (P : Type*)
[has_mul M] [has_mul N] [has_mul P]

/- Mathlib:

class is_mul_hom {α β : Type*} [has_mul α] [has_mul β] (f : α → β) : Prop :=
(map_mul : ∀ x y, f (x * y) = f x * f y)

structure mul_equiv (α β : Type*) [has_mul α] [has_mul β] extends α ≃ β :=
(hom : is_mul_hom to_fun)

notation ≃* for mul_equiv, proved to be reflexive, symmetric and transitive

-- not yet found a use for this instance. Should `is_mul_hom` be a structure?
instance (h : α ≃* β) : is_mul_hom h.to_equiv := h.hom

-/

namespace mul

/-- bundled homs FTW -/
structure hom (M N : Type*) [has_mul M] [has_mul N] :=
(f : M  N)
(map_mul :  x y, f (x * y) = f x * f y)

-- but now if I delete `is_mul_hom`, how do I define `mul_equiv`?
-- notation for homs
infix ` →* `:25 := hom

view this post on Zulip Mario Carneiro (Jul 18 2019 at 04:22):

mul_equiv A B extends equiv A B, mul_hom A B

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 04:23):

Should I be using old or new structures for these things?

view this post on Zulip Mario Carneiro (Jul 18 2019 at 04:23):

old structures FTW

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 04:23):

Is what you call mul_hom what I called mul.hom?

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 04:23):

Did I name it wrong?

view this post on Zulip Mario Carneiro (Jul 18 2019 at 04:23):

I don't think so

view this post on Zulip Mario Carneiro (Jul 18 2019 at 04:24):

mul_hom A B for me is the type of augmented functions from A to B

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 04:24):

but mul.hom has got a field f and equiv has got a field to_fun and these are supposed to be defeq and have the same name.

view this post on Zulip Mario Carneiro (Jul 18 2019 at 04:24):

I don't see mul.hom in the example

view this post on Zulip Mario Carneiro (Jul 18 2019 at 04:25):

Oh there it is

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 04:25):

I'm talking about my attempt to bundle homs.

view this post on Zulip Mario Carneiro (Jul 18 2019 at 04:25):

I think that should be mul_hom

view this post on Zulip Mario Carneiro (Jul 18 2019 at 04:25):

mul isn't a namespace

view this post on Zulip Mario Carneiro (Jul 18 2019 at 04:26):

mul_hom should have a field called to_fun

view this post on Zulip Mario Carneiro (Jul 18 2019 at 04:26):

so that mul_equiv works

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 04:31):

to_fun is such a horrible name for a function. I guess its canonical name is the coercion so maybe it doesn't matter. Wait -- the map from mul_equiv X Y to mul_hom X Y -- that is no longer an instance, because mul_hom isn't a class. Is this still done with coercions somehow?

view this post on Zulip Mario Carneiro (Jul 18 2019 at 04:32):

it's a function called to_mul_hom

view this post on Zulip Mario Carneiro (Jul 18 2019 at 04:32):

You can try using a coercion but this one tends to trigger rarely

view this post on Zulip Mario Carneiro (Jul 18 2019 at 04:34):

given that the parent functions are always called to_*, to_fun seems to match that naming convention

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 04:55):

structure mul_hom (M N : Type*) [has_mul M] [has_mul N] :=
(to_fun : M  N)
(map_mul :  x y, to_fun (x * y) = to_fun x * to_fun y)

Should this have a coercion to fun?

view this post on Zulip Mario Carneiro (Jul 18 2019 at 04:56):

yes

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 05:03):

My map_mul is crappy:

set_option old_structure_cmd true

/-- bundled homs FTW -/
structure mul_hom (M N : Type*) [has_mul M] [has_mul N] :=
(to_fun : M  N)
(map_mul :  x y, to_fun (x * y) = to_fun x * to_fun y)

-- notation for homs
infix ` →* `:25 := mul_hom

instance : has_coe_to_fun (M →* N) :=
{ F := λ _, M  N,
  coe := mul_hom.to_fun }

#check mul_hom.map_mul
/-
mul_hom.map_mul : ∀ (c : ?M_1 →* ?M_2) (x y : ?M_1), c.to_fun (x * y) = c.to_fun x * c.to_fun y
-- yeah but I want it to be the coercion, not `c.to_fun`
-/

It has come out non-canonically. Am I supposed to be doing this:

def mul_hom.map_mul' :  (f : M →* N) (x y : M), f (x * y) = f x * f y := mul_hom.map_mul

?

view this post on Zulip Mario Carneiro (Jul 18 2019 at 05:04):

with the primes inverted

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 05:04):

So you're saying I need to change mathlib

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 05:04):

no

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 05:05):

you're saying I need to change my structure field's name.

view this post on Zulip Mario Carneiro (Jul 18 2019 at 05:05):

yes

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 05:25):

Should this

structure mul_equiv' (A B) [has_mul A] [has_mul B] extends equiv A B, mul_hom A B

have a coercion to fun?

view this post on Zulip Mario Carneiro (Jul 18 2019 at 05:31):

yes

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 05:56):

import data.equiv.basic algebra.group
import data.equiv.algebra

variables {α : Type*} {β : Type*} {γ : Type*}
[has_mul α] [has_mul β] [has_mul γ]
(M : Type*) (N : Type*) (P : Type*)
[has_mul M] [has_mul N] [has_mul P]

-- Recall that the unbundled definition of a mul_hom
-- and the definition of a mul_equiv, with notation ≃*, are in mathlib.

/- Mathlib:

-- in root namespace
class is_mul_hom {α β : Type*} [has_mul α] [has_mul β] (f : α → β) : Prop :=
(map_mul : ∀ x y, f (x * y) = f x * f y)

-- root namespace
structure mul_equiv (α β : Type*) [has_mul α] [has_mul β] extends α ≃ β :=
(hom : is_mul_hom to_fun)

notation ≃*, proved to be reflexive, symmetric and transitive (note: it is not a Prop)
-/


--. We will define
-- bundled homomorphisms of muls, with notation →*, and bundled
-- equivs, with notation ≃*'


set_option old_structure_cmd true

/-- bundled homs -/
structure mul_hom (M N : Type*) [has_mul M] [has_mul N] :=
(to_fun : M  N)
(map_mul' :  x y, to_fun (x * y) = to_fun x * to_fun y)

-- notation for homs
infix ` →* `:25 := mul_hom

-- I want to think of a hom as a function sometimes
instance : has_coe_to_fun (M →* N) :=
{ F := λ _, M  N,
  coe := mul_hom.to_fun }

/-- the statement that mul_homs preserve mul, in its canonical form -/
def mul_hom.map_mul :  (f : α →* β) (x y : α), f (x * y) = f x * f y := mul_hom.map_mul'

-- for structures like this you need to prove `id` and `comp` next.
namespace mul_hom

/-- the identity is a mul_hom-/
def id : M →* M := {to_fun := id, map_mul' := λ _ _, rfl}

/-- composite of mul_homs is a mul_hom -/
def comp (f : α →* β) (g : β →* γ) : α →* γ :=
{ to_fun := λ m, g (f m),
  map_mul' := λ x y, by rw [map_mul f, map_mul g] }

end mul_hom

/-- mul_equiv' (bundled mul_equiv -- the name mul_equiv is currently nicked by unbundled mul_equiv) -/
structure mul_equiv' (A B) [has_mul A] [has_mul B] extends equiv A B, mul_hom A B

-- notation for mul_equiv'
infix ` *' `:25 := mul_equiv'

instance : has_coe_to_fun (M *' N) := { F := _,
  coe := mul_equiv'.to_fun }

def mul_equiv'.map_mul :  (f : α *' β) (x y : α), f (x * y) = f x * f y
:= mul_equiv'.map_mul'

-- now need reflexive, symmetric and transitive

namespace mul_equiv'

@[refl] def refl (α : Type*) [has_mul α] : α *' α :=
{ map_mul' := λ x y, rfl,
..equiv.refl α}

-- this one did not go so well.
@[symm] def symm (h : α *' β) : β *' α :=
{ map_mul' := λ n₁ n₂, function.injective_of_left_inverse h.left_inv begin
    show h.to_fun (h.inv_fun (n₁ * n₂)) =
    h (h.inv_fun n₁ * h.inv_fun n₂), -- annoying to have to `show`
    rw h.right_inv,
    rw h.map_mul,
    convert rfl, -- annoying to have to `convert`. This should surely just be rewrites.
      exact h.right_inv _,
    exact h.right_inv _,
  end,
  ..h.to_equiv.symm}

@[trans] def trans (h1 : α *' β) (h2 : β *' γ) : (α *' γ) :=
{ map_mul' := λ x y,
    show h2 (h1 (x * y)) = h2 (h1 x) * h2 (h1 y),
    by rw [h1.map_mul, h2.map_mul],
  ..equiv.trans h1.to_equiv h2.to_equiv }

-- an ≃*' is a hom
def equiv'.to_hom (h : M *' N) : M →* N :=
  { to_fun := h.to_equiv,
    map_mul' := h.map_mul'
  }

def equiv'.inv_hom (h : M *' N) : N →* M :=
  { to_fun := h.symm.to_equiv,
  map_mul' := h.symm.map_mul
  }

end mul_equiv'

equiv'.symm didn't go well but most of the other stuff looks OK to me

view this post on Zulip Mario Carneiro (Jul 18 2019 at 06:00):

People will complain about the order of arguments to comp

view this post on Zulip Johan Commelin (Jul 18 2019 at 06:01):

@Kevin Buzzard You probably know this but mul_hom.map_mul should be a lemma, and it is a very good simp-lemma.

view this post on Zulip Mario Carneiro (Jul 18 2019 at 06:01):

What's wrong with symm? It looks like that's the sort of thing that is mathematically substantive anyway

view this post on Zulip Johan Commelin (Jul 18 2019 at 06:02):

In fact, that's the most important reason for bundling in the first place. That this is a simp-lemma that actually triggers.

view this post on Zulip Johan Commelin (Jul 18 2019 at 06:02):

Also, we'll want simp-lemmas id_apply and comp_apply.

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 06:25):

Kevin Buzzard You probably know this but mul_hom.map_mul should be a lemma, and it is a very good simp-lemma.

I'm not very good at simp still.

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 11:49):

So anyway, there is a bunch of structure most of which is correctly named, and hopefully defined sensibly. Do we want all all of this in mathlib? And then there's the equivalent stuff for semigroup, for monoid and for group. I don't care about the mul stuff really, I was just practicing. I do care about equivs of monoids and of groups and would like some students to prepare a mathlib PR.

What are we looking for in such a PR? Should the students try and define everything for semigroup when we don't really need it? Is a PR of this nature for group welcome? @Chris Hughes do you have any opinions on this? I've talked to you before about it and you seem to have a clear head about what should be there.

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 11:50):

Note that we can define group.hom to be mul_hom

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 11:50):

I think the last time we talked about this, you liked that idea.

view this post on Zulip Chris Hughes (Jul 18 2019 at 12:08):

Don't bother with semigroup stuff unless it's virtually no effort. I'd actually prefer group_hom and monoid_hom to be the same, since these are the two that are actually used. You could write a custom constructor without the unnecessary axiom.

Same idea goes for ring_hom and semiring_hom

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 12:16):

so you're saying you want group.hom to be called group_hom and to demand that f(1)=1?

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 12:16):

What should the custom constructor be called?

view this post on Zulip Chris Hughes (Jul 18 2019 at 12:26):

Yes @[reducible] def group_hom := monoid_hom.

group_hom.mk

view this post on Zulip Chris Hughes (Jul 18 2019 at 12:27):

That way, simp lemmas you prove about monoid_homs will work with group homs.

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 18:15):

And should this be reducible too? [sorry for prime on mul_equiv, mathlib has a slightly more unbundled one]

def monoid_equiv (M N) [monoid M] [monoid N] := mul_equiv' M N

view this post on Zulip Johan Commelin (Jul 18 2019 at 18:18):

Is it clear that making some of these definitions does not create leakage?

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 18:19):

I am just experimenting. I will certainly report back.

view this post on Zulip Johan Commelin (Jul 18 2019 at 18:21):

Also, I think Lean is quite bad at dealing with situations like this:
I have M1 M2 : Type and [monoid M1] [monoid M2]
I also have f : monoid_hom M1 M2.
Then, for some reason, it happens that I can actually prove that M1 and M2 are groups.
Now I need to work to turn f into a group hom. And if I don't do that, certain lemma's can't be applied, and simp gets stuck etc...

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 18:22):

This won't happen with Chris' suggesting of defining group_hom to be equal to monoid_hom

view this post on Zulip Johan Commelin (Jul 18 2019 at 18:22):

I know it is not very beginner-friendly. But I'm becoming more and more of the opinion that we shouldn't have these "shadowing" classes. Like vector_space (and even module). And so, maybe we should also just get rid of group_homs

view this post on Zulip Johan Commelin (Jul 18 2019 at 18:22):

Nope, that's not true.

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 18:22):

and making it reducible

view this post on Zulip Johan Commelin (Jul 18 2019 at 18:22):

If I have a module over a field, I can't apply linear algebra results.

view this post on Zulip Johan Commelin (Jul 18 2019 at 18:23):

Even if vector_space is reducibly defined to be a module.

view this post on Zulip Johan Commelin (Jul 18 2019 at 18:23):

This has bitten me several times.

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 18:24):

We need some way of being able to talk about group homomorphisms. What is your suggestion? Unbundled homs? I thought this had problems too?

view this post on Zulip Johan Commelin (Jul 18 2019 at 18:24):

No, it's somewhat orthogonal to bundling, but it's very much related to refactoring.

view this post on Zulip Johan Commelin (Jul 18 2019 at 18:24):

I want to propose/discuss just ditching group_hom altogether.

view this post on Zulip Johan Commelin (Jul 18 2019 at 18:25):

Just write monoid_hom.mk' for the case that you construct monoid homs between groups.

view this post on Zulip Johan Commelin (Jul 18 2019 at 18:25):

It doesn't look nice... but it is more flexible.

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 18:26):

This has bitten me several times.

If you try to fix it by making the actual object you want from the object you have (e.g. the vector space over the field from the module), then you then have two objects which mathematicians find completely indistinguishable, but for which Lean finds it hard to port results about one object to results from the other. This sounds like a good place to try out a transfer tactic, no?

view this post on Zulip Johan Commelin (Jul 18 2019 at 18:27):

Meh... I would rather let the problem go away.

view this post on Zulip Johan Commelin (Jul 18 2019 at 18:27):

Maybe group_hom can be an abbreviation?? I still don't know what this does exactly.

view this post on Zulip Johan Commelin (Jul 18 2019 at 18:28):

But it seems to be something like hyper-super-duper-reducible.

view this post on Zulip Chris Hughes (Jul 18 2019 at 18:28):

And should this be reducible too? [sorry for prime on mul_equiv, mathlib has a slightly more unbundled one]

def monoid_equiv (M N) [monoid M] [monoid N] := mul_equiv' M N

That shouldn't exist

view this post on Zulip Johan Commelin (Jul 18 2019 at 18:29):

For the same reason that vector_space shouldn't exist?

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 18:34):

I want to propose/discuss just ditching group_hom altogether.

If we ditch group_hom altogether, what will be the canonical way of representing the concept of f:GHf:G\to H with f(xy)=f(x)f(y)f(xy)=f(x)f(y) with GG, HH groups?

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 18:35):

def monoid_equiv (M N) [monoid M] [monoid N] := mul_equiv' M N

That shouldn't exist

If that doesn't exist at all, then what happens to the poor newbie who shows up with their two monoids and wants to know where the equiv is?

view this post on Zulip Johan Commelin (Jul 18 2019 at 18:37):

We tell them to use M1 =* M2.

view this post on Zulip Johan Commelin (Jul 18 2019 at 18:37):

If we ditch group_hom you just write f : G →m H

view this post on Zulip Johan Commelin (Jul 18 2019 at 18:37):

Or whatever the notation for monoid homs will be.

view this post on Zulip Chris Hughes (Jul 18 2019 at 18:41):

I started on ->1*, but I propose ->*, and screw mul homs notation.

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 19:11):

So notation can attempt to solve the issue. Chris are you proposing the notation with no 1 to be overloaded? I am mostly interested in group homs and isoms because a student of mine needs them asap

view this post on Zulip Chris Hughes (Jul 18 2019 at 19:16):

I'm proposing no notation for mul homs, since they're rarely used.

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 20:12):

then what term is ->* notation for?

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 20:12):

I am happy to implement your idea but I don't understand it yet. I would just like isomorphisms and bundled homomorphisms of groups sooner rather than later.

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 20:13):

I want to do more experiments with the bundled morphisms approach.

view this post on Zulip Chris Hughes (Jul 18 2019 at 20:13):

monoid homs

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 20:14):

A monoid hom has this extra condition that 1 goes to 1. So we define monoid_hom, and we can make \equiv\_g be notation for monoid_hom.

view this post on Zulip Johan Commelin (Jul 18 2019 at 20:15):

Sure, so Chris is saying →* for monoid homs and group homs. No notation for mul_hom.

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 20:15):

and we could also make \equiv\_m be notation for monoid_hom for when we're working with moniods, and then Lean's prettyprinter would have an impossible notation problem to solve.

view this post on Zulip Johan Commelin (Jul 18 2019 at 20:15):

And \equiv* might be a nice fit for mul_equiv (and we don't need monoid_equiv or group_equiv).

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 20:16):

So we just tell the user in comments in the group section: "the notation for group homomorphisms is ->* and the notation for group isomorphisms is \equiv*"

view this post on Zulip Johan Commelin (Jul 18 2019 at 20:17):

Sure... and because the notation is somewhat natural it is even avoiding the awkard f : monoid_hom G H for group homs.

view this post on Zulip Johan Commelin (Jul 18 2019 at 20:17):

I think this is quite a nice solution.

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 20:19):

That's quite interesting that the force of the mathematical interpretation ->* is "I preserve everything relevant to multiplication that is present"

view this post on Zulip Johan Commelin (Jul 18 2019 at 20:19):

The special constructor could be

def group_hom {G H : Type} [group G] [group H] (h : f (x*y) = f x * f y) : G →* H := sorry

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 20:20):

If you defined monoids to mathematicians and then said "OK now what do you think MNM\to^*N means?" they'd be like "monoid hom I guess"

view this post on Zulip Johan Commelin (Jul 18 2019 at 20:20):

(That example didn't type check, but you get the idea.)

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 20:21):

But Chris seems to be explictly suggesting that the name group_hom is never assigned. Is this what you think @Chris Hughes ?

view this post on Zulip Johan Commelin (Jul 18 2019 at 20:21):

What I'm saying is that monoid_hom.mk is a bad name for constructing monoid homs between groups.

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 20:22):

These are all such irrelevances, there must be some solution with automation or something. Mathematically we are doing absolutely nothing at all.

view this post on Zulip Johan Commelin (Jul 18 2019 at 20:22):

I've been saying time and again that Fabian can auto-generate all of these.

view this post on Zulip Johan Commelin (Jul 18 2019 at 20:22):

But people don't really seem to care.

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 20:26):

@Mario Carneiro we need computer science help. We have a very rigorous notion of "the same" here -- this seems to me like this is type class inference in a tangle. Do you understand why we are struggling? Why can't Johan do linear algebra with a module over a field? @Johan Commelin can you give a MWE? We need to get good at this.

view this post on Zulip Mario Carneiro (Jul 18 2019 at 20:41):

I think that more names for the same thing is bad for formalization, although I understand why it is mathematically desirable. I am on board with Chris's suggestions

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 20:44):

We also need the additive version of everything, I suppose? That entire process can be automated. Can you literally to a regex on the file to generate its additive version? And then you can look observe the funny fact that there are two olean files which are exactly the same

view this post on Zulip Mario Carneiro (Jul 18 2019 at 20:44):

While I don't want to minimize Fabian's work, the proofs are not the hard part here. This is all API design questions

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 20:44):

Right. I'm trying really hard to make a mathematician's API.

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 20:45):

I now have a much better understanding of the issues here and I think it's a really important question for drawing mathematicians in. We want to make it look easy.

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 20:47):

I think we might be losing half our audience at

inductive nat
| zero : what does all this weird stuff mean

We just want to say "The naturals are N\mathbb{N}, typed \N and they work exactly as you would expect them to". Implementing this is not a trivial thing at all!

view this post on Zulip Mario Carneiro (Jul 18 2019 at 20:50):

I heartily disagree

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 20:50):

"It goes without saying that if AA and BB are isomorphic comm_rings then AA is Gorenstein iff BB is. It does not need a proof. "

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 20:50):

that one is not proving trivial to implement

view this post on Zulip Mario Carneiro (Jul 18 2019 at 20:50):

hardcoding what "they work exactly as you would expect" means is just making lean more "magical" and less comprehensible

view this post on Zulip Mario Carneiro (Jul 18 2019 at 20:51):

which is setting yourself up for failure

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 20:51):

You guys worry too much about these tedious implementation issues

view this post on Zulip Mario Carneiro (Jul 18 2019 at 20:52):

That's not an implementation issue, it's a pedagogy issue

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 20:52):

We're never going to run the code we're making, you don't need to optimise it

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 20:52):

We just want to eat every proposition and every proof bit by bit

view this post on Zulip Mario Carneiro (Jul 18 2019 at 20:52):

if lean has tons of special cases then it's big and complicated to learn. This is not an exaggeration, it's already the case

view this post on Zulip Mario Carneiro (Jul 18 2019 at 20:56):

implementing transfer is hard because type theory is big and complicated

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 20:57):

You should just solve it with pointers or something

view this post on Zulip Mario Carneiro (Jul 18 2019 at 21:03):

:expressionless:

view this post on Zulip Mario Carneiro (Jul 18 2019 at 21:05):

That said, transfer is already implemented and mostly works. As I've said many times, what is needed is not a tactic but lemmas for it to use

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 21:08):

So mathematicians have a gigantic list of abstract mathematical ideas. And for each of these ideas computer scientists have developed some term in type theory, or perhaps some token (the mathematical symbol of isomorphism comes to mind), and said "look here it is", and then we say "Thanks. Does it do this, this, that and this?" and you guys go "Yes of course. And it does a gazillion other things too like look you can see inside it and you can do that if you want" and we say "no thanks, we just need this this that and this. We will now promise that any future terms will be built using that interface. In return, you must understand our notion of equality, which you can work out from the interface I suppose"

Examples: the real numbers, a group, the localisation of a ring, the module of one-forms for an algebra over a ring, or a sheaf on a space.

view this post on Zulip Mario Carneiro (Jul 18 2019 at 21:09):

Except that sometimes you break the interface and pretend you didn't

view this post on Zulip Mario Carneiro (Jul 18 2019 at 21:11):

Reading the MO question I was amused that no one noticed that RC\Bbb R\subseteq\Bbb C is not an isomorphism-invariant statement. They say "we know isomorphisms don't matter so we may as well assume it's the case" but then it's not isomorphism invariant anymore

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 21:12):

I find those endless comments very hard to read.

view this post on Zulip Mario Carneiro (Jul 18 2019 at 21:13):

I think that statement showed up in one of the answers

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 21:13):

Was it the one I accepted?

view this post on Zulip Mario Carneiro (Jul 18 2019 at 21:15):

https://mathoverflow.net/a/336233/34444

view this post on Zulip Mario Carneiro (Jul 18 2019 at 21:16):

Relatedly, we can assume that RC\Bbb R\subseteq\Bbb C because we only care about the axiomatized properties of R\Bbb R, which are preserved under isomorphism. One could manually preserve the original R\Bbb R as an actual subset of its quadratic extension, but that is unnecessary for the reason I just stated.

This reasoning fails to take into account that by taking advantage of isomorphism invariance you break it

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 21:16):

There are also two deleted answers with positive scores which degenerated into flamewars resulting in the OP just deleting everything

view this post on Zulip Mario Carneiro (Jul 18 2019 at 21:17):

I saw the comment but I'm not high rep on MO so I can't read it :(

view this post on Zulip Mario Carneiro (Jul 18 2019 at 21:17):

Andrej usually has interesting things to say

view this post on Zulip Mario Carneiro (Jul 18 2019 at 21:20):

To me the process is tedious but straightforward. We need equiv.rel in mathlib, and then a bunch of isomorphism builders, and a bunch of isomorphism statements, and then this will be easy

view this post on Zulip Mario Carneiro (Jul 18 2019 at 21:22):

Don't come to me about making a tactic to do it until you've already done it 10 times and know what it looks like

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 21:22):

I think Andrej and I follow each other on Twitter; I'll prod him.

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 21:32):

What is the role that this predicate should play? We define the Cauchy reals, and we prove that they are a complete arch field, and then we prove that any two complete arch fields are uniquely isomorphic as ordered fields. We then have this type real and this promise that we will only use complete_archimedean_ordered_field real or whatever. We have given you a precise interface here. What you now need to do somehow is to make this a primitive object -- I would quite happily be in an environment where the real type and its instance as a complete archimedean ordered field was some structure and a bunch of axioms. Why can't we use this abstraction for the reals and only have access to this interface?

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 21:34):

It would presumably be easier to reason about proof transportability if you knew the proof had stuck to the interface.

view this post on Zulip Mario Carneiro (Jul 18 2019 at 21:34):

I'm talking about transfer specifically. This is independent of any interface to the reals you may or may not be adhering to

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 21:34):

I want a little bit of HoTT magic at exactly this point

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 21:34):

So tell me again what transfer specifically means?

view this post on Zulip Mario Carneiro (Jul 18 2019 at 21:35):

To me the process is tedious but straightforward. We need equiv.rel in mathlib, and then a bunch of isomorphism builders, and a bunch of isomorphism statements, and then this will be easy

view this post on Zulip Mario Carneiro (Jul 18 2019 at 21:36):

The only way to get, provably in lean, invariance from syntax generically is if you have a deeply embedded language and express all your properties in that language. I'm sure we don't want to do that

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 21:36):

Will this tedious but straightforward process be easier to do in Lean 4?

view this post on Zulip Mario Carneiro (Jul 18 2019 at 21:36):

not particularly

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 21:36):

So we may as well start right away :-)

view this post on Zulip Mario Carneiro (Jul 18 2019 at 21:37):

like I said, stop thinking of tactics and start thinking about the problem

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 21:37):

Isn't the immediate problem that someone has to write some meta code?

view this post on Zulip Mario Carneiro (Jul 18 2019 at 21:37):

Once you know what the problem is and what the solution is the tactic writes itself

view this post on Zulip Mario Carneiro (Jul 18 2019 at 21:37):

no

view this post on Zulip Mario Carneiro (Jul 18 2019 at 21:37):

meta code comes later

view this post on Zulip Mario Carneiro (Jul 18 2019 at 21:38):

proofs come first

view this post on Zulip Mario Carneiro (Jul 18 2019 at 21:40):

Tactics never allow you to prove something you couldn't prove before. They just make it easier to do things you already knew how to do

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 21:40):

So maybe a tactic which does this would be interesting: I will define the Dedekind reals in Lean, prove they're a complete arch ordered field, and then demand from you a copy of the Bochner integral but all with Dedekind reals instead of Cauchy reals.

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 21:40):

Do I "know how to do that"? Is this one we're going to solve with tags?

view this post on Zulip Mario Carneiro (Jul 18 2019 at 21:41):

You don't, that's the problem

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 21:41):

the idea is that any PR to mathlib which didn't use the allowable interface would not be accepted.

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 21:42):

So you just have to write some regex to check that people aren't fiddling with the real's privates

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 21:42):

and run all PR's through the regex to check for safety

view this post on Zulip Mario Carneiro (Jul 18 2019 at 21:42):

The safety check is not the problem, the equivalence proofs are

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 21:42):

and if they pass you can accept the PR and then some Lean code generates a proof that all the stuff in mathlib is still "safe"

view this post on Zulip Mario Carneiro (Jul 18 2019 at 21:43):

Even if we know everything is safe that doesn't provide a proof of equivalence

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 21:43):

So what formally is the problem?

view this post on Zulip Mario Carneiro (Jul 18 2019 at 21:43):

You have already stated it: Given a concrete predicate P on rings prove that if A and B are isomorphic rings then P(A) iff P(B)

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 21:43):

Surely it provides a proof that the term exists, it just doesn't actually make the term.

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 21:44):

Why isn't that P(A) iff P(B) thing easy?

view this post on Zulip Mario Carneiro (Jul 18 2019 at 21:44):

It is

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 21:44):

You just peel P apart and do it by induction

view this post on Zulip Mario Carneiro (Jul 18 2019 at 21:44):

Yes, so do it

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 21:44):

You mean it's hard to implement?

view this post on Zulip Mario Carneiro (Jul 18 2019 at 21:44):

No, it's easy

view this post on Zulip Mario Carneiro (Jul 18 2019 at 21:44):

but it's work

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 21:45):

I can't do it, I have my decency.

view this post on Zulip Mario Carneiro (Jul 18 2019 at 21:45):

and it needs to actually be in mathlib

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 21:45):

It's not maths.

view this post on Zulip Mario Carneiro (Jul 18 2019 at 21:45):

transfer will not work until mathlib is full of theorems like that

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 21:45):

that's an axiom, you guys have to do that one :-) I would have no idea how to do it. Is it the sort of thing a novice tactic-writer could try?

view this post on Zulip Mario Carneiro (Jul 18 2019 at 21:46):

If you don't know how to do it, how would a novice know?

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 21:46):

I mean maybe they can just read Programming In Lean and then just do it

view this post on Zulip Mario Carneiro (Jul 18 2019 at 21:46):

A novice tactic writer can generalize from examples, but we have none

view this post on Zulip Mario Carneiro (Jul 18 2019 at 21:46):

once we have done it by hand 10 times a novice tactic writer can do the rest

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 21:46):

So what needs doing in practice?

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 21:47):

What's the first thing that needs to be done?

view this post on Zulip Mario Carneiro (Jul 18 2019 at 21:47):

equiv.rel, isomorphism builders, and theorems of the form A ~= B -> P(A) <-> P(B)

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 21:47):

Are there some sorts of milestones which you can see to making this transfer tactic?

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 21:47):

So what is the type of equiv.rel?

view this post on Zulip Mario Carneiro (Jul 18 2019 at 21:48):

equiv.rel (e : A ~= B) : A -> B -> Prop := \lam a b, e a = b

view this post on Zulip Mario Carneiro (Jul 18 2019 at 21:49):

This allows you to state a theorem of the form A ~= B -> P(A) <-> P(B) as e.rel => iff where => is that funny relator operation

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 21:49):

oh so that one's done now, right?

view this post on Zulip Mario Carneiro (Jul 18 2019 at 21:50):

You need a few theorems about it

view this post on Zulip Mario Carneiro (Jul 18 2019 at 21:50):

the most important ones for transfer is that it is left and right unique

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 21:50):

OK so is there some structure I need to make on equiv.rel?

view this post on Zulip Mario Carneiro (Jul 18 2019 at 21:50):

and the converse is given by equiv.rel of the inverse equiv

view this post on Zulip Mario Carneiro (Jul 18 2019 at 21:51):

I think left_unique and right_unique are typeclasses

view this post on Zulip Mario Carneiro (Jul 18 2019 at 21:52):

If you look at logic.relator there are several functions related to this sort of thing

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 21:57):

Just to be clear -- the e : A =~ B notation -- the type of e is just some random type T A B, or does it have to have some sort of equivalence relation properties?

view this post on Zulip Mario Carneiro (Jul 18 2019 at 21:58):

e is an equiv

view this post on Zulip Mario Carneiro (Jul 18 2019 at 21:59):

not a fancy equiv, just an equiv

view this post on Zulip Mario Carneiro (Jul 18 2019 at 22:00):

More complicated things would have something like (e.to_equiv.rel => iff) Gorenstein Gorenstein where e is a ring equiv

view this post on Zulip Jeremy Avigad (Jul 18 2019 at 22:00):

@Kevin Buzzard I can't resist a bit of history here. Read Dedekind's Was sind und was sollen die Zahlen (1888), roughly "What are the [natural] numbers and what should they be." See especially the introduction. (It is the second essay here: http://www.gutenberg.org/files/21016/21016-pdf.pdf.) The answer to the question posed in the title is expressed more clearly in his letter to Keferstein: http://www.bris.ac.uk/media-library/sites/structuralism/migrated/documents/kerfstein.pdf. It is as you say: We don't care what they are, as long as they satisfy the properties we want. We only need to construct one to show that the notion is coherent. Then, if as long as we respect the interface, anything we say about one will be true of the other. (The part about respecting the interface is in Section 134 on page 48 of the essay.) In modern terms, he gave an axiomatic characterization of the natural numbers, a set theoretic construction (from the assumption that there exists an infinite set), and a proof that any two systems satisfying the axioms are isomorphic.

Dedekind was an early proponent of a modern, structural view of mathematics, at a time when the subject had a much more calculational style. According to van der Waerden, Emmy Noether used to say "Es steht alles schon bei Dedekind," i.e. everything is already there, in Dedekind.

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 22:11):

I have seen all this stuff before but I just never really understood its depth until recently

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 23:10):

But in some sense it really is not mathematics. This whole thing is just a tedious implementation issue.

view this post on Zulip Kevin Buzzard (Jul 18 2019 at 23:10):

Everything is already there, in Dedekind.

view this post on Zulip Andrew Ashworth (Jul 19 2019 at 10:57):

Maybe the old usage of transfer to prove properties about ints-as-pairs-of-naturals should be the in mathlib docs, i.e. https://github.com/leanprover/lean/blob/6ab792733d09878d82ce98d88f6f476c8e0f34d8/library/init/data/int/basic.lean

view this post on Zulip Kevin Buzzard (Jul 19 2019 at 18:22):

import data.equiv.basic
import logic.relator

def equiv.rel {A B : Type*} (e : A  B) : A  B  Prop := λ a b, e a = b

variables {A : Type*} {B : Type*} (e : A  B)

instance : relator.left_unique (equiv.rel e) := λ a₁ b a₂ h1 h2, equiv.injective e $ eq.trans h1 h2.symm
instance : relator.right_unique (equiv.rel e) := λ a b₁ b₂ h1 h2, eq.trans h1.symm h2

What next?

view this post on Zulip Mario Carneiro (Jul 19 2019 at 18:24):

pick a simple predicate or construction and try to prove its isomorphism theorem

view this post on Zulip Kevin Buzzard (Jul 19 2019 at 19:02):

lemma rel_imp : (iff  (iff   iff)) implies implies :=

this logic.relator file is pretty cool :-)

But didn't @Scott Morrison and/or @Simon Hudon write a bunch of this sort of code years ago?

view this post on Zulip Kevin Buzzard (Jul 19 2019 at 19:02):

the lemma below looks like some experimental new one way traffic system

view this post on Zulip Kevin Buzzard (Jul 19 2019 at 19:02):

lemma rel_iff : (()  ()  ()) () () := ...

view this post on Zulip Mario Carneiro (Jul 19 2019 at 19:03):

It's a new way to write *_congr lemmas

view this post on Zulip Mario Carneiro (Jul 19 2019 at 19:04):

For the proof, I would just unfold the notations straight away until I know what I'm doing. The transfer tactic knows how to put the lemmas together without unfolding them

view this post on Zulip Kevin Buzzard (Jul 19 2019 at 19:06):

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/how.20to.20use.20transfer/near/135299706

view this post on Zulip Kevin Buzzard (Jul 19 2019 at 19:07):

We've talked about this stuff before and I have just about enough control of Zulip search to be able to find some of it.

view this post on Zulip Mario Carneiro (Jul 19 2019 at 19:08):

There's another old post where I prove isomorphism theorem for maximal ideals this way

view this post on Zulip Mario Carneiro (Jul 19 2019 at 19:08):

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Perfectoid.20spaces/near/159808751

view this post on Zulip Kevin Buzzard (Jul 19 2019 at 19:09):

And there was definitely one where I started talking about this sort of thing and was asking how to make a transfer tactic, and Simon and Scott just talked about it for a while and then I think Scott wrote a tonne of code, and there was quite an active period during which you (Mario) were asleep, and then you woke up and checked Zulip and were like "wooah you guys have moved fast" or something. I'd really like to find that thread.

view this post on Zulip Kevin Buzzard (Jul 19 2019 at 19:10):

At the time I just remember not understanding the issues well enough, and hence being unable to understand the code properly

view this post on Zulip Kevin Buzzard (Jul 19 2019 at 19:11):

It was some code which went through a fair few primitives and proved a lemma about each of them, and then started proving lemmas about other things all hands-on.

view this post on Zulip Kevin Buzzard (Jul 19 2019 at 19:12):

Maybe there was also talk about using tags for transfer, and using typeclass resolution to tag more and more stuff as "still OK if replaced by isomorphic thing"

view this post on Zulip Mario Carneiro (Jul 19 2019 at 19:12):

oh that's right there was a respects_isomorphism typeclass IIRC

view this post on Zulip Mario Carneiro (Jul 19 2019 at 19:13):

I forget the actual name

view this post on Zulip Kevin Buzzard (Jul 19 2019 at 19:13):

Each time this transfer conversation occurs I learn quite a lot about the idea, but I still have work to do.

view this post on Zulip Kevin Buzzard (Jul 19 2019 at 23:55):

import data.real.basic

instance notation.sub_eq_add_neg (X : Type) [has_add X] [has_neg X] :
has_sub X := ⟨λ a b, a + -b

class has_field_notation (X : Type) extends has_zero X, has_one X,
has_mul X, has_add X, has_neg X -- note: don't use has_sub
-- because it might cause a diamond now

instance : has_field_notation  := by refine {};apply_instance

class complete_ordered_archimedean_field (X : Type) [has_field_notation X] : Prop :=
(all_the_axioms :  x y : X, x + y = y + x) -- ...
(etc :  x : X, 1 * x = 1)

-- boring proof omitted
instance cauchy_reals_are_complete : complete_ordered_archimedean_field  := sorry

structure Reals :=
(X : Type)
[h : has_field_notation X]
(e : complete_ordered_archimedean_field X)

def CauchyReals : Reals :=
{ X := ,
  h := by apply_instance,
  e := cauchy_reals_are_complete
}

structure ordered_field_equiv (X Y : Type) [has_field_notation X] [has_field_notation Y]
  [complete_ordered_archimedean_field X] [complete_ordered_archimedean_field Y]
  extends equiv X Y -- add extra axioms here

theorem all_reals_are_the_same (X : Type) [has_field_notation X]
  [complete_ordered_archimedean_field X] :
 e : ordered_field_equiv X , true := sorry -- boring proof omitted

class platonist_friendly (P : set Reals) : Prop :=
(e :  X : Reals, P X  P CauchyReals)

instance (P Q : set Reals) [platonist_friendly P] [platonist_friendly Q] :
platonist_friendly (P  Q) := ⟨λ X, begin
  show P X  Q X  P CauchyReals  Q CauchyReals,
  rw [_inst_1.e, _inst_2.e]
end

I didn't look at your work yet, I just thought I'd try and work out some concepts with this Cauchy / Dedekind reals thing.

One could even play the same game with the Lau Rationals (the field of fractions of Z\mathbb{Z}) vs the computer science rationals in mathlib.

view this post on Zulip Kevin Buzzard (Jul 20 2019 at 00:02):

Is the idea that a tactic can generate instances of the platonist_friendly class, by induction on P somehow? There are no relators above so they are also clearly offering something which I've not yet understood. And finally there is this question which does not appear to be addressed by the above -- if I prove some theorem about some Bochner integral of some function being equal to pi, how do I mark this theorem with the "there is a version of me for Dedekind reals and indeed for all terms of type Reals" tag?

view this post on Zulip Mario Carneiro (Jul 20 2019 at 00:22):

What relators bring to the table is the ability to deal with n-ary predicates, with a variety of equivalences on the inputs (one type might be in bijection, the other is a module and there's a module iso, and then relative to the first equiv some elements a and b are related)

view this post on Zulip Mario Carneiro (Jul 20 2019 at 00:23):

This is necessary for making the "proof by induction" go through

view this post on Zulip Mario Carneiro (Jul 20 2019 at 00:23):

which is why I'm not supportive of the typeclass approach

view this post on Zulip Mario Carneiro (Jul 20 2019 at 00:25):

The relator way to write platonist_friendly P is (e.rel => iff) P P where e is an ordered field equiv

view this post on Zulip Mario Carneiro (Jul 20 2019 at 00:28):

well that's not quite accurate since you bundled Reals. Normally you would use some relation R : Reals -> Reals -> Prop asserting that the two elements of Reals are isomorphic, but in the case of Reals that's the trivially true relation

view this post on Zulip Kevin Buzzard (Jul 20 2019 at 08:55):

Yes, the reals are somehow an easier case, the universal predicate applies to types with field notation and is just the assertion that they're complete ordered Archimedean fields which is enough to make them "the same as" the platonic reals

view this post on Zulip Kevin Buzzard (Jul 21 2019 at 02:25):

I bundled subthings and morphisms of things!

import data.equiv.basic

class thing (α : Type) : Type. -- insert data here (usually notation and some axioms)

variables {α β γ: Type} [thing α] [thing β] [thing γ]

class is_subthing (s : set α) : Prop := true -- this class should not exist. Sometimes you see it in mathlib though.

set_option old_structure_cmd true

structure subthing (α : Type) [thing α] :=
(carrier : set α)
(proof : is_subthing carrier) -- replace with notation closure axioms e.g. one_mem, mul_mem etc. Note that is_subthing is never used again.

instance : has_coe_to_sort (subthing α) := ⟨_, subthing.carrier

instance : has_coe (subthing α) (set α) := subthing.carrier

-- another deprecated class
def is_thing_morphism (f : α  β) : Prop := true -- this class should not exist. Sometimes you see it in mathlib though.
-- I won't bother making it into a class. It's deprecated.

structure thing_morphism α β [thing α] [thing β]:=
(to_fun : α  β)
(h : is_thing_morphism to_fun) -- replace with notation-preserving axioms e.g. map_one, map_mul.... Note that `is_thing_morphism`  never occurs again

infixr ` t `:25 := thing_morphism

instance : has_coe_to_fun (α t β) :=
{ F := λ _, α  β,
  coe := thing_morphism.to_fun}

lemma thing_morphism.ext (f g : α t β) : (f : α  β) = g  f = g := begin
  intro h,
  cases f,
  cases g,
  rwa thing_morphism.mk.inj_eq,
end

-- bundled equivs using old structure command so no `to_fun` problems
structure thing_equiv α β [thing α] [thing β] extends equiv α β, thing_morphism α β

infix ` t `:25 := thing_equiv

namespace thing_equiv

instance : has_coe_to_fun (thing_equiv α β) := { F := λ _, α  β, coe := to_fun}

theorem ext {f g : thing_equiv α β} (h : (f : α  β) = g) : f = g :=
begin
  cases f, cases g,
  rw thing_equiv.mk.inj_eq,
  refine equiv.mk.inj _;try {assumption},
  change f_to_fun = g_to_fun at h,
  refine equiv.ext _ _ _,
  exact congr_fun h,
end

lemma coe_inj : function.injective (thing_equiv.to_equiv : thing_equiv α β  equiv α β) := begin
  intros f g h,
  apply ext,
  -- is this idiomatic?
  show (to_equiv f) = _,
  rw h,
  refl,
end

@[refl] protected def refl (α : Type) [thing α] : α t α := { h := trivial,..equiv.refl α}
@[symm] protected def symm (e : α t β) : β t α := { h := trivial,..e.to_equiv.symm}
@[trans] protected def trans (e1 : β t γ) (e2 : α t β) : α t γ := { h := trivial,..e2.to_equiv.trans e1.to_equiv}

-- perms
def perm (α : Type) [thing α] := thing_equiv α α

instance : has_one (perm α) := thing_equiv.refl α
instance : has_mul (perm α) := thing_equiv.trans -- goodness knows if this is "right" or whether I should swap
instance : has_inv (perm α) := thing_equiv.symm

instance : group (perm α) :=
{ mul := (*),
  one := 1,
  inv := λ x, x⁻¹,
  mul_assoc := λ _ _ _, ext rfl,
  one_mul := λ _, ext rfl,
  mul_one := λ _, ext rfl,
  mul_left_inv := λ f, ext $ begin funext x, exact f.left_inv x end}

end thing_equiv

I got as far as the automorphism group of a thing.

view this post on Zulip Kevin Buzzard (Jul 21 2019 at 02:31):

Now someone can knock off a tactic and we can just bundle everything instantly.

view this post on Zulip Kevin Buzzard (Jul 21 2019 at 02:31):

@Sian Carey

view this post on Zulip Kevin Buzzard (Jul 21 2019 at 04:14):

@Chris Hughes my understanding is that you want bundled monoid_hom but no definition of group_hom. Could there still be a group_hom namespace though?

view this post on Zulip Kevin Buzzard (Jul 21 2019 at 04:45):

I want to define field homomorphisms between $fields$ which I guess are called discrete_field. Chris / @Mario Carneiro -- what do you people want the bundled class to be called (discrete_field_hom, field_hom, ring_hom, semiring_hom...) and exactly what instances to you want Lean to ask for in the actual definition of the structure? (e.g. map_zero follows from map_add because everything is a field in my case of interest, so we don't need it, but I don't care if map_zero is a field or not, I just want to do it right).

view this post on Zulip Mario Carneiro (Jul 21 2019 at 04:47):

Are semiring_hom, ring_hom and field_hom all the same?

view this post on Zulip Kevin Buzzard (Jul 21 2019 at 04:47):

yes but I thought Chris was arguing that some of these things shouldn't even be tokens.

view this post on Zulip Mario Carneiro (Jul 21 2019 at 04:48):

Of those ring_hom is my favorite

view this post on Zulip Kevin Buzzard (Jul 21 2019 at 04:49):

I thought he suggested that group_hom be not defined, ->* be notation for monoid_hom which also demands map_one and just tell the user to use the right notation for group homs which happens to coincide with the notation for monoid homs. They will never have to make one with their bare hands hopefully :-)

view this post on Zulip Mario Carneiro (Jul 21 2019 at 04:50):

We can do the same thing with field homs - call it ring_hom, but it's really a semiring hom and you use it for semirings and fields too

view this post on Zulip Kevin Buzzard (Jul 21 2019 at 04:50):

If field_hom is not even defined, can there still be a field_hom namespace? Does that ever happen in mathlib?

view this post on Zulip Mario Carneiro (Jul 21 2019 at 04:50):

There can be a namespace

view this post on Zulip Mario Carneiro (Jul 21 2019 at 04:51):

Although you will miss out on dot notation

view this post on Zulip Kevin Buzzard (Jul 21 2019 at 04:52):

but theorems which are specific for fields, such as injectivity of the underlying map, naturally live there I think...oh, I see your point.

view this post on Zulip Kevin Buzzard (Jul 21 2019 at 04:53):

Is ->*+ horrible notation for a ring hom?

view this post on Zulip Mario Carneiro (Jul 21 2019 at 04:54):

lgtm

view this post on Zulip Kevin Buzzard (Jul 21 2019 at 04:54):

I want a LaTeX right-arrow with a + and a * floating over it when we're doing the controlled natural language thing; this notation is just a temporary thing

view this post on Zulip Mario Carneiro (Jul 21 2019 at 04:56):

You don't have to convince me, I find this kind of notation more palatable than random selections from the unicode arrow palette

view this post on Zulip Kevin Buzzard (Jul 21 2019 at 04:56):

@Kenny Lau what is the categorification of subring R?

view this post on Zulip Kenny Lau (Jul 21 2019 at 04:56):

mathematically?

view this post on Zulip Kevin Buzzard (Jul 21 2019 at 04:57):

Is it ring_hom A R or injective_ring_hom A R?

view this post on Zulip Kevin Buzzard (Jul 21 2019 at 04:57):

Is the question mathematically meaningful?

view this post on Zulip Kenny Lau (Jul 21 2019 at 04:57):

https://ncatlab.org/nlab/show/subobject

view this post on Zulip Kenny Lau (Jul 21 2019 at 04:57):

it's an isomorphism class of monomorphisms

view this post on Zulip Kevin Buzzard (Jul 21 2019 at 04:57):

Thanks.

view this post on Zulip Kevin Buzzard (Jul 21 2019 at 05:03):

So I think you're saying it's injective_ring_hom.

view this post on Zulip Kevin Buzzard (Jul 21 2019 at 05:04):

injective is a predicate on ring_hom.

view this post on Zulip Kevin Buzzard (Jul 21 2019 at 05:04):

which implies monic

view this post on Zulip Kevin Buzzard (Jul 21 2019 at 05:05):

Is this something to do with topologies on categories?

view this post on Zulip Kevin Buzzard (Jul 21 2019 at 05:07):

These categories -- lattices -- are the best categories in Lean. Do we have topologies on these categories?

view this post on Zulip Kevin Buzzard (Jul 21 2019 at 05:23):

structure ring_equiv (R S : Type) [ring R] [ring S] extends (R  S), (R →+* S)

view this post on Zulip Kevin Buzzard (Jul 21 2019 at 05:24):

end of definition

view this post on Zulip Kenny Lau (Jul 21 2019 at 05:41):

These categories -- lattices -- are the best categories in Lean. Do we have topologies on these categories?

we have... Groethendieck topologies

view this post on Zulip Kevin Buzzard (Jul 21 2019 at 06:47):

Is monic an example?

view this post on Zulip Kenny Lau (Jul 21 2019 at 06:50):

of what?

view this post on Zulip Kevin Buzzard (Jul 21 2019 at 06:58):

Something that satisfies the axioms for the admissible morphisms in a grothendieck topology

view this post on Zulip Kenny Lau (Jul 21 2019 at 07:01):

grothendieck topology needs admissible families of morphisms right

view this post on Zulip Kenny Lau (Jul 21 2019 at 07:01):

I can say that { A_i -> A } is admissible if the images generate the whole ring

view this post on Zulip Scott Morrison (Jul 21 2019 at 08:14):

abbreviation ring_equiv (R S : Type) [ring R] [ring S] := Ring.of R ≅ Ring.of S

view this post on Zulip Yury G. Kudryashov (Jul 21 2019 at 09:10):

@Scott Morrison The definition with has two drawbacks.
1. It only works for R and S in the same universe.
2. It's harder to define elements of this type. Currently, ≃* etc ask for a proof of to_fun being a hom, and automatically deduce that inv is a hom.

view this post on Zulip Kevin Buzzard (Jul 21 2019 at 12:10):

2 can be solved with a constructor. 1 I personally don't care about because I am a mathematician

view this post on Zulip Kevin Buzzard (Jul 21 2019 at 15:43):

Can we use function composition notation with bundled homs? If f : thing_hom A B and g : thing_hom B C then can we have f \circ g : thing_hom A C or whichever way round you want it? Does one just overload notation in this situation?

view this post on Zulip Yury G. Kudryashov (Jul 21 2019 at 18:42):

Possibly, we can have something like has_comp and use it.

view this post on Zulip Yury G. Kudryashov (Jul 21 2019 at 18:43):

Though it means overriding notation from core.

view this post on Zulip Yury G. Kudryashov (Jul 21 2019 at 18:44):

(of course, we can use some other symbol)

view this post on Zulip Scott Morrison (Jul 21 2019 at 20:13):

... Kevin, is bring able to talk about things in different universes so important to you that you're willing to give up the completely uniform notation for morphisms, composition, isomorphism, tensor product, etc, notation that the category theory API provides?

view this post on Zulip Kevin Buzzard (Jul 21 2019 at 21:04):

I know I know, but the category theory API bundles objects which makes it scary. I don't know how to glue sheaves using the category theory version of sheaves.

view this post on Zulip Kevin Buzzard (Jul 28 2019 at 18:42):

linear_equiv is defined with the old structure command, and mul_equiv with the new one. In practice this means that mul_equiv just has a field to_equiv and then all the equiv stuff like left_inv comes off that:

import linear_algebra.basic

#print linear_equiv -- long
#print mul_equiv -- short

#check linear_equiv.left_inv -- works
#check mul_equiv.left_inv -- fails

Which is best?

view this post on Zulip Chris Hughes (Jul 28 2019 at 19:51):

Old structures are the best.

view this post on Zulip Andrew Ashworth (Jul 28 2019 at 19:51):

So the disadvantage with the new structure command is that if you want to use properties of equiv, you have to explicitly write to_equiv. The advantage of new structures is that they are faster.

view this post on Zulip Andrew Ashworth (Jul 28 2019 at 19:53):

My rule of thumb is: use old structures if the thing you are describing is a genuine mathematical object. Use a new structure if it's just a universal property.

view this post on Zulip Kevin Buzzard (Jul 28 2019 at 19:56):

So all the structures we built in the perfectoid project -- for example adic spaces -- should all be using the old structure command?

view this post on Zulip Kevin Buzzard (Jul 28 2019 at 19:57):

@Chris Hughes it's about time we started calling them "good old structures" and "the good old structure command".

view this post on Zulip Andrew Ashworth (Jul 28 2019 at 19:57):

well, they're equivalent, in a sense, so no need to rewrite things that don't need to be rewritten

view this post on Zulip Andrew Ashworth (Jul 28 2019 at 19:57):

in fact, if you've already done it using new structures

view this post on Zulip Andrew Ashworth (Jul 28 2019 at 19:57):

you should keep them that way. after all, they are faster

view this post on Zulip Andrew Ashworth (Jul 28 2019 at 20:01):

maybe a better rule of thumb is: use a new structure, unless you get annoyed with always having to write to_equiv

view this post on Zulip Andrew Ashworth (Jul 28 2019 at 20:03):

the most important difference is new structures can't have duplicate fields

view this post on Zulip Chris Hughes (Jul 28 2019 at 20:05):

It's just a pain to use the constructor for new structures.

view this post on Zulip Andrew Ashworth (Jul 28 2019 at 20:06):

yes, in the original description of new structures, Leo assumed a bunch of the tactics would be updated to transparently handle it all. Well, it didn't

view this post on Zulip Kevin Buzzard (Jul 28 2019 at 20:07):

We never really ran into these issues as far as I remember -- our main goal was a definition, and our structures just got bigger and bigger but we were lucky not to ever run into duplicate substructures.

view this post on Zulip Kevin Buzzard (Jul 28 2019 at 20:07):

The tactics didn't get updated, or they couldn't be updated?

view this post on Zulip Andrew Ashworth (Jul 28 2019 at 20:07):

didn't get updated

view this post on Zulip Andrew Ashworth (Jul 28 2019 at 20:09):

I guess also since we have no idea what's happening in Lean 4, maybe prefer and start with new structures and hope they are easier to work with whenever the new version gets released

view this post on Zulip Andrew Ashworth (Jul 28 2019 at 20:10):

ahh, so you see, in my last three paras I've given completely contradictory advise

view this post on Zulip Andrew Ashworth (Jul 28 2019 at 20:11):

I suppose I don't know which one to prefer either :)

view this post on Zulip Kevin Buzzard (Jul 29 2019 at 15:46):

Here's a question about mul_equivs. I really don't know how to set these up. So far I have gone for the old structure command, extending equiv and adding a field map_mul. The problem is with proving things like symmetry. I have goals like

h.to_fun ((equiv.symm (to_equiv h)).to_fun (n₁ * n₂)) =
    h.to_fun ((equiv.symm (to_equiv h)).to_fun n₁ * (equiv.symm (to_equiv h)).to_fun n₂)

which I really just want to put into a canonical form and then rewrite/simp to death. But the problem is that the canonical form of h.inv_fun seems to be h.symm when h is an equiv, and if I define symm on mul_equiv then I have to reprove stuff like symm_apply_apply in this situation.

view this post on Zulip Kenny Lau (Jul 29 2019 at 15:48):

yeah but the proof is just equiv.symm_apply_apply

view this post on Zulip Kevin Buzzard (Jul 29 2019 at 15:48):

but I can't rewrite it

view this post on Zulip Kevin Buzzard (Jul 29 2019 at 15:49):

In fact my first question is what the canonical notation for the inverse bijection should be with h : mul_equiv G H

view this post on Zulip Chris Hughes (Jul 29 2019 at 15:51):

Prove that f.symm.to_equiv = f.to_equiv.symm and make it simp

view this post on Zulip Kevin Buzzard (Jul 29 2019 at 15:51):

I think my issue is that I am in the middle of defining mul_equiv.symm and I am complaining about not being able to use the canonical notation h.symm when stating some intermediate result, but this is spurious because h.symm is in the process of being defined.

view this post on Zulip Yury G. Kudryashov (Aug 09 2019 at 18:40):

Hi, I was away for some time. It seems that monoid_hom and add_monoid_hom are already bundled. I have a few questions about the implementation:
1. Why do we repeat all the proofs instead of using to_additive? My guess is “to provide docstrings” but we can use tactic.add_doc_string. Actually, the new docstring can be turned into the second optional argument to to_additive.
2. I see that M, N, G, H is used for monoids/groups. Doesn't it break the naming conventions? I'm trying to understand how strict is the style guide w.r.t. naming convention.
3. If I want to migrate, say, polynomial.C to monoid_hom, the definition will look like def C {α} ... : α →* polynomial α, and C (1 : α) fails to coerce C to a function. It works, if I make α a mandatory argument but this is not convenient.

view this post on Zulip Kevin Buzzard (Aug 09 2019 at 18:43):

1. because I only really worked out the full power of to_additive today (see a thread in #general).
2. Yes it breaks the naming conventions. Computer scientists get a lot of things right about names, but I believe that one of very few exceptions is here. If a computer scientist wants to a call a group alpha and a normal subgroup beta and then some auxiliary set gamma then that's fine by me, but if we call the group G and the normal subgroup N and the auxiliary set S then it is much easier to see at a glance what is happening, especially if variables are being used and the definitions of alpha and beta are 150 lines up.
3. Probably @Chris Hughes will have something to say on the matter.

view this post on Zulip Kevin Buzzard (Aug 09 2019 at 18:44):

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/to_additive.20and.20tags

view this post on Zulip Kevin Buzzard (Aug 09 2019 at 18:45):

See https://github.com/leanprover-community/mathlib/blob/659533e1dc63074d3386ffb8b2fbed50151dd34c/src/group_theory/submonoid.lean#L344 for the kind of code I am writing now. I think this is better -- I repeat almost nothing.

view this post on Zulip Yury G. Kudryashov (Aug 09 2019 at 18:48):

@Kevin Buzzard Thanks for explanations. I'd like to help with migrating to bundled hom. What can I work on to avoid duplication of effort?

view this post on Zulip Kevin Buzzard (Aug 09 2019 at 18:50):

You would be more than welcome to help @Amelia Livingston and me with all the to_additive stuff. As you can see we got up to line 569. Amelia also refactored localisation.lean in that branch, to see how things look with the changes, and they seemed fine. We did not think about polynomials though.

view this post on Zulip Yury G. Kudryashov (Aug 09 2019 at 18:51):

E.g., I can rewrite algebra/group/hom using to_additive. Is it OK?

view this post on Zulip Kevin Buzzard (Aug 09 2019 at 18:51):

Here's a message I sent Amelia earlier today:

So what I currently believe is this. Say you have made 10 definitions and proved 20 lemmas in the namespace submonoid and you want to get additive versions in add_submonoid. The one thing which can almost always be avoided is having to write out a proof twice, once in the multiplicative and once in the additive case.

The best possible scenario is when defining a lemma; in this case you can use @[to_additive add_submonoid.foo] and that might be almost all you need to do; this will hopefully generate the proof automatically. Unfortunately it doesn't generate the docstring automatically and you have to add it with this run_cmd which which I don't really understand. There are plenty of examples in the commit I pushed today (all in this bundled_submonoids branch of mathlib).

More complicated is a definition. I have been writing definition submonoid.foo ..., getting it working, and then writing #print prefix submonoid.foo (note that you need submonoid even if you're in the submonoid namespace). You then see submonoid.foo but also perhaps submonoid.foo.match_1 or submonoid.foo.equations_eqn3 or something. For structures you see loads of things. After the definition you can write to_additive [add_submonoid.foo.proof_3] submonoid.foo.proof_3 and this needs to be done for everything in the output. However it all has to be done in the right order. If you get red squiggles under a to_additive then look at the error, see if it mentions add_submonoid.foo.equation_2 and then move the corresponding to_additive line above the line with the error. In all cases I got this to work. And don't forget the docstring. Note that in one case the errors I got were errors involving functions which I had not defined -- other people had missed out the to_additive tags on other functions, so I had to add those in (they should probably be moved to the correct part of mathlib at some point).

Even more complicated is a structure. I have been defining the additive ones by hand. And there are some lemmas or definitions which don't port, for example those involving powers x^n turn into ones involving smultiples n \bub x and because the order got switched to_additive sometimes can't handle it. In these cases I leave the submonoid namespace immediately, define the additive one by hand (i.e. write the same code again), do all the to_additive tags and the docstring, and then go back into the submonoid namespace. You then have to re-input all the variables which you had open in that namespace. Variables outside a namespace survive inside it, but variables inside a namespace die once the namespace is closed, even if you go back in.

view this post on Zulip Kevin Buzzard (Aug 09 2019 at 18:53):

Everything we have done is in the bundled_submonoids branch of mathlib and our plan was to finish submonoid.lean and then make a PR.

view this post on Zulip Kevin Buzzard (Aug 09 2019 at 18:55):

We didn't touch the hom file so it will be OK.

view this post on Zulip Yury G. Kudryashov (Aug 09 2019 at 18:55):

Probably, one of us should learn more about Lean tactic language, and let to_additive handle mydef._proof_n and all those mystruct.cases_on etc.
Another idea is to have @[bundled_hom] user attr that defines has_coe_to_fun and restates all axioms using coe instead of f.to_fun.

view this post on Zulip Yury G. Kudryashov (Aug 09 2019 at 18:57):

OK, then I'll go through hom, then I'll try to migrate concrete categories (Mon etc.) to bundled homs.

view this post on Zulip Kevin Buzzard (Aug 09 2019 at 18:58):

Bundling group and monoid and ring stuff (subthings, homs and isomorphisms) is just a one-off job which needs to be done once. The reason I am motivated to do it now is because I think it makes it easier for mathematicians -- but I am not sure about this. Other people also believe it's best to do things like bundle homs and subobjects, for other reasons. What became clear to me was that the task of actually removing unbundled homs and replacing them with bundled ones is a vast task, because is_submonoid appears 200 times in the library and one of the appearances is in the definition of is_subgroup which appears 200 more times, and then is_subring uses both of these etc etc.

view this post on Zulip Kevin Buzzard (Aug 09 2019 at 19:01):

Furthermore, the switch would be one huge PR which would take a very long time to write and would have to constantly be playing catch-up with the library. This sounded very unappealing. So my plan is to bundle stuff, leave the unbundled stuff in for now (but mention that it is deprecated in docstrings) and then start changing leaf nodes to see if things work. Amelia changed localisation.lean and it worked fine. But changing stuff deeper in mathlib is painful. So our plan is to work from the outside in. The disadvantage of our approach is that ultimately it will in some sense be more work, probably. The advantage is that we can access bundled homs immediately, which is what I wanted really.

view this post on Zulip Patrick Massot (Aug 09 2019 at 19:54):

I'm very worried about this thread. For the sensitivity conjecture project, I worked seriously with linear maps for the first time. They are bundled, and it simply does not work. The coercion to function works completely randomly, and there are instance search timeout all over the place. It's extremely time-consuming and frustrating to fight that

view this post on Zulip Mario Carneiro (Aug 09 2019 at 19:57):

Bundled maps have much lower pressure on the typeclass system, because you aren't inferring the fact that the function is a hom anymore

view this post on Zulip Mario Carneiro (Aug 09 2019 at 19:58):

I can believe that the coercion is problematic sometimes though. The alternative is to write .to_fun

view this post on Zulip Patrick Massot (Aug 09 2019 at 19:58):

but coercions are part of the type class system

view this post on Zulip Patrick Massot (Aug 09 2019 at 19:58):

The alternative doesn't work, because lemmas are stated without .to_fun

view this post on Zulip Mario Carneiro (Aug 09 2019 at 19:59):

Personally, I would happily live with to_fun everywhere. I put the coercions in because you guys are always going on about nice looking notation and lean 3 provides few other opportunities for this kind of thing

view this post on Zulip Patrick Massot (Aug 09 2019 at 20:00):

This is really sad

view this post on Zulip Yury G. Kudryashov (Aug 09 2019 at 20:00):

/me prefers Python-style obj.__call__ convention over typeclass resolution

view this post on Zulip Mario Carneiro (Aug 09 2019 at 20:01):

I agree completely (to both statements)

view this post on Zulip Yury G. Kudryashov (Aug 09 2019 at 20:09):

@Mario Carneiro What's are the other opportunities in Lean 3 for this kind of thing?

view this post on Zulip Mario Carneiro (Aug 09 2019 at 20:10):

for zero-notation functions, nothing, but if you are willing to accept a character or two you can use a notation

view this post on Zulip Yury G. Kudryashov (Aug 09 2019 at 20:12):

BTW, what's wrong with dropping has_coe_to_fun and using f.1?

view this post on Zulip Yury G. Kudryashov (Aug 09 2019 at 20:13):

Forgot to tag @Kevin Buzzard

view this post on Zulip Patrick Massot (Aug 09 2019 at 20:13):

This is really not how we think about maps

view this post on Zulip Yury G. Kudryashov (Aug 09 2019 at 20:22):

@Patrick Massot I see the following options:
1. the old way; pros: already implemented; easy to say that the same map can be is_mul_hom or is_monoid_hom under different assumptions; cons: need to find is_*_hom instances here and there; what else?
2. bundled homs, implicit coercion; pros: map_mul and map_one are right there; M →* N is exactly Mon.of M \--> Mon.of N (not yet); cons: need to find has_coe_to_fun every time; sometimes this coercion fails;
3. bundled homs, f.1; pros: see 2 + no class instance resolution at all; cons: unnatural notation.
What do I miss?

view this post on Zulip Patrick Massot (Aug 09 2019 at 20:55):

I don't see what I could add here. Type class inference doesn't work in Lean 3, and it doesn't provide error messages

view this post on Zulip Patrick Massot (Aug 09 2019 at 21:02):

2. Yes it breaks the naming conventions. Computer scientists get a lot of things right about names, but I believe that one of very few exceptions is here. If a computer scientist wants to a call a group alpha and a normal subgroup beta and then some auxiliary set gamma then that's fine by me, but if we call the group G and the normal subgroup N and the auxiliary set S then it is much easier to see at a glance what is happening, especially if variables are being used and the definitions of alpha and beta are 150 lines up.

I also wanted to comment on that. The linear algebra library uses the random greek letter convention, and it's really a nightmare. They are lots of type involved, and not knowing which one is meant to be a base field, an indexing type or a vector space is really awful. They are tons of lemmas whose statements are very hard to parse, and would be very easy with reasonable type naming conventions.

view this post on Zulip Yury G. Kudryashov (Aug 09 2019 at 21:10):

Then maybe docs/contribute/naming.md should be adjusted.

view this post on Zulip Yury G. Kudryashov (Aug 09 2019 at 21:10):

With some sensible theory-specific naming conventions.

view this post on Zulip Patrick Massot (Aug 09 2019 at 21:10):

I'd love that

view this post on Zulip Kevin Buzzard (Aug 09 2019 at 22:10):

+1 from me.

view this post on Zulip Kevin Buzzard (Aug 09 2019 at 22:12):

@Yury G. Kudryashov the reason I'm bundling is because the community seems to think it's the best idea. To a certain extent it might just be about experimenting to find out what works best. I have seen coercions fail before and you can just write (f : G -> H) to make them happen; I quite like that notation

view this post on Zulip Kevin Buzzard (Aug 09 2019 at 23:03):

The one place where I feel that the alpha beta notation is natural is when dealing with types that really are that -- just types. For example equiv alpha beta seems fine to me because for all I know this is what computer scientists really call types. But types which are playing a mathematical role such as groups have got such a history of notation behind them and it's used to guide readers, and I don't see the point of throwing it away. Sure some people use kk for a number field and some use KK, but nobody uses α\alpha. The number field library that will one day be written will need to choose a notation, but it should, in my opinion, use one which is already in use.

view this post on Zulip Andrew Ashworth (Aug 10 2019 at 00:50):

morally speaking isn't it [G : group alpha]?

view this post on Zulip Scott Morrison (Aug 10 2019 at 01:07):

It is really unfortunate the coercions to function types barely work. I think this is the main pain point with bundling.

view this post on Zulip Yury G. Kudryashov (Aug 10 2019 at 08:44):

@Andrew Ashworth Groups are not bundled, so after [G : group α] you still have to say x : α, and this is not very readable, especially if you have, e.g., a group acting on a space.

view this post on Zulip Kevin Buzzard (Aug 10 2019 at 09:12):

Mathematicians read x : α as xαx\in\alpha and they are far more used to gGg\in G. In fact this is in some sense exactly the point -- if I see gGg\in G in the middle of a maths paper without any context then I would be likely to guess that GG was a group and gg an element. If I see x : α in a library file then I have no clue.

view this post on Zulip Yury G. Kudryashov (Aug 15 2019 at 17:48):

@Kevin Buzzard I rewrote to_additive to automatically take care of many things. I'll try to PR it tonight or tomorrow. Current state (no docs, WIP) is available at https://github.com/urkud/mathlib/blob/to_additive/src/algebra/group/to_additive.lean

view this post on Zulip Yury G. Kudryashov (Aug 15 2019 at 17:51):

Namely, (1) it automatically adds to_additive attribute to structure fields; (2) it looks for prefixes in dict instead of full names; (3) it automatically transfers decl._proof_1, decl._match_1 etc . With (2), we don't need to have attribute [to_additive add_monoid_hom.cases_on] monoid_hom.cases_on etc.

view this post on Zulip Kevin Buzzard (Aug 15 2019 at 17:52):

I'm away from Lean until Monday (camping)

view this post on Zulip Kevin Buzzard (Aug 15 2019 at 17:52):

Feel free to take a look at the bundled submonoids branch

view this post on Zulip Yury G. Kudryashov (Aug 15 2019 at 17:53):

@Kevin Buzzard Good luck with camping!

view this post on Zulip Kevin Buzzard (Aug 15 2019 at 17:53):

@Amelia Livingston did you push everything you have? The submonoid.lean file is half toadditiveised

view this post on Zulip Amelia Livingston (Aug 15 2019 at 17:55):

Not yet, I'm tidying things up a bit but I will push today. I've not toadditiveised anything yet.

view this post on Zulip Yury G. Kudryashov (Aug 15 2019 at 18:09):

@Amelia Livingston It should be easier to use @[to_additive] with my changes, so you should probably postpone to_additiveisation for a day or two. I'll try to tidy my patch tonight.

view this post on Zulip Amelia Livingston (Aug 15 2019 at 18:10):

Okay. Thank you for working on it!

view this post on Zulip Yury G. Kudryashov (Aug 16 2019 at 14:49):

@Amelia Livingston I pushed a new version of @[to_additive] to the to_additive branch of urkud/mathlib.
It automates:

  • mapping of structure fields;
  • mapping of hidden defs like name._proof_1, name._match_1;
  • mapping of projections like semigroup.to_has_mul (relies on @[ancestor] attributes);
  • mapping of name.cases_on by mapping prefixes instead of names.

view this post on Zulip Yury G. Kudryashov (Aug 16 2019 at 15:03):

Other items I want to add before making a PR:

  • take docstring as an optional argument; alternative is to use run_cmd add_doc_string after each definition;
  • autogenerate target namespace using to_additive_attr.get_param src.get_prefix; ask for the suffix only;
  • make “target name” argument optional;
    • simple: use the same suffix as in the source name, e.g. monoid_hom.compadd_monoid_hom.comp;
    • advanced: parse suffix replacing mul→add, one→zero, prod→sum (what else?).
  • automatically create target.equations._eqn_1.

view this post on Zulip Yury G. Kudryashov (Aug 16 2019 at 15:16):

@Mario Carneiro what is responsible for creating my_name.equations._eqn_1? Is it intentional that this thing is called after normal defs but not after add_decls?

view this post on Zulip Floris van Doorn (Aug 16 2019 at 15:35):

I think it's the equation compiler who adds those equalities. add_decl (and its relatives, like add_inductive) indeed doesn't have the same side effects (like creating auxiliary definitions) as adding a declaration normally. It's probably useful to have both the version with and without side-effects, and it was suggested previously to expose versions with side effects in the community fork of Lean.

view this post on Zulip Yury G. Kudryashov (Aug 16 2019 at 15:51):

@Floris van Doorn Then I'll postpone automatic handling of equations till we have add_decl_with_side_effects.

view this post on Zulip Mario Carneiro (Aug 16 2019 at 16:58):

it's already available in community lean

view this post on Zulip Yury G. Kudryashov (Aug 18 2019 at 15:42):

See https://github.com/leanprover-community/mathlib/pull/1345 for the new to_additive. It seems that I've broken compilation in one of the last commits. I'll fix it tonight.


Last updated: May 11 2021 at 15:12 UTC