## Stream: Coq users

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

#### 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?

#### 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?

#### 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)...

#### 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.

#### 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.

#### 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...??

#### Gaëtan Gilbert (Oct 28 2023 at 15:05):

N.succ is the equivalent of S

#### 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.)

#### 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

#### 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?

#### Pierre Castéran (Oct 28 2023 at 15:53):

You may for instance look at the definition (and the constructors) of the types `N`and `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.
``````
``````
``````

#### 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...

#### Notification Bot (Nov 01 2023 at 19:10):

Julio Di Egidio has marked this topic as unresolved.

#### 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?

#### 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).

#### Ana de Almeida Borges (Nov 02 2023 at 14:50):

Indeed I meant using `Nnat`.

#### 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