diff options
Diffstat (limited to 'theories/Numbers/Rational/BigQ/BigQ.v')
-rw-r--r-- | theories/Numbers/Rational/BigQ/BigQ.v | 162 |
1 files changed, 0 insertions, 162 deletions
diff --git a/theories/Numbers/Rational/BigQ/BigQ.v b/theories/Numbers/Rational/BigQ/BigQ.v deleted file mode 100644 index 850afe53..00000000 --- a/theories/Numbers/Rational/BigQ/BigQ.v +++ /dev/null @@ -1,162 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(** * BigQ: an efficient implementation of rational numbers *) - -(** Initial authors: Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) - -Require Export BigZ. -Require Import Field Qfield QSig QMake Orders GenericMinMax. - -(** We choose for BigQ an implemention with - multiple representation of 0: 0, 1/0, 2/0 etc. - See [QMake.v] *) - -(** First, we provide translations functions between [BigN] and [BigZ] *) - -Module BigN_BigZ <: NType_ZType BigN.BigN BigZ. - Definition Z_of_N := BigZ.Pos. - Lemma spec_Z_of_N : forall n, BigZ.to_Z (Z_of_N n) = BigN.to_Z n. - Proof. - reflexivity. - Qed. - Definition Zabs_N := BigZ.to_N. - Lemma spec_Zabs_N : forall z, BigN.to_Z (Zabs_N z) = Z.abs (BigZ.to_Z z). - Proof. - unfold Zabs_N; intros. - rewrite BigZ.spec_to_Z, Z.mul_comm; apply Z.sgn_abs. - Qed. -End BigN_BigZ. - -(** This allows building [BigQ] out of [BigN] and [BigQ] via [QMake] *) - -Delimit Scope bigQ_scope with bigQ. - -Module BigQ <: QType <: OrderedTypeFull <: TotalOrder. - Include QMake.Make BigN BigZ BigN_BigZ - <+ !QProperties <+ HasEqBool2Dec - <+ !MinMaxLogicalProperties <+ !MinMaxDecProperties. - Ltac order := Private_Tac.order. -End BigQ. - -(** Notations about [BigQ] *) - -Local Open Scope bigQ_scope. - -Notation bigQ := BigQ.t. -Bind Scope bigQ_scope with bigQ BigQ.t BigQ.t_. -(** As in QArith, we use [#] to denote fractions *) -Notation "p # q" := (BigQ.Qq p q) (at level 55, no associativity) : bigQ_scope. -Local Notation "0" := BigQ.zero : bigQ_scope. -Local Notation "1" := BigQ.one : bigQ_scope. -Infix "+" := BigQ.add : bigQ_scope. -Infix "-" := BigQ.sub : bigQ_scope. -Notation "- x" := (BigQ.opp x) : bigQ_scope. -Infix "*" := BigQ.mul : bigQ_scope. -Infix "/" := BigQ.div : bigQ_scope. -Infix "^" := BigQ.power : bigQ_scope. -Infix "?=" := BigQ.compare : bigQ_scope. -Infix "==" := BigQ.eq : bigQ_scope. -Notation "x != y" := (~x==y) (at level 70, no associativity) : bigQ_scope. -Infix "<" := BigQ.lt : bigQ_scope. -Infix "<=" := BigQ.le : bigQ_scope. -Notation "x > y" := (BigQ.lt y x) (only parsing) : bigQ_scope. -Notation "x >= y" := (BigQ.le y x) (only parsing) : bigQ_scope. -Notation "x < y < z" := (x<y /\ y<z) : bigQ_scope. -Notation "x < y <= z" := (x<y /\ y<=z) : bigQ_scope. -Notation "x <= y < z" := (x<=y /\ y<z) : bigQ_scope. -Notation "x <= y <= z" := (x<=y /\ y<=z) : bigQ_scope. -Notation "[ q ]" := (BigQ.to_Q q) : bigQ_scope. - -(** [BigQ] is a field *) - -Lemma BigQfieldth : - field_theory 0 1 BigQ.add BigQ.mul BigQ.sub BigQ.opp - BigQ.div BigQ.inv BigQ.eq. -Proof. -constructor. -constructor. -exact BigQ.add_0_l. exact BigQ.add_comm. exact BigQ.add_assoc. -exact BigQ.mul_1_l. exact BigQ.mul_comm. exact BigQ.mul_assoc. -exact BigQ.mul_add_distr_r. exact BigQ.sub_add_opp. -exact BigQ.add_opp_diag_r. exact BigQ.neq_1_0. -exact BigQ.div_mul_inv. exact BigQ.mul_inv_diag_l. -Qed. - -Declare Equivalent Keys pow_N pow_pos. - -Lemma BigQpowerth : - power_theory 1 BigQ.mul BigQ.eq Z.of_N BigQ.power. -Proof. -constructor. intros. BigQ.qify. -replace ([r] ^ Z.of_N n)%Q with (pow_N 1 Qmult [r] n)%Q by (now destruct n). -destruct n. reflexivity. -induction p; simpl; auto; rewrite ?BigQ.spec_mul, ?IHp; reflexivity. -Qed. - -Ltac isBigQcst t := - match t with - | BigQ.Qz ?t => isBigZcst t - | BigQ.Qq ?n ?d => match isBigZcst n with - | true => isBigNcst d - | false => constr:(false) - end - | BigQ.zero => constr:(true) - | BigQ.one => constr:(true) - | BigQ.minus_one => constr:(true) - | _ => constr:(false) - end. - -Ltac BigQcst t := - match isBigQcst t with - | true => constr:(t) - | false => constr:(NotConstant) - end. - -Add Field BigQfield : BigQfieldth - (decidable BigQ.eqb_correct, - completeness BigQ.eqb_complete, - constants [BigQcst], - power_tac BigQpowerth [Qpow_tac]). - -Section TestField. - -Let ex1 : forall x y z, (x+y)*z == (x*z)+(y*z). - intros. - ring. -Qed. - -Let ex8 : forall x, x ^ 2 == x*x. - intro. - ring. -Qed. - -Let ex10 : forall x y, y!=0 -> (x/y)*y == x. -intros. -field. -auto. -Qed. - -End TestField. - -(** [BigQ] can also benefit from an "order" tactic *) - -Ltac bigQ_order := BigQ.order. - -Section TestOrder. -Let test : forall x y : bigQ, x<=y -> y<=x -> x==y. -Proof. bigQ_order. Qed. -End TestOrder. - -(** We can also reason by switching to QArith thanks to tactic - BigQ.qify. *) - -Section TestQify. -Let test : forall x : bigQ, 0+x == 1*x. -Proof. intro x. BigQ.qify. ring. Qed. -End TestQify. |