proposition: Lemma filter2s_correct p ps l : let ps1 := fold_left (filter2s p) l ps in (forall i, In i (fst (fst ps1)) <-> In i (fst (fst ps)) \/ (~In i (snd (fst ps)) /\ In i l /\ is_odd p)) /\ (forall i, In i (snd (fst ps1)) <-> In i (snd (fst ps)) \/ (~In i (fst (fst ps)) /\ In i l /\ p <> 1%positive)) /\ (forall i, In i (snd ps1) <-> In i (snd ps) \/ (~In i (fst (fst ps)) /\ ~In i (snd (fst ps)) /\ In i l)).
proof: Proof. revert ps; elim l; clear l; simpl; auto. - intros ps; split; [idtac | split]; intros i; split; auto. + intros [HH | (_, (HH, _))]; auto; case HH. + intros [HH | (_, (HH, _))]; auto; case HH. + intros [HH | (_, (_, HH))]; auto; case HH. - intros a l Hrec ps. case (Hrec (filter2s p ps a)); intros H1 (H2, H3); split; [idtac | idtac]. + intros i; apply iff_trans with (1 := H1 i). unfold filter2s; case ps; simpl; intros ps1; case ps1; intros s1 s2 s3; clear ps ps1 H1 H2 H3. generalize (in_states_correct a s1); case in_states; simpl; auto. * intros H5; split. -- intros [HH | (HH, (HH1, HH2))]; auto. -- intros [HH | (HH, ([HH1 | HH1], HH2))]; subst; auto. * intros Ha. generalize (in_states_correct a s2); case in_states; simpl; auto. -- intros Hb; split. ++ intros [HH | (HH, (HH1, HH2))]; auto. ++ intros [HH | (HH, ([HH1 | HH1], HH2))]; subst; auto. case HH; auto. -- intros Hb; case p; simpl. ++ intros _; split. ** intros [[HH | HH]| (HH, (HH1, _))]; subst; auto. right; auto. ** intros [HH | (HH, ([HH1 | HH1], _))]; subst; auto. generalize (state_eq_correct a i); case state_eq; auto. intros HH2; right; auto; split; auto. intros [HH3 | HH3]; subst; auto. ++ intros _; split. ** intros [HH | (_, (_, HH))]; auto; case HH. ** intros [HH | (_, (_, HH))]; auto; case HH. ++ split. ** intros [[HH | HH] | (HH, (HH1, _))]; subst; auto. ** intros [HH | (HH, ([HH1 | HH1], _))]; auto. + split. * intros i; apply iff_trans with (1:= H2 i). unfold filter2s; case ps; simpl; intros ps1; case ps1; intros s1 s2 s3; clear ps ps1 H1 H2 H3. generalize (in_states_correct a s1); case in_states; simpl; auto. -- intros H5; split. ++ intros [HH | (HH, (HH1, HH2))]; auto. ++ intros [HH | (HH, ([HH1 | HH1], HH2))]; subst; auto. case HH; auto. -- intros Ha. generalize (in_states_correct a s2); case in_states; simpl; auto. ++ intros Hb; split. ** intros [HH | (HH, (HH1, HH2))]; auto. ** intros [HH | (HH, ([HH1 | HH1], HH2))]; subst; auto. ++ intros Hb; case p; simpl. ** intros p1; split. --- intros [[HH | HH]| (HH, (HH1, _))]; subst; auto. +++ right; repeat (split; auto); intros HH; discriminate. +++ right; split; auto; split; auto; intros HH2; discriminate. --- intros [HH | (HH, ([HH1 | HH1], _))]; subst; auto. generalize (state_eq_correct a i); case state_eq; auto. intros HH2; right; auto; split; auto. +++ intros [HH3 | HH3]; subst; auto. +++ split; auto; intros HH3; discriminate. ** intros p1; split. --- intros [[HH | HH] | (HH, (HH1, _))]; subst; auto. +++ right; repeat (split; auto); intros HH; discriminate. +++ right; split; auto; split; auto; intros HH2; discriminate. --- intros [HH | (HH, ([HH1 | HH1], _))]; auto. right; repeat (split; auto); intros HH2; discriminate. ** split. --- intros [HH | (_, (_, HH))]; auto; case HH; auto. --- intros [HH | (_, (_, HH))]; auto; case HH; auto. * intros i; apply iff_trans with (1:= H3 i). unfold filter2s; case ps; simpl; intros ps1; case ps1; intros s1 s2 s3; clear ps ps1 H1 H2 H3. generalize (in_states_correct a s1); case in_states; simpl; auto. -- intros H5; split. ++ intros [HH | (HH, (HH1, HH2))]; auto. ++ intros [HH | (HH, (HH1, [HH2 | HH2]))]; subst; auto; case HH; auto. -- intros Ha. generalize (in_states_correct a s2); case in_states; simpl; auto. ++ intros Hb; split. ** intros [HH | (HH, (HH1, HH2))]; auto. ** intros [HH | (HH, (HH1, [HH2 | HH2]))]; subst; auto; case HH1; auto. ++ intros Hb; case p; simpl. ** intros _; split. --- intros [[HH | HH]| (HH, (HH1, HH2))]; subst; auto. right; repeat split; auto. --- intros [HH | (HH, (HH1, [HH2 | HH2]))]; auto. generalize (state_eq_correct a i); case state_eq; auto. intros HH3; right; repeat split; auto. +++ intros [HH4 | HH4]; subst; auto. +++ intros [HH4 | HH4]; subst; auto. ** intros _; split. --- intros [[HH | HH]| (HH, (HH1, HH2))]; subst; auto. right; repeat split; auto. --- intros [HH | (HH, (HH1, [HH2 | HH2]))]; auto. generalize (state_eq_correct a i); case state_eq; auto. intros HH3; right; repeat split; auto. intros [HH4 | HH4]; subst; auto. ** split. --- intros [[HH | HH]| (HH, (HH1, HH2))]; subst; auto. right; repeat split; auto. --- intros [HH | (HH, (HH1, [HH2 | HH2]))]; auto. generalize (state_eq_correct a i); case state_eq; auto. intros HH3; right; repeat split; auto. intros [HH4 | HH4]; subst; auto. Qed.
imports: ZArith List