From mathcomp.ssreflect
Require Import ssreflect ssrbool ssrnat eqtype ssrfun seq.
From mathcomp
Require Import path.
Require Import Eqdep.
Require Import Relation_Operators.
From fcsl
Require Import pred prelude ordtype finmap pcm unionmap heap.
From DiSeL
Require Import Freshness State EqTypeX DepMaps.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Section SoupPredicates.

(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) x (consume_msg s i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t' c') pt to true)), @eq (Ordered.sort mid) j x *)
(* Goal: forall (i0 : Ordered.sort mid) (t : nat) (c : list nat) (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i0 (consume_msg s i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) pt to true))), is_true (andb (@eq_op nat_eqType t tg) (@eq_op (seq_eqType nat_eqType) c cnt)) *)
(*****************************************************)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) x (consume_msg s i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t' c') pt to true)), @eq (Ordered.sort mid) j x *)
(* Goal: forall (i0 : Ordered.sort mid) (t : nat) (c : list nat) (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i0 (consume_msg s i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) pt to true))), is_true (andb (@eq_op nat_eqType t tg) (@eq_op (seq_eqType nat_eqType) c cnt)) *)
(* Message predicates

[Valid messages in soup]

The following generic definition "msg_in_souop" specifies which
messages are considered valid in the specific state and the soup. 

The derived definition come next.

(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) x (consume_msg s i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t' c') pt to true)), @eq (Ordered.sort mid) j x *)
(* Goal: forall (i0 : Ordered.sort mid) (t : nat) (c : list nat) (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i0 (consume_msg s i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) pt to true))), is_true (andb (@eq_op nat_eqType t tg) (@eq_op (seq_eqType nat_eqType) c cnt)) *)
 *)

(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
Definition msg_in_soup (from to : nid) (criterion : nat -> seq nat -> bool)
           (d : soup) : Prop :=
  (exists! i, exists t c,
        find i d = Some (Msg (TMsg t c) from to true)) /\
  forall i t c,
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
    find i d = Some (Msg (TMsg t c) from to true) ->
    criterion t c.

(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) x (consume_msg s i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t' c') pt to true)), @eq (Ordered.sort mid) j x *)
(* Goal: forall (i0 : Ordered.sort mid) (t : nat) (c : list nat) (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i0 (consume_msg s i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) pt to true))), is_true (andb (@eq_op nat_eqType t tg) (@eq_op (seq_eqType nat_eqType) c cnt)) *)
(* Fix specific tag and content *)
Definition msg_spec from to tg cnt :=
  msg_in_soup from to (fun x y => (x == tg) && (y == cnt)).

Definition no_msg_from (from : nid) (d : soup) : Prop :=
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
  forall i to tms b, find i d = Some (Msg tms from to b) -> b = false.

Definition no_msg_to (to : nid) (d : soup) : Prop :=
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
  forall i from tms b, find i d = Some (Msg tms from to b) -> b = false.


