proposition: Lemma filters_correct ps l : let ps1 := fold_left filters l ps in (forall i, In i (fst ps1) <-> In i (fst ps) \/ In i l) /\ (forall i, In i (snd ps1) <-> In i (snd ps) \/ (~In i (fst ps) /\ In i l)).
proof: Proof. revert ps; elim l; clear l; simpl; auto. - intros ps; split; intros i; split; auto. + intros [HH | HH]; auto; case HH. + intros [HH | HH]; auto; case HH; intros _ HH1; case HH1. - intros a l Hrec ps. case (Hrec (filters ps a)); intros H1 H2; split. + intros i; apply iff_trans with (1:= H1 i). unfold filter; case ps; simpl; intros s1 s2. generalize (in_states_correct a s1); case in_states; simpl; auto. * intros H5; split; intros [HH | HH]; auto. case HH; auto; intros; subst i; auto. * intros H5; split; intros [HH | HH]; auto. -- case HH; auto. -- case HH; auto. + intros i; apply iff_trans with (1:= H2 i). unfold filter; case ps; simpl; intros s1 s2. generalize (in_states_correct a s1); case in_states; simpl; auto. * intros H5; split; intros [HH | HH]; auto. -- case HH; auto. -- case HH; intros HH1 [HH2 | HH2]; auto. case HH1; rewrite <- HH2; auto. * intros H5; split; intros [HH | HH]; auto. -- case HH; auto; intros; subst i; auto. -- case HH; intros HH1 HH2; right; auto. -- generalize (state_eq_correct a i); case state_eq; auto; intros He. case HH; intros HH1 [HH2 | HH2]; auto. right; split; auto. intros [HH3 | HH3]; auto. Qed.
imports: ZArith List