Stream: Coq users

Topic: Equivalent of nat S in Coq.NArith.NArith


view this post on Zulip Julio Di Egidio (Oct 28 2023 at 14:31):

Hi there, a quick one I hope: I am importing Coq.NArith.NArith, then opening the scope N_scope, and there is notation for the usual operators but I cannot find a notation for N.succ. Should I be importing/opening something else or that's simply not in the library?

view this post on Zulip Pierre Rousselin (Oct 28 2023 at 14:40):

I guess you could Import N. and then succ would refer to N.succ. Is it what you asked for?

view this post on Zulip Julio Di Egidio (Oct 28 2023 at 14:41):

I am also having troubles finding the equivalent of the nat constructor 'S'. Sorry, in fact I don't think I understand how to use this library yet... Essentially, I had done a little development with nat and now I was trying to convert to N since the original fails with stack overflows already for small numbers (the numbers I need to test)...

view this post on Zulip Julio Di Egidio (Oct 28 2023 at 14:49):

I was hoping for some easy translation, I was also using theorems from Coq.Arith.PeanoNat, e.g. Nat.div_add.

view this post on Zulip Julio Di Egidio (Oct 28 2023 at 14:56):

Concretely, after replacing all occurrences of nat with N, the next problem was 'S' not defined, hence my question: but I have wrongly asked about N.succ, while it's the equivalent of the nat constructor S that I am not finding.

view this post on Zulip Julio Di Egidio (Oct 28 2023 at 14:59):

If I look at the definition of N, I find Npos, but that takes as argument a positive, not an N...??

view this post on Zulip Gaëtan Gilbert (Oct 28 2023 at 15:05):

N.succ is the equivalent of S

view this post on Zulip Julio Di Egidio (Oct 28 2023 at 15:11):

But I am not able to pattern-match on N.succ, am I? Quick example:

Require Import Coq.NArith.NArith.

Local Open Scope N_scope.

Fixpoint sum_up_to_spec__do (a n : N) : N :=
  match n with
  | O    => a
  | N.succ n' => sum_up_to_spec__do (a + n) n'
  end.

I get "Unknown constructor: N.succ". (In fact I don't know what's exactly happening with O either, except that it's some implicit coercion, but I guess that's part of the same question.)

view this post on Zulip Gaëtan Gilbert (Oct 28 2023 at 15:21):

your stack overflow is because of using a type where +1 is a constructor, you can't fix it without giving up on that

view this post on Zulip Julio Di Egidio (Oct 28 2023 at 15:24):

Alright, that makes sense, still I have no clue how to use N: is there some example or tutorial, otherwise how should I rewrite the above example?

view this post on Zulip Pierre Castéran (Oct 28 2023 at 15:53):

You may for instance look at the definition (and the constructors) of the types Nand positive.
Then define your own successor and predecessor functions in positive.
In a second step, define your versions of successor and predecessor in N.

For instance:

Print N.
Print positive.

Fixpoint succ (x:positive) : positive :=
 match x with
   xH => xO x
 | xO y =>  xI y
 | xI y => xO (succ y)
end.

Compute succ 6%positive.
Compute succ 7%positive.


Fixpoint pred (x:positive) : positive :=
  match x with
    xH => xH (* to get a total function *)
  | xI y => xO y
  | xO xH => xH
  | xO y => xI (pred y)
  end.

Compute pred 10%positive.
Compute pred 11%positive.
Compute pred 2%positive.

Lemma pred_of_succ:  forall x, pred (succ x) = x.
(* ... *)

Definition N_succ (n:N) :=
  match n with
    0%N => 1%N
  | Npos p => Npos (succ p)
end.

view this post on Zulip Julio Di Egidio (Oct 28 2023 at 15:58):

Meanwhile I had found an example here
<https://www.cs.princeton.edu/courses/archive/fall07/cos595/stdlib/html/Coq.NArith.BinNat.html#Ndiv2>
but it's not a fixpoint and I do get errors if I try that directly in a fixpoint definition...

I see you define your succ/pred fixpoints on positive directly. I'll see if I manage that...

view this post on Zulip Notification Bot (Nov 01 2023 at 19:10):

Julio Di Egidio has marked this topic as unresolved.

view this post on Zulip Julio Di Egidio (Nov 01 2023 at 19:10):

Thanks very much @Ana de Almeida Borges for the advice: that's indeed what I was thinking and trying, the spec and the theorems in nat, the implementation in N, plus the "equivalence" of nat and N (I was actually thinking the equivalence of the two functions, i.e. a proof of correctness): except that my spec is itself a function and I have been unable to prove even the simplest results about the equivalence of operations in nat with those in N...

Having the spec as a function is nice because I can compute with it, but maybe that one I can write if I really need it: at this point I am thinking I should rather have the spec in Prop and go the reflect way... right? Is that what you meant?

view this post on Zulip Julio Di Egidio (Nov 01 2023 at 20:20):

But I have just discovered Coq.NArith.Nnat which might be what I was missing (to have the spec a function without reinventing the wheel).

view this post on Zulip Ana de Almeida Borges (Nov 02 2023 at 14:50):

Indeed I meant using Nnat.

view this post on Zulip Ana de Almeida Borges (Nov 02 2023 at 14:52):

I also meant having an implementation in nat and an implementation in N. You then prove the nat implementation corresponds to the nat specification and that the nat implementation corresponds to the N implementation (via Nnat). Composing the two results you obtain that the N implementation corresponds to the nat specification.


Last updated: Jun 13 2024 at 19:02 UTC