Lemma no_msg_from_post (from from' to : nid) (s : soup) tms :
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
  valid s ->
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
  no_msg_from from s -> from' != from ->
  no_msg_from from (post_msg s (Msg tms from' to true)).1.
Proof.
(* Goal: forall (_ : is_true (@PCM.valid (union_mapPCM mid (msg TaggedMessage)) s)) (_ : no_msg_from_to' from to cond s), no_msg_from_to' from to cond (consume_msg s i) *)
move=>V H/negbTE N i to' tms' b/=.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) z (@PCM.join (union_mapPCM mid (msg TaggedMessage)) s (@um_pts nat_ordType (msg TaggedMessage) (@fresh (msg TaggedMessage) s) (@Msg TaggedMessage (TMsg tg cnt) from to true)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), @eq nat (@fresh (msg TaggedMessage) s) z *)
rewrite findUnR ?valid_fresh?V//.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (consume_msg s i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
case: ifP; last by move=>_/H.
(* Goal: forall (_ : is_true (@in_mem (Ordered.sort mid) i (@mem (Equality.sort (Ordered.eqType mid)) (seq_predType (Ordered.eqType mid)) (@UMC.dom mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) (@um_pts nat_ordType (msg TaggedMessage) (@fresh (msg TaggedMessage) s) (@Msg TaggedMessage (TMsg tg cnt) from to true)))))) (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@um_pts nat_ordType (msg TaggedMessage) (@fresh (msg TaggedMessage) s) (@Msg TaggedMessage (TMsg tg cnt) from to true))) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true))), is_true (andb (@eq_op nat_eqType t tg) (@eq_op (seq_eqType nat_eqType) c cnt)) *)
(* Goal: @ex nat (@unique nat (fun i : nat => @ex nat (fun t : nat => @ex (list nat) (fun c : list nat => @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@PCM.join (union_mapPCM mid (msg TaggedMessage)) s (@um_pts nat_ordType (msg TaggedMessage) (@fresh (msg TaggedMessage) s) (@Msg TaggedMessage (TMsg tg cnt) from to true)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)))))) *)
rewrite domPt inE/==>/eqP Z; subst i.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) (@fresh (msg TaggedMessage) s) (@um_pts nat_ordType (msg TaggedMessage) (@fresh (msg TaggedMessage) s) (@Msg TaggedMessage tms from' to true))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tms' from to' b)), @eq bool b false *)
rewrite findPt/=; case=>Z1 Z2 Z3; subst to' tms' from'.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
by rewrite eqxx in N.
Qed.

Lemma no_msg_from_consume from from' to s i m :
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
  find i s = Some {| content := m; from := from'; to := to; active := true |} ->
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
  valid s ->
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
  no_msg_from from s ->
  no_msg_from from (consume_msg s i).
Proof.
(* Goal: forall (_ : is_true (@PCM.valid (union_mapPCM mid (msg TaggedMessage)) s)) (_ : no_msg_from_to' from to cond s), no_msg_from_to' from to cond (consume_msg s i) *)
move=>F V NM j to' tms b.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) k (consume_msg s i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t' c') pt to true)), is_true (andb (@eq_op nat_eqType t' tg) (@eq_op (seq_eqType nat_eqType) c' cnt)) *)
case H: (j == i).
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
- move /eqP in H. subst j.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) z (@PCM.join (union_mapPCM mid (msg TaggedMessage)) s (@um_pts nat_ordType (msg TaggedMessage) (@fresh (msg TaggedMessage) s) (@Msg TaggedMessage (TMsg tg cnt) from to true)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), @eq nat (@fresh (msg TaggedMessage) s) z *)
  rewrite (find_consume _ F) //.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
  by case.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) z (@PCM.join (union_mapPCM mid (msg TaggedMessage)) s (@um_pts nat_ordType (msg TaggedMessage) (@fresh (msg TaggedMessage) s) (@Msg TaggedMessage (TMsg tg cnt) from to true)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), @eq nat (@fresh (msg TaggedMessage) s) z *)
rewrite mark_other//.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j s) (@Some (msg TaggedMessage) (@Msg TaggedMessage tms from to' b)), @eq bool b false *)
exact: NM.
Qed.

Definition no_msg_from_to from to (d : soup) :=
  forall i tms b,
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
    find i d = Some (Msg tms from to b) -> b = false.

Lemma no_msg_from_to_consume from to s i:
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
  valid s ->
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
  no_msg_from_to from to s ->
  no_msg_from_to from to (consume_msg s i).
Proof.
(* Goal: forall (_ : is_true (@PCM.valid (union_mapPCM mid (msg TaggedMessage)) s)) (_ : no_msg_from_to' from to cond s), no_msg_from_to' from to cond (consume_msg s i) *)
move=>V H m tms b .
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (consume_msg s i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
rewrite /consume_msg; case: (find i s); last by move=>F; apply: (H m tms b F).
(* Goal: forall (a : msg TaggedMessage) (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage a) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true))), is_true (negb (cond t c)) *)
move=>ms; case B: (m == i).
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
- by move/eqP: B=>B; subst m; rewrite findU eqxx/= V; case. 
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
by rewrite findU B/==>/(H m tms b).
Qed.

Lemma msg_spec_consume s from to tg cnt cnt' i :
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
  valid s -> 
  find i s = Some {| content := TMsg tg cnt';
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
                     from := from; to := to; active := true |} ->
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
  msg_spec from to tg cnt s ->
  no_msg_from_to from to (consume_msg s i).
Proof.
(* Goal: forall (_ : is_true (@PCM.valid (union_mapPCM mid (msg TaggedMessage)) s)) (_ : no_msg_from_to' from to cond s), no_msg_from_to' from to cond (consume_msg s i) *)
move=>V E[][j][[t][c]]F H1 H2. 
(* Goal: no_msg_from_to from to (consume_msg s i) *)
move=>m tms b; rewrite /consume_msg; move: (find_some E).
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
case: dom_find=>// msg->_ _; case B: (m == i).
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
- by move/eqP: B=>B; subst m; rewrite findU eqxx/= V; case. 
have X: j = i by  apply: (H1 i); exists tg, cnt'.
(* Goal: forall _ : @eq (option (State.msg TaggedMessage)) (@UMC.find mid (State.msg TaggedMessage) (union_mapUMC mid (State.msg TaggedMessage)) m (@UMC.upd mid (State.msg TaggedMessage) (union_mapUMC mid (State.msg TaggedMessage)) i (@mark_msg TaggedMessage msg) s)) (@Some (State.msg TaggedMessage) (@Msg TaggedMessage tms from to b)), @eq bool b false *)
subst j; rewrite findU B/=; case: b=>// E'.
(* Goal: @eq bool true false *)
suff X: i = m by subst i; rewrite eqxx in B.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
by apply: (H1 m); case: tms E'=>t' c' E'; exists t', c'. 
Qed.

Lemma msg_specE_consume s pt from to to' tg cnt i m :
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
  valid s ->
  find i s =
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
  Some {| content := m; from := from; to := to'; active := true |} ->
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
  (pt != from) || (to != to') ->
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
  msg_spec pt to tg cnt s ->
  msg_spec pt to tg cnt (consume_msg s i).
Proof.
(* Goal: forall (_ : is_true (@PCM.valid (union_mapPCM mid (msg TaggedMessage)) s)) (_ : no_msg_from_to' from to cond s), no_msg_from_to' from to cond (consume_msg s i) *)
  move=>V E N[][j][[t][c]]F H1 H2.
(* Goal: msg_spec pt to tg cnt (consume_msg s i) *)
  have Nij: i != j.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
  - case H: (i == j)=>//.
(* Goal: forall (_ : is_true (@PCM.valid (union_mapPCM mid (msg TaggedMessage)) s)) (_ : no_msg_from_to' from to cond s), no_msg_from_to' from to cond (consume_msg s i) *)
    move/eqP in H. subst i.
(* Goal: forall (_ : is_true (@PCM.valid (union_mapPCM mid (msg TaggedMessage)) s)) (_ : no_msg_from_to' from to cond s), no_msg_from_to' from to cond (consume_msg s i) *)
    move: E. rewrite F. case. intros. subst.
(* Goal: is_true (negb true) *)
(* Goal: msg_spec pt to tg cnt (consume_msg s i) *)
    move: N=>/orP[]/eqP; congruence.
(* Goal: @unique (Ordered.sort mid) (fun i0 : Ordered.sort mid => @ex nat (fun t : nat => @ex (list nat) (fun c : list nat => @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i0 (consume_msg s i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) pt to true))))) j *)
(* Goal: forall (i0 : Ordered.sort mid) (t : nat) (c : list nat) (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i0 (consume_msg s i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) pt to true))), is_true (andb (@eq_op nat_eqType t tg) (@eq_op (seq_eqType nat_eqType) c cnt)) *)
  split.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
  - exists j.
(* Goal: @unique (Ordered.sort mid) (fun i0 : Ordered.sort mid => @ex nat (fun t : nat => @ex (list nat) (fun c : list nat => @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i0 (consume_msg s i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) pt to true))))) j *)
(* Goal: forall (i0 : Ordered.sort mid) (t : nat) (c : list nat) (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i0 (consume_msg s i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) pt to true))), is_true (andb (@eq_op nat_eqType t tg) (@eq_op (seq_eqType nat_eqType) c cnt)) *)
    split.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) k (consume_msg s i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t' c') pt to true)), is_true (andb (@eq_op nat_eqType t' tg) (@eq_op (seq_eqType nat_eqType) c' cnt)) *)
    + exists t, c. rewrite mark_other// eq_sym. by apply /negbTE.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) k (consume_msg s i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t' c') pt to true)), is_true (andb (@eq_op nat_eqType t' tg) (@eq_op (seq_eqType nat_eqType) c' cnt)) *)
    + move => x [t'][c'].
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) k (consume_msg s i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t' c') pt to true)), is_true (andb (@eq_op nat_eqType t' tg) (@eq_op (seq_eqType nat_eqType) c' cnt)) *)
      case H: (x == i).
