Library Coq.Numbers.Rational.BigQ.BigQ
BigQ: an efficient implementation of rational numbers
Initial authors: Benjamin Gregoire, Laurent Thery, INRIA, 2007
We choose for BigQ an implemention with
multiple representation of 0: 0, 1/0, 2/0 etc.
See QMake.v
First, we provide translations functions between BigN and BigZ
This allows to build BigQ out of BigN and BigQ via QMake
Notations about BigQ
Notation bigQ :=
BigQ.t.
Delimit Scope bigQ_scope with bigQ.
As in QArith, we use # to denote fractions
Notation "p # q" := (
BigQ.Qq p q) (
at level 55,
no associativity) :
bigQ_scope.
Local Notation "0" :=
BigQ.zero :
bigQ_scope.
Local Notation "1" :=
BigQ.one :
bigQ_scope.
Infix "+" :=
BigQ.add :
bigQ_scope.
Infix "-" :=
BigQ.sub :
bigQ_scope.
Notation "- x" := (
BigQ.opp x) :
bigQ_scope.
Infix "*" :=
BigQ.mul :
bigQ_scope.
Infix "/" :=
BigQ.div :
bigQ_scope.
Infix "^" :=
BigQ.power :
bigQ_scope.
Infix "?=" :=
BigQ.compare :
bigQ_scope.
Infix "==" :=
BigQ.eq :
bigQ_scope.
Notation "x != y" := (
~x==y)%
bigQ (
at level 70,
no associativity) :
bigQ_scope.
Infix "<" :=
BigQ.lt :
bigQ_scope.
Infix "<=" :=
BigQ.le :
bigQ_scope.
Notation "x > y" := (
BigQ.lt y x)(
only parsing) :
bigQ_scope.
Notation "x >= y" := (
BigQ.le y x)(
only parsing) :
bigQ_scope.
Notation "x < y < z" := (
x<y /\ y<z)%
bigQ :
bigQ_scope.
Notation "x < y <= z" := (
x<y /\ y<=z)%
bigQ :
bigQ_scope.
Notation "x <= y < z" := (
x<=y /\ y<z)%
bigQ :
bigQ_scope.
Notation "x <= y <= z" := (
x<=y /\ y<=z)%
bigQ :
bigQ_scope.
Notation "[ q ]" := (
BigQ.to_Q q) :
bigQ_scope.
Local Open Scope bigQ_scope.
BigQ is a field
BigQ can also benefit from an "order" tactic
We can also reason by switching to QArith thanks to tactic
BigQ.qify.