Library Coq.Numbers.Integer.BigZ.BigZ



Require Export BigN.
Require Import ZProperties ZDivFloor ZSig ZSigZAxioms ZMake.

BigZ : arbitrary large efficient integers.



The following BigZ module regroups both the operations and all the abstract properties:
  • ZMake.Make BigN provides the operations and basic specs w.r.t. ZArith
  • ZTypeIsZAxioms shows (mainly) that these operations implement the interface ZAxioms
  • ZPropSig adds all generic properties derived from ZAxioms
  • ZDivPropFunct provides generic properties of div and mod ("Floor" variant)
  • MinMax*Properties provides properties of min and max

Module BigZ <: ZType <: OrderedTypeFull <: TotalOrder :=
 ZMake.Make BigN <+ ZTypeIsZAxioms
 <+ !ZPropSig <+ !ZDivPropFunct <+ HasEqBool2Dec
 <+ !MinMaxLogicalProperties <+ !MinMaxDecProperties.

Notations about BigZ

Notation bigZ := BigZ.t.

Delimit Scope bigZ_scope with bigZ.

Local Notation "0" := BigZ.zero : bigZ_scope.
Local Notation "1" := BigZ.one : bigZ_scope.
Infix "+" := BigZ.add : bigZ_scope.
Infix "-" := BigZ.sub : bigZ_scope.
Notation "- x" := (BigZ.opp x) : bigZ_scope.
Infix "*" := BigZ.mul : bigZ_scope.
Infix "/" := BigZ.div : bigZ_scope.
Infix "^" := BigZ.power : bigZ_scope.
Infix "?=" := BigZ.compare : bigZ_scope.
Infix "==" := BigZ.eq (at level 70, no associativity) : bigZ_scope.
Notation "x != y" := (~x==y)%bigZ (at level 70, no associativity) : bigZ_scope.
Infix "<" := BigZ.lt : bigZ_scope.
Infix "<=" := BigZ.le : bigZ_scope.
Notation "x > y" := (BigZ.lt y x)(only parsing) : bigZ_scope.
Notation "x >= y" := (BigZ.le y x)(only parsing) : bigZ_scope.
Notation "x < y < z" := (x<y /\ y<z)%bigZ : bigZ_scope.
Notation "x < y <= z" := (x<y /\ y<=z)%bigZ : bigZ_scope.
Notation "x <= y < z" := (x<=y /\ y<z)%bigZ : bigZ_scope.
Notation "x <= y <= z" := (x<=y /\ y<=z)%bigZ : bigZ_scope.
Notation "[ i ]" := (BigZ.to_Z i) : bigZ_scope.
Infix "mod" := BigZ.modulo (at level 40, no associativity) : bigN_scope.

Local Open Scope bigZ_scope.

Some additional results about BigZ

Theorem spec_to_Z: forall n : bigZ,
  BigN.to_Z (BigZ.to_N n) = ((Zsgn [n]) * [n])%Z.

Theorem spec_to_N n:
 ([n] = Zsgn [n] * (BigN.to_Z (BigZ.to_N n)))%Z.

Theorem spec_to_Z_pos: forall n, (0 <= [n])%Z ->
  BigN.to_Z (BigZ.to_N n) = [n].

BigZ is a ring

Lemma BigZring :
 ring_theory 0 1 BigZ.add BigZ.mul BigZ.sub BigZ.opp BigZ.eq.

Lemma BigZeqb_correct : forall x y, BigZ.eq_bool x y = true -> x==y.

Lemma BigZpower : power_theory 1 BigZ.mul BigZ.eq (@id N) BigZ.power.

Lemma BigZdiv : div_theory BigZ.eq BigZ.add BigZ.mul (@id _)
 (fun a b => if BigZ.eq_bool b 0 then (0,a) else BigZ.div_eucl a b).

Detection of constants

Ltac isBigZcst t :=
 match t with
 | BigZ.Pos ?t => isBigNcst t
 | BigZ.Neg ?t => isBigNcst t
 | BigZ.zero => constr:true
 | BigZ.one => constr:true
 | BigZ.minus_one => constr:true
 | _ => constr:false
 end.

Ltac BigZcst t :=
 match isBigZcst t with
 | true => constr:t
 | false => constr:NotConstant
 end.

Registration for the "ring" tactic

Add Ring BigZr : BigZring
 (decidable BigZeqb_correct,
  constants [BigZcst],
  power_tac BigZpower [Ncst],
  div BigZdiv).

Section TestRing.
Let test : forall x y, 1 + x*y + x^2 + 1 == 1*1 + 1 + y*x + 1*x*x.
Let test' : forall x y, 1 + x*y + x^2 - 1*1 - y*x + 1*(-x)*x == 0.
End TestRing.

BigZ also benefits from an "order" tactic

Ltac bigZ_order := BigZ.order.

Section TestOrder.
Let test : forall x y : bigZ, x<=y -> y<=x -> x==y.
End TestOrder.

We can use at least a bit of (r)omega by translating to Z.

Section TestOmega.
Let test : forall x y : bigZ, x<=y -> y<=x -> x==y.
End TestOmega.

Todo: micromega