proposition: Theorem reachable_equality : true_in_reachable step_dup step_async_init sequence_equality.
proof: Proof. Proof using. apply true_in_reachable_reqs; unfold sequence_equality; simpl in *; intuition. match goal with H : reachable _ _ _ |- _ => apply reachable_sane in H end. unfold sequence_sane, sequence_equality in *. intros. match goal with H : step_dup _ _ _ |- _ => invcs H end; simpl in *; find_inversion. - unfold seq_num_net_handlers in *. repeat do_in_app. repeat find_rewrite. repeat break_match; find_inversion; simpl in *; intuition; repeat do_in_map; subst; simpl in *. + repeat do_in_app. intuition auto with datatypes. + find_inversion. match goal with | x : prod _ _, x' : prod _ _ |- _ => replace x with x' by (eapply processPackets_seq_eq; eauto) end; auto. + match goal with H : processPackets _ _ = _ |- _ => eapply processPackets_ge_start in H end; eauto. match goal with _ : In ?p _, H : forall _ : packet, In _ _ -> _ |- _ => specialize (H p); forward H; [do_in_app; intuition auto with datatypes|]; [concludes] end. repeat find_rewrite. lia. + find_inversion. match goal with H : processPackets _ _ = _ |- _ => eapply processPackets_ge_start in H end; eauto. match goal with _ : In ?p _, H : forall _ : packet, In _ _ -> _ |- _ => specialize (H p); forward H; [do_in_app; intuition auto with datatypes|]; [concludes] end. simpl in *. repeat find_rewrite. lia. + match goal with H : forall _ _ : packet, In _ _ -> _ |- ?p = ?p' => specialize (H p p'); repeat (forward H; [repeat do_in_app; intuition auto with datatypes|]; concludes) end; auto. - unfold seq_num_input_handlers in *. repeat do_in_app. repeat break_match; find_inversion; simpl in *; intuition; repeat do_in_map; subst; simpl in *. + find_inversion. match goal with | x : prod _ _, x' : prod _ _ |- _ => replace x with x' by (eapply processPackets_seq_eq; eauto) end; auto. + match goal with H : processPackets _ _ = _ |- _ => eapply processPackets_ge_start in H end; eauto. match goal with _ : In ?p _, H : forall _ : packet, In _ _ -> _ |- _ => specialize (H p); forward H; [in_crush|]; [concludes] end. simpl in *. repeat find_rewrite. lia. + find_inversion. match goal with H : processPackets _ _ = _ |- _ => eapply processPackets_ge_start in H end; eauto. match goal with _ : In ?p _, H : forall _ : packet, In _ _ -> _ |- _ => specialize (H p); forward H; [in_crush|]; [concludes] end. simpl in *. repeat find_rewrite. lia. - repeat find_rewrite. repeat break_or_hyp; subst; intuition auto with datatypes. Qed.
imports: Verdi(Verdi) Coq(FunctionalExtensionality) Verdi(SeqNum)