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?

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

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

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

Thanks so much!

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

Ezra Sitorus has marked this topic as resolved.

Last updated: Sep 28 2023 at 10:01 UTC