Zulip Chat Archive

Stream: general

Topic: Dependent types

Sebastien Gouezel (Jan 31 2019 at 19:46):

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 (Jan 31 2019 at 19:47):

use fin.cast

Johannes Hölzl (Jan 31 2019 at 19:47):

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 (Jan 31 2019 at 19:49):

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

Simon Hudon (Jan 31 2019 at 19:49):

Then you don't need cast

Simon Hudon (Jan 31 2019 at 19:50):

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 (Jan 31 2019 at 19:55):

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 (Jan 31 2019 at 19:56):

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

Reid Barton (Jan 31 2019 at 19:59):

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 (Jan 31 2019 at 20:01):

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 (Jan 31 2019 at 20:06):

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 (Jan 31 2019 at 20:09):

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!

Last updated: Aug 03 2023 at 10:10 UTC