Adding: Field instance for Q.

      : Power function from Q -> Z -> Q.
      : Absolute value function.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9901 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 427 insertions, 130 deletions

diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v
index f919398f0..198fedd55 100644
--- a/theories/QArith/QArith_base.v
+++ b/theories/QArith/QArith_base.v
@@ -165,6 +165,13 @@ Infix "/" := Qdiv : Q_scope.
 
 Notation " ' x " := (Zpos x) (at level 20, no associativity) : Z_scope.
 
+Lemma Qmake_Qdiv : forall a b, a#b==inject_Z a/inject_Z ('b).
+Proof.
+intros a b.
+unfold Qeq.
+simpl.
+ring.
+Qed.
 
 (** * Setoid compatibility results *)
 
@@ -416,6 +423,11 @@ Qed.
 
 (** * Inverse and division. *) 
 
+Lemma Qinv_involutive : forall q, (/ / q) == q.
+Proof.
+intros [[|n|n] d]; red; simpl; reflexivity.
+Qed.
+
 Theorem Qmult_inv_r : forall x, ~ x == 0 -> x*(/x) == 1.
 Proof.
   intros (x1, x2); unfold Qeq, Qdiv, Qmult; case x1; simpl;
@@ -641,50 +653,45 @@ Proof.
   Close Scope Z_scope.
 Qed.
 
-(** * Rational to the n-th power *)
-
-Fixpoint Qpower (q:Q)(n:nat) { struct n } : Q := 
-  match n with 
-    | O => 1
-    | S n => q * (Qpower q n)
-  end. 
-
-Notation " q ^ n " := (Qpower q n) : Q_scope.
-
-Lemma Qpower_1 : forall n, 1^n == 1.
+Lemma Qmult_le_0_compat : forall a b, 0 <= a -> 0 <= b -> 0 <= a*b.
 Proof.
-  induction n; simpl; auto with qarith.
-  rewrite IHn; auto with qarith.
+intros a b Ha Hb.
+unfold Qle in *.
+simpl in *.
+auto with *.
 Qed.
 
-Lemma Qpower_0 : forall n, n<>O -> 0^n == 0.
+Lemma Qinv_le_0_compat : forall a, 0 <= a -> 0 <= /a.
 Proof.
-  destruct n; simpl.
-  destruct 1; auto.
-  intros. 
-  compute; auto.
+intros [[|n|n] d] Ha; assumption.
 Qed.
 
-Lemma Qpower_pos : forall p n, 0 <= p -> 0 <= p^n.
-Proof.
-  induction n; simpl; auto with qarith.
-  intros; compute; intro; discriminate.
-  intros.
-  apply Qle_trans with (0*(p^n)).
-  compute; intro; discriminate.
-  apply Qmult_le_compat_r; auto.
-Qed.
+(** * Rational to the n-th power *)
+
+Definition Qpower_positive (q:Q)(p:positive) : Q := 
+ pow_pos Qmult q p.
 
