FAQ on porting

Stream: mathlib4

[Riccardo Brasca]

I think we need to create a FAQ for the porting, listing all the small problems we get in porting a file and that are likely to bother someone else.

For example, in mathlib4#626, I noticed that (with the long line)

def CommMonoid [h : MulOneClass X]
    (distrib : ∀ a b c d, ((a * b) <m₁> c * d) = (a <m₁> c) * b <m₁> d) : CommMonoid X :=
  { h with mul := (· * ·), one := 1, mul_comm := (mul_comm h₁ MulOneClass.IsUnital distrib).comm, mul_assoc := (mul_assoc h₁ MulOneClass.IsUnital distrib).assoc }

works, but (just putting mul_assoc on a new line to make the linter happy)

def CommMonoid [h : MulOneClass X]
    (distrib : ∀ a b c d, ((a * b) <m₁> c * d) = (a <m₁> c) * b <m₁> d) : CommMonoid X :=
  { h with mul := (· * ·), one := 1, mul_comm := (mul_comm h₁ MulOneClass.IsUnital distrib).comm,
      mul_assoc := (mul_assoc h₁ MulOneClass.IsUnital distrib).assoc }

doesn't, and the error is not clear at all. Scott quickly find the solution (also the mul :=... has to be on a new line), but I am sure this is going to confuse someone else.

This is just an example, but it's worth to have a centralized place for questions like this one, rather than asking/searching on zulip each time.

[Scott Morrison]

@Riccardo Brasca, could you please include this in the #port-guide?

[Riccardo Brasca]

Ah yes, the paragraph "Some common fixes" is essentially what I wanted. Maybe we should move it to a separate wiki if it gets too big, but we will see. (I am updating it.)

Another problem I found is that instances for out_param now need to be out_param themselves. For example

class SubAdditiveHomClass (F : Type _) (α β : outParam (Type _)) [outParam (Add α)]
  [outParam (Add β)] [outParam (LE β)] extends ...

doesn't work if Add α is not an outParam (this is not the case in Lean3). If this is the correct way of fixing the problem I will also add it to the wiki.

[Moritz Doll]

Riccardo, I think I've mentioned that before: it would be great if everyone that encountered a non-trivial problem when porting files writes a short paragraph in the wiki on it got fixed (given that it might occur again).

[Scott Morrison]

I don't understand your outParam example. It sounds like something could be broken, so a MWE would be great.

[Riccardo Brasca]

That's exactly my point. These issues will pop out over and over, we really need a centralized place for them.

Let me write a mwe.

[Riccardo Brasca]

This

import Mathlib.Algebra.Group.Defs

class foo (F : outParam (Type _)) [Zero F] where
  bar : ∀ f : F, f = 0

gives the error "invalid class, parameter #2 depends on outParam, but it is not an outParam". This

import Mathlib.Algebra.Group.Defs

class foo (F : outParam (Type _)) [outParam (Zero F)] where
  bar : ∀ f : F, f = 0

is OK. In Lean3 it was not the case.

[Scott Morrison]

I feel like this is just Lean being unhelpful. Do you think you could come up with a MWE that doesn't have any imports, and then post an issue on the Lean 4 repo?

[Riccardo Brasca]

Let me try

[Riccardo Brasca]

That was easy.

class foo (F : Type) where
  foo : F

class foobar (F : outParam Type) [foo F] where
  bar : F

[Riccardo Brasca]

Voilà

[Anne Baanen]

This might be related to my PR lean#657 which changed some aspects of out_param handling in Lean 3

[Riccardo Brasca]

I am also adding the fact that include and omit are gone and that the corresponding lines can just be deleted.

[Riccardo Brasca]

Can someone else comment my issue? Leo is asking if we prefer to omit the outParam in instances. Personally I think it's really better, but maybe I am missing something.

[Winston Yin]

(deleted)

[Riccardo Brasca]

I wanted to remove the now unnecessary outParam, but if I remove any other outParam in #692 I get an error. I don't understand what's going on, the first outParam were removed without problems.

[Riccardo Brasca]

It's really strange, if I remove the second outParam in

/-- `NonArchimedeanHomClass F α β` states that `F` is a type of non-archimedean morphisms. -/
class NonArchimedeanHomClass (F : Type _) (α β : outParam (Type _)) [outParam (Add α)]
  [outParam (LinearOrder β)] extends FunLike F α fun _ => β where
  /-- the image of a sum is less or equal than the maximum of the images. -/
  map_add_le_max (f : F) : ∀ a b, f (a + b) ≤ max (f a) (f b)
#align nonarchimedean_hom_class NonArchimedeanHomClass

I get an error ("function expected at f term has type F") in

@[to_additive]
theorem le_map_mul_map_div [Group α] [CommSemigroup β] [LE β] [SubMultiplicativeHomClass F α β]
    (f : F) (a b : α) : f a ≤ f b * f (a / b) := by
  simpa only [mul_comm, div_mul_cancel'] using map_mul_le_mul f (a / b) b
#align le_map_mul_map_div le_map_mul_map_div

even if this theorem seems unrelated to NonArchimedeanHomClass.

[Winston Yin]

Recent commits to master seem to have broken some classes that use outParam. The following example would've worked before:

:working_on_it:

The outParams in ZeroHomClass should eventually (now?) be removed, but #synth still fails.

[Scott Morrison]

Where are you expecting the instance to come from? You need to define an instance ... : ZeroHomClass (ZeroHom M N) M N := ....

[Scott Morrison]

(Also, I think this is misuse of <| notation. It's very helpful if the closing parenthesis would be far off in the distance and hard to keep track of, but probably just confusing for short expressions.)

[Winston Yin]

Oops apologies let me fix the example

[Winston Yin]

Also, I think this is misuse of <| notation

I was hoping its awkwardness would remind me to revisit this once outParam works nicely :sweat_smile: