rw seeing through type synonym?

Stream: mathlib4

[Kevin Buzzard]

Yes this is very surprising to me. In Lean 3 the rewrite would fail. Here are examples on mathlib3 and mathlib4 master:

-- lean 3
import algebra.group.opposite
import group_theory.group_action.defs

variable (α : Type)

instance has_mul.to_has_opposite_smul [has_mul α] : has_smul αᵐᵒᵖ α :=
  ⟨fun c x, x * c.unop⟩

theorem MulOpposite.smul_eq_mul_unop [has_mul α] {a : αᵐᵒᵖ} {a' : α} : a • a' = a' * a.unop :=
begin
  -- rw smul_eq_mul, -- fails
  -- rw @smul_eq_mul αᵐᵒᵖ -- fails
  sorry
end

-- lean 4
import Mathlib.Algebra.Group.Opposite
import Mathlib.GroupTheory.GroupAction.Defs

instance Mul.toHasOppositeSmul [Mul α] : SMul αᵐᵒᵖ α :=
  ⟨fun c x => x * c.unop⟩

theorem MulOpposite.smul_eq_mul_unop [Mul α] {a : αᵐᵒᵖ} {a' : α} : a • a' = a' * a.unop := by
  -- the • in the goal is `@HSMul.hSMul αᵐᵒᵖ α α instHSMul a a' : α`
  rw [@smul_eq_mul αᵐᵒᵖ] -- works! Even though `a'` does not have type `αᵐᵒᵖ`.
  rfl

Is this a change in the behaviour of rw?

[Kevin Buzzard]

You should maybe change the title of the thread to "rw seeing through type synonym?" because this is kind of weird.

[Yury G. Kudryashov]

Should we use a structure instead of a type synonym in Lean 4?

[Yury G. Kudryashov]

With the new structure eta(?) rfl, we'll have both op_unop and unop_op as rfl lemmas.

[Kevin Buzzard]

Here's a mathlib-free MWE: all the declarations are from mathlib.

-- lean 4

class SMul (M : Type _) (α : Type _) where
  smul : M → α → α

class HSMul (α : Type u) (β : Type v) (γ : outParam (Type w)) where
  hSMul : α → β → γ

infixr:73 " • " => HSMul.hSMul

instance instHSMul [SMul α β] : HSMul α β β where
  hSMul := SMul.smul

-- type synonym
def MulOpposite (α : Type u) : Type u :=
  α

postfix:max "ᵐᵒᵖ" => MulOpposite

namespace MulOpposite

def unop : αᵐᵒᵖ → α :=
  id

def op : α → αᵐᵒᵖ :=
  id

instance [Mul α] : Mul αᵐᵒᵖ where mul x y := op (unop y * unop x)

end MulOpposite

instance (priority := 910) Mul.toSMul (α : Type _) [Mul α] : SMul α α :=
  ⟨(· * ·)⟩

@[simp]
theorem smul_eq_mul (α : Type _) [Mul α] {a a' : α} : a • a' = a * a' := rfl

instance Mul.toHasOppositeSmul [Mul α] : SMul αᵐᵒᵖ α :=
  ⟨fun c x => x * c.unop⟩

@[simp]
theorem MulOpposite.smul_eq_mul_unop [Mul α] {a : αᵐᵒᵖ} {a' : α} : a • a' = a' * a.unop := by
  rw [@smul_eq_mul αᵐᵒᵖ] -- wouldn't work in Lean 3
  rfl

/- The `simpNF` linter reports:
SOME SIMP LEMMAS ARE NOT IN SIMP-NORMAL FORM.
see note [simp-normal form] for tips how to debug this.
https://leanprover-community.github.io/mathlib_docs/notes.html#simp-normal%20form -/
#check @MulOpposite.smul_eq_mul_unop /- Left-hand side simplifies from
  a • a'
to
  a * a'
using
  simp only [smul_eq_mul]
Try to change the left-hand side to the simplified term!
 -/

[Kevin Buzzard]

Type synonyms like opposite were a big cause of weird leakage in Lean 3, which led to weird goals (which were super-hard to debug before widgets). More recently we learnt how to tame them in mathlib3, by making the API and then afterwards marking the declarations irreducible. This approach is no longer possible in Lean 4 because you cannot change the reducibility of a declaraction once it's been made (the autoporter rather annoyingly just ignores changes in transparency without flagging them as "something which is no longer possible just got skipped").

This is also a very weird goal above: it looks to me like we're being type-careful in the declarations, but the simplifier is breaking the abstraction. Here a * a' has a term of type α but the multiplication is the mul on αᵐᵒᵖ so a' has somehow been coerced to αᵐᵒᵖ. The fact that it's happening, and the fact that we also have this issue about being unable to change the transparency of a declaration after it's been made, make me tentatively agree with Yury that we should perhaps consider using a structure and hoping that eta for structures will mean that the pain incurred is not too bad. It would be great to get some expert opinion on this because this is a big call. @Gabriel Ebner @Mario Carneiro @Scott Morrison ?

[Kevin Buzzard]

I guess Gabriel is probably for this, judging by https://github.com/leanprover/lean4/issues/777

[Gabriel Ebner]

Yes, I think it is the right choice to turn most of these wrappers into structures, precisely because it's way to easy to break the abstraction otherwise.

[Jireh Loreaux]

TODO: This advice needs to be added to the porting wiki.

[Yaël Dillies]

This is going to be a lot of API writing :sad: but I'm with you on this.

[Yury G. Kudryashov]

Some of these wrappers (e.g., mul_opposite) are supposed to be irreducible. But some wrappers (e.g., order_dual) are often used to quickly get the order-dual lemma by forcing defeq.

[Yury G. Kudryashov]

additive is used in both ways.

[Yury G. Kudryashov]

Do you suggest that we completely move away from the order_dual-style?

[Patrick Massot]

Maybe we need a tactic supporting the proofs where we want to abuse order_dual.

[Yaël Dillies]

Yaël Dillies said:

My dream is still for a to_additive-like tactic to handle them all.

More discussion above and below

[Gabriel Ebner]

Maybe it's worth looking at the (now rotten) #6045. Turning additive into a structure is not that painful. I don't think order_dual would be much worse.

[Yaël Dillies]

I mean, we would need to add a few thousands more lines of code :shrug:

[Yakov Pechersky]

I don't see why that's the case. The "tactic" here is defining the recursor (unary, binary, tritary). We're already often changing lemma names. Including an "order_dual.rec_2 <|" in various lines shouldn't be too bad.

[Yaël Dillies]

In the case where we make order_dual a structure without providing a to_dual attribute, I am firmly convinced we have to write about 10k more lines of code. In the case where we make order_dual a structure and provide a to_dual attribute, we might end up reducing the number of lines.

[Mario Carneiro]

I'm really not a fan of the to_additive proof method, that is, translating all the proofs from the bottom up. From a proof theory perspective this is very wasteful when you can just instantiate a structure and apply the old theorem, and from an automation perspective it's more brittle because you have to translate a bunch of internals, in addition to reading proofs out of the environment which is something we want to crack down on in the future

[Yaël Dillies]

I think order_dual is genuinely much worse than additive for two reasons:

• There's only one way of translating a multiplicative statement to an additive one (except a handful of edge cases), while there are 2^#types appearing in the statement ways of dualising.
• order_dual is used in a defeq-forcing manner much more pervasively than additive

[Yaël Dillies]

That's interesting, Mario. I always thought to_additive was the pinnacle of proof translation.

[Mario Carneiro]

From a UX standpoint to_additive is great, it's just the proof method that isn't great. I would rather have something like to_additive do its proof by translating the statement and using transfer theorems to turn everything into facts about additive of something and then applying the old theorem

[Mario Carneiro]

many of the proofs we're talking about are basically doing exactly that, but with defeq abuse in place of a transfer tactic

[Yaël Dillies]

Oh I understand now. Yeah, this would be the best of both worlds.

[Kevin Buzzard]

wooah I changed the definition of αᵐᵒᵖ from := α to a structure (i.e. I totally changed the definitions in the first few lines of Mathlib.Algebra.Opposites, and the entire file still compiled apart from one lemma which is arguably incorrect in mathlib3 anyway. See mathlib4#1036 . I'm going to bed now, if anyone wants to push this any further. I'm unlikely to look at this for around 24 hours because I have a very busy day at work tomorrow.

[Gabriel Ebner]

For types that were already irreducible in mathlib3, turning them into structures in Lean 4 shouldn't make much of a difference. Except for shenanigans like local attribute [semireducible] mul_opposite.

[Matej Penciak]

Yury G. Kudryashov said:

Some of these wrappers (e.g., mul_opposite) are supposed to be irreducible. But some wrappers (e.g., order_dual) are often used to quickly get the order-dual lemma by forcing defeq.

Is this what was causing the instance issues for mathlib4#1001? (thread here: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.231001.20failed.20to.20synthesize.20instance/near/315730442)

[Eric Wieser]

Yury G. Kudryashov said:

Some of these wrappers (e.g., mul_opposite) are supposed to be irreducible. But some wrappers (e.g., order_dual) are often used to quickly get the order-dual lemma by forcing defeq.

mul_opposite is irreducible but add_opposite isn't!

[Eric Wieser]

Note that there are places in mathlib that take advantage of the fact that (pseudocode)additive (quotient_group X) = quotient_add_group (multiplicative X) to transfer results; in these places, we have to temporarily make mul_opposite semireducible again. We won't have that option if we make things a structure

[Eric Wieser]

Kevin Buzzard said:

and the entire file still compiled

Of course, the real test is whether the entire set of yet-to-be-ported files still compile...

[Reid Barton]

There was some push a while ago to try to remove occurrences of local attribute [semireducible] from mathlib, right?

[Kevin Buzzard]

I can see that this might be a good idea in the sense that (a) it would in theory help with porting and (b) it would make a bunch of lemmas be moved to more appropriate places (assuming the mathlib3 philosophy is "start with it semireducible, prove stuff, make it irreducible, and don't fiddle with it any more"). As it happens I do now have 30 minutes more to work on this stuff so I'd like to temporarily claim it back.

[Kevin Buzzard]

https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/make.20.60MulOpposite.60.20a.20structure/near/316018381

[Floris van Doorn]

Mario Carneiro said:

From a UX standpoint to_additive is great, it's just the proof method that isn't great. I would rather have something like to_additive do its proof by translating the statement and using transfer theorems to turn everything into facts about additive of something and then applying the old theorem

I am also not happy with the current implementation of to_additive. The fact that we have to also translate all this internal stuff is definitely a bad sign.
However, your approach is only a partial fix, since proof terms can occur in a theorem statement. In that case, you will still have to translate proof terms (or at the very least a lemma name that is exactly that proof term)

[Yury G. Kudryashov]

Should I try to turn Multiplicative and Additive into structures (in mathlib 4, not in mathlib 3)?

[Kevin Buzzard]

I think so. They accepted my PR for MulOpposite because it seemed to be solving problems.

[Yury G. Kudryashov]

Currently, ofAdd etc are Equivs. If I define, e.g.,

structure Multiplicative (α : Type _) := ofAdd :: toAdd : α

then they're no longer Equivs. What should I do?

• Define as above, add Multiplicative.ofAddEquiv and Additive.ofMulEquiv?
• Define with some other names (e.g., mk and out) and add ofAdd and toAdd as Equivs?

[Yury G. Kudryashov]

I prefer ofAdd :: toAdd : α but it may make porting harder.

[Yaël Dillies]

I think it's fine to make them undecorated functions, because there are many bundlings they could be.

[Eric Wieser]

I'm worried we're setting ourselves up for trouble if we don't start by attempting to backport this first

[Yaël Dillies]

We can try to backport it, but I expect it be fine.

[Kevin Buzzard]

When I tried an experimental version of this I gave the unequiv constructor/eliminator primed names

[Yury G. Kudryashov]

I made mathlib4 compile with structures for Additive and Multiplicative. But this is not free.

[Yury G. Kudryashov]

We forced defeq here and there in mathlib3.

[Yury G. Kudryashov]

https://github.com/leanprover-community/mathlib4/pull/1213

[Yury G. Kudryashov]

I'll cherry-pick some changes that make sense any way to another branch.

[Kevin Buzzard]

Yes I tried this and it was much harder than MulOpposite

[Kevin Buzzard]

@Yury G. Kudryashov do you think this should be backported to mathlib3?

[Gabriel Ebner]

There's already a mathlib PR changing Additive/Multiplicative to structures. #6045 (slightly fermented)

[Yury G. Kudryashov]

I'm not sure whether it should be backported: some Lean 4 rfls are useful. But I can revive #6045 if needed.

[Kevin Buzzard]

I guess the argument against backporting is that the mathlib4 PR might be solving problems which weren't present in mathlib3.

[Scott Morrison]

What is happening, if anything with #1213? Can I close? Is there still desire to merge?

[Yury G. Kudryashov]

If mathlib can compile without it (which is true, as we see), then I have no reason to advocate for merging it. Unless someone else steps in, we should close this PR.

[Scott Morrison]

Closed.