Zulip Chat Archive

Stream: general

Topic: Dependent types


view this post on Zulip 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).

view this post on Zulip Johannes Hölzl (Jan 31 2019 at 19:47):

use fin.cast

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Simon Hudon (Jan 31 2019 at 19:49):

Then you don't need cast

view this post on Zulip 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

view this post on Zulip 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!)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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: May 17 2021 at 21:12 UTC