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 Protocols Worlds NetworkSem.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m')))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
(* Rely-transitions of the network in the presence of the given world *)

Section Rely.

Variable w : world.
Variable this: nid.

Notation getl := (getLocal).
Notation gets := getStatelet.
Notation getp := (@getProtocol _ w).

(* The following is the "rely" relation *)
Fixpoint network_rely' n s1 s2 :=
(* Goal: is_true (@PCM.valid (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.pts mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) (@fresh (msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg (@t_snd (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) st) a) z to' true)) (dsoup d))) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (if @eq_op (Ordered.eqType mid) m (@fresh (msg TaggedMessage) (dsoup d)) then @Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg (@t_snd (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) st) a) z to' true) else @UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
(* Goal: forall (_ : @Coherence.sort (Protocols.nodes (getProtocol w l)) (coh (getProtocol w l)) match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l s with | Some d => d | None => empty_dstatelet end) (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l s with | Some d => d | None => empty_dstatelet end)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b))), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l s with | Some d => d | None => empty_dstatelet end (@coh_s w l s C) pf) (dstate match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l s with | Some d => d | None => empty_dstatelet end)) (consume_msg (dsoup match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l s with | Some d => d | None => empty_dstatelet end) m')))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
  if n is n'.+1
  then exists z s3,
        [/\ this != z, network_step w z s1 s3 & network_rely' n' s3 s2]
    else s1 = s2 /\ s1 \In Coh w.

Definition network_rely s1 s2 := exists n, network_rely' n s1 s2.

(* Basic properties: reflexivity and transitifity *)
Lemma rely_refl s : s \In Coh w -> network_rely s s.
(* Goal: forall _ : @InMem state s (@Mem state (PredPredType state) (Coh w)), network_rely s s *)
Proof. move=>H; by exists 0. Qed.

Lemma rely_trans s1 s2 s3 :
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m')))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
  network_rely s1 s2 -> network_rely s2 s3 -> network_rely s1 s3.
Proof.
(* Goal: forall (_ : network_rely s s') (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (getStatelet s l))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm from this true))), @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (getStatelet s' l))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm from this true)) *)
case=>n; elim: n s1 s2=>[?? [<-]|n Hi s1 s2]//.
(* Goal: forall (_ : network_rely' (S n) s1 s2) (_ : network_rely s2 s3), network_rely s1 s3 *)
move=>[z][s4][N]H1 H2 H3; case: (Hi _ _ H2 H3)=>m H4.
(* Goal: @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (getStatelet s' l))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
by exists m.+1, z, s4.
Qed.

Lemma rely_coh' n s1 s2 :
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m')))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
  network_rely' n s1 s2 -> Coh w s1 /\ Coh w s2.
Proof.
(* Goal: @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (getStatelet s' l))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
by elim:n s1=>[s1[<-]|n Hi s1]//=[z][s3][N]/step_coh[]H1 H2 /Hi[].
Qed.

Lemma rely_coh s1 s2 :
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m')))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
  network_rely s1 s2 -> Coh w s1 /\ Coh w s2.
Proof. by case=>n/rely_coh'. Qed.

(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m')))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
(* With the rely-steps, this' local is untouched *)
Lemma rely_loc s1 s2 l:
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m')))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
  network_rely s1 s2 -> find this (dstate (gets s1 l)) = find this (dstate (gets s2 l)).
Proof.
(* Goal: forall (_ : network_rely s s') (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (getStatelet s l))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b))), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (getStatelet s' l))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
case=>n; elim: n s1=>/=[s1 [E C]|n Ih s1 [z][s''][N]S R]; first by subst s2.
(* Goal: @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (getStatelet s' l))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
by rewrite -(@Ih s'' R); clear R Ih; apply: (step_is_local l S N).
Qed.

Lemma step_consume_other l s s' m tm from z:
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m')))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
  this != z -> network_step w z s s' ->
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m')))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
  find m (dsoup (gets s l)) = Some (Msg tm from this true) ->
  find m (dsoup (gets s' l)) = Some (Msg tm from this true).
Proof.
(* Goal: forall _ : network_rely i j, @eq Heap.heap (getLocal this (getStatelet j l)) (getLocal this (getStatelet i l)) *)
move=>N S.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m')))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
case: (S)=>[[H1 <-] | k st _ to a loc' pf D C S' Pf Spf ->/= |
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m')))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
            k rt _ m' from' pf D C tm' T [H2 H3->/=]]//;
move: (coh_coh l C);                                                         
rewrite /gets findU; case B: (l == k)=>//=; move/eqP: B=>B; subst k;
rewrite (stepV1 S).
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m')))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
- case: (dom_find l s)=>[|d->_]; first by move/find_none; rewrite D.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m')))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
  move=> C' E; rewrite -E; rewrite joinC findPtUn2; last first.
(* Goal: is_true (@PCM.valid (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.pts mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) (@fresh (msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg (@t_snd (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) st) a) z to' true)) (dsoup d))) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (if @eq_op (Ordered.eqType mid) m (@fresh (msg TaggedMessage) (dsoup d)) then @Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg (@t_snd (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) st) a) z to' true) else @UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
(* Goal: forall (_ : @Coherence.sort (Protocols.nodes (getProtocol w l)) (coh (getProtocol w l)) match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l s with | Some d => d | None => empty_dstatelet end) (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l s with | Some d => d | None => empty_dstatelet end)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b))), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l s with | Some d => d | None => empty_dstatelet end (@coh_s w l s C) pf) (dstate match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l s with | Some d => d | None => empty_dstatelet end)) (consume_msg (dsoup match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l s with | Some d => d | None => empty_dstatelet end) m')))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
  + rewrite joinC valid_fresh; apply: (cohVs C').
(* Goal: @eq (option (msg TaggedMessage)) (if @eq_op (Ordered.eqType mid) m (@fresh (msg TaggedMessage) (dsoup d)) then @Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg (@t_snd (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) st) a) z to true) else @UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) *)
(* Goal: forall (_ : @Coherence.sort (Protocols.nodes (getProtocol w l)) (coh (getProtocol w l)) match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l s with | Some d => d | None => empty_dstatelet end) (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l s with | Some d => d | None => empty_dstatelet end)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm from this true))), @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l s with | Some d => d | None => empty_dstatelet end (@coh_s w l s C) pf) (dstate match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l s with | Some d => d | None => empty_dstatelet end)) (consume_msg (dsoup match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l s with | Some d => d | None => empty_dstatelet end) m')))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm from this true)) *)
  case: ifP=>///eqP; move/find_some: E=>F Z.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m')))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
  by move/negbTE: (dom_fresh (dsoup d)); rewrite -Z F.
(* Goal: forall (_ : @Coherence.sort (Protocols.nodes (getProtocol w l)) (coh (getProtocol w l)) match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l s with | Some d => d | None => empty_dstatelet end) (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l s with | Some d => d | None => empty_dstatelet end)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm from this true))), @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l s with | Some d => d | None => empty_dstatelet end (@coh_s w l s C) pf) (dstate match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l s with | Some d => d | None => empty_dstatelet end)) (consume_msg (dsoup match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l s with | Some d => d | None => empty_dstatelet end) m')))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm from this true)) *)
move: H2=>{H3}; move: (coh_s l C) pf; rewrite /gets.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m')))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
case: (dom_find l s)=>[|d-> _ C' pf H2 _]; first by move/find_none; rewrite D. 
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm from this true)), @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m')))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm from this true)) *)
case B: (m == m'); do[move/eqP: B=>Z; subst|move=>H]. 
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m')))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
- by rewrite H2; case=>Z1 Z2 Z3; subst z; move/negbTE: N; rewrite eqxx.
(* Well, this should be easier *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm from this true)), @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m')))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm from this true)) *)
rewrite /consume_msg; case B: (find m' (dsoup d))=>[v|]//= H.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m')))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
by rewrite findU; move/eqP/negbTE: Z=>->/=.
Qed.  

(* Nobody consumes my messages *)
Lemma rely_consume_other l s s' m tm from:
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m')))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
  network_rely s s' ->
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m')))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
  find m (dsoup (gets s l)) = Some (Msg tm from this true) ->
  find m (dsoup (gets s' l)) = Some (Msg tm from this true).
Proof.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m')))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
case=>n; elim: n s=>/=[?[-> C]|n Ih s [z][s''][N] S R E]//.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m')))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
by rewrite -(@Ih s'' R)=>//; clear Ih; apply: (step_consume_other N S).
Qed.

Lemma step_send_other l s s' m tm to b z:
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m')))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
  this != z -> network_step w z s s' ->
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m')))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
  find m (dsoup (gets s' l)) = Some (Msg tm this to b) ->
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m')))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
  exists b', find m (dsoup (gets s l)) = Some (Msg tm this to b') /\ (b -> b').
Proof.
(* Goal: forall _ : network_rely i j, @eq Heap.heap (getLocal this (getStatelet j l)) (getLocal this (getStatelet i l)) *)
move=>N S.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m')))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
case: (S)=>[[H1 <-->] | k st _ to' a loc' pf D C S' Ph Spf ->/= |
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m')))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
            k rt _ m' from' pf D C tm' T [H2 H3->/=]]//; do?[by exists b];
move: (coh_coh l C);                                                         
rewrite /gets findU; case B: (l == k)=>//=; do?[by exists b];
move/eqP: B=>B; subst k; rewrite (stepV1 S).
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m')))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
- case: (dom_find l s)=>[|d->_ C']; first by move/find_none; rewrite D.
(* Goal: forall (_ : network_rely s s') (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (getStatelet s l))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b))), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (getStatelet s' l))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
  rewrite joinC findPtUn2; last first.
(* Goal: is_true (@PCM.valid (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.pts mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) (@fresh (msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg (@t_snd (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) st) a) z to' true)) (dsoup d))) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (if @eq_op (Ordered.eqType mid) m (@fresh (msg TaggedMessage) (dsoup d)) then @Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg (@t_snd (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) st) a) z to' true) else @UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
(* Goal: forall (_ : @Coherence.sort (Protocols.nodes (getProtocol w l)) (coh (getProtocol w l)) match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l s with | Some d => d | None => empty_dstatelet end) (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l s with | Some d => d | None => empty_dstatelet end)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b))), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l s with | Some d => d | None => empty_dstatelet end (@coh_s w l s C) pf) (dstate match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l s with | Some d => d | None => empty_dstatelet end)) (consume_msg (dsoup match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l s with | Some d => d | None => empty_dstatelet end) m')))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
  + rewrite joinC valid_fresh; apply: (cohVs C').
(* Goal: forall (_ : network_rely s s') (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (getStatelet s l))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b))), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (getStatelet s' l))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
  case B: (m == fresh (dsoup d)); first by case=>_ Z _; subst; move/eqP: N.
(* Goal: @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (getStatelet s' l))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
  by move=>H; exists b; split.
move: H2; move: (coh_s l C) pf; rewrite /gets;
case B: (m == m'); do[move/eqP: B=>Z; subst m'|];
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m')))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
case: (dom_find l s)=>[|d->_ C' pf H2 _]; do?[by move=>->? ? _; rewrite/consume_msg !find0E].
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m')))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
- rewrite /consume_msg; case B: (find m (dsoup d))=>[v|]; last by rewrite B.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@Some (msg TaggedMessage) v) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@mark_msg TaggedMessage v) (dsoup d))))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m')))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
  rewrite /mark_msg findU eqxx/= (cohVs C')/==>E; rewrite B in H2; clear B.
(* Goal: @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (@content TaggedMessage v) (@from TaggedMessage v) (@State.to TaggedMessage v) false)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m')))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
  case: v H2 E=>c x y a; case=>Z1 Z2 Z3 Z4; subst c x y a=>/=.
(* Goal: @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (getStatelet s' l))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
  by case=>Z1 Z2 Z3 Z4; subst b to from' tm'; exists true; split.
(* Goal: forall (_ : network_rely s s') (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (getStatelet s l))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b))), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (getStatelet s' l))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
rewrite/consume_msg; case B': (find m' (dsoup d))=>[v|]; last by exists b.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m')))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
by rewrite findU B/==>->; exists b.
Qed.

(* A backwards lemma: no one can send messages on my behalf, i.e., no new messages appear *)
Lemma rely_send_other l s s' m tm to b:
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m')))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
  network_rely s s' ->
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m')))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
  find m (dsoup (gets s' l)) = Some (Msg tm this to b) ->
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m')))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
  exists b', find m (dsoup (gets s l)) = Some (Msg tm this to b') /\ (b -> b').
Proof.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m')))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
case=>n; elim: n s=>/=[?[-> C]|n Ih s [z][s''][N] S R E]//; first by exists b.
(* Goal: @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (getStatelet s' l))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
case: (@Ih s'' R E)=>b''[H1 H2]. 
(* Goal: @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (getStatelet s' l))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
by case: (step_send_other N S H1)=>c[H3 H4]; exists c; split=>// Z; auto.
Qed.


Lemma step_send_other' l s s' m tm to b z:
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m')))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
  this != z -> network_step w z s s' ->
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m')))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
  find m (dsoup (gets s l)) = Some (Msg tm this to b) ->
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m')))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
  exists b', find m (dsoup (gets s' l)) = Some (Msg tm this to b') /\ (b' -> b).
Proof.
(* Goal: forall _ : network_rely i j, @eq Heap.heap (getLocal this (getStatelet j l)) (getLocal this (getStatelet i l)) *)
move=>N S.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m')))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
case: (S)=>[[H1 <-->] | k st _ to' a loc' pf D C S' Ph Spf ->/= |
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m')))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
            k rt _ m' from' pf D C tm' T [H2 H3->/=]]//; do?[by exists b];
move: (coh_coh l C);                                                         
rewrite /gets findU; case B: (l == k)=>//=; do?[by exists b];
move/eqP: B=>B; subst k; rewrite (stepV1 S).
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m')))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
- case: (dom_find l s)=>[|d->_ C']; first by move/find_none; rewrite D.
(* Goal: forall (_ : network_rely s s') (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (getStatelet s l))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b))), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (getStatelet s' l))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
  rewrite joinC findPtUn2; last first.
(* Goal: is_true (@PCM.valid (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.pts mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) (@fresh (msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg (@t_snd (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) st) a) z to' true)) (dsoup d))) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (if @eq_op (Ordered.eqType mid) m (@fresh (msg TaggedMessage) (dsoup d)) then @Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg (@t_snd (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) st) a) z to' true) else @UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
(* Goal: forall (_ : @Coherence.sort (Protocols.nodes (getProtocol w l)) (coh (getProtocol w l)) match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l s with | Some d => d | None => empty_dstatelet end) (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l s with | Some d => d | None => empty_dstatelet end)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b))), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l s with | Some d => d | None => empty_dstatelet end (@coh_s w l s C) pf) (dstate match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l s with | Some d => d | None => empty_dstatelet end)) (consume_msg (dsoup match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l s with | Some d => d | None => empty_dstatelet end) m')))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
  + rewrite joinC valid_fresh; apply: (cohVs C').
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m')))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
  case B: (m == fresh (dsoup d)); last by move=>->; exists b.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg (@t_snd (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) st) a) z to' true)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
(* Goal: forall (_ : @Coherence.sort (Protocols.nodes (getProtocol w l)) (coh (getProtocol w l)) match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l s with | Some d => d | None => empty_dstatelet end) (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l s with | Some d => d | None => empty_dstatelet end)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b))), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l s with | Some d => d | None => empty_dstatelet end (@coh_s w l s C) pf) (dstate match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l s with | Some d => d | None => empty_dstatelet end)) (consume_msg (dsoup match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l s with | Some d => d | None => empty_dstatelet end) m')))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
  move/eqP:B=>B; subst m; move: (dom_fresh (dsoup d))=>B.
(* Goal: @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (getStatelet s' l))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
  by move/find_some=>E; rewrite E in B.
move: H2; move: (coh_s l C) pf; rewrite /gets;
case B: (m == m'); do[move/eqP: B=>Z; subst m'|];
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m')))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
case: (dom_find l s)=>[|d->_ C' pf H2 _]; do?[by move=>->? ? _; rewrite/consume_msg !find0E].
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m')))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
- rewrite /consume_msg; case B: (find m (dsoup d))=>[v|]; last by rewrite B.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@Some (msg TaggedMessage) v) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@mark_msg TaggedMessage v) (dsoup d))))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m')))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
  rewrite /mark_msg findU eqxx/= (cohVs C')/==>E; rewrite B in H2; clear B.
(* Goal: @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (@content TaggedMessage v) (@from TaggedMessage v) (@State.to TaggedMessage v) false)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m')))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
  case: v H2 E=>c x y a; case=>Z1 Z2 Z3 Z4; subst c x y a=>/=.
(* Goal: @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (getStatelet s' l))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
  by case=>Z1 Z2 Z3 Z4; subst b to from' tm'; exists false. 
(* Goal: forall (_ : network_rely s s') (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (getStatelet s l))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b))), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (getStatelet s' l))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
rewrite/consume_msg; case B': (find m' (dsoup d))=>[v|]; last by exists b.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m')))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
by rewrite findU B/==>->; exists b.
Qed.

(* A forward lemma: messages sent on my behalf don't disappear but might get consumed *)
Lemma rely_send_other' l s s' m tm to b:
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m')))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
  network_rely s s' ->
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m')))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
  find m (dsoup (gets s l)) = Some (Msg tm this to b) ->
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m')))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
  exists b', find m (dsoup (gets s' l)) = Some (Msg tm this to b') /\ (b' -> b).
Proof.
(* Goal: forall (_ : network_rely s s') (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (getStatelet s l))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b))), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (getStatelet s' l))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
case=>n; elim: n s b; first by move=>s b[Z C]; subst s'; exists b. 
(* Goal: forall _ : network_rely i j, @eq Heap.heap (getLocal this (getStatelet j l)) (getLocal this (getStatelet i l)) *)
move=>n Ih s b [z][s''][N] S R H.
(* Goal: @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (getStatelet s' l))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
case: (step_send_other' N S H)=>c[H3 H4].
(* Goal: @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (getStatelet s' l))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
by case: (@Ih s'' c R H3)=>b'[G1 G2]; exists b'; split=>//; auto.
Qed.

Notation loc i l := (getLocal this (getStatelet i l)).
Notation msgs i l := (dsoup (getStatelet i l)).

(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m)))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup d)) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b)), @ex bool (fun b' : bool => and (@eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (dsoup (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) z (@receive_step (Protocols.nodes (getProtocol w l)) (Protocols.coh (getProtocol w l)) rt z from' (tms_cont tm') d C' pf) (dstate d)) (consume_msg (dsoup d) m')))) (@Some (msg TaggedMessage) (@Msg TaggedMessage tm this to b'))) (forall _ : is_true b', is_true b)) *)
Lemma rely_loc' l i j : network_rely i j -> loc j l = loc i l.
Proof.
(* Goal: forall _ : network_rely i j, @eq Heap.heap (getLocal this (getStatelet j l)) (getLocal this (getStatelet i l)) *)
move => R.
(* Goal: @eq Heap.heap (getLocal this (getStatelet j l)) (getLocal this (getStatelet i l)) *)
now rewrite /getLocal(rely_loc _ R).
Qed.

End Rely.

