proposition: Lemma step_fun_sound: forall task s l s', step_fun task s = Some (l,s') -> step s l s'.
proof: Proof. Proof using max_nid_eq. intros task s l s' Hstep. unfold step_fun, SysPredefs.init_nid in *. rewrite ?nids_eq in *. rewrite ?nid_in_dec_existsb in *. rewrite <-?max_nid in *. simpl. destruct task; simpl in Hstep. * case_eq (s n); intros ? ? ? ? ? Heq; rewrite Heq in *. rewrite nid_in_dec_existsb in *. destruct (List.in_dec NId_eq_dec n SysPredefs.nids); try discriminate. destruct prog0; inversion Hstep; clear Hstep; subst. - apply state_eq_override in Heq. rewrite Heq at 1. constructor; auto. - apply state_eq_override in Heq. rewrite Heq at 1. rewrite <-nid_eq_equiv in *. constructor; auto. - apply state_eq_override in Heq. rewrite Heq at 1. constructor; auto. * case_eq (s n1); intros ? ? ? ? ? Heq1; rewrite Heq1 in *. case_eq (s n2); intros ? ? ? ? ? Heq2; rewrite Heq2 in *. rewrite nid_in_dec_existsb in *. destruct (NId_eq_dec n1 n2); subst. rewrite Nat.eqb_refl in *. inversion Hstep; clear Hstep; subst. inversion Hstep; clear Hstep; subst. apply Nat.eqb_neq in n; rewrite n in *. apply Nat.eqb_neq in n. destruct (List.in_dec NId_eq_dec n1 SysPredefs.nids); try discriminate. case_eq (Nat.ltb (rec0 n2) (Datatypes.length ptrace1)); intro Hltb_eq; rewrite ?Hltb_eq in *; case_eq (List.forallb (fun pid : PutId => Nat.leb (put_id_clock pid) (rec0 (put_id_nid pid))) (t_put_dep (List.nth (rec0 n2) ptrace1 dummy_t_put))); intro Hforall_eq; rewrite ?Hforall_eq in *; simpl in *; try (inversion H0; clear H0; subst). autorewrite with nat in *. apply state_eq_override in Heq1. apply state_eq_override in Heq2. rewrite Heq2 at 1. rewrite Heq1 at 1. constructor; auto. apply List.Forall_forall. setoid_rewrite <-Nat.leb_le. apply ->List.forallb_forall. auto. Qed.
imports: Coq(FunctionalExtensionality List Arith Lia) Chapar(Predefs KVStore)