Library Coq.Numbers.Rational.BigQ.BigQ



Require Import Field Qfield BigN BigZ QSig QMake.

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.