Stream: Coq users

Topic: ✔ Hypothesis in if then else


view this post on Zulip 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?

view this post on Zulip Gregory Malecha (Sep 16 2022 at 13:32):

It is.

view this post on Zulip Gregory Malecha (Sep 16 2022 at 13:33):

You can get the equality proof from eq_nat_dec and using match

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Ezra Sitorus (Sep 16 2022 at 13:38):

Thanks so much!

view this post on Zulip Notification Bot (Sep 16 2022 at 13:51):

Ezra Sitorus has marked this topic as resolved.


Last updated: Feb 05 2023 at 22:03 UTC