proposition: Lemma check_all_schedules_correct_fun_equiv: forall max_steps ls1 sched1 check s, (check_all_schedules nids max_steps ls1 sched1 s check = true <-> (forall sched2 ls s', valid_schedule nids sched2 -> List.length sched2 <= max_steps -> step_star_fun ls1 (sched1 ++ sched2)%list s = Some (ls,s') -> check ls s' = true)).
proof: Proof. Proof using max_nid_eq. split; intros. rewrite nids_eq in *. * rename H0 into Hvalid_sched. rename H into Hperm. rename H1 into Hsched_len. rename H2 into Hss. revert ls1 sched2 Hsched_len sched1 s s' Hvalid_sched Hperm Hss. induction max_steps; simpl; intros. - destruct sched2; inversion Hsched_len. rewrite List.app_nil_r in *. rewrite Hss in Hperm. rewrite !Bool.andb_true_iff in *. apply Hperm. - repeat mcase_eq in Hperm. rewrite !Bool.andb_true_iff in *. destruct Hperm as [Heq Hperm]. rewrite List.forallb_forall in Hperm. setoid_rewrite Bool.andb_true_iff in Hperm. setoid_rewrite List.forallb_forall in Hperm. destruct sched2 as [ | [ n1 | n1 n2 ] sched2 ]. + rewrite List.app_nil_r in *; intuition auto. rewrite H in Hss; inversion Hss; clear Hss; auto. rewrite <- H2. rewrite <- H3. assumption. + simpl in Hsched_len; apply le_S_n in Hsched_len. apply valid_schedule_cons in Hvalid_sched. rewrite step_star_fun_app, H in Hss. destruct Hvalid_sched as [Hin Hvalid_sched]. simpl in Hin. rewrite <-nids_eq in *. eapply IHmax_steps with (s:=s0) (sched1:=[SchedProc n1]%list) (sched2:=sched2); auto. eapply Hperm; eauto. intuition (subst; eauto). + simpl in Hsched_len; apply le_S_n in Hsched_len. apply valid_schedule_cons in Hvalid_sched. rewrite step_star_fun_app, H in Hss. destruct Hvalid_sched as [Hin Hvalid_sched]. simpl in Hin. eapply IHmax_steps with (sched1:=[SchedUpdate n1 n2]%list); eauto. eapply Hperm; apply Hin. + rewrite step_star_fun_app, H in Hss; discriminate. * rename H into Hss. revert ls1 sched1 s Hss. clear max_nid_eq. induction max_steps; simpl; intros; subst. - repeat mcase_eq; subst; auto. rewrite Bool.andb_true_r; auto. apply (Hss nil); simpl; auto. constructor. rewrite List.app_nil_r; auto. - repeat mcase_eq; subst; auto. rewrite !Bool.andb_true_iff in *. rewrite List.forallb_forall. setoid_rewrite Bool.andb_true_iff. setoid_rewrite List.forallb_forall. split; intros; split_all; intros; try match goal with | Hss: context[_ -> check _ _ = true], IH: context[check_all_schedules _ _ _ _ _ _ = true] |- check_all_schedules _ _ _ _ _ _ = true => eapply IHmax_steps; repeat match goal with |- _->?a => fail 1 | |- forall _:_, _ => intro end; intros; eapply (Hss (_::_)%list); simpl; [ | | rewrite step_star_fun_app, H; eauto]; [ eapply valid_schedule_cons; split; auto; simpl; auto | lia ] | |- true = true => reflexivity end. apply (Hss nil); simpl. constructor. lia. rewrite List.app_nil_r; auto. Qed.
imports: Coq(FunctionalExtensionality List Arith Lia) Chapar(Predefs KVStore)