-Lemma Qinv_power_n : forall n p, (1#p)^n == /(inject_Z ('p))^n.
+Add Morphism Qpower_positive with signature Qeq ==> eq ==> Qeq as Qpower_positive_comp.
 Proof.
-  induction n.
-  compute; auto.
-  simpl.
-  intros; rewrite IHn; clear IHn.
-  unfold Qdiv; rewrite Qinv_mult_distr.
-  setoid_replace (1#p) with (/ inject_Z ('p)).
-  apply Qeq_refl.
-  compute; auto.
+intros x1 x2 Hx y.
+unfold Qpower_positive.
+induction y; simpl;
+try rewrite IHy;
+try rewrite Hx;
+reflexivity.
 Qed.
 
+Definition Qpower (q:Q) (z:Z) :=
+    match z with
+      | Zpos p => Qpower_positive q p
+      | Z0 => 1
+      | Zneg p => /Qpower_positive q p
+    end.
+
+Notation " q ^ z " := (Qpower q z) : Q_scope.
 
+Add Morphism Qpower with signature Qeq ==> eq ==> Qeq as Qpower_comp.
+Proof.
+intros x1 x2 Hx [|y|y]; try reflexivity;
+simpl; rewrite Hx; reflexivity.
+Qed.
diff --git a/theories/QArith/Qabs.v b/theories/QArith/Qabs.v
new file mode 100644
index 000000000..511463ee7
--- /dev/null
+++ b/theories/QArith/Qabs.v
@@ -0,0 +1,103 @@
+Require Export QArith.
+Require Export Qreduction.
+
+Hint Resolve Qlt_le_weak : qarith.
+
+Definition Qabs (x:Q) := let (n,d):=x in (Zabs n#d).
+
+Lemma Qabs_case : forall (x:Q) (P : Q -> Type), (0 <= x -> P x) -> (x <= 0 -> P (- x)) -> P (Qabs x).
+Proof.
+intros x P H1 H2.
+destruct x as [[|xn|xn] xd];
+[apply H1|apply H1|apply H2];
+abstract (compute; discriminate).
+Defined.
+
+Add Morphism Qabs with signature Qeq ==> Qeq as Qabs_wd.
+intros [xn xd] [yn yd] H.
+simpl.
+unfold Qeq in *.
+simpl in *.
+change (' yd)%Z with (Zabs (' yd)).
+change (' xd)%Z with (Zabs (' xd)).
+repeat rewrite <- Zabs_Zmult.
+congruence.
+Qed.
+
+Lemma Qabs_pos : forall x, 0 <= x -> Qabs x == x.
+Proof.
+intros x H.
+apply Qabs_case.
+reflexivity.
+intros H0.
+setoid_replace x with 0.
+reflexivity.
+apply Qle_antisym; assumption.
+Qed.
+
+Lemma Qabs_neg : forall x, x <= 0 -> Qabs x == - x.
+Proof.
+intros x H.
+apply Qabs_case.
+intros H0.
+setoid_replace x with 0.
+reflexivity.
+apply Qle_antisym; assumption.
+reflexivity.
+Qed.
+
+Lemma Qabs_nonneg : forall x, 0 <= (Qabs x).
+intros x.
+apply Qabs_case.
+auto.
+apply (Qopp_le_compat x 0).
+Qed.
+
+Lemma Zabs_Qabs : forall n d, (Zabs n#d)==Qabs (n#d).
+Proof.
+intros [|n|n]; reflexivity.
+Qed.
+
+Lemma Qabs_opp : forall x, Qabs (-x) == Qabs x.
+Proof.
+intros x.
+do 2 apply Qabs_case; try (intros; ring);
+(intros H0 H1;
+setoid_replace x with 0;[reflexivity|];
+apply Qle_antisym);try assumption;
+rewrite Qle_minus_iff in *;
+ring_simplify;
+ring_simplify in H1;
+assumption.
+Qed.
+
+Lemma Qabs_triangle : forall x y, Qabs (x+y) <= Qabs x + Qabs y.
+Proof.
+intros [xn xd] [yn yd].
+unfold Qplus.
+unfold Qle.
+simpl.
+apply Zmult_le_compat_r;auto with *.
+change (' yd)%Z with (Zabs (' yd)).
+change (' xd)%Z with (Zabs (' xd)).
+repeat rewrite <- Zabs_Zmult.
+apply Zabs_triangle.
+Qed.
+
+Lemma Qabs_triangle_reverse : forall x y, Qabs x - Qabs y <= Qabs (x - y).
+Proof.
+intros x y.
+rewrite Qle_minus_iff.
+setoid_replace (Qabs (x - y) + - (Qabs x - Qabs y)) with ((Qabs (x - y) + Qabs y) + - Qabs x) by ring.
+rewrite <- Qle_minus_iff.
+setoid_replace (Qabs x) with (Qabs (x-y+y)).
+apply Qabs_triangle.
+apply Qabs_wd.
+ring.
+Qed.
+
+Definition Qminus' x y := Qred (Qminus x y).
+Lemma Qminus'_correct : forall p q : Q, (Qminus' p q)==(Qminus p q).
+Proof.
+  intros; unfold Qminus' in |- *; apply Qred_correct; auto.
+Qed.
diff --git a/theories/QArith/Qfield.v b/theories/QArith/Qfield.v
new file mode 100644
index 000000000..3b14a47ce
--- /dev/null
+++ b/theories/QArith/Qfield.v
@@ -0,0 +1,131 @@
+(************************************************************************)
+(*  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: Qring.v 9427 2006-12-11 18:46:35Z bgregoir $ i*)
+
+Require Export Field.
+Require Export QArith_base.
+Require Import NArithRing.
+
+(** * A ring tactic for rational numbers *)
+
+Definition Qeq_bool (x y : Q) :=
+  if Qeq_dec x y then true else false.
+
+Lemma Qeq_bool_correct : forall x y : Q, Qeq_bool x y = true -> x==y.
+Proof.
+  intros x y; unfold Qeq_bool in |- *; case (Qeq_dec x y); simpl in |- *; auto.
+  intros _ H; inversion H.
+Qed.
+
+Definition Qsft : field_theory 0 1 Qplus Qmult Qminus Qopp Qdiv Qinv Qeq.
+Proof.
+  constructor.
+  constructor.
+  exact Qplus_0_l.
+  exact Qplus_comm.
+  exact Qplus_assoc.
+  exact Qmult_1_l.
+  exact Qmult_comm.
+  exact Qmult_assoc.
+  exact Qmult_plus_distr_l.
+  reflexivity.
+  exact Qplus_opp_r.
+  discriminate.
+  reflexivity.
+  intros p Hp.
+  rewrite Qmult_comm.
+  apply Qmult_inv_r.
+  exact Hp.
+Qed.
+
+Lemma Qpower_theory : power_theory 1 Qmult Qeq Z_of_N Qpower.
+Proof.
+constructor.
+intros r [|n];
+reflexivity.
+Qed.
+
+Ltac isQcst t :=
+  match t with
+  | inject_Z ?z => isZcst z
+  | Qmake ?n ?d =>
+    match isZcst n with
+      true => isPcst d
+    | _ => false
+    end
+  | _ => false
+  end.
+
+Ltac Qcst t :=
+  match isQcst t with
+    true => t
+    | _ => NotConstant
+  end.
+
+Ltac Qpow_tac t :=
+  match t with
+  | Z_of_N ?n => Ncst n
+  | NtoZ ?n => Ncst n
+  | _ => NotConstant
+  end.
+
+Add Field Qfield : Qsft(decidable Qeq_bool_correct, constants [Qcst], power_tac Qpower_theory [Qpow_tac]).
+(** Exemple of use: *)
+
+Section Examples. 
+
+Let ex1 : forall x y z : Q, (x+y)*z ==  (x*z)+(y*z).
+  intros.
+  ring.
+Qed.
+
+Let ex2 : forall x y : Q, x+y == y+x.
+  intros. 
+  ring.
+Qed.
+
+Let ex3 : forall x y z : Q, (x+y)+z == x+(y+z).
+  intros.
+  ring.
+Qed.
+
+Let ex4 : (inject_Z 1)+(inject_Z 1)==(inject_Z 2).
+  ring.
+Qed.
+
+Let ex5 : 1+1 == 2#1.
+  ring.
+Qed.
+
+Let ex6 : (1#1)+(1#1) == 2#1.
+  ring.
+Qed.
+
+Let ex7 : forall x : Q, x-x== 0#1.
+  intro.
+  ring.
+Qed.
+
+Example test_field : forall x y : Q, ~(y==0) -> (x/y)*y == x.
+intros.
+field.
+auto.
+Qed.
+
+End Examples.
+
+Lemma Qopp_plus : forall a b,  -(a+b) == -a + -b.
+Proof.
+  intros; ring.
+Qed.
+
+Lemma Qopp_opp : forall q, - -q==q.
+Proof.
+  intros; ring.
+Qed.
diff --git a/theories/QArith/Qpower.v b/theories/QArith/Qpower.v
new file mode 100644
index 000000000..d50443498
--- /dev/null
+++ b/theories/QArith/Qpower.v
@@ -0,0 +1,139 @@
+Require Import Qfield.
+
+Lemma Qpower_positive_1 : forall n, Qpower_positive 1 n == 1.
+Proof.
+induction n;
+simpl; try rewrite IHn; reflexivity.
+Qed.
+
+Lemma Qpower_1 : forall n, 1^n == 1.
+Proof.
+  intros [|n|n]; simpl; try rewrite Qpower_positive_1; reflexivity.
+Qed.
+
+Lemma Qpower_positive_0 : forall n, Qpower_positive 0 n == 0.
+Proof.
+induction n;
+simpl; try rewrite IHn; reflexivity.
+Qed.
+
+Lemma Qpower_0 : forall n, (n<>0)%Z -> 0^n == 0.
+Proof.
+  intros [|n|n] Hn; try (elim Hn; reflexivity); simpl;
+  rewrite Qpower_positive_0; reflexivity.
+Qed.
+
+Lemma Qpower_not_0_positive : forall a n, ~a==0 -> ~Qpower_positive a n == 0.
+Proof.
+intros a n X H.
+apply X; clear X.
+induction n; simpl in *; try assumption;
+destruct (Qmult_integral _ _ H);
+try destruct (Qmult_integral _ _ H0); auto.
+Qed.
+
+Lemma Qpower_pos_positive : forall p n, 0 <= p -> 0 <= Qpower_positive p n.
+intros p n Hp.
+induction n; simpl; repeat apply Qmult_le_0_compat;assumption.
+Qed.
+
+Lemma Qpower_pos : forall p n, 0 <= p -> 0 <= p^n.
+Proof.
+  intros p [|n|n] Hp; simpl; try discriminate;
+  try apply Qinv_le_0_compat;  apply Qpower_pos_positive; assumption.
+Qed.
+
+Lemma Qmult_power_positive  : forall a b n, Qpower_positive (a*b) n == (Qpower_positive a n)*(Qpower_positive b n).
+Proof.
+induction n;
+simpl; repeat rewrite IHn; ring.
+Qed.
+
+Lemma Qmult_power : forall a b n, (a*b)^n == a^n*b^n.
+Proof.
+  intros a b [|n|n]; simpl; 
+  try rewrite Qmult_power_positive;
+  try rewrite Qinv_mult_distr;
+  reflexivity.
+Qed.
+
+Lemma Qinv_power_positive  : forall a n, Qpower_positive (/a) n == /(Qpower_positive a n).
+Proof.
+induction n;
+simpl; repeat (rewrite IHn || rewrite Qinv_mult_distr); reflexivity.
+Qed.
+
+Lemma Qinv_power : forall a n, (/a)^n == /a^n.
+Proof.
+  intros a [|n|n]; simpl; 
+  try rewrite Qinv_power_positive;
+  reflexivity.
+Qed.
+
+Lemma Qdiv_power : forall a b n, (a/b)^n == (a^n/b^n).
+Proof.
+unfold Qdiv.
+intros a b n.
+rewrite Qmult_power.
+rewrite Qinv_power.
+reflexivity.
+Qed.
+
+Lemma Qinv_power_n : forall n p, (1#p)^n == /(inject_Z ('p))^n.
+Proof.
+intros n p.
+rewrite Qmake_Qdiv.
+rewrite Qdiv_power.
+rewrite Qpower_1.
+unfold Qdiv.
+ring.
+Qed.
+
+Lemma Qpower_plus_positive : forall a n m, Qpower_positive a (n+m) == (Qpower_positive a n)*(Qpower_positive a m).
+Proof.
+intros a n m.
+unfold Qpower_positive.
+apply pow_pos_Pplus.
+apply Q_Setoid.
+apply Qmult_comp.
+apply Qmult_comm.
+apply Qmult_assoc.
+Qed.
+
+Lemma Qpower_opp : forall a n, a^(-n) == /a^n.
+Proof.
+intros a [|n|n]; simpl; try reflexivity.
+symmetry; apply Qinv_involutive.
+Qed.
+
+Lemma Qpower_minus_positive : forall a (n m:positive), (Pcompare n m Eq=Gt)%positive -> Qpower_positive a (n-m)%positive == (Qpower_positive a n)/(Qpower_positive a m).
+Proof.
+intros a n m H.
+destruct (Qeq_dec a 0).
+ rewrite q.
+ repeat rewrite Qpower_positive_0.
+ reflexivity.
+rewrite <- (Qdiv_mult_l (Qpower_positive a (n - m)) (Qpower_positive a m)).
+ apply Qpower_not_0_positive; assumption.
+apply Qdiv_comp;[|reflexivity].
+rewrite Qmult_comm.
+rewrite <- Qpower_plus_positive.
+rewrite Pplus_minus.
+reflexivity.
+assumption.
+Qed.
+
+Lemma Qpower_plus : forall a n m, ~a==0 -> a^(n+m) == a^n*a^m.
+Proof.
+intros a [|n|n] [|m|m] H; simpl; try ring;
+try rewrite Qpower_plus_positive;
+try apply Qinv_mult_distr; try reflexivity;
+case_eq ((n ?= m)%positive Eq); intros H0; simpl;
+ try rewrite Qpower_minus_positive;
+ try rewrite (Pcompare_Eq_eq _ _ H0);
+ try (field; try split; apply Qpower_not_0_positive);
+ try assumption;
+ apply ZC2;
+ assumption.
+Qed.
+
diff --git a/theories/QArith/Qreduction.v b/theories/QArith/Qreduction.v
index 7ca07f841..ddd9b0a26 100644
--- a/theories/QArith/Qreduction.v
+++ b/theories/QArith/Qreduction.v
@@ -145,6 +145,7 @@ Qed.
 
 Definition Qplus' (p q : Q) := Qred (Qplus p q).
 Definition Qmult' (p q : Q) := Qred (Qmult p q). 
+Definition Qminus' x y := Qred (Qminus x y).
 
 Lemma Qplus'_correct : forall p q : Q, (Qplus' p q)==(Qplus p q).
 Proof.
@@ -156,6 +157,11 @@ Proof.
   intros; unfold Qmult' in |- *; apply Qred_correct; auto.
 Qed.
 
+Lemma Qminus'_correct : forall p q : Q, (Qminus' p q)==(Qminus p q).
+Proof.
+  intros; unfold Qminus' in |- *; apply Qred_correct; auto.
+Qed.
+
 Add Morphism Qplus' : Qplus'_comp.
 Proof.
   intros; unfold Qplus' in |- *.
