Equivalent of nat S in Coq.NArith.NArith · Coq users

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

Julio Di Egidio (Oct 28 2023 at 15:11):

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

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

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 (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):

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.

Stream: Coq users

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

Julio Di Egidio (Oct 28 2023 at 14:31):