Typechecking integers with graded things

Stream: lean4

[Gareth Ma]

So I have some graded objects, say GradedPapers below:

structure GradedPapers (n : Int) where
  grade : Int

def GradedPapers.combine {n : Int} (a : GradedPapers n) (b : GradedPapers n) : GradedPapers n :=
  ⟨a.grade + b.grade⟩

def PaperA : GradedPapers 3 := ⟨10⟩
def PaperB : GradedPapers (2 + 1) := ⟨10⟩
#check PaperA.combine PaperB

instance GradedPapers.instAdd {n : Int} : Add (GradedPapers n) := ⟨combine⟩

#check PaperA + PaperB
#check (PaperA + PaperB : GradedPapers 3)

def PaperB' : GradedPapers 3 := PaperB
def PaperAB : GradedPapers (1 + 1 + 1) := PaperA + PaperB'

The first check succeeds, while the last two fails, and the final definition succeeds (but not with PaperB). I kind of understand why, but also not really, so I have some questions/clarifications:

1. Since the first check succeeds, I believe 3 and 2 + 1 are definitionally equal in the kernel/typechecker. Is that correct?
2. If so, why don't the second and third checks work?
3. In fact, if I turn set_option trace.Meta.synthInstance on, I see the following:

[Meta.synthInstance] ✅ HAdd (GradedPapers 3) (GradedPapers 3) (GradedPapers 3) ▼
[Meta.synthInstance] ❌ HAdd (GradedPapers 3) (GradedPapers (2 + 1)) ?m.483 ▶

3a. Why doesn't it use the green tick line?? The output type is correct
3b. Why is the output type of the red cross line a hole (?m.483)? It seems especially weird on the third check, because I explicitly wrote : GradedPapers 3 for the output type. Same for the PaperAB if you replace PaperB' by PaperB.

4. Is there any way to make + work smoothly here?

[Gareth Ma]

(There are questions hidden under the code block, please click "Show more" :D)

[Eric Wieser]

#check PaperA + (by exact PaperB) work too!

[Gareth Ma]

Wow I hate it

[Gareth Ma]

Okay hmm but is there any other way? I think it's quite annoying if I have to write something like

import Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic

open EisensteinSeries ModularForm UpperHalfPlane CongruenceSubgroup

local notation "G[" k "]" => @eisensteinSeries_MF k 1 (by decide) 0
noncomputable def E₄ : ModularForm (Gamma 1) 4 := (1/2) • G[4]
noncomputable def E₆ : ModularForm (Gamma 1) 6 := (1/2) • G[6]
noncomputable def Δ : ModularForm (Gamma 1) 12 :=
  (1/1728) • ((by exact (E₄.mul E₄).mul E₄) - (by exact E₆.mul E₆))

But if that's the best way for now, then sure.

[Gareth Ma]

But maybe it would be nice to have an extension of the (... : _) syntax to really really force the type of the term (syntactically)

[Yakov Pechersky]

Can you make your 'combine' take two separate GradedPapers, one over n, one over m, and combine also takes a proof that n = m that is proven by autoparam omega or decide or something?

[Gareth Ma]

Okay I just tried, and (as always) the first check works, that's expected. But then I don't know how to define the Add instance, so I changed it to a HAdd instance, and now everything breaks down :(

import Mathlib.Tactic

structure GradedPapers (n : Int) where
  grade : Int

set_option linter.unusedVariables false in
def GradedPapers.combine {n m : Int} (a : GradedPapers n) (b : GradedPapers m) (h' : n = m := by omega) :
    GradedPapers n :=
  ⟨a.grade + b.grade⟩

def PaperA : GradedPapers 3 := ⟨10⟩
def PaperB : GradedPapers (2 + 1) := ⟨10⟩
#check PaperA.combine PaperB

-- instance GradedPapers.instAdd {n : Int} : Add (GradedPapers n) := ⟨combine⟩
instance GradedPapers.instHAdd {n : Int} {m : Int} [h : Fact (n = m)] :
  HAdd (GradedPapers n) (GradedPapers m) (GradedPapers n) := ⟨fun x y ↦ combine x y h.out⟩

#check PaperA + PaperB
#check (PaperA + PaperB : GradedPapers 3)

def PaperB' : GradedPapers 3 := PaperB
def PaperAB : GradedPapers (1 + 1 + 1) := PaperA + PaperB'

[Gareth Ma]

(Small reminder that there's a "View in Playground" button)

[Yakov Pechersky]

Why Fact the equality? TC will never solve that

[Gareth Ma]

How should I do it then?

[Yakov Pechersky]

Under my omega proposal, you'd have notation based addition, not via a typeclass

[Gareth Ma]

What does that mean?

[Gareth Ma]

Oh like define a new notation+\_m or something, then write that instead (M1 +\_m M2 +\_m M3)?

[Yakov Pechersky]

https://github.com/leanprover-community/mathlib4/blob/ed125a4216d18273cb1b96d4c846d32b85d74faf/Mathlib%2FGroupTheory%2FPerm%2FCycle%2FConcrete.lean#L468-L469

[Yakov Pechersky]

Like the cycle notation is able to discharge the proof of nodup of the list

[Yakov Pechersky]

First show that your combine will work when calling combine explicitly on your 3 and 1+1+1 examples without having to provide a proof.

[Gareth Ma]

set_option quotPrecheck false in
notation A "+ₘ" B => GradedPapers.combine A B (by omega)

#check PaperA +ₘ PaperB
#check (PaperA +ₘ  PaperB : GradedPapers 3)

def PaperAB : GradedPapers (1 + 1 + 1) := PaperA +ₘ PaperB

Okay I think this works perfectly - I think this is what you mean :thinking:

[Gareth Ma]

(all works)

[Gareth Ma]

In fact, using this I can remove the auto outParam for m = n entirely

[Yakov Pechersky]

You could, or make it an implicit autoparam so that the notation doesn't even have to mention omega

[Yakov Pechersky]

Not sure if explicit vs implicit matters

[Gareth Ma]

structure GradedPapers (n : Int) where
  grade : Int

set_option linter.unusedVariables false in
def GradedPapers.combine {n m : Int} (a : GradedPapers n) (b : GradedPapers n) {h' : n = m} :
    GradedPapers n :=
  ⟨a.grade + b.grade⟩

def PaperA : GradedPapers 3 := ⟨10⟩
def PaperB : GradedPapers (2 + 1) := ⟨10⟩
#check PaperA.combine PaperB

set_option quotPrecheck false in
notation A "+ₘ" B => GradedPapers.combine A B (h' := by omega)

#check PaperA +ₘ PaperB
#check (PaperA +ₘ PaperB : GradedPapers 3)

def PaperAB : GradedPapers (1 + 1 + 1) := PaperA +ₘ PaperB

This seems to break, and I don't know why

[Yakov Pechersky]

When I said make it implicit, I meant implicit autoparam. It breaks now because your by omega in notation never fires on the h' argument

[Yakov Pechersky]

And you use n twice in arguments to combine

[Gareth Ma]

:man_facepalming: yes the second one is the issue

[Gareth Ma]

Thank you. I think I will stick with removing the h' entirely for now, and when it breaks for whatever reason I can fall back to this

[Gareth Ma]

Also one more thing, is it possible to get dot notation to work in notation?

[Gareth Ma]

notation A "+ₘ" B => A.combine B fails for some reason (the .combine is treated as some metavariable I don't understand

[Gareth Ma]

Because I have two types of graded papers, both with an .add, and it would be great to have the same notation for them

[Gareth Ma]

notation A "+ₘ" B => (A).combine B works!