proposition: Lemma step_fun_complete: forall s l s', step s l s' -> exists task, step_fun task s = Some (l,s').
proof: Proof. Proof using max_nid_eq. intros s l s' Hstep. inversion Hstep; clear Hstep. * exists (SchedProc n). unfold step_fun. rewrite nids_eq in *. rewrite nid_in_dec_existsb in *. simpl. destruct (List.in_dec NId_eq_dec n SysPredefs.nids); try contradiction. simpl_override. simpl. subst u' d' r' m'. f_equal. f_equal. apply functional_extensionality; intros. case_eq (n =? x); autorewrite with nat; intros; subst; simpl_override; auto. * exists (SchedProc n). unfold step_fun, SysPredefs.init_nid in *. rewrite ?nids_eq in *. rewrite ?nid_in_dec_existsb in *. rewrite <-?max_nid in *. simpl. mcase_eq; try contradiction. simpl_override. simpl. subst n'' c'' d'' d' v s l s'. f_equal. f_equal. simpl_override. rewrite max_nid_eq. destruct Peano_dec.eq_nat_dec as [Heq | Hneq]; auto; [ rewrite Heq, Nat.eqb_refl; auto | apply Nat.eqb_neq in Hneq; rewrite Hneq ]; apply functional_extensionality; intros; case_eq (n =? x); autorewrite with nat; intros; subst; simpl_override; auto. * exists (SchedUpdate n_1 n_2). unfold step_fun, SysPredefs.init_nid in *. rewrite ?nids_eq in *. rewrite ?nid_in_dec_existsb in *. rewrite <-?max_nid in *. simpl. destruct (List.in_dec NId_eq_dec n_1 SysPredefs.nids); try contradiction. subst k v d r_1' m_1'. simpl_override. simpl. apply Nat.eqb_neq in H0; rewrite H0. case_eq (Nat.ltb (r_1 n_2) (Datatypes.length u_2)); autorewrite with nat; intro; try lia. match goal with | H: List.Forall ?f ?l |- context[List.forallb _ _] => rewrite List.Forall_forall in H; setoid_rewrite <-Nat.leb_le in H; apply <-List.forallb_forall in H; rewrite H end. simpl. simpl_override. f_equal. f_equal. apply Nat.eqb_neq in H0. rewrite override_neq with (n1:=n_1) (n2:=n_2); auto. rewrite override_eq. rewrite override_neq with (n1:=n_1) (n2:=n_2); auto. rewrite override_eq. rewrite override_neq with (n1:=n_1) (n2:=n_2); auto. * exists (SchedProc n). unfold step_fun. rewrite nids_eq in *. rewrite nid_in_dec_existsb in *. simpl. destruct (List.in_dec NId_eq_dec n SysPredefs.nids); try contradiction. simpl_override. simpl. f_equal. f_equal. apply functional_extensionality; intros. case_eq (n =? x); autorewrite with nat; intros; subst; simpl_override; auto. Qed.
imports: Coq(FunctionalExtensionality List Arith Lia) Chapar(Predefs KVStore)