(* Goal: forall (_ : is_true (@PCM.valid (union_mapPCM mid (msg TaggedMessage)) s)) (_ : no_msg_from_to' from to cond s), no_msg_from_to' from to cond (consume_msg s i) *)
      * move /eqP in H. subst x.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
        by rewrite (find_consume _ E)//.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) z (@PCM.join (union_mapPCM mid (msg TaggedMessage)) s (@um_pts nat_ordType (msg TaggedMessage) (@fresh (msg TaggedMessage) s) (@Msg TaggedMessage (TMsg tg cnt) from to true)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), @eq nat (@fresh (msg TaggedMessage) s) z *)
      * rewrite mark_other//.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) k s) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t' c') pt to true)), is_true (andb (@eq_op nat_eqType t' tg) (@eq_op (seq_eqType nat_eqType) c' cnt)) *)
        eauto.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
  - move=>k t' c'.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) k (consume_msg s i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t' c') pt to true)), is_true (andb (@eq_op nat_eqType t' tg) (@eq_op (seq_eqType nat_eqType) c' cnt)) *)
    case H: (k == i).
(* Goal: forall (_ : is_true (@PCM.valid (union_mapPCM mid (msg TaggedMessage)) s)) (_ : no_msg_from_to' from to cond s), no_msg_from_to' from to cond (consume_msg s i) *)
    + move /eqP in H. subst.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) z (@PCM.join (union_mapPCM mid (msg TaggedMessage)) s (@um_pts nat_ordType (msg TaggedMessage) (@fresh (msg TaggedMessage) s) (@Msg TaggedMessage (TMsg tg cnt) from to true)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), @eq nat (@fresh (msg TaggedMessage) s) z *)
      rewrite (find_consume _ E) //.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) z (@PCM.join (union_mapPCM mid (msg TaggedMessage)) s (@um_pts nat_ordType (msg TaggedMessage) (@fresh (msg TaggedMessage) s) (@Msg TaggedMessage (TMsg tg cnt) from to true)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), @eq nat (@fresh (msg TaggedMessage) s) z *)
    + rewrite mark_other//.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) k s) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t' c') pt to true)), is_true (andb (@eq_op nat_eqType t' tg) (@eq_op (seq_eqType nat_eqType) c' cnt)) *)
      eauto.
Qed.

Lemma msg_specE_consume1 s pt from to to' tg cnt i m :
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
  valid s ->
  find i s =
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
  Some {| content := m; from := from; to := to'; active := true |} ->
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
  (pt != from) ->
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
  msg_spec pt to tg cnt s ->
  msg_spec pt to tg cnt (consume_msg s i).
Proof.
(* Goal: forall (_ : is_true (@PCM.valid (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) s)) (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i s) (@Some (msg TaggedMessage) (@Msg TaggedMessage m from to' true))) (_ : is_true (negb (@eq_op nat_eqType to to'))) (_ : msg_spec pt to tg cnt s), msg_spec pt to tg cnt (consume_msg s i) *)
  intros.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) k s) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t' c') pt to true)), is_true (andb (@eq_op nat_eqType t' tg) (@eq_op (seq_eqType nat_eqType) c' cnt)) *)
  eapply msg_specE_consume; eauto.
(* Goal: is_true (orb (negb (@eq_op nat_eqType pt from)) (negb (@eq_op nat_eqType to to'))) *)
  apply /orP; auto.
Qed.

Lemma msg_specE_consume2 s pt from to to' tg cnt i m :
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
  valid s ->
  find i s =
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
  Some {| content := m; from := from; to := to'; active := true |} ->
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
  (to != to') ->
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
  msg_spec pt to tg cnt s ->
  msg_spec pt to tg cnt (consume_msg s i).
Proof.
(* Goal: forall (_ : is_true (@PCM.valid (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) s)) (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i s) (@Some (msg TaggedMessage) (@Msg TaggedMessage m from to' true))) (_ : is_true (negb (@eq_op nat_eqType to to'))) (_ : msg_spec pt to tg cnt s), msg_spec pt to tg cnt (consume_msg s i) *)
  intros.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) k s) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t' c') pt to true)), is_true (andb (@eq_op nat_eqType t' tg) (@eq_op (seq_eqType nat_eqType) c' cnt)) *)
  eapply msg_specE_consume; eauto.
