incomplete discriminant refinement procedure

Stream: lean4

[Arthur Adjedj]

The following is fairly unrelated to this thread, but I thought it might be worth pointing out somewhere:
When trying to rewrite the work presented here in Agda form, I quickly encountered a pattern-matching failure that I did not expect to find, and would expect to be a bug:

inductive Add' : Nat → Nat → Nat → Type where
  | zel : Add' 0 n n
  | zer : Add' n 0 n
  | susu : Add' l m n → Add' (l+1) (m+1) (n+2)

inductive Poly : Nat → Type where
  | ι : Poly (n+1)
  | times : Poly l → Poly m → Add' l m n → Poly n

def Poly.delta : Poly (n+1) → Poly n
  | ι
  | times p r .zel => sorry
  | times p r .zer => sorry
  | times p r (.susu a) => sorry
  /-Application type mismatch: The argument
      a.susu
    has type
      Add' (?m.39 + 1) (?m.40 + 1) (?m.41 + 2)
    but is expected to have type
      Add' ?m.34 ?m.35 (n + 1)
    in the application
      p.times r a.susu-/

[Aaron Liu]

fixed it

inductive Add' : Nat → Nat → Nat → Type where
  | zel : Add' 0 n n
  | zer : Add' n 0 n
  | susu : Add' l m n → Add' (l+1) (m+1) (n+2)

inductive Poly : Nat → Type where
  | ι : Poly (n+1)
  | times : Poly l → Poly m → Add' l m n → Poly n

def Poly.delta : Poly (n+1) → Poly n := fun poly =>
  match n, poly with
  | _, ι
  | _, times p r .zel => sorry
  | _, times p r .zer => sorry
  | _, times _ _ (.susu a) => sorry

the matcher sometimes doesn't include enough variables

[Arthur Adjedj]

Yes, I'm conscious this is easily solvable, I'm still surprised this isn't done automatically

[Aaron Liu]

there's a heuristic for when to rope in more variables

[Joachim Breitner]

Since it’s unrelated I took the liberty to rename.