proposition: Lemma MsgUnlock_moves_client : forall n c s, lb_step_execution lb_step_async s -> Nth (queue (nwState (evt_a (hd s)) Server)) (S n) c -> now (occurred MsgUnlock) s -> next (fun s => Nth (queue (nwState (evt_a (hd s)) Server)) n c /\ (n = 0 -> In (mkPacket Server (Client c) Locked) (nwPackets (evt_a (hd s))))) s.
proof: Proof. Proof using. intros n c s Hexec HNth Hlabel. destruct s. simpl. invcs Hexec. match goal with | H : lb_step_async _ _ _ _ |- _ => invcs H end. - unfold occurred in *. match goal with | H : MsgUnlock = _ |- _ => symmetry in H; repeat find_rewrite; clear H end. monad_unfold. unfold NetHandler in *. break_match. + find_apply_lem_hyp ClientNetHandler_lbcases. intuition; congruence. + find_apply_lem_hyp ServerNetHandler_lbcases. repeat (break_and; try break_or_hyp); break_exists; repeat (break_and; try break_or_hyp); try congruence. * exfalso. repeat find_rewrite. invcs HNth. repeat find_reverse_rewrite. simpl in *. subst. solve_by_inversion. * fold LockServ_MultiParams in *. repeat find_rewrite. simpl in *. find_apply_lem_hyp Nth_tl. repeat find_rewrite. intuition; [|intros; subst; solve_by_inversion]. rewrite_update. congruence. - unfold occurred in *. match goal with | H : MsgUnlock = _ |- _ => symmetry in H; repeat find_rewrite; clear H end. monad_unfold. find_apply_lem_hyp InputHandler_lbcases. intuition; break_exists; intuition; congruence. - unfold occurred in *. congruence. Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition) Verdi(LabeledNet) InfSeqExt(infseq classical)