proposition: Lemma fast_prove_no_fault: forall program h s n run_steps, StepStar.step_star (init program) h s -> (forall n, program n <> fault) -> (forall sched_length, fast_check_all_schedules nids (run_steps + sched_length) (init program) (check_no_fault'' nids) = true) -> (forall l, List.In l h -> l <> fault_label n).
proof: Proof. Proof using max_nid_eq. intros program h s n run_steps Hss Hinit_no_fault Hcheck_scheds. intros l Hin. generalize (step_star_not_in_nids _ _ _ n Hss); intro Hnot_nids_eq. apply step_star_fun_complete in Hss. destruct Hss as [sched Hss]. apply List.in_split in Hin. destruct Hin as [h1[h2 Heq]]; subst h. apply step_star_fun_app_inv in Hss. destruct Hss as [sched1[s'[sched2'[Heq[Hss1 Hss2]]]]]; subst sched. apply step_star_fun_cons_inv in Hss2. destruct Hss2 as [task[s''[sched2[Heq[Hs _]]]]]; subst sched2'. eapply step_label_check_no_fault''; eauto. clear task Hs. destruct (list_end _ sched1) as [Heq | [sched[task Heq]]]; subst sched1. * simpl in Hss1. inversion Hss1; clear Hss1. unfold check_no_fault''. apply List.forallb_forall. intros n1 Hin1. simpl. mcase_eq; auto. exfalso. eapply Hinit_no_fault; eauto. * rewrite step_star_fun_app in Hss1. mcase_eq as Hss in Hss1; try discriminate. destruct p. simpl in Hss1. mcase_eq as Hs in Hss1; try discriminate. destruct p. inversion Hss1; clear Hss1; subst h1 s1. eapply check_all_schedules'_correct with (check:=fun l s => check_no_fault'' nids s) (max_steps:= run_steps + (S (List.length sched))) (sched:=sched) (task:=task) (s':=s0); eauto. - eapply fast_check_all_schedules_correct'; eauto. - eapply valid_schedule_step_star_fun with (ls1:=nil) (sched:=(sched++[task])%list) (prog0:=program); eauto. rewrite step_star_fun_app, Hss. simpl; rewrite Hs; reflexivity. - lia. Qed.
imports: Coq(FunctionalExtensionality List Arith Lia) Chapar(Predefs KVStore)