Hi, I'd like to create a function that takes 2 vectors of same type but of lengths m and n and does something with them if m = n. For example:

```
Definition f {X : Type} (m n : nat) (a : Vector.t X m) (b : Vector.t X n)
: option (Vector.t X m)
:= if m =? n then something_here else None
```

For now it might be something simple like pairwise addition with nat vectors. I've used Lean before which has something called dite, where you bring the hypothesis into the cases. In this case, if I had a hypothesis that m = n then I could probably use the map2 function. So can someone let me know if this is possible?

It is.

You can get the equality proof from `eq_nat_dec`

and using `match`

So something like

```
match eq_nat_dec n m with
| left pf => ... pf : n = m ...
| right pf => ... pf : n <> m (not usually needed) ...
end
```

There might be a newer, fancier way though. I'm kind of a dinosaur when it comes to Coq

Thanks so much!

Ezra Sitorus has marked this topic as resolved.

Last updated: Jun 25 2024 at 14:01 UTC