proposition: Theorem update_primes_false_imp_prime : forall k l l1, 1 < k -> all_multiples l -> all_intervals k l -> all_prime_in_first k l -> update_primes k l = (l1,false) -> prime k.
proof: Proof. intros k l l1 Hkgt1 Ham Hai Hap Heq. elim (prime_dec k); auto. - intros Hkeq0or1;elim Hkeq0or1. + intros Hkeq0. rewrite Hkeq0 in Hkgt1; elim (Nat.nlt_0_r 1); assumption. + intros Hkeq1; rewrite Hkeq1 in Hkgt1; elim (Nat.lt_irrefl 1); assumption. - intros Hpdec; elim Hpdec. + intros Hexdiv. generalize (div_by_prime _ Hkgt1 Hexdiv). intros (p, ((Hpgt1,Hpltk), (Hpr, Hex))). elim (Hap p); auto. * intros l'1 (l2, (n, Heq')). elim Hex; intros q Heq''. assert (Hint: n - p < k <= n). { unfold all_intervals in Hai. apply Hai with l'1 l2. auto. } assert (Hmult : (exists q':nat, n = p*q')). { unfold all_multiples in Ham. apply Ham with l'1 l2. auto. } elim Hmult; intros q' Heq3. assert (Heq4: q=q'). { apply interval_eq with p. rewrite <- Heq3. rewrite <- Heq''. assumption. } assert (false= true). { case_eq (update_primes k ((p,n)::l2)). intros l3 b Hup. generalize (update_primes_true_aux k ((p,n)::l2) l3 l'1 l1 false). intros H; apply H. - generalize Hup. simpl. case (update_primes k l2). intros l5 b2. rewrite Heq''; rewrite Heq3; rewrite Heq4. rewrite Nat.compare_refl. intros Heq5; injection Heq5; intros Heq6 Heq7; rewrite Heq6;rewrite Heq7; auto with arith. - rewrite <- Heq'. assumption. } discriminate. * auto with arith. + trivial. Qed.
imports: List Arith