Unexpected type error in equality proposition

Stream: new members

[Kevin Sullivan]

set_option pp.all true
#reduce eq.refl 0
#reduce eq.refl (1-1)
#check (eq.refl 0) = (eq.refl 0) -- this works
#check (eq.refl 0) = (eq.refl (1-1)) -- type error!>?<!

Why>

[Andrew Ashworth]

this also works: #check (eq.refl (0)) = (eq.refl ((1 - 1):ℕ))

[Andrew Ashworth]

Unfortunately I don't know why it needs a type ascription

[Kevin Buzzard]

Is it because Lean doesn't know what that zero is? It's just has_zero.zero until you tell it that it's nat's zero

[Kevin Sullivan]

Or that it doesn't know what that (1-1) is? The preceding lines seem to indicate that all the terms really are equal, so this result is a bit mystifying.

[Mario Carneiro]

It's an elaborator order problem, as usual. For eq.refl a = eq.refl b to typecheck, a and b must be defeq. These both work:

#check (eq.refl 0) = (eq.refl 0)
#check (eq.refl (1-1)) = (eq.refl (1-1))

because lean knows that (0:A) == 0 definitionally and similarly for (1-1:A) == (1-1:A). In particular, it doesn't need to know that A = nat for this to work. Now having successfully elaborated the term, it knows that the statement is (eq.refl (0:?m)) = (eq.refl 0), and so since there is a numeral with unknown type, lean does its late nat defaulting, setting ?m = nat, inferring the typeclass args, and you get what you see in the pp.all.

In the case (eq.refl 0) = (eq.refl (1-1)), it doesn't work out so well. Lean tries to check (0:A) =?= 1-1, and this fails, because in an arbitrary type with subtraction and 0 and 1 this doesn't necessarily hold by definition. So it fails right here, and never gets to the nat fallback.

[Mario Carneiro]

The moral of the story: don't trust nat defaulting. It's a convenience so that #eval 1 + 1 does what you expect. You should really think of these terms as having unknown type.

[Kenny Lau]

I think the correct answer is, what on earth are you doing with (eq.refl 0) = (eq.refl (1-1))

[Kevin Sullivan]

Mario, Thank you very much. That's was a very helpful answer. I had to read it a few times, but now I understand.

Kenny, Ha ha. I'm teaching early undergraduates students (400 of them) discrete math using Lean. One of them was dutifully exploring applications of the various principles I've taught them, tried out the example here, and was mystified by the answer.