proposition: Lemma fold_nexts_nreach n ps : (forall s, In s (fst ps) <-> nlreachable n s) /\ (forall s, (nsreachable n s -> In s (snd ps)) /\ (In s (snd ps) -> nlreachable n s)) -> (forall s, In s (fst (fold_left nexts (snd ps) (fst ps,nil))) <-> nlreachable (S n) s) /\ (forall s, (nsreachable (S n) s -> In s (snd (fold_left nexts (snd ps) (fst ps,nil)))) /\ (In s (snd (fold_left nexts (snd ps) (fst ps,nil))) -> nlreachable (S n) s)).
proof: Proof. destruct ps as (ss1, ss2). unfold nexts. rewrite fold_left_comb with (f := fun (y: state) (y1: state -> state) => y1 y) (g := filters). match goal with |- context[fold_right ?X ?Y ?Z] => change (fold_right X Y Z) with (candidate_list Z) end; fold filters. simpl fst; simpl snd. intros (H1, H2); generalize (filters_correct (ss1, nil) (candidate_list ss2)); case (fold_left filters (candidate_list ss2) (ss1, nil)). intros ss4 ss5; simpl; intros (H3, H4). assert (tmp: forall (A B: Prop), A -> (A -> B) -> A /\ B); auto. apply tmp; clear tmp. - intros s; apply iff_trans with (1:= H3 s). split. + intros [H5 | H5]. * case (H1 s); intros HH _. case (HH H5); intros m (Hm1, Hm2). exists m; auto with arith. * assert (H6 := candidate_list_correct ss2 n). case (fun x => H6 x s); auto. + assert (H6 := candidate_list_correct ss2 n). intros H7. case (nlreachable_bound _ _ H7); intros m (Hm, Hm1). apply Nat.le_lteq in Hm; destruct Hm as [Hm2|Hm2]. -- left. assert (nlreachable n s). apply nlreach_weak with m; auto with arith. exists m; split; auto; case Hm1; auto. case (H1 s); auto. -- subst m; case (fun x => H6 x s); auto. - intros H5 s; split; intros H6. + assert (F0 : In s ss4). case (H5 s); auto. intros _ H7; apply H7; clear H7. exists (S n); split; auto; case H6; auto. assert (F1: ~ In s ss1). intros H7; case (H1 s); intros H8 _; clear H1. generalize (H8 H7); clear H8 H7; intros H7. case H7; intros m (Hm1, Hm2); clear H7. case H6; intros _ H7. case (H7 m); auto with arith. case (H4 s); intros _ HH; apply HH; clear HH H4; auto. right; split; auto. case (H3 s); intros H7 _; auto. case H7; auto. intros H8; case F1; auto. + case (H5 s); intros HH _; apply HH; clear H5 HH. case (H3 s); intros _ HH; apply HH; clear H3 HH. right; case (H4 s); clear H4. intros HH _; case (HH H6); clear HH H6; intros HH; case HH; auto. Qed.
imports: ZArith List