proposition: Lemma ServerNetHandler_lbcases : forall src m st l out st' ms, ServerNetHandler src m st = (l, out, st', ms) -> out = [] /\ ((exists c, src = Client c /\ (m = Lock /\ l = MsgLock c /\ queue st' = queue st ++ [c] /\ ((queue st = [] /\ ms = [(Client c, Locked)]) \/ (queue st <> [] /\ ms = [])))) \/ ((m = Unlock /\ l = MsgUnlock /\ queue st' = tail (queue st) /\ ((queue st' = [] /\ ms = []) \/ (exists next t, queue st' = next :: t /\ ms = [(Client next, Locked)])))) \/ ms = [] /\ st' = st /\ l = Nop).
proof: Proof. Proof using. handler_unfold. intros. repeat break_match; repeat tuple_inversion; subst. - find_apply_lem_hyp null_sound. find_rewrite. simpl. intuition. left. eexists. intuition. - simpl. find_apply_lem_hyp null_false_neq_nil. intuition. left. eexists. intuition. - simpl. intuition. - simpl. destruct st; simpl in *; subst; intuition. - simpl in *. intuition. - simpl in *. intuition eauto. - simpl. intuition. Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition) Verdi(LabeledNet) InfSeqExt(infseq classical)