Dependent types

Stream: general

[Sebastien Gouezel]

Suppose that I have two natural numbers n and m, and a proof that they are equal h : n = m. I have essentially never needed dependent types, but here I really have to deal with them and define the identity map from fin n to fin m. Can someone help with this? (I am in tactic mode, if that matters).

[Johannes Hölzl]

use fin.cast

[Johannes Hölzl]

The important thing is that it copies the contained value, so when projecting it you don't have an rw in your data

[Simon Hudon]

If you're in tactic mode, you may have better result if you call subst n first.

[Simon Hudon]

Then you don't need cast

[Simon Hudon]

Here's my thinking when considering using cast:

• try to avoid cast
• try harder
• are you sure it doesn't work
• hide cast as far from public view as possible

[Sebastien Gouezel]

fin.cast uses the specifics offin if I look at the definition. I am more looking for the syntax for the more general situation where you have dependent types C k, a proof that k = l, and want to define the identity from C k to C l starting from the identity from C k to C k (which is the same map, but I don't how to convince lean of this). How would I use cast or subst in such a situation? (I never used any of them, so I don't know what they are supposed to do, or their syntax!)

[Johannes Hölzl]

You can use eq.rec. But be very careful, it is usually a bad idea to do computation under it

[Reid Barton]

But note that all of the general-purpose alternatives like the subst and rw tactics are also going to use eq.rec under the hood.

[Neil Strickland]

In some sense the "obvious" thing to do is is as follows: given h : k = l you have congr_arg C h : C k = C l and cast (congr_arg C h) : C k -> C l. But this approach leads to a lot of awkwardness. It is common that you have some data combined with some properties, and you can define a map that just applies cast to the properties while leaving the data alone. This is what fin.cast does. It generally works much better because of proof irrelevance: any two proofs of the same proposition are considered the same, so you don't need to worry about what exactly the cast did.

[Reid Barton]

The issue is that in a situation like

variables {i n : ℕ} (h : i < n)
variables {m : ℕ} (e : n = m)

#reduce (eq.rec_on e (fin.mk i h) : fin m).val

this expression is not definitionally equal to i, even though you can prove that it is equal to i.

[Sebastien Gouezel]

OK, thanks a lot for your explanations. Definitional equality is really useful for me here, so I will go for fin.cast as advocated by Johannes, but I have learnt a lot!