diff options
Diffstat (limited to 'theories/QArith/Qcanon.v')
| -rw-r--r-- | theories/QArith/Qcanon.v | 344 |
1 files changed, 184 insertions, 160 deletions
diff --git a/theories/QArith/Qcanon.v b/theories/QArith/Qcanon.v index 9cbd400d..98c5ff9e 100644 --- a/theories/QArith/Qcanon.v +++ b/theories/QArith/Qcanon.v @@ -6,9 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Qcanon.v 8989 2006-06-25 22:17:49Z letouzey $ i*) +(*i $Id: Qcanon.v 9245 2006-10-17 12:53:34Z notin $ i*) +Require Import Field. Require Import QArith. +Require Import Znumtheory. Require Import Eqdep_dec. (** [Qc] : A canonical representation of rational numbers. @@ -22,50 +24,50 @@ Arguments Scope Qcmake [Q_scope]. Open Scope Qc_scope. Lemma Qred_identity : - forall q:Q, Zgcd (Qnum q) (QDen q) = 1%Z -> Qred q = q. + forall q:Q, Zgcd (Qnum q) (QDen q) = 1%Z -> Qred q = q. Proof. -unfold Qred; intros (a,b); simpl. -generalize (Zggcd_gcd a ('b)) (Zggcd_correct_divisors a ('b)). -intros. -rewrite H1 in H; clear H1. -destruct (Zggcd a ('b)) as (g,(aa,bb)); simpl in *; subst. -destruct H0. -rewrite Zmult_1_l in H, H0. -subst; simpl; auto. + unfold Qred; intros (a,b); simpl. + generalize (Zggcd_gcd a ('b)) (Zggcd_correct_divisors a ('b)). + intros. + rewrite H1 in H; clear H1. + destruct (Zggcd a ('b)) as (g,(aa,bb)); simpl in *; subst. + destruct H0. + rewrite Zmult_1_l in H, H0. + subst; simpl; auto. Qed. Lemma Qred_identity2 : - forall q:Q, Qred q = q -> Zgcd (Qnum q) (QDen q) = 1%Z. -Proof. -unfold Qred; intros (a,b); simpl. -generalize (Zggcd_gcd a ('b)) (Zggcd_correct_divisors a ('b)) (Zgcd_is_pos a ('b)). -intros. -rewrite <- H; rewrite <- H in H1; clear H. -destruct (Zggcd a ('b)) as (g,(aa,bb)); simpl in *; subst. -injection H2; intros; clear H2. -destruct H0. -clear H0 H3. -destruct g as [|g|g]; destruct bb as [|bb|bb]; simpl in *; try discriminate. -f_equal. -apply Pmult_reg_r with bb. -injection H2; intros. -rewrite <- H0. -rewrite H; simpl; auto. -elim H1; auto. + forall q:Q, Qred q = q -> Zgcd (Qnum q) (QDen q) = 1%Z. +Proof. + unfold Qred; intros (a,b); simpl. + generalize (Zggcd_gcd a ('b)) (Zggcd_correct_divisors a ('b)) (Zgcd_is_pos a ('b)). + intros. + rewrite <- H; rewrite <- H in H1; clear H. + destruct (Zggcd a ('b)) as (g,(aa,bb)); simpl in *; subst. + injection H2; intros; clear H2. + destruct H0. + clear H0 H3. + destruct g as [|g|g]; destruct bb as [|bb|bb]; simpl in *; try discriminate. + f_equal. + apply Pmult_reg_r with bb. + injection H2; intros. + rewrite <- H0. + rewrite H; simpl; auto. + elim H1; auto. Qed. Lemma Qred_iff : forall q:Q, Qred q = q <-> Zgcd (Qnum q) (QDen q) = 1%Z. Proof. -split; intros. -apply Qred_identity2; auto. -apply Qred_identity; auto. + split; intros. + apply Qred_identity2; auto. + apply Qred_identity; auto. Qed. Lemma Qred_involutive : forall q:Q, Qred (Qred q) = Qred q. Proof. -intros; apply Qred_complete. -apply Qred_correct. + intros; apply Qred_complete. + apply Qred_correct. Qed. Definition Q2Qc (q:Q) : Qc := Qcmake (Qred q) (Qred_involutive q). @@ -74,16 +76,16 @@ Notation " !! " := Q2Qc : Qc_scope. Lemma Qc_is_canon : forall q q' : Qc, q == q' -> q = q'. Proof. -intros (q,proof_q) (q',proof_q'). -simpl. -intros H. -assert (H0:=Qred_complete _ _ H). -assert (q = q') by congruence. -subst q'. -assert (proof_q = proof_q'). - apply eq_proofs_unicity; auto; intros. - repeat decide equality. -congruence. + intros (q,proof_q) (q',proof_q'). + simpl. + intros H. + assert (H0:=Qred_complete _ _ H). + assert (q = q') by congruence. + subst q'. + assert (proof_q = proof_q'). + apply eq_proofs_unicity; auto; intros. + repeat decide equality. + congruence. Qed. Hint Resolve Qc_is_canon. @@ -105,39 +107,39 @@ Notation "p ?= q" := (Qccompare p q) : Qc_scope. Lemma Qceq_alt : forall p q, (p = q) <-> (p ?= q) = Eq. Proof. -unfold Qccompare. -intros; rewrite <- Qeq_alt. -split; auto. -intro H; rewrite H; auto with qarith. + unfold Qccompare. + intros; rewrite <- Qeq_alt. + split; auto. + intro H; rewrite H; auto with qarith. Qed. Lemma Qclt_alt : forall p q, (p<q) <-> (p?=q = Lt). Proof. -intros; exact (Qlt_alt p q). + intros; exact (Qlt_alt p q). Qed. Lemma Qcgt_alt : forall p q, (p>q) <-> (p?=q = Gt). Proof. -intros; exact (Qgt_alt p q). + intros; exact (Qgt_alt p q). Qed. Lemma Qle_alt : forall p q, (p<=q) <-> (p?=q <> Gt). Proof. -intros; exact (Qle_alt p q). + intros; exact (Qle_alt p q). Qed. Lemma Qge_alt : forall p q, (p>=q) <-> (p?=q <> Lt). Proof. -intros; exact (Qge_alt p q). + intros; exact (Qge_alt p q). Qed. (** equality on [Qc] is decidable: *) Theorem Qc_eq_dec : forall x y:Qc, {x=y} + {x<>y}. Proof. - intros. - destruct (Qeq_dec x y) as [H|H]; auto. - right; swap H; subst; auto with qarith. + intros. + destruct (Qeq_dec x y) as [H|H]; auto. + right; swap H; subst; auto with qarith. Defined. (** The addition, multiplication and opposite are defined @@ -160,8 +162,8 @@ Infix "/" := Qcdiv : Qc_scope. Lemma Q_apart_0_1 : 1 <> 0. Proof. - unfold Q2Qc. - intros H; discriminate H. + unfold Q2Qc. + intros H; discriminate H. Qed. Ltac qc := match goal with @@ -175,309 +177,309 @@ Opaque Qred. Theorem Qcplus_assoc : forall x y z, x+(y+z)=(x+y)+z. Proof. - intros; qc; apply Qplus_assoc. + intros; qc; apply Qplus_assoc. Qed. (** [0] is a neutral element for addition: *) Lemma Qcplus_0_l : forall x, 0+x = x. Proof. - intros; qc; apply Qplus_0_l. + intros; qc; apply Qplus_0_l. Qed. Lemma Qcplus_0_r : forall x, x+0 = x. Proof. - intros; qc; apply Qplus_0_r. + intros; qc; apply Qplus_0_r. Qed. (** Commutativity of addition: *) Theorem Qcplus_comm : forall x y, x+y = y+x. Proof. - intros; qc; apply Qplus_comm. + intros; qc; apply Qplus_comm. Qed. (** Properties of [Qopp] *) Lemma Qcopp_involutive : forall q, - -q = q. Proof. - intros; qc; apply Qopp_involutive. + intros; qc; apply Qopp_involutive. Qed. Theorem Qcplus_opp_r : forall q, q+(-q) = 0. Proof. - intros; qc; apply Qplus_opp_r. + intros; qc; apply Qplus_opp_r. Qed. (** Multiplication is associative: *) Theorem Qcmult_assoc : forall n m p, n*(m*p)=(n*m)*p. Proof. - intros; qc; apply Qmult_assoc. + intros; qc; apply Qmult_assoc. Qed. (** [1] is a neutral element for multiplication: *) Lemma Qcmult_1_l : forall n, 1*n = n. Proof. - intros; qc; apply Qmult_1_l. + intros; qc; apply Qmult_1_l. Qed. Theorem Qcmult_1_r : forall n, n*1=n. Proof. - intros; qc; apply Qmult_1_r. + intros; qc; apply Qmult_1_r. Qed. (** Commutativity of multiplication *) Theorem Qcmult_comm : forall x y, x*y=y*x. Proof. - intros; qc; apply Qmult_comm. + intros; qc; apply Qmult_comm. Qed. (** Distributivity *) Theorem Qcmult_plus_distr_r : forall x y z, x*(y+z)=(x*y)+(x*z). Proof. - intros; qc; apply Qmult_plus_distr_r. + intros; qc; apply Qmult_plus_distr_r. Qed. Theorem Qcmult_plus_distr_l : forall x y z, (x+y)*z=(x*z)+(y*z). Proof. - intros; qc; apply Qmult_plus_distr_l. + intros; qc; apply Qmult_plus_distr_l. Qed. (** Integrality *) Theorem Qcmult_integral : forall x y, x*y=0 -> x=0 \/ y=0. Proof. - intros. - destruct (Qmult_integral x y); try qc; auto. - injection H; clear H; intros. - rewrite <- (Qred_correct (x*y)). - rewrite <- (Qred_correct 0). - rewrite H; auto with qarith. + intros. + destruct (Qmult_integral x y); try qc; auto. + injection H; clear H; intros. + rewrite <- (Qred_correct (x*y)). + rewrite <- (Qred_correct 0). + rewrite H; auto with qarith. Qed. Theorem Qcmult_integral_l : forall x y, ~ x = 0 -> x*y = 0 -> y = 0. Proof. - intros; destruct (Qcmult_integral _ _ H0); tauto. + intros; destruct (Qcmult_integral _ _ H0); tauto. Qed. (** Inverse and division. *) Theorem Qcmult_inv_r : forall x, x<>0 -> x*(/x) = 1. Proof. - intros; qc; apply Qmult_inv_r; auto. + intros; qc; apply Qmult_inv_r; auto. Qed. Theorem Qcmult_inv_l : forall x, x<>0 -> (/x)*x = 1. Proof. - intros. - rewrite Qcmult_comm. - apply Qcmult_inv_r; auto. + intros. + rewrite Qcmult_comm. + apply Qcmult_inv_r; auto. Qed. Lemma Qcinv_mult_distr : forall p q, / (p * q) = /p * /q. Proof. - intros; qc; apply Qinv_mult_distr. + intros; qc; apply Qinv_mult_distr. Qed. Theorem Qcdiv_mult_l : forall x y, y<>0 -> (x*y)/y = x. Proof. - unfold Qcdiv. - intros. - rewrite <- Qcmult_assoc. - rewrite Qcmult_inv_r; auto. - apply Qcmult_1_r. + unfold Qcdiv. + intros. + rewrite <- Qcmult_assoc. + rewrite Qcmult_inv_r; auto. + apply Qcmult_1_r. Qed. Theorem Qcmult_div_r : forall x y, ~ y = 0 -> y*(x/y) = x. Proof. - unfold Qcdiv. - intros. - rewrite Qcmult_assoc. - rewrite Qcmult_comm. - rewrite Qcmult_assoc. - rewrite Qcmult_inv_l; auto. - apply Qcmult_1_l. + unfold Qcdiv. + intros. + rewrite Qcmult_assoc. + rewrite Qcmult_comm. + rewrite Qcmult_assoc. + rewrite Qcmult_inv_l; auto. + apply Qcmult_1_l. Qed. (** Properties of order upon Q. *) Lemma Qcle_refl : forall x, x<=x. Proof. -unfold Qcle; intros; simpl; apply Qle_refl. + unfold Qcle; intros; simpl; apply Qle_refl. Qed. Lemma Qcle_antisym : forall x y, x<=y -> y<=x -> x=y. Proof. -unfold Qcle; intros; simpl in *. -apply Qc_is_canon; apply Qle_antisym; auto. + unfold Qcle; intros; simpl in *. + apply Qc_is_canon; apply Qle_antisym; auto. Qed. Lemma Qcle_trans : forall x y z, x<=y -> y<=z -> x<=z. Proof. -unfold Qcle; intros; eapply Qle_trans; eauto. + unfold Qcle; intros; eapply Qle_trans; eauto. Qed. Lemma Qclt_not_eq : forall x y, x<y -> x<>y. Proof. -unfold Qclt; intros; simpl in *. -intro; destruct (Qlt_not_eq _ _ H). -subst; auto with qarith. + unfold Qclt; intros; simpl in *. + intro; destruct (Qlt_not_eq _ _ H). + subst; auto with qarith. Qed. (** Large = strict or equal *) Lemma Qclt_le_weak : forall x y, x<y -> x<=y. Proof. -unfold Qcle, Qclt; intros; apply Qlt_le_weak; auto. + unfold Qcle, Qclt; intros; apply Qlt_le_weak; auto. Qed. Lemma Qcle_lt_trans : forall x y z, x<=y -> y<z -> x<z. Proof. -unfold Qcle, Qclt; intros; eapply Qle_lt_trans; eauto. + unfold Qcle, Qclt; intros; eapply Qle_lt_trans; eauto. Qed. Lemma Qclt_le_trans : forall x y z, x<y -> y<=z -> x<z. Proof. -unfold Qcle, Qclt; intros; eapply Qlt_le_trans; eauto. + unfold Qcle, Qclt; intros; eapply Qlt_le_trans; eauto. Qed. Lemma Qlt_trans : forall x y z, x<y -> y<z -> x<z. Proof. -unfold Qclt; intros; eapply Qlt_trans; eauto. + unfold Qclt; intros; eapply Qlt_trans; eauto. Qed. (** [x<y] iff [~(y<=x)] *) Lemma Qcnot_lt_le : forall x y, ~ x<y -> y<=x. Proof. -unfold Qcle, Qclt; intros; apply Qnot_lt_le; auto. + unfold Qcle, Qclt; intros; apply Qnot_lt_le; auto. Qed. Lemma Qcnot_le_lt : forall x y, ~ x<=y -> y<x. Proof. -unfold Qcle, Qclt; intros; apply Qnot_le_lt; auto. + unfold Qcle, Qclt; intros; apply Qnot_le_lt; auto. Qed. Lemma Qclt_not_le : forall x y, x<y -> ~ y<=x. Proof. -unfold Qcle, Qclt; intros; apply Qlt_not_le; auto. + unfold Qcle, Qclt; intros; apply Qlt_not_le; auto. Qed. Lemma Qcle_not_lt : forall x y, x<=y -> ~ y<x. Proof. -unfold Qcle, Qclt; intros; apply Qle_not_lt; auto. + unfold Qcle, Qclt; intros; apply Qle_not_lt; auto. Qed. Lemma Qcle_lt_or_eq : forall x y, x<=y -> x<y \/ x==y. Proof. -unfold Qcle, Qclt; intros; apply Qle_lt_or_eq; auto. + unfold Qcle, Qclt; intros; apply Qle_lt_or_eq; auto. Qed. (** Some decidability results about orders. *) Lemma Qc_dec : forall x y, {x<y} + {y<x} + {x=y}. Proof. -unfold Qclt, Qcle; intros. -destruct (Q_dec x y) as [H|H]. -left; auto. -right; apply Qc_is_canon; auto. + unfold Qclt, Qcle; intros. + destruct (Q_dec x y) as [H|H]. + left; auto. + right; apply Qc_is_canon; auto. Defined. Lemma Qclt_le_dec : forall x y, {x<y} + {y<=x}. Proof. -unfold Qclt, Qcle; intros; apply Qlt_le_dec; auto. + unfold Qclt, Qcle; intros; apply Qlt_le_dec; auto. Defined. (** Compatibility of operations with respect to order. *) Lemma Qcopp_le_compat : forall p q, p<=q -> -q <= -p. Proof. -unfold Qcle, Qcopp; intros; simpl in *. -repeat rewrite Qred_correct. -apply Qopp_le_compat; auto. + unfold Qcle, Qcopp; intros; simpl in *. + repeat rewrite Qred_correct. + apply Qopp_le_compat; auto. Qed. Lemma Qcle_minus_iff : forall p q, p <= q <-> 0 <= q+-p. Proof. -unfold Qcle, Qcminus; intros; simpl in *. -repeat rewrite Qred_correct. -apply Qle_minus_iff; auto. + unfold Qcle, Qcminus; intros; simpl in *. + repeat rewrite Qred_correct. + apply Qle_minus_iff; auto. Qed. Lemma Qclt_minus_iff : forall p q, p < q <-> 0 < q+-p. Proof. -unfold Qclt, Qcplus, Qcopp; intros; simpl in *. -repeat rewrite Qred_correct. -apply Qlt_minus_iff; auto. + unfold Qclt, Qcplus, Qcopp; intros; simpl in *. + repeat rewrite Qred_correct. + apply Qlt_minus_iff; auto. Qed. Lemma Qcplus_le_compat : - forall x y z t, x<=y -> z<=t -> x+z <= y+t. + forall x y z t, x<=y -> z<=t -> x+z <= y+t. Proof. -unfold Qcplus, Qcle; intros; simpl in *. -repeat rewrite Qred_correct. -apply Qplus_le_compat; auto. + unfold Qcplus, Qcle; intros; simpl in *. + repeat rewrite Qred_correct. + apply Qplus_le_compat; auto. Qed. Lemma Qcmult_le_compat_r : forall x y z, x <= y -> 0 <= z -> x*z <= y*z. Proof. -unfold Qcmult, Qcle; intros; simpl in *. -repeat rewrite Qred_correct. -apply Qmult_le_compat_r; auto. + unfold Qcmult, Qcle; intros; simpl in *. + repeat rewrite Qred_correct. + apply Qmult_le_compat_r; auto. Qed. Lemma Qcmult_lt_0_le_reg_r : forall x y z, 0 < z -> x*z <= y*z -> x <= y. Proof. -unfold Qcmult, Qcle, Qclt; intros; simpl in *. -repeat progress rewrite Qred_correct in * |-. -eapply Qmult_lt_0_le_reg_r; eauto. + unfold Qcmult, Qcle, Qclt; intros; simpl in *. + repeat progress rewrite Qred_correct in * |-. + eapply Qmult_lt_0_le_reg_r; eauto. Qed. Lemma Qcmult_lt_compat_r : forall x y z, 0 < z -> x < y -> x*z < y*z. Proof. -unfold Qcmult, Qclt; intros; simpl in *. -repeat progress rewrite Qred_correct in *. -eapply Qmult_lt_compat_r; eauto. + unfold Qcmult, Qclt; intros; simpl in *. + repeat progress rewrite Qred_correct in *. + eapply Qmult_lt_compat_r; eauto. Qed. (** Rational to the n-th power *) Fixpoint Qcpower (q:Qc)(n:nat) { struct n } : Qc := - match n with - | O => 1 - | S n => q * (Qcpower q n) - end. + match n with + | O => 1 + | S n => q * (Qcpower q n) + end. Notation " q ^ n " := (Qcpower q n) : Qc_scope. Lemma Qcpower_1 : forall n, 1^n = 1. Proof. -induction n; simpl; auto with qarith. -rewrite IHn; auto with qarith. + induction n; simpl; auto with qarith. + rewrite IHn; auto with qarith. Qed. Lemma Qcpower_0 : forall n, n<>O -> 0^n = 0. Proof. -destruct n; simpl. -destruct 1; auto. -intros. -apply Qc_is_canon. -simpl. -compute; auto. + destruct n; simpl. + destruct 1; auto. + intros. + apply Qc_is_canon. + simpl. + compute; auto. 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 Qcle_trans with (0*(p^n)). -compute; intro; discriminate. -apply Qcmult_le_compat_r; auto. + induction n; simpl; auto with qarith. + intros; compute; intro; discriminate. + intros. + apply Qcle_trans with (0*(p^n)). + compute; intro; discriminate. + apply Qcmult_le_compat_r; auto. Qed. (** And now everything is easier concerning tactics: *) @@ -488,10 +490,12 @@ Definition Qc_eq_bool (x y : Qc) := if Qc_eq_dec x y then true else false. Lemma Qc_eq_bool_correct : forall x y : Qc, Qc_eq_bool x y = true -> x=y. -intros x y; unfold Qc_eq_bool in |- *; case (Qc_eq_dec x y); simpl in |- *; auto. -intros _ H; inversion H. +Proof. + intros x y; unfold Qc_eq_bool in |- *; case (Qc_eq_dec x y); simpl in |- *; auto. + intros _ H; inversion H. Qed. +(* Definition Qcrt : Ring_Theory Qcplus Qcmult 1 0 Qcopp Qc_eq_bool. Proof. constructor. @@ -506,17 +510,37 @@ exact Qcmult_plus_distr_l. unfold Is_true; intros x y; generalize (Qc_eq_bool_correct x y); case (Qc_eq_bool x y); auto. Qed. - Add Ring Qc Qcplus Qcmult 1 0 Qcopp Qc_eq_bool Qcrt [ Qcmake ]. +*) +Definition Qcrt : ring_theory 0 1 Qcplus Qcmult Qcminus Qcopp (eq(A:=Qc)). +Proof. + constructor. + exact Qcplus_0_l. + exact Qcplus_comm. + exact Qcplus_assoc. + exact Qcmult_1_l. + exact Qcmult_comm. + exact Qcmult_assoc. + exact Qcmult_plus_distr_l. + reflexivity. + exact Qcplus_opp_r. +Qed. -(** A field tactic for rational numbers *) +Definition Qcft : + field_theory 0%Qc 1%Qc Qcplus Qcmult Qcminus Qcopp Qcdiv Qcinv (eq(A:=Qc)). +Proof. + constructor. + exact Qcrt. + exact Q_apart_0_1. + reflexivity. + exact Qcmult_inv_l. +Qed. -Require Import Field. +Add Field Qcfield : Qcft. -Add Field Qc Qcplus Qcmult 1 0 Qcopp Qc_eq_bool Qcinv Qcrt Qcmult_inv_l - with div:=Qcdiv. +(** A field tactic for rational numbers *) -Example test_field : forall x y : Qc, y<>0 -> (x/y)*y = x. +Example test_field : (forall x y : Qc, y<>0 -> (x/y)*y = x)%Qc. intros. field. auto. |