(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)
(*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
(************************************************************************)

(*i $Id: QpMake.v 11027 2008-06-01 13:28:59Z letouzey $ i*)

Require Import Bool.
Require Import ZArith.
Require Import Znumtheory.
Require Import BigNumPrelude.
Require Import Arith.
Require Export BigN.
Require Export BigZ.
Require Import QArith.
Require Import Qcanon.
Require Import Qpower.
Require Import QMake_base.

Notation Nspec_lt := BigNAxiomsMod.NZOrdAxiomsMod.spec_lt.
Notation Nspec_le := BigNAxiomsMod.NZOrdAxiomsMod.spec_le.

Module Qp.

 (** The notation of a rational number is either an integer x,
     interpreted as itself or a pair (x,y) of an integer x and a naturel
     number y interpreted as x/(y+1). *)

 Definition t := q_type.

 Definition zero: t := Qz BigZ.zero.
 Definition one: t := Qz BigZ.one.
 Definition minus_one: t := Qz BigZ.minus_one.

 Definition of_Z x: t := Qz (BigZ.of_Z x).

 Definition d_to_Z d := BigZ.Pos (BigN.succ d).

 Definition of_Q q: t := 
 match q with x # y =>
  Qq (BigZ.of_Z x) (BigN.pred (BigN.of_N (Npos y)))
 end.

 Definition of_Qc q := of_Q (this q).

 Definition to_Q (q: t) := 
 match q with 
  Qz x => BigZ.to_Z x # 1
 |Qq x y => BigZ.to_Z x # Z2P (BigN.to_Z (BigN.succ y))
 end.

 Definition to_Qc q := !!(to_Q q).

 Notation "[[ x ]]" := (to_Qc x).

 Notation "[ x ]" := (to_Q x).

 Theorem spec_to_Q: forall q: Q, [of_Q q] = q.
 intros (x,y); simpl.
 rewrite BigZ.spec_of_Z; auto.
 rewrite BigN.spec_succ; simpl. simpl.
 rewrite BigN.spec_pred; rewrite (BigN.spec_of_pos).
 replace (Zpos y - 1 + 1)%Z with (Zpos y); auto; ring.
 red; auto.
 Qed.

 Theorem spec_to_Qc: forall q, [[of_Qc q]] = q.
 intros (x, Hx); unfold of_Qc, to_Qc; simpl.
 apply Qc_decomp; simpl.
 intros; rewrite spec_to_Q; auto.
 Qed.

 Definition opp (x: t): t :=
  match x with
  | Qz zx => Qz (BigZ.opp zx)
  | Qq nx dx => Qq (BigZ.opp nx) dx
  end.


 Theorem spec_opp: forall q, ([opp q] = -[q])%Q.
 intros [z | x y]; simpl.
 rewrite BigZ.spec_opp; auto.
 rewrite BigZ.spec_opp; auto.
 Qed.


 Theorem spec_oppc: forall q, [[opp q]] = -[[q]].
 intros q; unfold Qcopp, to_Qc, Q2Qc.
 apply Qc_decomp; intros _ _; unfold this.
 rewrite spec_opp.
 rewrite <- Qred_opp.
 rewrite Qred_involutive; auto.
 Qed.

 Definition compare (x y: t) :=
  match x, y with
  | Qz zx, Qz zy => BigZ.compare zx zy
  | Qz zx, Qq ny dy => BigZ.compare (BigZ.mul zx (d_to_Z dy)) ny
  | Qq nx dy, Qz zy => BigZ.compare nx (BigZ.mul zy (d_to_Z dy))
  | Qq nx dx, Qq ny dy =>
    BigZ.compare (BigZ.mul nx (d_to_Z dy)) (BigZ.mul ny (d_to_Z dx))
  end.

 Theorem spec_compare: forall q1 q2,
  compare q1 q2 = ([q1] ?= [q2])%Q.
 intros [z1 | x1 y1] [z2 | x2 y2]; unfold Qcompare; simpl.
 repeat rewrite Zmult_1_r.
 generalize (BigZ.spec_compare z1 z2); case BigZ.compare; intros H; auto.
 rewrite H; rewrite Zcompare_refl; auto.
 rewrite Zmult_1_r.
 rewrite BigN.spec_succ.
 rewrite Z2P_correct; auto with zarith.
  2: generalize (BigN.spec_pos y2); auto with zarith.
 generalize (BigZ.spec_compare (z1 * d_to_Z y2) x2)%bigZ; case BigZ.compare; 
   intros H; rewrite <- H.
 rewrite BigZ.spec_mul; unfold d_to_Z; simpl.
 rewrite BigN.spec_succ.
 rewrite Zcompare_refl; auto.
 rewrite BigZ.spec_mul; unfold d_to_Z; simpl.
 rewrite BigN.spec_succ; auto.
 rewrite BigZ.spec_mul; unfold d_to_Z; simpl.
 rewrite BigN.spec_succ; auto.
 rewrite Zmult_1_r.
 rewrite BigN.spec_succ.
 rewrite Z2P_correct; auto with zarith.
  2: generalize (BigN.spec_pos y1); auto with zarith.
 generalize (BigZ.spec_compare x1 (z2 * d_to_Z y1))%bigZ; case BigZ.compare;
    rewrite BigZ.spec_mul; unfold d_to_Z; simpl;  
    rewrite BigN.spec_succ; intros H; auto.
 rewrite H; rewrite Zcompare_refl; auto.
 repeat rewrite BigN.spec_succ; auto.
 repeat rewrite Z2P_correct; auto with zarith.
  2: generalize (BigN.spec_pos y1); auto with zarith.
  2: generalize (BigN.spec_pos y2); auto with zarith.
 generalize (BigZ.spec_compare (x1 * d_to_Z  y2)
                  (x2 * d_to_Z y1))%bigZ; case BigZ.compare;
    repeat rewrite BigZ.spec_mul; unfold d_to_Z; simpl;  
    repeat rewrite BigN.spec_succ; intros H; auto.
 rewrite H; auto.
 rewrite Zcompare_refl; auto.
 Qed.


 Theorem spec_comparec: forall q1 q2,
  compare q1 q2 = ([[q1]] ?= [[q2]]).
 unfold Qccompare, to_Qc. 
 intros q1 q2; rewrite spec_compare; simpl.
 apply Qcompare_comp; apply Qeq_sym; apply Qred_correct.
 Qed.

(* Inv d > 0, Pour la forme normal unique on veut d > 1 *)
 Definition norm n d: t :=
  if BigZ.eq_bool n BigZ.zero then zero
  else
    let gcd := BigN.gcd (BigZ.to_N n) d in
    if BigN.eq_bool gcd BigN.one then Qq n (BigN.pred d)
    else	
      let n := BigZ.div n (BigZ.Pos gcd) in
      let d := BigN.div d gcd in
      if BigN.eq_bool d BigN.one then Qz n
      else Qq n (BigN.pred d).

 Theorem spec_norm: forall n q, 
    ((0 < BigN.to_Z q)%Z -> [norm n q] == [Qq n (BigN.pred q)])%Q.
 intros p q; unfold norm; intros Hq.
 assert (Hp := BigN.spec_pos (BigZ.to_N p)).
 match goal with  |- context[BigZ.eq_bool ?X ?Y] => 
   generalize (BigZ.spec_eq_bool X Y); case BigZ.eq_bool
 end; auto; rewrite BigZ.spec_0; intros H1.
   red; simpl; rewrite H1; ring.
 case (Zle_lt_or_eq _ _ Hp); clear Hp; intros Hp.
 case (Zle_lt_or_eq _ _ 
      (Zgcd_is_pos (BigN.to_Z (BigZ.to_N p)) (BigN.to_Z q))); intros H4.
 2: generalize Hq; rewrite (Zgcd_inv_0_r _ _ (sym_equal H4)); auto with zarith.
 2: red; simpl; auto with zarith.
 match goal with  |- context[BigN.eq_bool ?X ?Y] => 
   generalize (BigN.spec_eq_bool X Y); case BigN.eq_bool
 end; auto; rewrite BigN.spec_1; intros H2.
   apply Qeq_refl.
 match goal with  |- context[BigN.eq_bool ?X ?Y] => 
   generalize (BigN.spec_eq_bool X Y); case BigN.eq_bool
 end; auto; rewrite BigN.spec_1.
 red; simpl.
 rewrite BigZ.spec_div; simpl; rewrite BigN.spec_gcd; auto with zarith.
 rewrite BigN.spec_div; simpl; rewrite BigN.spec_gcd; auto with zarith.
 rewrite Zmult_1_r.
 rewrite BigN.succ_pred by (rewrite Nspec_lt, BigN.spec_0; auto).
 rewrite Z2P_correct; auto with zarith.
 rewrite spec_to_N; intros; rewrite Zgcd_div_swap; auto.
 rewrite H; ring.
 intros H3.
 red; simpl.
 rewrite BigZ.spec_div; simpl; rewrite BigN.spec_gcd; auto with zarith.
 rewrite BigN.succ_pred by (rewrite Nspec_lt, BigN.spec_0; auto).
 assert (F: (0 < BigN.to_Z (q / BigN.gcd (BigZ.to_N p) q)%bigN)%Z).
   rewrite BigN.spec_div; auto with zarith.
   rewrite BigN.spec_gcd.
   apply Zgcd_div_pos; auto.
   rewrite BigN.spec_gcd; auto.
 rewrite BigN.succ_pred by (rewrite Nspec_lt, BigN.spec_0; auto).
 rewrite Z2P_correct; auto.
 rewrite Z2P_correct; auto.
 rewrite BigN.spec_div; simpl; rewrite BigN.spec_gcd; auto with zarith.
 rewrite spec_to_N; apply Zgcd_div_swap; auto.
 case H1; rewrite spec_to_N; rewrite <- Hp; ring.
 Qed.

 Theorem spec_normc: forall n q, 
    (0 < BigN.to_Z q)%Z -> [[norm n q]] = [[Qq n (BigN.pred q)]].
 intros n q H; unfold to_Qc, Q2Qc.
 apply Qc_decomp; intros _ _; unfold this.
 apply Qred_complete; apply spec_norm; auto.
 Qed.
   
 Definition add (x y: t): t :=
  match x, y with
  | Qz zx, Qz zy => Qz (BigZ.add zx zy)
  | Qz zx, Qq ny dy => Qq (BigZ.add (BigZ.mul zx (d_to_Z dy)) ny) dy
  | Qq nx dx, Qz zy => Qq (BigZ.add nx (BigZ.mul zy (d_to_Z dx))) dx
  | Qq nx dx, Qq ny dy => 
    let dx' := BigN.succ dx in
    let dy' := BigN.succ dy in
    let n := BigZ.add (BigZ.mul nx (BigZ.Pos dy')) (BigZ.mul ny (BigZ.Pos dx')) in
    let d := BigN.pred (BigN.mul dx' dy') in
    Qq n d
  end. 

 Theorem spec_d_to_Z: forall dy,
     (BigZ.to_Z (d_to_Z dy) = BigN.to_Z dy + 1)%Z.
 intros dy; unfold d_to_Z; simpl.
 rewrite BigN.spec_succ; auto.
 Qed.

 Theorem spec_succ_pos: forall p,
  (0 < BigN.to_Z (BigN.succ p))%Z.
 intros p; rewrite BigN.spec_succ;
   generalize (BigN.spec_pos p); auto with zarith.
 Qed.

 Theorem spec_add x y: ([add x y] == [x] + [y])%Q.
 intros [x | nx dx] [y | ny dy]; unfold Qplus; simpl.
 rewrite BigZ.spec_add; repeat rewrite Zmult_1_r; auto.
  apply Qeq_refl; auto.
 assert (F1:= BigN.spec_pos dy).
 rewrite Zmult_1_r.
 simpl; rewrite Z2P_correct; rewrite BigN.spec_succ; auto with zarith.
 rewrite BigZ.spec_add; rewrite BigZ.spec_mul.
 rewrite spec_d_to_Z; apply Qeq_refl.
 assert (F1:= BigN.spec_pos dx).
 rewrite Zmult_1_r; rewrite Pmult_1_r.
 simpl; rewrite Z2P_correct; rewrite BigN.spec_succ; auto with zarith.
 rewrite BigZ.spec_add; rewrite BigZ.spec_mul.
 rewrite spec_d_to_Z; apply Qeq_refl.
 repeat rewrite BigN.spec_succ.
 assert (Fx: (0 < BigN.to_Z dx + 1)%Z).
   generalize (BigN.spec_pos dx); auto with zarith.
 assert (Fy: (0 < BigN.to_Z dy + 1)%Z).
   generalize (BigN.spec_pos dy); auto with zarith.
 repeat rewrite BigN.spec_pred.
 rewrite BigZ.spec_add; repeat rewrite BigN.spec_mul;
   repeat rewrite BigN.spec_succ.
 assert (tmp: forall x, (x-1+1 = x)%Z); [intros; ring | rewrite tmp; clear tmp].
 repeat rewrite Z2P_correct; auto.
 repeat rewrite BigZ.spec_mul; simpl.
 repeat rewrite BigN.spec_succ.
 assert (tmp: 
  (forall a b, 0 < a -> 0 < b -> Z2P (a * b) = (Z2P a * Z2P b)%positive)%Z).
  intros [|a|a] [|b|b]; simpl; auto; intros; apply False_ind; auto with zarith.
 rewrite tmp; auto; apply Qeq_refl.
 rewrite BigN.spec_mul; repeat rewrite BigN.spec_succ; auto with zarith.
 apply Zmult_lt_0_compat; auto.
 Qed.

 Theorem spec_addc x y: [[add x y]] = [[x]] + [[y]].
 intros x y; unfold to_Qc.
 apply trans_equal with (!! ([x] + [y])).
 unfold Q2Qc.
 apply Qc_decomp; intros _ _; unfold this.
 apply Qred_complete; apply spec_add.
 unfold Qcplus, Q2Qc.
 apply Qc_decomp; intros _ _; unfold this.
 apply Qred_complete.
 apply Qplus_comp; apply Qeq_sym; apply Qred_correct.
 Qed.

 Definition add_norm (x y: t): t := 
  match x, y with
  | Qz zx, Qz zy => Qz (BigZ.add zx zy)
  | Qz zx, Qq ny dy => 
    let d := BigN.succ dy in
    norm (BigZ.add (BigZ.mul zx (BigZ.Pos d)) ny) d 
  | Qq nx dx, Qz zy =>
    let d := BigN.succ dx in
    norm (BigZ.add (BigZ.mul zy (BigZ.Pos d)) nx) d
  | Qq nx dx, Qq ny dy =>
    let dx' := BigN.succ dx in
    let dy' := BigN.succ dy in
    let n := BigZ.add (BigZ.mul nx (BigZ.Pos dy')) (BigZ.mul ny (BigZ.Pos dx')) in
    let d := BigN.mul dx' dy' in
    norm n d 
  end.

 Theorem spec_add_norm x y: ([add_norm x y] == [x] + [y])%Q.
 intros x y; rewrite <- spec_add.
 unfold add_norm, add; case x; case y.
  intros; apply Qeq_refl.
 intros p1 n p2.
 match goal with |- [norm ?X ?Y] == _ =>
  apply Qeq_trans with ([Qq X (BigN.pred Y)]);
  [apply spec_norm | idtac]
 end.
 rewrite BigN.spec_succ; generalize (BigN.spec_pos n); auto with zarith.
 simpl.
 repeat rewrite BigZ.spec_add.
 repeat rewrite BigZ.spec_mul; simpl.
 rewrite BigN.succ_pred; try apply Qeq_refl; apply lt_0_succ.
 intros p1 n p2.
 match goal with |- [norm ?X ?Y] == _ =>
  apply Qeq_trans with ([Qq X (BigN.pred Y)]);
  [apply spec_norm | idtac]
 end.
 rewrite BigN.spec_succ; generalize (BigN.spec_pos p2); auto with zarith.
 simpl.
 repeat rewrite BigZ.spec_add.
 repeat rewrite BigZ.spec_mul; simpl.
 rewrite BinInt.Zplus_comm.
 rewrite BigN.succ_pred; try apply Qeq_refl; apply lt_0_succ.
 intros p1 q1 p2 q2.
 match goal with |- [norm ?X ?Y] == _ =>
  apply Qeq_trans with ([Qq X (BigN.pred Y)]);
  [apply spec_norm | idtac]
 end; try apply Qeq_refl.
 rewrite BigN.spec_mul.
 apply Zmult_lt_0_compat; apply spec_succ_pos.
 Qed.

 Theorem spec_add_normc x y: [[add_norm x y]] = [[x]] + [[y]].
 intros x y; unfold to_Qc.
 apply trans_equal with (!! ([x] + [y])).
 unfold Q2Qc.
 apply Qc_decomp; intros _ _; unfold this.
 apply Qred_complete; apply spec_add_norm.
 unfold Qcplus, Q2Qc.
 apply Qc_decomp; intros _ _; unfold this.
 apply Qred_complete.
 apply Qplus_comp; apply Qeq_sym; apply Qred_correct.
 Qed.
 
 Definition sub (x y: t): t := add x (opp y).

 Theorem spec_sub x y: ([sub x y] == [x] - [y])%Q.
 intros x y; unfold sub; rewrite spec_add.
 rewrite spec_opp; ring.
 Qed.

 Theorem spec_subc x y: [[sub x y]] = [[x]] - [[y]].
 intros x y; unfold sub; rewrite spec_addc.
 rewrite spec_oppc; ring.
 Qed.

 Definition sub_norm x y := add_norm x (opp y).

 Theorem spec_sub_norm x y: ([sub_norm x y] == [x] - [y])%Q.
 intros x y; unfold sub_norm; rewrite spec_add_norm.
 rewrite spec_opp; ring.
 Qed.

 Theorem spec_sub_normc x y: [[sub_norm x y]] = [[x]] - [[y]].
 intros x y; unfold sub_norm; rewrite spec_add_normc.
 rewrite spec_oppc; ring.
 Qed.


 Definition mul (x y: t): t :=
  match x, y with
  | Qz zx, Qz zy => Qz (BigZ.mul zx zy)
  | Qz zx, Qq ny dy => Qq (BigZ.mul zx ny) dy
  | Qq nx dx, Qz zy => Qq (BigZ.mul nx zy) dx
  | Qq nx dx, Qq ny dy => 
    Qq (BigZ.mul nx ny) (BigN.pred (BigN.mul (BigN.succ dx) (BigN.succ dy)))
  end.

 Theorem spec_mul x y: ([mul x y] == [x] * [y])%Q.
 intros [x | nx dx] [y | ny dy]; unfold Qmult; simpl.
 rewrite BigZ.spec_mul; repeat rewrite Zmult_1_r; auto.
  apply Qeq_refl; auto.
 rewrite BigZ.spec_mul; apply Qeq_refl.
 rewrite BigZ.spec_mul; rewrite Pmult_1_r; auto.
  apply Qeq_refl; auto.
 assert (F1:= spec_succ_pos dx).
 assert (F2:= spec_succ_pos dy).
 rewrite BigN.succ_pred.
 rewrite BigN.spec_mul; rewrite BigZ.spec_mul.
 assert (tmp: 
  (forall a b, 0 < a -> 0 < b -> Z2P (a * b) = (Z2P a * Z2P b)%positive)%Z).
  intros [|a|a] [|b|b]; simpl; auto; intros; apply False_ind; auto with zarith.
 rewrite tmp; auto; apply Qeq_refl.
 rewrite Nspec_lt, BigN.spec_0, BigN.spec_mul; auto.
 apply Zmult_lt_0_compat; apply spec_succ_pos.
 Qed.

 Theorem spec_mulc x y: [[mul x y]] = [[x]] * [[y]].
 intros x y; unfold to_Qc.
 apply trans_equal with (!! ([x] * [y])).
 unfold Q2Qc.
 apply Qc_decomp; intros _ _; unfold this.
 apply Qred_complete; apply spec_mul.
 unfold Qcmult, Q2Qc.
 apply Qc_decomp; intros _ _; unfold this.
 apply Qred_complete.
 apply Qmult_comp; apply Qeq_sym; apply Qred_correct.
 Qed.

 Definition mul_norm (x y: t): t := 
  match x, y with
  | Qz zx, Qz zy => Qz (BigZ.mul zx zy)
  | Qz zx, Qq ny dy =>
    if BigZ.eq_bool zx BigZ.zero then zero
    else	
      let d := BigN.succ dy in
      let gcd := BigN.gcd (BigZ.to_N zx) d in
      if BigN.eq_bool gcd BigN.one then Qq (BigZ.mul zx ny) dy
      else 
        let zx := BigZ.div zx (BigZ.Pos gcd) in
        let d := BigN.div d gcd in
        if BigN.eq_bool d BigN.one then Qz (BigZ.mul zx ny)
        else Qq (BigZ.mul zx ny) (BigN.pred d)
  | Qq nx dx, Qz zy =>   
    if BigZ.eq_bool zy BigZ.zero then zero
    else	
      let d := BigN.succ dx in
      let gcd := BigN.gcd (BigZ.to_N zy) d in
      if BigN.eq_bool gcd BigN.one then Qq (BigZ.mul zy nx) dx
      else 
        let zy := BigZ.div zy (BigZ.Pos gcd) in
        let d := BigN.div d gcd in
        if BigN.eq_bool d BigN.one then Qz (BigZ.mul zy nx)
        else Qq (BigZ.mul zy nx) (BigN.pred d)
  | Qq nx dx, Qq ny dy => 
    norm (BigZ.mul nx ny) (BigN.mul (BigN.succ dx) (BigN.succ dy))
  end.

 Theorem spec_mul_norm x y: ([mul_norm x y] == [x] * [y])%Q.
 intros x y; rewrite <- spec_mul.
 unfold mul_norm, mul; case x; case y.
  intros; apply Qeq_refl.
 intros p1 n p2.
 match goal with  |- context[BigZ.eq_bool ?X ?Y] => 
   generalize (BigZ.spec_eq_bool X Y); case BigZ.eq_bool
 end; unfold zero, to_Q; repeat rewrite BigZ.spec_0; intros H.
 rewrite BigZ.spec_mul; rewrite H; red; auto.
 assert (F: (0 < BigN.to_Z (BigZ.to_N p2))%Z).
  case (Zle_lt_or_eq _ _ (BigN.spec_pos (BigZ.to_N p2))); auto.
  intros H1; case H; rewrite spec_to_N; rewrite <- H1; ring.
 assert (F1: (0 < BigN.to_Z (BigN.succ n))%Z).
  rewrite BigN.spec_succ; generalize (BigN.spec_pos n); auto with zarith.
 assert (F2: (0 < Zgcd (BigN.to_Z (BigZ.to_N p2)) (BigN.to_Z (BigN.succ n)))%Z).
   case (Zle_lt_or_eq _ _ (Zgcd_is_pos (BigN.to_Z (BigZ.to_N p2))
                                       (BigN.to_Z (BigN.succ n)))); intros H3; auto.
   generalize F; rewrite (Zgcd_inv_0_l _ _ (sym_equal H3)); auto with zarith.
 match goal with  |- context[BigN.eq_bool ?X ?Y] => 
   generalize (BigN.spec_eq_bool X Y); case BigN.eq_bool
 end; rewrite BigN.spec_1; intros H1.
  intros; apply Qeq_refl.
 match goal with  |- context[BigN.eq_bool ?X ?Y] => 
   generalize (BigN.spec_eq_bool X Y); case BigN.eq_bool
 end; rewrite BigN.spec_1.
 rewrite BigN.spec_div; rewrite BigN.spec_gcd;
   auto with zarith.
 intros H2.
 red; simpl.
 repeat rewrite BigZ.spec_mul.
 rewrite BigZ.spec_div; simpl; rewrite BigN.spec_gcd; auto with zarith.
 rewrite Z2P_correct; auto with zarith.
 rewrite spec_to_N.
 rewrite Zmult_1_r; repeat rewrite <- Zmult_assoc.
 rewrite (Zmult_comm (BigZ.to_Z p1)).
 repeat rewrite Zmult_assoc.
 rewrite Zgcd_div_swap; auto with zarith.
 rewrite H2; ring.
 intros H2.
 red; simpl.
 repeat rewrite BigZ.spec_mul.
 rewrite BigZ.spec_div; simpl; rewrite BigN.spec_gcd; auto with zarith.
 rewrite Z2P_correct; auto with zarith.
 rewrite (spec_to_N p2).
 case (Zle_lt_or_eq _ _
       (BigN.spec_pos  (BigN.succ n / 
                         BigN.gcd (BigZ.to_N p2) 
                                  (BigN.succ n)))%bigN); intros F3.
 rewrite BigN.succ_pred; auto with zarith.
 rewrite Z2P_correct; auto with zarith.
 rewrite BigN.spec_div; simpl; rewrite BigN.spec_gcd; auto with zarith.
 repeat rewrite <- Zmult_assoc.
 rewrite (Zmult_comm (BigZ.to_Z p1)).
 repeat rewrite Zmult_assoc.
 rewrite Zgcd_div_swap; auto; try ring.
 rewrite Nspec_lt, BigN.spec_0; auto.
 apply False_ind; generalize F1.
 rewrite (Zdivide_Zdiv_eq
          (Zgcd (BigN.to_Z (BigZ.to_N p2)) (BigN.to_Z (BigN.succ n)))
           (BigN.to_Z (BigN.succ n))); auto.
 generalize F3; rewrite BigN.spec_div; rewrite BigN.spec_gcd;
   auto with zarith.
 intros HH; rewrite <- HH; auto with zarith.
 assert (FF:= Zgcd_is_gcd (BigN.to_Z (BigZ.to_N p2))
           (BigN.to_Z (BigN.succ n))); inversion FF; auto.
 intros p1 p2 n.
 match goal with  |- context[BigZ.eq_bool ?X ?Y] => 
   generalize (BigZ.spec_eq_bool X Y); case BigZ.eq_bool
 end; unfold zero, to_Q; repeat rewrite BigZ.spec_0; intros H.
 rewrite BigZ.spec_mul; rewrite H; red; simpl; ring.
 assert (F: (0 < BigN.to_Z (BigZ.to_N p1))%Z).
  case (Zle_lt_or_eq _ _ (BigN.spec_pos (BigZ.to_N p1))); auto.
  intros H1; case H; rewrite spec_to_N; rewrite <- H1; ring.
 assert (F1: (0 < BigN.to_Z (BigN.succ n))%Z).
  rewrite BigN.spec_succ; generalize (BigN.spec_pos n); auto with zarith.
 assert (F2: (0 < Zgcd (BigN.to_Z (BigZ.to_N p1)) (BigN.to_Z (BigN.succ n)))%Z).
   case (Zle_lt_or_eq _ _ (Zgcd_is_pos (BigN.to_Z (BigZ.to_N p1))
                                       (BigN.to_Z (BigN.succ n)))); intros H3; auto.
   generalize F; rewrite (Zgcd_inv_0_l _ _ (sym_equal H3)); auto with zarith.
 match goal with  |- context[BigN.eq_bool ?X ?Y] => 
   generalize (BigN.spec_eq_bool X Y); case BigN.eq_bool
 end; rewrite BigN.spec_1; intros H1.
  intros; repeat rewrite BigZ.spec_mul; rewrite Zmult_comm; apply Qeq_refl.
 match goal with  |- context[BigN.eq_bool ?X ?Y] => 
   generalize (BigN.spec_eq_bool X Y); case BigN.eq_bool
 end; rewrite BigN.spec_1.
 rewrite BigN.spec_div; rewrite BigN.spec_gcd;
   auto with zarith.
 intros H2.
 red; simpl.
 repeat rewrite BigZ.spec_mul.
 rewrite BigZ.spec_div; simpl; rewrite BigN.spec_gcd; auto with zarith.
 rewrite Z2P_correct; auto with zarith.
 rewrite spec_to_N.
 rewrite Zmult_1_r; repeat rewrite <- Zmult_assoc.
 rewrite (Zmult_comm (BigZ.to_Z p2)).
 repeat rewrite Zmult_assoc.
 rewrite Zgcd_div_swap; auto with zarith.
 rewrite H2; ring.
 intros H2.
 red; simpl.
 repeat rewrite BigZ.spec_mul.
 rewrite BigZ.spec_div; simpl; rewrite BigN.spec_gcd; auto with zarith.
 rewrite Z2P_correct; auto with zarith.
 rewrite (spec_to_N p1).
 case (Zle_lt_or_eq _ _
       (BigN.spec_pos  (BigN.succ n / 
                         BigN.gcd (BigZ.to_N p1) 
                                  (BigN.succ n)))%bigN); intros F3.
 rewrite BigN.succ_pred; auto with zarith.
 rewrite Z2P_correct; auto with zarith.
 rewrite BigN.spec_div; simpl; rewrite BigN.spec_gcd; auto with zarith.
 repeat rewrite <- Zmult_assoc.
 rewrite (Zmult_comm (BigZ.to_Z p2)).
 repeat rewrite Zmult_assoc.
 rewrite Zgcd_div_swap; auto; try ring.
 rewrite Nspec_lt, BigN.spec_0; auto.
 apply False_ind; generalize F1.
 rewrite (Zdivide_Zdiv_eq
          (Zgcd (BigN.to_Z (BigZ.to_N p1)) (BigN.to_Z (BigN.succ n)))
           (BigN.to_Z (BigN.succ n))); auto.
 generalize F3; rewrite BigN.spec_div; rewrite BigN.spec_gcd;
   auto with zarith.
 intros HH; rewrite <- HH; auto with zarith.
 assert (FF:= Zgcd_is_gcd (BigN.to_Z (BigZ.to_N p1))
           (BigN.to_Z (BigN.succ n))); inversion FF; auto.
 intros p1 n1 p2 n2.
 match goal with |- [norm ?X ?Y] == _ =>
  apply Qeq_trans with ([Qq X (BigN.pred Y)]);
  [apply spec_norm | idtac]
 end; try  apply Qeq_refl.
 rewrite BigN.spec_mul.
 apply Zmult_lt_0_compat; rewrite BigN.spec_succ;
    generalize (BigN.spec_pos n1) (BigN.spec_pos n2); auto with zarith.
 Qed.

 Theorem spec_mul_normc x y: [[mul_norm x y]] = [[x]] * [[y]].
 intros x y; unfold to_Qc.
 apply trans_equal with (!! ([x] * [y])).
 unfold Q2Qc.
 apply Qc_decomp; intros _ _; unfold this.
 apply Qred_complete; apply spec_mul_norm.
 unfold Qcmult, Q2Qc.
 apply Qc_decomp; intros _ _; unfold this.
 apply Qred_complete.
 apply Qmult_comp; apply Qeq_sym; apply Qred_correct.
 Qed.

 Definition inv (x: t): t := 
  match x with
  | Qz (BigZ.Pos n) => 
    if BigN.eq_bool n BigN.zero then zero else Qq BigZ.one (BigN.pred n)
  | Qz (BigZ.Neg n) => 
    if BigN.eq_bool n BigN.zero then zero else Qq BigZ.minus_one (BigN.pred n)
  | Qq (BigZ.Pos n) d => 
    if BigN.eq_bool n BigN.zero then zero else Qq (BigZ.Pos (BigN.succ d)) (BigN.pred n)
  | Qq (BigZ.Neg n) d => 
    if BigN.eq_bool n BigN.zero then zero else Qq (BigZ.Neg (BigN.succ d)) (BigN.pred n)
  end.

 Theorem spec_inv x: ([inv x] == /[x])%Q.
 intros [ [x | x] | [nx | nx] dx]; unfold inv.
 match goal with  |- context[BigN.eq_bool ?X ?Y] => 
   generalize (BigN.spec_eq_bool X Y); case BigN.eq_bool
 end; rewrite BigN.spec_0; intros H.
  unfold zero, to_Q; rewrite BigZ.spec_0.
 unfold BigZ.to_Z; rewrite H; apply Qeq_refl.
 assert (F: (0 < BigN.to_Z x)%Z).
   case (Zle_lt_or_eq _ _ (BigN.spec_pos x)); auto with zarith.
 unfold to_Q; rewrite BigZ.spec_1.
 rewrite BigN.succ_pred by (rewrite Nspec_lt, BigN.spec_0; auto).
 red; unfold Qinv; simpl.
 generalize F; case BigN.to_Z; auto with zarith.
 intros p Hp; discriminate Hp.
 match goal with  |- context[BigN.eq_bool ?X ?Y] => 
   generalize (BigN.spec_eq_bool X Y); case BigN.eq_bool
 end; rewrite BigN.spec_0; intros H.
  unfold zero, to_Q; rewrite BigZ.spec_0.
 unfold BigZ.to_Z; rewrite H; apply Qeq_refl.
 assert (F: (0 < BigN.to_Z x)%Z).
   case (Zle_lt_or_eq _ _ (BigN.spec_pos x)); auto with zarith.
 red; unfold Qinv; simpl.
 rewrite BigN.succ_pred by (rewrite Nspec_lt, BigN.spec_0; auto).
 generalize F; case BigN.to_Z; simpl; auto with zarith.
 intros p Hp; discriminate Hp.
 match goal with  |- context[BigN.eq_bool ?X ?Y] => 
   generalize (BigN.spec_eq_bool X Y); case BigN.eq_bool
 end; rewrite BigN.spec_0; intros H.
  unfold zero, to_Q; rewrite BigZ.spec_0.
 unfold BigZ.to_Z; rewrite H; apply Qeq_refl.
 assert (F: (0 < BigN.to_Z nx)%Z).
   case (Zle_lt_or_eq _ _ (BigN.spec_pos nx)); auto with zarith.
 red; unfold Qinv; simpl.
 rewrite BigN.succ_pred by (rewrite Nspec_lt, BigN.spec_0; auto).
 rewrite BigN.spec_succ; rewrite Z2P_correct; auto with zarith.
 generalize F; case BigN.to_Z; auto with zarith.
 intros p Hp; discriminate Hp.
 generalize (BigN.spec_pos dx); auto with zarith.
 match goal with  |- context[BigN.eq_bool ?X ?Y] => 
   generalize (BigN.spec_eq_bool X Y); case BigN.eq_bool
 end; rewrite BigN.spec_0; intros H.
  unfold zero, to_Q; rewrite BigZ.spec_0.
 unfold BigZ.to_Z; rewrite H; apply Qeq_refl.
 assert (F: (0 < BigN.to_Z nx)%Z).
   case (Zle_lt_or_eq _ _ (BigN.spec_pos nx)); auto with zarith.
 red; unfold Qinv; simpl.
 rewrite BigN.succ_pred by (rewrite Nspec_lt, BigN.spec_0; auto).
 rewrite BigN.spec_succ; rewrite Z2P_correct; auto with zarith.
 generalize F; case BigN.to_Z; auto with zarith.
 simpl; intros.
 match goal with  |- (?X = Zneg ?Y)%Z => 
   replace (Zneg Y) with (-(Zpos Y))%Z;
   try rewrite Z2P_correct; auto with zarith
 end.
 rewrite Zpos_mult_morphism; 
   rewrite Z2P_correct; auto with zarith; try ring.
 generalize (BigN.spec_pos dx); auto with zarith.
 intros p Hp; discriminate Hp.
 generalize (BigN.spec_pos dx); auto with zarith.
 Qed.

 Theorem spec_invc x: [[inv x]] =  /[[x]].
 intros x; unfold to_Qc.
 apply trans_equal with (!! (/[x])).
 unfold Q2Qc.
 apply Qc_decomp; intros _ _; unfold this.
 apply Qred_complete; apply spec_inv.
 unfold Qcinv, Q2Qc.
 apply Qc_decomp; intros _ _; unfold this.
 apply Qred_complete.
 apply Qinv_comp; apply Qeq_sym; apply Qred_correct.
 Qed.

Definition inv_norm x := 
 match x with
 | Qz (BigZ.Pos n) => 
      if BigN.eq_bool n BigN.zero then zero else
      if BigN.eq_bool n BigN.one then x else Qq BigZ.one (BigN.pred n)
 | Qz (BigZ.Neg n) => 
      if BigN.eq_bool n BigN.zero then zero  else
      if BigN.eq_bool n BigN.one then x else Qq BigZ.minus_one (BigN.pred n)
 | Qq (BigZ.Pos n) d => let d := BigN.succ d in 
                  if BigN.eq_bool n BigN.zero then zero else
                  if BigN.eq_bool n BigN.one then Qz (BigZ.Pos d) 
                     else Qq (BigZ.Pos d) (BigN.pred n)
 | Qq (BigZ.Neg n) d => let d := BigN.succ d in 
                  if BigN.eq_bool n BigN.zero then zero else
                  if BigN.eq_bool n BigN.one then Qz (BigZ.Neg d) 
                     else Qq (BigZ.Neg d) (BigN.pred n)
 end.

 Theorem spec_inv_norm x: ([inv_norm x] == /[x])%Q.
 intros x; rewrite <- spec_inv.
 (case x; clear x); [intros [x | x] | intros nx dx];
  unfold inv_norm, inv.
 match goal with  |- context[BigN.eq_bool ?X ?Y] => 
   generalize (BigN.spec_eq_bool X Y); case BigN.eq_bool
 end; rewrite BigN.spec_0; intros H.
  apply Qeq_refl.
 assert (F: (0 < BigN.to_Z x)%Z).
   case (Zle_lt_or_eq _ _ (BigN.spec_pos x)); auto with zarith.
 match goal with  |- context[BigN.eq_bool ?X ?Y] => 
   generalize (BigN.spec_eq_bool X Y); case BigN.eq_bool
 end; rewrite BigN.spec_1; intros H1.
 red; simpl.
 rewrite BigN.succ_pred by (rewrite Nspec_lt, BigN.spec_0; auto).
 rewrite Z2P_correct; try rewrite H1; auto with zarith.
  apply Qeq_refl.
 match goal with  |- context[BigN.eq_bool ?X ?Y] => 
   generalize (BigN.spec_eq_bool X Y); case BigN.eq_bool
 end; rewrite BigN.spec_0; intros H.
  apply Qeq_refl.
 assert (F: (0 < BigN.to_Z x)%Z).
   case (Zle_lt_or_eq _ _ (BigN.spec_pos x)); auto with zarith.
 match goal with  |- context[BigN.eq_bool ?X ?Y] => 
   generalize (BigN.spec_eq_bool X Y); case BigN.eq_bool
 end; rewrite BigN.spec_1; intros H1.
 red; simpl.
 rewrite BigN.succ_pred by (rewrite Nspec_lt, BigN.spec_0; auto).
 rewrite Z2P_correct; try rewrite H1; auto with zarith.
  apply Qeq_refl.
 case nx; clear nx; intros nx.
 match goal with  |- context[BigN.eq_bool ?X ?Y] => 
   generalize (BigN.spec_eq_bool X Y); case BigN.eq_bool
 end; rewrite BigN.spec_0; intros H.
  apply Qeq_refl.
 match goal with  |- context[BigN.eq_bool ?X ?Y] => 
   generalize (BigN.spec_eq_bool X Y); case BigN.eq_bool
 end; rewrite BigN.spec_1; intros H1.
 red; simpl.
 rewrite BigN.succ_pred; try rewrite H1; auto with zarith.
 rewrite Nspec_lt, BigN.spec_0, H1; auto with zarith.
 apply Qeq_refl.
 match goal with  |- context[BigN.eq_bool ?X ?Y] => 
   generalize (BigN.spec_eq_bool X Y); case BigN.eq_bool
 end; rewrite BigN.spec_0; intros H.
  apply Qeq_refl.
 match goal with  |- context[BigN.eq_bool ?X ?Y] => 
   generalize (BigN.spec_eq_bool X Y); case BigN.eq_bool
 end; rewrite BigN.spec_1; intros H1.
 red; simpl.
 rewrite BigN.succ_pred; try rewrite H1; auto with zarith.
 rewrite Nspec_lt, BigN.spec_0, H1; auto with zarith.
 apply Qeq_refl.
 Qed.


 Definition div x y := mul x (inv y).

 Theorem spec_div x y: ([div x y] == [x] / [y])%Q.
 intros x y; unfold div; rewrite spec_mul; auto.
 unfold Qdiv; apply Qmult_comp.
 apply Qeq_refl.
 apply spec_inv; auto.
 Qed.

 Theorem spec_divc x y: [[div x y]] = [[x]] / [[y]].
 intros x y; unfold div; rewrite spec_mulc; auto.
 unfold Qcdiv; apply f_equal2 with (f := Qcmult); auto.
 apply spec_invc; auto. 
 Qed.

 Definition div_norm x y := mul_norm x (inv y).

 Theorem spec_div_norm x y: ([div_norm x y] == [x] / [y])%Q.
 intros x y; unfold div_norm; rewrite spec_mul_norm; auto.
 unfold Qdiv; apply Qmult_comp.
 apply Qeq_refl.
 apply spec_inv; auto.
 Qed.

 Theorem spec_div_normc x y: [[div_norm x y]] = [[x]] / [[y]].
 intros x y; unfold div_norm; rewrite spec_mul_normc; auto.
 unfold Qcdiv; apply f_equal2 with (f := Qcmult); auto.
 apply spec_invc; auto.
 Qed.


 Definition square (x: t): t :=
  match x with
  | Qz zx => Qz (BigZ.square zx)
  | Qq nx dx => Qq (BigZ.square nx) (BigN.pred (BigN.square (BigN.succ dx)))
  end.

 Theorem spec_square x: ([square x] == [x] ^ 2)%Q.
 intros [ x | nx dx]; unfold square.
 red; simpl; rewrite BigZ.spec_square; auto with zarith.
 red; simpl; rewrite BigZ.spec_square; auto with zarith.
 assert (F: (0 < BigN.to_Z (BigN.succ dx))%Z).
   rewrite BigN.spec_succ;
   case (Zle_lt_or_eq _ _ (BigN.spec_pos dx)); auto with zarith.
 assert (F1 : (0 < BigN.to_Z (BigN.square (BigN.succ dx)))%Z).
   rewrite BigN.spec_square; apply Zmult_lt_0_compat;
     auto with zarith.
 rewrite BigN.succ_pred by (rewrite Nspec_lt, BigN.spec_0; auto).
 rewrite Zpos_mult_morphism.
 repeat rewrite Z2P_correct; auto with zarith.
 repeat rewrite BigN.spec_succ; auto with zarith.
 rewrite BigN.spec_square; auto with zarith.
 repeat rewrite BigN.spec_succ; auto with zarith.
 Qed.

 Theorem spec_squarec x: [[square x]] =  [[x]]^2.
 intros x; unfold to_Qc.
 apply trans_equal with (!! ([x]^2)).
 unfold Q2Qc.
 apply Qc_decomp; intros _ _; unfold this.
 apply Qred_complete; apply spec_square.
 simpl Qcpower.
 replace (!! [x] * 1) with (!![x]); try ring.
 simpl.
 unfold Qcmult, Q2Qc.
 apply Qc_decomp; intros _ _; unfold this.
 apply Qred_complete.
 apply Qmult_comp; apply Qeq_sym; apply Qred_correct.
 Qed.

 Definition power_pos (x: t) p: t :=
  match x with
  | Qz zx => Qz (BigZ.power_pos zx p)
  | Qq nx dx => Qq (BigZ.power_pos nx p) (BigN.pred (BigN.power_pos (BigN.succ dx) p))
  end.


 Theorem spec_power_pos x p: ([power_pos x p] == [x] ^ Zpos p)%Q.
 Proof.
 intros [x | nx dx] p; unfold power_pos.
   unfold power_pos; red; simpl.
   generalize (Qpower_decomp p (BigZ.to_Z x) 1).
   unfold Qeq; simpl.
   rewrite Zpower_pos_1_l; simpl Z2P.
   rewrite Zmult_1_r.
   intros H; rewrite H.
   rewrite BigZ.spec_power_pos; simpl; ring.
 assert (F1: (0 < BigN.to_Z (BigN.succ dx))%Z).
     rewrite BigN.spec_succ;
     generalize (BigN.spec_pos dx); auto with zarith.
 assert (F2: (0 < BigN.to_Z (BigN.succ dx) ^ ' p)%Z).
  unfold Zpower; apply Zpower_pos_pos; auto.
 unfold power_pos; red; simpl.
 rewrite BigN.succ_pred, BigN.spec_power_pos.
 rewrite Z2P_correct; auto.
 generalize (Qpower_decomp p (BigZ.to_Z nx) 
               (Z2P (BigN.to_Z (BigN.succ dx)))).
 unfold Qeq; simpl.
 repeat rewrite Z2P_correct; auto.
 unfold Qeq; simpl; intros HH.
 rewrite HH.
 rewrite BigZ.spec_power_pos; simpl; ring.
 rewrite Nspec_lt, BigN.spec_0, BigN.spec_power_pos; auto.
 Qed.

 Theorem spec_power_posc x p: [[power_pos x p]] = [[x]] ^ nat_of_P p.
 intros x p; unfold to_Qc.
 apply trans_equal with (!! ([x]^Zpos p)).
 unfold Q2Qc.
 apply Qc_decomp; intros _ _; unfold this.
 apply Qred_complete; apply spec_power_pos.
 pattern p; apply Pind; clear p.
 simpl; ring.
 intros p Hrec.
 rewrite nat_of_P_succ_morphism; simpl Qcpower.
 rewrite <- Hrec.
 unfold Qcmult, Q2Qc.
 apply Qc_decomp; intros _ _;
 unfold this.
 apply Qred_complete.
 assert (F: [x] ^ ' Psucc p == [x] *   [x] ^ ' p).
  simpl; case x; simpl; clear x Hrec.
  intros x; simpl; repeat rewrite Qpower_decomp; simpl.
  red; simpl; repeat rewrite Zpower_pos_1_l; simpl Z2P.
  rewrite Pplus_one_succ_l.
  rewrite Zpower_pos_is_exp.
  rewrite Zpower_pos_1_r; auto.
  intros nx dx; simpl; repeat rewrite Qpower_decomp; simpl.
  red; simpl; repeat rewrite Zpower_pos_1_l; simpl Z2P.
  rewrite Pplus_one_succ_l.
  rewrite Zpower_pos_is_exp.
  rewrite Zpower_pos_1_r; auto.
  assert (F1: (0 < BigN.to_Z (BigN.succ dx))%Z).
    rewrite BigN.spec_succ; generalize (BigN.spec_pos dx); 
      auto with zarith.
  repeat rewrite Zpos_mult_morphism.
  repeat rewrite Z2P_correct; auto.
  2: apply Zpower_pos_pos; auto.
  2: apply Zpower_pos_pos; auto.
  rewrite Zpower_pos_is_exp.
  rewrite Zpower_pos_1_r; auto.
 rewrite F.
 apply Qmult_comp; apply Qeq_sym; apply Qred_correct.
 Qed.


End Qp.