proposition: Theorem update_primes_all_list_invariant : forall (P:nat->nat->nat->Prop), (forall k p n:nat, k = n -> P k p n -> P k p (n+p))-> (forall k p n:nat, n < k -> P k p n -> P k p (n+p))-> forall (k:nat)(l l':list(nat*nat))(b:bool), all_list (P k) l -> update_primes k l = (l',b) -> all_list (P k) l'.
proof: Proof. intros P Hp2 Hp3 k l; elim l. - simpl; intros Hal l' b Hup; injection Hup; intros Hb Hl'; rewrite <- Hl'; apply (all_list_nil (P k)). - simpl; intros (p, n) l0 Hrec l' b Hal; case_eq (update_primes k l0); intros l'0 b0 Hup0. case_eq (Nat.compare k n); intros Htwc Hup; injection Hup; intros Hb Hl'; rewrite <- Hl'; generalize (Hal nil l0 p n (refl_equal _)); intros HPkpn; generalize (Hrec l'0 b0 (all_list_transmit (P k) (p,n) l0 Hal) Hup0); intros Hal'; apply all_list_add; auto. + apply Hp2;[apply nat_compare_eq;auto| auto]. + apply Hp3;[apply nat_compare_Gt_gt;auto| auto]. Qed.
imports: List Arith