proposition: Lemma reachable_revert_step : forall st st' tr, reachable step_dup step_async_init st -> step_dup st st' tr -> step_async (revertNetwork st) (revertNetwork st') tr \/ (revertNetwork st = revertNetwork st' /\ filterMap trace_non_empty_out tr = []).
proof: Proof. Proof using. intros. find_copy_apply_lem_hyp reachable_sane. find_copy_apply_lem_hyp reachable_seen. find_copy_apply_lem_hyp reachable_equality. break_exists. match goal with H : step_dup _ _ _ |- _ => invcs H end. - unfold seq_num_net_handlers in *. match goal with | [H : context [ if _ then _ else _ ] |- _] => revert H end. break_if; intros. + right. find_inversion. simpl in *. unfold revertNetwork. simpl in *. intuition. f_equal. * f_equal. find_rewrite. symmetry. match goal with | |- filter ?f _ = filter ?g _ => assert (f = g) by (apply functional_extensionality; intros; repeat break_if; repeat find_rewrite; intuition) end. find_rewrite. apply filter_dedup. break_if; intuition. * apply functional_extensionality. intros. break_if; subst; intuition. + left. repeat break_let. find_inversion. match goal with | [ H : processPackets _ _ = _, H' : net_handlers _ _ _ _ = (_, d0, _) |- _ ] => eapply revertNetwork_deliver_step with (d := d0) in H; eauto end. break_exists. break_and. match goal with | [H : nwPackets _ = _ |- _ ] => eapply (StepAsync_deliver _ _ _ _ H); eauto end. - left. unfold seq_num_input_handlers in *. repeat break_let. find_inversion. find_eapply_lem_hyp revertNetwork_input; eauto. econstructor 2; simpl; eauto. - right. split; auto. unfold revertNetwork. f_equal. f_equal. f_equal. simpl. find_rewrite. eauto using dedup_eliminates_duplicates. Qed.
imports: Verdi(Verdi) Coq(FunctionalExtensionality) Verdi(SeqNum)