proposition: Theorem prime_sieve_invariant : forall k l, prime_sieve (S k)=l -> all_first_less_than (S (S k)) l /\ all_first_prime l /\ all_prime_in_first (S (S k)) l /\ all_intervals (S (S k)) l /\ all_multiples l /\ all_greater_than_one l.
proof: Proof. intros k; elim k. - simpl; intros l Hl; rewrite <- Hl; clear Hl l. split;[idtac | split; [idtac | split;[idtac|split;[idtac|split]]]]; try (intros l1 l2 p n Heq; elim (absurd_decompose_list _ _ _ _ Heq)). intros n Hle1 ((Hnneq0, Hnneq1),_); elim Hnneq1. elim Hle1; intros; apply (Nat.le_antisymm n 1); auto with arith. - intros k' Hrec l Hps. change ((let (l', b) := update_primes (S (S k')) (prime_sieve (S k')) in if b then l' else (S (S k'), 2*S (S k'))::l') = l) in Hps. case_eq (update_primes (S (S k')) (prime_sieve (S k'))); intros l' b Heq. generalize (Hrec (prime_sieve (S k'))); intros Hrec'. assert (Hal: all_first_less_than (S (S k')) l'). { apply update_primes_all_first_less_than with (prime_sieve (S k')) b; auto. intuition. } assert (Hafp: all_first_prime l'). { apply update_primes_all_first_prime with (S (S k')) (prime_sieve (S k')) b; auto. intuition. } assert (Hapf: all_prime_in_first (S (S k')) l'). { apply update_primes_all_prime_in_first with (prime_sieve (S k')) b; auto. intuition. } assert (Hai : all_intervals (S (S (S k'))) l'). { apply update_primes_all_intervals with (prime_sieve (S k')) b; auto. intuition. intuition. } assert (Ham : all_multiples l'). { apply update_primes_all_multiples with (S (S k')) (prime_sieve (S k')) b; auto. intuition. } assert (Ha1 : all_greater_than_one l'). { apply update_primes_all_greater_than_one with (S (S k')) (prime_sieve (S k')) b; auto. intuition. } case_eq b; intros Heqb; rewrite Heqb in Heq; rewrite Heq in Hps. + rewrite <- Hps. split;[idtac|split;[idtac|split;[idtac|split;[idtac|split;[idtac|idtac]]]]]; auto. * apply all_first_less_than_S; assumption. * unfold all_prime_in_first. intros n Hint Hpr; unfold all_prime_in_first in Hapf; apply Hapf; auto. split. -- intuition. -- elim Hint. intros Hngt0 Hnlek. elim (proj1 (Nat.lt_eq_cases _ _) Hnlek). ++ auto with arith; fail. ++ intros Hn'; injection Hn'. intros Hn; rewrite Hn in Hpr; elim Hpr. intros _ Hnex; elim Hnex. unfold divides. apply update_primes_true_imp_div with (prime_sieve (S k')) l'. ** intuition. ** intuition. ** intuition. ** auto. + split. * intros l1; case l1. -- simpl; intros l2 p n; rewrite <- Hps; intros Heq2;injection Heq2. intros Hl2 Hn Hp; rewrite <- Hp; auto with arith. -- intros fst_elem l'1 l2 p n; simpl; rewrite <- Hps; intros Heq2; injection Heq2; intros Hl' Hfst_elem. assert (Hal' : all_first_less_than (S (S (S k'))) l'). { apply all_first_less_than_S; auto. } apply (Hal' l'1 l2 p n); auto. * split. -- rewrite <- Hps; apply all_first_prime_add; auto. apply update_primes_false_imp_prime with (prime_sieve (S k')) l'; try tauto. auto with arith. -- split. ++ rewrite <- Hps. intros n (Hpos, Hle) Hpr. elim (proj1 (Nat.lt_eq_cases _ _) Hle). ** intros Hlt; elim (Hapf n); auto with arith. intros l'1 (l'2, (p, Heq2)); exists ((S (S k'), 2*S(S k'))::l'1); exists l'2; exists p. rewrite Heq2;reflexivity. ** intros Hn'; injection Hn'; intros Hn. exists (nil (A:=nat*nat)); exists l'; exists (2*S (S k')). rewrite Hn;reflexivity. ++ split. ** rewrite <- Hps; apply all_intervals_add; auto with arith. split. { simpl. rewrite Nat.add_comm. rewrite Nat.add_sub. rewrite <- plus_n_O. auto with arith. } { simpl. repeat rewrite <- plus_n_Sm. auto with arith. } ** split. { rewrite <- Hps; apply all_multiples_add; auto with arith. exists 2; rewrite (Nat.mul_comm 2); reflexivity. } rewrite <- Hps. apply all_greater_than_one_add; auto with arith. Qed.
imports: List Arith