(* Goal: is_true (orb (negb (@eq_op nat_eqType pt from)) (negb (@eq_op nat_eqType to to'))) *)
  apply /orP; auto.
Qed.

Definition no_msg_from_imp from to d :
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
  no_msg_from from d -> no_msg_from_to from to d.
Proof. by move=>H i; move: (H i to). Qed.


Lemma no_msg_from_toE from to s tms to':
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
  valid s -> 
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
  no_msg_from_to from to s -> to == to' = false ->
  no_msg_from_to from to (post_msg s (Msg tms from to' true)).1.
Proof.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) z (@PCM.join (union_mapPCM mid (msg TaggedMessage)) s (@um_pts nat_ordType (msg TaggedMessage) (@fresh (msg TaggedMessage) s) (@Msg TaggedMessage (TMsg tg cnt) from to true)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), @eq nat (@fresh (msg TaggedMessage) s) z *)
move=>V H X/= i m b; rewrite findUnR ?valid_fresh?V//.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (consume_msg s i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
case: ifP; last by move=>_/H.
(* Goal: forall (_ : is_true (@in_mem (Ordered.sort mid) i (@mem (Equality.sort (Ordered.eqType mid)) (seq_predType (Ordered.eqType mid)) (@UMC.dom mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) (@um_pts nat_ordType (msg TaggedMessage) (@fresh (msg TaggedMessage) s) (@Msg TaggedMessage (TMsg tg cnt) from to true)))))) (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@um_pts nat_ordType (msg TaggedMessage) (@fresh (msg TaggedMessage) s) (@Msg TaggedMessage (TMsg tg cnt) from to true))) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true))), is_true (andb (@eq_op nat_eqType t tg) (@eq_op (seq_eqType nat_eqType) c cnt)) *)
(* Goal: @ex nat (@unique nat (fun i : nat => @ex nat (fun t : nat => @ex (list nat) (fun c : list nat => @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@PCM.join (union_mapPCM mid (msg TaggedMessage)) s (@um_pts nat_ordType (msg TaggedMessage) (@fresh (msg TaggedMessage) s) (@Msg TaggedMessage (TMsg tg cnt) from to true)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)))))) *)
rewrite domPt inE/==>/eqP Z; subst i.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
by rewrite findPt/=; case=>_ Z; subst to'; rewrite eqxx in X.
Qed.

Lemma no_msg_from_toE' from to s tms from' to':
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
  valid s -> 
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
  no_msg_from_to from to s -> from' == from = false ->
  no_msg_from_to from to (post_msg s (Msg tms from' to' true)).1.
Proof.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) z (@PCM.join (union_mapPCM mid (msg TaggedMessage)) s (@um_pts nat_ordType (msg TaggedMessage) (@fresh (msg TaggedMessage) s) (@Msg TaggedMessage (TMsg tg cnt) from to true)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), @eq nat (@fresh (msg TaggedMessage) s) z *)
move=>V H X/= i m b; rewrite findUnR ?valid_fresh?V//.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (consume_msg s i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
case: ifP; last by move=>_/H.
(* Goal: forall (_ : is_true (@in_mem (Ordered.sort mid) i (@mem (Equality.sort (Ordered.eqType mid)) (seq_predType (Ordered.eqType mid)) (@UMC.dom mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) (@um_pts nat_ordType (msg TaggedMessage) (@fresh (msg TaggedMessage) s) (@Msg TaggedMessage (TMsg tg cnt) from to true)))))) (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@um_pts nat_ordType (msg TaggedMessage) (@fresh (msg TaggedMessage) s) (@Msg TaggedMessage (TMsg tg cnt) from to true))) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true))), is_true (andb (@eq_op nat_eqType t tg) (@eq_op (seq_eqType nat_eqType) c cnt)) *)
(* Goal: @ex nat (@unique nat (fun i : nat => @ex nat (fun t : nat => @ex (list nat) (fun c : list nat => @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@PCM.join (union_mapPCM mid (msg TaggedMessage)) s (@um_pts nat_ordType (msg TaggedMessage) (@fresh (msg TaggedMessage) s) (@Msg TaggedMessage (TMsg tg cnt) from to true)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)))))) *)
rewrite domPt inE/==>/eqP Z; subst i.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
by rewrite findPt/=; case=>Z' Z; subst from'; rewrite eqxx in X.
Qed.

Lemma msg_specE s from to tg cnt :
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
  valid s ->
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
  no_msg_from_to from to s ->
  msg_spec from to tg cnt (post_msg s (Msg (TMsg tg cnt) from to true)).1.
Proof.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (consume_msg s i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
move=>V H; split=>/=; last first.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) z (@PCM.join (union_mapPCM mid (msg TaggedMessage)) s (@um_pts nat_ordType (msg TaggedMessage) (@fresh (msg TaggedMessage) s) (@Msg TaggedMessage (TMsg tg cnt) from to true)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), @eq nat (@fresh (msg TaggedMessage) s) z *)
- move=>i t c; rewrite findUnR ?valid_fresh?V//.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (consume_msg s i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
  case: ifP; last by move=>_/H.
(* Goal: forall (_ : is_true (@in_mem (Ordered.sort mid) i (@mem (Equality.sort (Ordered.eqType mid)) (seq_predType (Ordered.eqType mid)) (@UMC.dom mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) (@um_pts nat_ordType (msg TaggedMessage) (@fresh (msg TaggedMessage) s) (@Msg TaggedMessage (TMsg tg cnt) from to true)))))) (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@um_pts nat_ordType (msg TaggedMessage) (@fresh (msg TaggedMessage) s) (@Msg TaggedMessage (TMsg tg cnt) from to true))) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true))), is_true (andb (@eq_op nat_eqType t tg) (@eq_op (seq_eqType nat_eqType) c cnt)) *)
(* Goal: @ex nat (@unique nat (fun i : nat => @ex nat (fun t : nat => @ex (list nat) (fun c : list nat => @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@PCM.join (union_mapPCM mid (msg TaggedMessage)) s (@um_pts nat_ordType (msg TaggedMessage) (@fresh (msg TaggedMessage) s) (@Msg TaggedMessage (TMsg tg cnt) from to true)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)))))) *)
  rewrite domPt inE/==>/eqP Z; subst i.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
  by rewrite findPt/=; case=>E Z; subst c t; rewrite !eqxx.
