Stream: Coq users

Topic: Working with multiple numeric types with notations


view this post on Zulip Anthony Peterson (Nov 02 2023 at 13:05):

In trying to do math with both N and nat types at the same time, and I wondered if there was a better way to handle multiple different numeric type notations at the same time. Even just providing the constant zero value collides between these two types.

I still have N_scope open, but because I open nat_scope just for this one definition, it seems to have priority if a notation is used by both nat and N.

I'm solving an Advent of Code problem from 2017 to get some practice in: "Now, instead of considering the next digit, it wants you to consider the digit halfway around the circular list. That is, if your list contains 10 items, only include a digit in your sum if the digit 10/2 = 5 steps forward matches it. Fortunately, your list has an even number of elements."

Definition matchHalfway (lv : list N) (index : nat) :=
  let len := length lv in
  let target := (index + (len / 2)) mod len in
  let o := nth index lv N.zero in
  let m := nth target lv N.zero in
  if N.eqb o m then o else N.zero.

Also, is there an array type that would better for indexing than lists? I know linked lists are particularly awful at this.

view this post on Zulip Pierre Roux (Nov 02 2023 at 13:08):

I guess, assuming the proper require imports, 42%N should be the constant of type N whereas 42%nat should be of type nat? Then you can Local Open Scope N_scope in your file if have more of the former.

view this post on Zulip Anthony Peterson (Nov 02 2023 at 13:09):

Pierre Roux said:

I guess, assuming the proper require imports, 42%N should be the constant of type N whereas 42%nat should be of type nat? Then you can Local Open Scope N_scope in your file if have more of the former.

Yeah I just changed N.zero to 0%N. But I still have equality in N and addition in nat. It's not that bad in a toy example I guess.

view this post on Zulip Anthony Peterson (Nov 02 2023 at 13:10):

I'm using N for the list values because I'm converting from ascii input to numeric, and that used N.

view this post on Zulip Pierre Roux (Nov 02 2023 at 13:14):

You can similarly do (x + y)%N and (x + y)%nat (see the refman page https://coq.inria.fr/doc/V8.18.0/refman/user-extensions/syntax-extensions.html for (a lot of) details about notatins).

view this post on Zulip Anthony Peterson (Nov 02 2023 at 13:15):

ah ok, that's helpful.

view this post on Zulip Anthony Peterson (Nov 02 2023 at 13:17):

also, there seems to be no boolean comparison on N, is that the case. I just used

match N.compare n 48 with
  | Lt => 0
  | _ => n - 48

instead.

view this post on Zulip Pierre Roux (Nov 02 2023 at 13:19):

There is N.eqb, notation (x =? y)%N.

view this post on Zulip Anthony Peterson (Nov 02 2023 at 13:21):

I see it now. Thanks for your help!


Last updated: Jun 22 2024 at 16:02 UTC