proposition: Lemma check_all_schedules'_correct_fun_equiv: forall max_steps check s, (check_all_schedules' nids max_steps s check = true <-> (forall sched task ls l s' s'', valid_schedule nids (sched++[task]) -> List.length sched < max_steps -> step_star_fun nil sched s = Some (ls,s') -> step_fun task s' = Some (l,s'') -> check l s'' = true)).
proof: Proof. Proof using max_nid_eq. split; intros. * rewrite nids_eq in *. rename H into Hperm. rename H0 into Hvalid_sched. rename H1 into Hsched_len. rename H2 into Hss. rename H3 into Hs. revert sched task ls l Hsched_len s s' s'' Hvalid_sched Hperm Hss Hs. clear max_nid_eq. induction max_steps; intros; subst. destruct sched; inversion Hsched_len. apply valid_schedule_app in Hvalid_sched. unfold check_all_schedules' in Hperm. fold check_all_schedules' in Hperm. rewrite List.forallb_forall in Hperm. setoid_rewrite Bool.andb_true_iff in Hperm. setoid_rewrite List.forallb_forall in Hperm. destruct Hvalid_sched as [Hvalid_sched Hin]. apply valid_schedule_cons in Hin; destruct Hin as [Hin _]. destruct sched as [ | task' sched ]. - simpl in Hss; inversion Hss; clear Hss; subst. destruct task as [ n1 | n1 n2 ]; [ specialize (Hperm n1 Hin); destruct Hperm as [Hcheck _]; rewrite Hs in Hcheck; apply Bool.andb_true_iff in Hcheck; tauto | destruct Hin as [Hin1 Hin2]; specialize (Hperm n1 Hin1); destruct Hperm as [_ HcheckUpd]; specialize (HcheckUpd n2 Hin2); rewrite Hs in HcheckUpd; apply Bool.andb_true_iff in HcheckUpd; tauto ]. - simpl in Hsched_len. apply Nat.succ_lt_mono in Hsched_len. simpl in Hss. apply valid_schedule_cons in Hvalid_sched. destruct Hvalid_sched as [Hin' Hvalid_sched]. repeat mcase_eq in Hss; try congruence; subst. apply prefix_inv_step_star_fun in Hss. destruct Hss as [ls3[Heq Hss]]; subst ls. destruct task' as [ n1 | n1 n2 ]. + specialize (Hperm n1 Hin'). destruct Hperm as [Hcheck _]. rewrite H in Hcheck. apply Bool.andb_true_iff in Hcheck. destruct Hcheck as [Hcheck Hcheck_all]. eapply IHmax_steps with (s:=s0) (s':=s'); eauto. apply valid_schedule_app; split; auto. apply valid_schedule_cons; split; auto; constructor. + destruct Hin' as [Hin1' Hin2']. specialize (Hperm n1 Hin1'). destruct Hperm as [_ HcheckUpd]. specialize (HcheckUpd n2 Hin2'). rewrite H in HcheckUpd. apply Bool.andb_true_iff in HcheckUpd. destruct HcheckUpd as [Hcheck Hcheck_all]. eapply IHmax_steps with (s:=s0) (s':=s'); eauto. apply valid_schedule_app; split; auto. apply valid_schedule_cons; split; auto; constructor. * rename H into Hss. revert s Hss. clear max_nid_eq. induction max_steps; intros; subst. - reflexivity. - unfold check_all_schedules'; fold check_all_schedules'. rewrite List.forallb_forall. setoid_rewrite Bool.andb_true_iff. setoid_rewrite List.forallb_forall. intros n1 Hin1. split. + mcase_eq; auto. destruct p as [l s']. rewrite Bool.andb_true_iff. split. eapply Hss with (sched:=nil) (ls:=nil); simpl; eauto. apply valid_nid_step_fun_Proc in H. apply valid_schedule_cons; split; auto; constructor. lia. eapply IHmax_steps; eauto. intros sched task ls l' s'' s''' Hvalid_sched Hsched_len Hss' Hs''. eapply Hss with (sched:=([SchedProc n1]++sched)%list) (ls:=([l]++ls)%list); eauto. rewrite <-List.app_assoc. apply valid_schedule_app; split; auto. apply valid_schedule_cons; split; auto; constructor. simpl; lia. rewrite step_star_fun_app. unfold step_star_fun; fold step_star_fun. rewrite H. simpl. apply prefix_step_star_fun with (ls3:=[l]); auto. + intros n2 Hin2. mcase_eq; auto. destruct p as [l s']. rewrite Bool.andb_true_iff. split. eapply Hss with (sched:=nil) (ls:=nil); simpl; eauto. apply valid_nid_step_fun_Update in H. apply valid_schedule_cons; split; auto; constructor. lia. eapply IHmax_steps; eauto. intros sched task ls l' s'' s''' Hvalid_sched Hsched_len Hss' Hs''. eapply Hss with (sched:=([SchedUpdate n1 n2]++sched)%list) (ls:=([l]++ls)%list); eauto. rewrite <-List.app_assoc. apply valid_schedule_app; split; auto. apply valid_schedule_cons; split; auto; constructor. simpl; lia. rewrite step_star_fun_app. unfold step_star_fun; fold step_star_fun. rewrite H. simpl. apply prefix_step_star_fun with (ls3:=[l]); auto. Qed.
imports: Coq(FunctionalExtensionality List Arith Lia) Chapar(Predefs KVStore)