(* Goal: @ex nat (@unique nat (fun i : nat => @ex nat (fun t : nat => @ex (list nat) (fun c : list nat => @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@PCM.join (union_mapPCM mid (msg TaggedMessage)) s (@um_pts nat_ordType (msg TaggedMessage) (@fresh (msg TaggedMessage) s) (@Msg TaggedMessage (TMsg tg cnt) from to true)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)))))) *)
exists (fresh s); split=>[|z[t][c]].
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) z (@PCM.join (union_mapPCM mid (msg TaggedMessage)) s (@um_pts nat_ordType (msg TaggedMessage) (@fresh (msg TaggedMessage) s) (@Msg TaggedMessage (TMsg tg cnt) from to true)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), @eq nat (@fresh (msg TaggedMessage) s) z *)
- exists tg, cnt; rewrite findUnR ?valid_fresh?V//.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
  by rewrite domPt inE eqxx/=findPt/=.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) z (@PCM.join (union_mapPCM mid (msg TaggedMessage)) s (@um_pts nat_ordType (msg TaggedMessage) (@fresh (msg TaggedMessage) s) (@Msg TaggedMessage (TMsg tg cnt) from to true)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), @eq nat (@fresh (msg TaggedMessage) s) z *)
rewrite findUnR ?valid_fresh?V// domPt !inE/=.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
by case: ifP=>[|_/H]//; move/eqP=>->.  
Qed.

Lemma msg_specE' s from to to' tg cnt tms :
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
  valid s -> to == to' = false ->
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
  msg_spec from to tg cnt s ->
  msg_spec from to tg cnt (post_msg s (Msg tms from to' true)).1.
Proof.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (consume_msg s i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
move=>V N H; split=>//=; last first.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) z (@PCM.join (union_mapPCM mid (msg TaggedMessage)) s (@um_pts nat_ordType (msg TaggedMessage) (@fresh (msg TaggedMessage) s) (@Msg TaggedMessage (TMsg tg cnt) from to true)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), @eq nat (@fresh (msg TaggedMessage) s) z *)
- move=>i t c; rewrite findUnR ?valid_fresh?V//.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (consume_msg s i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
  rewrite domPt inE/=; case:ifP; last by move=>_; move/(proj2 H).
(* Goal: forall (_ : is_true (@eq_op (Ordered.eqType mid) (@fresh (msg TaggedMessage) s) i)) (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@um_pts nat_ordType (msg TaggedMessage) (@fresh (msg TaggedMessage) s) (@Msg TaggedMessage tms from' to' true))) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true))), is_true (andb (@eq_op nat_eqType t tg) (@eq_op (seq_eqType nat_eqType) c cnt)) *)
(* Goal: @ex nat (@unique nat (fun i : nat => @ex nat (fun t : nat => @ex (list nat) (fun c : list nat => @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@PCM.join (union_mapPCM mid (msg TaggedMessage)) s (@um_pts nat_ordType (msg TaggedMessage) (@fresh (msg TaggedMessage) s) (@Msg TaggedMessage tms from' to' true)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)))))) *)
  move/eqP=>Z; subst i; rewrite findPt/=; case=>_ Z.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
  by subst to'; rewrite eqxx in N.   
(* Goal: @ex nat (@unique nat (fun i : nat => @ex nat (fun t : nat => @ex (list nat) (fun c : list nat => @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@PCM.join (union_mapPCM mid (msg TaggedMessage)) s (@um_pts nat_ordType (msg TaggedMessage) (@fresh (msg TaggedMessage) s) (@Msg TaggedMessage tms from' to' true)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)))))) *)
case: (H)=>H' _; case: H'=>i; case=>[[t]][c] U1 U2.
(* Goal: @ex nat (@unique nat (fun i : nat => @ex nat (fun t : nat => @ex (list nat) (fun c : list nat => @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@PCM.join (union_mapPCM mid (msg TaggedMessage)) s (@um_pts nat_ordType (msg TaggedMessage) (@fresh (msg TaggedMessage) s) (@Msg TaggedMessage tms from' to' true)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)))))) *)
exists i; split=>//.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) z (@PCM.join (union_mapPCM mid (msg TaggedMessage)) s (@um_pts nat_ordType (msg TaggedMessage) (@fresh (msg TaggedMessage) s) (@Msg TaggedMessage (TMsg tg cnt) from to true)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), @eq nat (@fresh (msg TaggedMessage) s) z *)
- exists t, c; rewrite findUnR ?valid_fresh?V//.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) (@fresh (msg TaggedMessage) s) (@um_pts nat_ordType (msg TaggedMessage) (@fresh (msg TaggedMessage) s) (@Msg TaggedMessage tms from' to' true))) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t' c') from to true)), @eq nat i (@fresh (msg TaggedMessage) s) *)
  rewrite domPt inE/=; case:ifP=>//.
(* Goal: is_true (negb true) *)
(* Goal: msg_spec pt to tg cnt (consume_msg s i) *)
  move/eqP=>Z; subst i.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
  by move/find_some: U1=>E; move:(dom_fresh s); rewrite E.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) z (@PCM.join (union_mapPCM mid (msg TaggedMessage)) s (@um_pts nat_ordType (msg TaggedMessage) (@fresh (msg TaggedMessage) s) (@Msg TaggedMessage (TMsg tg cnt) from to true)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), @eq nat (@fresh (msg TaggedMessage) s) z *)
