diff options
Diffstat (limited to 'theories/QArith/Qpower.v')
| -rw-r--r-- | theories/QArith/Qpower.v | 239 |
1 files changed, 239 insertions, 0 deletions
diff --git a/theories/QArith/Qpower.v b/theories/QArith/Qpower.v new file mode 100644 index 00000000..8672592d --- /dev/null +++ b/theories/QArith/Qpower.v @@ -0,0 +1,239 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + +Require Import Zpow_facts Qfield Qreduction. + +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)) by + (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. + +Lemma Qpower_plus' : forall a n m, (n+m <> 0)%Z -> a^(n+m) == a^n*a^m. +Proof. +intros a n m H. +destruct (Qeq_dec a 0)as [X|X]. +rewrite X. +rewrite Qpower_0 by assumption. +destruct n; destruct m; try (elim H; reflexivity); + simpl; repeat rewrite Qpower_positive_0; ring_simplify; + reflexivity. +apply Qpower_plus. +assumption. +Qed. + +Lemma Qpower_mult_positive : forall a n m, Qpower_positive a (n*m) == Qpower_positive (Qpower_positive a n) m. +Proof. +intros a n m. +induction n using Pind. + reflexivity. +rewrite Pmult_Sn_m. +rewrite Pplus_one_succ_l. +do 2 rewrite Qpower_plus_positive. +rewrite IHn. +rewrite Qmult_power_positive. +reflexivity. +Qed. + +Lemma Qpower_mult : forall a n m, a^(n*m) == (a^n)^m. +Proof. +intros a [|n|n] [|m|m]; simpl; + try rewrite Qpower_positive_1; + try rewrite Qpower_mult_positive; + try rewrite Qinv_power_positive; + try rewrite Qinv_involutive; + try reflexivity. +Qed. + +Lemma Zpower_Qpower : forall (a n:Z), (0<=n)%Z -> inject_Z (a^n) == (inject_Z a)^n. +Proof. +intros a [|n|n] H;[reflexivity| |elim H; reflexivity]. +induction n using Pind. + replace (a^1)%Z with a by ring. + ring. +rewrite Zpos_succ_morphism. +unfold Zsucc. +rewrite Zpower_exp; auto with *; try discriminate. +rewrite Qpower_plus' by discriminate. +rewrite <- IHn by discriminate. +replace (a^'n*a^1)%Z with (a^'n*a)%Z by ring. +ring_simplify. +reflexivity. +Qed. + +Lemma Qsqr_nonneg : forall a, 0 <= a^2. +Proof. +intros a. +destruct (Qlt_le_dec 0 a) as [A|A]. +apply (Qmult_le_0_compat a a); + (apply Qlt_le_weak; assumption). +setoid_replace (a^2) with ((-a)*(-a)) by ring. +rewrite Qle_minus_iff in A. +setoid_replace (0+ - a) with (-a) in A by ring. +apply Qmult_le_0_compat; assumption. +Qed. + +Theorem Qpower_decomp: forall p x y, + Qpower_positive (x #y) p == x ^ Zpos p # (Z2P ((Zpos y) ^ Zpos p)). +Proof. +induction p; intros; unfold Qmult; simpl. +(* xI *) +rewrite IHp, xI_succ_xO, <-Pplus_diag, Pplus_one_succ_l. +repeat rewrite Zpower_pos_is_exp. +red; unfold Qmult, Qnum, Qden, Zpower. +repeat rewrite Zpos_mult_morphism. +repeat rewrite Z2P_correct. +repeat rewrite Zpower_pos_1_r; ring. +apply Zpower_pos_pos; red; auto. +repeat apply Zmult_lt_0_compat; auto; + apply Zpower_pos_pos; red; auto. +(* xO *) +rewrite IHp, <-Pplus_diag. +repeat rewrite Zpower_pos_is_exp. +red; unfold Qmult, Qnum, Qden, Zpower. +repeat rewrite Zpos_mult_morphism. +repeat rewrite Z2P_correct; try ring. +apply Zpower_pos_pos; red; auto. +repeat apply Zmult_lt_0_compat; auto; + apply Zpower_pos_pos; red; auto. +(* xO *) +unfold Qmult; simpl. +red; simpl; rewrite Zpower_pos_1_r; + rewrite Zpos_mult_morphism; ring. +Qed. |