Zulip Chat Archive

Stream: new members

Topic: Unexpected type error in equality proposition


view this post on Zulip Kevin Sullivan (Feb 24 2019 at 02:28):

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>

view this post on Zulip Andrew Ashworth (Feb 24 2019 at 04:15):

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

view this post on Zulip Andrew Ashworth (Feb 24 2019 at 04:16):

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

view this post on Zulip Kevin Buzzard (Feb 24 2019 at 08:43):

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

view this post on Zulip Kevin Sullivan (Feb 24 2019 at 16:13):

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.

view this post on Zulip Mario Carneiro (Feb 24 2019 at 16:50):

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.

view this post on Zulip Mario Carneiro (Feb 24 2019 at 16:52):

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.

view this post on Zulip Kenny Lau (Feb 24 2019 at 16:54):

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

view this post on Zulip Kevin Sullivan (Feb 26 2019 at 18:19):

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.


Last updated: May 13 2021 at 19:20 UTC