proposition: Lemma valid_schedule_step_star_fun: forall ls1 sched prog0 hs', step_star_fun ls1 sched (init prog0) = Some hs' -> valid_schedule nids sched.
proof: Proof. Proof using. intros. clear max_nid_eq. assert (forall n1 n2, List.In n1 nids -> ~List.In n2 nids -> ptrace ((init prog0) n2) = nil /\ rec ((init prog0) n1) n2 = 0) by (split; reflexivity). remember (init prog0) as s. rename H into Hss. rename H0 into Hbad_nid_clock_zero. clear Heqs. revert ls1 s Hss Hbad_nid_clock_zero. induction sched as [ | [ n1 | n1 n2 ] sched ]; simpl; intros. * constructor. * rewrite nid_in_dec_existsb in Hss. generalize (Hbad_nid_clock_zero n1); intro Hbncz1. apply valid_schedule_cons; simpl; split; auto; repeat mcase_eq in Hss; auto; try discriminate; eapply IHsched; eauto; clear Hss H0 IHsched; intros ? n2; intros; generalize (Hbad_nid_clock_zero n2); intro Hbncz2; intuition (subst; auto); repeat match goal with | |- context[SysPredefs.override _ ?n1 _ ?n2] => (is_var n1 || is_var n2); destruct (NId_eq_dec n1 n2); [ subst; rewrite !SysPredefs.override_new_val | rewrite SysPredefs.override_old_val with (k:=n1) (k':=n2); auto ] | _ => progress simpl | _ => contradiction end; try solve [ eapply Hbad_nid_clock_zero; intuition auto | apply Hbncz1; auto ]. * assert (List.In n2 nids). { repeat mcase_eq in Hss; try discriminate. clear Hss IHsched. destruct (List.in_dec NId_eq_dec n2 nids) as [Hin|Hnin]; auto. exfalso. rewrite ?Bool.andb_true_iff, ?Bool.orb_true_iff in H1. autorewrite with nat in H1. specialize (Hbad_nid_clock_zero n1 n2). rewrite H in Hbad_nid_clock_zero. rewrite H0 in Hbad_nid_clock_zero. simpl in Hbad_nid_clock_zero. destruct H1 as [[[??]?]?]. rewrite nid_in_dec_existsb in *. mcase_eq in H2; try discriminate. lapply Hbad_nid_clock_zero; clear Hbad_nid_clock_zero; [ intro Hbad_nid_clock_zero | intuition (subst; auto) ]. lapply Hbad_nid_clock_zero; clear Hbad_nid_clock_zero; auto. intros [Heq1 Heq2]; rewrite ?Heq1, ?Heq2 in *. inversion H3. } generalize (Hbad_nid_clock_zero n2); intro Hbncz2. generalize (Hbad_nid_clock_zero n1); intro Hbncz1. rewrite nid_in_dec_existsb in *; nid_cases n1; nid_cases n2; simpl in *; repeat mcase_eq in Hss; try discriminate; rewrite ?Bool.andb_true_iff, ?Bool.orb_true_iff in *; intuition auto; try discriminate; apply valid_schedule_cons; simpl; split_all; auto; eapply IHsched; eauto; intros; auto; intuition (subst; auto); try discriminate; repeat match goal with | |- context[SysPredefs.override _ ?n1 _ ?n2] => (is_var n1 || is_var n2); destruct (NId_eq_dec n1 n2); [ subst; rewrite !SysPredefs.override_new_val | rewrite SysPredefs.override_old_val with (k:=n1) (k':=n2); auto ] | _ => progress simpl | _ => contradiction end; try solve [ eapply Hbad_nid_clock_zero; intuition auto | eapply Hbncz2; intuition auto | simpl; simpl_override; eapply Hbncz1; intuition auto ]. Qed.
imports: Coq(FunctionalExtensionality List Arith Lia) Chapar(Predefs KVStore)