diff options
Diffstat (limited to 'theories/Numbers/Rational/BigQ/Q0Make.v')
| -rw-r--r-- | theories/Numbers/Rational/BigQ/Q0Make.v | 1412 |
1 files changed, 1412 insertions, 0 deletions
diff --git a/theories/Numbers/Rational/BigQ/Q0Make.v b/theories/Numbers/Rational/BigQ/Q0Make.v new file mode 100644 index 00000000..93f52c03 --- /dev/null +++ b/theories/Numbers/Rational/BigQ/Q0Make.v @@ -0,0 +1,1412 @@ +(************************************************************************) +(* 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: Q0Make.v 11028 2008-06-01 17:34:19Z 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 QSig. +Require Import QMake_base. + +Module Q0 <: QType. + + Import BinInt Zorder. + + (** 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 natural + number y interpreted as x/y. The pairs (x,0) and (0,y) are all + interpreted as 0. *) + + Definition t := q_type. + + (** Specification with respect to [QArith] *) + + Open Local Scope Q_scope. + + Definition of_Z x: t := Qz (BigZ.of_Z x). + + Definition of_Q q: t := + match q with x # y => + Qq (BigZ.of_Z x) (BigN.of_N (Npos y)) + end. + + Definition to_Q (q: t) := + match q with + Qz x => BigZ.to_Z x # 1 + |Qq x y => if BigN.eq_bool y BigN.zero then 0 + else BigZ.to_Z x # Z2P (BigN.to_Z y) + end. + + Notation "[ x ]" := (to_Q x). + + Theorem strong_spec_of_Q: forall q: Q, [of_Q q] = q. + Proof. + intros (x,y); simpl. + 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_0. + rewrite BigN.spec_of_pos; intros HH; discriminate HH. + rewrite BigZ.spec_of_Z; simpl. + rewrite (BigN.spec_of_pos); auto. + Qed. + + Theorem spec_of_Q: forall q: Q, [of_Q q] == q. + Proof. + intros; rewrite strong_spec_of_Q; red; auto. + Qed. + + Definition eq x y := [x] == [y]. + + Definition zero: t := Qz BigZ.zero. + Definition one: t := Qz BigZ.one. + Definition minus_one: t := Qz BigZ.minus_one. + + Lemma spec_0: [zero] == 0. + Proof. + reflexivity. + Qed. + + Lemma spec_1: [one] == 1. + Proof. + reflexivity. + Qed. + + Lemma spec_m1: [minus_one] == -(1). + Proof. + reflexivity. + 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 strong_spec_opp: forall q, [opp q] = -[q]. + Proof. + intros [z | x y]; simpl. + rewrite BigZ.spec_opp; auto. + 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_0. + rewrite BigZ.spec_opp; auto. + Qed. + + Theorem spec_opp : forall q, [opp q] == -[q]. + Proof. + intros; rewrite strong_spec_opp; red; auto. + Qed. + + Definition compare (x y: t) := + match x, y with + | Qz zx, Qz zy => BigZ.compare zx zy + | Qz zx, Qq ny dy => + if BigN.eq_bool dy BigN.zero then BigZ.compare zx BigZ.zero + else BigZ.compare (BigZ.mul zx (BigZ.Pos dy)) ny + | Qq nx dx, Qz zy => + if BigN.eq_bool dx BigN.zero then BigZ.compare BigZ.zero zy + else BigZ.compare nx (BigZ.mul zy (BigZ.Pos dx)) + | Qq nx dx, Qq ny dy => + match BigN.eq_bool dx BigN.zero, BigN.eq_bool dy BigN.zero with + | true, true => Eq + | true, false => BigZ.compare BigZ.zero ny + | false, true => BigZ.compare nx BigZ.zero + | false, false => BigZ.compare (BigZ.mul nx (BigZ.Pos dy)) (BigZ.mul ny (BigZ.Pos dx)) + end + end. + + Theorem spec_compare: forall q1 q2, (compare q1 q2) = ([q1] ?= [q2]). + Proof. + intros [z1 | x1 y1] [z2 | x2 y2]; + unfold Qcompare, compare, to_Q, Qnum, Qden. + 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. + generalize (BigN.spec_eq_bool y2 BigN.zero); + case BigN.eq_bool; rewrite BigN.spec_0; intros HH. + rewrite Zmult_1_r; generalize (BigZ.spec_compare z1 BigZ.zero); + case BigZ.compare; auto. + rewrite BigZ.spec_0; intros HH1; rewrite HH1; rewrite Zcompare_refl; auto. + rewrite Z2P_correct; auto with zarith. + 2: generalize (BigN.spec_pos y2); auto with zarith. + generalize (BigZ.spec_compare (z1 * BigZ.Pos y2) x2)%bigZ; case BigZ.compare; + rewrite BigZ.spec_mul; simpl; intros H; apply sym_equal; auto. + rewrite H; rewrite Zcompare_refl; auto. + generalize (BigN.spec_eq_bool y1 BigN.zero); + case BigN.eq_bool; rewrite BigN.spec_0; intros HH. + rewrite Zmult_0_l; rewrite Zmult_1_r. + generalize (BigZ.spec_compare BigZ.zero z2); + case BigZ.compare; auto. + rewrite BigZ.spec_0; intros HH1; rewrite <- HH1; rewrite Zcompare_refl; auto. + rewrite Z2P_correct; auto with zarith. + 2: generalize (BigN.spec_pos y1); auto with zarith. + rewrite Zmult_1_r. + generalize (BigZ.spec_compare x1 (z2 * BigZ.Pos y1))%bigZ; case BigZ.compare; + rewrite BigZ.spec_mul; simpl; intros H; apply sym_equal; auto. + rewrite H; rewrite Zcompare_refl; auto. + generalize (BigN.spec_eq_bool y1 BigN.zero); + case BigN.eq_bool; rewrite BigN.spec_0; intros HH. + generalize (BigN.spec_eq_bool y2 BigN.zero); + case BigN.eq_bool; rewrite BigN.spec_0; intros HH1. + rewrite Zcompare_refl; auto. + rewrite Zmult_0_l; rewrite Zmult_1_r. + generalize (BigZ.spec_compare BigZ.zero x2); + case BigZ.compare; auto. + rewrite BigZ.spec_0; intros HH2; rewrite <- HH2; rewrite Zcompare_refl; auto. + generalize (BigN.spec_eq_bool y2 BigN.zero); + case BigN.eq_bool; rewrite BigN.spec_0; intros HH1. + rewrite Zmult_0_l; rewrite Zmult_1_r. + generalize (BigZ.spec_compare x1 BigZ.zero)%bigZ; case BigZ.compare; + auto; rewrite BigZ.spec_0. + intros HH2; rewrite <- HH2; rewrite Zcompare_refl; auto. + repeat rewrite Z2P_correct. + 2: generalize (BigN.spec_pos y1); auto with zarith. + 2: generalize (BigN.spec_pos y2); auto with zarith. + generalize (BigZ.spec_compare (x1 * BigZ.Pos y2) + (x2 * BigZ.Pos y1))%bigZ; case BigZ.compare; + repeat rewrite BigZ.spec_mul; simpl; intros H; apply sym_equal; auto. + rewrite H; rewrite Zcompare_refl; auto. + Qed. + + Definition lt n m := compare n m = Lt. + Definition le n m := compare n m <> Gt. + Definition min n m := match compare n m with Gt => m | _ => n end. + Definition max n m := match compare n m with Lt => m | _ => n end. + +(* Je pense que cette fonction normalise bien ... *) + Definition norm n d: t := + let gcd := BigN.gcd (BigZ.to_N n) d in + match BigN.compare BigN.one gcd with + | Lt => + let n := BigZ.div n (BigZ.Pos gcd) in + let d := BigN.div d gcd in + match BigN.compare d BigN.one with + | Gt => Qq n d + | Eq => Qz n + | Lt => zero + end + | Eq => Qq n d + | Gt => zero (* gcd = 0 => both numbers are 0 *) + end. + + Theorem spec_norm: forall n q, [norm n q] == [Qq n q]. + Proof. + intros p q; unfold norm. + assert (Hp := BigN.spec_pos (BigZ.to_N p)). + match goal with |- context[BigN.compare ?X ?Y] => + generalize (BigN.spec_compare X Y); case BigN.compare + end; auto; rewrite BigN.spec_1; rewrite BigN.spec_gcd; intros H1. + apply Qeq_refl. + generalize (BigN.spec_pos (q / BigN.gcd (BigZ.to_N p) q)%bigN). + match goal with |- context[BigN.compare ?X ?Y] => + generalize (BigN.spec_compare X Y); case BigN.compare + end; auto; rewrite BigN.spec_1; rewrite BigN.spec_div; + rewrite BigN.spec_gcd; auto with zarith; intros H2 HH. + red; simpl. + 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_0; intros H3; simpl; + rewrite BigZ.spec_div; simpl; rewrite BigN.spec_gcd; + auto with zarith. + generalize H2; rewrite H3; + rewrite Zdiv_0_l; auto with zarith. + generalize H1 H2 H3 (BigN.spec_pos q); clear H1 H2 H3. + rewrite spec_to_N. + set (a := (BigN.to_Z (BigZ.to_N p))). + set (b := (BigN.to_Z q)). + intros H1 H2 H3 H4; rewrite Z2P_correct; auto with zarith. + rewrite Zgcd_div_swap; auto with zarith. + rewrite H2; ring. + red; simpl. + 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_0; intros H3; simpl. + case H3. + generalize H1 H2 H3 HH; clear H1 H2 H3 HH. + set (a := (BigN.to_Z (BigZ.to_N p))). + set (b := (BigN.to_Z q)). + intros H1 H2 H3 HH. + rewrite (Zdivide_Zdiv_eq (Zgcd a b) b); auto with zarith. + case (Zle_lt_or_eq _ _ HH); auto with zarith. + intros HH1; rewrite <- HH1; ring. + generalize (Zgcd_is_gcd a b); intros HH1; inversion HH1; auto. + red; simpl. + 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_0; rewrite BigN.spec_div; + rewrite BigN.spec_gcd; auto with zarith; intros H3. + 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_0; intros H4. + case H3; rewrite H4; rewrite Zdiv_0_l; auto with zarith. + simpl. + assert (FF := BigN.spec_pos q). + rewrite Z2P_correct; auto with zarith. + rewrite <- BigN.spec_gcd; rewrite <- BigN.spec_div; auto with zarith. + rewrite Z2P_correct; auto with zarith. + rewrite BigN.spec_div; rewrite BigN.spec_gcd; auto with zarith. + simpl; rewrite BigZ.spec_div; simpl. + rewrite BigN.spec_gcd; auto with zarith. + generalize H1 H2 H3 H4 HH FF; clear H1 H2 H3 H4 HH FF. + set (a := (BigN.to_Z (BigZ.to_N p))). + set (b := (BigN.to_Z q)). + intros H1 H2 H3 H4 HH FF. + rewrite spec_to_N; fold a. + rewrite Zgcd_div_swap; auto with zarith. + rewrite BigN.spec_gcd; auto with zarith. + rewrite BigN.spec_div; + rewrite BigN.spec_gcd; auto with zarith. + rewrite BigN.spec_gcd; auto with zarith. + case (Zle_lt_or_eq _ _ + (BigN.spec_pos (BigN.gcd (BigZ.to_N p) q))); + rewrite BigN.spec_gcd; auto with zarith. + intros; apply False_ind; auto with zarith. + intros HH2; assert (FF1 := Zgcd_inv_0_l _ _ (sym_equal HH2)). + assert (FF2 := Zgcd_inv_0_l _ _ (sym_equal HH2)). + red; simpl. + 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_0; intros H2; simpl. + rewrite spec_to_N. + rewrite FF2; ring. + Qed. + + + Definition add (x y: t): t := + match x with + | Qz zx => + match y with + | Qz zy => Qz (BigZ.add zx zy) + | Qq ny dy => + if BigN.eq_bool dy BigN.zero then x + else Qq (BigZ.add (BigZ.mul zx (BigZ.Pos dy)) ny) dy + end + | Qq nx dx => + if BigN.eq_bool dx BigN.zero then y + else match y with + | Qz zy => Qq (BigZ.add nx (BigZ.mul zy (BigZ.Pos dx))) dx + | Qq ny dy => + if BigN.eq_bool dy BigN.zero then x + else + let n := BigZ.add (BigZ.mul nx (BigZ.Pos dy)) (BigZ.mul ny (BigZ.Pos dx)) in + let d := BigN.mul dx dy in + Qq n d + end + end. + + Theorem spec_add : forall x y, [add x y] == [x] + [y]. + Proof. + intros [x | nx dx] [y | ny dy]; unfold Qplus; simpl. + rewrite BigZ.spec_add; repeat rewrite Zmult_1_r; auto. + intros; apply Qeq_refl; auto. + assert (F1:= BigN.spec_pos dy). + rewrite Zmult_1_r; red; simpl. + generalize (BigN.spec_eq_bool dy BigN.zero); + case BigN.eq_bool; + rewrite BigN.spec_0; intros HH; simpl; try ring. + generalize (BigN.spec_eq_bool dy BigN.zero); + case BigN.eq_bool; + rewrite BigN.spec_0; intros HH1; simpl; try ring. + case HH; auto. + rewrite Z2P_correct; auto with zarith. + rewrite BigZ.spec_add; rewrite BigZ.spec_mul; simpl; auto. + generalize (BigN.spec_eq_bool dx BigN.zero); + case BigN.eq_bool; + rewrite BigN.spec_0; intros HH; simpl; try ring. + rewrite Zmult_1_r; apply Qeq_refl. + generalize (BigN.spec_eq_bool dx BigN.zero); + case BigN.eq_bool; + rewrite BigN.spec_0; intros HH1; simpl; try ring. + case HH; auto. + rewrite Z2P_correct; auto with zarith. + rewrite BigZ.spec_add; rewrite BigZ.spec_mul; simpl; auto. + rewrite Zmult_1_r; rewrite Pmult_1_r. + apply Qeq_refl. + assert (F1:= BigN.spec_pos dx); auto with zarith. + generalize (BigN.spec_eq_bool dx BigN.zero); + case BigN.eq_bool; rewrite BigN.spec_0; intros HH. + generalize (BigN.spec_eq_bool dy BigN.zero); + case BigN.eq_bool; rewrite BigN.spec_0; intros HH1. + simpl. + generalize (BigN.spec_eq_bool dy BigN.zero); + case BigN.eq_bool; rewrite BigN.spec_0; intros HH2. + apply Qeq_refl. + case HH2; auto. + simpl. + generalize (BigN.spec_eq_bool dy BigN.zero); + case BigN.eq_bool; rewrite BigN.spec_0; intros HH2. + case HH2; auto. + case HH1; auto. + rewrite Zmult_1_r; apply Qeq_refl. + generalize (BigN.spec_eq_bool dy BigN.zero); + case BigN.eq_bool; rewrite BigN.spec_0; intros HH1. + simpl. + generalize (BigN.spec_eq_bool dx BigN.zero); + case BigN.eq_bool; rewrite BigN.spec_0; intros HH2. + case HH; auto. + rewrite Zmult_1_r; rewrite Zplus_0_r; rewrite Pmult_1_r. + apply Qeq_refl. + simpl. + generalize (BigN.spec_eq_bool (dx * dy)%bigN BigN.zero); + case BigN.eq_bool; rewrite BigN.spec_mul; + rewrite BigN.spec_0; intros HH2. + (case (Zmult_integral _ _ HH2); intros HH3); + [case HH| case HH1]; auto. + rewrite BigZ.spec_add; repeat rewrite BigZ.spec_mul; simpl. + assert (Fx: (0 < BigN.to_Z dx)%Z). + generalize (BigN.spec_pos dx); auto with zarith. + assert (Fy: (0 < BigN.to_Z dy)%Z). + generalize (BigN.spec_pos dy); auto with zarith. + red; simpl; rewrite Zpos_mult_morphism. + repeat rewrite Z2P_correct; auto with zarith. + apply Zmult_lt_0_compat; auto. + Qed. + + Definition add_norm (x y: t): t := + match x with + | Qz zx => + match y with + | Qz zy => Qz (BigZ.add zx zy) + | Qq ny dy => + if BigN.eq_bool dy BigN.zero then x + else norm (BigZ.add (BigZ.mul zx (BigZ.Pos dy)) ny) dy + end + | Qq nx dx => + if BigN.eq_bool dx BigN.zero then y + else match y with + | Qz zy => norm (BigZ.add nx (BigZ.mul zy (BigZ.Pos dx))) dx + | Qq ny dy => + if BigN.eq_bool dy BigN.zero then x + else + 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 + end. + + Theorem spec_add_norm : forall x y, [add_norm x y] == [x] + [y]. + Proof. + intros x y; rewrite <- spec_add; auto. + case x; case y; clear x y; unfold add_norm, add. + intros; apply Qeq_refl. + intros p1 n p2. + generalize (BigN.spec_eq_bool n BigN.zero); + case BigN.eq_bool; rewrite BigN.spec_0; intros HH. + apply Qeq_refl. + match goal with |- [norm ?X ?Y] == _ => + apply Qeq_trans with ([Qq X Y]); + [apply spec_norm | idtac] + end. + simpl. + generalize (BigN.spec_eq_bool n BigN.zero); + case BigN.eq_bool; rewrite BigN.spec_0; intros HH1. + apply Qeq_refl. + apply Qeq_refl. + intros p1 p2 n. + generalize (BigN.spec_eq_bool n BigN.zero); + case BigN.eq_bool; rewrite BigN.spec_0; intros HH. + apply Qeq_refl. + match goal with |- [norm ?X ?Y] == _ => + apply Qeq_trans with ([Qq X Y]); + [apply spec_norm | idtac] + end. + apply Qeq_refl. + intros p1 q1 p2 q2. + generalize (BigN.spec_eq_bool q2 BigN.zero); + case BigN.eq_bool; rewrite BigN.spec_0; intros HH1. + apply Qeq_refl. + generalize (BigN.spec_eq_bool q1 BigN.zero); + case BigN.eq_bool; rewrite BigN.spec_0; intros HH2. + apply Qeq_refl. + match goal with |- [norm ?X ?Y] == _ => + apply Qeq_trans with ([Qq X Y]); + [apply spec_norm | idtac] + end. + apply Qeq_refl. + Qed. + + Definition sub x y := add x (opp y). + + Theorem spec_sub : forall x y, [sub x y] == [x] - [y]. + Proof. + intros x y; unfold sub; rewrite spec_add; auto. + rewrite spec_opp; ring. + Qed. + + Definition sub_norm x y := add_norm x (opp y). + + Theorem spec_sub_norm : forall x y, [sub_norm x y] == [x] - [y]. + Proof. + intros x y; unfold sub_norm; rewrite spec_add_norm; auto. + rewrite spec_opp; 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.mul dx dy) + end. + + Theorem spec_mul : forall x y, [mul x y] == [x] * [y]. + Proof. + intros [x | nx dx] [y | ny dy]; unfold Qmult; simpl. + rewrite BigZ.spec_mul; repeat rewrite Zmult_1_r; auto. + intros; apply Qeq_refl; auto. + 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 HH1. + red; simpl; ring. + rewrite BigZ.spec_mul; 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 HH1. + red; simpl; ring. + rewrite BigZ.spec_mul; rewrite Pmult_1_r. + 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; rewrite BigN.spec_mul; + intros HH1. + 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 HH2. + red; simpl; auto. + 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 HH3. + red; simpl; ring. + case (Zmult_integral _ _ HH1); intros HH. + case HH2; auto. + case HH3; auto. + 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 HH2. + case HH1; rewrite HH2; ring. + 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 HH3. + case HH1; rewrite HH3; ring. + 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. + generalize (BigN.spec_pos dx); auto with zarith. + generalize (BigN.spec_pos dy); auto with zarith. + 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 gcd := BigN.gcd (BigZ.to_N zx) dy in + match BigN.compare gcd BigN.one with + Gt => + let zx := BigZ.div zx (BigZ.Pos gcd) in + let d := BigN.div dy gcd in + if BigN.eq_bool d BigN.one then Qz (BigZ.mul zx ny) + else Qq (BigZ.mul zx ny) d + | _ => Qq (BigZ.mul zx ny) dy + end + | Qq nx dx, Qz zy => + if BigZ.eq_bool zy BigZ.zero then zero + else + let gcd := BigN.gcd (BigZ.to_N zy) dx in + match BigN.compare gcd BigN.one with + Gt => + let zy := BigZ.div zy (BigZ.Pos gcd) in + let d := BigN.div dx gcd in + if BigN.eq_bool d BigN.one then Qz (BigZ.mul zy nx) + else Qq (BigZ.mul zy nx) d + | _ => Qq (BigZ.mul zy nx) dx + end + | Qq nx dx, Qq ny dy => + let (nx, dy) := + let gcd := BigN.gcd (BigZ.to_N nx) dy in + match BigN.compare gcd BigN.one with + Gt => (BigZ.div nx (BigZ.Pos gcd), BigN.div dy gcd) + | _ => (nx, dy) + end in + let (ny, dx) := + let gcd := BigN.gcd (BigZ.to_N ny) dx in + match BigN.compare gcd BigN.one with + Gt => (BigZ.div ny (BigZ.Pos gcd), BigN.div dx gcd) + | _ => (ny, dx) + end in + let d := (BigN.mul dx dy) in + if BigN.eq_bool d BigN.one then Qz (BigZ.mul ny nx) + else Qq (BigZ.mul ny nx) d + end. + + Theorem spec_mul_norm : forall x y, [mul_norm x y] == [x] * [y]. + Proof. + intros x y; rewrite <- spec_mul; auto. + unfold mul_norm, mul; case x; case y; clear x y. + intros; apply Qeq_refl. + intros p1 n p2. + set (a := BigN.to_Z (BigZ.to_N p2)). + set (b := BigN.to_Z 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. + case BigN.eq_bool; try apply Qeq_refl. + rewrite BigZ.spec_mul; rewrite H. + red; simpl; ring. + assert (F: (0 < a)%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. + match goal with |- context[BigN.compare ?X ?Y] => + generalize (BigN.spec_compare X Y); case BigN.compare + end; rewrite BigN.spec_1; rewrite BigN.spec_gcd; + fold a b; intros H1. + apply Qeq_refl. + apply Qeq_refl. + assert (F0 : (0 < (Zgcd a b))%Z). + apply Zlt_trans with 1%Z. + red; auto. + apply Zgt_lt; auto. + 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; + fold a b; intros H2. + assert (F1: b = Zgcd a b). + pattern b at 1; rewrite (Zdivide_Zdiv_eq (Zgcd a b) b); + auto with zarith. + rewrite H2; ring. + assert (FF := Zgcd_is_gcd a b); inversion FF; auto. + assert (F2: (0 < b)%Z). + rewrite F1; auto. + 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; fold b; intros H3. + rewrite H3 in F2; discriminate F2. + rewrite BigZ.spec_mul. + rewrite BigZ.spec_div; simpl; rewrite BigN.spec_gcd; + fold a b; auto with zarith. + rewrite BigZ.spec_mul. + red; simpl; rewrite Z2P_correct; auto. + rewrite Zmult_1_r; rewrite spec_to_N; fold a b. + 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. + 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; rewrite BigN.spec_div; + rewrite BigN.spec_gcd; fold a b; auto; intros H3. + 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 H4. + apply Qeq_refl. + case H4; fold b. + rewrite (Zdivide_Zdiv_eq (Zgcd a b) b); auto. + rewrite H3; ring. + assert (FF := Zgcd_is_gcd a b); inversion FF; auto. + simpl. + 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; fold b; intros H4. + case H3; rewrite H4; rewrite Zdiv_0_l; auto. + rewrite BigZ.spec_mul; rewrite BigZ.spec_div; simpl; + rewrite BigN.spec_gcd; fold a b; auto with zarith. + assert (F1: (0 < b)%Z). + case (Zle_lt_or_eq _ _ (BigN.spec_pos n)); fold b; auto with zarith. + red; simpl. + rewrite BigZ.spec_mul. + repeat rewrite Z2P_correct; auto. + rewrite spec_to_N; fold a. + repeat rewrite <- Zmult_assoc. + rewrite (Zmult_comm (BigZ.to_Z p1)). + repeat rewrite Zmult_assoc. + rewrite Zgcd_div_swap; auto with zarith. + ring. + apply Zgcd_div_pos; auto. + intros p1 p2 n. + set (a := BigN.to_Z (BigZ.to_N p1)). + set (b := BigN.to_Z 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. + case BigN.eq_bool; try apply Qeq_refl. + rewrite BigZ.spec_mul; rewrite H. + red; simpl; ring. + assert (F: (0 < a)%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. + match goal with |- context[BigN.compare ?X ?Y] => + generalize (BigN.spec_compare X Y); case BigN.compare + end; rewrite BigN.spec_1; rewrite BigN.spec_gcd; + fold a b; intros H1. + repeat rewrite BigZ.spec_mul; rewrite Zmult_comm. + apply Qeq_refl. + repeat rewrite BigZ.spec_mul; rewrite Zmult_comm. + apply Qeq_refl. + assert (F0 : (0 < (Zgcd a b))%Z). + apply Zlt_trans with 1%Z. + red; auto. + apply Zgt_lt; auto. + 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; + fold a b; intros H2. + assert (F1: b = Zgcd a b). + pattern b at 1; rewrite (Zdivide_Zdiv_eq (Zgcd a b) b); + auto with zarith. + rewrite H2; ring. + assert (FF := Zgcd_is_gcd a b); inversion FF; auto. + assert (F2: (0 < b)%Z). + rewrite F1; auto. + 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; fold b; intros H3. + rewrite H3 in F2; discriminate F2. + rewrite BigZ.spec_mul. + rewrite BigZ.spec_div; simpl; rewrite BigN.spec_gcd; + fold a b; auto with zarith. + rewrite BigZ.spec_mul. + red; simpl; rewrite Z2P_correct; auto. + rewrite Zmult_1_r; rewrite spec_to_N; fold a b. + 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. + 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; rewrite BigN.spec_div; + rewrite BigN.spec_gcd; fold a b; auto; intros H3. + 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 H4. + apply Qeq_refl. + case H4; fold b. + rewrite (Zdivide_Zdiv_eq (Zgcd a b) b); auto. + rewrite H3; ring. + assert (FF := Zgcd_is_gcd a b); inversion FF; auto. + simpl. + 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; fold b; intros H4. + case H3; rewrite H4; rewrite Zdiv_0_l; auto. + rewrite BigZ.spec_mul; rewrite BigZ.spec_div; simpl; + rewrite BigN.spec_gcd; fold a b; auto with zarith. + assert (F1: (0 < b)%Z). + case (Zle_lt_or_eq _ _ (BigN.spec_pos n)); fold b; auto with zarith. + red; simpl. + rewrite BigZ.spec_mul. + repeat rewrite Z2P_correct; auto. + rewrite spec_to_N; fold a. + repeat rewrite <- Zmult_assoc. + rewrite (Zmult_comm (BigZ.to_Z p2)). + repeat rewrite Zmult_assoc. + rewrite Zgcd_div_swap; auto with zarith. + ring. + apply Zgcd_div_pos; auto. + set (f := fun p t => + match (BigN.gcd (BigZ.to_N p) t ?= BigN.one)%bigN with + | Eq => (p, t) + | Lt => (p, t) + | Gt => + ((p / BigZ.Pos (BigN.gcd (BigZ.to_N p) t))%bigZ, + (t / BigN.gcd (BigZ.to_N p) t)%bigN) + end). + assert (F: forall p t, + let (n, d) := f p t in [Qq p t] == [Qq n d]). + intros p t1; unfold f. + match goal with |- context[BigN.compare ?X ?Y] => + generalize (BigN.spec_compare X Y); case BigN.compare + end; rewrite BigN.spec_1; rewrite BigN.spec_gcd; intros H1. + apply Qeq_refl. + apply Qeq_refl. + set (a := BigN.to_Z (BigZ.to_N p)). + set (b := BigN.to_Z t1). + fold a b in H1. + assert (F0 : (0 < (Zgcd a b))%Z). + apply Zlt_trans with 1%Z. + red; auto. + apply Zgt_lt; auto. + red; simpl. + 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; fold b; intros HH1. + 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; fold b; intros HH2. + simpl; ring. + case HH2. + rewrite BigN.spec_div; rewrite BigN.spec_gcd; fold a b; auto. + rewrite HH1; rewrite Zdiv_0_l; auto. + 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; + rewrite BigN.spec_div; rewrite BigN.spec_gcd; fold a b; auto; + intros HH2. + case HH1. + rewrite (Zdivide_Zdiv_eq (Zgcd a b) b); auto. + rewrite HH2; ring. + assert (FF := Zgcd_is_gcd a b); inversion FF; auto. + simpl. + rewrite BigZ.spec_div; simpl; rewrite BigN.spec_gcd; fold a b; auto with zarith. + assert (F1: (0 < b)%Z). + case (Zle_lt_or_eq _ _ (BigN.spec_pos t1)); fold b; auto with zarith. + intros HH; case HH1; auto. + repeat rewrite Z2P_correct; auto. + rewrite spec_to_N; fold a. + rewrite Zgcd_div_swap; auto. + apply Zgcd_div_pos; auto. + intros HH; rewrite HH in F0; discriminate F0. + intros p1 n1 p2 n2. + change ([let (nx , dy) := f p2 n1 in + let (ny, dx) := f p1 n2 in + if BigN.eq_bool (dx * dy)%bigN BigN.one + then Qz (ny * nx) + else Qq (ny * nx) (dx * dy)] == [Qq (p2 * p1) (n2 * n1)]). + generalize (F p2 n1) (F p1 n2). + case f; case f. + intros u1 u2 v1 v2 Hu1 Hv1. + apply Qeq_trans with [mul (Qq p2 n1) (Qq p1 n2)]. + rewrite spec_mul; rewrite Hu1; rewrite Hv1. + 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_mul; intros HH1. + assert (F1: BigN.to_Z u2 = 1%Z). + case (Zmult_1_inversion_l _ _ HH1); auto. + generalize (BigN.spec_pos u2); auto with zarith. + assert (F2: BigN.to_Z v2 = 1%Z). + rewrite Zmult_comm in HH1. + case (Zmult_1_inversion_l _ _ HH1); auto. + generalize (BigN.spec_pos v2); auto with zarith. + red; simpl. + 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 H1. + rewrite H1 in F2; discriminate F2. + 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 H2. + rewrite H2 in F1; discriminate F1. + simpl; rewrite BigZ.spec_mul. + rewrite F1; rewrite F2; simpl; ring. + rewrite Qmult_comm; rewrite <- spec_mul. + apply Qeq_refl. + red; simpl. + 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; rewrite BigN.spec_mul; + rewrite Zmult_comm; intros H1. + 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; rewrite BigN.spec_mul; intros H2; auto. + case H2; auto. + 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; rewrite BigN.spec_mul; intros H2; auto. + case H1; auto. + Qed. + + +Definition inv (x: t): t := + match x with + | Qz (BigZ.Pos n) => Qq BigZ.one n + | Qz (BigZ.Neg n) => Qq BigZ.minus_one n + | Qq (BigZ.Pos n) d => Qq (BigZ.Pos d) n + | Qq (BigZ.Neg n) d => Qq (BigZ.Neg d) n + end. + + Theorem spec_inv : forall x, [inv x] == /[x]. + Proof. + intros [ [x | x] | [nx | nx] dx]; unfold inv, Qinv; simpl. + 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 H1; auto. + rewrite H1; apply Qeq_refl. + generalize H1 (BigN.spec_pos x); case (BigN.to_Z x); auto. + intros HH; case HH; auto. + intros; red; simpl; auto. + intros p _ HH; case HH; auto. + 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 H1; auto. + rewrite H1; apply Qeq_refl. + generalize H1 (BigN.spec_pos x); case (BigN.to_Z x); simpl; + auto. + intros HH; case HH; auto. + intros; red; simpl; auto. + intros p _ HH; case HH; auto. + 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 H1; auto. + 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 H2; simpl; auto. + apply Qeq_refl. + rewrite H1; 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 H2; simpl; auto. + rewrite H2; red; simpl; auto. + generalize H1 (BigN.spec_pos nx); case (BigN.to_Z nx); simpl; + auto. + intros HH; case HH; auto. + intros; red; simpl. + rewrite Zpos_mult_morphism. + rewrite Z2P_correct; auto. + generalize (BigN.spec_pos dx); auto with zarith. + intros p _ HH; case HH; auto. + 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 H1; auto. + 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 H2; simpl; auto. + apply Qeq_refl. + rewrite H1; 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 H2; simpl; auto. + rewrite H2; red; simpl; auto. + generalize H1 (BigN.spec_pos nx); case (BigN.to_Z nx); simpl; + auto. + intros HH; case HH; auto. + intros; red; simpl. + assert (tmp: forall x, Zneg x = Zopp (Zpos x)); auto. + rewrite tmp. + rewrite Zpos_mult_morphism. + rewrite Z2P_correct; auto. + ring. + generalize (BigN.spec_pos dx); auto with zarith. + intros p _ HH; case HH; auto. + Qed. + +Definition inv_norm (x: t): t := + match x with + | Qz (BigZ.Pos n) => + match BigN.compare n BigN.one with + Gt => Qq BigZ.one n + | _ => x + end + | Qz (BigZ.Neg n) => + match BigN.compare n BigN.one with + Gt => Qq BigZ.minus_one n + | _ => x + end + | Qq (BigZ.Pos n) d => + match BigN.compare n BigN.one with + Gt => Qq (BigZ.Pos d) n + | Eq => Qz (BigZ.Pos d) + | Lt => Qz (BigZ.zero) + end + | Qq (BigZ.Neg n) d => + match BigN.compare n BigN.one with + Gt => Qq (BigZ.Neg d) n + | Eq => Qz (BigZ.Neg d) + | Lt => Qz (BigZ.zero) + end + end. + + Theorem spec_inv_norm : forall x, [inv_norm x] == /[x]. + Proof. + intros [ [x | x] | [nx | nx] dx]; unfold inv_norm, Qinv. + match goal with |- context[BigN.compare ?X ?Y] => + generalize (BigN.spec_compare X Y); case BigN.compare + end; rewrite BigN.spec_1; intros H. + simpl; rewrite H; apply Qeq_refl. + case (Zle_lt_or_eq _ _ (BigN.spec_pos x)); simpl. + generalize H; case BigN.to_Z. + intros _ HH; discriminate HH. + intros p; case p; auto. + intros p1 HH; discriminate HH. + intros p1 HH; discriminate HH. + intros HH; discriminate HH. + intros p _ HH; discriminate HH. + intros HH; rewrite <- HH. + apply Qeq_refl. + generalize H; simpl. + 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 H1. + rewrite H1; intros HH; discriminate. + generalize H; case BigN.to_Z. + intros HH; discriminate HH. + intros; red; simpl; auto. + intros p HH; discriminate HH. + match goal with |- context[BigN.compare ?X ?Y] => + generalize (BigN.spec_compare X Y); case BigN.compare + end; rewrite BigN.spec_1; intros H. + simpl; rewrite H; apply Qeq_refl. + case (Zle_lt_or_eq _ _ (BigN.spec_pos x)); simpl. + generalize H; case BigN.to_Z. + intros _ HH; discriminate HH. + intros p; case p; auto. + intros p1 HH; discriminate HH. + intros p1 HH; discriminate HH. + intros HH; discriminate HH. + intros p _ HH; discriminate HH. + intros HH; rewrite <- HH. + apply Qeq_refl. + generalize H; simpl. + 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 H1. + rewrite H1; intros HH; discriminate. + generalize H; case BigN.to_Z. + intros HH; discriminate HH. + intros; red; simpl; auto. + intros p HH; discriminate HH. + simpl Qnum. + 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 H1; simpl. + case BigN.compare; red; simpl; auto. + rewrite H1; auto. + case BigN.eq_bool; auto. + simpl; rewrite H1; auto. + match goal with |- context[BigN.compare ?X ?Y] => + generalize (BigN.spec_compare X Y); case BigN.compare + end; rewrite BigN.spec_1; intros H2. + rewrite H2. + 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 H3. + case H1; auto. + red; simpl. + rewrite Zmult_1_r; rewrite Pmult_1_r; rewrite Z2P_correct; auto. + 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 H3. + case H1; auto. + generalize H2 (BigN.spec_pos nx); case (BigN.to_Z nx). + intros; apply Qeq_refl. + intros p; case p; clear p. + intros p HH; discriminate HH. + intros p HH; discriminate HH. + intros HH; discriminate HH. + intros p _ HH; case HH; auto. + 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 H3. + case H1; auto. + simpl; generalize H2; case (BigN.to_Z nx). + intros HH; discriminate HH. + intros p 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 H4. + rewrite H4 in H2; discriminate H2. + red; simpl. + rewrite Zpos_mult_morphism. + rewrite Z2P_correct; auto. + generalize (BigN.spec_pos dx); auto with zarith. + intros p HH; discriminate HH. + simpl Qnum. + 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 H1; simpl. + case BigN.compare; red; simpl; auto. + rewrite H1; auto. + case BigN.eq_bool; auto. + simpl; rewrite H1; auto. + match goal with |- context[BigN.compare ?X ?Y] => + generalize (BigN.spec_compare X Y); case BigN.compare + end; rewrite BigN.spec_1; intros H2. + rewrite H2. + 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 H3. + case H1; auto. + red; simpl. + assert (tmp: forall x, Zneg x = Zopp (Zpos x)); auto. + rewrite tmp. + rewrite Zmult_1_r; rewrite Pmult_1_r; rewrite Z2P_correct; auto. + 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 H3. + case H1; auto. + generalize H2 (BigN.spec_pos nx); case (BigN.to_Z nx). + intros; apply Qeq_refl. + intros p; case p; clear p. + intros p HH; discriminate HH. + intros p HH; discriminate HH. + intros HH; discriminate HH. + intros p _ HH; case HH; auto. + 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 H3. + case H1; auto. + simpl; generalize H2; case (BigN.to_Z nx). + intros HH; discriminate HH. + intros p 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 H4. + rewrite H4 in H2; discriminate H2. + red; simpl. + assert (tmp: forall x, Zneg x = Zopp (Zpos x)); auto. + rewrite tmp. + rewrite Zpos_mult_morphism. + rewrite Z2P_correct; auto. + ring. + generalize (BigN.spec_pos dx); auto with zarith. + intros p HH; discriminate HH. + Qed. + + Definition div x y := mul x (inv y). + + Theorem spec_div x y: [div x y] == [x] / [y]. + Proof. + intros x y; unfold div; rewrite spec_mul; auto. + unfold Qdiv; apply Qmult_comp. + apply Qeq_refl. + apply spec_inv; auto. + Qed. + + Definition div_norm x y := mul_norm x (inv y). + + Theorem spec_div_norm x y: [div_norm x y] == [x] / [y]. + Proof. + intros x y; unfold div_norm; rewrite spec_mul_norm; auto. + unfold Qdiv; apply Qmult_comp. + apply Qeq_refl. + apply spec_inv; auto. + Qed. + + Definition square (x: t): t := + match x with + | Qz zx => Qz (BigZ.square zx) + | Qq nx dx => Qq (BigZ.square nx) (BigN.square dx) + end. + + Theorem spec_square : forall x, [square x] == [x] ^ 2. + Proof. + intros [ x | nx dx]; unfold square. + red; simpl; rewrite BigZ.spec_square; auto with zarith. + simpl Qpower. + repeat 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_0; intros H. + red; simpl. + repeat 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_0; rewrite BigN.spec_square; + intros H1. + case H1; rewrite H; auto. + red; simpl. + repeat 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_0; rewrite BigN.spec_square; + intros H1. + case H; case (Zmult_integral _ _ H1); auto. + simpl. + rewrite BigZ.spec_square. + rewrite Zpos_mult_morphism. + 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. + generalize (BigN.spec_pos dx); auto with zarith. + generalize (BigN.spec_pos dx); auto with zarith. + 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.power_pos dx p) + end. + + Theorem spec_power_pos : forall x p, [power_pos x p] == [x] ^ Zpos p. + 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. + simpl. + 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_0; rewrite BigN.spec_power_pos; intros H1. + 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_0; intros H2. + elim p; simpl. + intros; red; simpl; auto. + intros p1 Hp1; rewrite <- Hp1; red; simpl; auto. + apply Qeq_refl. + case H2; generalize H1. + elim p; simpl. + intros p1 Hrec. + change (xI p1) with (1 + (xO p1))%positive. + rewrite Zpower_pos_is_exp; rewrite Zpower_pos_1_r. + intros HH; case (Zmult_integral _ _ HH); auto. + rewrite <- Pplus_diag. + rewrite Zpower_pos_is_exp. + intros HH1; case (Zmult_integral _ _ HH1); auto. + intros p1 Hrec. + rewrite <- Pplus_diag. + rewrite Zpower_pos_is_exp. + intros HH1; case (Zmult_integral _ _ HH1); auto. + rewrite Zpower_pos_1_r; auto. + 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_0; intros H2. + case H1; rewrite H2; auto. + simpl; rewrite Zpower_pos_0_l; auto. + assert (F1: (0 < BigN.to_Z dx)%Z). + generalize (BigN.spec_pos dx); auto with zarith. + assert (F2: (0 < BigN.to_Z dx ^ ' p)%Z). + unfold Zpower; apply Zpower_pos_pos; auto. + unfold power_pos; red; simpl. + generalize (Qpower_decomp p (BigZ.to_Z nx) + (Z2P (BigN.to_Z dx))). + unfold Qeq; simpl. + repeat rewrite Z2P_correct; auto. + unfold Qeq; simpl; intros HH. + rewrite HH. + rewrite BigZ.spec_power_pos; simpl; ring. + Qed. + + (** Interaction with [Qcanon.Qc] *) + + Open Scope Qc_scope. + + Definition of_Qc q := of_Q (this q). + + Definition to_Qc q := !!(to_Q q). + + Notation "[[ x ]]" := (to_Qc x). + + Theorem spec_of_Qc: forall q, [[of_Qc q]] = q. + Proof. + intros (x, Hx); unfold of_Qc, to_Qc; simpl. + apply Qc_decomp; simpl. + intros. + rewrite <- H0 at 2; apply Qred_complete. + apply spec_of_Q. + Qed. + + Theorem spec_oppc: forall q, [[opp q]] = -[[q]]. + Proof. + intros q; unfold Qcopp, to_Qc, Q2Qc. + apply Qc_decomp; intros _ _; unfold this. + apply Qred_complete. + rewrite spec_opp. + rewrite <- Qred_opp. + rewrite Qred_correct; red; auto. + Qed. + + Theorem spec_comparec: forall q1 q2, + compare q1 q2 = ([[q1]] ?= [[q2]]). + Proof. + unfold Qccompare, to_Qc. + intros q1 q2; rewrite spec_compare; simpl; auto. + apply Qcompare_comp; apply Qeq_sym; apply Qred_correct. + Qed. + + Theorem spec_addc x y: + [[add x y]] = [[x]] + [[y]]. + Proof. + 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; auto. + unfold Qcplus, Q2Qc. + apply Qc_decomp; intros _ _; unfold this. + apply Qred_complete. + apply Qplus_comp; apply Qeq_sym; apply Qred_correct. + Qed. + + Theorem spec_add_normc x y: + [[add_norm x y]] = [[x]] + [[y]]. + Proof. + 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; auto. + unfold Qcplus, Q2Qc. + apply Qc_decomp; intros _ _; unfold this. + apply Qred_complete. + apply Qplus_comp; apply Qeq_sym; apply Qred_correct. + Qed. + + Theorem spec_subc x y: [[sub x y]] = [[x]] - [[y]]. + Proof. + intros x y; unfold sub; rewrite spec_addc; auto. + rewrite spec_oppc; ring. + Qed. + + Theorem spec_sub_normc x y: + [[sub_norm x y]] = [[x]] - [[y]]. + intros x y; unfold sub_norm; rewrite spec_add_normc; auto. + rewrite spec_oppc; ring. + Qed. + + Theorem spec_mulc x y: + [[mul x y]] = [[x]] * [[y]]. + Proof. + 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; auto. + unfold Qcmult, Q2Qc. + apply Qc_decomp; intros _ _; unfold this. + apply Qred_complete. + apply Qmult_comp; apply Qeq_sym; apply Qred_correct. + Qed. + + Theorem spec_mul_normc x y: + [[mul_norm x y]] = [[x]] * [[y]]. + Proof. + 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; auto. + unfold Qcmult, Q2Qc. + apply Qc_decomp; intros _ _; unfold this. + apply Qred_complete. + apply Qmult_comp; apply Qeq_sym; apply Qred_correct. + Qed. + + Theorem spec_invc x: + [[inv x]] = /[[x]]. + Proof. + intros x; unfold to_Qc. + apply trans_equal with (!! (/[x])). + unfold Q2Qc. + apply Qc_decomp; intros _ _; unfold this. + apply Qred_complete; apply spec_inv; auto. + unfold Qcinv, Q2Qc. + apply Qc_decomp; intros _ _; unfold this. + apply Qred_complete. + apply Qinv_comp; apply Qeq_sym; apply Qred_correct. + Qed. + + Theorem spec_inv_normc x: + [[inv_norm x]] = /[[x]]. + Proof. + intros x; unfold to_Qc. + apply trans_equal with (!! (/[x])). + unfold Q2Qc. + apply Qc_decomp; intros _ _; unfold this. + apply Qred_complete; apply spec_inv_norm; auto. + unfold Qcinv, Q2Qc. + apply Qc_decomp; intros _ _; unfold this. + apply Qred_complete. + apply Qinv_comp; apply Qeq_sym; apply Qred_correct. + Qed. + + Theorem spec_divc x y: [[div x y]] = [[x]] / [[y]]. + Proof. + intros x y; unfold div; rewrite spec_mulc; auto. + unfold Qcdiv; apply f_equal2 with (f := Qcmult); auto. + apply spec_invc; auto. + Qed. + + Theorem spec_div_normc x y: [[div_norm x y]] = [[x]] / [[y]]. + Proof. + 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. + + Theorem spec_squarec x: [[square x]] = [[x]]^2. + Proof. + 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; auto. + 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. + + Theorem spec_power_posc x p: + [[power_pos x p]] = [[x]] ^ nat_of_P p. + Proof. + 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; auto. + 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. + 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_0. + unfold Qpower_positive. + assert (tmp: forall p, pow_pos Qmult 0%Q p = 0%Q). + intros p1; elim p1; simpl; auto; clear p1. + intros p1 Hp1; rewrite Hp1; auto. + intros p1 Hp1; rewrite Hp1; auto. + repeat rewrite tmp; intros; red; simpl; auto. + intros H1. + assert (F1: (0 < BigN.to_Z dx)%Z). + generalize (BigN.spec_pos dx); auto with zarith. + 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. + 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 Q0. |