diff options
Diffstat (limited to 'theories/Numbers')
| -rw-r--r-- | theories/Numbers/Rational/BigQ/BigQ.v | 5 | ||||
| -rw-r--r-- | theories/Numbers/Rational/BigQ/Q0Make.v | 413 | ||||
| -rw-r--r-- | theories/Numbers/Rational/SpecViaQ/QSig.v | 84 |
3 files changed, 321 insertions, 181 deletions
diff --git a/theories/Numbers/Rational/BigQ/BigQ.v b/theories/Numbers/Rational/BigQ/BigQ.v index c7c7735c0..8323d7884 100644 --- a/theories/Numbers/Rational/BigQ/BigQ.v +++ b/theories/Numbers/Rational/BigQ/BigQ.v @@ -19,9 +19,10 @@ 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. +Module BigQ <: QSig.QType := Q0. + +Notation bigQ := BigQ.t. Delimit Scope bigQ_scope with bigQ. Bind Scope bigQ_scope with bigQ. diff --git a/theories/Numbers/Rational/BigQ/Q0Make.v b/theories/Numbers/Rational/BigQ/Q0Make.v index d84efab23..ba49f59e6 100644 --- a/theories/Numbers/Rational/BigQ/Q0Make.v +++ b/theories/Numbers/Rational/BigQ/Q0Make.v @@ -20,24 +20,23 @@ Require Export BigZ. Require Import QArith. Require Import Qcanon. Require Import Qpower. +Require Import QSig. Require Import QMake_base. -Module Q0. +Module Q0 <: QType. Import BinInt Zorder. - Open Local Scope Q_scope. - Open Local Scope Qc_scope. (** The notation of a rational number is either an integer x, - interpreted as itself or a pair (x,y) of an integer x and a naturel + interpreted as itself or a pair (x,y) of an integer x and a natural number y interpreted as x/y. The pairs (x,0) and (0,y) are all interpreted as 0. *) Definition t := q_type. - Definition zero: t := Qz BigZ.zero. - Definition one: t := Qz BigZ.one. - Definition minus_one: t := Qz BigZ.minus_one. + (** Specification with respect to [QArith] *) + + Open Local Scope Q_scope. Definition of_Z x: t := Qz (BigZ.of_Z x). @@ -46,22 +45,17 @@ Module Q0. 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 + |Qq x y => if BigN.eq_bool y BigN.zero then 0 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. + Theorem strong_spec_of_Q: forall q: Q, [of_Q q] = q. + Proof. intros (x,y); simpl. match goal with |- context[BigN.eq_bool ?X ?Y] => generalize (BigN.spec_eq_bool X Y); case BigN.eq_bool @@ -71,10 +65,30 @@ Module Q0. 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. + Theorem spec_of_Q: forall q: Q, [of_Q q] == q. + Proof. + intros; rewrite strong_spec_of_Q; red; auto. + Qed. + + Definition eq x y := [x] == [y]. + + Definition zero: t := Qz BigZ.zero. + Definition one: t := Qz BigZ.one. + Definition minus_one: t := Qz BigZ.minus_one. + + Lemma spec_0: [zero] == 0. + Proof. + reflexivity. + Qed. + + Lemma spec_1: [one] == 1. + Proof. + reflexivity. + Qed. + + Lemma spec_m1: [minus_one] == -(1). + Proof. + reflexivity. Qed. Definition opp (x: t): t := @@ -83,7 +97,8 @@ Module Q0. | Qq nx dx => Qq (BigZ.opp nx) dx end. - Theorem spec_opp: forall q, ([opp q] = -[q])%Q. + Theorem strong_spec_opp: forall q, [opp q] = -[q]. + Proof. intros [z | x y]; simpl. rewrite BigZ.spec_opp; auto. match goal with |- context[BigN.eq_bool ?X ?Y] => @@ -92,12 +107,9 @@ Module Q0. 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. + Theorem spec_opp : forall q, [opp q] == -[q]. + Proof. + intros; rewrite strong_spec_opp; red; auto. Qed. Definition compare (x y: t) := @@ -118,8 +130,8 @@ Module Q0. end end. - Theorem spec_compare: forall q1 q2, - compare q1 q2 = ([q1] ?= [q2])%Q. + Theorem spec_compare: forall q1 q2, (compare q1 q2) = ([q1] ?= [q2]). + Proof. intros [z1 | x1 y1] [z2 | x2 y2]; unfold Qcompare, compare, to_Q, Qnum, Qden. repeat rewrite Zmult_1_r. @@ -172,12 +184,10 @@ Module Q0. 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. + Definition lt n m := compare n m = Lt. + Definition le n m := compare n m <> Gt. + Definition min n m := match compare n m with Gt => m | _ => n end. + Definition max n m := match compare n m with Lt => m | _ => n end. (* Je pense que cette fonction normalise bien ... *) Definition norm n d: t := @@ -195,10 +205,8 @@ Module Q0. | Gt => zero (* gcd = 0 => both numbers are 0 *) end. - - - Theorem spec_norm: forall n q, - ([norm n q] == [Qq n q])%Q. + Theorem spec_norm: forall n q, [norm n q] == [Qq n q]. + Proof. intros p q; unfold norm. assert (Hp := BigN.spec_pos (BigZ.to_N p)). match goal with |- context[BigN.compare ?X ?Y] => @@ -302,8 +310,8 @@ Module Q0. end end. - Theorem spec_add x y: - ([add x y] == [x] + [y])%Q. + Theorem spec_add : forall x y, [add x y] == [x] + [y]. + Proof. intros [x | nx dx] [y | ny dy]; unfold Qplus; simpl. rewrite BigZ.spec_add; repeat rewrite Zmult_1_r; auto. intros; apply Qeq_refl; auto. @@ -370,19 +378,6 @@ Module Q0. 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 => @@ -404,10 +399,9 @@ Module Q0. norm n d end end. - - Theorem spec_add_norm x y: - ([add_norm x y] == [x] + [y])%Q. + Theorem spec_add_norm : forall x y, [add_norm x y] == [x] + [y]. + Proof. intros x y; rewrite <- spec_add; auto. case x; case y; clear x y; unfold add_norm, add. intros; apply Qeq_refl. @@ -447,47 +441,22 @@ Module Q0. 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. + Theorem spec_sub : forall x y, [sub x y] == [x] - [y]. + Proof. intros x y; unfold sub; rewrite spec_add; auto. rewrite spec_opp; ring. Qed. - 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. + Theorem spec_sub_norm : forall x y, [sub_norm x y] == [x] - [y]. + Proof. intros x y; unfold sub_norm; rewrite spec_add_norm; auto. rewrite spec_opp; ring. Qed. - 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) @@ -496,8 +465,8 @@ Module Q0. | 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. + Theorem spec_mul : forall x y, [mul x y] == [x] * [y]. + Proof. intros [x | nx dx] [y | ny dy]; unfold Qmult; simpl. rewrite BigZ.spec_mul; repeat rewrite Zmult_1_r; auto. intros; apply Qeq_refl; auto. @@ -545,19 +514,6 @@ Module Q0. 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) @@ -603,8 +559,8 @@ Definition mul_norm (x y: t): t := else Qq (BigZ.mul ny nx) d end. - Theorem spec_mul_norm x y: - ([mul_norm x y] == [x] * [y])%Q. + Theorem spec_mul_norm : forall x y, [mul_norm x y] == [x] * [y]. + Proof. intros x y; rewrite <- spec_mul; auto. unfold mul_norm, mul; case x; case y; clear x y. intros; apply Qeq_refl. @@ -872,20 +828,6 @@ Definition mul_norm (x y: t): t := 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 @@ -895,8 +837,8 @@ Definition inv (x: t): t := | Qq (BigZ.Neg n) d => Qq (BigZ.Neg d) n end. - Theorem spec_inv x: - ([inv x] == /[x])%Q. + Theorem spec_inv : forall x, [inv x] == /[x]. + Proof. intros [ [x | x] | [nx | nx] dx]; unfold inv, Qinv; simpl. match goal with |- context[BigN.eq_bool ?X ?Y] => generalize (BigN.spec_eq_bool X Y); case BigN.eq_bool @@ -960,20 +902,6 @@ Definition inv (x: t): t := 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) => @@ -1000,7 +928,8 @@ Definition inv_norm (x: t): t := end end. - Theorem spec_inv_norm x: ([inv_norm x] == /[x])%Q. + Theorem spec_inv_norm : forall x, [inv_norm x] == /[x]. + Proof. intros [ [x | x] | [nx | nx] dx]; unfold inv_norm, Qinv. match goal with |- context[BigN.compare ?X ?Y] => generalize (BigN.spec_compare X Y); case BigN.compare @@ -1147,57 +1076,34 @@ Definition inv_norm (x: t): t := 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. + Theorem spec_div x y: [div x y] == [x] / [y]. + Proof. intros x y; unfold div; rewrite spec_mul; auto. unfold Qdiv; apply Qmult_comp. apply Qeq_refl. apply spec_inv; auto. Qed. - 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. + Theorem spec_div_norm x y: [div_norm x y] == [x] / [y]. + Proof. intros x y; unfold div_norm; rewrite spec_mul_norm; auto. unfold Qdiv; apply Qmult_comp. apply Qeq_refl. apply spec_inv; auto. Qed. - 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. + Theorem spec_square : forall x, [square x] == [x] ^ 2. + Proof. intros [ x | nx dx]; unfold square. red; simpl; rewrite BigZ.spec_square; auto with zarith. simpl Qpower. @@ -1227,29 +1133,13 @@ Definition inv_norm (x: t): t := 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. + Theorem spec_power_pos : forall x p, [power_pos x p] == [x] ^ Zpos p. Proof. intros [x | nx dx] p; unfold power_pos. unfold power_pos; red; simpl. @@ -1303,8 +1193,172 @@ Definition inv_norm (x: t): t := rewrite BigZ.spec_power_pos; simpl; ring. Qed. + (** Interaction with [Qcanon.Qc] *) + + Open Scope Qc_scope. + + Definition of_Qc q := of_Q (this q). + + Definition to_Qc q := !!(to_Q q). + + Notation "[[ x ]]" := (to_Qc x). + + Theorem spec_of_Qc: forall q, [[of_Qc q]] = q. + Proof. + intros (x, Hx); unfold of_Qc, to_Qc; simpl. + apply Qc_decomp; simpl. + intros. + rewrite <- H0 at 2; apply Qred_complete. + apply spec_of_Q. + Qed. + + Theorem spec_oppc: forall q, [[opp q]] = -[[q]]. + Proof. + intros q; unfold Qcopp, to_Qc, Q2Qc. + apply Qc_decomp; intros _ _; unfold this. + apply Qred_complete. + rewrite spec_opp. + rewrite <- Qred_opp. + rewrite Qred_correct; red; auto. + Qed. + + Theorem spec_comparec: forall q1 q2, + compare q1 q2 = ([[q1]] ?= [[q2]]). + Proof. + unfold Qccompare, to_Qc. + intros q1 q2; rewrite spec_compare; simpl; auto. + apply Qcompare_comp; apply Qeq_sym; apply Qred_correct. + Qed. + + Theorem spec_addc x y: + [[add x y]] = [[x]] + [[y]]. + Proof. + intros x y; unfold to_Qc. + apply trans_equal with (!! ([x] + [y])). + unfold Q2Qc. + apply Qc_decomp; intros _ _; unfold this. + apply Qred_complete; apply spec_add; auto. + unfold Qcplus, Q2Qc. + apply Qc_decomp; intros _ _; unfold this. + apply Qred_complete. + apply Qplus_comp; apply Qeq_sym; apply Qred_correct. + Qed. + + Theorem spec_add_normc x y: + [[add_norm x y]] = [[x]] + [[y]]. + Proof. + intros x y; unfold to_Qc. + apply trans_equal with (!! ([x] + [y])). + unfold Q2Qc. + apply Qc_decomp; intros _ _; unfold this. + apply Qred_complete; apply spec_add_norm; auto. + unfold Qcplus, Q2Qc. + apply Qc_decomp; intros _ _; unfold this. + apply Qred_complete. + apply Qplus_comp; apply Qeq_sym; apply Qred_correct. + Qed. + + Theorem spec_subc x y: [[sub x y]] = [[x]] - [[y]]. + Proof. + intros x y; unfold sub; rewrite spec_addc; auto. + rewrite spec_oppc; ring. + Qed. + + Theorem spec_sub_normc x y: + [[sub_norm x y]] = [[x]] - [[y]]. + intros x y; unfold sub_norm; rewrite spec_add_normc; auto. + rewrite spec_oppc; ring. + Qed. + + Theorem spec_mulc x y: + [[mul x y]] = [[x]] * [[y]]. + Proof. + intros x y; unfold to_Qc. + apply trans_equal with (!! ([x] * [y])). + unfold Q2Qc. + apply Qc_decomp; intros _ _; unfold this. + apply Qred_complete; apply spec_mul; auto. + unfold Qcmult, Q2Qc. + apply Qc_decomp; intros _ _; unfold this. + apply Qred_complete. + apply Qmult_comp; apply Qeq_sym; apply Qred_correct. + Qed. + + Theorem spec_mul_normc x y: + [[mul_norm x y]] = [[x]] * [[y]]. + Proof. + intros x y; unfold to_Qc. + apply trans_equal with (!! ([x] * [y])). + unfold Q2Qc. + apply Qc_decomp; intros _ _; unfold this. + apply Qred_complete; apply spec_mul_norm; auto. + unfold Qcmult, Q2Qc. + apply Qc_decomp; intros _ _; unfold this. + apply Qred_complete. + apply Qmult_comp; apply Qeq_sym; apply Qred_correct. + Qed. + + Theorem spec_invc x: + [[inv x]] = /[[x]]. + Proof. + intros x; unfold to_Qc. + apply trans_equal with (!! (/[x])). + unfold Q2Qc. + apply Qc_decomp; intros _ _; unfold this. + apply Qred_complete; apply spec_inv; auto. + unfold Qcinv, Q2Qc. + apply Qc_decomp; intros _ _; unfold this. + apply Qred_complete. + apply Qinv_comp; apply Qeq_sym; apply Qred_correct. + Qed. + + Theorem spec_inv_normc x: + [[inv_norm x]] = /[[x]]. + Proof. + intros x; unfold to_Qc. + apply trans_equal with (!! (/[x])). + unfold Q2Qc. + apply Qc_decomp; intros _ _; unfold this. + apply Qred_complete; apply spec_inv_norm; auto. + unfold Qcinv, Q2Qc. + apply Qc_decomp; intros _ _; unfold this. + apply Qred_complete. + apply Qinv_comp; apply Qeq_sym; apply Qred_correct. + Qed. + + Theorem spec_divc x y: [[div x y]] = [[x]] / [[y]]. + Proof. + intros x y; unfold div; rewrite spec_mulc; auto. + unfold Qcdiv; apply f_equal2 with (f := Qcmult); auto. + apply spec_invc; auto. + Qed. + + Theorem spec_div_normc x y: [[div_norm x y]] = [[x]] / [[y]]. + Proof. + intros x y; unfold div_norm; rewrite spec_mul_normc; auto. + unfold Qcdiv; apply f_equal2 with (f := Qcmult); auto. + apply spec_invc; auto. + Qed. + + Theorem spec_squarec x: [[square x]] = [[x]]^2. + Proof. + intros x; unfold to_Qc. + apply trans_equal with (!! ([x]^2)). + unfold Q2Qc. + apply Qc_decomp; intros _ _; unfold this. + apply Qred_complete; apply spec_square; auto. + simpl Qcpower. + replace (!! [x] * 1) with (!![x]); try ring. + simpl. + unfold Qcmult, Q2Qc. + apply Qc_decomp; intros _ _; unfold this. + apply Qred_complete. + apply Qmult_comp; apply Qeq_sym; apply Qred_correct. + Qed. + Theorem spec_power_posc x p: [[power_pos x p]] = [[x]] ^ nat_of_P p. + Proof. intros x p; unfold to_Qc. apply trans_equal with (!! ([x]^Zpos p)). unfold Q2Qc. @@ -1354,4 +1408,5 @@ Definition inv_norm (x: t): t := apply Qmult_comp; apply Qeq_sym; apply Qred_correct. Qed. + End Q0. diff --git a/theories/Numbers/Rational/SpecViaQ/QSig.v b/theories/Numbers/Rational/SpecViaQ/QSig.v new file mode 100644 index 000000000..6840eae25 --- /dev/null +++ b/theories/Numbers/Rational/SpecViaQ/QSig.v @@ -0,0 +1,84 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id$ i*) + +Require Import QArith Qpower. + +Open Scope Q_scope. + +(** * QSig *) + +(** Interface of a rich structure about rational numbers. + Specifications are written via translation to Q. +*) + +Module Type QType. + + Parameter t : Type. + + Parameter to_Q : t -> Q. + Notation "[ x ]" := (to_Q x). + + Definition eq x y := [x] == [y]. + + Parameter of_Q : Q -> t. + Parameter spec_of_Q: forall x, to_Q (of_Q x) == x. + + Parameter zero : t. + Parameter one : t. + Parameter minus_one : t. + + Parameter spec_0: [zero] == 0. + Parameter spec_1: [one] == 1. + Parameter spec_m1: [minus_one] == -(1). + + Parameter compare : t -> t -> comparison. + + Parameter spec_compare: forall x y, compare x y = ([x] ?= [y]). + + Definition lt n m := compare n m = Lt. + Definition le n m := compare n m <> Gt. + Definition min n m := match compare n m with Gt => m | _ => n end. + Definition max n m := match compare n m with Lt => m | _ => n end. + + Parameter add : t -> t -> t. + + Parameter spec_add: forall x y, [add x y] == [x] + [y]. + + Parameter sub : t -> t -> t. + + Parameter spec_sub: forall x y, [sub x y] == [x] - [y]. + + Parameter opp : t -> t. + + Parameter spec_opp: forall x, [opp x] == - [x]. + + Parameter mul : t -> t -> t. + + Parameter spec_mul: forall x y, [mul x y] == [x] * [y]. + + Parameter square : t -> t. + + Parameter spec_square: forall x, [square x] == [x] ^ 2. + + Parameter inv : t -> t. + + Parameter spec_inv : forall x, [inv x] == / [x]. + + Parameter div : t -> t -> t. + + Parameter spec_div: forall x y, [div x y] == [x] / [y]. + + Parameter power_pos : t -> positive -> t. + + Parameter spec_power_pos: forall x n, [power_pos x n] == [x] ^ Zpos n. + +End QType. + +(* TODO: add norm function and variants, add eq_bool, what about Qc ? *)
\ No newline at end of file |