@@ -167,3 +173,7 @@ Add Morphism Qmult' : Qmult'_comp.
   rewrite H; rewrite H0; auto with qarith.
 Qed.
 
+Add Morphism Qminus' : Qminus'_comp.
+  intros; unfold Qminus' in |- *.
+  rewrite H; rewrite H0; auto with qarith.
+Qed.
diff --git a/theories/QArith/Qring.v b/theories/QArith/Qring.v
index 609e82b07..8c9e2dfa3 100644
--- a/theories/QArith/Qring.v
+++ b/theories/QArith/Qring.v
@@ -8,97 +8,4 @@
 
 (*i $Id$ i*)
 
-Require Export Ring.
-Require Export QArith_base.
-
-(** * A ring tactic for rational numbers *)
-
-Definition Qeq_bool (x y : Q) :=
-  if Qeq_dec x y then true else false.
-
-Lemma Qeq_bool_correct : forall x y : Q, Qeq_bool x y = true -> x==y.
-Proof.
-  intros x y; unfold Qeq_bool in |- *; case (Qeq_dec x y); simpl in |- *; auto.
-  intros _ H; inversion H.
-Qed.
-
-Definition Qsrt : ring_theory 0 1 Qplus Qmult Qminus Qopp Qeq.
-Proof.
-  constructor.
-  exact Qplus_0_l.
-  exact Qplus_comm.
-  exact Qplus_assoc.
-  exact Qmult_1_l.
-  exact Qmult_comm.
-  exact Qmult_assoc.
-  exact Qmult_plus_distr_l.
-  reflexivity.
-  exact Qplus_opp_r.
-Qed.
-
-Ltac isQcst t :=
-  match t with
-  | inject_Z ?z => isZcst z
-  | Qmake ?n ?d =>
-    match isZcst n with
-      true => isPcst d
-    | _ => false
-    end
-  | _ => false
-  end.
-
-Ltac Qcst t :=
-  match isQcst t with
-    true => t
-    | _ => NotConstant
-  end.
-
-Add Ring Qring : Qsrt (decidable Qeq_bool_correct, constants [Qcst]).
-(** Exemple of use: *)
-
-Section Examples. 
-
-Let ex1 : forall x y z : Q, (x+y)*z ==  (x*z)+(y*z).
-  intros.
-  ring.
-Qed.
-
-Let ex2 : forall x y : Q, x+y == y+x.
-  intros. 
-  ring.
-Qed.
-
-Let ex3 : forall x y z : Q, (x+y)+z == x+(y+z).
-  intros.
-  ring.
-Qed.
-
-Let ex4 : (inject_Z 1)+(inject_Z 1)==(inject_Z 2).
- ring.
-Qed.
-
-Let ex5 : 1+1 == 2#1.
-  ring.
-Qed.
-
-Let ex6 : (1#1)+(1#1) == 2#1.
-  ring.
-Qed.
-
-Let ex7 : forall x : Q, x-x== 0#1.
-  intro.
-  ring.
-Qed.
-
-End Examples.
-
-Lemma Qopp_plus : forall a b,  -(a+b) == -a + -b.
-Proof.
-  intros; ring.
-Qed.
-
-Lemma Qopp_opp : forall q, - -q==q.
-Proof.
-  intros; ring.
-Qed.
-
+Require Export Qfield.