proposition: Lemma fold_nexts_correct ps ss : (forall s, In s (fst (fold_left nexts (snd ps) (fst ps, ss))) <-> In s (fst ps) \/ (exists f, exists i, In f movel /\ In i (snd ps) /\ s = f i /\ ~ In (f i) (fst ps))) /\ (forall s, In s (snd (fold_left nexts (snd ps) (fst ps, ss))) <-> In s ss \/ (exists f, exists i, In f movel /\ In i (snd ps) /\ s = f i /\ ~ In (f i) (fst ps))).
proof: Proof. destruct ps as (ss1, ss2); simpl fst; simpl snd. generalize ss1 ss; elim ss2; clear ss ss1 ss2; auto. - unfold fold_left, fst, snd. intros ss1 ss; split; intros ; split; auto; intros [H1 | H1]; auto; case H1; intros f (i, (_, (HH, _))); case HH. - intros s1 ss2 Hrec ss1 ss. rewrite fold_left_cons. generalize (nexts_correct (ss1, ss) s1); case nexts; simpl fst; simpl snd; intros ss3 ss4 (Hss3, Hss4). assert (tmp: forall A B:Prop, A -> (A -> B) -> A /\ B); auto. + apply tmp; clear tmp. * intros s; case (Hrec ss3 ss4); intros Hr1 Hr2; clear Hrec. apply iff_trans with (1 := Hr1 s). split; intros [H1 | H1]. -- rewrite Hss3 in H1; case H1; auto. intros (f, (Hf1, (Hf2, Hf3))); subst s; right; exists f; exists s1; auto with datatypes. -- case H1; intros f (i, (Hf1, (Hf2, (Hf3, Hf4)))); subst s; right; exists f; exists i; repeat split; auto with datatypes. intros H2; case Hf4. unfold lequiv in Hss3; rewrite Hss3; auto. -- left; unfold lequiv in Hss3; rewrite Hss3; auto. -- case H1; intros f (i, (Hf1, (Hf2, (Hf3, Hf4)))). simpl in Hf2; case Hf2; clear Hf2; intros Hf2. ++ subst; left; unfold lequiv in Hss3; rewrite Hss3; auto. right; exists f; auto. ++ generalize (in_states_correct s ss3); case in_states; auto; intros H3. right; exists f; exists i; repeat split; auto with datatypes. rewrite <- Hf3; auto. * intros Hl s; case (Hrec ss3 ss4); intros Hr1 Hr2; clear Hrec. apply iff_trans with (1 := Hr2 s); clear Hr2. split; intros [H1 | H1]. -- rewrite Hss4 in H1; case H1; auto. intros (f, (Hf1, (Hf2, Hf3))); subst s; right; exists f; exists s1; auto with datatypes. -- case H1; intros f (i, (Hf1, (Hf2, (Hf3, Hf4)))); subst s; right; exists f; exists i; repeat split; auto with datatypes. intros H2; case Hf4. unfold lequiv in Hss3; rewrite Hss3; auto. -- left; unfold lequiv in Hss4; rewrite Hss4; auto. -- match type of H1 with ?X => assert (F1: In s ss1 \/ X); auto end. rewrite <- Hl, Hr1 in F1; clear Hl Hr1. case F1; auto; clear F1; intros F1. case H1; intros f (i, (Hf1, (Hf2, (Hf3, Hf4)))); clear H1; subst s. rewrite Hss3 in F1; case F1; clear F1; intros F1. ++ case Hf4; auto. ++ left; rewrite Hss4; auto. Qed.
imports: ZArith List