proposition: Lemma correspond_inductive : forall net net' tr_m', step_async net net' tr_m' -> forall st st' tr_m tr_1 tr_1', correspond st (nwState net) tr_1 tr_m -> step_1_star st st' tr_1' -> inputs_1 tr_1' = inputs_m tr_m' -> correspond st' (nwState net') (tr_1 ++ tr_1') (tr_m ++ tr_m').
proof: Proof. Proof using. intros. invc H; repeat break_let; simpl in *; repeat match goal with | [ H : context [ inputs_m [(_, inr _)] ] |- _ ] => rewrite inputs_m_inr_singleton in H | [ H : context [ inputs_m [(Primary, inl (Request _))] ] |- _ ] => rewrite inputs_m_primary_inl_request_singleton in H | [ H : context [ inputs_m ((Primary, inl (Request _)) :: _) ] |- _ ] => rewrite inputs_m_primary_inl in H | [ H : context [ inputs_m [(_, inl Read)] ] |- _ ] => rewrite inputs_m_inl_read_singleton in H | [ H : context [ inputs_m ((_, inl Read) :: _) ] |- _ ] => rewrite inputs_m_inl_read in H | [ H : context [ inputs_1 _ = [] ] |- _ ] => apply inputs_1_nil_is_nil in H; subst | [ H : context [ inputs_m [_] ] |- _ ] => rewrite inputs_m_backup_singleton in H | [ H : context [ inputs_m (_ :: _) ] |- _ ] => rewrite inputs_m_backup in H | [ H : step_1_star _ _ [] |- _ ] => apply step_1_star_no_trace_no_step in H; [|solve [auto]]; subst | [ H : step_1_star _ _ [_] |- _ ] => apply step_1_star_singleton_trace in H | [ H : step_1 _ _ [_] |- _ ] => apply step_1_singleton_inversion in H | [ |- context [ _ ++ [] ] ] => repeat rewrite app_nil_r | [ H : context [ _ ++ [] ] |- _ ] => repeat rewrite app_nil_r in * | [ H : context [ [] ++ _ ] |- _ ] => repeat rewrite app_nil_l in * | [ H : context [PB_net _ _ _ _] |- _ ] => apply PB_net_defn in H | [ H : context [PB_input_handler _ _ _] |- _ ] => apply PB_input_handler_defn in H | [ H : context [inputs_1 _ = [_]] |- _ ] => apply inputs_1_singleton in H | [ H : _ /\ _ |- _ ] => break_and | [ H : exists _, _ |- _ ] => break_exists | [ H : _ \/ _ |- _ ] => break_or_hyp | _ => repeat break_let; repeat find_rewrite; repeat tuple_inversion; subst; auto end; repeat rewrite snoc_assoc; eauto using correspond_preserved_primary_same_no_outputs, update_nop, update_diff, outputs_m_inr_nil_singleton, outputs_m_inl_read_singleton, outputs_m_read_response_singleton. - eapply correspond_preserved_primary_apply_entry; eauto using update_eq. - eapply correspond_preserved_primary_apply_entry; eauto using update_eq. - eapply correspond_preserved_primary_same_no_outputs; eauto. eapply correspond_preserved_snoc; eauto; rewrite update_eq by auto; repeat find_rewrite; auto. - eapply correspond_preserved_primary_same_no_outputs; eauto. eapply correspond_preserved_snoc; eauto; rewrite update_eq by auto; repeat find_rewrite; auto. Qed.
imports: Verdi(Verdi HandlerMonad)