proposition: Lemma Erasure'': forall s1 l s2, N.CExec.step s1 l s2 -> forall s1', erase_state s1' s1 -> exists l' s2', N.ICExec.step s1' l' s2' /\ erase_state s2' s2 /\ l = erase_label l'.
proof: Proof. destruct 1; substs; destruct s1'; simpl; intuition. replace node_states with (override node_states n (N.ICExec.node_state (put k v p) (N.ICExec.alg_state (node_states n)) (N.ICExec.clock_state (node_states n)))). do 3 esplit. constructor; auto. Ltac erase_state := unfold erase_state in *; simpl in *; intuition; try (apply Rmessages_app; auto; apply Rmessages_map; simpl; intuition). erase_state. Ltac nid_cases := match goal with | [ |- context[override _ ?n1 _ ?n2] ] => match n1 with | n2 => fail 1 | _ => destruct (nid_eq_dec n1 n2); subst; intuition; try match goal with | [ H : forall n : NId, _ |- _ ] => specialize (H n2) end; repeat (autorewrite with core in *; simpl in *; intuition) end end. nid_cases. nid_cases. Ltac use_nid := match goal with | [ H : forall n : NId, _ |- context[_ ?n] ] => specialize (H n); repeat (simpl in *; autorewrite with core in *; intuition) end. Ltac put_method := match goal with | [ |- context[put_method N.ICExec.InstVal ?n ?s1 ?k ?v1] ] => match goal with | [ |- context[put_method Val n ?s2 k ?v2] ] => specialize (put_method_R _ _ R n s1 s2 k v1 v2); destruct (put_method N.ICExec.InstVal n s1 k v1), (put_method Val n s2 k v2); unfold erase_state in *; simpl in *; destruct 1; intuition; try use_nid; cbv beta; try (apply Rmessages_app; auto; apply Rmessages_map; simpl; intuition) end end. put_method. put_method. erase_state. extensionality n0. nid_cases. Ltac apart := match goal with | [ |- N.ICExec.node_state _ _ _ = ?X ] => destruct X; simpl in *; subst; intuition end. apart. replace node_states with (override node_states n (N.ICExec.node_state (get k p) (N.ICExec.alg_state (node_states n)) (N.ICExec.clock_state (node_states n)))). do 3 esplit. constructor; auto. erase_state. nid_cases. f_equal. assert (A := get_method_R). specialize (A N.ICExec.InstVal Val R n0 (N.ICExec.alg_state (node_states n0)) s k). depremise A. assumption. destruct (get_method N.ICExec.InstVal n0 (N.ICExec.alg_state (node_states n0)) k). destruct (get_method Val n0 s k). destruct A as [A _]. unfold R in A. unfold N.ICExec.inst_val_val in A. simpl. assumption. nid_cases. Ltac get_method := match goal with | [ |- context[get_method N.ICExec.InstVal ?n ?s1 ?k] ] => match goal with | [ |- context[get_method Val n ?s2 k] ] => specialize (get_method_R _ _ R n s1 s2 k); destruct (get_method N.ICExec.InstVal n s1 k), (get_method Val n s2 k); unfold erase_state in *; simpl in *; destruct 1; intuition; try use_nid end end. get_method. get_method. unfold R in H0. unfold N.ICExec.inst_val_val in H0. rewrite H0. reflexivity. erase_state. extensionality n0. nid_cases. apart. generalize H1; destruct 1; simpl in *. clear H2. apply Rmessages_app_bwd in H3; destruct H3 as [ ? [ ] ]; intuition (subst; simpl in * ). inversion_clear H5. replace node_states with (override node_states n (N.ICExec.node_state p (N.ICExec.alg_state (node_states n)) (N.ICExec.clock_state (node_states n)))). destruct m; simpl in *; subst. do 3 esplit. constructor; auto. erase_state. specialize (H3 n); autorewrite with core in *; intuition. erewrite guard_method_R; (cbv beta; eauto). erase_state. nid_cases. nid_cases. auto using update_method_R. erase_state. extensionality n0. subst. nid_cases. specialize (H5 (N.ICExec.msg_receiver m)); simpl in *; intuition. apart. autorewrite with core; auto. generalize H0; destruct 1; simpl in *. replace node_states with (override node_states n (N.ICExec.node_state fault (N.ICExec.alg_state (node_states n)) (N.ICExec.clock_state (node_states n)))). do 3 esplit. constructor; auto. erase_state. specialize (H3 n); autorewrite with core in *; intuition. erase_state. nid_cases. nid_cases. erase_state. extensionality n0. subst. nid_cases. specialize (H1 n0). open_conjs. apart. autorewrite with core; auto. Qed.
imports: Coq(FunctionalExtensionality Arith Lia) Coq(Arith.Peano_dec Arith.Compare_dec) Coq(Relations.Relation_Operators) Coq(List) Chapar(Predefs)