Zulip Chat Archive

Stream: new members

Topic: fin heq


Nicolò Cavalleri (Jul 04 2021 at 13:55):

Why does this not trigger an error?

example (z : fin 4) (n : fin (2 + 2)) : z = n := sorry

I mean don't I need to give it a proof that 2 + 2 = 4 to know that fin 4 and fin 2 + 2 are the same type?

Eric Rodriguez (Jul 04 2021 at 13:56):

example : 2 + 2 = 4 := rfl :)

Nicolò Cavalleri (Jul 04 2021 at 13:58):

Ok I probably miss something on the definition of addition... I'll have a look

Nicolò Cavalleri (Jul 04 2021 at 14:00):

Eric Rodriguez said:

example : 2 + 2 = 4 := rfl :)

Why is this the case? Is it true for any recursive definition?

Mario Carneiro (Jul 04 2021 at 14:02):

lean knows how to evaluate recursive functions when determining that two things are "the same by definition", and this is the relation that determines when an element of one type also has another type

Adam Topaz (Jul 04 2021 at 14:03):

They both reduce to succ (succ (succ ( succ zero ) ) )

Nicolò Cavalleri (Jul 04 2021 at 14:04):

Ok thanks

Nicolò Cavalleri (Jul 04 2021 at 14:05):

Well the reason why I am asking this is that I am trying to explain heq to a person that does not know type theory. What is the simplest example you can think of two types that are equal but not definitionally equal?

Adam Topaz (Jul 04 2021 at 14:06):

But if you have variables m and n, then you'll run into issues with fin (m+n) vs fin (n+m), for example

Nicolò Cavalleri (Jul 04 2021 at 14:10):

Ok thanks that could be an example

Adam Topaz (Jul 04 2021 at 14:14):

The easiest example would probably be to compare fin m and fin (0 + m), with m : \nat a variable.

Mario Carneiro (Jul 04 2021 at 14:14):

Another source of examples even with closed terms is anything using an axiom in the proof, for example (true /\ true) = true

Mario Carneiro (Jul 04 2021 at 14:17):

In fact that example is pretty interesting because the two types feel very different. One is a pair type and the other is a unit type (and you can throw in nat -> true which is a function type). It seems odd that a lambda and a pair constructor are living in "the same" type, but math says that (true /\ true) = (nat -> true)


Last updated: Dec 20 2023 at 11:08 UTC