use/coerce one dependent type as an equal one?

Stream: general

[Andrew Tindall]

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]

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]

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

[Andrew Tindall]

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

[Kenny Lau]

maybe you should change the type of f first

[Reid Barton]

Oh, in the core library! Right

[Kenny Lau]

also, MWE

[Reid Barton]

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)