move=>z[t'][c']; rewrite findUnR ?valid_fresh?V//.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (consume_msg s i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
rewrite domPt inE/=; case:ifP=>//; last first.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
- by move=>_ G; apply: (U2 z); exists t', c'. 
(* Goal: forall (_ : is_true (@eq_op (Ordered.eqType mid) (@fresh (msg TaggedMessage) s) z)) (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) z (@um_pts nat_ordType (msg TaggedMessage) (@fresh (msg TaggedMessage) s) (@Msg TaggedMessage tms from' to' true))) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t' c') from to true))), @eq nat i z *)
move/eqP=>Z; subst z.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) (@fresh (msg TaggedMessage) s) (@um_pts nat_ordType (msg TaggedMessage) (@fresh (msg TaggedMessage) s) (@Msg TaggedMessage tms from' to' true))) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t' c') from to true)), @eq nat i (@fresh (msg TaggedMessage) s) *)
rewrite findPt/=; case=>Z1 Z2. 
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
by subst to'; rewrite eqxx in N.
Qed.

Lemma msg_specE'' s from from' to to' tg cnt tms :
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
  valid s -> from == from' = false ->
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
  msg_spec from to tg cnt s ->
  msg_spec from to tg cnt (post_msg s (Msg tms from' to' true)).1.
Proof.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (consume_msg s i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
move=>V N H; split=>//=; last first.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) z (@PCM.join (union_mapPCM mid (msg TaggedMessage)) s (@um_pts nat_ordType (msg TaggedMessage) (@fresh (msg TaggedMessage) s) (@Msg TaggedMessage (TMsg tg cnt) from to true)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), @eq nat (@fresh (msg TaggedMessage) s) z *)
- move=>i t c; rewrite findUnR ?valid_fresh?V//.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (consume_msg s i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
  rewrite domPt inE/=; case:ifP; last by move=>_; move/(proj2 H).
(* Goal: forall (_ : is_true (@eq_op (Ordered.eqType mid) (@fresh (msg TaggedMessage) s) i)) (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@um_pts nat_ordType (msg TaggedMessage) (@fresh (msg TaggedMessage) s) (@Msg TaggedMessage tms from' to' true))) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true))), is_true (andb (@eq_op nat_eqType t tg) (@eq_op (seq_eqType nat_eqType) c cnt)) *)
(* Goal: @ex nat (@unique nat (fun i : nat => @ex nat (fun t : nat => @ex (list nat) (fun c : list nat => @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@PCM.join (union_mapPCM mid (msg TaggedMessage)) s (@um_pts nat_ordType (msg TaggedMessage) (@fresh (msg TaggedMessage) s) (@Msg TaggedMessage tms from' to' true)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)))))) *)
  move/eqP=>Z; subst i; rewrite findPt/=; case=>_ Z.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
  by subst from'; rewrite eqxx in N.   
(* Goal: @ex nat (@unique nat (fun i : nat => @ex nat (fun t : nat => @ex (list nat) (fun c : list nat => @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@PCM.join (union_mapPCM mid (msg TaggedMessage)) s (@um_pts nat_ordType (msg TaggedMessage) (@fresh (msg TaggedMessage) s) (@Msg TaggedMessage tms from' to' true)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)))))) *)
case: (H)=>H' _; case: H'=>i; case=>[[t]][c] U1 U2.
(* Goal: @ex nat (@unique nat (fun i : nat => @ex nat (fun t : nat => @ex (list nat) (fun c : list nat => @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@PCM.join (union_mapPCM mid (msg TaggedMessage)) s (@um_pts nat_ordType (msg TaggedMessage) (@fresh (msg TaggedMessage) s) (@Msg TaggedMessage tms from' to' true)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)))))) *)
exists i; split=>//.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) z (@PCM.join (union_mapPCM mid (msg TaggedMessage)) s (@um_pts nat_ordType (msg TaggedMessage) (@fresh (msg TaggedMessage) s) (@Msg TaggedMessage (TMsg tg cnt) from to true)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), @eq nat (@fresh (msg TaggedMessage) s) z *)
- exists t, c; rewrite findUnR ?valid_fresh?V//.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) (@fresh (msg TaggedMessage) s) (@um_pts nat_ordType (msg TaggedMessage) (@fresh (msg TaggedMessage) s) (@Msg TaggedMessage tms from' to' true))) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t' c') from to true)), @eq nat i (@fresh (msg TaggedMessage) s) *)
  rewrite domPt inE/=; case:ifP=>//.
(* Goal: is_true (negb true) *)
(* Goal: msg_spec pt to tg cnt (consume_msg s i) *)
  move/eqP=>Z; subst i.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
  by move/find_some: U1=>E; move:(dom_fresh s); rewrite E.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) z (@PCM.join (union_mapPCM mid (msg TaggedMessage)) s (@um_pts nat_ordType (msg TaggedMessage) (@fresh (msg TaggedMessage) s) (@Msg TaggedMessage (TMsg tg cnt) from to true)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), @eq nat (@fresh (msg TaggedMessage) s) z *)
move=>z[t'][c']; rewrite findUnR ?valid_fresh?V//.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (consume_msg s i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
rewrite domPt inE/=; case:ifP=>//; last first.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
- by move=>_ G; apply: (U2 z); exists t', c'. 
(* Goal: forall (_ : is_true (@eq_op (Ordered.eqType mid) (@fresh (msg TaggedMessage) s) z)) (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) z (@um_pts nat_ordType (msg TaggedMessage) (@fresh (msg TaggedMessage) s) (@Msg TaggedMessage tms from' to' true))) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t' c') from to true))), @eq nat i z *)
move/eqP=>Z; subst z.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) (@fresh (msg TaggedMessage) s) (@um_pts nat_ordType (msg TaggedMessage) (@fresh (msg TaggedMessage) s) (@Msg TaggedMessage tms from' to' true))) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t' c') from to true)), @eq nat i (@fresh (msg TaggedMessage) s) *)
rewrite findPt/=; case=>Z1 Z2. 
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
by subst from'; rewrite eqxx in N.
Qed.

