fin heq

Stream: new members

[Nicolò Cavalleri]

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]

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

[Nicolò Cavalleri]

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

[Nicolò Cavalleri]

Eric Rodriguez said:

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

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

[Mario Carneiro]

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]

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

[Nicolò Cavalleri]

Ok thanks

[Nicolò Cavalleri]

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]

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]

Ok thanks that could be an example

[Adam Topaz]

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

[Mario Carneiro]

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

[Mario Carneiro]

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)