Stream: Coq users

Topic: ✔ Hypothesis in if then else

Ezra Sitorus (Sep 16 2022 at 13:14):

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.

Gregory Malecha (Sep 16 2022 at 13:33):

You can get the equality proof from `eq_nat_dec` and using `match`

Gregory Malecha (Sep 16 2022 at 13:35):

So something like

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

Gregory Malecha (Sep 16 2022 at 13:35):

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

Thanks so much!

Notification Bot (Sep 16 2022 at 13:51):

Ezra Sitorus has marked this topic as resolved.

Last updated: Jun 25 2024 at 14:01 UTC