type mismatch for fin n

Stream: general

[Kevin Buzzard]

I am surprised that this doesn't typecheck:

[Kevin Buzzard]

def subtypeadd {m : ℕ} {n : ℕ} (A : fin m) (B : fin n) : fin (m+n) :=
  ⟨A.val+B.val,add_lt_add A.is_lt B.is_lt⟩

example (A : fin 3) (B : fin 4) (C : fin 7)
  : A = ⟨2,dec_trivial⟩ → B = ⟨0,dec_trivial⟩ → C = subtypeadd A B → C = ⟨2,dec_trivial⟩ := sorry

[Kevin Buzzard]

It complains at subtypeadd that A has type fin 3 and it expects it to have type fin 6??

[Mario Carneiro]

I think this is the default elaboration strategy's fault

[Kevin Buzzard]

It's hard for me to see what's going on because it doesn't typecheck so I don't have any term to work with

[Kevin Buzzard]

Obviously I can fix it with @

[Kevin Buzzard]

but here -- hey -- can you be the elaborator like you sometimes do?

[Mario Carneiro]

You can make it typecheck by writing @subtypeadd _ _ A B or adding @[elab_simple] to the definition of subtypeadd

[Kevin Buzzard]

You have to figure out what m and n are

[Kevin Buzzard]

and the only clues you have are that A : fin m and A : fin 3

[Kevin Buzzard]

what do you think

[Kevin Buzzard]

mr elaborator

[Mario Carneiro]

It sees that the goal is fin 7 and so has to solve 7 =?= ?m1 + ?m2. I think if you unfold 7 enough (bit1 (bit1 one)) you get bit0 (bit1 one) + 1, i.e. 6+1. So it's the most obvious split and lean takes it

[Kevin Buzzard]

Aah excellent!

[Kevin Buzzard]

so in fact this is a fun game

[Kevin Buzzard]

guess the error

[Kevin Buzzard]

example (A : fin 3) (B : fin 5) (C : fin 8)
  : A = ⟨2,dec_trivial⟩ → B = ⟨0,dec_trivial⟩ → C = subtypeadd A B → C = ⟨2,dec_trivial⟩ := sorry

[Kevin Buzzard]

you have to guess the spurious complaint that Lean makes

[Kevin Buzzard]

for fin 2n it wants A : fin n and for fin (2n+1) it wants A : fin (2n)