diff options
Diffstat (limited to 'coqprime-8.4/Coqprime/ZSum.v')
| -rw-r--r-- | coqprime-8.4/Coqprime/ZSum.v | 335 |
1 files changed, 335 insertions, 0 deletions
diff --git a/coqprime-8.4/Coqprime/ZSum.v b/coqprime-8.4/Coqprime/ZSum.v new file mode 100644 index 000000000..907720f7c --- /dev/null +++ b/coqprime-8.4/Coqprime/ZSum.v @@ -0,0 +1,335 @@ + +(*************************************************************) +(* This file is distributed under the terms of the *) +(* GNU Lesser General Public License Version 2.1 *) +(*************************************************************) +(* Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr *) +(*************************************************************) + +(*********************************************************************** + Summation.v from Z to Z + *********************************************************************) +Require Import Coq.Arith.Arith. +Require Import Coq.setoid_ring.ArithRing. +Require Import Coqprime.ListAux. +Require Import Coq.ZArith.ZArith. +Require Import Coqprime.Iterator. +Require Import Coqprime.ZProgression. + + +Open Scope Z_scope. +(* Iterated Sum *) + +Definition Zsum := + fun n m f => + if Zle_bool n m + then iter 0 f Zplus (progression Zsucc n (Zabs_nat ((1 + m) - n))) + else iter 0 f Zplus (progression Zpred n (Zabs_nat ((1 + n) - m))). +Hint Unfold Zsum . + +Lemma Zsum_nn: forall n f, Zsum n n f = f n. +intros n f; unfold Zsum; rewrite Zle_bool_refl. +replace ((1 + n) - n) with 1; auto with zarith. +simpl; ring. +Qed. + +Theorem permutation_rev: forall (A:Set) (l : list A), permutation (rev l) l. +intros a l; elim l; simpl; auto. +intros a1 l1 Hl1. +apply permutation_trans with (cons a1 (rev l1)); auto. +change (permutation (rev l1 ++ (a1 :: nil)) (app (cons a1 nil) (rev l1))); auto. +Qed. + +Lemma Zsum_swap: forall (n m : Z) (f : Z -> Z), Zsum n m f = Zsum m n f. +intros n m f; unfold Zsum. +generalize (Zle_cases n m) (Zle_cases m n); case (Zle_bool n m); + case (Zle_bool m n); auto with arith. +intros; replace n with m; auto with zarith. +3:intros H1 H2; contradict H2; auto with zarith. +intros H1 H2; apply iter_permutation; auto with zarith. +apply permutation_trans + with (rev (progression Zsucc n (Zabs_nat ((1 + m) - n)))). +apply permutation_sym; apply permutation_rev. +rewrite Zprogression_opp; auto with zarith. +replace (n + Z_of_nat (pred (Zabs_nat ((1 + m) - n)))) with m; auto. +replace (Zabs_nat ((1 + m) - n)) with (S (Zabs_nat (m - n))); auto with zarith. +simpl. +rewrite inj_Zabs_nat; auto with zarith. +rewrite Zabs_eq; auto with zarith. +replace ((1 + m) - n) with (1 + (m - n)); auto with zarith. +cut (0 <= m - n); auto with zarith; unfold Zabs_nat. +case (m - n); auto with zarith. +intros p; case p; simpl; auto with zarith. +intros p1 Hp1; rewrite nat_of_P_xO; rewrite nat_of_P_xI; + rewrite nat_of_P_succ_morphism. +simpl; repeat rewrite plus_0_r. +repeat rewrite <- plus_n_Sm; simpl; auto. +intros p H3; contradict H3; auto with zarith. +intros H1 H2; apply iter_permutation; auto with zarith. +apply permutation_trans + with (rev (progression Zsucc m (Zabs_nat ((1 + n) - m)))). +rewrite Zprogression_opp; auto with zarith. +replace (m + Z_of_nat (pred (Zabs_nat ((1 + n) - m)))) with n; auto. +replace (Zabs_nat ((1 + n) - m)) with (S (Zabs_nat (n - m))); auto with zarith. +simpl. +rewrite inj_Zabs_nat; auto with zarith. +rewrite Zabs_eq; auto with zarith. +replace ((1 + n) - m) with (1 + (n - m)); auto with zarith. +cut (0 <= n - m); auto with zarith; unfold Zabs_nat. +case (n - m); auto with zarith. +intros p; case p; simpl; auto with zarith. +intros p1 Hp1; rewrite nat_of_P_xO; rewrite nat_of_P_xI; + rewrite nat_of_P_succ_morphism. +simpl; repeat rewrite plus_0_r. +repeat rewrite <- plus_n_Sm; simpl; auto. +intros p H3; contradict H3; auto with zarith. +apply permutation_rev. +Qed. + +Lemma Zsum_split_up: + forall (n m p : Z) (f : Z -> Z), + ( n <= m < p ) -> Zsum n p f = Zsum n m f + Zsum (m + 1) p f. +intros n m p f [H H0]. +case (Zle_lt_or_eq _ _ H); clear H; intros H. +unfold Zsum; (repeat rewrite Zle_imp_le_bool); auto with zarith. +assert (H1: n < p). +apply Zlt_trans with ( 1 := H ); auto with zarith. +assert (H2: m < 1 + p). +apply Zlt_trans with ( 1 := H0 ); auto with zarith. +assert (H3: n < 1 + m). +apply Zlt_trans with ( 1 := H ); auto with zarith. +assert (H4: n < 1 + p). +apply Zlt_trans with ( 1 := H1 ); auto with zarith. +replace (Zabs_nat ((1 + p) - (m + 1))) + with (minus (Zabs_nat ((1 + p) - n)) (Zabs_nat ((1 + m) - n))). +apply iter_progression_app; auto with zarith. +apply inj_le_rev. +(repeat rewrite inj_Zabs_nat); auto with zarith. +(repeat rewrite Zabs_eq); auto with zarith. +rewrite next_n_Z; auto with zarith. +rewrite inj_Zabs_nat; auto with zarith. +rewrite Zabs_eq; auto with zarith. +apply inj_eq_rev; auto with zarith. +rewrite inj_minus1; auto with zarith. +(repeat rewrite inj_Zabs_nat); auto with zarith. +(repeat rewrite Zabs_eq); auto with zarith. +apply inj_le_rev. +(repeat rewrite inj_Zabs_nat); auto with zarith. +(repeat rewrite Zabs_eq); auto with zarith. +subst m. +rewrite Zsum_nn; auto with zarith. +unfold Zsum; generalize (Zle_cases n p); generalize (Zle_cases (n + 1) p); + case (Zle_bool n p); case (Zle_bool (n + 1) p); auto with zarith. +intros H1 H2. +replace (Zabs_nat ((1 + p) - n)) with (S (Zabs_nat (p - n))); auto with zarith. +replace (n + 1) with (Zsucc n); auto with zarith. +replace ((1 + p) - Zsucc n) with (p - n); auto with zarith. +apply inj_eq_rev; auto with zarith. +rewrite inj_S; (repeat rewrite inj_Zabs_nat); auto with zarith. +(repeat rewrite Zabs_eq); auto with zarith. +Qed. + +Lemma Zsum_S_left: + forall (n m : Z) (f : Z -> Z), n < m -> Zsum n m f = f n + Zsum (n + 1) m f. +intros n m f H; rewrite (Zsum_split_up n n m f); auto with zarith. +rewrite Zsum_nn; auto with zarith. +Qed. + +Lemma Zsum_S_right: + forall (n m : Z) (f : Z -> Z), + n <= m -> Zsum n (m + 1) f = Zsum n m f + f (m + 1). +intros n m f H; rewrite (Zsum_split_up n m (m + 1) f); auto with zarith. +rewrite Zsum_nn; auto with zarith. +Qed. + +Lemma Zsum_split_down: + forall (n m p : Z) (f : Z -> Z), + ( p < m <= n ) -> Zsum n p f = Zsum n m f + Zsum (m - 1) p f. +intros n m p f [H H0]. +case (Zle_lt_or_eq p (m - 1)); auto with zarith; intros H1. +pattern m at 1; replace m with ((m - 1) + 1); auto with zarith. +repeat rewrite (Zsum_swap n). +rewrite (Zsum_swap (m - 1)). +rewrite Zplus_comm. +apply Zsum_split_up; auto with zarith. +subst p. +repeat rewrite (Zsum_swap n). +rewrite Zsum_nn. +unfold Zsum; (repeat rewrite Zle_imp_le_bool); auto with zarith. +replace (Zabs_nat ((1 + n) - (m - 1))) with (S (Zabs_nat (n - (m - 1)))). +rewrite Zplus_comm. +replace (Zabs_nat ((1 + n) - m)) with (Zabs_nat (n - (m - 1))); auto with zarith. +pattern m at 4; replace m with (Zsucc (m - 1)); auto with zarith. +apply f_equal with ( f := Zabs_nat ); auto with zarith. +apply inj_eq_rev; auto with zarith. +rewrite inj_S. +(repeat rewrite inj_Zabs_nat); auto with zarith. +(repeat rewrite Zabs_eq); auto with zarith. +Qed. + + +Lemma Zsum_ext: + forall (n m : Z) (f g : Z -> Z), + n <= m -> + (forall (x : Z), ( n <= x <= m ) -> f x = g x) -> Zsum n m f = Zsum n m g. +intros n m f g HH H. +unfold Zsum; auto. +unfold Zsum; (repeat rewrite Zle_imp_le_bool); auto with zarith. +apply iter_ext; auto with zarith. +intros a H1; apply H; auto; split. +apply Zprogression_le_init with ( 1 := H1 ). +cut (a < Zsucc m); auto with zarith. +replace (Zsucc m) with (n + Z_of_nat (Zabs_nat ((1 + m) - n))); auto with zarith. +apply Zprogression_le_end; auto with zarith. +rewrite inj_Zabs_nat; auto with zarith. +(repeat rewrite Zabs_eq); auto with zarith. +Qed. + +Lemma Zsum_add: + forall (n m : Z) (f g : Z -> Z), + Zsum n m f + Zsum n m g = Zsum n m (fun (i : Z) => f i + g i). +intros n m f g; unfold Zsum; case (Zle_bool n m); apply iter_comp; + auto with zarith. +Qed. + +Lemma Zsum_times: + forall n m x f, x * Zsum n m f = Zsum n m (fun i=> x * f i). +intros n m x f. +unfold Zsum. case (Zle_bool n m); intros; apply iter_comp_const with (k := (fun y : Z => x * y)); auto with zarith. +Qed. + +Lemma inv_Zsum: + forall (P : Z -> Prop) (n m : Z) (f : Z -> Z), + n <= m -> + P 0 -> + (forall (a b : Z), P a -> P b -> P (a + b)) -> + (forall (x : Z), ( n <= x <= m ) -> P (f x)) -> P (Zsum n m f). +intros P n m f HH H H0 H1. +unfold Zsum; rewrite Zle_imp_le_bool; auto with zarith; apply iter_inv; auto. +intros x H3; apply H1; auto; split. +apply Zprogression_le_init with ( 1 := H3 ). +cut (x < Zsucc m); auto with zarith. +replace (Zsucc m) with (n + Z_of_nat (Zabs_nat ((1 + m) - n))); auto with zarith. +apply Zprogression_le_end; auto with zarith. +rewrite inj_Zabs_nat; auto with zarith. +(repeat rewrite Zabs_eq); auto with zarith. +Qed. + + +Lemma Zsum_pred: + forall (n m : Z) (f : Z -> Z), + Zsum n m f = Zsum (n + 1) (m + 1) (fun (i : Z) => f (Zpred i)). +intros n m f. +unfold Zsum. +generalize (Zle_cases n m); generalize (Zle_cases (n + 1) (m + 1)); + case (Zle_bool n m); case (Zle_bool (n + 1) (m + 1)); auto with zarith. +replace ((1 + (m + 1)) - (n + 1)) with ((1 + m) - n); auto with zarith. +intros H1 H2; cut (exists c , c = Zabs_nat ((1 + m) - n) ). +intros [c H3]; rewrite <- H3. +generalize n; elim c; auto with zarith; clear H1 H2 H3 c n. +intros c H n; simpl; eq_tac; auto with zarith. +eq_tac; unfold Zpred; auto with zarith. +replace (Zsucc (n + 1)) with (Zsucc n + 1); auto with zarith. +exists (Zabs_nat ((1 + m) - n)); auto. +replace ((1 + (n + 1)) - (m + 1)) with ((1 + n) - m); auto with zarith. +intros H1 H2; cut (exists c , c = Zabs_nat ((1 + n) - m) ). +intros [c H3]; rewrite <- H3. +generalize n; elim c; auto with zarith; clear H1 H2 H3 c n. +intros c H n; simpl; (eq_tac; auto with zarith). +eq_tac; unfold Zpred; auto with zarith. +replace (Zpred (n + 1)) with (Zpred n + 1); auto with zarith. +unfold Zpred; auto with zarith. +exists (Zabs_nat ((1 + n) - m)); auto. +Qed. + +Theorem Zsum_c: + forall (c p q : Z), p <= q -> Zsum p q (fun x => c) = ((1 + q) - p) * c. +intros c p q Hq; unfold Zsum. +rewrite Zle_imp_le_bool; auto with zarith. +pattern ((1 + q) - p) at 2. + rewrite <- Zabs_eq; auto with zarith. + rewrite <- inj_Zabs_nat; auto with zarith. +cut (exists r , r = Zabs_nat ((1 + q) - p) ); + [intros [r H1]; rewrite <- H1 | exists (Zabs_nat ((1 + q) - p))]; auto. +generalize p; elim r; auto with zarith. +intros n H p0; replace (Z_of_nat (S n)) with (Z_of_nat n + 1); auto with zarith. +simpl; rewrite H; ring. +rewrite inj_S; auto with zarith. +Qed. + +Theorem Zsum_Zsum_f: + forall (i j k l : Z) (f : Z -> Z -> Z), + i <= j -> + k < l -> + Zsum i j (fun x => Zsum k (l + 1) (fun y => f x y)) = + Zsum i j (fun x => Zsum k l (fun y => f x y) + f x (l + 1)). +intros; apply Zsum_ext; intros; auto with zarith. +rewrite Zsum_S_right; auto with zarith. +Qed. + +Theorem Zsum_com: + forall (i j k l : Z) (f : Z -> Z -> Z), + Zsum i j (fun x => Zsum k l (fun y => f x y)) = + Zsum k l (fun y => Zsum i j (fun x => f x y)). +intros; unfold Zsum; case (Zle_bool i j); case (Zle_bool k l); apply iter_com; + auto with zarith. +Qed. + +Theorem Zsum_le: + forall (n m : Z) (f g : Z -> Z), + n <= m -> + (forall (x : Z), ( n <= x <= m ) -> (f x <= g x )) -> + (Zsum n m f <= Zsum n m g ). +intros n m f g Hl H. +unfold Zsum; rewrite Zle_imp_le_bool; auto with zarith. +unfold Zsum; + cut + (forall x, + In x (progression Zsucc n (Zabs_nat ((1 + m) - n))) -> ( f x <= g x )). +elim (progression Zsucc n (Zabs_nat ((1 + m) - n))); simpl; auto with zarith. +intros x H1; apply H; split. +apply Zprogression_le_init with ( 1 := H1 ); auto. +cut (x < m + 1); auto with zarith. +replace (m + 1) with (n + Z_of_nat (Zabs_nat ((1 + m) - n))); auto with zarith. +apply Zprogression_le_end; auto with zarith. +rewrite inj_Zabs_nat; auto with zarith. +rewrite Zabs_eq; auto with zarith. +Qed. + +Theorem iter_le: +forall (f g: Z -> Z) l, (forall a, In a l -> f a <= g a) -> + iter 0 f Zplus l <= iter 0 g Zplus l. +intros f g l; elim l; simpl; auto with zarith. +Qed. + +Theorem Zsum_lt: + forall n m f g, + (forall x, n <= x -> x <= m -> f x <= g x) -> + (exists x, n <= x /\ x <= m /\ f x < g x) -> + Zsum n m f < Zsum n m g. +intros n m f g H (d, (Hd1, (Hd2, Hd3))); unfold Zsum; rewrite Zle_imp_le_bool; auto with zarith. +cut (In d (progression Zsucc n (Zabs_nat (1 + m - n)))). +cut (forall x, In x (progression Zsucc n (Zabs_nat (1 + m - n)))-> f x <= g x). +elim (progression Zsucc n (Zabs_nat (1 + m - n))); simpl; auto with zarith. +intros a l Rec H0 [H1 | H1]; subst; auto. +apply Zle_lt_trans with (f d + iter 0 g Zplus l); auto with zarith. +apply Zplus_le_compat_l. +apply iter_le; auto. +apply Zlt_le_trans with (f a + iter 0 g Zplus l); auto with zarith. +intros x H1; apply H. +apply Zprogression_le_init with ( 1 := H1 ); auto. +cut (x < m + 1); auto with zarith. +replace (m + 1) with (n + Z_of_nat (Zabs_nat ((1 + m) - n))); auto with zarith. +apply Zprogression_le_end with ( 1 := H1 ); auto with arith. +rewrite inj_Zabs_nat; auto with zarith. +rewrite Zabs_eq; auto with zarith. +apply in_Zprogression. +rewrite inj_Zabs_nat; auto with zarith. +rewrite Zabs_eq; auto with zarith. +Qed. + +Theorem Zsum_minus: + forall n m f g, Zsum n m f - Zsum n m g = Zsum n m (fun x => f x - g x). +intros n m f g; apply trans_equal with (Zsum n m f + (-1) * Zsum n m g); auto with zarith. +rewrite Zsum_times; rewrite Zsum_add; auto with zarith. +Qed. |