End SoupPredicates.

(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) x (consume_msg s i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t' c') pt to true)), @eq (Ordered.sort mid) j x *)
(* Goal: forall (i0 : Ordered.sort mid) (t : nat) (c : list nat) (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i0 (consume_msg s i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) pt to true))), is_true (andb (@eq_op nat_eqType t tg) (@eq_op (seq_eqType nat_eqType) c cnt)) *)
(************************************************************)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) x (consume_msg s i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t' c') pt to true)), @eq (Ordered.sort mid) j x *)
(* Goal: forall (i0 : Ordered.sort mid) (t : nat) (c : list nat) (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i0 (consume_msg s i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) pt to true))), is_true (andb (@eq_op nat_eqType t tg) (@eq_op (seq_eqType nat_eqType) c cnt)) *)
(*                       List lemmas                        *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) x (consume_msg s i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t' c') pt to true)), @eq (Ordered.sort mid) j x *)
(* Goal: forall (i0 : Ordered.sort mid) (t : nat) (c : list nat) (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i0 (consume_msg s i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) pt to true))), is_true (andb (@eq_op nat_eqType t tg) (@eq_op (seq_eqType nat_eqType) c cnt)) *)
(************************************************************)

Lemma has_all_true xs (ps : seq nid) x:
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
  perm_eq [seq i.1 | i <- xs] ps ->
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
  all id [seq i.2 | i <- xs] ->
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
  x \in ps -> (x, true) \in xs.
Proof.
(* Goal: forall (_ : is_true (@perm_eq nat_eqType (@map (prod nid bool) nid (fun i : prod nid bool => @fst nid bool i) xs) ps)) (_ : is_true (@in_mem (Equality.sort nat_eqType) x (@mem (Equality.sort nat_eqType) (seq_predType nat_eqType) ps))), @ex (Equality.sort bool_eqType) (fun b : Equality.sort bool_eqType => is_true (@in_mem (prod (Equality.sort nat_eqType) (Equality.sort bool_eqType)) (@pair (Equality.sort nat_eqType) (Equality.sort bool_eqType) x b) (@mem (Equality.sort (prod_eqType nat_eqType bool_eqType)) (seq_predType (prod_eqType nat_eqType bool_eqType)) xs))) *)
move=>P A D; move: (perm_eq_mem P x).
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) x (consume_msg s i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t' c') pt to true)), @eq (Ordered.sort mid) j x *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) x (consume_msg s i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t' c') pt to true)), @eq (Ordered.sort mid) j x *)
(* Goal: forall (i0 : Ordered.sort mid) (t : nat) (c : list nat) (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i0 (consume_msg s i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) pt to true))), is_true (andb (@eq_op nat_eqType t tg) (@eq_op (seq_eqType nat_eqType) c cnt)) *)
rewrite D=>/mapP[z] I Z; subst x.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
rewrite all_map/= in A; move/allP: A=>/(_ z I)/=<-.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
by rewrite -surjective_pairing.
Qed.

(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) x (consume_msg s i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t' c') pt to true)), @eq (Ordered.sort mid) j x *)
(* Goal: forall (i0 : Ordered.sort mid) (t : nat) (c : list nat) (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i0 (consume_msg s i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) pt to true))), is_true (andb (@eq_op nat_eqType t tg) (@eq_op (seq_eqType nat_eqType) c cnt)) *)
Lemma has_some_false (xs : seq (nid * bool)) ps x:
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
  perm_eq [seq i.1 | i <- xs] ps ->
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
  x \in ps -> exists b, (x, b) \in xs.
Proof.
(* Goal: forall (_ : is_true (@perm_eq nat_eqType (@map (prod nid bool) nid (fun i : prod nid bool => @fst nid bool i) xs) ps)) (_ : is_true (@in_mem (Equality.sort nat_eqType) x (@mem (Equality.sort nat_eqType) (seq_predType nat_eqType) ps))), @ex (Equality.sort bool_eqType) (fun b : Equality.sort bool_eqType => is_true (@in_mem (prod (Equality.sort nat_eqType) (Equality.sort bool_eqType)) (@pair (Equality.sort nat_eqType) (Equality.sort bool_eqType) x b) (@mem (Equality.sort (prod_eqType nat_eqType bool_eqType)) (seq_predType (prod_eqType nat_eqType bool_eqType)) xs))) *)
move=>P D; move: (perm_eq_mem P x).
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) x (consume_msg s i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t' c') pt to true)), @eq (Ordered.sort mid) j x *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) x (consume_msg s i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t' c') pt to true)), @eq (Ordered.sort mid) j x *)
(* Goal: forall (i0 : Ordered.sort mid) (t : nat) (c : list nat) (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i0 (consume_msg s i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) pt to true))), is_true (andb (@eq_op nat_eqType t tg) (@eq_op (seq_eqType nat_eqType) c cnt)) *)
rewrite D=>/mapP[z] I Z; subst x.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
by exists z.2; rewrite -surjective_pairing.
Qed.

(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) x (consume_msg s i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t' c') pt to true)), @eq (Ordered.sort mid) j x *)
(* Goal: forall (i0 : Ordered.sort mid) (t : nat) (c : list nat) (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i0 (consume_msg s i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) pt to true))), is_true (andb (@eq_op nat_eqType t tg) (@eq_op (seq_eqType nat_eqType) c cnt)) *)
(********************************************************)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) x (consume_msg s i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t' c') pt to true)), @eq (Ordered.sort mid) j x *)
(* Goal: forall (i0 : Ordered.sort mid) (t : nat) (c : list nat) (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i0 (consume_msg s i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) pt to true))), is_true (andb (@eq_op nat_eqType t tg) (@eq_op (seq_eqType nat_eqType) c cnt)) *)
(*** More elaborated versions of the same predicates  ***)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) x (consume_msg s i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t' c') pt to true)), @eq (Ordered.sort mid) j x *)
(* Goal: forall (i0 : Ordered.sort mid) (t : nat) (c : list nat) (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i0 (consume_msg s i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) pt to true))), is_true (andb (@eq_op nat_eqType t tg) (@eq_op (seq_eqType nat_eqType) c cnt)) *)
(********************************************************)

