diff options
| author | thery | 2007-10-25 12:42:51 +0000 |
|---|---|---|
| committer | thery | 2007-10-25 12:42:51 +0000 |
| commit | 7156868c56b1a1cea0fde1889db087f3308f3f5d (patch) | |
| tree | 8143b25447fd4321f8167298ddbb04e251584246 | |
| parent | d7690f1f394e00211802f16d07de53505ddbcd2d (diff) | |
Adding BigQ and proofs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10265 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | Makefile.common | 2 | ||||
| -rw-r--r-- | parsing/g_intsyntax.ml | 33 | ||||
| -rw-r--r-- | theories/Ints/BigN.v | 10 | ||||
| -rw-r--r-- | theories/Ints/BigZ.v | 29 | ||||
| -rw-r--r-- | theories/Ints/Q/QBAux.v | 75 | ||||
| -rw-r--r-- | theories/Ints/Z/ZAux.v | 104 | ||||
| -rw-r--r-- | theories/Ints/Z/ZDivModAux.v | 31 | ||||
| -rw-r--r-- | theories/Ints/num/BigQ.v | 22 | ||||
| -rw-r--r-- | theories/Ints/num/GenDiv.v | 4 | ||||
| -rw-r--r-- | theories/Ints/num/GenDivn1.v | 12 | ||||
| -rw-r--r-- | theories/Ints/num/GenLift.v | 2 | ||||
| -rw-r--r-- | theories/Ints/num/Q0Make.v | 1343 | ||||
| -rw-r--r-- | theories/Ints/num/QMake.v | 901 | ||||
| -rw-r--r-- | theories/Ints/num/QMake_base.v | 23 | ||||
| -rw-r--r-- | theories/Ints/num/QbiMake.v | 1066 | ||||
| -rw-r--r-- | theories/Ints/num/QifMake.v | 975 | ||||
| -rw-r--r-- | theories/Ints/num/QpMake.v | 878 | ||||
| -rw-r--r-- | theories/Ints/num/QvMake.v | 1134 | ||||
| -rw-r--r-- | theories/Ints/num/ZMake.v | 24 |
19 files changed, 5751 insertions, 917 deletions
diff --git a/Makefile.common b/Makefile.common index ccc5d94cd4..19821e7183 100644 --- a/Makefile.common +++ b/Makefile.common @@ -523,7 +523,7 @@ INTSVO:=\ theories/Ints/num/GenLift.vo theories/Ints/num/Zn2Z.vo\ theories/Ints/num/Nbasic.vo theories/Ints/num/NMake.vo \ theories/Ints/BigN.vo theories/Ints/num/ZMake.vo \ - theories/Ints/BigZ.vo theories/Ints/num/QMake.vo + theories/Ints/BigZ.vo theories/Ints/num/BigQ.vo # theories/Ints/List/ListAux.vo # theories/Ints/List/LPermutation.vo theories/Ints/List/Iterator.vo \ # theories/Ints/List/ZProgression.vo diff --git a/parsing/g_intsyntax.ml b/parsing/g_intsyntax.ml index 7abafb070e..b1a8ae3485 100644 --- a/parsing/g_intsyntax.ml +++ b/parsing/g_intsyntax.ml @@ -8,7 +8,7 @@ (*i $ $ i*) -(* digit-based syntax for int31, bigN and bigZ *) +(* digit-based syntax for int31, bigN bigZ and bigQ *) open Bigint open Libnames @@ -90,6 +90,15 @@ let bigZ_pos = ConstructRef ((bigZ_id "t_",0),1) let bigZ_neg = ConstructRef ((bigZ_id "t_",0),2) +(*bigQ stuff*) +let bigQ_module = ["Coq"; "Ints"; "num"; "BigQ"] +let qmake_module = ["Coq"; "Ints"; "num"; "QMake_base"] +let bigQ_path = make_path bigQ_module "bigQ" +(* big ugly hack bis *) +let bigQ_id = make_kn qmake_module +let bigQ_scope = "bigQ_scope" + +let bigQ_z = ConstructRef ((bigQ_id "q_type",0),1) (*** Definition of the Non_closed exception, used in the pretty printing ***) @@ -309,3 +318,25 @@ let _ = Notation.declare_numeral_interpreter bigZ_scope RRef (Util.dummy_loc, bigZ_neg)], uninterp_bigZ, true) + +(*** Parsing for bigQ in digital notation ***) +let interp_bigQ dloc n = + let ref_z = RRef (dloc, bigQ_z) in + let ref_pos = RRef (dloc, bigZ_pos) in + let ref_neg = RRef (dloc, bigZ_neg) in + if is_pos_or_zero n then + RApp (dloc, ref_z, + [RApp (dloc, ref_pos, [bigN_of_pos_bigint dloc n])]) + else + RApp (dloc, ref_z, + [RApp (dloc, ref_neg, [bigN_of_pos_bigint dloc (neg n)])]) + +let uninterp_bigQ rc = None + + +(* Actually declares the interpreter for bigQ *) +let _ = Notation.declare_numeral_interpreter bigQ_scope + (bigQ_path, bigQ_module) + interp_bigQ + ([], uninterp_bigQ, + true) diff --git a/theories/Ints/BigN.v b/theories/Ints/BigN.v index d7b406d3de..e8b92186bd 100644 --- a/theories/Ints/BigN.v +++ b/theories/Ints/BigN.v @@ -113,3 +113,13 @@ Notation " i * j " := (BigN.mul i j) : bigN_scope. Notation " i / j " := (BigN.div i j) : bigN_scope. Notation " i ?= j " := (BigN.compare i j) : bigN_scope. + Theorem succ_pred: forall q, + (0 < BigN.to_Z q -> + BigN.to_Z (BigN.succ (BigN.pred q)) = BigN.to_Z q)%Z. + intros q Hq. + rewrite BigN.spec_succ. + rewrite BigN.spec_pred; auto. + generalize Hq; set (a := BigN.to_Z q). + ring_simplify (a - 1 + 1)%Z; auto. + Qed. + diff --git a/theories/Ints/BigZ.v b/theories/Ints/BigZ.v index 78fe2bced1..8c7c1f809c 100644 --- a/theories/Ints/BigZ.v +++ b/theories/Ints/BigZ.v @@ -17,3 +17,32 @@ Notation " i - j " := (BigZ.sub i j) : bigZ_scope. Notation " i * j " := (BigZ.mul i j) : bigZ_scope. Notation " i / j " := (BigZ.div i j) : bigZ_scope. Notation " i ?= j " := (BigZ.compare i j) : bigZ_scope. + + + Theorem spec_to_Z: + forall n, BigN.to_Z (BigZ.to_N n) = + (Zsgn (BigZ.to_Z n) * BigZ.to_Z n)%Z. + intros n; case n; simpl; intros p; + generalize (BigN.spec_pos p); case (BigN.to_Z p); auto. + intros p1 H1; case H1; auto. + intros p1 H1; case H1; auto. + Qed. + + Theorem spec_to_N n: + (BigZ.to_Z n = + Zsgn (BigZ.to_Z n) * (BigN.to_Z (BigZ.to_N n)))%Z. + intros n; case n; simpl; intros p; + generalize (BigN.spec_pos p); case (BigN.to_Z p); auto. + intros p1 H1; case H1; auto. + intros p1 H1; case H1; auto. + Qed. + + Theorem spec_to_Z_pos: + forall n, (0 <= BigZ.to_Z n -> + BigN.to_Z (BigZ.to_N n) = BigZ.to_Z n)%Z. + intros n; case n; simpl; intros p; + generalize (BigN.spec_pos p); case (BigN.to_Z p); auto. + intros p1 _ H1; case H1; auto. + intros p1 H1; case H1; auto. + Qed. + diff --git a/theories/Ints/Q/QBAux.v b/theories/Ints/Q/QBAux.v new file mode 100644 index 0000000000..6b4bfc8140 --- /dev/null +++ b/theories/Ints/Q/QBAux.v @@ -0,0 +1,75 @@ + +(*************************************************************) +(* This file is distributed under the terms of the *) +(* GNU Lesser General Public License Version 2.1 *) +(*************************************************************) +(* Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr *) +(*************************************************************) + +(********************************************************************** + QBAux.v + + Auxillary functions & Theorems for Q + **********************************************************************) + +Require Import ZAux. +Require Import QArith. +Require Import Qcanon. + + Theorem Qred_opp: forall q, + (Qred (-q) = - (Qred q))%Q. + intros (x, y); unfold Qred; simpl. + rewrite Zggcd_opp; case Zggcd; intros p1 (p2, p3); simpl. + unfold Qopp; auto. + Qed. + + Theorem Qcompare_red: forall x y, + Qcompare x y = Qcompare (Qred x) (Qred y). + intros x y; apply Qcompare_comp; apply Qeq_sym; apply Qred_correct. + Qed. + + + + Theorem Qpower_decomp: forall p x y, + Qpower_positive (x #y) p == x ^ Zpos p # (Z2P ((Zpos y) ^ Zpos p)). + Proof. + intros p; elim p; clear p. + intros p Hrec x y. + unfold Qmult; simpl; rewrite Hrec. + rewrite xI_succ_xO; rewrite <- Pplus_diag; rewrite Pplus_one_succ_l. + repeat rewrite Zpower_pos_is_exp. + red; unfold Qmult, Qnum, Qden, Zpower. + repeat rewrite Zpos_mult_morphism. + repeat rewrite Z2P_correct. + 2: apply ZAux.Zpower_pos_pos; red; auto. + 2: repeat apply Zmult_lt_0_compat; auto; + apply ZAux.Zpower_pos_pos; red; auto. + repeat rewrite ZAux.Zpower_pos_1_r; ring. + + intros p Hrec x y. + unfold Qmult; simpl; rewrite Hrec. + rewrite <- Pplus_diag. + repeat rewrite Zpower_pos_is_exp. + red; unfold Qmult, Qnum, Qden, Zpower. + repeat rewrite Zpos_mult_morphism. + repeat rewrite Z2P_correct; try ring. + apply ZAux.Zpower_pos_pos; red; auto. + repeat apply Zmult_lt_0_compat; auto; + apply ZAux.Zpower_pos_pos; red; auto. + intros x y. + unfold Qmult; simpl. + red; simpl; rewrite ZAux.Zpower_pos_1_r; + rewrite Zpos_mult_morphism; ring. + Qed. + + + Theorem Qc_decomp: forall (x y: Qc), + (Qred x = x -> Qred y = y -> (x:Q) = y)-> x = y. + intros (q, Hq) (q', Hq'); simpl; intros H. + assert (H1 := H Hq Hq'). + subst q'. + assert (Hq = Hq'). + apply Eqdep_dec.eq_proofs_unicity; auto; intros. + repeat decide equality. + congruence. + Qed. diff --git a/theories/Ints/Z/ZAux.v b/theories/Ints/Z/ZAux.v index 3f0c7a5c65..83c54bd478 100644 --- a/theories/Ints/Z/ZAux.v +++ b/theories/Ints/Z/ZAux.v @@ -729,6 +729,60 @@ apply Zgcd_is_gcd. inversion_clear H3; auto. Qed. + Theorem Zggcd_opp: + forall x y, Zggcd (-x) y = + let (p1,p) := Zggcd x y in + let (p2,p3) := p in + (p1,(-p2,p3))%Z. + intros [|x|x] [|y|y]; unfold Zggcd, Zopp; auto. + case Pggcd; intros p1 (p2, p3); auto. + case Pggcd; intros p1 (p2, p3); auto. + case Pggcd; intros p1 (p2, p3); auto. + case Pggcd; intros p1 (p2, p3); auto. + Qed. + + Theorem Zgcd_inv_0_l: forall x y, (Zgcd x y = 0)%Z -> x = 0%Z. + intros x y H. + assert (F1: (Zdivide 0 x)%Z). + rewrite <- H. + generalize (Zgcd_is_gcd x y); intros HH; inversion HH; auto. + inversion F1 as[z H1]. + rewrite H1; ring. + Qed. + + Theorem Zgcd_inv_0_r: forall x y, (Zgcd x y = 0)%Z -> y = 0%Z. + intros x y H. + assert (F1: (Zdivide 0 y)%Z). + rewrite <- H. + generalize (Zgcd_is_gcd x y); intros HH; inversion HH; auto. + inversion F1 as[z H1]. + rewrite H1; ring. + Qed. + + Theorem Zgcd_div: forall a b c, + (0 < c -> (c | b) -> (a * b)/c = a * (b/c))%Z. + intros a b c H1 H2. + inversion H2 as [z Hz]. + rewrite Hz; rewrite Zmult_assoc. + repeat rewrite Z_div_mult; auto with zarith. + Qed. + + Theorem Zgcd_div_swap a b c: + (0 < Zgcd a b)%Z -> + (0 < b)%Z -> + (c * a / Zgcd a b * b)%Z = (c * a * (b/Zgcd a b))%Z. + intros a b c Hg Hb. + assert (F := (Zgcd_is_gcd a b)); inversion F as [F1 F2 F3]. + pattern b at 2; rewrite (Zdivide_Zdiv_eq (Zgcd a b) b); auto. + repeat rewrite Zmult_assoc. + apply f_equal2 with (f := Zmult); auto. + rewrite Zgcd_div; auto. + rewrite <- Zmult_assoc. + rewrite (fun x y => Zmult_comm (x /y)); + rewrite <- (Zdivide_Zdiv_eq); auto. + Qed. + + (************************************** Properties rel_prime **************************************) @@ -1233,6 +1287,56 @@ intros z n; unfold Zpower_nat_tr. rewrite Zpower_tr_aux_correct with (p := 0%nat); auto. Qed. + + Theorem Zpower_pos_1_r: forall x, Zpower_pos x 1 = x. + Proof. + intros x; unfold Zpower_pos; simpl; ring. + Qed. + + Theorem Zpower_pos_1_l: forall p, Zpower_pos 1 p = 1%Z. + Proof. + intros p; elim p; clear p. + intros p Hrec. + rewrite xI_succ_xO; rewrite <- Pplus_diag; rewrite Pplus_one_succ_l. + repeat rewrite Zpower_pos_is_exp. + rewrite Zpower_pos_1_r. + rewrite Hrec; ring. + intros p Hrec. + rewrite <- Pplus_diag. + repeat rewrite Zpower_pos_is_exp. + rewrite Hrec; ring. + rewrite Zpower_pos_1_r; auto. + Qed. + + + + Theorem Zpower_pos_0_l: forall p, Zpower_pos 0 p = 0%Z. + intros p; elim p; clear p. + intros p H1. + change (xI p) with (1 + (xO p))%positive. + rewrite Zpower_pos_is_exp; rewrite Zpower_pos_1_r; auto. + intros p Hrec; rewrite <- Pplus_diag; + rewrite Zpower_pos_is_exp; rewrite Hrec; auto. + rewrite Zpower_pos_1_r; auto. + Qed. + + + Theorem Zpower_pos_pos: forall x p, + (0 < x -> 0 < Zpower_pos x p)%Z. + Proof. + intros x p; elim p; clear p. + intros p Hrec H0. + rewrite xI_succ_xO; rewrite <- Pplus_diag; rewrite Pplus_one_succ_l. + repeat rewrite Zpower_pos_is_exp. + rewrite Zpower_pos_1_r. + repeat apply Zmult_lt_0_compat; auto. + intros p Hrec H0. + rewrite <- Pplus_diag. + repeat rewrite Zpower_pos_is_exp. + repeat apply Zmult_lt_0_compat; auto. + rewrite Zpower_pos_1_r; auto. + Qed. + (************************************** Definition of Zsquare **************************************) diff --git a/theories/Ints/Z/ZDivModAux.v b/theories/Ints/Z/ZDivModAux.v index cb6a01fcd3..127d3cefab 100644 --- a/theories/Ints/Z/ZDivModAux.v +++ b/theories/Ints/Z/ZDivModAux.v @@ -211,9 +211,24 @@ Hint Resolve Zlt_gt Zle_ge: zarith. rewrite Zmult_assoc; apply Z_div_mod_eq; auto with zarith. Qed. - Theorem Zdiv_0: forall a, 0 < a -> 0 / a = 0. + Theorem Zdiv_0_l: forall a, 0 / a = 0. Proof. - intros a H;apply sym_equal;apply Zdiv_unique with (r := 0); auto with zarith. + intros a; case a; auto. + Qed. + + Theorem Zdiv_0_r: forall a, a / 0 = 0. + Proof. + intros a; case a; auto. + Qed. + + Theorem Zmod_0_l: forall a, 0 mod a = 0. + Proof. + intros a; case a; auto. + Qed. + + Theorem Zmod_0_r: forall a, a mod 0 = 0. + Proof. + intros a; case a; auto. Qed. Theorem Zdiv_le_upper_bound: @@ -449,4 +464,16 @@ Hint Resolve Zlt_gt Zle_ge: zarith. destruct x;change (0<y);auto with zarith. destruct p;trivial;discriminate z. Qed. + + + Theorem Zgcd_div_pos a b: + (0 < b)%Z -> (0 < Zgcd a b)%Z -> (0 < b / Zgcd a b)%Z. + intros a b Ha Hg. + case (Zle_lt_or_eq 0 (b/Zgcd a b)); auto. + apply Zdiv_pos; auto with zarith. + intros H; generalize Ha. + pattern b at 1; rewrite (Zdivide_Zdiv_eq (Zgcd a b) b); auto. + rewrite <- H; auto with zarith. + assert (F := (Zgcd_is_gcd a b)); inversion F; auto. + Qed. diff --git a/theories/Ints/num/BigQ.v b/theories/Ints/num/BigQ.v new file mode 100644 index 0000000000..bd889e12f2 --- /dev/null +++ b/theories/Ints/num/BigQ.v @@ -0,0 +1,22 @@ +Require Export QMake_base. +Require Import QpMake. +Require Import QvMake. +Require Import Q0Make. +Require Import QifMake. +Require Import QbiMake. + +(* We choose for Q the implemention with + multiple representation of 0: 0, 1/0, 2/0 etc *) +Module BigQ := Q0. + +Definition bigQ := BigQ.t. + +Delimit Scope bigQ_scope with bigQ. +Bind Scope bigQ_scope with bigQ. +Bind Scope bigQ_scope with BigQ.t. + +Notation " i + j " := (BigQ.add i j) : bigQ_scope. +Notation " i - j " := (BigQ.sub i j) : bigQ_scope. +Notation " i * j " := (BigQ.mul i j) : bigQ_scope. +Notation " i / j " := (BigQ.div i j) : bigQ_scope. +Notation " i ?= j " := (BigQ.compare i j) : bigQ_scope. diff --git a/theories/Ints/num/GenDiv.v b/theories/Ints/num/GenDiv.v index 3bf0615c2b..6466c198ff 100644 --- a/theories/Ints/num/GenDiv.v +++ b/theories/Ints/num/GenDiv.v @@ -944,8 +944,8 @@ Section GenDivGt. (spec_add_mul_div bh bl Hb) (spec_add_mul_div bl w_0 Hb); rewrite spec_w_0; repeat rewrite Zmult_0_l;repeat rewrite Zplus_0_l; - rewrite Zdiv_0;repeat rewrite Zplus_0_r. - Spec_w_to_Z ah;Spec_w_to_Z bh. 2:apply Zpower_lt_0;zarith. + rewrite Zdiv_0_l;repeat rewrite Zplus_0_r. + Spec_w_to_Z ah;Spec_w_to_Z bh. unfold base;repeat rewrite Zmod_shift_r;zarith. assert (H3:=to_Z_div_minus_p ah HHHH);assert(H4:=to_Z_div_minus_p al HHHH); assert (H5:=to_Z_div_minus_p bl HHHH). diff --git a/theories/Ints/num/GenDivn1.v b/theories/Ints/num/GenDivn1.v index f404c92433..84bf247f75 100644 --- a/theories/Ints/num/GenDivn1.v +++ b/theories/Ints/num/GenDivn1.v @@ -328,11 +328,7 @@ Section GENDIVN1. assert (U3 : 0 < Zpos w_digits). exact (refl_equal Lt). destruct x;unfold high;fold high. unfold gen_to_Z,zn2z_to_Z;rewrite spec_0. - rewrite Zdiv_0;trivial. - apply Zpower_lt_0;auto with zarith. - change (Zpos (gen_digits w_digits (S n))) with - (2*Zpos (gen_digits w_digits n)). - auto with zarith. + rewrite Zdiv_0_l;trivial. assert (U0 := spec_gen_to_Z w_digits w_to_Z spec_to_Z n w0); assert (U1 := spec_gen_to_Z w_digits w_to_Z spec_to_Z n w1). simpl [!S n|WW w0 w1!]. @@ -396,10 +392,9 @@ Section GENDIVN1. assert ([|w_add_mul_div (w_head0 b) b w_0|] = 2 ^ [|w_head0 b|] * [|b|]). rewrite (spec_add_mul_div b w_0); auto with zarith. - rewrite spec_0;rewrite Zdiv_0; try omega. + rewrite spec_0;rewrite Zdiv_0_l; try omega. rewrite Zplus_0_r; rewrite Zmult_comm. rewrite Zmod_def_small; auto with zarith. - apply Zpower_lt_0; try omega. assert (H5 := spec_to_Z (high n a)). assert ([|w_add_mul_div (w_head0 b) w_0 (high n a)|] @@ -429,7 +424,7 @@ Section GENDIVN1. (w_add_mul_div (w_head0 b) w_0 (high n a)) a (gen_0 w_0 n)) as (q,r). assert (U:= spec_gen_digits n). - rewrite spec_gen_0 in H7;trivial;rewrite Zdiv_0 in H7. + rewrite spec_gen_0 in H7;trivial;rewrite Zdiv_0_l in H7. rewrite Zplus_0_r in H7. rewrite spec_add_mul_div in H7;auto with zarith. rewrite spec_0 in H7;rewrite Zmult_0_l in H7;rewrite Zplus_0_l in H7. @@ -487,7 +482,6 @@ Section GENDIVN1. apply Zdiv_lt_upper_bound;auto with zarith. rewrite Zmult_comm;auto with zarith. exact (spec_gen_to_Z w_digits w_to_Z spec_to_Z n a). - apply Zpower_lt_0;auto with zarith. Qed. diff --git a/theories/Ints/num/GenLift.v b/theories/Ints/num/GenLift.v index 68d03fd82f..a7d8480ba6 100644 --- a/theories/Ints/num/GenLift.v +++ b/theories/Ints/num/GenLift.v @@ -290,7 +290,7 @@ Section GenLift. contradict H0; case (spec_to_Z xl); auto with zarith. Qed. - Hint Rewrite Zdiv_0 Zmult_0_l Zplus_0_l Zmult_0_r Zplus_0_r + Hint Rewrite Zdiv_0_l Zmult_0_l Zplus_0_l Zmult_0_r Zplus_0_r spec_w_W0 spec_w_0W spec_w_WW spec_w_0 (wB_div w_digits w_to_Z spec_to_Z) (wB_div_plus w_digits w_to_Z spec_to_Z) : w_rewrite. diff --git a/theories/Ints/num/Q0Make.v b/theories/Ints/num/Q0Make.v new file mode 100644 index 0000000000..09a060e421 --- /dev/null +++ b/theories/Ints/num/Q0Make.v @@ -0,0 +1,1343 @@ +Require Import Bool. +Require Import ZArith. +Require Import Znumtheory. +Require Import ZAux. +Require Import ZDivModAux. +Require Import Arith. +Require Export BigN. +Require Export BigZ. +Require Import QArith. +Require Import Qcanon. +Require Import QBAux. +Require Import QMake_base. + +Module Q0. + + (* Troisieme solution : + 0 a de nombreuse representation : + 0, -0, 1/0, ... n/0, + il faut alors faire attention avec la comparaison et l'addition + *) + + 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 of_Q q: t := + match q with x # y => + Qq (BigZ.of_Z x) (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 => if BigN.eq_bool y BigN.zero then 0%Q + else BigZ.to_Z x # Z2P (BigN.to_Z 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. + 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_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. + 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_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 => + 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])%Q. + 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. + + Theorem spec_comparec: forall q1 q2, + compare q1 q2 = ([[q1]] ?= [[q2]]). + unfold Qccompare, to_Qc. + intros q1 q2; rewrite spec_compare; simpl; auto. + apply Qcompare_comp; apply Qeq_sym; apply Qred_correct. + Qed. + +(* 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])%Q. + 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 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. + 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. + + 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; auto. + 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 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 x y: + ([add_norm x y] == [x] + [y])%Q. + 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. + + 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; auto. + 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 := add x (opp y). + + + Theorem spec_sub x y: + ([sub x y] == [x] - [y])%Q. + intros x y; unfold sub; rewrite spec_add; auto. + rewrite spec_opp; ring. + Qed. + + Theorem spec_subc x y: [[sub x y]] = [[x]] - [[y]]. + intros x y; unfold sub; rewrite spec_addc; auto. + 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; auto. + 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; auto. + 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.mul dx 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. + 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. + + 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; auto. + 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 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 x y: + ([mul_norm x y] == [x] * [y])%Q. + 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. + + 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; auto. + 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) => 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 x: + ([inv x] == /[x])%Q. + 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. + + 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; auto. + 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: 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 x: ([inv_norm x] == /[x])%Q. + 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. + + Theorem spec_inv_normc x: + [[inv_norm 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_norm; auto. + unfold Qcinv, Q2Qc. + apply Qc_decomp; intros _ _; unfold this. + apply Qred_complete. + apply Qinv_comp; apply Qeq_sym; apply Qred_correct. + 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.square 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. + 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. + + 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; 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. + + + 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 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. + 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. + + 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; 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. diff --git a/theories/Ints/num/QMake.v b/theories/Ints/num/QMake.v deleted file mode 100644 index d24a318cd5..0000000000 --- a/theories/Ints/num/QMake.v +++ /dev/null @@ -1,901 +0,0 @@ -Require Import Bool. -Require Import ZArith. -Require Import Arith. -Require Export BigN. -Require Export BigZ. - -Inductive q_type : Set := - | Qz : BigZ.t -> q_type - | Qq : BigZ.t -> BigN.t -> q_type. - -Definition print_type x := - match x with - | Qz _ => Z - | _ => (Z*Z)%type - end. - -Definition print x := - match x return print_type x with - | Qz zx => BigZ.to_Z zx - | Qq nx dx => (BigZ.to_Z nx, BigN.to_Z dx) - end. - -Module Qp. - - Definition t := q_type. - - Definition zero := Qz BigZ.zero. - Definition one := Qz BigZ.one. - Definition minus_one := Qz BigZ.minus_one. - - Definition of_Z x := Qz (BigZ.of_Z x). - - Definition d_to_Z d := BigZ.Pos (BigN.succ d). - - Definition compare x y := - 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. - - Definition opp x := - match x with - | Qz zx => Qz (BigZ.opp zx) - | Qq nx dx => Qq (BigZ.opp nx) dx - end. - -(* Inv d > 0, Pour la forme normal unique on veut d > 1 *) - Definition norm n d := - 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). - - Definition add x y := - 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. - - Definition add_norm x y := - 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. - - Definition sub x y := add x (opp y). - - Definition sub_norm x y := add_norm x (opp y). - - Definition mul x y := - 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. - - Definition mul_norm x y := - 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. - - Definition inv x := - 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. - -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 n - | Qq (BigZ.Pos n) d => let d := BigN.succ d in - 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.one then Qz (BigZ.Neg d) - else Qq (BigZ.Pos d) (BigN.pred n) - end. - - - Definition square x := - match x with - | Qz zx => Qz (BigZ.square zx) - | Qq nx dx => Qq (BigZ.square nx) (BigN.pred (BigN.square (BigN.succ dx))) - end. - - Definition power_pos x p := - 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. - -End Qp. - - -Module Qv. - - (* /!\ Invariant maintenu par les fonctions : - - le denominateur n'est jamais nul *) - - Definition t := q_type. - - Definition zero := Qz BigZ.zero. - Definition one := Qz BigZ.one. - Definition minus_one := Qz BigZ.minus_one. - - Definition of_Z x := Qz (BigZ.of_Z x). - - Definition is_valid x := - match x with - | Qz _ => True - | Qq n d => if BigN.eq_bool d BigN.zero then False else True - end. - (* Les fonctions doivent assurer que si leur arguments sont valides alors - le resultat est correct et valide (si c'est un Q) - *) - - Definition compare x y := - match x, y with - | Qz zx, Qz zy => BigZ.compare zx zy - | Qz zx, Qq ny dy => BigZ.compare (BigZ.mul zx (BigZ.Pos dy)) ny - | Qq nx dx, Qz zy => BigZ.compare BigZ.zero zy - | Qq nx dx, Qq ny dy => BigZ.compare (BigZ.mul nx (BigZ.Pos dy)) (BigZ.mul ny (BigZ.Pos dx)) - end. - - Definition opp x := - match x with - | Qz zx => Qz (BigZ.opp zx) - | Qq nx dx => Qq (BigZ.opp nx) dx - end. - - Definition norm n d := - 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 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 d. - - Definition add x y := - match x, y with - | Qz zx, Qz zy => Qz (BigZ.add zx zy) - | Qz zx, Qq ny dy => Qq (BigZ.add (BigZ.mul zx (BigZ.Pos dy)) ny) dy - | Qq nx dx, Qz zy => Qq (BigZ.add nx (BigZ.mul zy (BigZ.Pos dx))) dx - | Qq nx dx, Qq ny dy => - 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. - - Definition add_norm x y := - match x, y with - | Qz zx, Qz zy => Qz (BigZ.add zx zy) - | Qz zx, Qq ny dy => - norm (BigZ.add (BigZ.mul zx (BigZ.Pos dy)) ny) dy - | Qq nx dx, Qz zy => - norm (BigZ.add (BigZ.mul zy (BigZ.Pos dx)) nx) dx - | Qq nx dx, Qq ny dy => - 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. - - Definition sub x y := add x (opp y). - - Definition sub_norm x y := add_norm x (opp y). - - Definition mul x y := - 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. - - Definition mul_norm x y := - 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 - 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 dy gcd in - if BigN.eq_bool d BigN.one then Qz (BigZ.mul zx ny) - else Qq (BigZ.mul zx ny) d - | 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 - 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 dx gcd in - if BigN.eq_bool d BigN.one then Qz (BigZ.mul zy nx) - else Qq (BigZ.mul zy nx) d - | Qq nx dx, Qq ny dy => norm (BigZ.mul nx ny) (BigN.mul dx dy) - end. - - Definition inv x := - match x with - | Qz (BigZ.Pos n) => - if BigN.eq_bool n BigN.zero then zero else Qq BigZ.one n - | Qz (BigZ.Neg n) => - if BigN.eq_bool n BigN.zero then zero else Qq BigZ.minus_one n - | Qq (BigZ.Pos n) d => - if BigN.eq_bool n BigN.zero then zero else Qq (BigZ.Pos d) n - | Qq (BigZ.Neg n) d => - if BigN.eq_bool n BigN.zero then zero else Qq (BigZ.Neg d) n - end. - - Definition square x := - match x with - | Qz zx => Qz (BigZ.square zx) - | Qq nx dx => Qq (BigZ.square nx) (BigN.square dx) - end. - - Definition power_pos x p := - 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. - -End Qv. - -Module Q. - - (* Troisieme solution : - 0 a de nombreuse representation : - 0, -0, 1/0, ... n/0, - il faut alors faire attention avec la comparaison et l'addition - *) - - Definition t := q_type. - - Definition zero := Qz BigZ.zero. - Definition one := Qz BigZ.one. - Definition minus_one := Qz BigZ.minus_one. - - Definition of_Z x := Qz (BigZ.of_Z x). - - Definition compare x y := - 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. - - Definition opp x := - match x with - | Qz zx => Qz (BigZ.opp zx) - | Qq nx dx => Qq (BigZ.opp nx) dx - end. - -(* Je pense que cette fonction normalise bien ... *) - Definition norm n d := - 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. - - Definition add x y := - 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. - - Definition add_norm x y := - 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. - - Definition sub x y := add x (opp y). - - Definition sub_norm x y := add_norm x (opp y). - - Definition mul x y := - 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. - -Definition mul_norm x y := - 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) 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) d - | Qq nx dx, Qq ny dy => - let (nx, dy) := - let gcd := BigN.gcd (BigZ.to_N nx) dy in - if BigN.eq_bool gcd BigN.one then (nx, dy) - else (BigZ.div nx (BigZ.Pos gcd), BigN.div dy gcd) in - let (ny, dx) := - let gcd := BigN.gcd (BigZ.to_N ny) dx in - if BigN.eq_bool gcd BigN.one then (ny, dx) - else (BigZ.div ny (BigZ.Pos gcd), BigN.div dx gcd) 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. - - -Definition inv x := - match x with - | Qz (BigZ.Pos n) => Qq BigZ.one (BigN.pred n) - | Qz (BigZ.Neg n) => Qq BigZ.minus_one (BigN.pred n) - | Qq (BigZ.Pos n) d => Qq (BigZ.Pos (BigN.succ d)) (BigN.pred n) - | Qq (BigZ.Neg n) d => Qq (BigZ.Neg (BigN.succ d)) (BigN.pred n) - end. - - -Definition inv_norm x := - match x with - | Qz (BigZ.Pos n) => 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.one then x else Qq BigZ.minus_one n - | Qq (BigZ.Pos n) d => let d := BigN.succ d in - 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.one then Qz (BigZ.Neg d) - else Qq (BigZ.Pos d) (BigN.pred n) - end. - - Definition square x := - match x with - | Qz zx => Qz (BigZ.square zx) - | Qq nx dx => Qq (BigZ.square nx) (BigN.square dx) - end. - - Definition power_pos x p := - 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. - -End Q. - -Module Qif. - - (* Troisieme solution : - 0 a de nombreuse representation : - 0, -0, 1/0, ... n/0, - il faut alors faire attention avec la comparaison et l'addition - - Les fonctions de normalization s'effectue seulement si les - nombres sont grands. - *) - - Definition t := q_type. - - Definition zero := Qz BigZ.zero. - Definition one := Qz BigZ.one. - Definition minus_one := Qz BigZ.minus_one. - - Definition of_Z x := Qz (BigZ.of_Z x). - - Definition compare x y := - 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. - - Definition opp x := - match x with - | Qz zx => Qz (BigZ.opp zx) - | Qq nx dx => Qq (BigZ.opp nx) dx - end. - - - Definition do_norm_n n := - match n with - | BigN.N0 _ => false - | BigN.N1 _ => false - | BigN.N2 _ => false - | BigN.N3 _ => false - | BigN.N4 _ => false - | BigN.N5 _ => false - | BigN.N6 _ => false - | BigN.N7 _ => false - | BigN.N8 _ => false - | BigN.N9 _ => true - | BigN.N10 _ => true - | BigN.N11 _ => true - | BigN.N12 _ => true - | BigN.N13 _ => true - | BigN.Nn n _ => true - end. - - Definition do_norm_z z := - match z with - | BigZ.Pos n => do_norm_n n - | BigZ.Neg n => do_norm_n n - end. - -Require Import Bool. -(* Je pense que cette fonction normalise bien ... *) - Definition norm n d := - if andb (do_norm_z n) (do_norm_n d) then - 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 - else Qq n d. - - - - Definition add x y := - 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. - - Definition add_norm x y := - 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. - - Definition sub x y := add x (opp y). - - Definition sub_norm x y := add_norm x (opp y). - - Definition mul x y := - 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. - - Definition mul_norm x y := - match x, y with - | Qz zx, Qz zy => Qz (BigZ.mul zx zy) - | Qz zx, Qq ny dy => norm (BigZ.mul zx ny) dy - | Qq nx dx, Qz zy => norm (BigZ.mul nx zy) dx - | Qq nx dx, Qq ny dy => norm (BigZ.mul nx ny) (BigN.mul dx dy) - end. - - Definition inv x := - 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. - - Definition inv_norm x := - match x with - | Qz (BigZ.Pos n) => - if BigN.eq_bool n BigN.zero then zero else Qq BigZ.one n - | Qz (BigZ.Neg n) => - if BigN.eq_bool n BigN.zero then zero else Qq BigZ.minus_one n - | Qq (BigZ.Pos n) d => - if BigN.eq_bool n BigN.zero then zero else Qq (BigZ.Pos d) n - | Qq (BigZ.Neg n) d => - if BigN.eq_bool n BigN.zero then zero else Qq (BigZ.Neg d) n - end. - - Definition square x := - match x with - | Qz zx => Qz (BigZ.square zx) - | Qq nx dx => Qq (BigZ.square nx) (BigN.square dx) - end. - - Definition power_pos x p := - 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. - -End Qif. - -Module Qbi. - - (* Troisieme solution : - 0 a de nombreuse representation : - 0, -0, 1/0, ... n/0, - il faut alors faire attention avec la comparaison et l'addition - - Les fonctions de normalization s'effectue seulement si les - nombres sont grands. - *) - - Definition t := q_type. - - Definition zero := Qz BigZ.zero. - Definition one := Qz BigZ.one. - Definition minus_one := Qz BigZ.minus_one. - - Definition of_Z x := Qz (BigZ.of_Z x). - - Definition compare x y := - 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 - match BigZ.cmp_sign zx ny with - | Lt => Lt - | Gt => Gt - | Eq => BigZ.compare (BigZ.mul zx (BigZ.Pos dy)) ny - end - | Qq nx dx, Qz zy => - if BigN.eq_bool dx BigN.zero then BigZ.compare BigZ.zero zy - else - match BigZ.cmp_sign nx zy with - | Lt => Lt - | Gt => Gt - | Eq => BigZ.compare nx (BigZ.mul zy (BigZ.Pos dx)) - end - | 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 => - match BigZ.cmp_sign nx ny with - | Lt => Lt - | Gt => Gt - | Eq => BigZ.compare (BigZ.mul nx (BigZ.Pos dy)) (BigZ.mul ny (BigZ.Pos dx)) - end - end - end. - - Definition opp x := - match x with - | Qz zx => Qz (BigZ.opp zx) - | Qq nx dx => Qq (BigZ.opp nx) dx - end. - - - Definition do_norm_n n := - match n with - | BigN.N0 _ => false - | BigN.N1 _ => false - | BigN.N2 _ => false - | BigN.N3 _ => false - | BigN.N4 _ => false - | BigN.N5 _ => false - | BigN.N6 _ => false - | BigN.N7 _ => false - | BigN.N8 _ => false - | BigN.N9 _ => true - | BigN.N10 _ => true - | BigN.N11 _ => true - | BigN.N12 _ => true - | BigN.N13 _ => true - | BigN.Nn n _ => true - end. - - Definition do_norm_z z := - match z with - | BigZ.Pos n => do_norm_n n - | BigZ.Neg n => do_norm_n n - end. - -(* Je pense que cette fonction normalise bien ... *) - Definition norm n d := - if andb (do_norm_z n) (do_norm_n d) then - 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 - else Qq n d. - - - Definition add x y := - 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 - if BigN.eq_bool dx dy then - let n := BigZ.add nx ny in - Qq n dx - 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. - - Definition add_norm x y := - 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 - if BigN.eq_bool dx dy then - let n := BigZ.add nx ny in - norm n dx - 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. - - Definition sub x y := add x (opp y). - - Definition sub_norm x y := add_norm x (opp y). - - Definition mul x y := - 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. - - Definition mul_norm x y := - match x, y with - | Qz zx, Qz zy => Qz (BigZ.mul zx zy) - | Qz zx, Qq ny dy => mul (Qz ny) (norm zx dy) - | Qq nx dx, Qz zy => mul (Qz nx) (norm zy dx) - | Qq nx dx, Qq ny dy => mul (norm nx dy) (norm ny dx) - end. - - Definition inv x := - 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. - - Definition inv_norm x := - match x with - | Qz (BigZ.Pos n) => - if BigN.eq_bool n BigN.zero then zero else Qq BigZ.one n - | Qz (BigZ.Neg n) => - if BigN.eq_bool n BigN.zero then zero else Qq BigZ.minus_one n - | Qq (BigZ.Pos n) d => - if BigN.eq_bool n BigN.zero then zero else Qq (BigZ.Pos d) n - | Qq (BigZ.Neg n) d => - if BigN.eq_bool n BigN.zero then zero else Qq (BigZ.Neg d) n - end. - - Definition square x := - match x with - | Qz zx => Qz (BigZ.square zx) - | Qq nx dx => Qq (BigZ.square nx) (BigN.square dx) - end. - - Definition power_pos x p := - 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. - -End Qbi. - - - - diff --git a/theories/Ints/num/QMake_base.v b/theories/Ints/num/QMake_base.v new file mode 100644 index 0000000000..f82c5d25b2 --- /dev/null +++ b/theories/Ints/num/QMake_base.v @@ -0,0 +1,23 @@ +Require Export BigN. +Require Export BigZ. + + + +(* Basic type for Q: a Z or a pair of a Z and an N *) +Inductive q_type : Set := + | Qz : BigZ.t -> q_type + | Qq : BigZ.t -> BigN.t -> q_type. + + + +Definition print_type x := + match x with + | Qz _ => Z + | _ => (Z*Z)%type + end. + +Definition print x := + match x return print_type x with + | Qz zx => BigZ.to_Z zx + | Qq nx dx => (BigZ.to_Z nx, BigN.to_Z dx) + end. diff --git a/theories/Ints/num/QbiMake.v b/theories/Ints/num/QbiMake.v new file mode 100644 index 0000000000..fe7d9cb25d --- /dev/null +++ b/theories/Ints/num/QbiMake.v @@ -0,0 +1,1066 @@ +Require Import Bool. +Require Import ZArith. +Require Import Znumtheory. +Require Import ZAux. +Require Import ZDivModAux. +Require Import Arith. +Require Export BigN. +Require Export BigZ. +Require Import QArith. +Require Import Qcanon. +Require Import QBAux. +Require Import QMake_base. + +Module Qbi. + + (* Troisieme solution : + 0 a de nombreuse representation : + 0, -0, 1/0, ... n/0, + il faut alors faire attention avec la comparaison et l'addition + + Les fonctions de normalization s'effectue seulement si les + nombres sont grands. + *) + + 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 of_Q q: t := + match q with x # y => + Qq (BigZ.of_Z x) (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 => if BigN.eq_bool y BigN.zero then 0%Q + else BigZ.to_Z x # Z2P (BigN.to_Z 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. + 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_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. + 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_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 => + if BigN.eq_bool dy BigN.zero then BigZ.compare zx BigZ.zero + else + match BigZ.cmp_sign zx ny with + | Lt => Lt + | Gt => Gt + | Eq => BigZ.compare (BigZ.mul zx (BigZ.Pos dy)) ny + end + | Qq nx dx, Qz zy => + if BigN.eq_bool dx BigN.zero then BigZ.compare BigZ.zero zy + else + match BigZ.cmp_sign nx zy with + | Lt => Lt + | Gt => Gt + | Eq => BigZ.compare nx (BigZ.mul zy (BigZ.Pos dx)) + end + | 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 => + match BigZ.cmp_sign nx ny with + | Lt => Lt + | Gt => Gt + | Eq => BigZ.compare (BigZ.mul nx (BigZ.Pos dy)) (BigZ.mul ny (BigZ.Pos dx)) + end + end + end. + + Theorem spec_compare: forall q1 q2, + compare q1 q2 = ([q1] ?= [q2])%Q. + 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. + set (a := BigZ.to_Z z1); set (b := BigZ.to_Z x2); + set (c := BigN.to_Z y2); fold c in HH. + assert (F: (0 < c)%Z). + case (Zle_lt_or_eq _ _ (BigN.spec_pos y2)); fold c; auto. + intros H1; case HH; rewrite <- H1; auto. + rewrite Z2P_correct; auto with zarith. + generalize (BigZ.spec_cmp_sign z1 x2); case BigZ.cmp_sign; fold a b c. + intros _; generalize (BigZ.spec_compare (z1 * BigZ.Pos y2)%bigZ x2); + case BigZ.compare; rewrite BigZ.spec_mul; simpl; fold a b c; auto. + intros H1; rewrite H1; rewrite Zcompare_refl; auto. + intros (H1, H2); apply sym_equal; change (a * c < b)%Z. + apply Zlt_le_trans with (2 := H2). + change 0%Z with (0 * c)%Z. + apply Zmult_lt_compat_r; auto with zarith. + intros (H1, H2); apply sym_equal; change (a * c > b)%Z. + apply Zlt_gt. + apply Zlt_le_trans with (1 := H2). + change 0%Z with (0 * c)%Z. + apply Zmult_le_compat_r; auto with zarith. + 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. + set (a := BigZ.to_Z z2); set (b := BigZ.to_Z x1); + set (c := BigN.to_Z y1); fold c in HH. + assert (F: (0 < c)%Z). + case (Zle_lt_or_eq _ _ (BigN.spec_pos y1)); fold c; auto. + intros H1; case HH; rewrite <- H1; auto. + rewrite Zmult_1_r; rewrite Z2P_correct; auto with zarith. + generalize (BigZ.spec_cmp_sign x1 z2); case BigZ.cmp_sign; fold a b c. + intros _; generalize (BigZ.spec_compare x1 (z2 * BigZ.Pos y1)%bigZ); + case BigZ.compare; rewrite BigZ.spec_mul; simpl; fold a b c; auto. + intros H1; rewrite H1; rewrite Zcompare_refl; auto. + intros (H1, H2); apply sym_equal; change (b < a * c)%Z. + apply Zlt_le_trans with (1 := H1). + change 0%Z with (0 * c)%Z. + apply Zmult_le_compat_r; auto with zarith. + intros (H1, H2); apply sym_equal; change (b > a * c)%Z. + apply Zlt_gt. + apply Zlt_le_trans with (2 := H1). + change 0%Z with (0 * c)%Z. + apply Zmult_lt_compat_r; auto with zarith. + 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. + set (a := BigZ.to_Z x1); set (b := BigZ.to_Z x2); + set (c1 := BigN.to_Z y1); set (c2 := BigN.to_Z y2). + fold c1 in HH; fold c2 in HH1. + assert (F1: (0 < c1)%Z). + case (Zle_lt_or_eq _ _ (BigN.spec_pos y1)); fold c1; auto. + intros H1; case HH; rewrite <- H1; auto. + assert (F2: (0 < c2)%Z). + case (Zle_lt_or_eq _ _ (BigN.spec_pos y2)); fold c2; auto. + intros H1; case HH1; rewrite <- H1; auto. + repeat rewrite Z2P_correct; auto. + generalize (BigZ.spec_cmp_sign x1 x2); case BigZ.cmp_sign. + intros _; generalize (BigZ.spec_compare (x1 * BigZ.Pos y2)%bigZ + (x2 * BigZ.Pos y1)%bigZ); + case BigZ.compare; rewrite BigZ.spec_mul; simpl; fold a b c1 c2; auto. + rewrite BigZ.spec_mul; simpl; fold a b c1; intros HH2; rewrite HH2; + rewrite Zcompare_refl; auto. + rewrite BigZ.spec_mul; simpl; auto. + rewrite BigZ.spec_mul; simpl; auto. + fold a b; intros (H1, H2); apply sym_equal; change (a * c2 < b * c1)%Z. + apply Zlt_le_trans with 0%Z. + change 0%Z with (0 * c2)%Z. + apply Zmult_lt_compat_r; auto with zarith. + apply Zmult_le_0_compat; auto with zarith. + fold a b; intros (H1, H2); apply sym_equal; change (a * c2 > b * c1)%Z. + apply Zlt_gt; apply Zlt_le_trans with 0%Z. + change 0%Z with (0 * c1)%Z. + apply Zmult_lt_compat_r; auto with zarith. + apply Zmult_le_0_compat; auto with zarith. + Qed. + + + Definition do_norm_n n := + match n with + | BigN.N0 _ => false + | BigN.N1 _ => false + | BigN.N2 _ => false + | BigN.N3 _ => false + | BigN.N4 _ => false + | BigN.N5 _ => false + | BigN.N6 _ => false + | BigN.N7 _ => false + | BigN.N8 _ => false + | BigN.N9 _ => true + | BigN.N10 _ => true + | BigN.N11 _ => true + | BigN.N12 _ => true + | BigN.N13 _ => true + | BigN.Nn n _ => true + end. + + Definition do_norm_z z := + match z with + | BigZ.Pos n => do_norm_n n + | BigZ.Neg n => do_norm_n n + end. + +(* Je pense que cette fonction normalise bien ... *) + Definition norm n d: t := + if andb (do_norm_z n) (do_norm_n d) then + 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 + else Qq n d. + + Theorem spec_norm: forall n q, + ([norm n q] == [Qq n q])%Q. + intros p q; unfold norm. + case do_norm_z; simpl andb. + 2: apply Qeq_refl. + case do_norm_n. + 2: apply Qeq_refl. + 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 + if BigN.eq_bool dx dy then + let n := BigZ.add nx ny in + Qq n dx + 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 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. + 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. + generalize (BigN.spec_eq_bool dx dy); + case BigN.eq_bool; intros HH3. + rewrite <- HH3. + assert (Fx: (0 < BigN.to_Z dx)%Z). + generalize (BigN.spec_pos dx); auto with zarith. + red; simpl. + generalize (BigN.spec_eq_bool dx BigN.zero); + case BigN.eq_bool; rewrite BigN.spec_0; intros HH4. + case HH; auto. + simpl; rewrite Zpos_mult_morphism. + repeat rewrite Z2P_correct; auto with zarith. + rewrite BigZ.spec_add; repeat rewrite BigZ.spec_mul; simpl. + ring. + 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. + 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_mul; + rewrite BigN.spec_0; intros H3; simpl. + absurd (0 < 0)%Z; auto with zarith. + rewrite BigZ.spec_add; repeat rewrite BigZ.spec_mul; simpl. + repeat rewrite Z2P_correct; 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; auto. + 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 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 + if BigN.eq_bool dx dy then + let n := BigZ.add nx ny in + norm n dx + 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 x y: + ([add_norm x y] == [x] + [y])%Q. + 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 |- context[BigN.eq_bool ?X ?Y] => + generalize (BigN.spec_eq_bool X Y); case BigN.eq_bool + end; intros HH3; + match goal with |- [norm ?X ?Y] == _ => + apply Qeq_trans with ([Qq X Y]); + [apply spec_norm | idtac] + end; apply Qeq_refl. + 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; auto. + 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 := add x (opp y). + + Theorem spec_sub x y: + ([sub x y] == [x] - [y])%Q. + intros x y; unfold sub; rewrite spec_add; auto. + rewrite spec_opp; ring. + Qed. + + Theorem spec_subc x y: [[sub x y]] = [[x]] - [[y]]. + intros x y; unfold sub; rewrite spec_addc; auto. + 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; auto. + 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; auto. + 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.mul dx 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. + 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. + + 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; auto. + 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 => mul (Qz ny) (norm zx dy) + | Qq nx dx, Qz zy => mul (Qz nx) (norm zy dx) + | Qq nx dx, Qq ny dy => mul (norm nx dy) (norm ny dx) + end. + + Theorem spec_mul_norm x y: + ([mul_norm x y] == [x] * [y])%Q. + intros x y; rewrite <- spec_mul; auto. + unfold mul_norm; case x; case y; clear x y. + intros; apply Qeq_refl. + intros p1 n p2. + repeat rewrite spec_mul. + match goal with |- ?Z == _ => + match Z with context id [norm ?X ?Y] => + let y := context id [Qq X Y] in + apply Qeq_trans with y; [repeat apply Qmult_comp; + repeat apply Qplus_comp; repeat apply Qeq_refl; + apply spec_norm | idtac] + end + end. + 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 HH; simpl; ring. + intros p1 p2 n. + repeat rewrite spec_mul. + match goal with |- ?Z == _ => + match Z with context id [norm ?X ?Y] => + let y := context id [Qq X Y] in + apply Qeq_trans with y; [repeat apply Qmult_comp; + repeat apply Qplus_comp; repeat apply Qeq_refl; + apply spec_norm | idtac] + end + end. + 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 HH; simpl; try ring. + rewrite Pmult_1_r; auto. + intros p1 n1 p2 n2. + repeat rewrite spec_mul. + repeat match goal with |- ?Z == _ => + match Z with context id [norm ?X ?Y] => + let y := context id [Qq X Y] in + apply Qeq_trans with y; [repeat apply Qmult_comp; + repeat apply Qplus_comp; repeat apply Qeq_refl; + apply spec_norm | idtac] + end + end. + 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; + 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; try ring. + repeat rewrite Zpos_mult_morphism; ring. + 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; auto. + 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) => 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 x: + ([inv x] == /[x])%Q. + 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. + + 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; auto. + 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: t): t := + match x with + | Qz (BigZ.Pos n) => + if BigN.eq_bool n BigN.zero then zero else Qq BigZ.one n + | Qz (BigZ.Neg n) => + if BigN.eq_bool n BigN.zero then zero else Qq BigZ.minus_one n + | Qq (BigZ.Pos n) d => + if BigN.eq_bool n BigN.zero then zero else Qq (BigZ.Pos d) n + | Qq (BigZ.Neg n) d => + if BigN.eq_bool n BigN.zero then zero else Qq (BigZ.Neg d) n + end. + + Theorem spec_inv_norm x: ([inv_norm x] == /[x])%Q. + intros x; rewrite <- spec_inv; generalize x; clear x. + intros [ [x | x] | [nx | 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 H1; try 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; intros H2; auto; + case H2; auto. + Qed. + + Theorem spec_inv_normc x: + [[inv_norm 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_norm; auto. + unfold Qcinv, Q2Qc. + apply Qc_decomp; intros _ _; unfold this. + apply Qred_complete. + apply Qinv_comp; apply Qeq_sym; apply Qred_correct. + 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.square 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. + 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. + + 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; 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. + + 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 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. + 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. + + 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; 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 Qbi. + + + + diff --git a/theories/Ints/num/QifMake.v b/theories/Ints/num/QifMake.v new file mode 100644 index 0000000000..3ee0227766 --- /dev/null +++ b/theories/Ints/num/QifMake.v @@ -0,0 +1,975 @@ +Require Import Bool. +Require Import ZArith. +Require Import Znumtheory. +Require Import ZAux. +Require Import ZDivModAux. +Require Import Arith. +Require Export BigN. +Require Export BigZ. +Require Import QArith. +Require Import Qcanon. +Require Import QBAux. +Require Import QMake_base. + +Module Qif. + + (* Troisieme solution : + 0 a de nombreuse representation : + 0, -0, 1/0, ... n/0, + il faut alors faire attention avec la comparaison et l'addition + + Les fonctions de normalization s'effectue seulement si les + nombres sont grands. + *) + + 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 of_Q q: t := + match q with x # y => + Qq (BigZ.of_Z x) (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 => if BigN.eq_bool y BigN.zero then 0%Q + else BigZ.to_Z x # Z2P (BigN.to_Z 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. + 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_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. + 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_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 => + 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])%Q. + 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 do_norm_n n := + match n with + | BigN.N0 _ => false + | BigN.N1 _ => false + | BigN.N2 _ => false + | BigN.N3 _ => false + | BigN.N4 _ => false + | BigN.N5 _ => false + | BigN.N6 _ => false + | BigN.N7 _ => false + | BigN.N8 _ => false + | BigN.N9 _ => true + | BigN.N10 _ => true + | BigN.N11 _ => true + | BigN.N12 _ => true + | BigN.N13 _ => true + | BigN.Nn n _ => true + end. + + Definition do_norm_z z := + match z with + | BigZ.Pos n => do_norm_n n + | BigZ.Neg n => do_norm_n n + end. + +(* Je pense que cette fonction normalise bien ... *) + Definition norm n d: t := + if andb (do_norm_z n) (do_norm_n d) then + 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 + else Qq n d. + + Theorem spec_norm: forall n q, + ([norm n q] == [Qq n q])%Q. + intros p q; unfold norm. + case do_norm_z; simpl andb. + 2: apply Qeq_refl. + case do_norm_n. + 2: apply Qeq_refl. + 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 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. + 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. + + 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; auto. + 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 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 x y: + ([add_norm x y] == [x] + [y])%Q. + 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. + + 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; auto. + 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 := add x (opp y). + + + Theorem spec_sub x y: + ([sub x y] == [x] - [y])%Q. + intros x y; unfold sub; rewrite spec_add; auto. + rewrite spec_opp; ring. + Qed. + + Theorem spec_subc x y: [[sub x y]] = [[x]] - [[y]]. + intros x y; unfold sub; rewrite spec_addc; auto. + 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; auto. + 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; auto. + 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.mul dx 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. + 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. + + 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; auto. + 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 => norm (BigZ.mul zx ny) dy + | Qq nx dx, Qz zy => norm (BigZ.mul nx zy) dx + | Qq nx dx, Qq ny dy => norm (BigZ.mul nx ny) (BigN.mul dx dy) + end. + + Theorem spec_mul_norm x y: + ([mul_norm x y] == [x] * [y])%Q. + 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. + match goal with |- [norm ?X ?Y] == _ => + apply Qeq_trans with ([Qq X Y]); + [apply spec_norm | idtac] + end; apply Qeq_refl. + intros p1 p2 n. + match goal with |- [norm ?X ?Y] == _ => + apply Qeq_trans with ([Qq X Y]); + [apply spec_norm | idtac] + end; apply Qeq_refl. + intros p1 n1 p2 n2. + match goal with |- [norm ?X ?Y] == _ => + apply Qeq_trans with ([Qq X Y]); + [apply spec_norm | idtac] + end; apply Qeq_refl. + 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; auto. + 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) => 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 x: + ([inv x] == /[x])%Q. + 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. + + 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; auto. + 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: 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 x: ([inv_norm x] == /[x])%Q. + 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. + + Theorem spec_inv_normc x: + [[inv_norm 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_norm; auto. + unfold Qcinv, Q2Qc. + apply Qc_decomp; intros _ _; unfold this. + apply Qred_complete. + apply Qinv_comp; apply Qeq_sym; apply Qred_correct. + 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.square 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. + 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. + + 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; 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. + + +End Qif. diff --git a/theories/Ints/num/QpMake.v b/theories/Ints/num/QpMake.v new file mode 100644 index 0000000000..1ae9fa4ef3 --- /dev/null +++ b/theories/Ints/num/QpMake.v @@ -0,0 +1,878 @@ +Require Import Bool. +Require Import ZArith. +Require Import Znumtheory. +Require Import ZAux. +Require Import ZDivModAux. +Require Import Arith. +Require Export BigN. +Require Export BigZ. +Require Import QArith. +Require Import Qcanon. +Require Import QBAux. +Require Import QMake_base. + + +Module Qp. + + 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; auto with zarith. + 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; auto with zarith. + 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; auto with zarith. + 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 spec_succ_pos. + 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 Zplus_comm. + rewrite BigN.succ_pred; try apply Qeq_refl; apply spec_succ_pos. + 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. + 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. + 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. + 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; 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; 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; 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; 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 (Zopp (Zpos Y)); + 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; 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; 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. + 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. + 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; 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; rewrite BigN.spec_power_pos; auto. + 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. + 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. diff --git a/theories/Ints/num/QvMake.v b/theories/Ints/num/QvMake.v new file mode 100644 index 0000000000..c223b6bd23 --- /dev/null +++ b/theories/Ints/num/QvMake.v @@ -0,0 +1,1134 @@ +Require Import Bool. +Require Import ZArith. +Require Import Znumtheory. +Require Import ZAux. +Require Import ZDivModAux. +Require Import Arith. +Require Export BigN. +Require Export BigZ. +Require Import QArith. +Require Import Qcanon. +Require Import QBAux. +Require Import QMake_base. + +Module Qv. + + (* /!\ Invariant maintenu par les fonctions : + - le denominateur n'est jamais nul *) + + 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 wf x := + match x with + | Qz _ => True + | Qq n d => if BigN.eq_bool d BigN.zero then False else True + end. + + Definition of_Q q: t := + match q with x # y => + Qq (BigZ.of_Z x) (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 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; simpl. + rewrite (BigN.spec_of_pos); 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 wf_opp: forall x, wf x -> wf (opp x). + intros [zx | nx dx]; unfold opp, wf; auto. + Qed. + + 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. + + (* Les fonctions doivent assurer que si leur arguments sont valides alors + le resultat est correct et valide (si c'est un Q) + *) + + 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 (BigZ.Pos dy)) ny + | Qq nx dx, Qz zy => BigZ.compare nx (BigZ.mul zy (BigZ.Pos dx)) + | Qq nx dx, Qq ny dy => BigZ.compare (BigZ.mul nx (BigZ.Pos dy)) (BigZ.mul ny (BigZ.Pos dx)) + end. + + Theorem spec_compare: forall q1 q2, wf q1 -> wf q2 -> + compare q1 q2 = ([q1] ?= [q2])%Q. + intros [z1 | x1 y1] [z2 | x2 y2]; + unfold Qcompare, compare, to_Q, Qnum, Qden, wf. + 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. + intros _ _ HH; case HH. + rewrite BigN.spec_0; intros HH _ _. + 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. + intros _ HH; case HH. + rewrite BigN.spec_0; intros HH _ _. + 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. + intros _ HH; case HH. + rewrite BigN.spec_0; intros HH1. + generalize (BigN.spec_eq_bool y2 BigN.zero); + case BigN.eq_bool. + intros _ _ HH; case HH. + rewrite BigN.spec_0; intros HH2 _ _. + 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. + + Theorem spec_comparec: forall q1 q2, wf q1 -> wf q2 -> + compare q1 q2 = ([[q1]] ?= [[q2]]). + unfold Qccompare, to_Qc. + intros q1 q2 Hq1 Hq2; rewrite spec_compare; simpl; auto. + apply Qcompare_comp; apply Qeq_sym; apply Qred_correct. + Qed. + + 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 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 d. + + Theorem wf_norm: forall n q, + (BigN.to_Z q <> 0)%Z -> wf (norm n q). + intros p q; unfold norm, wf; 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. + simpl; 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_1. + match goal with |- context[BigN.eq_bool ?X ?Y] => + generalize (BigN.spec_eq_bool X Y); case BigN.eq_bool + end; 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_1. + 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. + set (a := BigN.to_Z (BigZ.to_N p)). + set (b := (BigN.to_Z q)). + assert (F: (0 < Zgcd a b)%Z). + case (Zle_lt_or_eq _ _ (Zgcd_is_pos a b)); auto. + intros HH1; case Hq; apply (Zgcd_inv_0_r _ _ (sym_equal HH1)). + rewrite BigN.spec_div; rewrite BigN.spec_gcd; auto; fold a; fold b. + intros H; case Hq; fold b. + rewrite (Zdivide_Zdiv_eq (Zgcd a b) b); auto. + rewrite H; auto with zarith. + assert (F1:= Zgcd_is_gcd a b); inversion F1; auto. + Qed. + + Theorem spec_norm: forall n q, + ((0 < BigN.to_Z q)%Z -> [norm n q] == [Qq n 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 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. + 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 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 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 (BigZ.Pos dy)) ny) dy + | Qq nx dx, Qz zy => Qq (BigZ.add nx (BigZ.mul zy (BigZ.Pos dx))) dx + | Qq nx dx, Qq ny dy => + 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. + + Theorem wf_add: forall x y, wf x -> wf y -> wf (add x y). + intros [zx | nx dx] [zy | ny dy]; unfold add, wf; auto. + 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_mul. + intros H1 H2 H3. + case (Zmult_integral _ _ H1); auto with zarith. + Qed. + + Theorem spec_add x y: wf x -> wf 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. + intros; apply Qeq_refl; auto. + assert (F1:= BigN.spec_pos dy). + rewrite Zmult_1_r. + generalize (BigN.spec_eq_bool dy BigN.zero); + case BigN.eq_bool. + intros _ _ HH; case HH. + rewrite BigN.spec_0; intros HH _ _. + rewrite Z2P_correct; auto with zarith. + rewrite BigZ.spec_add; rewrite BigZ.spec_mul. + simpl; apply Qeq_refl. + generalize (BigN.spec_eq_bool dx BigN.zero); + case BigN.eq_bool. + intros _ HH; case HH. + rewrite BigN.spec_0; intros HH _ _. + assert (F1:= BigN.spec_pos dx). + rewrite Zmult_1_r; rewrite Pmult_1_r. + simpl; rewrite Z2P_correct; auto with zarith. + rewrite BigZ.spec_add; rewrite BigZ.spec_mul; simpl. + apply Qeq_refl. + generalize (BigN.spec_eq_bool dx BigN.zero); + case BigN.eq_bool. + intros _ HH; case HH. + rewrite BigN.spec_0; intros HH1. + generalize (BigN.spec_eq_bool dy BigN.zero); + case BigN.eq_bool. + intros _ _ HH; case HH. + rewrite BigN.spec_0; intros HH2 _ _. + 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. + rewrite BigZ.spec_add; repeat rewrite BigN.spec_mul. + red; simpl. + rewrite Zpos_mult_morphism. + repeat rewrite Z2P_correct; auto. + repeat rewrite BigZ.spec_mul; simpl; auto. + apply Zmult_lt_0_compat; auto. + Qed. + + Theorem spec_addc x y: wf x -> wf y -> + [[add x y]] = [[x]] + [[y]]. + intros x y H1 H2; 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. + + 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 => + norm (BigZ.add (BigZ.mul zx (BigZ.Pos dy)) ny) dy + | Qq nx dx, Qz zy => + norm (BigZ.add (BigZ.mul zy (BigZ.Pos dx)) nx) dx + | Qq nx dx, Qq ny dy => + 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 wf_add_norm: forall x y, wf x -> wf y -> wf (add_norm x y). + intros [zx | nx dx] [zy | ny dy]; unfold add_norm; auto. + intros HH1 HH2; apply wf_norm. + generalize HH2; simpl. + match goal with |- context[BigN.eq_bool ?X ?Y] => + generalize (BigN.spec_eq_bool X Y); case BigN.eq_bool + end; auto. + intros HH1 HH2; apply wf_norm. + generalize HH1; simpl. + match goal with |- context[BigN.eq_bool ?X ?Y] => + generalize (BigN.spec_eq_bool X Y); case BigN.eq_bool + end; auto. + intros HH1 HH2; apply wf_norm. + rewrite BigN.spec_mul; intros HH3. + case (Zmult_integral _ _ HH3). + generalize HH1; simpl. + match goal with |- context[BigN.eq_bool ?X ?Y] => + generalize (BigN.spec_eq_bool X Y); case BigN.eq_bool + end; auto. + generalize HH2; simpl. + match goal with |- context[BigN.eq_bool ?X ?Y] => + generalize (BigN.spec_eq_bool X Y); case BigN.eq_bool + end; auto. + Qed. + + Theorem spec_add_norm x y: wf x -> wf y -> + ([add_norm x y] == [x] + [y])%Q. + intros x y H1 H2; rewrite <- spec_add; auto. + generalize H1 H2; unfold add_norm, add, wf; case x; case y; clear H1 H2. + intros; apply Qeq_refl. + intros p1 n p2 _. + generalize (BigN.spec_eq_bool n BigN.zero); + case BigN.eq_bool. + intros _ HH; case HH. + rewrite BigN.spec_0; intros HH _. + match goal with |- [norm ?X ?Y] == _ => + apply Qeq_trans with ([Qq X Y]); + [apply spec_norm | idtac] + end. + generalize (BigN.spec_pos n); auto with zarith. + simpl. + repeat rewrite BigZ.spec_add. + repeat rewrite BigZ.spec_mul; simpl. + apply Qeq_refl. + intros p1 n p2. + generalize (BigN.spec_eq_bool p2 BigN.zero); + case BigN.eq_bool. + intros _ HH; case HH. + rewrite BigN.spec_0; intros HH _ _. + match goal with |- [norm ?X ?Y] == _ => + apply Qeq_trans with ([Qq X Y]); + [apply spec_norm | idtac] + end. + generalize (BigN.spec_pos p2); auto with zarith. + simpl. + repeat rewrite BigZ.spec_add. + repeat rewrite BigZ.spec_mul; simpl. + rewrite Zplus_comm. + apply Qeq_refl. + intros p1 q1 p2 q2. + generalize (BigN.spec_eq_bool q2 BigN.zero); + case BigN.eq_bool. + intros _ HH; case HH. + rewrite BigN.spec_0; intros HH1 _. + generalize (BigN.spec_eq_bool q1 BigN.zero); + case BigN.eq_bool. + intros _ HH; case HH. + rewrite BigN.spec_0; intros HH2 _. + match goal with |- [norm ?X ?Y] == _ => + apply Qeq_trans with ([Qq X Y]); + [apply spec_norm | idtac] + end; try apply Qeq_refl. + rewrite BigN.spec_mul. + apply Zmult_lt_0_compat. + generalize (BigN.spec_pos q2); auto with zarith. + generalize (BigN.spec_pos q1); auto with zarith. + Qed. + + Theorem spec_add_normc x y: wf x -> wf y -> + [[add_norm x y]] = [[x]] + [[y]]. + intros x y Hx Hy; 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. + + Definition sub x y := add x (opp y). + + Theorem wf_sub x y: wf x -> wf y -> wf (sub x y). + intros x y Hx Hy; unfold sub; apply wf_add; auto. + apply wf_opp; auto. + Qed. + + Theorem spec_sub x y: wf x -> wf y -> + ([sub x y] == [x] - [y])%Q. + intros x y Hx Hy; unfold sub; rewrite spec_add; auto. + apply wf_opp; auto. + rewrite spec_opp; ring. + Qed. + + Theorem spec_subc x y: wf x -> wf y -> + [[sub x y]] = [[x]] - [[y]]. + intros x y Hx Hy; unfold sub; rewrite spec_addc; auto. + rewrite spec_oppc; ring. + apply wf_opp; auto. + Qed. + + Definition sub_norm x y := add_norm x (opp y). + + Theorem wf_sub_norm x y: wf x -> wf y -> wf (sub_norm x y). + intros x y Hx Hy; unfold sub_norm; apply wf_add_norm; auto. + apply wf_opp; auto. + Qed. + + Theorem spec_sub_norm x y: wf x -> wf y -> + ([sub_norm x y] == [x] - [y])%Q. + intros x y Hx Hy; unfold sub_norm; rewrite spec_add_norm; auto. + apply wf_opp; auto. + rewrite spec_opp; ring. + Qed. + + Theorem spec_sub_normc x y: wf x -> wf y -> + [[sub_norm x y]] = [[x]] - [[y]]. + intros x y Hx Hy; unfold sub_norm; rewrite spec_add_normc; auto. + rewrite spec_oppc; ring. + apply wf_opp; auto. + 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 wf_mul: forall x y, wf x -> wf y -> wf (mul x y). + intros [zx | nx dx] [zy | ny dy]; unfold mul, wf; auto. + 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_mul. + intros H1 H2 H3. + case (Zmult_integral _ _ H1); auto with zarith. + Qed. + + Theorem spec_mul x y: wf x -> wf 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. + 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; auto. + intros _ _ HH; case HH. + rewrite BigN.spec_0; intros HH1 _ _. + 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; auto. + intros _ HH; case HH. + rewrite BigN.spec_0; intros HH1 _ _. + 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; auto. + intros _ HH; case HH. + match goal with |- context[BigN.eq_bool ?X ?Y] => + generalize (BigN.spec_eq_bool X Y); case BigN.eq_bool + end; auto. + intros _ _ _ HH; case HH. + rewrite BigN.spec_0; intros H1 H2 _ _. + rewrite BigZ.spec_mul; rewrite BigN.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. + + Theorem spec_mulc x y: wf x -> wf y -> + [[mul x y]] = [[x]] * [[y]]. + intros x y Hx Hy; 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. + + 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 + 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 dy gcd in + if BigN.eq_bool d BigN.one then Qz (BigZ.mul zx ny) + else Qq (BigZ.mul zx ny) d + | 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 + 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 dx gcd in + if BigN.eq_bool d BigN.one then Qz (BigZ.mul zy nx) + else Qq (BigZ.mul zy nx) d + | Qq nx dx, Qq ny dy => norm (BigZ.mul nx ny) (BigN.mul dx dy) + end. + + Theorem wf_mul_norm: forall x y, wf x -> wf y -> wf (mul_norm x y). + intros [zx | nx dx] [zy | ny dy]; unfold mul_norm; auto. + intros HH1 HH2. + match goal with |- context[BigN.eq_bool ?X ?Y] => + generalize (BigN.spec_eq_bool X Y); case BigN.eq_bool + end; auto; + match goal with |- context[BigZ.eq_bool ?X ?Y] => + generalize (BigZ.spec_eq_bool X Y); case BigZ.eq_bool + end; 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_1; rewrite BigZ.spec_0. + intros H1 H2; unfold wf. + 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. + set (a := BigN.to_Z (BigZ.to_N zx)). + set (b := (BigN.to_Z dy)). + assert (F: (0 < Zgcd a b)%Z). + case (Zle_lt_or_eq _ _ (Zgcd_is_pos a b)); auto. + intros HH3; case H2; rewrite spec_to_N; fold a. + rewrite (Zgcd_inv_0_l _ _ (sym_equal HH3)); try ring. + rewrite BigN.spec_div; rewrite BigN.spec_gcd; fold a; fold b; auto. + intros H. + generalize HH2; simpl wf. + 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 HH; case HH; fold b. + rewrite (Zdivide_Zdiv_eq (Zgcd a b) b); auto. + rewrite H; auto with zarith. + assert (F1:= Zgcd_is_gcd a b); inversion F1; 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_1; rewrite BigN.spec_gcd. + intros HH1 H1 H2. + match goal with |- context[BigZ.eq_bool ?X ?Y] => + generalize (BigZ.spec_eq_bool X Y); case BigZ.eq_bool + end; auto. + rewrite BigN.spec_1; rewrite BigN.spec_gcd. + intros HH1 H1 H2. + 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 HH2. + match goal with |- context[BigN.eq_bool ?X ?Y] => + generalize (BigN.spec_eq_bool X Y); case BigN.eq_bool + end; auto. + set (a := BigN.to_Z (BigZ.to_N zy)). + set (b := (BigN.to_Z dx)). + assert (F: (0 < Zgcd a b)%Z). + case (Zle_lt_or_eq _ _ (Zgcd_is_pos a b)); auto. + intros HH3; case HH2; rewrite spec_to_N; fold a. + rewrite (Zgcd_inv_0_l _ _ (sym_equal HH3)); try ring. + rewrite BigN.spec_div; rewrite BigN.spec_gcd; fold a; fold b; auto. + intros H; unfold wf. + 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; fold a; fold b; auto. + intros HH; generalize H1; simpl wf. + 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 HH3; case HH3; fold b. + rewrite (Zdivide_Zdiv_eq (Zgcd a b) b); auto. + rewrite HH; auto with zarith. + assert (F1:= Zgcd_is_gcd a b); inversion F1; auto. + intros HH1 HH2; apply wf_norm. + rewrite BigN.spec_mul; intros HH3. + case (Zmult_integral _ _ HH3). + generalize HH1; simpl. + match goal with |- context[BigN.eq_bool ?X ?Y] => + generalize (BigN.spec_eq_bool X Y); case BigN.eq_bool + end; auto. + generalize HH2; simpl. + match goal with |- context[BigN.eq_bool ?X ?Y] => + generalize (BigN.spec_eq_bool X Y); case BigN.eq_bool + end; auto. + Qed. + + Theorem spec_mul_norm x y: wf x -> wf y -> + ([mul_norm x y] == [x] * [y])%Q. + intros x y Hx Hy; rewrite <- spec_mul; auto. + unfold mul_norm, mul; generalize Hx Hy; case x; case y; clear Hx Hy. + intros; apply Qeq_refl. + intros p1 n p2 Hx Hy. + 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 n)%Z). + generalize Hy; simpl. + match goal with |- context[BigN.eq_bool ?X ?Y] => + generalize (BigN.spec_eq_bool X Y); case BigN.eq_bool + end; auto. + intros _ HH; case HH. + rewrite BigN.spec_0; generalize (BigN.spec_pos n); auto with zarith. + set (a := BigN.to_Z (BigZ.to_N p2)). + set (b := BigN.to_Z n). + assert (F2: (0 < Zgcd a b )%Z). + case (Zle_lt_or_eq _ _ (Zgcd_is_pos a b)); intros H3; auto. + generalize F; fold a; 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; try rewrite BigN.spec_gcd; + fold a b; 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; fold a b; intros H2. + red; simpl. + repeat rewrite BigZ.spec_mul. + rewrite BigZ.spec_div; simpl; rewrite BigN.spec_gcd; + fold a b; auto with zarith. + rewrite Z2P_correct; auto with zarith. + rewrite spec_to_N; fold a; fold b. + 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. + repeat rewrite BigZ.spec_mul. + rewrite BigZ.spec_div; simpl; rewrite BigN.spec_gcd; + fold a b; auto with zarith. + rewrite BigN.spec_div; simpl; rewrite BigN.spec_gcd; + fold a b; auto with zarith. + intros H2; red; simpl. + repeat rewrite BigZ.spec_mul. + rewrite Z2P_correct; auto with zarith. + rewrite (spec_to_N p2); fold a b. + rewrite Z2P_correct; 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. + case (Zle_lt_or_eq _ _ + (BigN.spec_pos (n / + BigN.gcd (BigZ.to_N p2) + n))%bigN); + rewrite BigN.spec_div; simpl; rewrite BigN.spec_gcd; + fold a b; auto with zarith. + intros H3. + apply False_ind; generalize F1. + generalize Hy; 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; auto with zarith. + intros HH; case HH; fold b. + rewrite (Zdivide_Zdiv_eq (Zgcd a b) b); auto. + rewrite <- H3; ring. + assert (FF:= Zgcd_is_gcd a b); inversion FF; auto. + intros p1 p2 n Hx Hy. + 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. + set (a := BigN.to_Z (BigZ.to_N p1)). + set (b := BigN.to_Z n). + 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. + assert (F1: (0 < b)%Z). + generalize Hx; unfold wf. + 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; auto with zarith. + generalize (BigN.spec_pos n); fold b; auto with zarith. + assert (F2: (0 < Zgcd a b)%Z). + case (Zle_lt_or_eq _ _ (Zgcd_is_pos a b)); 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; rewrite BigN.spec_gcd; fold a b; 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. + fold a b; intros H2. + red; simpl. + repeat rewrite BigZ.spec_mul. + rewrite BigZ.spec_div; simpl; rewrite BigN.spec_gcd; + fold a b; auto with zarith. + rewrite Z2P_correct; auto with zarith. + rewrite spec_to_N; fold a b. + 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; + fold a b; auto with zarith. + rewrite Z2P_correct; auto with zarith. + rewrite (spec_to_N p1); fold a b. + case (Zle_lt_or_eq _ _ + (BigN.spec_pos (n / BigN.gcd (BigZ.to_N p1) n))%bigN); intros F3. + rewrite Z2P_correct; auto with zarith. + rewrite BigN.spec_div; simpl; rewrite BigN.spec_gcd; + fold a b; 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. + apply False_ind; generalize F1. + rewrite (Zdivide_Zdiv_eq (Zgcd a b) b); auto. + generalize F3; rewrite BigN.spec_div; rewrite BigN.spec_gcd; fold a b; + auto with zarith. + intros HH; rewrite <- HH; auto with zarith. + assert (FF:= Zgcd_is_gcd a b); inversion FF; auto. + intros p1 n1 p2 n2 Hn1 Hn2. + match goal with |- [norm ?X ?Y] == _ => + apply Qeq_trans with ([Qq X Y]); + [apply spec_norm | idtac] + end; try apply Qeq_refl. + rewrite BigN.spec_mul. + apply Zmult_lt_0_compat. + generalize Hn1; 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; auto with zarith. + generalize (BigN.spec_pos n1) (BigN.spec_pos n2); auto with zarith. + generalize Hn2; 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; auto with zarith. + generalize (BigN.spec_pos n1) (BigN.spec_pos n2); auto with zarith. + Qed. + + Theorem spec_mul_normc x y: wf x -> wf y -> + [[mul_norm x y]] = [[x]] * [[y]]. + intros x y Hx Hy; 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. + + 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 n + | Qz (BigZ.Neg n) => + if BigN.eq_bool n BigN.zero then zero else Qq BigZ.minus_one n + | Qq (BigZ.Pos n) d => + if BigN.eq_bool n BigN.zero then zero else Qq (BigZ.Pos d) n + | Qq (BigZ.Neg n) d => + if BigN.eq_bool n BigN.zero then zero else Qq (BigZ.Neg d) n + end. + + + Theorem wf_inv: forall x, wf x -> wf (inv x). + intros [ zx | nx dx]; unfold inv, wf; auto. + case zx; clear zx. + intros nx. + 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_mul. + intros nx. + 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_mul. + 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 _ HH; case HH. + intros H1 _. + case nx; clear nx. + intros nx. + repeat match goal with |- context[BigN.eq_bool ?X ?Y] => + generalize (BigN.spec_eq_bool X Y); case BigN.eq_bool + end; simpl; auto. + intros nx. + repeat match goal with |- context[BigN.eq_bool ?X ?Y] => + generalize (BigN.spec_eq_bool X Y); case BigN.eq_bool + end; simpl; auto. + Qed. + + Theorem spec_inv x: wf 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. + 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. + generalize F; case BigN.to_Z; simpl; auto with zarith. + intros p Hp; discriminate Hp. + simpl wf. + 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. + intros HH; case HH. + intros _. + 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 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. + simpl wf. + 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. + intros HH; case HH. + intros _. + 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 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 (Zopp (Zpos Y)); + 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: wf x -> + [[inv x]] = /[[x]]. + intros x Hx; 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. + + + Definition div x y := mul x (inv y). + + Theorem wf_div x y: wf x -> wf y -> wf (div x y). + intros x y Hx Hy; unfold div; apply wf_mul; auto. + apply wf_inv; auto. + Qed. + + Theorem spec_div x y: wf x -> wf y -> + ([div x y] == [x] / [y])%Q. + intros x y Hx Hy; unfold div; rewrite spec_mul; auto. + apply wf_inv; auto. + unfold Qdiv; apply Qmult_comp. + apply Qeq_refl. + apply spec_inv; auto. + Qed. + + Theorem spec_divc x y: wf x -> wf y -> + [[div x y]] = [[x]] / [[y]]. + intros x y Hx Hy; unfold div; rewrite spec_mulc; auto. + unfold Qcdiv; apply f_equal2 with (f := Qcmult); auto. + apply spec_invc; auto. + apply wf_inv; auto. + Qed. + + Definition div_norm x y := mul_norm x (inv y). + + Theorem wf_div_norm x y: wf x -> wf y -> wf (div_norm x y). + intros x y Hx Hy; unfold div_norm; apply wf_mul_norm; auto. + apply wf_inv; auto. + Qed. + + Theorem spec_div_norm x y: wf x -> wf y -> + ([div_norm x y] == [x] / [y])%Q. + intros x y Hx Hy; unfold div_norm; rewrite spec_mul_norm; auto. + apply wf_inv; auto. + unfold Qdiv; apply Qmult_comp. + apply Qeq_refl. + apply spec_inv; auto. + Qed. + + Theorem spec_div_normc x y: wf x -> wf y -> + [[div_norm x y]] = [[x]] / [[y]]. + intros x y Hx Hy; unfold div_norm; rewrite spec_mul_normc; auto. + unfold Qcdiv; apply f_equal2 with (f := Qcmult); auto. + apply spec_invc; auto. + apply wf_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 wf_square: forall x, wf x -> wf (square x). + intros [ zx | nx dx]; unfold square, wf; auto. + 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 H2; case H2. + case (Zmult_integral _ _ H1); auto. + Qed. + + Theorem spec_square x: wf x -> ([square x] == [x] ^ 2)%Q. + intros [ x | nx dx]; unfold square. + intros _. + red; simpl; rewrite BigZ.spec_square; auto with zarith. + unfold wf. + 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 _ HH; case HH. + intros H1 _. + red; simpl; rewrite BigZ.spec_square; auto with zarith. + assert (F: (0 < BigN.to_Z dx)%Z). + case (Zle_lt_or_eq _ _ (BigN.spec_pos dx)); auto with zarith. + assert (F1 : (0 < BigN.to_Z (BigN.square dx))%Z). + rewrite BigN.spec_square; apply Zmult_lt_0_compat; + auto with zarith. + rewrite Zpos_mult_morphism. + repeat rewrite Z2P_correct; auto with zarith. + rewrite BigN.spec_square; auto with zarith. + Qed. + + Theorem spec_squarec x: wf x -> [[square x]] = [[x]]^2. + intros x Hx; 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. + + + 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 wf_power_pos: forall x p, wf x -> wf (power_pos x p). + intros [ zx | nx dx] p; unfold power_pos, wf; auto. + 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_power_pos; simpl. + intros H1 H2 _. + case (Zle_lt_or_eq _ _ (BigN.spec_pos dx)); auto with zarith. + intros H3; generalize (Zpower_pos_pos _ p H3); auto with zarith. + Qed. + + Theorem spec_power_pos x p: wf x -> ([power_pos x p] == [x] ^ Zpos p)%Q. + Proof. + intros [x | nx dx] p; unfold power_pos. + intros _; 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. + unfold wf. + 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 _ HH; case HH. + intros H1 _. + 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. + rewrite Z2P_correct; rewrite BigN.spec_power_pos; auto. + 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. + + Theorem spec_power_posc x p: wf x -> + [[power_pos x p]] = [[x]] ^ nat_of_P p. + intros x p Hx; 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; generalize Hx; case x; simpl; clear x Hx 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. + intros _ HH; case HH. + 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 Qv. + diff --git a/theories/Ints/num/ZMake.v b/theories/Ints/num/ZMake.v index 7fe5b1088e..0a2b5cd3fd 100644 --- a/theories/Ints/num/ZMake.v +++ b/theories/Ints/num/ZMake.v @@ -113,6 +113,14 @@ Module Make (N:NType). | Neg nx => Zopp (N.to_Z nx) end. + Theorem spec_of_Z: forall x, to_Z (of_Z x) = x. + intros x; case x; unfold to_Z, of_Z, zero. + exact N.spec_0. + intros; rewrite N.spec_of_N; auto. + intros; rewrite N.spec_of_N; auto. + Qed. + + Theorem spec_0: to_Z zero = 0. exact N.spec_0. Qed. @@ -186,6 +194,22 @@ Module Make (N:NType). if N.eq_bool nx N.zero then Eq else Lt | _, _ => Eq end. + + Theorem spec_cmp_sign: forall x y, + match cmp_sign x y with + | Gt => 0 <= to_Z x /\ to_Z y < 0 + | Lt => to_Z x < 0 /\ 0 <= to_Z y + | Eq => True + end. + Proof. + intros [x | x] [y | y]; unfold cmp_sign; auto. + generalize (N.spec_eq_bool y N.zero); case N.eq_bool; auto. + rewrite N.spec_0; unfold to_Z. + generalize (N.spec_pos x) (N.spec_pos y); auto with zarith. + generalize (N.spec_eq_bool x N.zero); case N.eq_bool; auto. + rewrite N.spec_0; unfold to_Z. + generalize (N.spec_pos x) (N.spec_pos y); auto with zarith. + Qed. Definition to_N x := match x with |
