summaryrefslogtreecommitdiff
path: root/theories/Numbers/Rational
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:46:51 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:46:51 +0200
commit5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch)
tree631ad791a7685edafeb1fb2e8faeedc8379318ae /theories/Numbers/Rational
parentda178a880e3ace820b41d38b191d3785b82991f5 (diff)
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'theories/Numbers/Rational')
-rw-r--r--theories/Numbers/Rational/BigQ/BigQ.v207
-rw-r--r--theories/Numbers/Rational/BigQ/QMake.v721
-rw-r--r--theories/Numbers/Rational/SpecViaQ/QSig.v202
3 files changed, 597 insertions, 533 deletions
diff --git a/theories/Numbers/Rational/BigQ/BigQ.v b/theories/Numbers/Rational/BigQ/BigQ.v
index f01cbbc5..0bc71166 100644
--- a/theories/Numbers/Rational/BigQ/BigQ.v
+++ b/theories/Numbers/Rational/BigQ/BigQ.v
@@ -5,12 +5,13 @@
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *)
-(************************************************************************)
-(*i $Id: BigQ.v 12509 2009-11-12 15:52:50Z letouzey $ i*)
+(** * BigQ: an efficient implementation of rational numbers *)
+
+(** Initial authors: Benjamin Gregoire, Laurent Thery, INRIA, 2007 *)
-Require Import Field Qfield BigN BigZ QSig QMake.
+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.
@@ -34,7 +35,9 @@ End BigN_BigZ.
(** This allows to build [BigQ] out of [BigN] and [BigQ] via [QMake] *)
-Module BigQ <: QSig.QType := QMake.Make BigN BigZ BigN_BigZ.
+Module BigQ <: QType <: OrderedTypeFull <: TotalOrder :=
+ QMake.Make BigN BigZ BigN_BigZ <+ !QProperties <+ HasEqBool2Dec
+ <+ !MinMaxLogicalProperties <+ !MinMaxDecProperties.
(** Notations about [BigQ] *)
@@ -43,12 +46,40 @@ Notation bigQ := BigQ.t.
Delimit Scope bigQ_scope with bigQ.
Bind Scope bigQ_scope with bigQ.
Bind Scope bigQ_scope with BigQ.t.
-
-(* Allow nice printing of rational numerals, either as (Qz 1234)
- or as (Qq 1234 5678) *)
+Bind Scope bigQ_scope with BigQ.t_.
+(* Bind Scope has no retroactive effect, let's declare scopes by hand. *)
Arguments Scope BigQ.Qz [bigZ_scope].
-Arguments Scope BigQ.Qq [bigZ_scope bigN_scope].
-
+Arguments Scope BigQ.Qq [bigZ_scope bigN_scope].
+Arguments Scope BigQ.to_Q [bigQ_scope].
+Arguments Scope BigQ.red [bigQ_scope].
+Arguments Scope BigQ.opp [bigQ_scope].
+Arguments Scope BigQ.inv [bigQ_scope].
+Arguments Scope BigQ.square [bigQ_scope].
+Arguments Scope BigQ.add [bigQ_scope bigQ_scope].
+Arguments Scope BigQ.sub [bigQ_scope bigQ_scope].
+Arguments Scope BigQ.mul [bigQ_scope bigQ_scope].
+Arguments Scope BigQ.div [bigQ_scope bigQ_scope].
+Arguments Scope BigQ.eq [bigQ_scope bigQ_scope].
+Arguments Scope BigQ.lt [bigQ_scope bigQ_scope].
+Arguments Scope BigQ.le [bigQ_scope bigQ_scope].
+Arguments Scope BigQ.eq [bigQ_scope bigQ_scope].
+Arguments Scope BigQ.compare [bigQ_scope bigQ_scope].
+Arguments Scope BigQ.min [bigQ_scope bigQ_scope].
+Arguments Scope BigQ.max [bigQ_scope bigQ_scope].
+Arguments Scope BigQ.eq_bool [bigQ_scope bigQ_scope].
+Arguments Scope BigQ.power_pos [bigQ_scope positive_scope].
+Arguments Scope BigQ.power [bigQ_scope Z_scope].
+Arguments Scope BigQ.inv_norm [bigQ_scope].
+Arguments Scope BigQ.add_norm [bigQ_scope bigQ_scope].
+Arguments Scope BigQ.sub_norm [bigQ_scope bigQ_scope].
+Arguments Scope BigQ.mul_norm [bigQ_scope bigQ_scope].
+Arguments Scope BigQ.div_norm [bigQ_scope bigQ_scope].
+Arguments Scope BigQ.power_norm [bigQ_scope bigQ_scope].
+
+(** 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.
@@ -57,142 +88,102 @@ 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)%bigQ (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 : bigQ_scope.
+Notation "x < y <= z" := (x<y /\ y<=z)%bigQ : bigQ_scope.
+Notation "x <= y < z" := (x<=y /\ y<z)%bigQ : bigQ_scope.
+Notation "x <= y <= z" := (x<=y /\ y<=z)%bigQ : bigQ_scope.
Notation "[ q ]" := (BigQ.to_Q q) : bigQ_scope.
-Open Scope bigQ_scope.
-
-(** [BigQ] is a setoid *)
-
-Add Relation BigQ.t BigQ.eq
- reflexivity proved by (fun x => Qeq_refl [x])
- symmetry proved by (fun x y => Qeq_sym [x] [y])
- transitivity proved by (fun x y z => Qeq_trans [x] [y] [z])
-as BigQeq_rel.
-
-Add Morphism BigQ.add with signature BigQ.eq ==> BigQ.eq ==> BigQ.eq as BigQadd_wd.
-Proof.
- unfold BigQ.eq; intros; rewrite !BigQ.spec_add; rewrite H, H0; apply Qeq_refl.
-Qed.
-
-Add Morphism BigQ.opp with signature BigQ.eq ==> BigQ.eq as BigQopp_wd.
-Proof.
- unfold BigQ.eq; intros; rewrite !BigQ.spec_opp; rewrite H; apply Qeq_refl.
-Qed.
-
-Add Morphism BigQ.sub with signature BigQ.eq ==> BigQ.eq ==> BigQ.eq as BigQsub_wd.
-Proof.
- unfold BigQ.eq; intros; rewrite !BigQ.spec_sub; rewrite H, H0; apply Qeq_refl.
-Qed.
-
-Add Morphism BigQ.mul with signature BigQ.eq ==> BigQ.eq ==> BigQ.eq as BigQmul_wd.
-Proof.
- unfold BigQ.eq; intros; rewrite !BigQ.spec_mul; rewrite H, H0; apply Qeq_refl.
-Qed.
-
-Add Morphism BigQ.inv with signature BigQ.eq ==> BigQ.eq as BigQinv_wd.
-Proof.
- unfold BigQ.eq; intros; rewrite !BigQ.spec_inv; rewrite H; apply Qeq_refl.
-Qed.
-
-Add Morphism BigQ.div with signature BigQ.eq ==> BigQ.eq ==> BigQ.eq as BigQdiv_wd.
-Proof.
- unfold BigQ.eq; intros; rewrite !BigQ.spec_div; rewrite H, H0; apply Qeq_refl.
-Qed.
-
-(* TODO : fix this. For the moment it's useless (horribly slow)
-Hint Rewrite
- BigQ.spec_0 BigQ.spec_1 BigQ.spec_m1 BigQ.spec_compare
- BigQ.spec_red BigQ.spec_add BigQ.spec_sub BigQ.spec_opp
- BigQ.spec_mul BigQ.spec_inv BigQ.spec_div BigQ.spec_power_pos
- BigQ.spec_square : bigq. *)
-
+Local Open Scope bigQ_scope.
(** [BigQ] is a field *)
Lemma BigQfieldth :
- field_theory BigQ.zero BigQ.one BigQ.add BigQ.mul BigQ.sub BigQ.opp BigQ.div BigQ.inv BigQ.eq.
+ field_theory 0 1 BigQ.add BigQ.mul BigQ.sub BigQ.opp
+ BigQ.div BigQ.inv BigQ.eq.
Proof.
constructor.
-constructor; intros; red.
-rewrite BigQ.spec_add, BigQ.spec_0; ring.
-rewrite ! BigQ.spec_add; ring.
-rewrite ! BigQ.spec_add; ring.
-rewrite BigQ.spec_mul, BigQ.spec_1; ring.
-rewrite ! BigQ.spec_mul; ring.
-rewrite ! BigQ.spec_mul; ring.
-rewrite BigQ.spec_add, ! BigQ.spec_mul, BigQ.spec_add; ring.
-unfold BigQ.sub; apply Qeq_refl.
-rewrite BigQ.spec_add, BigQ.spec_0, BigQ.spec_opp; ring.
-compute; discriminate.
-intros; red.
-unfold BigQ.div; apply Qeq_refl.
-intros; red.
-rewrite BigQ.spec_mul, BigQ.spec_inv, BigQ.spec_1; field.
-rewrite <- BigQ.spec_0; auto.
-Qed.
-
-Lemma BigQpowerth :
- power_theory BigQ.one BigQ.mul BigQ.eq Z_of_N BigQ.power.
-Proof.
constructor.
-intros; red.
-rewrite BigQ.spec_power.
-replace ([r] ^ Z_of_N n)%Q with (pow_N 1 Qmult [r] n)%Q.
-destruct n.
-simpl; compute; auto.
-induction p; simpl; auto; try rewrite !BigQ.spec_mul, !IHp; apply Qeq_refl.
-destruct n; reflexivity.
-Qed.
-
-Lemma BigQ_eq_bool_correct :
- forall x y, BigQ.eq_bool x y = true -> x==y.
-Proof.
-intros; generalize (BigQ.spec_eq_bool x y); rewrite H; auto.
+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.
-Lemma BigQ_eq_bool_complete :
- forall x y, x==y -> BigQ.eq_bool x y = true.
+Lemma BigQpowerth :
+ power_theory 1 BigQ.mul BigQ.eq Z_of_N BigQ.power.
Proof.
-intros; generalize (BigQ.spec_eq_bool x y).
-destruct BigQ.eq_bool; auto.
+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.
-(* TODO : improve later the detection of constants ... *)
+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 t with
- | BigQ.zero => BigQ.zero
- | BigQ.one => BigQ.one
- | BigQ.minus_one => BigQ.minus_one
- | _ => NotConstant
+ match isBigQcst t with
+ | true => constr:t
+ | false => constr:NotConstant
end.
Add Field BigQfield : BigQfieldth
- (decidable BigQ_eq_bool_correct,
- completeness BigQ_eq_bool_complete,
+ (decidable BigQ.eqb_correct,
+ completeness BigQ.eqb_complete,
constants [BigQcst],
power_tac BigQpowerth [Qpow_tac]).
-Section Examples.
+Section TestField.
Let ex1 : forall x y z, (x+y)*z == (x*z)+(y*z).
intros.
ring.
Qed.
-Let ex8 : forall x, x ^ 1 == x.
+Let ex8 : forall x, x ^ 2 == x*x.
intro.
ring.
Qed.
-Let ex10 : forall x y, ~(y==BigQ.zero) -> (x/y)*y == x.
+Let ex10 : forall x y, y!=0 -> (x/y)*y == x.
intros.
field.
auto.
Qed.
-End Examples. \ No newline at end of file
+End TestField.
+
+(** [BigQ] can also benefit from an "order" tactic *)
+
+Module BigQ_Order := !OrdersTac.MakeOrderTac BigQ.
+Ltac bigQ_order := BigQ_Order.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.
diff --git a/theories/Numbers/Rational/BigQ/QMake.v b/theories/Numbers/Rational/BigQ/QMake.v
index 494420bd..407f7b90 100644
--- a/theories/Numbers/Rational/BigQ/QMake.v
+++ b/theories/Numbers/Rational/BigQ/QMake.v
@@ -5,15 +5,20 @@
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *)
-(************************************************************************)
-(*i $Id: QMake.v 11208 2008-07-04 16:57:46Z letouzey $ i*)
+(** * QMake : a generic efficient implementation of rational numbers *)
+
+(** Initial authors : Benjamin Gregoire, Laurent Thery, INRIA, 2007 *)
Require Import BigNumPrelude ROmega.
-Require Import QArith Qcanon Qpower.
+Require Import QArith Qcanon Qpower Qminmax.
Require Import NSig ZSig QSig.
+(** We will build rationals out of an implementation of integers [ZType]
+ for numerators and an implementation of natural numbers [NType] for
+ denominators. But first we will need some glue between [NType] and
+ [ZType]. *)
+
Module Type NType_ZType (N:NType)(Z:ZType).
Parameter Z_of_N : N.t -> Z.t.
Parameter spec_Z_of_N : forall n, Z.to_Z (Z_of_N n) = N.to_Z n.
@@ -28,27 +33,27 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
number y interpreted as x/y. The pairs (x,0) and (0,y) are all
interpreted as 0. *)
- Inductive t_ :=
+ Inductive t_ :=
| Qz : Z.t -> t_
| Qq : Z.t -> N.t -> t_.
Definition t := t_.
- (** Specification with respect to [QArith] *)
+ (** Specification with respect to [QArith] *)
- Open Local Scope Q_scope.
+ Local Open Scope Q_scope.
Definition of_Z x: t := Qz (Z.of_Z x).
- Definition of_Q (q:Q) : t :=
- let (x,y) := q in
- match y with
+ Definition of_Q (q:Q) : t :=
+ let (x,y) := q in
+ match y with
| 1%positive => Qz (Z.of_Z x)
| _ => Qq (Z.of_Z x) (N.of_N (Npos y))
end.
- Definition to_Q (q: t) :=
- match q with
+ Definition to_Q (q: t) :=
+ match q with
| Qz x => Z.to_Z x # 1
| Qq x y => if N.eq_bool y N.zero then 0
else Z.to_Z x # Z2P (N.to_Z y)
@@ -56,17 +61,56 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
Notation "[ x ]" := (to_Q x).
+ Lemma N_to_Z_pos :
+ forall x, (N.to_Z x <> N.to_Z N.zero)%Z -> (0 < N.to_Z x)%Z.
+ Proof.
+ intros x; rewrite N.spec_0; generalize (N.spec_pos x). romega.
+ Qed.
+(*
+ Lemma if_fun_commut : forall A B (f:A->B)(b:bool) a a',
+ f (if b then a else a') = if b then f a else f a'.
+ Proof. now destruct b. Qed.
+
+ Lemma if_fun_commut' : forall A B C D (f:A->B)(b:{C}+{D}) a a',
+ f (if b then a else a') = if b then f a else f a'.
+ Proof. now destruct b. Qed.
+*)
+ Ltac destr_eqb :=
+ match goal with
+ | |- context [Z.eq_bool ?x ?y] =>
+ rewrite (Z.spec_eq_bool x y);
+ generalize (Zeq_bool_if (Z.to_Z x) (Z.to_Z y));
+ case (Zeq_bool (Z.to_Z x) (Z.to_Z y));
+ destr_eqb
+ | |- context [N.eq_bool ?x ?y] =>
+ rewrite (N.spec_eq_bool x y);
+ generalize (Zeq_bool_if (N.to_Z x) (N.to_Z y));
+ case (Zeq_bool (N.to_Z x) (N.to_Z y));
+ [ | let H:=fresh "H" in
+ try (intro H;generalize (N_to_Z_pos _ H); clear H)];
+ destr_eqb
+ | _ => idtac
+ end.
+
+ Hint Rewrite
+ Zplus_0_r Zplus_0_l Zmult_0_r Zmult_0_l Zmult_1_r Zmult_1_l
+ Z.spec_0 N.spec_0 Z.spec_1 N.spec_1 Z.spec_m1 Z.spec_opp
+ Z.spec_compare N.spec_compare
+ Z.spec_add N.spec_add Z.spec_mul N.spec_mul Z.spec_div N.spec_div
+ Z.spec_gcd N.spec_gcd Zgcd_Zabs Zgcd_1
+ spec_Z_of_N spec_Zabs_N
+ : nz.
+ Ltac nzsimpl := autorewrite with nz in *.
+
+ Ltac qsimpl := try red; unfold to_Q; simpl; intros;
+ destr_eqb; simpl; nzsimpl; intros;
+ rewrite ?Z2P_correct by auto;
+ auto.
+
Theorem strong_spec_of_Q: forall q: Q, [of_Q q] = q.
Proof.
- intros(x,y); destruct y; simpl; rewrite Z.spec_of_Z; auto.
- generalize (N.spec_eq_bool (N.of_N (Npos y~1)) N.zero);
- case N.eq_bool; auto; rewrite N.spec_0.
- rewrite N.spec_of_N; intros; discriminate.
- rewrite N.spec_of_N; auto.
- generalize (N.spec_eq_bool (N.of_N (Npos y~0)) N.zero);
- case N.eq_bool; auto; rewrite N.spec_0.
- rewrite N.spec_of_N; intros; discriminate.
- rewrite N.spec_of_N; auto.
+ intros(x,y); destruct y; simpl; rewrite ?Z.spec_of_Z; auto;
+ destr_eqb; now rewrite ?N.spec_0, ?N.spec_of_N.
Qed.
Theorem spec_of_Q: forall q: Q, [of_Q q] == q.
@@ -82,131 +126,96 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
Lemma spec_0: [zero] == 0.
Proof.
- simpl; rewrite Z.spec_0; reflexivity.
+ simpl. nzsimpl. reflexivity.
Qed.
Lemma spec_1: [one] == 1.
Proof.
- simpl; rewrite Z.spec_1; reflexivity.
+ simpl. nzsimpl. reflexivity.
Qed.
Lemma spec_m1: [minus_one] == -(1).
Proof.
- simpl; rewrite Z.spec_m1; reflexivity.
+ simpl. nzsimpl. reflexivity.
Qed.
Definition compare (x y: t) :=
match x, y with
| Qz zx, Qz zy => Z.compare zx zy
- | Qz zx, Qq ny dy =>
+ | Qz zx, Qq ny dy =>
if N.eq_bool dy N.zero then Z.compare zx Z.zero
else Z.compare (Z.mul zx (Z_of_N dy)) ny
- | Qq nx dx, Qz zy =>
- if N.eq_bool dx N.zero then Z.compare Z.zero zy
+ | Qq nx dx, Qz zy =>
+ if N.eq_bool dx N.zero then Z.compare Z.zero zy
else Z.compare nx (Z.mul zy (Z_of_N dx))
| Qq nx dx, Qq ny dy =>
match N.eq_bool dx N.zero, N.eq_bool dy N.zero with
| true, true => Eq
| true, false => Z.compare Z.zero ny
| false, true => Z.compare nx Z.zero
- | false, false => Z.compare (Z.mul nx (Z_of_N dy))
+ | false, false => Z.compare (Z.mul nx (Z_of_N dy))
(Z.mul ny (Z_of_N dx))
end
end.
- Lemma Zcompare_spec_alt :
- forall z z', Z.compare z z' = (Z.to_Z z ?= Z.to_Z z')%Z.
+ Theorem spec_compare: forall q1 q2, (compare q1 q2) = ([q1] ?= [q2]).
Proof.
- intros; generalize (Z.spec_compare z z'); destruct Z.compare; auto.
- intro H; rewrite H; symmetry; apply Zcompare_refl.
+ intros [z1 | x1 y1] [z2 | x2 y2];
+ unfold Qcompare, compare; qsimpl.
Qed.
-
- Lemma Ncompare_spec_alt :
- forall n n', N.compare n n' = (N.to_Z n ?= N.to_Z n')%Z.
+
+ Definition lt n m := [n] < [m].
+ Definition le n m := [n] <= [m].
+
+ 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.
+
+ Lemma spec_min : forall n m, [min n m] == Qmin [n] [m].
Proof.
- intros; generalize (N.spec_compare n n'); destruct N.compare; auto.
- intro H; rewrite H; symmetry; apply Zcompare_refl.
+ unfold min, Qmin, GenericMinMax.gmin. intros.
+ rewrite spec_compare; destruct Qcompare; auto with qarith.
Qed.
- Lemma N_to_Z2P : forall n, N.to_Z n <> 0%Z ->
- Zpos (Z2P (N.to_Z n)) = N.to_Z n.
+ Lemma spec_max : forall n m, [max n m] == Qmax [n] [m].
Proof.
- intros; apply Z2P_correct.
- generalize (N.spec_pos n); romega.
+ unfold max, Qmax, GenericMinMax.gmax. intros.
+ rewrite spec_compare; destruct Qcompare; auto with qarith.
Qed.
- Hint Rewrite
- Zplus_0_r Zplus_0_l Zmult_0_r Zmult_0_l Zmult_1_r Zmult_1_l
- Z.spec_0 N.spec_0 Z.spec_1 N.spec_1 Z.spec_m1 Z.spec_opp
- Zcompare_spec_alt Ncompare_spec_alt
- Z.spec_add N.spec_add Z.spec_mul N.spec_mul
- Z.spec_gcd N.spec_gcd Zgcd_Zabs
- spec_Z_of_N spec_Zabs_N
- : nz.
- Ltac nzsimpl := autorewrite with nz in *.
-
- Ltac destr_neq_bool := repeat
- (match goal with |- context [N.eq_bool ?x ?y] =>
- generalize (N.spec_eq_bool x y); case N.eq_bool
- end).
-
- Ltac destr_zeq_bool := repeat
- (match goal with |- context [Z.eq_bool ?x ?y] =>
- generalize (Z.spec_eq_bool x y); case Z.eq_bool
- end).
-
- Ltac simpl_ndiv := rewrite N.spec_div by (nzsimpl; romega).
- Tactic Notation "simpl_ndiv" "in" "*" :=
- rewrite N.spec_div in * by (nzsimpl; romega).
-
- Ltac simpl_zdiv := rewrite Z.spec_div by (nzsimpl; romega).
- Tactic Notation "simpl_zdiv" "in" "*" :=
- rewrite Z.spec_div in * by (nzsimpl; romega).
-
- Ltac qsimpl := try red; unfold to_Q; simpl; intros;
- destr_neq_bool; destr_zeq_bool; simpl; nzsimpl; auto; intros.
+ Definition eq_bool n m :=
+ match compare n m with Eq => true | _ => false end.
- Theorem spec_compare: forall q1 q2, (compare q1 q2) = ([q1] ?= [q2]).
+ Theorem spec_eq_bool: forall x y, eq_bool x y = Qeq_bool [x] [y].
Proof.
- intros [z1 | x1 y1] [z2 | x2 y2];
- unfold Qcompare, compare; qsimpl; rewrite ! N_to_Z2P; auto.
+ intros. unfold eq_bool. rewrite spec_compare. reflexivity.
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.
+ (** [check_int] : is a reduced fraction [n/d] in fact a integer ? *)
- Definition eq_bool n m :=
- match compare n m with Eq => true | _ => false end.
+ Definition check_int n d :=
+ match N.compare N.one d with
+ | Lt => Qq n d
+ | Eq => Qz n
+ | Gt => zero (* n/0 encodes 0 *)
+ end.
- Theorem spec_eq_bool: forall x y,
- if eq_bool x y then [x] == [y] else ~([x] == [y]).
+ Theorem strong_spec_check_int : forall n d, [check_int n d] = [Qq n d].
Proof.
- intros.
- unfold eq_bool.
- rewrite spec_compare.
- generalize (Qeq_alt [x] [y]).
- destruct Qcompare.
- intros H; rewrite H; auto.
- intros H H'; rewrite H in H'; discriminate.
- intros H H'; rewrite H in H'; discriminate.
+ intros; unfold check_int.
+ nzsimpl.
+ destr_zcompare.
+ simpl. rewrite <- H; qsimpl. congruence.
+ reflexivity.
+ qsimpl. exfalso; romega.
Qed.
(** Normalisation function *)
Definition norm n d : t :=
- let gcd := N.gcd (Zabs_N n) d in
+ let gcd := N.gcd (Zabs_N n) d in
match N.compare N.one gcd with
- | Lt =>
- let n := Z.div n (Z_of_N gcd) in
- let d := N.div d gcd in
- match N.compare d N.one with
- | Gt => Qq n d
- | Eq => Qz n
- | Lt => zero
- end
- | Eq => Qq n d
+ | Lt => check_int (Z.div n (Z_of_N gcd)) (N.div d gcd)
+ | Eq => check_int n d
| Gt => zero (* gcd = 0 => both numbers are 0 *)
end.
@@ -217,29 +226,16 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
assert (Hq := N.spec_pos q).
nzsimpl.
destr_zcompare.
+ (* Eq *)
+ rewrite strong_spec_check_int; reflexivity.
+ (* Lt *)
+ rewrite strong_spec_check_int.
qsimpl.
-
- simpl_ndiv.
- destr_zcompare.
- qsimpl.
- rewrite H1 in *; rewrite Zdiv_0_l in H0; discriminate.
- rewrite N_to_Z2P; auto.
- simpl_zdiv; nzsimpl.
- rewrite Zgcd_div_swap0, H0; romega.
-
- qsimpl.
- assert (0 < N.to_Z q / Zgcd (Z.to_Z p) (N.to_Z q))%Z.
- apply Zgcd_div_pos; romega.
- romega.
-
- qsimpl.
- simpl_ndiv in *; nzsimpl; romega.
- simpl_ndiv in *.
- rewrite H1, Zdiv_0_l in H2; elim H2; auto.
- rewrite 2 N_to_Z2P; auto.
- simpl_ndiv; simpl_zdiv; nzsimpl.
+ generalize (Zgcd_div_pos (Z.to_Z p) (N.to_Z q)). romega.
+ replace (N.to_Z q) with 0%Z in * by assumption.
+ rewrite Zdiv_0_l in *; auto with zarith.
apply Zgcd_div_swap0; romega.
-
+ (* Gt *)
qsimpl.
assert (H' : Zgcd (Z.to_Z p) (N.to_Z q) = 0%Z).
generalize (Zgcd_is_pos (Z.to_Z p) (N.to_Z q)); romega.
@@ -249,48 +245,37 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
Theorem strong_spec_norm : forall p q, [norm p q] = Qred [Qq p q].
Proof.
intros.
- replace (Qred [Qq p q]) with (Qred [norm p q]) by
+ replace (Qred [Qq p q]) with (Qred [norm p q]) by
(apply Qred_complete; apply spec_norm).
symmetry; apply Qred_identity.
unfold norm.
assert (Hp := N.spec_pos (Zabs_N p)).
assert (Hq := N.spec_pos q).
nzsimpl.
- destr_zcompare.
+ destr_zcompare; rewrite ?strong_spec_check_int.
(* Eq *)
- simpl.
- destr_neq_bool; nzsimpl; simpl; auto.
- intros.
- rewrite N_to_Z2P; auto.
- (* Lt *)
- simpl_ndiv.
- destr_zcompare.
- qsimpl; auto.
qsimpl.
+ (* Lt *)
qsimpl.
- simpl_zdiv; nzsimpl.
- rewrite N_to_Z2P; auto.
- clear H1.
- simpl_ndiv; nzsimpl.
rewrite Zgcd_1_rel_prime.
destruct (Z_lt_le_dec 0 (N.to_Z q)).
apply Zis_gcd_rel_prime; auto with zarith.
apply Zgcd_is_gcd.
replace (N.to_Z q) with 0%Z in * by romega.
- rewrite Zdiv_0_l in H0; discriminate.
+ rewrite Zdiv_0_l in *; romega.
(* Gt *)
- simpl; auto.
+ simpl; auto with zarith.
Qed.
- (** Reduction function : producing irreducible fractions *)
+ (** Reduction function : producing irreducible fractions *)
- Definition red (x : t) : t :=
- match x with
+ Definition red (x : t) : t :=
+ match x with
| Qz z => x
| Qq n d => norm n d
end.
- Definition Reduced x := [red x] = [x].
+ Class Reduced x := is_reduced : [red x] = [x].
Theorem spec_red : forall x, [red x] == [x].
Proof.
@@ -304,21 +289,21 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
Proof.
intros [ z | n d ].
unfold red.
- symmetry; apply Qred_identity; simpl; auto.
+ symmetry; apply Qred_identity; simpl; auto with zarith.
unfold red; apply strong_spec_norm.
Qed.
-
+
Definition add (x y: t): t :=
match x with
| Qz zx =>
match y with
| Qz zy => Qz (Z.add zx zy)
- | Qq ny dy =>
- if N.eq_bool dy N.zero then x
+ | Qq ny dy =>
+ if N.eq_bool dy N.zero then x
else Qq (Z.add (Z.mul zx (Z_of_N dy)) ny) dy
end
| Qq nx dx =>
- if N.eq_bool dx N.zero then y
+ if N.eq_bool dx N.zero then y
else match y with
| Qz zy => Qq (Z.add nx (Z.mul zy (Z_of_N dx))) dx
| Qq ny dy =>
@@ -332,19 +317,12 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
Theorem spec_add : forall x y, [add x y] == [x] + [y].
Proof.
- intros [x | nx dx] [y | ny dy]; unfold Qplus; qsimpl.
- intuition.
- rewrite N_to_Z2P; auto.
- intuition.
- rewrite Pmult_1_r, N_to_Z2P; auto.
- intuition.
- rewrite Pmult_1_r, N_to_Z2P; auto.
- destruct (Zmult_integral _ _ H); intuition.
- rewrite Zpos_mult_morphism, 2 N_to_Z2P; auto.
- rewrite (Z2P_correct (N.to_Z dx * N.to_Z dy)); auto.
- apply Zmult_lt_0_compat.
- generalize (N.spec_pos dx); romega.
- generalize (N.spec_pos dy); romega.
+ intros [x | nx dx] [y | ny dy]; unfold Qplus; qsimpl;
+ auto with zarith.
+ rewrite Pmult_1_r, Z2P_correct; auto.
+ rewrite Pmult_1_r, Z2P_correct; auto.
+ destruct (Zmult_integral (N.to_Z dx) (N.to_Z dy)); intuition.
+ rewrite Zpos_mult_morphism, 2 Z2P_correct; auto.
Qed.
Definition add_norm (x y: t): t :=
@@ -352,12 +330,12 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
| Qz zx =>
match y with
| Qz zy => Qz (Z.add zx zy)
- | Qq ny dy =>
- if N.eq_bool dy N.zero then x
+ | Qq ny dy =>
+ if N.eq_bool dy N.zero then x
else norm (Z.add (Z.mul zx (Z_of_N dy)) ny) dy
end
| Qq nx dx =>
- if N.eq_bool dx N.zero then y
+ if N.eq_bool dx N.zero then y
else match y with
| Qz zy => norm (Z.add nx (Z.mul zy (Z_of_N dx))) dx
| Qq ny dy =>
@@ -372,26 +350,20 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
Theorem spec_add_norm : forall x y, [add_norm x y] == [x] + [y].
Proof.
intros x y; rewrite <- spec_add.
- destruct x; destruct y; unfold add_norm, add;
- destr_neq_bool; auto using Qeq_refl, spec_norm.
+ destruct x; destruct y; unfold add_norm, add;
+ destr_eqb; auto using Qeq_refl, spec_norm.
Qed.
- Theorem strong_spec_add_norm : forall x y : t,
- Reduced x -> Reduced y -> Reduced (add_norm x y).
+ Instance strong_spec_add_norm x y
+ `(Reduced x, Reduced y) : Reduced (add_norm x y).
Proof.
unfold Reduced; intros.
rewrite strong_spec_red.
- rewrite <- (Qred_complete [add x y]);
+ rewrite <- (Qred_complete [add x y]);
[ | rewrite spec_add, spec_add_norm; apply Qeq_refl ].
rewrite <- strong_spec_red.
- destruct x as [zx|nx dx]; destruct y as [zy|ny dy].
- simpl in *; auto.
- simpl; intros.
- destr_neq_bool; nzsimpl; simpl; auto.
- simpl; intros.
- destr_neq_bool; nzsimpl; simpl; auto.
- simpl; intros.
- destr_neq_bool; nzsimpl; simpl; auto.
+ destruct x as [zx|nx dx]; destruct y as [zy|ny dy];
+ simpl; destr_eqb; nzsimpl; simpl; auto.
Qed.
Definition opp (x: t): t :=
@@ -404,7 +376,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
Proof.
intros [z | x y]; simpl.
rewrite Z.spec_opp; auto.
- match goal with |- context[N.eq_bool ?X ?Y] =>
+ match goal with |- context[N.eq_bool ?X ?Y] =>
generalize (N.spec_eq_bool X Y); case N.eq_bool
end; auto; rewrite N.spec_0.
rewrite Z.spec_opp; auto.
@@ -415,7 +387,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
intros; rewrite strong_spec_opp; red; auto.
Qed.
- Theorem strong_spec_opp_norm : forall q, Reduced q -> Reduced (opp q).
+ Instance strong_spec_opp_norm q `(Reduced q) : Reduced (opp q).
Proof.
unfold Reduced; intros.
rewrite strong_spec_opp, <- H, !strong_spec_red, <- Qred_opp.
@@ -438,8 +410,8 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
rewrite spec_opp; ring.
Qed.
- Theorem strong_spec_sub_norm : forall x y,
- Reduced x -> Reduced y -> Reduced (sub_norm x y).
+ Instance strong_spec_sub_norm x y
+ `(Reduced x, Reduced y) : Reduced (sub_norm x y).
Proof.
intros.
unfold sub_norm.
@@ -458,35 +430,34 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
Theorem spec_mul : forall x y, [mul x y] == [x] * [y].
Proof.
intros [x | nx dx] [y | ny dy]; unfold Qmult; simpl; qsimpl.
- rewrite Pmult_1_r, N_to_Z2P; auto.
- destruct (Zmult_integral _ _ H1); intuition.
- rewrite H0 in H1; elim H1; auto.
- rewrite H0 in H1; elim H1; auto.
- rewrite H in H1; nzsimpl; elim H1; auto.
- rewrite Zpos_mult_morphism, 2 N_to_Z2P; auto.
- rewrite (Z2P_correct (N.to_Z dx * N.to_Z dy)); auto.
- apply Zmult_lt_0_compat.
- generalize (N.spec_pos dx); omega.
- generalize (N.spec_pos dy); omega.
+ rewrite Pmult_1_r, Z2P_correct; auto.
+ destruct (Zmult_integral (N.to_Z dx) (N.to_Z dy)); intuition.
+ rewrite H0 in H1; auto with zarith.
+ rewrite H0 in H1; auto with zarith.
+ rewrite H in H1; nzsimpl; auto with zarith.
+ rewrite Zpos_mult_morphism, 2 Z2P_correct; auto.
Qed.
- Lemma norm_denum : forall n d,
- [if N.eq_bool d N.one then Qz n else Qq n d] == [Qq n d].
+ Definition norm_denum n d :=
+ if N.eq_bool d N.one then Qz n else Qq n d.
+
+ Lemma spec_norm_denum : forall n d,
+ [norm_denum n d] == [Qq n d].
Proof.
- intros; simpl; qsimpl.
- rewrite H0 in H; discriminate.
- rewrite N_to_Z2P, H0; auto with zarith.
+ unfold norm_denum; intros; simpl; qsimpl.
+ congruence.
+ rewrite H0 in *; auto with zarith.
Qed.
- Definition irred n d :=
+ Definition irred n d :=
let gcd := N.gcd (Zabs_N n) d in
- match N.compare gcd N.one with
+ match N.compare gcd N.one with
| Gt => (Z.div n (Z_of_N gcd), N.div d gcd)
| _ => (n, d)
end.
- Lemma spec_irred : forall n d, exists g,
- let (n',d') := irred n d in
+ Lemma spec_irred : forall n d, exists g,
+ let (n',d') := irred n d in
(Z.to_Z n' * g = Z.to_Z n)%Z /\ (N.to_Z d' * g = N.to_Z d)%Z.
Proof.
intros.
@@ -503,15 +474,15 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
exists (Zgcd (Z.to_Z n) (N.to_Z d)).
simpl.
split.
- simpl_zdiv; nzsimpl.
+ nzsimpl.
destruct (Zgcd_is_gcd (Z.to_Z n) (N.to_Z d)).
rewrite Zmult_comm; symmetry; apply Zdivide_Zdiv_eq; auto with zarith.
- simpl_ndiv; nzsimpl.
+ nzsimpl.
destruct (Zgcd_is_gcd (Z.to_Z n) (N.to_Z d)).
rewrite Zmult_comm; symmetry; apply Zdivide_Zdiv_eq; auto with zarith.
Qed.
- Lemma spec_irred_zero : forall n d,
+ Lemma spec_irred_zero : forall n d,
(N.to_Z d = 0)%Z <-> (N.to_Z (snd (irred n d)) = 0)%Z.
Proof.
intros.
@@ -520,10 +491,10 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
nzsimpl; intros.
destr_zcompare; auto.
simpl.
- simpl_ndiv; nzsimpl.
+ nzsimpl.
rewrite H, Zdiv_0_l; auto.
nzsimpl; destr_zcompare; simpl; auto.
- simpl_ndiv; nzsimpl.
+ nzsimpl.
intros.
generalize (N.spec_pos d); intros.
destruct (N.to_Z d); auto.
@@ -535,8 +506,8 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
compute in H1; elim H1; auto.
Qed.
- Lemma strong_spec_irred : forall n d,
- (N.to_Z d <> 0%Z) ->
+ Lemma strong_spec_irred : forall n d,
+ (N.to_Z d <> 0%Z) ->
let (n',d') := irred n d in Zgcd (Z.to_Z n') (N.to_Z d') = 1%Z.
Proof.
unfold irred; intros.
@@ -546,7 +517,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
apply (Zgcd_inv_0_r (Z.to_Z n)).
generalize (Zgcd_is_pos (Z.to_Z n) (N.to_Z d)); romega.
- simpl_ndiv; simpl_zdiv; nzsimpl.
+ nzsimpl.
rewrite Zgcd_1_rel_prime.
apply Zis_gcd_rel_prime.
generalize (N.spec_pos d); romega.
@@ -554,89 +525,81 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
apply Zgcd_is_gcd; auto.
Qed.
- Definition mul_norm_Qz_Qq z n d :=
- if Z.eq_bool z Z.zero then zero
+ Definition mul_norm_Qz_Qq z n d :=
+ if Z.eq_bool z Z.zero then zero
else
let gcd := N.gcd (Zabs_N z) d in
match N.compare gcd N.one with
- | Gt =>
+ | Gt =>
let z := Z.div z (Z_of_N gcd) in
let d := N.div d gcd in
- if N.eq_bool d N.one then Qz (Z.mul z n) else Qq (Z.mul z n) d
+ norm_denum (Z.mul z n) d
| _ => Qq (Z.mul z n) d
end.
- Definition mul_norm (x y: t): t :=
+ Definition mul_norm (x y: t): t :=
match x, y with
| Qz zx, Qz zy => Qz (Z.mul zx zy)
| Qz zx, Qq ny dy => mul_norm_Qz_Qq zx ny dy
| Qq nx dx, Qz zy => mul_norm_Qz_Qq zy nx dx
- | Qq nx dx, Qq ny dy =>
- let (nx, dy) := irred nx dy in
- let (ny, dx) := irred ny dx in
- let d := N.mul dx dy in
- if N.eq_bool d N.one then Qz (Z.mul ny nx) else Qq (Z.mul ny nx) d
+ | Qq nx dx, Qq ny dy =>
+ let (nx, dy) := irred nx dy in
+ let (ny, dx) := irred ny dx in
+ norm_denum (Z.mul ny nx) (N.mul dx dy)
end.
- Lemma spec_mul_norm_Qz_Qq : forall z n d,
+ Lemma spec_mul_norm_Qz_Qq : forall z n d,
[mul_norm_Qz_Qq z n d] == [Qq (Z.mul z n) d].
Proof.
intros z n d; unfold mul_norm_Qz_Qq; nzsimpl; rewrite Zcompare_gt.
- destr_zeq_bool; intros Hz; nzsimpl.
+ destr_eqb; nzsimpl; intros Hz.
qsimpl; rewrite Hz; auto.
- assert (Hd := N.spec_pos d).
- destruct Z_le_gt_dec.
+ destruct Z_le_gt_dec; intros.
qsimpl.
- rewrite norm_denum.
+ rewrite spec_norm_denum.
qsimpl.
- simpl_ndiv in *; nzsimpl.
- rewrite (Zdiv_gcd_zero _ _ H0 H) in z0; discriminate.
- simpl_ndiv in *; nzsimpl.
- rewrite H, Zdiv_0_l in H0; elim H0; auto.
- rewrite 2 N_to_Z2P; auto.
- simpl_ndiv; simpl_zdiv; nzsimpl.
- rewrite (Zmult_comm (Z.to_Z z)), <- 2 Zmult_assoc.
- rewrite <- Zgcd_div_swap0; auto with zarith; ring.
+ rewrite Zdiv_gcd_zero in z0; auto with zarith.
+ rewrite H in *. rewrite Zdiv_0_l in *; discriminate.
+ rewrite <- Zmult_assoc, (Zmult_comm (Z.to_Z n)), Zmult_assoc.
+ rewrite Zgcd_div_swap0; try romega.
+ ring.
Qed.
- Lemma strong_spec_mul_norm_Qz_Qq : forall z n d,
- Reduced (Qq n d) -> Reduced (mul_norm_Qz_Qq z n d).
+ Instance strong_spec_mul_norm_Qz_Qq z n d :
+ forall `(Reduced (Qq n d)), Reduced (mul_norm_Qz_Qq z n d).
Proof.
- unfold Reduced; intros z n d.
+ unfold Reduced.
rewrite 2 strong_spec_red, 2 Qred_iff.
simpl; nzsimpl.
- destr_neq_bool; intros Hd H; simpl in *; nzsimpl.
-
+ destr_eqb; intros Hd H; simpl in *; nzsimpl.
+
unfold mul_norm_Qz_Qq; nzsimpl; rewrite Zcompare_gt.
- destr_zeq_bool; intros Hz; simpl; nzsimpl; simpl; auto.
+ destr_eqb; intros Hz; simpl; nzsimpl; simpl; auto.
destruct Z_le_gt_dec.
simpl; nzsimpl.
- destr_neq_bool; simpl; nzsimpl; auto.
- intros H'; elim H'; auto.
- destr_neq_bool; simpl; nzsimpl.
- simpl_ndiv; nzsimpl; rewrite Hd, Zdiv_0_l; intros; discriminate.
+ destr_eqb; simpl; nzsimpl; auto with zarith.
+ unfold norm_denum. destr_eqb; simpl; nzsimpl.
+ rewrite Hd, Zdiv_0_l; discriminate.
intros _.
- destr_neq_bool; simpl; nzsimpl; auto.
- simpl_ndiv; nzsimpl; rewrite Hd, Zdiv_0_l; intro H'; elim H'; auto.
+ destr_eqb; simpl; nzsimpl; auto.
+ nzsimpl; rewrite Hd, Zdiv_0_l; auto with zarith.
- rewrite N_to_Z2P in H; auto.
+ rewrite Z2P_correct in H; auto.
unfold mul_norm_Qz_Qq; nzsimpl; rewrite Zcompare_gt.
- destr_zeq_bool; intros Hz; simpl; nzsimpl; simpl; auto.
+ destr_eqb; intros Hz; simpl; nzsimpl; simpl; auto.
destruct Z_le_gt_dec as [H'|H'].
simpl; nzsimpl.
- destr_neq_bool; simpl; nzsimpl; auto.
+ destr_eqb; simpl; nzsimpl; auto.
intros.
- rewrite N_to_Z2P; auto.
+ rewrite Z2P_correct; auto.
apply Zgcd_mult_rel_prime; auto.
generalize (Zgcd_inv_0_l (Z.to_Z z) (N.to_Z d))
(Zgcd_is_pos (Z.to_Z z) (N.to_Z d)); romega.
- destr_neq_bool; simpl; nzsimpl; auto.
- simpl_ndiv; simpl_zdiv; nzsimpl.
- intros.
- destr_neq_bool; simpl; nzsimpl; auto.
- simpl_ndiv in *; nzsimpl.
- intros.
- rewrite Z2P_correct.
+ destr_eqb; simpl; nzsimpl; auto.
+ unfold norm_denum.
+ destr_eqb; nzsimpl; simpl; destr_eqb; simpl; auto.
+ intros; nzsimpl.
+ rewrite Z2P_correct; auto.
apply Zgcd_mult_rel_prime.
rewrite Zgcd_1_rel_prime.
apply Zis_gcd_rel_prime.
@@ -652,9 +615,6 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
rewrite <- Huv; rewrite Hd0 at 2; ring.
rewrite Hd0 at 1.
symmetry; apply Z_div_mult_full; auto with zarith.
- apply Zgcd_div_pos.
- generalize (N.spec_pos d); romega.
- generalize (Zgcd_is_pos (Z.to_Z z) (N.to_Z d)); romega.
Qed.
Theorem spec_mul_norm : forall x y, [mul_norm x y] == [x] * [y].
@@ -670,37 +630,31 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
destruct (spec_irred ny dx) as (g' & Hg').
assert (Hz := spec_irred_zero nx dy).
assert (Hz':= spec_irred_zero ny dx).
- destruct irred as (n1,d1); destruct irred as (n2,d2).
+ destruct irred as (n1,d1); destruct irred as (n2,d2).
simpl snd in *; destruct Hg as [Hg1 Hg2]; destruct Hg' as [Hg1' Hg2'].
- rewrite norm_denum.
+ rewrite spec_norm_denum.
qsimpl.
- elim H; destruct (Zmult_integral _ _ H0) as [Eq|Eq].
- rewrite <- Hz' in Eq; rewrite Eq; simpl; auto.
- rewrite <- Hz in Eq; rewrite Eq; nzsimpl; auto.
+ destruct (Zmult_integral _ _ H0) as [Eq|Eq].
+ rewrite Eq in *; simpl in *.
+ rewrite <- Hg2' in *; auto with zarith.
+ rewrite Eq in *; simpl in *.
+ rewrite <- Hg2 in *; auto with zarith.
- elim H0; destruct (Zmult_integral _ _ H) as [Eq|Eq].
- rewrite Hz' in Eq; rewrite Eq; simpl; auto.
- rewrite Hz in Eq; rewrite Eq; nzsimpl; auto.
+ destruct (Zmult_integral _ _ H) as [Eq|Eq].
+ rewrite Hz' in Eq; rewrite Eq in *; auto with zarith.
+ rewrite Hz in Eq; rewrite Eq in *; auto with zarith.
- rewrite 2 Z2P_correct.
rewrite <- Hg1, <- Hg2, <- Hg1', <- Hg2'; ring.
-
- assert (0 <= N.to_Z d2 * N.to_Z d1)%Z
- by (apply Zmult_le_0_compat; apply N.spec_pos).
- romega.
- assert (0 <= N.to_Z dx * N.to_Z dy)%Z
- by (apply Zmult_le_0_compat; apply N.spec_pos).
- romega.
Qed.
- Theorem strong_spec_mul_norm : forall x y,
- Reduced x -> Reduced y -> Reduced (mul_norm x y).
+ Instance strong_spec_mul_norm x y :
+ forall `(Reduced x, Reduced y), Reduced (mul_norm x y).
Proof.
unfold Reduced; intros.
rewrite strong_spec_red, Qred_iff.
destruct x as [zx|nx dx]; destruct y as [zy|ny dy].
- simpl in *; auto.
+ simpl in *; auto with zarith.
simpl.
rewrite <- Qred_iff, <- strong_spec_red, strong_spec_mul_norm_Qz_Qq; auto.
simpl.
@@ -712,26 +666,27 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
assert (Hz':= spec_irred_zero ny dx).
assert (Hgc := strong_spec_irred nx dy).
assert (Hgc' := strong_spec_irred ny dx).
- destruct irred as (n1,d1); destruct irred as (n2,d2).
+ destruct irred as (n1,d1); destruct irred as (n2,d2).
simpl snd in *; destruct Hg as [Hg1 Hg2]; destruct Hg' as [Hg1' Hg2'].
- destr_neq_bool; simpl; nzsimpl; intros.
- apply Zis_gcd_gcd; auto with zarith; apply Zis_gcd_1.
- destr_neq_bool; simpl; nzsimpl; intros.
- auto.
+
+ unfold norm_denum; qsimpl.
+
+ assert (NEQ : N.to_Z dy <> 0%Z) by
+ (rewrite Hz; intros EQ; rewrite EQ in *; romega).
+ specialize (Hgc NEQ).
+
+ assert (NEQ' : N.to_Z dx <> 0%Z) by
+ (rewrite Hz'; intro EQ; rewrite EQ in *; romega).
+ specialize (Hgc' NEQ').
revert H H0.
rewrite 2 strong_spec_red, 2 Qred_iff; simpl.
- destr_neq_bool; simpl; nzsimpl; intros.
- rewrite Hz in H; rewrite H in H2; nzsimpl; elim H2; auto.
- rewrite Hz' in H0; rewrite H0 in H2; nzsimpl; elim H2; auto.
- rewrite Hz in H; rewrite H in H2; nzsimpl; elim H2; auto.
+ destr_eqb; simpl; nzsimpl; try romega; intros.
+ rewrite Z2P_correct in *; auto.
- rewrite N_to_Z2P in *; auto.
- rewrite Z2P_correct.
+ apply Zgcd_mult_rel_prime; rewrite Zgcd_comm;
+ apply Zgcd_mult_rel_prime; rewrite Zgcd_comm; auto.
- apply Zgcd_mult_rel_prime; rewrite Zgcd_sym;
- apply Zgcd_mult_rel_prime; rewrite Zgcd_sym; auto.
-
rewrite Zgcd_1_rel_prime in *.
apply bezout_rel_prime.
destruct (rel_prime_bezout _ _ H4) as [u v Huv].
@@ -743,21 +698,17 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
destruct (rel_prime_bezout _ _ H3) as [u v Huv].
apply Bezout_intro with (u*g)%Z (v*g')%Z.
rewrite <- Huv, <- Hg2', <- Hg1. ring.
-
- assert (0 <= N.to_Z d2 * N.to_Z d1)%Z.
- apply Zmult_le_0_compat; apply N.spec_pos.
- romega.
Qed.
- Definition inv (x: t): t :=
+ Definition inv (x: t): t :=
match x with
- | Qz z =>
- match Z.compare Z.zero z with
+ | Qz z =>
+ match Z.compare Z.zero z with
| Eq => zero
| Lt => Qq Z.one (Zabs_N z)
| Gt => Qq Z.minus_one (Zabs_N z)
end
- | Qq n d =>
+ | Qq n d =>
match Z.compare Z.zero n with
| Eq => zero
| Lt => Qq (Z_of_N d) (Zabs_N n)
@@ -770,13 +721,13 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
destruct x as [ z | n d ].
(* Qz z *)
simpl.
- rewrite Zcompare_spec_alt; destr_zcompare.
+ rewrite Z.spec_compare; destr_zcompare.
(* 0 = z *)
rewrite <- H.
simpl; nzsimpl; compute; auto.
(* 0 < z *)
simpl.
- destr_neq_bool; nzsimpl; [ intros; rewrite Zabs_eq in *; romega | intros _ ].
+ destr_eqb; nzsimpl; [ intros; rewrite Zabs_eq in *; romega | intros _ ].
set (z':=Z.to_Z z) in *; clearbody z'.
red; simpl.
rewrite Zabs_eq by romega.
@@ -784,7 +735,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
unfold Qinv; simpl; destruct z'; simpl; auto; discriminate.
(* 0 > z *)
simpl.
- destr_neq_bool; nzsimpl; [ intros; rewrite Zabs_non_eq in *; romega | intros _ ].
+ destr_eqb; nzsimpl; [ intros; rewrite Zabs_non_eq in *; romega | intros _ ].
set (z':=Z.to_Z z) in *; clearbody z'.
red; simpl.
rewrite Zabs_non_eq by romega.
@@ -792,14 +743,14 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
unfold Qinv; simpl; destruct z'; simpl; auto; discriminate.
(* Qq n d *)
simpl.
- rewrite Zcompare_spec_alt; destr_zcompare.
+ rewrite Z.spec_compare; destr_zcompare.
(* 0 = n *)
rewrite <- H.
simpl; nzsimpl.
- destr_neq_bool; intros; compute; auto.
+ destr_eqb; intros; compute; auto.
(* 0 < n *)
simpl.
- destr_neq_bool; nzsimpl; intros.
+ destr_eqb; nzsimpl; intros.
intros; rewrite Zabs_eq in *; romega.
intros; rewrite Zabs_eq in *; romega.
clear H1.
@@ -811,10 +762,10 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
red; simpl.
rewrite Z2P_correct by auto.
unfold Qinv; simpl; destruct n'; simpl; auto; try discriminate.
- rewrite Zpos_mult_morphism, N_to_Z2P; auto.
+ rewrite Zpos_mult_morphism, Z2P_correct; auto.
(* 0 > n *)
simpl.
- destr_neq_bool; nzsimpl; intros.
+ destr_eqb; nzsimpl; intros.
intros; rewrite Zabs_non_eq in *; romega.
intros; rewrite Zabs_non_eq in *; romega.
clear H1.
@@ -826,28 +777,28 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
rewrite Z2P_correct by romega.
unfold Qinv; simpl; destruct n'; simpl; auto; try discriminate.
assert (T : forall x, Zneg x = Zopp (Zpos x)) by auto.
- rewrite T, Zpos_mult_morphism, N_to_Z2P; auto; ring.
+ rewrite T, Zpos_mult_morphism, Z2P_correct; auto; ring.
Qed.
- Definition inv_norm (x: t): t :=
+ Definition inv_norm (x: t): t :=
match x with
- | Qz z =>
- match Z.compare Z.zero z with
+ | Qz z =>
+ match Z.compare Z.zero z with
| Eq => zero
| Lt => Qq Z.one (Zabs_N z)
| Gt => Qq Z.minus_one (Zabs_N z)
end
- | Qq n d =>
- if N.eq_bool d N.zero then zero else
- match Z.compare Z.zero n with
+ | Qq n d =>
+ if N.eq_bool d N.zero then zero else
+ match Z.compare Z.zero n with
| Eq => zero
- | Lt =>
- match Z.compare n Z.one with
+ | Lt =>
+ match Z.compare n Z.one with
| Gt => Qq (Z_of_N d) (Zabs_N n)
| _ => Qz (Z_of_N d)
end
- | Gt =>
- match Z.compare n Z.minus_one with
+ | Gt =>
+ match Z.compare n Z.minus_one with
| Lt => Qq (Z.opp (Z_of_N d)) (Zabs_N n)
| _ => Qz (Z.opp (Z_of_N d))
end
@@ -861,74 +812,72 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
destruct x as [ z | n d ].
(* Qz z *)
simpl.
- rewrite Zcompare_spec_alt; destr_zcompare; auto with qarith.
+ rewrite Z.spec_compare; destr_zcompare; auto with qarith.
(* Qq n d *)
- simpl; nzsimpl; destr_neq_bool.
+ simpl; nzsimpl; destr_eqb.
destr_zcompare; simpl; auto with qarith.
- destr_neq_bool; nzsimpl; auto with qarith.
+ destr_eqb; nzsimpl; auto with qarith.
intros _ Hd; rewrite Hd; auto with qarith.
- destr_neq_bool; nzsimpl; auto with qarith.
+ destr_eqb; nzsimpl; auto with qarith.
intros _ Hd; rewrite Hd; auto with qarith.
(* 0 < n *)
destr_zcompare; auto with qarith.
destr_zcompare; nzsimpl; simpl; auto with qarith; intros.
- destr_neq_bool; nzsimpl; [ intros; rewrite Zabs_eq in *; romega | intros _ ].
+ destr_eqb; nzsimpl; [ intros; rewrite Zabs_eq in *; romega | intros _ ].
rewrite H0; auto with qarith.
romega.
(* 0 > n *)
destr_zcompare; nzsimpl; simpl; auto with qarith.
- destr_neq_bool; nzsimpl; [ intros; rewrite Zabs_non_eq in *; romega | intros _ ].
+ destr_eqb; nzsimpl; [ intros; rewrite Zabs_non_eq in *; romega | intros _ ].
rewrite H0; auto with qarith.
romega.
Qed.
- Theorem strong_spec_inv_norm : forall x, Reduced x -> Reduced (inv_norm x).
+ Instance strong_spec_inv_norm x : Reduced x -> Reduced (inv_norm x).
Proof.
- unfold Reduced.
+ unfold Reduced.
intros.
destruct x as [ z | n d ].
(* Qz *)
simpl; nzsimpl.
rewrite strong_spec_red, Qred_iff.
destr_zcompare; simpl; nzsimpl; auto.
- destr_neq_bool; nzsimpl; simpl; auto.
- destr_neq_bool; nzsimpl; simpl; auto.
+ destr_eqb; nzsimpl; simpl; auto.
+ destr_eqb; nzsimpl; simpl; auto.
(* Qq n d *)
rewrite strong_spec_red, Qred_iff in H; revert H.
simpl; nzsimpl.
- destr_neq_bool; nzsimpl; auto with qarith.
+ destr_eqb; nzsimpl; auto with qarith.
destr_zcompare; simpl; nzsimpl; auto; intros.
(* 0 < n *)
destr_zcompare; simpl; nzsimpl; auto.
- destr_neq_bool; nzsimpl; simpl; auto.
+ destr_eqb; nzsimpl; simpl; auto.
rewrite Zabs_eq; romega.
intros _.
rewrite strong_spec_norm; simpl; nzsimpl.
- destr_neq_bool; nzsimpl.
+ destr_eqb; nzsimpl.
rewrite Zabs_eq; romega.
intros _.
rewrite Qred_iff.
simpl.
rewrite Zabs_eq; auto with zarith.
- rewrite N_to_Z2P in *; auto.
- rewrite Z2P_correct; auto with zarith.
- rewrite Zgcd_sym; auto.
+ rewrite Z2P_correct in *; auto.
+ rewrite Zgcd_comm; auto.
(* 0 > n *)
- destr_neq_bool; nzsimpl; simpl; auto; intros.
+ destr_eqb; nzsimpl; simpl; auto; intros.
destr_zcompare; simpl; nzsimpl; auto.
- destr_neq_bool; nzsimpl.
+ destr_eqb; nzsimpl.
rewrite Zabs_non_eq; romega.
intros _.
rewrite strong_spec_norm; simpl; nzsimpl.
- destr_neq_bool; nzsimpl.
+ destr_eqb; nzsimpl.
rewrite Zabs_non_eq; romega.
intros _.
rewrite Qred_iff.
simpl.
- rewrite N_to_Z2P in *; auto.
- rewrite Z2P_correct; auto with zarith.
+ rewrite Z2P_correct in *; auto.
intros.
- rewrite Zgcd_sym, Zgcd_Zabs, Zgcd_sym.
+ rewrite Zgcd_comm, Zgcd_Zabs, Zgcd_comm.
apply Zis_gcd_gcd; auto with zarith.
apply Zis_gcd_minus.
rewrite Zopp_involutive, <- H1; apply Zgcd_is_gcd.
@@ -939,7 +888,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
Theorem spec_div x y: [div x y] == [x] / [y].
Proof.
- intros x y; unfold div; rewrite spec_mul; auto.
+ unfold div; rewrite spec_mul; auto.
unfold Qdiv; apply Qmult_comp.
apply Qeq_refl.
apply spec_inv; auto.
@@ -949,14 +898,14 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
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 div_norm; rewrite spec_mul_norm; auto.
unfold Qdiv; apply Qmult_comp.
apply Qeq_refl.
apply spec_inv_norm; auto.
Qed.
-
- Theorem strong_spec_div_norm : forall x y,
- Reduced x -> Reduced y -> Reduced (div_norm x y).
+
+ Instance strong_spec_div_norm x y
+ `(Reduced x, Reduced y) : Reduced (div_norm x y).
Proof.
intros; unfold div_norm.
apply strong_spec_mul_norm; auto.
@@ -974,15 +923,13 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
destruct x as [ z | n d ].
simpl; rewrite Z.spec_square; red; auto.
simpl.
- destr_neq_bool; nzsimpl; intros.
+ destr_eqb; nzsimpl; intros.
apply Qeq_refl.
rewrite N.spec_square in *; nzsimpl.
- contradict H; elim (Zmult_integral _ _ H0); auto.
+ elim (Zmult_integral _ _ H0); romega.
rewrite N.spec_square in *; nzsimpl.
- rewrite H in H0; simpl in H0; elim H0; auto.
- assert (0 < N.to_Z d)%Z by (generalize (N.spec_pos d); romega).
- clear H H0.
- rewrite Z.spec_square, N.spec_square.
+ rewrite H in H0; romega.
+ rewrite Z.spec_square, N.spec_square.
red; simpl.
rewrite Zpos_mult_morphism; rewrite !Z2P_correct; auto.
apply Zmult_lt_0_compat; auto.
@@ -993,7 +940,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
| Qz zx => Qz (Z.power_pos zx p)
| Qq nx dx => Qq (Z.power_pos nx p) (N.power_pos dx p)
end.
-
+
Theorem spec_power_pos : forall x p, [power_pos x p] == [x] ^ Zpos p.
Proof.
intros [ z | n d ] p; unfold power_pos.
@@ -1006,44 +953,42 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
(* Qq *)
simpl.
rewrite Z.spec_power_pos.
- destr_neq_bool; nzsimpl; intros.
+ destr_eqb; nzsimpl; intros.
apply Qeq_sym; apply Qpower_positive_0.
rewrite N.spec_power_pos in *.
- assert (0 < N.to_Z d ^ ' p)%Z.
- apply Zpower_gt_0; auto with zarith.
- generalize (N.spec_pos d); romega.
+ assert (0 < N.to_Z d ^ ' p)%Z by
+ (apply Zpower_gt_0; auto with zarith).
romega.
rewrite N.spec_power_pos, H in *.
- rewrite Zpower_0_l in H0; [ elim H0; auto | discriminate ].
+ rewrite Zpower_0_l in H0; [romega|discriminate].
rewrite Qpower_decomp.
red; simpl; do 3 f_equal.
rewrite Z2P_correct by (generalize (N.spec_pos d); romega).
rewrite N.spec_power_pos. auto.
Qed.
- Theorem strong_spec_power_pos : forall x p,
- Reduced x -> Reduced (power_pos x p).
+ Instance strong_spec_power_pos x p `(Reduced x) : Reduced (power_pos x p).
Proof.
destruct x as [z | n d]; simpl; intros.
red; simpl; auto.
red; simpl; intros.
rewrite strong_spec_norm; simpl.
- destr_neq_bool; nzsimpl; intros.
+ destr_eqb; nzsimpl; intros.
simpl; auto.
rewrite Qred_iff.
revert H.
unfold Reduced; rewrite strong_spec_red, Qred_iff; simpl.
- destr_neq_bool; nzsimpl; simpl; intros.
+ destr_eqb; nzsimpl; simpl; intros.
rewrite N.spec_power_pos in H0.
- elim H0; rewrite H; rewrite Zpower_0_l; auto; discriminate.
- rewrite N_to_Z2P in *; auto.
+ rewrite H, Zpower_0_l in *; [romega|discriminate].
+ rewrite Z2P_correct in *; auto.
rewrite N.spec_power_pos, Z.spec_power_pos; auto.
rewrite Zgcd_1_rel_prime in *.
apply rel_prime_Zpower; auto with zarith.
Qed.
- Definition power (x : t) (z : Z) : t :=
- match z with
+ Definition power (x : t) (z : Z) : t :=
+ match z with
| Z0 => one
| Zpos p => power_pos x p
| Zneg p => inv (power_pos x p)
@@ -1058,8 +1003,8 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
rewrite spec_inv, spec_power_pos; apply Qeq_refl.
Qed.
- Definition power_norm (x : t) (z : Z) : t :=
- match z with
+ Definition power_norm (x : t) (z : Z) : t :=
+ match z with
| Z0 => one
| Zpos p => power_pos x p
| Zneg p => inv_norm (power_pos x p)
@@ -1074,7 +1019,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
rewrite spec_inv_norm, spec_power_pos; apply Qeq_refl.
Qed.
- Theorem strong_spec_power_norm : forall x z,
+ Instance strong_spec_power_norm x z :
Reduced x -> Reduced (power_norm x z).
Proof.
destruct z; simpl.
@@ -1087,7 +1032,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
(** Interaction with [Qcanon.Qc] *)
-
+
Open Scope Qc_scope.
Definition of_Qc q := of_Q (this q).
@@ -1102,7 +1047,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
unfold of_Qc; rewrite strong_spec_of_Q; auto.
Qed.
- Lemma strong_spec_of_Qc_bis : forall q, Reduced (of_Qc q).
+ Instance strong_spec_of_Qc_bis q : Reduced (of_Qc q).
Proof.
intros; red; rewrite strong_spec_red, strong_spec_of_Qc.
destruct q; simpl; auto.
@@ -1143,7 +1088,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
Theorem spec_addc x y:
[[add x y]] = [[x]] + [[y]].
Proof.
- intros x y; unfold to_Qc.
+ unfold to_Qc.
apply trans_equal with (!! ([x] + [y])).
unfold Q2Qc.
apply Qc_decomp; intros _ _; unfold this.
@@ -1157,7 +1102,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
Theorem spec_add_normc x y:
[[add_norm x y]] = [[x]] + [[y]].
Proof.
- intros x y; unfold to_Qc.
+ unfold to_Qc.
apply trans_equal with (!! ([x] + [y])).
unfold Q2Qc.
apply Qc_decomp; intros _ _; unfold this.
@@ -1168,7 +1113,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
apply Qplus_comp; apply Qeq_sym; apply Qred_correct.
Qed.
- Theorem spec_add_normc_bis : forall x y : Qc,
+ Theorem spec_add_normc_bis : forall x y : Qc,
[add_norm (of_Qc x) (of_Qc y)] = x+y.
Proof.
intros.
@@ -1180,18 +1125,18 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
Theorem spec_subc x y: [[sub x y]] = [[x]] - [[y]].
Proof.
- intros x y; unfold sub; rewrite spec_addc; auto.
+ unfold sub; rewrite spec_addc; auto.
rewrite spec_oppc; ring.
Qed.
Theorem spec_sub_normc x y:
[[sub_norm x y]] = [[x]] - [[y]].
Proof.
- intros x y; unfold sub_norm; rewrite spec_add_normc; auto.
+ unfold sub_norm; rewrite spec_add_normc; auto.
rewrite spec_oppc; ring.
Qed.
- Theorem spec_sub_normc_bis : forall x y : Qc,
+ Theorem spec_sub_normc_bis : forall x y : Qc,
[sub_norm (of_Qc x) (of_Qc y)] = x-y.
Proof.
intros.
@@ -1199,13 +1144,13 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
rewrite strong_spec_red.
symmetry; apply (Qred_complete (x+(-y)%Qc)%Q).
rewrite spec_sub_norm, ! strong_spec_of_Qc.
- unfold Qcopp, Q2Qc; rewrite Qred_correct; auto with qarith.
+ unfold Qcopp, Q2Qc, this. rewrite Qred_correct ; auto with qarith.
Qed.
Theorem spec_mulc x y:
[[mul x y]] = [[x]] * [[y]].
Proof.
- intros x y; unfold to_Qc.
+ unfold to_Qc.
apply trans_equal with (!! ([x] * [y])).
unfold Q2Qc.
apply Qc_decomp; intros _ _; unfold this.
@@ -1219,7 +1164,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
Theorem spec_mul_normc x y:
[[mul_norm x y]] = [[x]] * [[y]].
Proof.
- intros x y; unfold to_Qc.
+ unfold to_Qc.
apply trans_equal with (!! ([x] * [y])).
unfold Q2Qc.
apply Qc_decomp; intros _ _; unfold this.
@@ -1230,7 +1175,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
apply Qmult_comp; apply Qeq_sym; apply Qred_correct.
Qed.
- Theorem spec_mul_normc_bis : forall x y : Qc,
+ Theorem spec_mul_normc_bis : forall x y : Qc,
[mul_norm (of_Qc x) (of_Qc y)] = x*y.
Proof.
intros.
@@ -1243,7 +1188,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
Theorem spec_invc x:
[[inv x]] = /[[x]].
Proof.
- intros x; unfold to_Qc.
+ unfold to_Qc.
apply trans_equal with (!! (/[x])).
unfold Q2Qc.
apply Qc_decomp; intros _ _; unfold this.
@@ -1257,7 +1202,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
Theorem spec_inv_normc x:
[[inv_norm x]] = /[[x]].
Proof.
- intros x; unfold to_Qc.
+ unfold to_Qc.
apply trans_equal with (!! (/[x])).
unfold Q2Qc.
apply Qc_decomp; intros _ _; unfold this.
@@ -1268,7 +1213,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
apply Qinv_comp; apply Qeq_sym; apply Qred_correct.
Qed.
- Theorem spec_inv_normc_bis : forall x : Qc,
+ Theorem spec_inv_normc_bis : forall x : Qc,
[inv_norm (of_Qc x)] = /x.
Proof.
intros.
@@ -1280,19 +1225,19 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
Theorem spec_divc x y: [[div x y]] = [[x]] / [[y]].
Proof.
- intros x y; unfold div; rewrite spec_mulc; auto.
+ unfold div; rewrite spec_mulc; auto.
unfold Qcdiv; apply f_equal2 with (f := Qcmult); auto.
- apply spec_invc; 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 div_norm; rewrite spec_mul_normc; auto.
unfold Qcdiv; apply f_equal2 with (f := Qcmult); auto.
apply spec_inv_normc; auto.
Qed.
- Theorem spec_div_normc_bis : forall x y : Qc,
+ Theorem spec_div_normc_bis : forall x y : Qc,
[div_norm (of_Qc x) (of_Qc y)] = x/y.
Proof.
intros.
@@ -1300,12 +1245,12 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
rewrite strong_spec_red.
symmetry; apply (Qred_complete (x*(/y)%Qc)%Q).
rewrite spec_div_norm, ! strong_spec_of_Qc.
- unfold Qcinv, Q2Qc; rewrite Qred_correct; auto with qarith.
+ unfold Qcinv, Q2Qc, this; rewrite Qred_correct; auto with qarith.
Qed.
- Theorem spec_squarec x: [[square x]] = [[x]]^2.
+ Theorem spec_squarec x: [[square x]] = [[x]]^2.
Proof.
- intros x; unfold to_Qc.
+ unfold to_Qc.
apply trans_equal with (!! ([x]^2)).
unfold Q2Qc.
apply Qc_decomp; intros _ _; unfold this.
@@ -1322,7 +1267,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
Theorem spec_power_posc x p:
[[power_pos x p]] = [[x]] ^ nat_of_P p.
Proof.
- intros x p; unfold to_Qc.
+ unfold to_Qc.
apply trans_equal with (!! ([x]^Zpos p)).
unfold Q2Qc.
apply Qc_decomp; intros _ _; unfold this.
diff --git a/theories/Numbers/Rational/SpecViaQ/QSig.v b/theories/Numbers/Rational/SpecViaQ/QSig.v
index be9b2d4e..10d0189a 100644
--- a/theories/Numbers/Rational/SpecViaQ/QSig.v
+++ b/theories/Numbers/Rational/SpecViaQ/QSig.v
@@ -6,9 +6,9 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: QSig.v 11207 2008-07-04 16:50:32Z letouzey $ i*)
+(*i $Id$ i*)
-Require Import QArith Qpower.
+Require Import QArith Qpower Qminmax Orders RelationPairs GenericMinMax.
Open Scope Q_scope.
@@ -23,75 +23,203 @@ Module Type QType.
Parameter t : Type.
Parameter to_Q : t -> Q.
- Notation "[ x ]" := (to_Q x).
+ Local Notation "[ x ]" := (to_Q x).
Definition eq x y := [x] == [y].
+ Definition lt x y := [x] < [y].
+ Definition le x y := [x] <= [y].
Parameter of_Q : Q -> t.
Parameter spec_of_Q: forall x, to_Q (of_Q x) == x.
+ Parameter red : t -> t.
+ Parameter compare : t -> t -> comparison.
+ Parameter eq_bool : t -> t -> bool.
+ Parameter max : t -> t -> t.
+ Parameter min : t -> t -> t.
Parameter zero : t.
Parameter one : t.
Parameter minus_one : t.
+ Parameter add : t -> t -> t.
+ Parameter sub : t -> t -> t.
+ Parameter opp : t -> t.
+ Parameter mul : t -> t -> t.
+ Parameter square : t -> t.
+ Parameter inv : t -> t.
+ Parameter div : t -> t -> t.
+ Parameter power : t -> Z -> t.
+ Parameter spec_red : forall x, [red x] == [x].
+ Parameter strong_spec_red : forall x, [red x] = Qred [x].
+ Parameter spec_compare : forall x y, compare x y = ([x] ?= [y]).
+ Parameter spec_eq_bool : forall x y, eq_bool x y = Qeq_bool [x] [y].
+ Parameter spec_max : forall x y, [max x y] == Qmax [x] [y].
+ Parameter spec_min : forall x y, [min x y] == Qmin [x] [y].
Parameter spec_0: [zero] == 0.
Parameter spec_1: [one] == 1.
Parameter spec_m1: [minus_one] == -(1).
+ Parameter spec_add: forall x y, [add x y] == [x] + [y].
+ Parameter spec_sub: forall x y, [sub x y] == [x] - [y].
+ Parameter spec_opp: forall x, [opp x] == - [x].
+ Parameter spec_mul: forall x y, [mul x y] == [x] * [y].
+ Parameter spec_square: forall x, [square x] == [x] ^ 2.
+ Parameter spec_inv : forall x, [inv x] == / [x].
+ Parameter spec_div: forall x y, [div x y] == [x] / [y].
+ Parameter spec_power: forall x z, [power x z] == [x] ^ z.
- Parameter compare : t -> t -> comparison.
+End QType.
- Parameter spec_compare : forall x y, compare x y = ([x] ?= [y]).
+(** NB: several of the above functions come with [..._norm] variants
+ that expect reduced arguments and return reduced results. *)
- 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.
+(** TODO : also speak of specifications via Qcanon ... *)
- Parameter eq_bool : t -> t -> bool.
-
- Parameter spec_eq_bool : forall x y,
- if eq_bool x y then [x]==[y] else ~([x]==[y]).
+Module Type QType_Notation (Import Q : QType).
+ Notation "[ x ]" := (to_Q x).
+ Infix "==" := eq (at level 70).
+ Notation "x != y" := (~x==y) (at level 70).
+ Infix "<=" := le.
+ Infix "<" := lt.
+ Notation "0" := zero.
+ Notation "1" := one.
+ Infix "+" := add.
+ Infix "-" := sub.
+ Infix "*" := mul.
+ Notation "- x" := (opp x).
+ Infix "/" := div.
+ Notation "/ x" := (inv x).
+ Infix "^" := power.
+End QType_Notation.
- Parameter red : t -> t.
-
- Parameter spec_red : forall x, [red x] == [x].
- Parameter strong_spec_red : forall x, [red x] = Qred [x].
+Module Type QType' := QType <+ QType_Notation.
- Parameter add : t -> t -> t.
- Parameter spec_add: forall x y, [add x y] == [x] + [y].
+Module QProperties (Import Q : QType').
- Parameter sub : t -> t -> t.
+(** Conversion to Q *)
- Parameter spec_sub: forall x y, [sub x y] == [x] - [y].
+Hint Rewrite
+ spec_red spec_compare spec_eq_bool spec_min spec_max
+ spec_add spec_sub spec_opp spec_mul spec_square spec_inv spec_div
+ spec_power : qsimpl.
+Ltac qify := unfold eq, lt, le in *; autorewrite with qsimpl;
+ try rewrite spec_0 in *; try rewrite spec_1 in *; try rewrite spec_m1 in *.
- Parameter opp : t -> t.
+(** NB: do not add [spec_0] in the autorewrite database. Otherwise,
+ after instanciation in BigQ, this lemma become convertible to 0=0,
+ and autorewrite loops. Idem for [spec_1] and [spec_m1] *)
- Parameter spec_opp: forall x, [opp x] == - [x].
+(** Morphisms *)
- Parameter mul : t -> t -> t.
+Ltac solve_wd1 := intros x x' Hx; qify; now rewrite Hx.
+Ltac solve_wd2 := intros x x' Hx y y' Hy; qify; now rewrite Hx, Hy.
- Parameter spec_mul: forall x y, [mul x y] == [x] * [y].
+Local Obligation Tactic := solve_wd2 || solve_wd1.
- Parameter square : t -> t.
+Instance : Measure to_Q.
+Instance eq_equiv : Equivalence eq.
- Parameter spec_square: forall x, [square x] == [x] ^ 2.
+Program Instance lt_wd : Proper (eq==>eq==>iff) lt.
+Program Instance le_wd : Proper (eq==>eq==>iff) le.
+Program Instance red_wd : Proper (eq==>eq) red.
+Program Instance compare_wd : Proper (eq==>eq==>Logic.eq) compare.
+Program Instance eq_bool_wd : Proper (eq==>eq==>Logic.eq) eq_bool.
+Program Instance min_wd : Proper (eq==>eq==>eq) min.
+Program Instance max_wd : Proper (eq==>eq==>eq) max.
+Program Instance add_wd : Proper (eq==>eq==>eq) add.
+Program Instance sub_wd : Proper (eq==>eq==>eq) sub.
+Program Instance opp_wd : Proper (eq==>eq) opp.
+Program Instance mul_wd : Proper (eq==>eq==>eq) mul.
+Program Instance square_wd : Proper (eq==>eq) square.
+Program Instance inv_wd : Proper (eq==>eq) inv.
+Program Instance div_wd : Proper (eq==>eq==>eq) div.
+Program Instance power_wd : Proper (eq==>Logic.eq==>eq) power.
- Parameter inv : t -> t.
+(** Let's implement [HasCompare] *)
- Parameter spec_inv : forall x, [inv x] == / [x].
+Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y).
+Proof. intros. qify. destruct (Qcompare_spec [x] [y]); auto. Qed.
- Parameter div : t -> t -> t.
+(** Let's implement [TotalOrder] *)
- Parameter spec_div: forall x y, [div x y] == [x] / [y].
+Definition lt_compat := lt_wd.
+Instance lt_strorder : StrictOrder lt.
- Parameter power : t -> Z -> t.
+Lemma le_lteq : forall x y, x<=y <-> x<y \/ x==y.
+Proof. intros. qify. apply Qle_lteq. Qed.
- Parameter spec_power: forall x z, [power x z] == [x] ^ z.
+Lemma lt_total : forall x y, x<y \/ x==y \/ y<x.
+Proof. intros. destruct (compare_spec x y); auto. Qed.
-End QType.
+(** Let's implement [HasEqBool] *)
-(** NB: several of the above functions come with [..._norm] variants
- that expect reduced arguments and return reduced results. *)
+Definition eqb := eq_bool.
-(** TODO : also speak of specifications via Qcanon ... *)
+Lemma eqb_eq : forall x y, eq_bool x y = true <-> x == y.
+Proof. intros. qify. apply Qeq_bool_iff. Qed.
+
+Lemma eqb_correct : forall x y, eq_bool x y = true -> x == y.
+Proof. now apply eqb_eq. Qed.
+
+Lemma eqb_complete : forall x y, x == y -> eq_bool x y = true.
+Proof. now apply eqb_eq. Qed.
+
+(** Let's implement [HasMinMax] *)
+
+Lemma max_l : forall x y, y<=x -> max x y == x.
+Proof. intros x y. qify. apply Qminmax.Q.max_l. Qed.
+
+Lemma max_r : forall x y, x<=y -> max x y == y.
+Proof. intros x y. qify. apply Qminmax.Q.max_r. Qed.
+
+Lemma min_l : forall x y, x<=y -> min x y == x.
+Proof. intros x y. qify. apply Qminmax.Q.min_l. Qed.
+
+Lemma min_r : forall x y, y<=x -> min x y == y.
+Proof. intros x y. qify. apply Qminmax.Q.min_r. Qed.
+
+(** Q is a ring *)
+
+Lemma add_0_l : forall x, 0+x == x.
+Proof. intros. qify. apply Qplus_0_l. Qed.
+
+Lemma add_comm : forall x y, x+y == y+x.
+Proof. intros. qify. apply Qplus_comm. Qed.
+
+Lemma add_assoc : forall x y z, x+(y+z) == x+y+z.
+Proof. intros. qify. apply Qplus_assoc. Qed.
+
+Lemma mul_1_l : forall x, 1*x == x.
+Proof. intros. qify. apply Qmult_1_l. Qed.
+
+Lemma mul_comm : forall x y, x*y == y*x.
+Proof. intros. qify. apply Qmult_comm. Qed.
+
+Lemma mul_assoc : forall x y z, x*(y*z) == x*y*z.
+Proof. intros. qify. apply Qmult_assoc. Qed.
+
+Lemma mul_add_distr_r : forall x y z, (x+y)*z == x*z + y*z.
+Proof. intros. qify. apply Qmult_plus_distr_l. Qed.
+
+Lemma sub_add_opp : forall x y, x-y == x+(-y).
+Proof. intros. qify. now unfold Qminus. Qed.
+
+Lemma add_opp_diag_r : forall x, x+(-x) == 0.
+Proof. intros. qify. apply Qplus_opp_r. Qed.
+
+(** Q is a field *)
+
+Lemma neq_1_0 : 1!=0.
+Proof. intros. qify. apply Q_apart_0_1. Qed.
+
+Lemma div_mul_inv : forall x y, x/y == x*(/y).
+Proof. intros. qify. now unfold Qdiv. Qed.
+
+Lemma mul_inv_diag_l : forall x, x!=0 -> /x * x == 1.
+Proof. intros x. qify. rewrite Qmult_comm. apply Qmult_inv_r. Qed.
+
+End QProperties.
+
+Module QTypeExt (Q : QType)
+ <: QType <: TotalOrder <: HasCompare Q <: HasMinMax Q <: HasEqBool Q
+ := Q <+ QProperties. \ No newline at end of file