Library Coq.Numbers.Rational.BigQ.BigQ
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
Module BigN_BigZ <: NType_ZType BigN.BigN BigZ.
Definition Z_of_N := BigZ.Pos.
Lemma spec_Z_of_N : forall n, BigZ.to_Z (Z_of_N n) = BigN.to_Z n.
Definition Zabs_N := BigZ.to_N.
Lemma spec_Zabs_N : forall z, BigN.to_Z (Zabs_N z) = Zabs (BigZ.to_Z z).
End BigN_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.
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.
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 "[ q ]" := (BigQ.to_Q q) : bigQ_scope.
Open Scope bigQ_scope.
BigQ is a setoid
Add Relation BigQ.t BigQ.eq
reflexivity proved by (fun x => Qeq_refl [x])
symmetry proved by (fun x y => Qeq_sym [x] [y])
transitivity proved by (fun x y z => Qeq_trans [x] [y] [z])
as BigQeq_rel.
Add Morphism BigQ.add with signature BigQ.eq ==> BigQ.eq ==> BigQ.eq as BigQadd_wd.
Add Morphism BigQ.opp with signature BigQ.eq ==> BigQ.eq as BigQopp_wd.
Add Morphism BigQ.sub with signature BigQ.eq ==> BigQ.eq ==> BigQ.eq as BigQsub_wd.
Add Morphism BigQ.mul with signature BigQ.eq ==> BigQ.eq ==> BigQ.eq as BigQmul_wd.
Add Morphism BigQ.inv with signature BigQ.eq ==> BigQ.eq as BigQinv_wd.
Add Morphism BigQ.div with signature BigQ.eq ==> BigQ.eq ==> BigQ.eq as BigQdiv_wd.
BigQ is a field
Lemma BigQfieldth :
field_theory BigQ.zero BigQ.one BigQ.add BigQ.mul BigQ.sub BigQ.opp BigQ.div BigQ.inv BigQ.eq.
Lemma BigQpowerth :
power_theory BigQ.one BigQ.mul BigQ.eq Z_of_N BigQ.power.
Lemma BigQ_eq_bool_correct :
forall x y, BigQ.eq_bool x y = true -> x==y.
Lemma BigQ_eq_bool_complete :
forall x y, x==y -> BigQ.eq_bool x y = true.
Ltac BigQcst t :=
match t with
| BigQ.zero => BigQ.zero
| BigQ.one => BigQ.one
| BigQ.minus_one => BigQ.minus_one
| _ => NotConstant
end.
Add Field BigQfield : BigQfieldth
(decidable BigQ_eq_bool_correct,
completeness BigQ_eq_bool_complete,
constants [BigQcst],
power_tac BigQpowerth [Qpow_tac]).
Section Examples.
Let ex1 : forall x y z, (x+y)*z == (x*z)+(y*z).
Qed.
Let ex8 : forall x, x ^ 1 == x.
Qed.
Let ex10 : forall x y, ~(y==BigQ.zero) -> (x/y)*y == x.
Qed.
End Examples.