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?

I guess you could `Import N.`

and then `succ`

would refer to `N.succ`

. Is it what you asked for?

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

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

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.

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

N.succ is the equivalent of S

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

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

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?

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

```
```

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

Julio Di Egidio has marked this topic as unresolved.

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?

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

Indeed I meant using `Nnat`

.

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