proposition: Theorem revertNetwork_input : forall (st : seq_num_network) h (d : @data orig_base_params) l l' n, sequence_sane st -> sequence_seen st -> sequence_equality st -> processPackets (tdNum (nwState st h)) l = (n, l') -> revertNetwork (@mkNetwork _ multi_params (send_packets h l' ++ nwPackets st) (update name_eq_dec (nwState st) h (@mkseq_num_data _ orig_multi_params n (tdSeen (nwState st h)) d))) = {| nwPackets := (@send_packets _ orig_multi_params h l) ++ (nwPackets (revertNetwork st)); nwState := update name_eq_dec (nwState (revertNetwork st)) h d |}.
proof: Proof. Proof using. intros. unfold revertNetwork. simpl in *. match goal with [ |- context [ dedup ?eq (map ?f ?l ++ ?l') ] ] => assert (dedup eq (map f l ++ l') = (map f l) ++ (dedup eq l')) by (find_eapply_lem_hyp processPackets_dedup; eauto; repeat find_rewrite; in_crush) end. find_rewrite. rewrite filter_app. rewrite map_app. f_equal. f_equal. - rewrite filter_true_id. + match goal with | _ : processPackets ?n ?l = _ |- _ => rewrite <- (processPackets_preserves_messages n l) end. find_rewrite. simpl in *. unfold revertPacket. repeat rewrite map_map. auto. + intros. in_crush. find_eapply_lem_hyp processPackets_ge_start; [|eauto]. repeat (break_if; simpl in *; repeat find_rewrite; intuition); unfold sequence_seen in *; find_apply_hyp_hyp; lia. - f_equal. apply filter_fun_ext_eq. intros. repeat (break_if; simpl in *; repeat find_rewrite; intuition). - apply functional_extensionality. intros; repeat break_if; simpl in *; intuition. Qed.
imports: Verdi(Verdi) Coq(FunctionalExtensionality) Verdi(SeqNum)