Definition no_msg_from_to' from to
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
           (criterion : nat -> seq nat -> bool) (d : soup) :=
  forall i t c,
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
    find i d = Some (Msg (TMsg t c) from to true) ->
    ~~criterion t c.

Lemma no_msg_from_to_consume' from to cond s i:
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
  valid s ->
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
  no_msg_from_to' from to cond s ->
  no_msg_from_to' from to cond (consume_msg s i).
Proof.
(* Goal: forall (_ : is_true (@PCM.valid (union_mapPCM mid (msg TaggedMessage)) s)) (_ : no_msg_from_to' from to cond s), no_msg_from_to' from to cond (consume_msg s i) *)
move=>V H m t c .
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (consume_msg s i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
rewrite /consume_msg; case: (find i s); last by move=>F; apply: (H m t c F).
(* Goal: forall (a : msg TaggedMessage) (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage a) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true))), is_true (negb (cond t c)) *)
move=>ms; case B: (m == i).
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
- by move/eqP: B=>B; subst m; rewrite findU eqxx/= V.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
by rewrite findU B/==>/(H m t c).
Qed.

(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) x (consume_msg s i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t' c') pt to true)), @eq (Ordered.sort mid) j x *)
(* Goal: forall (i0 : Ordered.sort mid) (t : nat) (c : list nat) (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i0 (consume_msg s i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) pt to true))), is_true (andb (@eq_op nat_eqType t tg) (@eq_op (seq_eqType nat_eqType) c cnt)) *)
(* Lemma msg_spec_consume' s from to tg cnt cond i : *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
(*   valid s ->  *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) x (consume_msg s i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t' c') pt to true)), @eq (Ordered.sort mid) j x *)
(* Goal: forall (i0 : Ordered.sort mid) (t : nat) (c : list nat) (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i0 (consume_msg s i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) pt to true))), is_true (andb (@eq_op nat_eqType t tg) (@eq_op (seq_eqType nat_eqType) c cnt)) *)
(*   find i s = Some {| content := TMsg tg cnt; *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
(*                      from := from; to := to; active := true |} -> *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
(*   msg_in_soup from to cond s -> *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) x (consume_msg s i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t' c') pt to true)), @eq (Ordered.sort mid) j x *)
(* Goal: forall (i0 : Ordered.sort mid) (t : nat) (c : list nat) (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i0 (consume_msg s i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) pt to true))), is_true (andb (@eq_op nat_eqType t tg) (@eq_op (seq_eqType nat_eqType) c cnt)) *)
(*   no_msg_from_to' from to cond (consume_msg s i). *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) x (consume_msg s i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t' c') pt to true)), @eq (Ordered.sort mid) j x *)
(* Goal: forall (i0 : Ordered.sort mid) (t : nat) (c : list nat) (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i0 (consume_msg s i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) pt to true))), is_true (andb (@eq_op nat_eqType t tg) (@eq_op (seq_eqType nat_eqType) c cnt)) *)
(* Proof. *)
(* Goal: forall (_ : is_true (@PCM.valid (union_mapPCM mid (msg TaggedMessage)) s)) (_ : no_msg_from_to' from to cond s), no_msg_from_to' from to cond (consume_msg s i) *)
(* move=>V E[][j][[t][c]]F H1 H2.  *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) x (consume_msg s i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t' c') pt to true)), @eq (Ordered.sort mid) j x *)
(* Goal: forall (i0 : Ordered.sort mid) (t : nat) (c : list nat) (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i0 (consume_msg s i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) pt to true))), is_true (andb (@eq_op nat_eqType t tg) (@eq_op (seq_eqType nat_eqType) c cnt)) *)
(* move=>m t' c'; rewrite /consume_msg; move: (find_some E). *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
(* case: dom_find=>// msg->_ _; case B: (m == i). *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage ms) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true)), is_true (negb (cond t c)) *)
(* - by move/eqP: B=>B; subst m; rewrite findU eqxx/= V. *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) x (consume_msg s i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t' c') pt to true)), @eq (Ordered.sort mid) j x *)
(* Goal: forall (i0 : Ordered.sort mid) (t : nat) (c : list nat) (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i0 (consume_msg s i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) pt to true))), is_true (andb (@eq_op nat_eqType t tg) (@eq_op (seq_eqType nat_eqType) c cnt)) *)
(* have X: j = i by apply: (H1 i); exists tg, cnt. *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) x (consume_msg s i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t' c') pt to true)), @eq (Ordered.sort mid) j x *)
(* Goal: forall (i0 : Ordered.sort mid) (t : nat) (c : list nat) (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i0 (consume_msg s i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) pt to true))), is_true (andb (@eq_op nat_eqType t tg) (@eq_op (seq_eqType nat_eqType) c cnt)) *)
(* subst j; rewrite findU B/=. case: b=>// E' _. *)
(* Goal: @eq bool true false *)
(* suff X: i = m by subst i; rewrite eqxx in B. *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) x (consume_msg s i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t' c') pt to true)), @eq (Ordered.sort mid) j x *)
(* Goal: forall (i0 : Ordered.sort mid) (t : nat) (c : list nat) (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i0 (consume_msg s i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) pt to true))), is_true (andb (@eq_op nat_eqType t tg) (@eq_op (seq_eqType nat_eqType) c cnt)) *)
(* by apply: (H1 m); exists t', c'.  *)
(* Qed. *)
