Require Export BigZ.
Require Import Field Qfield QSig QMake Orders GenericMinMax.

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) = Z.abs (BigZ.to_Z z).
End BigN_BigZ.

Delimit Scope bigQ_scope with bigQ.

Module BigQ <: QType <: OrderedTypeFull <: TotalOrder.
 Include QMake.Make BigN BigZ BigN_BigZ [scope abstract_scope to bigQ_scope].
 Include !QProperties <+ HasEqBool2Dec
  <+ !MinMaxLogicalProperties <+ !MinMaxDecProperties.
 Ltac order := Private_Tac.order.
End BigQ.

Local Open Scope bigQ_scope.

Notation bigQ := BigQ.t.

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) (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_scope.
Notation "x < y <= z" := (x<y /\ y<=z) : bigQ_scope.
Notation "x <= y < z" := (x<=y /\ y<z) : bigQ_scope.
Notation "x <= y <= z" := (x<=y /\ y<=z) : bigQ_scope.
Notation "[ q ]" := (BigQ.to_Q q) : bigQ_scope.

Lemma BigQfieldth :
 field_theory 0 1 BigQ.add BigQ.mul BigQ.sub BigQ.opp
  BigQ.div BigQ.inv BigQ.eq.

Lemma BigQpowerth :
 power_theory 1 BigQ.mul BigQ.eq Z.of_N BigQ.power.

Ltac isBigQcst t :=
 match t with
 | BigQ.Qz ?t => isBigZcst t
 | BigQ.Qq ?n ?d => match isBigZcst n with
             | true => isBigNcst d
             | false => constr:false
             end
 | BigQ.zero => constr:true
 | BigQ.one => constr:true
 | BigQ.minus_one => constr:true
 | _ => constr:false
 end.

Ltac BigQcst t :=
 match isBigQcst t with
 | true => constr:t
 | false => constr:NotConstant
 end.

Add Field BigQfield : BigQfieldth
 (decidable BigQ.eqb_correct,
  completeness BigQ.eqb_complete,
  constants [BigQcst],
  power_tac BigQpowerth [Qpow_tac]).

Section TestField.

Let ex1 : forall x y z, (x+y)*z == (x*z)+(y*z).
Qed.

Let ex8 : forall x, x ^ 2 == x*x.
Qed.

Let ex10 : forall x y, y!=0 -> (x/y)*y == x.
Qed.

End TestField.

Ltac bigQ_order := BigQ.order.

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

Section TestQify.
Let test : forall x : bigQ, 0+x == 1*x.
End TestQify.