Zulip Chat Archive

Stream: general

Topic: use/coerce one dependent type as an equal one?


view this post on Zulip Andrew Tindall (Sep 23 2018 at 13:55):

I am trying to apply a function to a vector, and get the error message

type mismatch at application
  f (vector.take j v)
term
  vector.take j v
has type
  vector (S.A) (min j (max j k))
but is expected to have type
  vector (S.A) j

j and k are nats. I know that j = min j (max j k), but I don't know how to use that equivalence to coerce v from one type to another. Should I just make a specific instance of has_coe and then use it to cast v?

view this post on Zulip Keeley Hoek (Sep 23 2018 at 13:59):

If it was me I would explicitly turn vector.take j v into something of type vector (S.A) j before applying the coercion

view this post on Zulip Reid Barton (Sep 23 2018 at 14:14):

Isn't j = min j (max j k) always true? Where is vector.take defined?

view this post on Zulip Andrew Tindall (Sep 23 2018 at 14:21):

Yes, it's always true. vector.takeis in data.vector.

view this post on Zulip Kenny Lau (Sep 23 2018 at 14:22):

maybe you should change the type of f first

view this post on Zulip Reid Barton (Sep 23 2018 at 14:23):

Oh, in the core library! Right

view this post on Zulip Kenny Lau (Sep 23 2018 at 14:23):

also, MWE

view this post on Zulip Reid Barton (Sep 23 2018 at 14:29):

If this is in a programming context, I would probably use the convert tactic or some rw and prove j = min j (max j k).
If this is in a theorem-proving context, where I need to prove some fact about the result of this expression, I would just define my own take' with a more useful type like

def vec.take' (i n : ) (h : i <= n) : vector α n  vector α i

(the implementation can probably even be the same)


Last updated: May 11 2021 at 21:10 UTC