Library Stdlib.Numbers.Integer.Abstract.ZAxioms

From Stdlib Require Export NZAxioms.
From Stdlib Require Import Bool NZParity NZPow NZSqrt NZLog NZGcd NZDiv NZBits.

We obtain integers by postulating that successor of predecessor is identity.

Module Type ZAxiom (Import Z : NZAxiomsSig').
Axiom succ_pred : forall n, S (P n) == n.
End ZAxiom.

For historical reasons, ZAxiomsMiniSig isn't just NZ + ZAxiom, we also add an opp function, that can be seen as a shortcut for sub 0.

Module Type Opp (Import T:Typ).
Parameter Inline opp : t -> t.
End Opp.

Module Type OppNotation (T:Typ)(Import O : Opp T).
Notation "- x" := (opp x) (at level 35, right associativity).
End OppNotation.

Module Type Opp' (T:Typ) := Opp T <+ OppNotation T.

Module Type IsOpp (Import Z : NZAxiomsSig')(Import O : Opp' Z).
#[global]
Declare Instance opp_wd : Proper (eq ==>eq) opp.
Axiom opp_0 : - 0 == 0.
Axiom opp_succ : forall n, - (S n ) == P (- n).
End IsOpp.

Module Type OppCstNotation (Import A : NZAxiomsSig)(Import B : Opp A).
Notation "- 1" := (opp one).
Notation "- 2" := (opp two).
End OppCstNotation.

Module Type ZAxiomsMiniSig := NZOrdAxiomsSig <+ ZAxiom <+ Opp <+ IsOpp.
Module Type ZAxiomsMiniSig' := NZOrdAxiomsSig' <+ ZAxiom <+ Opp' <+ IsOpp
<+ OppCstNotation.

Other functions and their specifications

Absolute value

Module Type HasAbs(Import Z : ZAxiomsMiniSig').
Parameter Inline abs : t -> t.
Axiom abs_eq : forall n, 0<=n -> abs n == n.
Axiom abs_neq : forall n, n <=0 -> abs n == -n.
End HasAbs.

A sign function

Module Type HasSgn (Import Z : ZAxiomsMiniSig').
Parameter Inline sgn : t -> t.
Axiom sgn_null : forall n, n ==0 -> sgn n == 0.
Axiom sgn_pos : forall n, 0<n -> sgn n == 1.
Axiom sgn_neg : forall n, n <0 -> sgn n == -1.
End HasSgn.

Divisions

First, the usual Coq convention of Truncated-Toward-Bottom (a.k.a Floor). We simply extend the NZ signature.

Then, the Truncated-Toward-Zero convention. For not colliding with Floor operations, we use different names

Module Type QuotRem (Import A : Typ).
Parameters Inline quot rem : t -> t -> t.
End QuotRem.

Module Type QuotRemNotation (A : Typ)(Import B : QuotRem A).
Infix "÷" := quot (at level 40, left associativity).
Infix "rem" := rem (at level 40, no associativity).
End QuotRemNotation.

Module Type QuotRem' (A : Typ) := QuotRem A <+ QuotRemNotation A.

Module Type QuotRemSpec (Import A : ZAxiomsMiniSig')(Import B : QuotRem' A).
#[global]
Declare Instance quot_wd : Proper (eq ==>eq ==>eq) quot.
#[global]
Declare Instance rem_wd : Proper (eq ==>eq ==>eq) B.rem.
Axiom quot_rem : forall a b, b ~= 0 -> a == b *(a ÷b ) + (a rem b ).
Axiom rem_bound_pos : forall a b, 0<=a -> 0<b -> 0 <= a rem b < b.
Axiom rem_opp_l : forall a b, b ~= 0 -> (-a ) rem b == - (a rem b ).
Axiom rem_opp_r : forall a b, b ~= 0 -> a rem (-b ) == a rem b.
End QuotRemSpec.

Module Type ZQuot (Z:ZAxiomsMiniSig) := QuotRem Z <+ QuotRemSpec Z.
Module Type ZQuot' (Z:ZAxiomsMiniSig) := QuotRem' Z <+ QuotRemSpec Z.

For all other functions, the NZ axiomatizations are enough.

Let's group everything