proposition: Lemma InstExecToExecStep': forall s1 l s2, N.ICExec.StepStarArgs.step s1 l s2 -> exists l', I.CExec.StepStarArgs.step (state_map s1) l' (state_map s2) /\ inst_exec_eff l = exec_eff l'.
proof: Proof. intros. inversion H. subst l0. pose (l' := (I.CExec.put_label n k (InstSyntaxArg.inst_val n (c + 1) v))). exists l'. simpl. split. rewrite H1. rewrite H3. unfold I.CExec.StepStarArgs.step. assert (A1: state_map s1 = I.CExec.state (override (I.CExec.node_states (state_map s1)) n (I.CExec.node_state (I.CExec.Syntax.put k (InstSyntaxArg.inst_val n (c + 1) v) (prog_map p n (c + 1))) s)) (map msg_map ms)). rewrite <- H1 at 1. unfold state_map at 1. f_equal. apply functional_extensionality. intro n0. destruct (eq_nat_dec n0 n). subst n0. simpl_override. simpl_override. f_equal. simpl_override. simpl_override. rewrite <- H1. simpl. simpl_override. reflexivity. assert (A2: state_map s2 = I.CExec.state (override (I.CExec.node_states (state_map s1)) n (I.CExec.node_state (prog_map p n (c + 1)) s')) ((map msg_map ms) ++ (map (fun n' => (I.CExec.message k (InstSyntaxArg.inst_val n (c + 1) v) u n')) (filter (fun n' => if (nid_eq_dec n n') then false else true) nids)))). rewrite <- H3 at 1. unfold state_map at 1. f_equal. apply functional_extensionality. intro n0. destruct (eq_nat_dec n0 n). subst n0. simpl_override. simpl_override. reflexivity. simpl_override. simpl_override. rewrite <- H1. simpl. simpl_override. reflexivity. simpl. rewrite map_app. f_equal. rewrite map_map. f_equal. subv l'. rewrite A1. rewrite A2. constructor. assumption. unfold Val. reflexivity. pose (l' := (I.CExec.get_label n k (InstSyntaxArg.inst_val n' c' v'))). exists l'. simpl. split. rewrite H1. rewrite H3. unfold I.CExec.StepStarArgs.step. assert (A1: state_map s1 = I.CExec.state (override (I.CExec.node_states (state_map s1)) n (I.CExec.node_state (I.CExec.Syntax.get k (fun v => (prog_map (p (inst_val_val v)) n c))) s)) (map msg_map ms)). rewrite <- H1 at 1. unfold state_map at 1. f_equal. apply functional_extensionality. intro n0. destruct (eq_nat_dec n0 n). subst n0. simpl_override. simpl_override. f_equal. simpl_override. simpl_override. rewrite <- H1. simpl. simpl_override. reflexivity. assert (A2: state_map s2 = I.CExec.state (override (I.CExec.node_states (state_map s1)) n (I.CExec.node_state (prog_map (p (inst_val_val (InstSyntaxArg.inst_val n' c' v'))) n c) s')) (map msg_map ms)). rewrite <- H3 at 1. unfold state_map at 1. f_equal. apply functional_extensionality. intro n0. destruct (eq_nat_dec n0 n). subst n0. simpl_override. simpl_override. reflexivity. simpl_override. simpl_override. rewrite <- H1. simpl. simpl_override. reflexivity. assert (A3: get_method N.ICExec.InstVal n s k = ((inst_val n' c' v'), s')). subv n'. subv c'. subv v'. subv s'. subv u. subv r. destruct (get_method N.ICExec.InstVal n s k). simpl. f_equal. destruct i. simpl. reflexivity. assert (A4: inst_val n' c' v' = fst (get_method N.ICExec.InstVal n s k)). rewrite A3. reflexivity. assert (A5: s' = snd (get_method N.ICExec.InstVal n s k)). rewrite A3. reflexivity. subv l'. rewrite A1. rewrite A2. rewrite A4. rewrite A5. constructor. assumption. unfold Val. reflexivity. pose (l' := (I.CExec.update_label n k (InstSyntaxArg.inst_val n' c' v))). exists l'. simpl. split. rewrite H2. rewrite H4. unfold I.CExec.StepStarArgs.step. assert (A1: state_map s1 = I.CExec.state (override (I.CExec.node_states (state_map s1)) n (I.CExec.node_state (prog_map p n c) s)) ((map msg_map ms1) ++ (I.CExec.message k (N.ICExec.inst_val n' c' v) u n) :: (map msg_map ms2))). rewrite <- H2 at 1. unfold state_map at 1. f_equal. apply functional_extensionality. intro n0. destruct (eq_nat_dec n0 n). subst n0. simpl_override. simpl_override. f_equal. simpl_override. simpl_override. rewrite <- H2. simpl. simpl_override. reflexivity. simpl. rewrite map_app. f_equal. assert (A2: state_map s2 = I.CExec.state (override (I.CExec.node_states (state_map s1)) n (I.CExec.node_state (prog_map p n c) s')) ((map msg_map ms1) ++ (map msg_map ms2))). rewrite <- H4 at 1. unfold state_map at 1. f_equal. apply functional_extensionality. intro n0. destruct (eq_nat_dec n0 n). subst n0. simpl_override. simpl_override. reflexivity. simpl_override. simpl_override. rewrite <- H2. simpl. simpl_override. reflexivity. simpl. rewrite map_app. reflexivity. assert (A3: s' = update_method Val n s k (inst_val n' c' v) u). subv s'. reflexivity. subv l'. rewrite A1. rewrite A2. rewrite A3. constructor. assumption. assumption. unfold Val. reflexivity. pose (l' := (I.CExec.fault_label n)). exists l'. simpl. split. rewrite H1. rewrite H3. unfold I.CExec.StepStarArgs.step. assert (A1: state_map s1 = I.CExec.state (override (I.CExec.node_states (state_map s1)) n (I.CExec.node_state I.CExec.Syntax.fault s)) (map msg_map ms)). rewrite <- H1 at 1. unfold state_map at 1. f_equal. apply functional_extensionality. intro n0. destruct (eq_nat_dec n0 n). subst n0. simpl_override. simpl_override. f_equal. simpl_override. simpl_override. rewrite <- H1. simpl. simpl_override. reflexivity. assert (A2: state_map s2 = I.CExec.state (override (I.CExec.node_states (state_map s1)) n (I.CExec.node_state I.CExec.Syntax.skip s)) (map msg_map ms)). rewrite <- H3 at 1. unfold state_map at 1. f_equal. apply functional_extensionality. intro n0. destruct (eq_nat_dec n0 n). subst n0. simpl_override. simpl_override. simpl. reflexivity. simpl_override. simpl_override. rewrite <- H1. simpl. simpl_override. reflexivity. subv l'. rewrite A1. rewrite A2. constructor. assumption. assumption. unfold Val. reflexivity. Qed.
imports: Coq(FunctionalExtensionality Arith Lia) Coq(Arith.Peano_dec Arith.Compare_dec) Coq(Relations.Relation_Operators) Coq(List) Chapar(Predefs)