Require Import ZArith. Require Import List. Require Import util. Require Import machine_int. Import MachineInt. Require Import machine_int_spec. Open Local Scope Z_scope. (*****************************************************************************) (* sum predicates *) (*****************************************************************************) (* sum up the list member up to the kth element included (starting with 0) *) Fixpoint sum_k (l:nat) (k:nat) (lst:list (int l)) {struct lst} : Z := match lst with nil => 0 | hd::tl => match k with O => u2Z hd | S k' => u2Z hd + 2^^l * sum_k l k' tl end end. Implicit Arguments sum_k. Lemma sum_k_0 : forall (l:nat) hd (tl:list (int l)), sum_k 0 (hd::tl) = u2Z hd. auto. Qed. Lemma sum_k_nil : forall (l:nat) n, sum_k n (@nil (int l)) = 0. auto. Qed. Lemma sum_k_S : forall n (l:nat) (hd:int l) tl, sum_k (S n) (hd :: tl) = u2Z hd + 2^^l * sum_k n tl. intros. simpl. auto. Qed. (* sum up the first k list member (with k>=1) *) Definition Sum l k (lst: list (int l)) : Z := match k with O => 0 | S k' => sum_k k' lst end. Implicit Arguments Sum. Lemma Sum_nil : forall l x, Sum x (@nil (int l)) = 0. intros. destruct x; auto. Qed. Lemma Sum_S : forall l x (hd:int l) tl, Sum (S x) (hd::tl) = u2Z hd + Zpower 2 l * Sum x tl. intros. unfold Sum at 1. destruct x. rewrite sum_k_0. simpl. ring. rewrite sum_k_S. unfold Sum. ring. Qed. Lemma Sum_pos : forall l (lst:list (int l)) n, 0 <= Sum n lst. induction lst; intro. rewrite Sum_nil. apply Zle_refl. destruct n. simpl. apply Zle_refl. rewrite Sum_S. apply Zplus_le_0_compat. apply min_u2Z. apply Zmult_le_0_compat. apply Zle_trans with 1. omega. apply Zpower_1. apply IHlst. Qed. (**** beta * (a_0 ... a_{k-1}) = (0 a_0...a_{k-1}) ****) Lemma Sum_beta_0 : forall n lst, length lst = n -> Zbeta 1 * Sum n lst = Sum (S n) (zero32::lst). intros. destruct n. simpl. unfold zero32. rewrite Z2u_injection. auto. generalize (Zpower_1 32); omega. unfold Sum. rewrite sum_k_S. rewrite <-Zbeta_power1. unfold zero32. rewrite Z2u_injection. auto. generalize (Zpower_1 32); omega. Qed. (**** (0 a_0 ... a_{k-1}) + z = (z a_0 ... a_{k-1}) ****) Lemma Sum_0 : forall n lst, length lst = n -> forall z, Sum (S n) (zero32::lst) + u2Z z = Sum (S n) (z::lst). intros. unfold Sum. destruct n. simpl. unfold zero32. rewrite Z2u_injection. omega. generalize (Zpower_1 32); omega. rewrite sum_k_S. rewrite sum_k_S. unfold zero32. rewrite Z2u_injection. omega. generalize (Zpower_1 32); omega. Qed. Lemma Sum_0_swap : forall l k hd hd' (tl:list (int l)), (k > 0)%nat -> Sum k (hd::tl) + u2Z hd' = Sum k (hd'::tl) + u2Z hd. intros. destruct k. inversion H. unfold Sum. destruct k. simpl. ring. rewrite sum_k_S. rewrite sum_k_S. ring. Qed. Lemma Sum_1 : forall lst, Sum 1 lst = u2Z (nth 0 lst zero32). intros. destruct lst. simpl. unfold zero32. rewrite Z2u_injection. auto. generalize (Zpower_1 32); omega. simpl. auto. Qed. Lemma nth_nil : forall (A:Set) n a, nth n (@nil A) a = a. intros. simpl. destruct n; auto. Qed. Lemma Sum_remove_last' : forall n l (lst:list (int l)) x, length lst = n -> Sum (S x) lst = Sum x lst + Zpower 2 (x * l) * u2Z (nth x lst (Z2u l 0)). induction n. intros. destruct lst; try discriminate. rewrite Sum_nil. rewrite Sum_nil. rewrite nth_nil. rewrite Z2u_injection. ring. generalize (Zpower_1 l); omega. intros. destruct lst; try discriminate. simpl in H; injection H; clear H; intro. rewrite Sum_S. destruct x. unfold Sum. simpl nth. simpl Zpower. ring. rewrite Sum_S. rewrite IHn. simpl u2Z. ring. rewrite <-Zpower_is_exp. cutrewrite (l+x*l = S x*l)%nat. auto. rewrite S_to_plus_one. rewrite mult_plus_distr_r. omega. auto. Qed. Lemma Sum_remove_last : forall l (lst:list (int l)) x, Sum (S x) lst = Sum x lst + Zpower 2 (x * l) * u2Z (nth x lst (Z2u l 0)). intros. apply Sum_remove_last' with (length lst). auto. Qed. Lemma Sum_remove_last_32 : forall lst n, Sum n lst + u2Z (nth n lst zero32) * Zbeta n = Sum (S n) lst. intros. rewrite Sum_remove_last. unfold Zbeta. unfold zero32. ring. Qed. Lemma Sum_remove_first : forall hd (tl:list (int 32)) n, Sum (S n) (hd::tl) = u2Z hd + Zbeta 1 * Sum n tl. intros. unfold Sum. destruct n. unfold sum_k. ring. unfold sum_k. rewrite <-Zbeta_power1. ring. Qed. (*Definition sum l (lst:list (int l)) : nat := sum_k (pred (length lst)) lst. Implicit Arguments sum.*) Lemma Sum_cut : forall k1 (lst1:list (int 32)), length lst1 = k1 -> forall k (lst:list (int 32)) lst2, length lst = k -> lst = lst1 ++ lst2 -> Sum k (lst1 ++ lst2) = Sum k1 lst1 + Zbeta k1 * Sum (k-k1) lst2. induction k1. intros. destruct lst1; try discriminate. rewrite <-minus_n_O. simpl app. rewrite Sum_nil. unfold Zbeta. simpl Zpower. ring. intros. destruct lst1; try discriminate. simpl in H; injection H; clear H; intro. destruct k. destruct lst; try discriminate. simpl in H1. destruct lst; try discriminate. simpl in H0; injection H0; clear H0; intro. injection H1; clear H1; intros; subst i0. generalize (IHk1 _ H _ _ _ H0 H1); intro. rewrite Sum_S. cutrewrite ( ((i :: lst1) ++ lst2) = i :: (lst1 ++ lst2) ). rewrite Sum_S. rewrite (IHk1 lst1 H k lst lst2). simpl (S k - S k1)%nat. rewrite Zmult_plus_distr_r. rewrite <-Zbeta_power1. rewrite Zmult_assoc. rewrite <-Zbeta_is_exp. cutrewrite (1+k1=S k1)%nat. ring. ring. auto. auto. auto. Qed. Lemma Sum_beyond : forall n l (lst:list (int l)), length lst = n -> forall lst', Sum n lst = Sum n (lst++lst'). induction n. intros. destruct lst; try discriminate. auto. intros. destruct lst; try discriminate. simpl in H; injection H; clear H; intro. rewrite Sum_S. cutrewrite ((i :: lst) ++ lst' = i::(lst++lst')). rewrite Sum_S. rewrite (IHn l lst H lst'). auto. auto. Qed. Lemma Sum_beyond2 : forall (l:nat) (k:nat) (lst:list (int l)), length lst = k -> forall n, Sum (k+n) lst = Sum k lst. induction k. intros. destruct lst; try discriminate. simpl. rewrite Sum_nil. auto. intros. destruct lst; try discriminate. simpl in H; injection H; clear H; intro. rewrite Sum_S. cutrewrite (S k + n = S (k+n))%nat. rewrite Sum_S. rewrite IHk. ring. auto. omega. Qed. Lemma Sum_update_list : forall n (lst:list (int 32)) k m, length lst = n -> Sum k lst = Sum k (update_list lst k m). induction n. intros. destruct lst; try discriminate. auto. intros. destruct lst; try discriminate. simpl in H; injection H; clear H; intro. destruct k. auto. simpl update_list. rewrite Sum_remove_first. rewrite Sum_remove_first. rewrite (IHn lst k m H). auto. Qed. Lemma Sum_cut_last : forall k (lst1:list (int 32)) last, (k > 0)%nat -> length (lst1 ++ last::nil) = k -> Sum k (lst1 ++ last::nil) = Sum (k-1)%nat lst1 + Zbeta (k-1)%nat * u2Z last. intros. assert (length lst1 = k-1)%nat. rewrite length_app in H0. simpl in H0. omega. rewrite (Sum_cut (k-1) lst1 H1 k (lst1++last::nil)). cutrewrite (k-(k-1)=1)%nat. simpl. reflexivity. omega. auto. auto. Qed. Lemma Sum_cut_last_beyond : forall k (lst:list (int 32)), (k > 0)%nat -> length lst = k -> Sum k lst = Sum (k-1)%nat lst + Zbeta (k-1)%nat * u2Z (nth (k-1)%nat lst zero32). intros. generalize (list_last' _ _ _ zero32 H0 H); intro X; inversion_clear X. rewrite H1 in H0; rewrite length_app in H0; simpl in H0. assert ( Sum (k - 1)%nat (x ++ (nth (k-1)%nat lst zero32) :: nil) = Sum (k - 1)%nat x ). rewrite <-Sum_beyond. auto. omega. rewrite H1. rewrite Sum_cut_last. rewrite nth_app. cutrewrite (k-1-length x=0)%nat. simpl. auto. omega. omega. omega. auto. rewrite length_app; simpl; omega. Qed. Lemma Sum_update_list2 : forall n (lst:list (int 32)) k z, length lst = n -> (k < n)%nat -> Sum n lst - u2Z (nth k lst zero32) * Zbeta k + u2Z z * Zbeta k = Sum n (update_list lst k z). induction n. intros. inversion H0. intros. destruct lst; try discriminate. simpl in H; injection H; clear H; intro. destruct k. simpl nth. simpl update_list. unfold Zbeta. simpl Zpower. repeat rewrite Zmult_1_r. do 2 rewrite Sum_S. ring. assert (k Sum_hole k (k-1)%nat lst = Sum (k-1)%nat lst. intros. unfold Sum_hole. destruct k. destruct lst; try discriminate. auto. assert (length lst > 0)%nat. omega. generalize (list_last _ lst H0); intro X; inversion_clear X. inversion_clear H1. generalize (del_nth_last_exact' _ x x0); intro. assert (length x = k). rewrite H2 in H; rewrite length_app in H; simpl in H; omega. rewrite H3 in H1. rewrite <-H2 in H1. pattern lst at 2. rewrite H2. rewrite <-Sum_beyond. cutrewrite (S k - 1 = k)%nat. rewrite H1. auto. omega. omega. Qed. Lemma Sum_hole_last' : forall (lst:list (int 32)) (k:nat), length lst = k -> Sum_hole k 0 lst = Sum (k-1)%nat (List.tail lst). destruct lst. intros. simpl in H. subst k. simpl. unfold Sum_hole. simpl. auto. intros. simpl. destruct k; try discriminate. simpl. rewrite <-minus_n_O. simpl in H; injection H; clear H; intros. unfold Sum_hole. simpl. rewrite <-minus_n_O. auto. Qed. Lemma Sum_hole_shift : forall (k:nat) (lst:list (int 32)), length lst = k -> forall (j:nat), (j < k)%nat -> Sum_hole k j lst + u2Z (nth j lst zero32) * Zbeta (j-1)%nat = Sum_hole k (j-1)%nat lst + u2Z (nth (j-1)%nat lst zero32) * Zbeta (j-1)%nat. induction k. intros. destruct lst; try discriminate. destruct j. auto. inversion H0. intros. destruct j. simpl. auto. generalize (list_split' _ (S k) lst zero32 H (gt_Sn_O k) _ H0); intro X; inversion_clear X as [lst1]. inversion_clear H1. inversion_clear H3 as [lst2]. unfold Sum_hole. simpl. rewrite <-minus_n_O. rewrite <-minus_n_O. pattern lst at 1. rewrite H1. assert ( (del_nth (S j) (lst1 ++ nth (S j) lst zero32 :: nil ++ lst2)) = lst1 ++ lst2 ). rewrite <-H1. apply del_nth_app with (nth (S j) lst zero32). auto. auto. rewrite H3. assert (length lst1 > 0)%nat. omega. assert (j < S j)%nat. omega. generalize (list_split' _ (S j) lst1 zero32 H2 (gt_Sn_O j) _ H5); intro X; inversion_clear X as [lst1']. inversion_clear H6. inversion_clear H8 as [lst3]. destruct lst3. rewrite H6 in H1. simpl in H1. rewrite app_ass in H1. simpl in H1. assert ( del_nth j (lst1' ++ nth j lst1 zero32 :: nil ++ (nth (S j) lst zero32) :: lst2) = lst1' ++ (nth (S j) lst zero32) :: lst2 ) . simpl. rewrite <-H1. apply del_nth_app with (nth j lst1 zero32). auto. auto. simpl in H8. rewrite <-H1 in H8. rewrite H8. rewrite H6. simpl. rewrite app_ass. simpl. assert ( length (lst1' ++ nth j lst1 zero32 :: lst2) = k). rewrite length_app. simpl. rewrite H1 in H. rewrite length_app in H. simpl in H. omega. pattern k at 1. rewrite <-H9. rewrite (Sum_cut _ _ H7 (length (lst1'++ nth j lst1 zero32 ::lst2)) (lst1'++ nth j lst1 zero32 ::lst2) (nth j lst1 zero32 ::lst2)); auto. rewrite H9. assert ( length (lst1' ++ nth (S j) lst zero32 :: lst2) = k). rewrite length_app. simpl. rewrite H1 in H. rewrite length_app in H. simpl in H. omega. pattern k at 2. rewrite <-H10. rewrite (Sum_cut _ _ H7 (length (lst1'++ nth (S j) lst zero32 ::lst2)) (lst1'++ nth (S j) lst zero32 ::lst2) (nth (S j) lst zero32 ::lst2)); auto. rewrite H10. cut ( Sum (k - j) (nth j lst1 zero32 :: lst2) + u2Z (nth (S j) lst zero32) = Sum (k - j) (nth (S j) lst zero32 :: lst2) + u2Z (nth j lst1 zero32) ). intro. rewrite (Zmult_comm (Zbeta j)). rewrite <-Zplus_assoc. rewrite <-Zmult_plus_distr_l. rewrite H11. ring. assert (nth j lst1 zero32 = nth j lst zero32). rewrite H1. simpl in H6. cutrewrite ( lst1' ++ nth j lst1 zero32 :: nth (S j) lst zero32 :: lst2 = (lst1' ++ nth j lst1 zero32 :: nil) ++ nth (S j) lst zero32 :: lst2 ). rewrite <-H6. rewrite <-nth_beyond. auto. omega. rewrite app_ass. auto. rewrite H12. auto. apply (Sum_0_swap 32). omega. rewrite H6 in H2. rewrite length_app in H2. simpl in H2. rewrite H7 in H2. assert (forall x y, x + S (S y) <> S x)%nat. intros. omega. generalize (H8 j (length lst3)); intro. tauto. Qed. Lemma Sum_hole_update_list : forall n (lst:list (int 32)) k m, length lst = n -> Sum_hole n k lst = Sum_hole n k (update_list lst k m). intros. unfold Sum_hole. rewrite del_nth_update_list. auto. Qed. (* * list of zeros *) Fixpoint list_of_nzeros (n:nat) : list (int 32) := match n with O => nil | S n' => zero32 :: list_of_nzeros n' end. Lemma list_of_nzeros_length: forall n, length (list_of_nzeros n) = n. induction n; simpl; auto. Qed. Definition list_of_zeros (l:list (int 32)) : Prop := l = list_of_nzeros (length l). Lemma list_of_zeros_app: forall l1 l2, list_of_zeros l1 -> list_of_zeros l2 -> list_of_zeros (l1 ++ l2). induction l1; auto. unfold list_of_zeros. unfold list_of_zeros in IHl1. intros. simpl in H. injection H; clear H; intros; subst a. rewrite <- app_comm_cons; auto. rewrite IHl1; auto. simpl. rewrite list_of_nzeros_length; auto. Qed. Lemma Sum_list_of_zeros: forall l k, list_of_zeros l -> Sum k l = 0. induction l. destruct k; auto. destruct k; auto. simpl; intros. red in H. simpl in H. injection H; clear H; intros; subst a. unfold zero32. rewrite Z2u_injection. unfold Sum in IHl. unfold list_of_zeros in IHl. generalize (IHl k H); intros. destruct k; auto. rewrite H0. omega. generalize (Zpower_1 32); omega. Qed.