Inductive type port maybe needs to add the type parameter

Stream: mathlib4

[Lars Ericson]

Quaternions are expressed in Lean 3 as

@[derive decidable_eq]
inductive quaternion_group (n : ℕ) : Type
| a : zmod (2 * n) → quaternion_group
| xa : zmod (2 * n) → quaternion_group

In Lean 4 this gets translated as

inductive QuaternionGroup (n : ℕ) : Type
  | a : ZMod (2 * n) → QuaternionGroup
  | xa : ZMod (2 * n) → QuaternionGroup
  deriving DecidableEq

Without specifying an argument, the QuaternionGroup references give Infoview error

type expected, got
  (QuaternionGroup : ℕ → Type)

Adding an n to each reference solves the problem:

inductive QuaternionGroup (n : ℕ) : Type
  | a : ZMod (2 * n) → QuaternionGroup n
  | xa : ZMod (2 * n) → QuaternionGroup n
  deriving DecidableEq

Perhaps the mathport script should add type parameters to inductive type references since they will be required.

[Damiano Testa]

This could probably be automated, but I think that it is not a priority to include this feature, given that

• approximately 3/4 of the porting is done,
• this happens fewer than 100 times (a rough estimate),
• many of these cases have already been ported.

[Damiano Testa]

I believe that the issue is due to the fact that in Lean 3, you could only use as match arguments the ones that happened after the "colon", the ones before were "fixed" and automatically inserted in the recursive calls.

In Lean 4, you have the flexibility of modifying the arguments in recursive calls, even if they appear before the "colon" and this is why you get the errors you are seeing.

[Damiano Testa]

E.g. in the example above, in Lean 3, → quaternion_group really means → quaternion_group n and you cannot change n to something else. In Lean 4 you can.

[Damiano Testa]

Also, congratulations on finding a file that may not be already PRed/ported! Hopefully there will not be many issues.

If you want to contribute to the port, I encourage you to create a WIP PR right away, so that others will know that someone is working on this file.

[Julian Külshammer]

It is the generalised quaternion groups, not the quaternions. It is probably a good beginner file as it is very close to the corresponding file for dihedral groups, which was recently ported, so you can check the solutions there.

[Lars Ericson]

@Damiano Testa I like to wait on the WIP PR for two reasons:

• I don't have confidence that I will get through the whole file and I don't want to hold it up
• Every file I've discussed so far has been picked up and solved overnight by someone in the room, so I am feeling productive as a cheerleader if nothing else.

I will put in a PR for any file I can solve completely that no one else has grabbed in the meantime. I learn a little bit of Lean 4 with each one, and there are about 700 to go, so there is still plenty to do.

[Yaël Dillies]

Yeah but that's just not how it works:

• You don't need to get through it all. Just tag your PR help-wanted and people will help.
• Probably nobody has read the threads where you were solving problems in porting files, because at no point the process says "Check that people work on this file on a random Zulip thread". On the other hand, if you open a porting PR, it's indicated on the port dashboard. So your work so far has been completely uneffective, even from a cheerleading standpoint.

Please just open a porting PR.