## Stream: general

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

#### 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?

#### 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

#### Reid Barton (Sep 23 2018 at 14:14):

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

#### Andrew Tindall (Sep 23 2018 at 14:21):

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

#### Kenny Lau (Sep 23 2018 at 14:22):

maybe you should change the type of f first

#### Reid Barton (Sep 23 2018 at 14:23):

Oh, in the core library! Right

also, MWE

#### 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