proposition: Theorem prime_fun_complete : forall k, prime k -> prime_fun k = true.
proof: Proof. intros k; case k. - intros ((Hneq0, Hneq1),Hnex); elim Hneq0; auto. - intros k'; case k'. + intros ((Hneq0, Hneq1),Hnex); elim Hneq1; auto. + intros k'' ((_,_),Hnex); unfold prime_fun. assert (Hps: prime_sieve (S (S k'')) = 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')). { auto. } rewrite Hps. case_eq (update_primes (S (S k'')) (prime_sieve (S k''))). intros l' b; case b; intros Hup. * elim Hnex. unfold divides. generalize (prime_sieve_invariant k'' (prime_sieve (S k''))); intros Hinv. apply (update_primes_true_imp_div (S (S k'')) (prime_sieve (S k''))) with l'; intuition. * rewrite (Nat.compare_refl (S (S k''))); auto. Qed.
imports: List Arith