From mathcomp.ssreflect
Require Import ssreflect ssrbool ssrnat eqtype ssrfun seq.
From mathcomp
Require Import path.
Require Import Eqdep.
Require Import Relation_Operators.
From fcsl
Require Import pred prelude ordtype finmap pcm unionmap heap.
From DiSeL
Require Import Freshness State EqTypeX DepMaps Protocols Worlds NetworkSem.
From DiSeL
Require Import Actions Injection InductiveInv.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Section ProcessSyntax.

Variable this : nid.

(* Syntax for process *)
Inductive proc (W : world) A :=
  Unfinished | Ret of A | Act of action W A this |
(* Goal: forall (_ : match t with | Unfinished => True | Ret a => True | Act a => True | @Seq _ _ _ B p p0 => True | @Inject _ _ _ V K i p => True | WithInv p I0 ii e p0 => True end) (_ : match t with | Unfinished => False | Ret v => @ex state (fun s1' : state => and3 (@eq state s2 s1) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s1 s1')) | Act a => False | @Seq _ _ _ B p0 p1 => False | @Inject _ _ _ V K i p0 => False | WithInv p0 I0 ii e p1 => False end), or (@ex A (fun v : A => and6 (@eq schedule WithInvRet WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule WithInvRet (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
(* Goal: forall (s : schedule) (_ : @safe (mkWorld pr) A t s s1) (_ : @ex (proc this (mkWorld pr) A) (fun t2' : proc this (mkWorld pr) A => and (@eq (proc this W A) q (@WithInv this W A pr I ii pf t2')) (@step (mkWorld pr) A s1 t s s2 t2'))), or (@ex A (fun v : A => and6 (@eq schedule (WithInvStep s) WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule (WithInvStep s) (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
  Seq B of proc W B & B -> proc W A |
  Inject V K of injects V W K & proc V A |
  WithInv p I (ii : InductiveInv p I) of
          W = mkWorld (ProtocolWithIndInv ii) & proc (mkWorld p) A.  

(* Goal: forall (_ : match t with | Unfinished => True | Ret a => True | Act a => True | @Seq _ _ _ B p p0 => True | @Inject _ _ _ V K i p => True | WithInv p I0 ii e p0 => True end) (_ : match t with | Unfinished => False | Ret v => @ex state (fun s1' : state => and3 (@eq state s2 s1) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s1 s1')) | Act a => False | @Seq _ _ _ B p0 p1 => False | @Inject _ _ _ V K i p0 => False | WithInv p0 I0 ii e p1 => False end), or (@ex A (fun v : A => and6 (@eq schedule WithInvRet WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule WithInvRet (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
(* Goal: forall (s : schedule) (_ : @safe (mkWorld pr) A t s s1) (_ : @ex (proc this (mkWorld pr) A) (fun t2' : proc this (mkWorld pr) A => and (@eq (proc this W A) q (@WithInv this W A pr I ii pf t2')) (@step (mkWorld pr) A s1 t s s2 t2'))), or (@ex A (fun v : A => and6 (@eq schedule (WithInvStep s) WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule (WithInvStep s) (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
Definition pcat W A B (t : proc W A) (k : A -> Pred (proc W B)) :=
  [Pred s | exists q, s = Seq t q /\ forall x, q x \In k x].

Inductive schedule :=
  ActStep | SeqRet | SeqStep of schedule |  
  InjectStep of schedule | InjectRet |
  WithInvStep of schedule | WithInvRet.

End ProcessSyntax.

Arguments Unfinished [this W A].
Arguments Ret [this W A].
Arguments Act [this W A].
Arguments Seq [this W A B].
Arguments WithInv [this W A].

Section ProcessSemantics.

Variable this : nid.

Fixpoint step (W : world) A (s1 : state) (p1 : proc this W A)
         sc (s2 : state) (p2 : proc this W A) : Prop :=
  match sc, p1 with
(* Goal: forall (_ : match t with | Unfinished => True | Ret a => True | Act a => True | @Seq _ _ _ B p p0 => True | @Inject _ _ _ V K i p => True | WithInv p I0 ii e p0 => True end) (_ : match t with | Unfinished => False | Ret v => @ex state (fun s1' : state => and3 (@eq state s2 s1) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s1 s1')) | Act a => False | @Seq _ _ _ B p0 p1 => False | @Inject _ _ _ V K i p0 => False | WithInv p0 I0 ii e p1 => False end), or (@ex A (fun v : A => and6 (@eq schedule WithInvRet WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule WithInvRet (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
(* Goal: forall (s : schedule) (_ : @safe (mkWorld pr) A t s s1) (_ : @ex (proc this (mkWorld pr) A) (fun t2' : proc this (mkWorld pr) A => and (@eq (proc this W A) q (@WithInv this W A pr I ii pf t2')) (@step (mkWorld pr) A s1 t s s2 t2'))), or (@ex A (fun v : A => and6 (@eq schedule (WithInvStep s) WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule (WithInvStep s) (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
  (* Action - make a step *)  
  | ActStep, Act a => exists v pf, @a_step _ _ _ a s1 pf s2 v /\ p2 = Ret v
(* Goal: forall (_ : match t with | Unfinished => True | Ret a => True | Act a => True | @Seq _ _ _ B p p0 => True | @Inject _ _ _ V K i p => True | WithInv p I0 ii e p0 => True end) (_ : match t with | Unfinished => False | Ret v => @ex state (fun s1' : state => and3 (@eq state s2 s1) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s1 s1')) | Act a => False | @Seq _ _ _ B p0 p1 => False | @Inject _ _ _ V K i p0 => False | WithInv p0 I0 ii e p1 => False end), or (@ex A (fun v : A => and6 (@eq schedule WithInvRet WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule WithInvRet (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
(* Goal: forall (s : schedule) (_ : @safe (mkWorld pr) A t s s1) (_ : @ex (proc this (mkWorld pr) A) (fun t2' : proc this (mkWorld pr) A => and (@eq (proc this W A) q (@WithInv this W A pr I ii pf t2')) (@step (mkWorld pr) A s1 t s s2 t2'))), or (@ex A (fun v : A => and6 (@eq schedule (WithInvStep s) WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule (WithInvStep s) (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
  (* Sequencing - apply a continuation *)  
  | SeqRet, Seq _ (Ret v) k => s2 = s1 /\ p2 = k v
  | SeqStep sc', Seq _ p' k1 => 
    exists p'', step s1 p' sc' s2 p'' /\ p2 = Seq p'' k1
(* Goal: forall (_ : match t with | Unfinished => True | Ret a => True | Act a => True | @Seq _ _ _ B p p0 => True | @Inject _ _ _ V K i p => True | WithInv p I0 ii e p0 => True end) (_ : match t with | Unfinished => False | Ret v => @ex state (fun s1' : state => and3 (@eq state s2 s1) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s1 s1')) | Act a => False | @Seq _ _ _ B p0 p1 => False | @Inject _ _ _ V K i p0 => False | WithInv p0 I0 ii e p1 => False end), or (@ex A (fun v : A => and6 (@eq schedule WithInvRet WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule WithInvRet (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
(* Goal: forall (s : schedule) (_ : @safe (mkWorld pr) A t s s1) (_ : @ex (proc this (mkWorld pr) A) (fun t2' : proc this (mkWorld pr) A => and (@eq (proc this W A) q (@WithInv this W A pr I ii pf t2')) (@step (mkWorld pr) A s1 t s s2 t2'))), or (@ex A (fun v : A => and6 (@eq schedule (WithInvStep s) WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule (WithInvStep s) (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
  (* Injection of a non-reduced term *)
  | InjectRet, Inject V K pf (Ret v) =>
     exists s1', [/\ s2 = s1, p2 = Ret v & extends pf s1 s1']
  | InjectStep sc', Inject V K pf t1' =>
    exists s1' s2' s t2', 
(* Goal: forall _ : @ex A (fun v : A => and6 (@eq schedule sc WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii)))), @pstep W A s1 (@WithInv this W A pr I ii pf t) sc s2 q *)
(* Goal: forall _ : @ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule sc (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t'))), @pstep W A s1 (@WithInv this W A pr I ii pf t) sc s2 q *)
(* Goal: forall _ : @pstep W A s1 (@WithInv this W A pr I ii pf t) sc s2 q, or (@ex A (fun v : A => and6 (@eq schedule sc WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule sc (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
    [/\ p2 = Inject pf t2', s1 = s1' \+ s, s2 = s2' \+ s, 
     s1' \In Coh V & step s1' t1' sc' s2' t2']
(* Goal: forall (_ : match t with | Unfinished => True | Ret a => True | Act a => True | @Seq _ _ _ B p p0 => True | @Inject _ _ _ V K i p => True | WithInv p I0 ii e p0 => True end) (_ : match t with | Unfinished => False | Ret v => @ex state (fun s1' : state => and3 (@eq state s2 s1) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s1 s1')) | Act a => False | @Seq _ _ _ B p0 p1 => False | @Inject _ _ _ V K i p0 => False | WithInv p0 I0 ii e p1 => False end), or (@ex A (fun v : A => and6 (@eq schedule WithInvRet WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule WithInvRet (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
(* Goal: forall (s : schedule) (_ : @safe (mkWorld pr) A t s s1) (_ : @ex (proc this (mkWorld pr) A) (fun t2' : proc this (mkWorld pr) A => and (@eq (proc this W A) q (@WithInv this W A pr I ii pf t2')) (@step (mkWorld pr) A s1 t s s2 t2'))), or (@ex A (fun v : A => and6 (@eq schedule (WithInvStep s) WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule (WithInvStep s) (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
  (* Imposing an inductive invariant on a non-reduced term *)
  | WithInvRet, WithInv p inv ii pf (Ret v) =>
     exists s1', [/\ s2 = s1, p2 = Ret v & s1 = s1']
  | WithInvStep sc', WithInv p inv ii pf t1' =>
    exists t2', p2 = WithInv p inv ii pf t2' /\  
                     step s1 t1' sc' s2 t2'   
  | _, _ => False
  end.

Fixpoint good (W : world) A (p : proc this W A) sc  : Prop :=
  match sc, p with
  | ActStep, Act _ => True
  | SeqRet, Seq _ (Ret _) _ => True
  | SeqStep sc', Seq _ p' _ => good p' sc'
  | InjectStep sc', Inject _ _ _ p' => good p' sc'
  | InjectRet, Inject _ _ _ (Ret _) => True
  | WithInvStep sc', WithInv _ _ _ _ p' => good p' sc'
  | WithInvRet, WithInv _ _ _ _ (Ret _) => True
  | _, _ => False
  end.

(*

(* Goal: forall (_ : match t with | Unfinished => True | Ret a => True | Act a => True | @Seq _ _ _ B p p0 => True | @Inject _ _ _ V K i p => True | WithInv p I0 ii e p0 => True end) (_ : match t with | Unfinished => False | Ret v => @ex state (fun s1' : state => and3 (@eq state s2 s1) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s1 s1')) | Act a => False | @Seq _ _ _ B p0 p1 => False | @Inject _ _ _ V K i p0 => False | WithInv p0 I0 ii e p1 => False end), or (@ex A (fun v : A => and6 (@eq schedule WithInvRet WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule WithInvRet (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
(* Goal: forall (s : schedule) (_ : @safe (mkWorld pr) A t s s1) (_ : @ex (proc this (mkWorld pr) A) (fun t2' : proc this (mkWorld pr) A => and (@eq (proc this W A) q (@WithInv this W A pr I ii pf t2')) (@step (mkWorld pr) A s1 t s s2 t2'))), or (@ex A (fun v : A => and6 (@eq schedule (WithInvStep s) WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule (WithInvStep s) (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
[Safety in small-step semantics]

The safety (in order to make the following step) with respect to the
schedule is defined inductively on the shape of the program and the
schedule. Omitting the schedule is not a good idea, at it's required
in order to "sequentialize" the execution of the program
structure. Once it's dropped, this structure is lost.

 *)

Fixpoint safe (W : world) A (p : proc this W A) sc (s : state)  : Prop :=
  match sc, p with
  | ActStep, Act a => a_safe a s
  | SeqRet, Seq _ (Ret _) _ => True
  | SeqStep sc', Seq _ p' _ => safe p' sc' s
  | InjectStep sc', Inject V K pf p' =>
      exists s', extends pf s s' /\ safe p' sc' s'
  | InjectRet, Inject V K pf (Ret _) => exists s', extends pf s s'
  | WithInvStep sc', WithInv _ _ _ _ p' => safe p' sc' s
  | WithInvRet, WithInv _ _ _ _ (Ret _) => True
  | _, _ => True
  end.

Definition pstep (W : world) A s1 (p1 : proc this W A) sc s2 p2 := 
  [/\ s1 \In Coh W, safe p1 sc s1 & step s1 p1 sc s2 p2].

(* Some sanity lemmas wrt. stepping *)

Lemma pstep_safe (W : world) A s1 (t : proc this W A) sc s2 q : 
(* Goal: forall (_ : match t with | Unfinished => True | Ret a => True | Act a => True | @Seq _ _ _ B p p0 => True | @Inject _ _ _ V K i p => True | WithInv p I0 ii e p0 => True end) (_ : match t with | Unfinished => False | Ret v => @ex state (fun s1' : state => and3 (@eq state s2 s1) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s1 s1')) | Act a => False | @Seq _ _ _ B p0 p1 => False | @Inject _ _ _ V K i p0 => False | WithInv p0 I0 ii e p1 => False end), or (@ex A (fun v : A => and6 (@eq schedule WithInvRet WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule WithInvRet (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
(* Goal: forall (s : schedule) (_ : @safe (mkWorld pr) A t s s1) (_ : @ex (proc this (mkWorld pr) A) (fun t2' : proc this (mkWorld pr) A => and (@eq (proc this W A) q (@WithInv this W A pr I ii pf t2')) (@step (mkWorld pr) A s1 t s s2 t2'))), or (@ex A (fun v : A => and6 (@eq schedule (WithInvStep s) WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule (WithInvStep s) (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
        pstep s1 t sc s2 q -> safe t sc s1.
(* Goal: forall (_ : @InMem state s1 (@Mem state (PredPredType state) (Coh (mkWorld (@ProtocolWithIndInv pr I ii))))) (_ : @pstep (mkWorld pr) A s1 t sc s2 t'), @InMem state s2 (@Mem state (PredPredType state) (Coh (mkWorld (@ProtocolWithIndInv pr I ii)))) *)
Proof. by case. Qed.


(*

The following lemma established the operational "progress" property: a
program, which is safe and also the schedule is appropriate. Together,
this implies that we can do a step. 
 *)

Lemma proc_progress W A s (p : proc this W A) sc : 
(* Goal: forall (_ : match t with | Unfinished => True | Ret a => True | Act a => True | @Seq _ _ _ B p p0 => True | @Inject _ _ _ V K i p => True | WithInv p I0 ii e p0 => True end) (_ : match t with | Unfinished => False | Ret v => @ex state (fun s1' : state => and3 (@eq state s2 s1) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s1 s1')) | Act a => False | @Seq _ _ _ B p0 p1 => False | @Inject _ _ _ V K i p0 => False | WithInv p0 I0 ii e p1 => False end), or (@ex A (fun v : A => and6 (@eq schedule WithInvRet WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule WithInvRet (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
(* Goal: forall (s : schedule) (_ : @safe (mkWorld pr) A t s s1) (_ : @ex (proc this (mkWorld pr) A) (fun t2' : proc this (mkWorld pr) A => and (@eq (proc this W A) q (@WithInv this W A pr I ii pf t2')) (@step (mkWorld pr) A s1 t s s2 t2'))), or (@ex A (fun v : A => and6 (@eq schedule (WithInvStep s) WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule (WithInvStep s) (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
        s \In Coh W -> safe p sc s -> good p sc ->  
        exists s' (p' : proc this W A), pstep s p sc s' p'.
Proof.
(* Goal: forall (_ : @InMem state s (@Mem state (PredPredType state) (Coh W))) (_ : @safe W A p sc s) (_ : @good W A p sc), @ex state (fun s' : state => @ex (proc this W A) (fun p' : proc this W A => @pstep W A s p sc s' p')) *)
move=>C H1 H2; elim: sc W A s p H2 H1 C=>[||sc IH|sc IH||sc IH|]W A s. 
(* Goal: forall (_ : match t with | Unfinished => True | Ret a => True | Act a => True | @Seq _ _ _ B p p0 => True | @Inject _ _ _ V K i p => True | WithInv p I0 ii e p0 => True end) (_ : match t with | Unfinished => False | Ret v => @ex state (fun s1' : state => and3 (@eq state s2 s1) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s1 s1')) | Act a => False | @Seq _ _ _ B p0 p1 => False | @Inject _ _ _ V K i p0 => False | WithInv p0 I0 ii e p1 => False end), or (@ex A (fun v : A => and6 (@eq schedule WithInvRet WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule WithInvRet (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
(* Goal: forall (s : schedule) (_ : @safe (mkWorld pr) A t s s1) (_ : @ex (proc this (mkWorld pr) A) (fun t2' : proc this (mkWorld pr) A => and (@eq (proc this W A) q (@WithInv this W A pr I ii pf t2')) (@step (mkWorld pr) A s1 t s s2 t2'))), or (@ex A (fun v : A => and6 (@eq schedule (WithInvStep s) WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule (WithInvStep s) (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
- case=>//=a _/= H; move/a_step_total: (H)=>[s'][r]H'.
(* Goal: forall (_ : @InMem state s1 (@Mem state (PredPredType state) (Coh (mkWorld (@ProtocolWithIndInv pr I ii))))) (_ : @pstep (mkWorld pr) A s1 t sc s2 t'), @InMem state s2 (@Mem state (PredPredType state) (Coh (mkWorld (@ProtocolWithIndInv pr I ii)))) *)
  by exists s', (Ret r); split=>//=; exists r, H.  
(* Goal: forall (_ : match t with | Unfinished => True | Ret a => True | Act a => True | @Seq _ _ _ B p p0 => True | @Inject _ _ _ V K i p => True | WithInv p I0 ii e p0 => True end) (_ : match t with | Unfinished => False | Ret v => @ex state (fun s1' : state => and3 (@eq state s2 s1) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s1 s1')) | Act a => False | @Seq _ _ _ B p0 p1 => False | @Inject _ _ _ V K i p0 => False | WithInv p0 I0 ii e p1 => False end), or (@ex A (fun v : A => and6 (@eq schedule WithInvRet WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule WithInvRet (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
(* Goal: forall (s : schedule) (_ : @safe (mkWorld pr) A t s s1) (_ : @ex (proc this (mkWorld pr) A) (fun t2' : proc this (mkWorld pr) A => and (@eq (proc this W A) q (@WithInv this W A pr I ii pf t2')) (@step (mkWorld pr) A s1 t s s2 t2'))), or (@ex A (fun v : A => and6 (@eq schedule (WithInvStep s) WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule (WithInvStep s) (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
- by case=>//; move=>B p k/=; case: p=>//b _ _; exists s, (k b). 
(* Goal: forall (_ : match t with | Unfinished => True | Ret a => True | Act a => True | @Seq _ _ _ B p p0 => True | @Inject _ _ _ V K i p => True | WithInv p I0 ii e p0 => True end) (_ : match t with | Unfinished => False | Ret v => @ex state (fun s1' : state => and3 (@eq state s2 s1) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s1 s1')) | Act a => False | @Seq _ _ _ B p0 p1 => False | @Inject _ _ _ V K i p0 => False | WithInv p0 I0 ii e p1 => False end), or (@ex A (fun v : A => and6 (@eq schedule WithInvRet WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule WithInvRet (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
(* Goal: forall (s : schedule) (_ : @safe (mkWorld pr) A t s s1) (_ : @ex (proc this (mkWorld pr) A) (fun t2' : proc this (mkWorld pr) A => and (@eq (proc this W A) q (@WithInv this W A pr I ii pf t2')) (@step (mkWorld pr) A s1 t s s2 t2'))), or (@ex A (fun v : A => and6 (@eq schedule (WithInvStep s) WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule (WithInvStep s) (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
- case=>//B p k/=H1 H2 C.
(* Goal: forall (_ : match t with | Unfinished => True | Ret a => @ex (UMDef.tp Label dstatelet) (fun s' : UMDef.tp Label dstatelet => @extends V W K em s1 s') | Act a => True | @Seq _ _ _ B p p0 => True | @Inject _ _ _ V0 K i p => True | WithInv p I0 ii e p0 => True end) (_ : match t with | Unfinished => False | Ret v => @ex (UMDef.tp Label dstatelet) (fun s1' : UMDef.tp Label dstatelet => and3 (@eq state s2 s1) (@eq (proc this W A) q (@Ret this W A v)) (@extends V W K em s1 s1')) | Act a => False | @Seq _ _ _ B p0 p1 => False | @Inject _ _ _ V0 K i p0 => False | WithInv p0 I0 ii e p1 => False end), or (@ex (UMDef.tp Label dstatelet) (fun s1' : UMDef.tp Label dstatelet => @ex A (fun v : A => and5 (@eq schedule InjectRet InjectRet) (@eq (proc this V A) t (@Ret this V A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@extends V W K em s1 s1')))) (@ex schedule (fun sc' : schedule => @ex (proc this V A) (fun t' : proc this V A => @ex (UMDef.tp Label dstatelet) (fun s1' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun s2' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun s : UMDef.tp Label dstatelet => and6 (@eq schedule InjectRet (InjectStep sc')) (@eq (proc this W A) q (@Inject this W A V K em t')) (@eq state s1 (@PCM.join (union_mapPCM Label dstatelet) s1' s)) (@eq state s2 (@PCM.join (union_mapPCM Label dstatelet) s2' s)) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep V A s1' t sc' s2' t'))))))) *)
(* Goal: forall (s : schedule) (_ : @ex (UMDef.tp Label dstatelet) (fun s' : UMDef.tp Label dstatelet => and (@extends V W K em s1 s') (@safe V A t s s'))) (_ : @ex (UMDef.tp Label dstatelet) (fun s1' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun s2' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun s0 : UMDef.tp Label dstatelet => @ex (proc this V A) (fun t2' : proc this V A => and5 (@eq (proc this W A) q (@Inject this W A V K em t2')) (@eq state s1 (@PCM.join (union_mapPCM Label dstatelet) s1' s0)) (@eq state s2 (@PCM.join (union_mapPCM Label dstatelet) s2' s0)) (@InMem (UMDef.tp Label dstatelet) s1' (@Mem state (PredPredType state) (Coh V))) (@step V A s1' t s s2' t2')))))), or (@ex (UMDef.tp Label dstatelet) (fun s1' : UMDef.tp Label dstatelet => @ex A (fun v : A => and5 (@eq schedule (InjectStep s) InjectRet) (@eq (proc this V A) t (@Ret this V A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@extends V W K em s1 s1')))) (@ex schedule (fun sc' : schedule => @ex (proc this V A) (fun t' : proc this V A => @ex (UMDef.tp Label dstatelet) (fun s1' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun s2' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun s0 : UMDef.tp Label dstatelet => and6 (@eq schedule (InjectStep s) (InjectStep sc')) (@eq (proc this W A) q (@Inject this W A V K em t')) (@eq state s1 (@PCM.join (union_mapPCM Label dstatelet) s1' s0)) (@eq state s2 (@PCM.join (union_mapPCM Label dstatelet) s2' s0)) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep V A s1' t sc' s2' t'))))))) *)
  case: (IH W B s p H1 H2 C)=>s'[p'][G1 G2].
(* Goal: forall (_ : @InMem state s1 (@Mem state (PredPredType state) (Coh (mkWorld (@ProtocolWithIndInv pr I ii))))) (_ : @pstep (mkWorld pr) A s1 t sc s2 t'), @InMem state s2 (@Mem state (PredPredType state) (Coh (mkWorld (@ProtocolWithIndInv pr I ii)))) *)
  by exists s', (Seq p' k); split=>//; exists p'. 
(* Goal: forall (_ : match t with | Unfinished => True | Ret a => True | Act a => True | @Seq _ _ _ B p p0 => True | @Inject _ _ _ V K i p => True | WithInv p I0 ii e p0 => True end) (_ : match t with | Unfinished => False | Ret v => @ex state (fun s1' : state => and3 (@eq state s2 s1) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s1 s1')) | Act a => False | @Seq _ _ _ B p0 p1 => False | @Inject _ _ _ V K i p0 => False | WithInv p0 I0 ii e p1 => False end), or (@ex A (fun v : A => and6 (@eq schedule WithInvRet WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule WithInvRet (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
(* Goal: forall (s : schedule) (_ : @safe (mkWorld pr) A t s s1) (_ : @ex (proc this (mkWorld pr) A) (fun t2' : proc this (mkWorld pr) A => and (@eq (proc this W A) q (@WithInv this W A pr I ii pf t2')) (@step (mkWorld pr) A s1 t s s2 t2'))), or (@ex A (fun v : A => and6 (@eq schedule (WithInvStep s) WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule (WithInvStep s) (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
- case=>// V K pf p/=H1 [z][E]H2 C. 
(* Goal: forall (_ : match t with | Unfinished => True | Ret a => @ex (UMDef.tp Label dstatelet) (fun s' : UMDef.tp Label dstatelet => @extends V W K em s1 s') | Act a => True | @Seq _ _ _ B p p0 => True | @Inject _ _ _ V0 K i p => True | WithInv p I0 ii e p0 => True end) (_ : match t with | Unfinished => False | Ret v => @ex (UMDef.tp Label dstatelet) (fun s1' : UMDef.tp Label dstatelet => and3 (@eq state s2 s1) (@eq (proc this W A) q (@Ret this W A v)) (@extends V W K em s1 s1')) | Act a => False | @Seq _ _ _ B p0 p1 => False | @Inject _ _ _ V0 K i p0 => False | WithInv p0 I0 ii e p1 => False end), or (@ex (UMDef.tp Label dstatelet) (fun s1' : UMDef.tp Label dstatelet => @ex A (fun v : A => and5 (@eq schedule InjectRet InjectRet) (@eq (proc this V A) t (@Ret this V A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@extends V W K em s1 s1')))) (@ex schedule (fun sc' : schedule => @ex (proc this V A) (fun t' : proc this V A => @ex (UMDef.tp Label dstatelet) (fun s1' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun s2' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun s : UMDef.tp Label dstatelet => and6 (@eq schedule InjectRet (InjectStep sc')) (@eq (proc this W A) q (@Inject this W A V K em t')) (@eq state s1 (@PCM.join (union_mapPCM Label dstatelet) s1' s)) (@eq state s2 (@PCM.join (union_mapPCM Label dstatelet) s2' s)) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep V A s1' t sc' s2' t'))))))) *)
(* Goal: forall (s : schedule) (_ : @ex (UMDef.tp Label dstatelet) (fun s' : UMDef.tp Label dstatelet => and (@extends V W K em s1 s') (@safe V A t s s'))) (_ : @ex (UMDef.tp Label dstatelet) (fun s1' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun s2' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun s0 : UMDef.tp Label dstatelet => @ex (proc this V A) (fun t2' : proc this V A => and5 (@eq (proc this W A) q (@Inject this W A V K em t2')) (@eq state s1 (@PCM.join (union_mapPCM Label dstatelet) s1' s0)) (@eq state s2 (@PCM.join (union_mapPCM Label dstatelet) s2' s0)) (@InMem (UMDef.tp Label dstatelet) s1' (@Mem state (PredPredType state) (Coh V))) (@step V A s1' t s s2' t2')))))), or (@ex (UMDef.tp Label dstatelet) (fun s1' : UMDef.tp Label dstatelet => @ex A (fun v : A => and5 (@eq schedule (InjectStep s) InjectRet) (@eq (proc this V A) t (@Ret this V A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@extends V W K em s1 s1')))) (@ex schedule (fun sc' : schedule => @ex (proc this V A) (fun t' : proc this V A => @ex (UMDef.tp Label dstatelet) (fun s1' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun s2' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun s0 : UMDef.tp Label dstatelet => and6 (@eq schedule (InjectStep s) (InjectStep sc')) (@eq (proc this W A) q (@Inject this W A V K em t')) (@eq state s1 (@PCM.join (union_mapPCM Label dstatelet) s1' s0)) (@eq state s2 (@PCM.join (union_mapPCM Label dstatelet) s2' s0)) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep V A s1' t sc' s2' t'))))))) *)
  case: (E)=>s3[Z] C1 C2.
(* Goal: forall (p : proc this W A) (_ : @good W A p WithInvRet) (_ : @safe W A p WithInvRet s) (_ : @InMem state s (@Mem state (PredPredType state) (Coh W))), @ex state (fun s' : state => @ex (proc this W A) (fun p' : proc this W A => @pstep W A s p WithInvRet s' p')) *)
  case: (IH V A z p H1 H2 C1) =>s'[p']H3; case: H3=>S St.
(* Goal: forall _ : @pstep W A s1 (@WithInv this W A pr I ii pf t) sc s2 q, or (@ex A (fun v : A => and6 (@eq schedule sc WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule sc (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
  exists (s' \+ s3), (Inject pf p'); split=>//; first by exists z.  
(* Goal: forall (_ : @InMem state s1 (@Mem state (PredPredType state) (Coh (mkWorld (@ProtocolWithIndInv pr I ii))))) (_ : @pstep (mkWorld pr) A s1 t sc s2 t'), @InMem state s2 (@Mem state (PredPredType state) (Coh (mkWorld (@ProtocolWithIndInv pr I ii)))) *)
  by subst s; exists z, s', s3, p'. 
(* Goal: forall (_ : match t with | Unfinished => True | Ret a => True | Act a => True | @Seq _ _ _ B p p0 => True | @Inject _ _ _ V K i p => True | WithInv p I0 ii e p0 => True end) (_ : match t with | Unfinished => False | Ret v => @ex state (fun s1' : state => and3 (@eq state s2 s1) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s1 s1')) | Act a => False | @Seq _ _ _ B p0 p1 => False | @Inject _ _ _ V K i p0 => False | WithInv p0 I0 ii e p1 => False end), or (@ex A (fun v : A => and6 (@eq schedule WithInvRet WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule WithInvRet (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
(* Goal: forall (s : schedule) (_ : @safe (mkWorld pr) A t s s1) (_ : @ex (proc this (mkWorld pr) A) (fun t2' : proc this (mkWorld pr) A => and (@eq (proc this W A) q (@WithInv this W A pr I ii pf t2')) (@step (mkWorld pr) A s1 t s s2 t2'))), or (@ex A (fun v : A => and6 (@eq schedule (WithInvStep s) WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule (WithInvStep s) (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
- case=>//V K pf; case=>// v/=_[s'] E C.          
(* Goal: forall (_ : @InMem state s1 (@Mem state (PredPredType state) (Coh (mkWorld (@ProtocolWithIndInv pr I ii))))) (_ : @pstep (mkWorld pr) A s1 t sc s2 t'), @InMem state s2 (@Mem state (PredPredType state) (Coh (mkWorld (@ProtocolWithIndInv pr I ii)))) *)
  by exists s, (Ret v); split=>//=; exists s'.
(* Goal: forall (_ : match t with | Unfinished => True | Ret a => True | Act a => True | @Seq _ _ _ B p p0 => True | @Inject _ _ _ V K i p => True | WithInv p I0 ii e p0 => True end) (_ : match t with | Unfinished => False | Ret v => @ex state (fun s1' : state => and3 (@eq state s2 s1) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s1 s1')) | Act a => False | @Seq _ _ _ B p0 p1 => False | @Inject _ _ _ V K i p0 => False | WithInv p0 I0 ii e p1 => False end), or (@ex A (fun v : A => and6 (@eq schedule WithInvRet WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule WithInvRet (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
(* Goal: forall (s : schedule) (_ : @safe (mkWorld pr) A t s s1) (_ : @ex (proc this (mkWorld pr) A) (fun t2' : proc this (mkWorld pr) A => and (@eq (proc this W A) q (@WithInv this W A pr I ii pf t2')) (@step (mkWorld pr) A s1 t s s2 t2'))), or (@ex A (fun v : A => and6 (@eq schedule (WithInvStep s) WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule (WithInvStep s) (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
- case=>//pr I ii E p/= H1 H2 C.
(* Goal: @ex state (fun s' : state => @ex (proc this W A) (fun p' : proc this W A => @pstep W A s (@WithInv this W A pr I ii E p) (WithInvStep sc) s' p')) *)
(* Goal: forall (p : proc this W A) (_ : @good W A p WithInvRet) (_ : @safe W A p WithInvRet s) (_ : @InMem state s (@Mem state (PredPredType state) (Coh W))), @ex state (fun s' : state => @ex (proc this W A) (fun p' : proc this W A => @pstep W A s p WithInvRet s' p')) *)
  have C' : s \In Coh (mkWorld pr) by subst W; apply: (with_inv_coh C). 
(* Goal: forall (_ : match t with | Unfinished => True | Ret a => @ex (UMDef.tp Label dstatelet) (fun s' : UMDef.tp Label dstatelet => @extends V W K em s1 s') | Act a => True | @Seq _ _ _ B p p0 => True | @Inject _ _ _ V0 K i p => True | WithInv p I0 ii e p0 => True end) (_ : match t with | Unfinished => False | Ret v => @ex (UMDef.tp Label dstatelet) (fun s1' : UMDef.tp Label dstatelet => and3 (@eq state s2 s1) (@eq (proc this W A) q (@Ret this W A v)) (@extends V W K em s1 s1')) | Act a => False | @Seq _ _ _ B p0 p1 => False | @Inject _ _ _ V0 K i p0 => False | WithInv p0 I0 ii e p1 => False end), or (@ex (UMDef.tp Label dstatelet) (fun s1' : UMDef.tp Label dstatelet => @ex A (fun v : A => and5 (@eq schedule InjectRet InjectRet) (@eq (proc this V A) t (@Ret this V A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@extends V W K em s1 s1')))) (@ex schedule (fun sc' : schedule => @ex (proc this V A) (fun t' : proc this V A => @ex (UMDef.tp Label dstatelet) (fun s1' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun s2' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun s : UMDef.tp Label dstatelet => and6 (@eq schedule InjectRet (InjectStep sc')) (@eq (proc this W A) q (@Inject this W A V K em t')) (@eq state s1 (@PCM.join (union_mapPCM Label dstatelet) s1' s)) (@eq state s2 (@PCM.join (union_mapPCM Label dstatelet) s2' s)) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep V A s1' t sc' s2' t'))))))) *)
(* Goal: forall (s : schedule) (_ : @ex (UMDef.tp Label dstatelet) (fun s' : UMDef.tp Label dstatelet => and (@extends V W K em s1 s') (@safe V A t s s'))) (_ : @ex (UMDef.tp Label dstatelet) (fun s1' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun s2' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun s0 : UMDef.tp Label dstatelet => @ex (proc this V A) (fun t2' : proc this V A => and5 (@eq (proc this W A) q (@Inject this W A V K em t2')) (@eq state s1 (@PCM.join (union_mapPCM Label dstatelet) s1' s0)) (@eq state s2 (@PCM.join (union_mapPCM Label dstatelet) s2' s0)) (@InMem (UMDef.tp Label dstatelet) s1' (@Mem state (PredPredType state) (Coh V))) (@step V A s1' t s s2' t2')))))), or (@ex (UMDef.tp Label dstatelet) (fun s1' : UMDef.tp Label dstatelet => @ex A (fun v : A => and5 (@eq schedule (InjectStep s) InjectRet) (@eq (proc this V A) t (@Ret this V A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@extends V W K em s1 s1')))) (@ex schedule (fun sc' : schedule => @ex (proc this V A) (fun t' : proc this V A => @ex (UMDef.tp Label dstatelet) (fun s1' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun s2' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun s0 : UMDef.tp Label dstatelet => and6 (@eq schedule (InjectStep s) (InjectStep sc')) (@eq (proc this W A) q (@Inject this W A V K em t')) (@eq state s1 (@PCM.join (union_mapPCM Label dstatelet) s1' s0)) (@eq state s2 (@PCM.join (union_mapPCM Label dstatelet) s2' s0)) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep V A s1' t sc' s2' t'))))))) *)
  case: (IH (mkWorld pr) A s p H1 H2 C')=>s'[p']H3.
(* Goal: @ex state (fun s' : state => @ex (proc this W A) (fun p' : proc this W A => @pstep W A s (@WithInv this W A pr I ii E p) (WithInvStep sc) s' p')) *)
(* Goal: forall (p : proc this W A) (_ : @good W A p WithInvRet) (_ : @safe W A p WithInvRet s) (_ : @InMem state s (@Mem state (PredPredType state) (Coh W))), @ex state (fun s' : state => @ex (proc this W A) (fun p' : proc this W A => @pstep W A s p WithInvRet s' p')) *)
  exists s', (WithInv pr I ii E p'); split=>//=.
(* Goal: forall (_ : @InMem state s1 (@Mem state (PredPredType state) (Coh (mkWorld (@ProtocolWithIndInv pr I ii))))) (_ : @pstep (mkWorld pr) A s1 t sc s2 t'), @InMem state s2 (@Mem state (PredPredType state) (Coh (mkWorld (@ProtocolWithIndInv pr I ii)))) *)
  by exists p'; split=>//; case: H3. 
(* Goal: forall (_ : match t with | Unfinished => True | Ret a => True | Act a => True | @Seq _ _ _ B p p0 => True | @Inject _ _ _ V K i p => True | WithInv p I0 ii e p0 => True end) (_ : match t with | Unfinished => False | Ret v => @ex state (fun s1' : state => and3 (@eq state s2 s1) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s1 s1')) | Act a => False | @Seq _ _ _ B p0 p1 => False | @Inject _ _ _ V K i p0 => False | WithInv p0 I0 ii e p1 => False end), or (@ex A (fun v : A => and6 (@eq schedule WithInvRet WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule WithInvRet (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
(* Goal: forall (s : schedule) (_ : @safe (mkWorld pr) A t s s1) (_ : @ex (proc this (mkWorld pr) A) (fun t2' : proc this (mkWorld pr) A => and (@eq (proc this W A) q (@WithInv this W A pr I ii pf t2')) (@step (mkWorld pr) A s1 t s s2 t2'))), or (@ex A (fun v : A => and6 (@eq schedule (WithInvStep s) WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule (WithInvStep s) (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
- case=>//pr I ii E; case=>//v/=_ _ C.          
(* Goal: forall (_ : @InMem state s1 (@Mem state (PredPredType state) (Coh (mkWorld (@ProtocolWithIndInv pr I ii))))) (_ : @pstep (mkWorld pr) A s1 t sc s2 t'), @InMem state s2 (@Mem state (PredPredType state) (Coh (mkWorld (@ProtocolWithIndInv pr I ii)))) *)
  by exists s, (Ret v); split=>//=; exists s. 
Qed.

(* Some view lemmas for processes and corresponding schedules *)

Lemma stepUnfin W A s1 sc s2 (t : proc this W A) : 
(* Goal: forall (_ : match t with | Unfinished => True | Ret a => True | Act a => True | @Seq _ _ _ B p p0 => True | @Inject _ _ _ V K i p => True | WithInv p I0 ii e p0 => True end) (_ : match t with | Unfinished => False | Ret v => @ex state (fun s1' : state => and3 (@eq state s2 s1) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s1 s1')) | Act a => False | @Seq _ _ _ B p0 p1 => False | @Inject _ _ _ V K i p0 => False | WithInv p0 I0 ii e p1 => False end), or (@ex A (fun v : A => and6 (@eq schedule WithInvRet WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule WithInvRet (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
(* Goal: forall (s : schedule) (_ : @safe (mkWorld pr) A t s s1) (_ : @ex (proc this (mkWorld pr) A) (fun t2' : proc this (mkWorld pr) A => and (@eq (proc this W A) q (@WithInv this W A pr I ii pf t2')) (@step (mkWorld pr) A s1 t s s2 t2'))), or (@ex A (fun v : A => and6 (@eq schedule (WithInvStep s) WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule (WithInvStep s) (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
        pstep s1 Unfinished sc s2 t <-> False.
Proof. by split=>//; case; case: sc. Qed.

Lemma stepRet W A s1 sc s2 (t : proc this W A) v : 
(* Goal: forall (_ : match t with | Unfinished => True | Ret a => True | Act a => True | @Seq _ _ _ B p p0 => True | @Inject _ _ _ V K i p => True | WithInv p I0 ii e p0 => True end) (_ : match t with | Unfinished => False | Ret v => @ex state (fun s1' : state => and3 (@eq state s2 s1) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s1 s1')) | Act a => False | @Seq _ _ _ B p0 p1 => False | @Inject _ _ _ V K i p0 => False | WithInv p0 I0 ii e p1 => False end), or (@ex A (fun v : A => and6 (@eq schedule WithInvRet WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule WithInvRet (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
(* Goal: forall (s : schedule) (_ : @safe (mkWorld pr) A t s s1) (_ : @ex (proc this (mkWorld pr) A) (fun t2' : proc this (mkWorld pr) A => and (@eq (proc this W A) q (@WithInv this W A pr I ii pf t2')) (@step (mkWorld pr) A s1 t s s2 t2'))), or (@ex A (fun v : A => and6 (@eq schedule (WithInvStep s) WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule (WithInvStep s) (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
        pstep s1 (Ret v) sc s2 t <-> False.
Proof. by split=>//; case; case: sc. Qed.

Lemma stepAct W A s1 a sc s2 (t : proc this W A) : 
(* Goal: forall (_ : match t with | Unfinished => True | Ret a => True | Act a => True | @Seq _ _ _ B p p0 => True | @Inject _ _ _ V K i p => True | WithInv p I0 ii e p0 => True end) (_ : match t with | Unfinished => False | Ret v => @ex state (fun s1' : state => and3 (@eq state s2 s1) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s1 s1')) | Act a => False | @Seq _ _ _ B p0 p1 => False | @Inject _ _ _ V K i p0 => False | WithInv p0 I0 ii e p1 => False end), or (@ex A (fun v : A => and6 (@eq schedule WithInvRet WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule WithInvRet (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
(* Goal: forall (s : schedule) (_ : @safe (mkWorld pr) A t s s1) (_ : @ex (proc this (mkWorld pr) A) (fun t2' : proc this (mkWorld pr) A => and (@eq (proc this W A) q (@WithInv this W A pr I ii pf t2')) (@step (mkWorld pr) A s1 t s s2 t2'))), or (@ex A (fun v : A => and6 (@eq schedule (WithInvStep s) WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule (WithInvStep s) (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
        pstep s1 (Act a) sc s2 t <->
        exists v pf, [/\ sc = ActStep, t = Ret v & @a_step _ _ _ a s1 pf s2 v].
Proof.
(* Goal: forall (_ : match t with | Unfinished => True | Ret a => True | Act a => True | @Seq _ _ _ B p p0 => True | @Inject _ _ _ V K i p => True | WithInv p I0 ii e p0 => True end) (_ : match t with | Unfinished => False | Ret v => @ex state (fun s1' : state => and3 (@eq state s2 s1) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s1 s1')) | Act a => False | @Seq _ _ _ B p0 p1 => False | @Inject _ _ _ V K i p0 => False | WithInv p0 I0 ii e p1 => False end), or (@ex A (fun v : A => and6 (@eq schedule WithInvRet WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule WithInvRet (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
(* Goal: forall (s : schedule) (_ : @safe (mkWorld pr) A t s s1) (_ : @ex (proc this (mkWorld pr) A) (fun t2' : proc this (mkWorld pr) A => and (@eq (proc this W A) q (@WithInv this W A pr I ii pf t2')) (@step (mkWorld pr) A s1 t s s2 t2'))), or (@ex A (fun v : A => and6 (@eq schedule (WithInvStep s) WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule (WithInvStep s) (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
split; first by case=>C; case: sc=>//= c [v [pf [H ->]]]; exists v, pf. 
(* Goal: forall (_ : match t with | Unfinished => True | Ret a => True | Act a => True | @Seq _ _ _ B p p0 => True | @Inject _ _ _ V K i p => True | WithInv p I0 ii e p0 => True end) (_ : match t with | Unfinished => False | Ret v => @ex state (fun s1' : state => and3 (@eq state s2 s1) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s1 s1')) | Act a => False | @Seq _ _ _ B p0 p1 => False | @Inject _ _ _ V K i p0 => False | WithInv p0 I0 ii e p1 => False end), or (@ex A (fun v : A => and6 (@eq schedule WithInvRet WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule WithInvRet (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
(* Goal: forall (s : schedule) (_ : @safe (mkWorld pr) A t s s1) (_ : @ex (proc this (mkWorld pr) A) (fun t2' : proc this (mkWorld pr) A => and (@eq (proc this W A) q (@WithInv this W A pr I ii pf t2')) (@step (mkWorld pr) A s1 t s s2 t2'))), or (@ex A (fun v : A => and6 (@eq schedule (WithInvStep s) WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule (WithInvStep s) (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
case=>v[pf] [->-> H]; split=>//; last by exists v, pf.
(* Goal: forall (_ : @InMem state s1 (@Mem state (PredPredType state) (Coh (mkWorld (@ProtocolWithIndInv pr I ii))))) (_ : @pstep (mkWorld pr) A s1 t sc s2 t'), @InMem state s2 (@Mem state (PredPredType state) (Coh (mkWorld (@ProtocolWithIndInv pr I ii)))) *)
by apply: (a_safe_coh pf). 
Qed.

Lemma stepSeq W A B s1 (t : proc this W B) k sc s2 (q : proc this W A) :
(* Goal: forall (_ : match t with | Unfinished => True | Ret a => True | Act a => True | @Seq _ _ _ B p p0 => True | @Inject _ _ _ V K i p => True | WithInv p I0 ii e p0 => True end) (_ : match t with | Unfinished => False | Ret v => @ex state (fun s1' : state => and3 (@eq state s2 s1) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s1 s1')) | Act a => False | @Seq _ _ _ B p0 p1 => False | @Inject _ _ _ V K i p0 => False | WithInv p0 I0 ii e p1 => False end), or (@ex A (fun v : A => and6 (@eq schedule WithInvRet WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule WithInvRet (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
(* Goal: forall (s : schedule) (_ : @safe (mkWorld pr) A t s s1) (_ : @ex (proc this (mkWorld pr) A) (fun t2' : proc this (mkWorld pr) A => and (@eq (proc this W A) q (@WithInv this W A pr I ii pf t2')) (@step (mkWorld pr) A s1 t s s2 t2'))), or (@ex A (fun v : A => and6 (@eq schedule (WithInvStep s) WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule (WithInvStep s) (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
        pstep s1 (Seq t k) sc s2 q <->
        (exists v, [/\ sc = SeqRet, t = Ret v, q = k v, s2 = s1 &
                       s1 \In Coh W]) \/
         exists sc' p',
           [/\ sc = SeqStep sc', q = Seq p' k & pstep s1 t sc' s2 p'].
Proof.
(* Goal: forall _ : @pstep W A s1 (@WithInv this W A pr I ii pf t) sc s2 q, or (@ex A (fun v : A => and6 (@eq schedule sc WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule sc (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
split; last first.
(* Goal: forall (_ : match t with | Unfinished => True | Ret a => True | Act a => True | @Seq _ _ _ B p p0 => True | @Inject _ _ _ V K i p => True | WithInv p I0 ii e p0 => True end) (_ : match t with | Unfinished => False | Ret v => @ex state (fun s1' : state => and3 (@eq state s2 s1) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s1 s1')) | Act a => False | @Seq _ _ _ B p0 p1 => False | @Inject _ _ _ V K i p0 => False | WithInv p0 I0 ii e p1 => False end), or (@ex A (fun v : A => and6 (@eq schedule WithInvRet WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule WithInvRet (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
(* Goal: forall (s : schedule) (_ : @safe (mkWorld pr) A t s s1) (_ : @ex (proc this (mkWorld pr) A) (fun t2' : proc this (mkWorld pr) A => and (@eq (proc this W A) q (@WithInv this W A pr I ii pf t2')) (@step (mkWorld pr) A s1 t s s2 t2'))), or (@ex A (fun v : A => and6 (@eq schedule (WithInvStep s) WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule (WithInvStep s) (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
- case; first by case=>v [->->->->]. 
(* Goal: forall (_ : match t with | Unfinished => True | Ret a => True | Act a => True | @Seq _ _ _ B p p0 => True | @Inject _ _ _ V K i p => True | WithInv p I0 ii e p0 => True end) (_ : match t with | Unfinished => False | Ret v => @ex state (fun s1' : state => and3 (@eq state s2 s1) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s1 s1')) | Act a => False | @Seq _ _ _ B p0 p1 => False | @Inject _ _ _ V K i p0 => False | WithInv p0 I0 ii e p1 => False end), or (@ex A (fun v : A => and6 (@eq schedule WithInvRet WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule WithInvRet (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
(* Goal: forall (s : schedule) (_ : @safe (mkWorld pr) A t s s1) (_ : @ex (proc this (mkWorld pr) A) (fun t2' : proc this (mkWorld pr) A => and (@eq (proc this W A) q (@WithInv this W A pr I ii pf t2')) (@step (mkWorld pr) A s1 t s s2 t2'))), or (@ex A (fun v : A => and6 (@eq schedule (WithInvStep s) WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule (WithInvStep s) (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
  by case=>sc' [t'][->->][S H]; do !split=>//; exists t'. 
(* Goal: forall _ : @pstep W A s1 (@Seq this W A B t k) sc s2 q, or (@ex B (fun v : B => and5 (@eq schedule sc SeqRet) (@eq (proc this W B) t (@Ret this W B v)) (@eq (proc this W A) q (k v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))))) (@ex schedule (fun sc' : schedule => @ex (proc this W B) (fun p' : proc this W B => and3 (@eq schedule sc (SeqStep sc')) (@eq (proc this W A) q (@Seq this W A B p' k)) (@pstep W B s1 t sc' s2 p')))) *)
case; case: sc=>//[|sc] C. 
(* Goal: forall (_ : match t with | Unfinished => True | Ret a => True | Act a => True | @Seq _ _ _ B p p0 => True | @Inject _ _ _ V K i p => True | WithInv p I0 ii e p0 => True end) (_ : match t with | Unfinished => False | Ret v => @ex state (fun s1' : state => and3 (@eq state s2 s1) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s1 s1')) | Act a => False | @Seq _ _ _ B p0 p1 => False | @Inject _ _ _ V K i p0 => False | WithInv p0 I0 ii e p1 => False end), or (@ex A (fun v : A => and6 (@eq schedule WithInvRet WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule WithInvRet (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
(* Goal: forall (s : schedule) (_ : @safe (mkWorld pr) A t s s1) (_ : @ex (proc this (mkWorld pr) A) (fun t2' : proc this (mkWorld pr) A => and (@eq (proc this W A) q (@WithInv this W A pr I ii pf t2')) (@step (mkWorld pr) A s1 t s s2 t2'))), or (@ex A (fun v : A => and6 (@eq schedule (WithInvStep s) WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule (WithInvStep s) (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
- by case: t=>//= v _ [->->]; left; exists v. 
(* Goal: forall (_ : match t with | Unfinished => True | Ret a => True | Act a => True | @Seq _ _ _ B p p0 => True | @Inject _ _ _ V K i p => True | WithInv p I0 ii e p0 => True end) (_ : match t with | Unfinished => False | Ret v => @ex state (fun s1' : state => and3 (@eq state s2 s1) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s1 s1')) | Act a => False | @Seq _ _ _ B p0 p1 => False | @Inject _ _ _ V K i p0 => False | WithInv p0 I0 ii e p1 => False end), or (@ex A (fun v : A => and6 (@eq schedule WithInvRet WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule WithInvRet (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
(* Goal: forall (s : schedule) (_ : @safe (mkWorld pr) A t s s1) (_ : @ex (proc this (mkWorld pr) A) (fun t2' : proc this (mkWorld pr) A => and (@eq (proc this W A) q (@WithInv this W A pr I ii pf t2')) (@step (mkWorld pr) A s1 t s s2 t2'))), or (@ex A (fun v : A => and6 (@eq schedule (WithInvStep s) WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule (WithInvStep s) (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
by move=>G /= [p' [H1 ->]]; right; exists sc, p'.
Qed.

Lemma stepInject V W K A (em : injects V W K) 
                s1 (t : proc this V A) sc s2 (q : proc this W A) :
(* Goal: forall (_ : match t with | Unfinished => True | Ret a => True | Act a => True | @Seq _ _ _ B p p0 => True | @Inject _ _ _ V K i p => True | WithInv p I0 ii e p0 => True end) (_ : match t with | Unfinished => False | Ret v => @ex state (fun s1' : state => and3 (@eq state s2 s1) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s1 s1')) | Act a => False | @Seq _ _ _ B p0 p1 => False | @Inject _ _ _ V K i p0 => False | WithInv p0 I0 ii e p1 => False end), or (@ex A (fun v : A => and6 (@eq schedule WithInvRet WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule WithInvRet (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
(* Goal: forall (s : schedule) (_ : @safe (mkWorld pr) A t s s1) (_ : @ex (proc this (mkWorld pr) A) (fun t2' : proc this (mkWorld pr) A => and (@eq (proc this W A) q (@WithInv this W A pr I ii pf t2')) (@step (mkWorld pr) A s1 t s s2 t2'))), or (@ex A (fun v : A => and6 (@eq schedule (WithInvStep s) WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule (WithInvStep s) (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
  pstep s1 (Inject em t) sc s2 q <->
  (* Case 1 : stepped to the final state s1' of the inner program*)
  (exists s1' v, [/\ sc = InjectRet, t = Ret v, q = Ret v, s2 = s1 &
                     extends em s1 s1']) \/
  (* Case 2 : stepped to the nextx state s12 of the inner program*)
  exists sc' t' s1' s2' s, 
    [/\ sc = InjectStep sc', q = Inject em t', 
(* Goal: forall _ : @ex A (fun v : A => and6 (@eq schedule sc WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii)))), @pstep W A s1 (@WithInv this W A pr I ii pf t) sc s2 q *)
(* Goal: forall _ : @ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule sc (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t'))), @pstep W A s1 (@WithInv this W A pr I ii pf t) sc s2 q *)
(* Goal: forall _ : @pstep W A s1 (@WithInv this W A pr I ii pf t) sc s2 q, or (@ex A (fun v : A => and6 (@eq schedule sc WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule sc (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
     s1 = s1' \+ s, s2 = s2' \+ s, s1 \In Coh W &
              pstep s1' t sc' s2' t'].
Proof.
(* Goal: forall _ : @pstep W A s1 (@WithInv this W A pr I ii pf t) sc s2 q, or (@ex A (fun v : A => and6 (@eq schedule sc WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule sc (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
split; last first.
(* Goal: forall (_ : match t with | Unfinished => True | Ret a => True | Act a => True | @Seq _ _ _ B p p0 => True | @Inject _ _ _ V K i p => True | WithInv p I0 ii e p0 => True end) (_ : match t with | Unfinished => False | Ret v => @ex state (fun s1' : state => and3 (@eq state s2 s1) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s1 s1')) | Act a => False | @Seq _ _ _ B p0 p1 => False | @Inject _ _ _ V K i p0 => False | WithInv p0 I0 ii e p1 => False end), or (@ex A (fun v : A => and6 (@eq schedule WithInvRet WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule WithInvRet (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
(* Goal: forall (s : schedule) (_ : @safe (mkWorld pr) A t s s1) (_ : @ex (proc this (mkWorld pr) A) (fun t2' : proc this (mkWorld pr) A => and (@eq (proc this W A) q (@WithInv this W A pr I ii pf t2')) (@step (mkWorld pr) A s1 t s s2 t2'))), or (@ex A (fun v : A => and6 (@eq schedule (WithInvStep s) WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule (WithInvStep s) (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
- case.
(* Goal: forall (_ : match t with | Unfinished => True | Ret a => True | Act a => True | @Seq _ _ _ B p p0 => True | @Inject _ _ _ V K i p => True | WithInv p I0 ii e p0 => True end) (_ : match t with | Unfinished => False | Ret v => @ex state (fun s1' : state => and3 (@eq state s2 s1) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s1 s1')) | Act a => False | @Seq _ _ _ B p0 p1 => False | @Inject _ _ _ V K i p0 => False | WithInv p0 I0 ii e p1 => False end), or (@ex A (fun v : A => and6 (@eq schedule WithInvRet WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule WithInvRet (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
(* Goal: forall (s : schedule) (_ : @safe (mkWorld pr) A t s s1) (_ : @ex (proc this (mkWorld pr) A) (fun t2' : proc this (mkWorld pr) A => and (@eq (proc this W A) q (@WithInv this W A pr I ii pf t2')) (@step (mkWorld pr) A s1 t s s2 t2'))), or (@ex A (fun v : A => and6 (@eq schedule (WithInvStep s) WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule (WithInvStep s) (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
  + case=>s1' [v][->->->->] E.
(* Goal: @pstep W A s1 (@Inject this W A V K em (@Ret this V A v)) InjectRet s1 (@Ret this W A v) *)
(* Goal: forall _ : @ex schedule (fun sc' : schedule => @ex (proc this V A) (fun t' : proc this V A => @ex (PCM.sort (union_mapPCM Label dstatelet)) (fun s1' : PCM.sort (union_mapPCM Label dstatelet) => @ex (PCM.sort (union_mapPCM Label dstatelet)) (fun s2' : PCM.sort (union_mapPCM Label dstatelet) => @ex (PCM.sort (union_mapPCM Label dstatelet)) (fun s : PCM.sort (union_mapPCM Label dstatelet) => and6 (@eq schedule sc (InjectStep sc')) (@eq (proc this W A) q (@Inject this W A V K em t')) (@eq state s1 (@PCM.join (union_mapPCM Label dstatelet) s1' s)) (@eq state s2 (@PCM.join (union_mapPCM Label dstatelet) s2' s)) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep V A s1' t sc' s2' t')))))), @pstep W A s1 (@Inject this W A V K em t) sc s2 q *)
(* Goal: forall _ : @pstep W A s1 (@Inject this W A V K em t) sc s2 q, or (@ex (PCM.sort (union_mapPCM Label dstatelet)) (fun s1' : PCM.sort (union_mapPCM Label dstatelet) => @ex A (fun v : A => and5 (@eq schedule sc InjectRet) (@eq (proc this V A) t (@Ret this V A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@extends V W K em s1 s1')))) (@ex schedule (fun sc' : schedule => @ex (proc this V A) (fun t' : proc this V A => @ex (PCM.sort (union_mapPCM Label dstatelet)) (fun s1' : PCM.sort (union_mapPCM Label dstatelet) => @ex (PCM.sort (union_mapPCM Label dstatelet)) (fun s2' : PCM.sort (union_mapPCM Label dstatelet) => @ex (PCM.sort (union_mapPCM Label dstatelet)) (fun s : PCM.sort (union_mapPCM Label dstatelet) => and6 (@eq schedule sc (InjectStep sc')) (@eq (proc this W A) q (@Inject this W A V K em t')) (@eq state s1 (@PCM.join (union_mapPCM Label dstatelet) s1' s)) (@eq state s2 (@PCM.join (union_mapPCM Label dstatelet) s2' s)) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep V A s1' t sc' s2' t'))))))) *)
    split=>//=; [by case: E=>x[] | by exists s1'|by exists s1'].
(* Goal: forall (_ : match t with | Unfinished => True | Ret a => True | Act a => True | @Seq _ _ _ B p p0 => True | @Inject _ _ _ V K i p => True | WithInv p I0 ii e p0 => True end) (_ : match t with | Unfinished => False | Ret v => @ex state (fun s1' : state => and3 (@eq state s2 s1) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s1 s1')) | Act a => False | @Seq _ _ _ B p0 p1 => False | @Inject _ _ _ V K i p0 => False | WithInv p0 I0 ii e p1 => False end), or (@ex A (fun v : A => and6 (@eq schedule WithInvRet WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule WithInvRet (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
(* Goal: forall (s : schedule) (_ : @safe (mkWorld pr) A t s s1) (_ : @ex (proc this (mkWorld pr) A) (fun t2' : proc this (mkWorld pr) A => and (@eq (proc this W A) q (@WithInv this W A pr I ii pf t2')) (@step (mkWorld pr) A s1 t s s2 t2'))), or (@ex A (fun v : A => and6 (@eq schedule (WithInvStep s) WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule (WithInvStep s) (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
  case=>sc' [t'][s1'][s2'][s][->->->-> C][[C' S] T]. 
(* Goal: forall _ : @pstep W A s1 (@WithInv this W A pr I ii pf t) sc s2 q, or (@ex A (fun v : A => and6 (@eq schedule sc WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule sc (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
  split=>//=; last by exists s1', s2', s, t'. 
(* Goal: forall (_ : @InMem state s1 (@Mem state (PredPredType state) (Coh (mkWorld (@ProtocolWithIndInv pr I ii))))) (_ : @pstep (mkWorld pr) A s1 t sc s2 t'), @InMem state s2 (@Mem state (PredPredType state) (Coh (mkWorld (@ProtocolWithIndInv pr I ii)))) *)
  by exists s1'; split=>//; exists s. 
(* Goal: forall _ : @pstep W A s1 (@WithInv this W A pr I ii pf t) sc s2 q, or (@ex A (fun v : A => and6 (@eq schedule sc WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule sc (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
case=>C; case: sc=>//=; last first.
(* Goal: forall (_ : match t with | Unfinished => True | Ret a => True | Act a => True | @Seq _ _ _ B p p0 => True | @Inject _ _ _ V K i p => True | WithInv p I0 ii e p0 => True end) (_ : match t with | Unfinished => False | Ret v => @ex state (fun s1' : state => and3 (@eq state s2 s1) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s1 s1')) | Act a => False | @Seq _ _ _ B p0 p1 => False | @Inject _ _ _ V K i p0 => False | WithInv p0 I0 ii e p1 => False end), or (@ex A (fun v : A => and6 (@eq schedule WithInvRet WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule WithInvRet (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
(* Goal: forall (s : schedule) (_ : @safe (mkWorld pr) A t s s1) (_ : @ex (proc this (mkWorld pr) A) (fun t2' : proc this (mkWorld pr) A => and (@eq (proc this W A) q (@WithInv this W A pr I ii pf t2')) (@step (mkWorld pr) A s1 t s s2 t2'))), or (@ex A (fun v : A => and6 (@eq schedule (WithInvStep s) WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule (WithInvStep s) (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
- case: t=>//= v [C1 S][s1'][->->{s2 q}] X.
(* Goal: forall (_ : @InMem state s1 (@Mem state (PredPredType state) (Coh (mkWorld (@ProtocolWithIndInv pr I ii))))) (_ : @pstep (mkWorld pr) A s1 t sc s2 t'), @InMem state s2 (@Mem state (PredPredType state) (Coh (mkWorld (@ProtocolWithIndInv pr I ii)))) *)
  by left; exists s1'; exists v. 
(* Goal: forall (s : schedule) (_ : @ex (UMDef.tp Label dstatelet) (fun s' : UMDef.tp Label dstatelet => and (@extends V W K em s1 s') (@safe V A t s s'))) (_ : @ex (UMDef.tp Label dstatelet) (fun s1' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun s2' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun s0 : UMDef.tp Label dstatelet => @ex (proc this V A) (fun t2' : proc this V A => and5 (@eq (proc this W A) q (@Inject this W A V K em t2')) (@eq state s1 (@PCM.join (union_mapPCM Label dstatelet) s1' s0)) (@eq state s2 (@PCM.join (union_mapPCM Label dstatelet) s2' s0)) (@InMem (UMDef.tp Label dstatelet) s1' (@Mem state (PredPredType state) (Coh V))) (@step V A s1' t s s2' t2')))))), or (@ex (UMDef.tp Label dstatelet) (fun s1' : UMDef.tp Label dstatelet => @ex A (fun v : A => and5 (@eq schedule (InjectStep s) InjectRet) (@eq (proc this V A) t (@Ret this V A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@extends V W K em s1 s1')))) (@ex schedule (fun sc' : schedule => @ex (proc this V A) (fun t' : proc this V A => @ex (UMDef.tp Label dstatelet) (fun s1' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun s2' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun s0 : UMDef.tp Label dstatelet => and6 (@eq schedule (InjectStep s) (InjectStep sc')) (@eq (proc this W A) q (@Inject this W A V K em t')) (@eq state s1 (@PCM.join (union_mapPCM Label dstatelet) s1' s0)) (@eq state s2 (@PCM.join (union_mapPCM Label dstatelet) s2' s0)) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep V A s1' t sc' s2' t'))))))) *)
move=>sc /= [s'][X] S [s1'][s2'][t'][t2'][??? C1'] T; subst q s1 s2. 
(* Goal: or (@ex (UMDef.tp Label dstatelet) (fun s1'0 : UMDef.tp Label dstatelet => @ex A (fun v : A => and5 (@eq schedule (InjectStep sc) InjectRet) (@eq (proc this V A) t (@Ret this V A v)) (@eq (proc this W A) (@Inject this W A V K em t2') (@Ret this W A v)) (@eq state (@PCM.join (union_mapPCM Label dstatelet) s2' t') (@PCM.join (union_mapPCM Label dstatelet) s1' t')) (@extends V W K em (@PCM.join (union_mapPCM Label dstatelet) s1' t') s1'0)))) (@ex schedule (fun sc' : schedule => @ex (proc this V A) (fun t'0 : proc this V A => @ex (UMDef.tp Label dstatelet) (fun s1'0 : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun s2'0 : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun s : UMDef.tp Label dstatelet => and6 (@eq schedule (InjectStep sc) (InjectStep sc')) (@eq (proc this W A) (@Inject this W A V K em t2') (@Inject this W A V K em t'0)) (@eq state (@PCM.join (union_mapPCM Label dstatelet) s1' t') (@PCM.join (union_mapPCM Label dstatelet) s1'0 s)) (@eq state (@PCM.join (union_mapPCM Label dstatelet) s2' t') (@PCM.join (union_mapPCM Label dstatelet) s2'0 s)) (@InMem state (@PCM.join (union_mapPCM Label dstatelet) s1' t') (@Mem state (PredPredType state) (Coh W))) (@pstep V A s1'0 t sc' s2'0 t'0))))))) *)
right; exists sc, t2', s1', s2', t'; do !split=>//.
by case: X=>t'' [E] Cs' _; rewrite (coh_prec (cohS C)  _ Cs' E). 
Qed.

Lemma stepWithInv W A pr I (ii : InductiveInv pr I) s1 
      (t : proc this (mkWorld pr) A) sc s2 (q : proc this W A) pf :
(* Goal: forall (_ : match t with | Unfinished => True | Ret a => True | Act a => True | @Seq _ _ _ B p p0 => True | @Inject _ _ _ V K i p => True | WithInv p I0 ii e p0 => True end) (_ : match t with | Unfinished => False | Ret v => @ex state (fun s1' : state => and3 (@eq state s2 s1) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s1 s1')) | Act a => False | @Seq _ _ _ B p0 p1 => False | @Inject _ _ _ V K i p0 => False | WithInv p0 I0 ii e p1 => False end), or (@ex A (fun v : A => and6 (@eq schedule WithInvRet WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule WithInvRet (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
(* Goal: forall (s : schedule) (_ : @safe (mkWorld pr) A t s s1) (_ : @ex (proc this (mkWorld pr) A) (fun t2' : proc this (mkWorld pr) A => and (@eq (proc this W A) q (@WithInv this W A pr I ii pf t2')) (@step (mkWorld pr) A s1 t s s2 t2'))), or (@ex A (fun v : A => and6 (@eq schedule (WithInvStep s) WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule (WithInvStep s) (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
  pstep s1 (WithInv pr I ii pf t) sc s2 q <-> 
  (exists v, [/\ sc = WithInvRet, t = Ret v, q = Ret v, s2 = s1,
                 s1 \In Coh W & W = mkWorld (ProtocolWithIndInv ii)]) \/
  exists sc' t' , [/\ sc = WithInvStep sc', q = WithInv pr I ii pf t',
                      W = mkWorld (ProtocolWithIndInv ii),
                      s1 \In Coh W & pstep s1 t sc' s2 t'].
Proof.
(* Goal: forall _ : @pstep W A s1 (@WithInv this W A pr I ii pf t) sc s2 q, or (@ex A (fun v : A => and6 (@eq schedule sc WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule sc (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
split; last first.
(* Goal: forall (_ : match t with | Unfinished => True | Ret a => True | Act a => True | @Seq _ _ _ B p p0 => True | @Inject _ _ _ V K i p => True | WithInv p I0 ii e p0 => True end) (_ : match t with | Unfinished => False | Ret v => @ex state (fun s1' : state => and3 (@eq state s2 s1) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s1 s1')) | Act a => False | @Seq _ _ _ B p0 p1 => False | @Inject _ _ _ V K i p0 => False | WithInv p0 I0 ii e p1 => False end), or (@ex A (fun v : A => and6 (@eq schedule WithInvRet WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule WithInvRet (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
(* Goal: forall (s : schedule) (_ : @safe (mkWorld pr) A t s s1) (_ : @ex (proc this (mkWorld pr) A) (fun t2' : proc this (mkWorld pr) A => and (@eq (proc this W A) q (@WithInv this W A pr I ii pf t2')) (@step (mkWorld pr) A s1 t s s2 t2'))), or (@ex A (fun v : A => and6 (@eq schedule (WithInvStep s) WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule (WithInvStep s) (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
- case.
(* Goal: forall (_ : match t with | Unfinished => True | Ret a => True | Act a => True | @Seq _ _ _ B p p0 => True | @Inject _ _ _ V K i p => True | WithInv p I0 ii e p0 => True end) (_ : match t with | Unfinished => False | Ret v => @ex state (fun s1' : state => and3 (@eq state s2 s1) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s1 s1')) | Act a => False | @Seq _ _ _ B p0 p1 => False | @Inject _ _ _ V K i p0 => False | WithInv p0 I0 ii e p1 => False end), or (@ex A (fun v : A => and6 (@eq schedule WithInvRet WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule WithInvRet (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
(* Goal: forall (s : schedule) (_ : @safe (mkWorld pr) A t s s1) (_ : @ex (proc this (mkWorld pr) A) (fun t2' : proc this (mkWorld pr) A => and (@eq (proc this W A) q (@WithInv this W A pr I ii pf t2')) (@step (mkWorld pr) A s1 t s s2 t2'))), or (@ex A (fun v : A => and6 (@eq schedule (WithInvStep s) WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule (WithInvStep s) (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
  + by case=>v[->->->->{s2}]C E; split=>//=; exists s1.
(* Goal: forall (_ : match t with | Unfinished => True | Ret a => True | Act a => True | @Seq _ _ _ B p p0 => True | @Inject _ _ _ V K i p => True | WithInv p I0 ii e p0 => True end) (_ : match t with | Unfinished => False | Ret v => @ex state (fun s1' : state => and3 (@eq state s2 s1) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s1 s1')) | Act a => False | @Seq _ _ _ B p0 p1 => False | @Inject _ _ _ V K i p0 => False | WithInv p0 I0 ii e p1 => False end), or (@ex A (fun v : A => and6 (@eq schedule WithInvRet WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule WithInvRet (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
(* Goal: forall (s : schedule) (_ : @safe (mkWorld pr) A t s s1) (_ : @ex (proc this (mkWorld pr) A) (fun t2' : proc this (mkWorld pr) A => and (@eq (proc this W A) q (@WithInv this W A pr I ii pf t2')) (@step (mkWorld pr) A s1 t s s2 t2'))), or (@ex A (fun v : A => and6 (@eq schedule (WithInvStep s) WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule (WithInvStep s) (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
   by case=>sc' [t'][->->{sc q}]E C[C' S]T; split=>//=; exists t'.   
(* Goal: forall _ : @pstep W A s1 (@WithInv this W A pr I ii pf t) sc s2 q, or (@ex A (fun v : A => and6 (@eq schedule sc WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule sc (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
case=>C; case: sc=>//=; last first.
(* Goal: forall (_ : match t with | Unfinished => True | Ret a => True | Act a => True | @Seq _ _ _ B p p0 => True | @Inject _ _ _ V K i p => True | WithInv p I0 ii e p0 => True end) (_ : match t with | Unfinished => False | Ret v => @ex state (fun s1' : state => and3 (@eq state s2 s1) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s1 s1')) | Act a => False | @Seq _ _ _ B p0 p1 => False | @Inject _ _ _ V K i p0 => False | WithInv p0 I0 ii e p1 => False end), or (@ex A (fun v : A => and6 (@eq schedule WithInvRet WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule WithInvRet (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
(* Goal: forall (s : schedule) (_ : @safe (mkWorld pr) A t s s1) (_ : @ex (proc this (mkWorld pr) A) (fun t2' : proc this (mkWorld pr) A => and (@eq (proc this W A) q (@WithInv this W A pr I ii pf t2')) (@step (mkWorld pr) A s1 t s s2 t2'))), or (@ex A (fun v : A => and6 (@eq schedule (WithInvStep s) WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule (WithInvStep s) (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
- by case: t=>//=v _[s1'][Z1]Z2 Z3; subst s2 s1' q; left; exists v. 
(* Goal: forall (_ : match t with | Unfinished => True | Ret a => True | Act a => True | @Seq _ _ _ B p p0 => True | @Inject _ _ _ V K i p => True | WithInv p I0 ii e p0 => True end) (_ : match t with | Unfinished => False | Ret v => @ex state (fun s1' : state => and3 (@eq state s2 s1) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s1 s1')) | Act a => False | @Seq _ _ _ B p0 p1 => False | @Inject _ _ _ V K i p0 => False | WithInv p0 I0 ii e p1 => False end), or (@ex A (fun v : A => and6 (@eq schedule WithInvRet WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule WithInvRet (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
(* Goal: forall (s : schedule) (_ : @safe (mkWorld pr) A t s s1) (_ : @ex (proc this (mkWorld pr) A) (fun t2' : proc this (mkWorld pr) A => and (@eq (proc this W A) q (@WithInv this W A pr I ii pf t2')) (@step (mkWorld pr) A s1 t s s2 t2'))), or (@ex A (fun v : A => and6 (@eq schedule (WithInvStep s) WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule (WithInvStep s) (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
move=>sc /=S[t'][->{q}T]; right; exists sc, t'; split=>//.
(* Goal: forall (_ : @InMem state s1 (@Mem state (PredPredType state) (Coh (mkWorld (@ProtocolWithIndInv pr I ii))))) (_ : @pstep (mkWorld pr) A s1 t sc s2 t'), @InMem state s2 (@Mem state (PredPredType state) (Coh (mkWorld (@ProtocolWithIndInv pr I ii)))) *)
by split=>//; subst W; apply: (with_inv_coh C).
Qed.

(*

[Stepping and network semantics]

The following lemma ensures that the operational semantics of our
programs respect the global network semantics.

 *)

Lemma pstep_network_sem (W : world) A s1 (t : proc this W A) sc s2 q :
(* Goal: forall (_ : match t with | Unfinished => True | Ret a => True | Act a => True | @Seq _ _ _ B p p0 => True | @Inject _ _ _ V K i p => True | WithInv p I0 ii e p0 => True end) (_ : match t with | Unfinished => False | Ret v => @ex state (fun s1' : state => and3 (@eq state s2 s1) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s1 s1')) | Act a => False | @Seq _ _ _ B p0 p1 => False | @Inject _ _ _ V K i p0 => False | WithInv p0 I0 ii e p1 => False end), or (@ex A (fun v : A => and6 (@eq schedule WithInvRet WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule WithInvRet (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
(* Goal: forall (s : schedule) (_ : @safe (mkWorld pr) A t s s1) (_ : @ex (proc this (mkWorld pr) A) (fun t2' : proc this (mkWorld pr) A => and (@eq (proc this W A) q (@WithInv this W A pr I ii pf t2')) (@step (mkWorld pr) A s1 t s s2 t2'))), or (@ex A (fun v : A => and6 (@eq schedule (WithInvStep s) WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule (WithInvStep s) (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
        pstep s1 t sc s2 q -> network_step W this s1 s2.
Proof.
elim: sc W A s1 s2 t q=>/=.
(* Goal: forall (_ : match t with | Unfinished => True | Ret a => True | Act a => True | @Seq _ _ _ B p p0 => True | @Inject _ _ _ V K i p => True | WithInv p I0 ii e p0 => True end) (_ : match t with | Unfinished => False | Ret v => @ex state (fun s1' : state => and3 (@eq state s2 s1) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s1 s1')) | Act a => False | @Seq _ _ _ B p0 p1 => False | @Inject _ _ _ V K i p0 => False | WithInv p0 I0 ii e p1 => False end), or (@ex A (fun v : A => and6 (@eq schedule WithInvRet WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule WithInvRet (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
(* Goal: forall (s : schedule) (_ : @safe (mkWorld pr) A t s s1) (_ : @ex (proc this (mkWorld pr) A) (fun t2' : proc this (mkWorld pr) A => and (@eq (proc this W A) q (@WithInv this W A pr I ii pf t2')) (@step (mkWorld pr) A s1 t s s2 t2'))), or (@ex A (fun v : A => and6 (@eq schedule (WithInvStep s) WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule (WithInvStep s) (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
- move=>W A s1 s2 p q; case: p; do?[by case|by move=>?; case].
(* Goal: forall _ : @ex A (fun v : A => and6 (@eq schedule sc WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii)))), @pstep W A s1 (@WithInv this W A pr I ii pf t) sc s2 q *)
(* Goal: forall _ : @ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule sc (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t'))), @pstep W A s1 (@WithInv this W A pr I ii pf t) sc s2 q *)
(* Goal: forall _ : @pstep W A s1 (@WithInv this W A pr I ii pf t) sc s2 q, or (@ex A (fun v : A => and6 (@eq schedule sc WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule sc (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
  + by move=>a/stepAct [v][pf][Z1]Z2 H; subst q; apply: (a_step_sem H).
(* Goal: forall _ : or (@ex A (fun v : A => and6 (@eq schedule sc WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule sc (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))), @pstep W A s1 (@WithInv this W A pr I ii pf t) sc s2 q *)
(* Goal: forall _ : @pstep W A s1 (@WithInv this W A pr I ii pf t) sc s2 q, or (@ex A (fun v : A => and6 (@eq schedule sc WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule sc (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
  + by move=>???; case. 
(* Goal: forall _ : or (@ex A (fun v : A => and6 (@eq schedule sc WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule sc (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))), @pstep W A s1 (@WithInv this W A pr I ii pf t) sc s2 q *)
(* Goal: forall _ : @pstep W A s1 (@WithInv this W A pr I ii pf t) sc s2 q, or (@ex A (fun v : A => and6 (@eq schedule sc WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule sc (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
  + by move=>????; case.
(* Goal: forall _ : or (@ex A (fun v : A => and6 (@eq schedule sc WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule sc (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))), @pstep W A s1 (@WithInv this W A pr I ii pf t) sc s2 q *)
(* Goal: forall _ : @pstep W A s1 (@WithInv this W A pr I ii pf t) sc s2 q, or (@ex A (fun v : A => and6 (@eq schedule sc WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule sc (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
  by move=>?????; case.   
(* Goal: forall (_ : match t with | Unfinished => True | Ret a => True | Act a => True | @Seq _ _ _ B p p0 => True | @Inject _ _ _ V K i p => True | WithInv p I0 ii e p0 => True end) (_ : match t with | Unfinished => False | Ret v => @ex state (fun s1' : state => and3 (@eq state s2 s1) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s1 s1')) | Act a => False | @Seq _ _ _ B p0 p1 => False | @Inject _ _ _ V K i p0 => False | WithInv p0 I0 ii e p1 => False end), or (@ex A (fun v : A => and6 (@eq schedule WithInvRet WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule WithInvRet (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
(* Goal: forall (s : schedule) (_ : @safe (mkWorld pr) A t s s1) (_ : @ex (proc this (mkWorld pr) A) (fun t2' : proc this (mkWorld pr) A => and (@eq (proc this W A) q (@WithInv this W A pr I ii pf t2')) (@step (mkWorld pr) A s1 t s s2 t2'))), or (@ex A (fun v : A => and6 (@eq schedule (WithInvStep s) WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule (WithInvStep s) (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
- move=>W A s1 s2 p q; case: p; do?[by case|by move=>?; case].
(* Goal: forall _ : @ex A (fun v : A => and6 (@eq schedule sc WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii)))), @pstep W A s1 (@WithInv this W A pr I ii pf t) sc s2 q *)
(* Goal: forall _ : @ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule sc (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t'))), @pstep W A s1 (@WithInv this W A pr I ii pf t) sc s2 q *)
(* Goal: forall _ : @pstep W A s1 (@WithInv this W A pr I ii pf t) sc s2 q, or (@ex A (fun v : A => and6 (@eq schedule sc WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule sc (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
  + move=>B p p0/stepSeq; case=>[[v][_]??? C|[sc'][p'][]]//.
(* Goal: forall (_ : @InMem state s1 (@Mem state (PredPredType state) (Coh (mkWorld (@ProtocolWithIndInv pr I ii))))) (_ : @pstep (mkWorld pr) A s1 t sc s2 t'), @InMem state s2 (@Mem state (PredPredType state) (Coh (mkWorld (@ProtocolWithIndInv pr I ii)))) *)
    by subst p s2; apply: Idle. 
(* Goal: forall (_ : @InMem state s1 (@Mem state (PredPredType state) (Coh (mkWorld (@ProtocolWithIndInv pr I ii))))) (_ : @pstep (mkWorld pr) A s1 t sc s2 t'), @InMem state s2 (@Mem state (PredPredType state) (Coh (mkWorld (@ProtocolWithIndInv pr I ii)))) *)
  by move=>????/stepInject; case=>[[?][?][?]|[?][?][?][?][?][?]]//.
(* Goal: forall _ : or (@ex A (fun v : A => and6 (@eq schedule sc WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule sc (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))), @pstep W A s1 (@WithInv this W A pr I ii pf t) sc s2 q *)
(* Goal: forall _ : @pstep W A s1 (@WithInv this W A pr I ii pf t) sc s2 q, or (@ex A (fun v : A => and6 (@eq schedule sc WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule sc (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
  by move=>?????; case.   
(* Goal: forall (_ : match t with | Unfinished => True | Ret a => True | Act a => True | @Seq _ _ _ B p p0 => True | @Inject _ _ _ V K i p => True | WithInv p I0 ii e p0 => True end) (_ : match t with | Unfinished => False | Ret v => @ex state (fun s1' : state => and3 (@eq state s2 s1) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s1 s1')) | Act a => False | @Seq _ _ _ B p0 p1 => False | @Inject _ _ _ V K i p0 => False | WithInv p0 I0 ii e p1 => False end), or (@ex A (fun v : A => and6 (@eq schedule WithInvRet WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule WithInvRet (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
(* Goal: forall (s : schedule) (_ : @safe (mkWorld pr) A t s s1) (_ : @ex (proc this (mkWorld pr) A) (fun t2' : proc this (mkWorld pr) A => and (@eq (proc this W A) q (@WithInv this W A pr I ii pf t2')) (@step (mkWorld pr) A s1 t s s2 t2'))), or (@ex A (fun v : A => and6 (@eq schedule (WithInvStep s) WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule (WithInvStep s) (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
- move=>sc HI W A s1 s2 p q; case: p; do?[by case|by move=>?; case].
(* Goal: forall _ : @ex A (fun v : A => and6 (@eq schedule sc WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii)))), @pstep W A s1 (@WithInv this W A pr I ii pf t) sc s2 q *)
(* Goal: forall _ : @ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule sc (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t'))), @pstep W A s1 (@WithInv this W A pr I ii pf t) sc s2 q *)
(* Goal: forall _ : @pstep W A s1 (@WithInv this W A pr I ii pf t) sc s2 q, or (@ex A (fun v : A => and6 (@eq schedule sc WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule sc (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
  + move=>B p p0/stepSeq; case=>[[?][?]|[sc'][p'][][]? ?]//.
(* Goal: forall (_ : @InMem state s1 (@Mem state (PredPredType state) (Coh (mkWorld (@ProtocolWithIndInv pr I ii))))) (_ : @pstep (mkWorld pr) A s1 t sc s2 t'), @InMem state s2 (@Mem state (PredPredType state) (Coh (mkWorld (@ProtocolWithIndInv pr I ii)))) *)
    by subst sc' q; apply: HI.
(* Goal: forall (_ : @InMem state s1 (@Mem state (PredPredType state) (Coh (mkWorld (@ProtocolWithIndInv pr I ii))))) (_ : @pstep (mkWorld pr) A s1 t sc s2 t'), @InMem state s2 (@Mem state (PredPredType state) (Coh (mkWorld (@ProtocolWithIndInv pr I ii)))) *)
  by move=>????; case=>? _.
(* Goal: forall _ : or (@ex A (fun v : A => and6 (@eq schedule sc WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule sc (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))), @pstep W A s1 (@WithInv this W A pr I ii pf t) sc s2 q *)
(* Goal: forall _ : @pstep W A s1 (@WithInv this W A pr I ii pf t) sc s2 q, or (@ex A (fun v : A => and6 (@eq schedule sc WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule sc (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
  by move=>?????; case.   
(* Goal: forall (_ : match t with | Unfinished => True | Ret a => True | Act a => True | @Seq _ _ _ B p p0 => True | @Inject _ _ _ V K i p => True | WithInv p I0 ii e p0 => True end) (_ : match t with | Unfinished => False | Ret v => @ex state (fun s1' : state => and3 (@eq state s2 s1) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s1 s1')) | Act a => False | @Seq _ _ _ B p0 p1 => False | @Inject _ _ _ V K i p0 => False | WithInv p0 I0 ii e p1 => False end), or (@ex A (fun v : A => and6 (@eq schedule WithInvRet WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule WithInvRet (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
(* Goal: forall (s : schedule) (_ : @safe (mkWorld pr) A t s s1) (_ : @ex (proc this (mkWorld pr) A) (fun t2' : proc this (mkWorld pr) A => and (@eq (proc this W A) q (@WithInv this W A pr I ii pf t2')) (@step (mkWorld pr) A s1 t s s2 t2'))), or (@ex A (fun v : A => and6 (@eq schedule (WithInvStep s) WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule (WithInvStep s) (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
- move=>sc HI W A s1 s2 p q; case: p; do?[by case|by move=>?; case].
(* Goal: forall _ : or (@ex A (fun v : A => and6 (@eq schedule sc WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule sc (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))), @pstep W A s1 (@WithInv this W A pr I ii pf t) sc s2 q *)
(* Goal: forall _ : @pstep W A s1 (@WithInv this W A pr I ii pf t) sc s2 q, or (@ex A (fun v : A => and6 (@eq schedule sc WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule sc (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
  + by move=>B p p0; case. 
  move=>V K pf p/stepInject; case=>[[?][?][?]|[sc'][t'][s1'][s2'][s][][]????]//. 
  subst sc' q s1 s2=>C; move/HI=>S; apply: (sem_extend pf)=>//.
  apply/(cohE pf); exists s2', s; case: (step_coh S)=>C1 C2; split=>//.
  move/(cohE pf): (C)=>[s1][s2][E]C' H.
(* Goal: forall (_ : @InMem state s1 (@Mem state (PredPredType state) (Coh (mkWorld (@ProtocolWithIndInv pr I ii))))) (_ : @pstep (mkWorld pr) A s1 t sc s2 t'), @InMem state s2 (@Mem state (PredPredType state) (Coh (mkWorld (@ProtocolWithIndInv pr I ii)))) *)
  by move: (coh_prec (cohS C) C1 C' E)=>Z; subst s1'; rewrite (joinxK (cohS C) E). 
(* Goal: forall _ : or (@ex A (fun v : A => and6 (@eq schedule sc WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule sc (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))), @pstep W A s1 (@WithInv this W A pr I ii pf t) sc s2 q *)
(* Goal: forall _ : @pstep W A s1 (@WithInv this W A pr I ii pf t) sc s2 q, or (@ex A (fun v : A => and6 (@eq schedule sc WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule sc (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
  by move=>?????; case.   
(* Goal: forall (_ : match t with | Unfinished => True | Ret a => True | Act a => True | @Seq _ _ _ B p p0 => True | @Inject _ _ _ V K i p => True | WithInv p I0 ii e p0 => True end) (_ : match t with | Unfinished => False | Ret v => @ex state (fun s1' : state => and3 (@eq state s2 s1) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s1 s1')) | Act a => False | @Seq _ _ _ B p0 p1 => False | @Inject _ _ _ V K i p0 => False | WithInv p0 I0 ii e p1 => False end), or (@ex A (fun v : A => and6 (@eq schedule WithInvRet WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule WithInvRet (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
(* Goal: forall (s : schedule) (_ : @safe (mkWorld pr) A t s s1) (_ : @ex (proc this (mkWorld pr) A) (fun t2' : proc this (mkWorld pr) A => and (@eq (proc this W A) q (@WithInv this W A pr I ii pf t2')) (@step (mkWorld pr) A s1 t s s2 t2'))), or (@ex A (fun v : A => and6 (@eq schedule (WithInvStep s) WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule (WithInvStep s) (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
- move=>W A s1 s2 p q; case: p; do?[by case|by move=>?; case].
(* Goal: forall _ : or (@ex A (fun v : A => and6 (@eq schedule sc WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule sc (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))), @pstep W A s1 (@WithInv this W A pr I ii pf t) sc s2 q *)
(* Goal: forall _ : @pstep W A s1 (@WithInv this W A pr I ii pf t) sc s2 q, or (@ex A (fun v : A => and6 (@eq schedule sc WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule sc (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
  + by move=>???; case.
(* Goal: forall _ : @ex A (fun v : A => and6 (@eq schedule sc WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii)))), @pstep W A s1 (@WithInv this W A pr I ii pf t) sc s2 q *)
(* Goal: forall _ : @ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule sc (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t'))), @pstep W A s1 (@WithInv this W A pr I ii pf t) sc s2 q *)
(* Goal: forall _ : @pstep W A s1 (@WithInv this W A pr I ii pf t) sc s2 q, or (@ex A (fun v : A => and6 (@eq schedule sc WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule sc (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
  + move=>V K i p; case/stepInject=>[[s1'][v][_]??? X|[?][?][?][?][?][?]]//.
(* Goal: forall (_ : @InMem state s1 (@Mem state (PredPredType state) (Coh (mkWorld (@ProtocolWithIndInv pr I ii))))) (_ : @pstep (mkWorld pr) A s1 t sc s2 t'), @InMem state s2 (@Mem state (PredPredType state) (Coh (mkWorld (@ProtocolWithIndInv pr I ii)))) *)
    by subst p q s2; apply: Idle; split=>//; case: X=>x []. 
(* Goal: forall _ : or (@ex A (fun v : A => and6 (@eq schedule sc WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule sc (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))), @pstep W A s1 (@WithInv this W A pr I ii pf t) sc s2 q *)
(* Goal: forall _ : @pstep W A s1 (@WithInv this W A pr I ii pf t) sc s2 q, or (@ex A (fun v : A => and6 (@eq schedule sc WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule sc (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
  by move=>?????; case.

(* Goal: forall (_ : match t with | Unfinished => True | Ret a => True | Act a => True | @Seq _ _ _ B p p0 => True | @Inject _ _ _ V K i p => True | WithInv p I0 ii e p0 => True end) (_ : match t with | Unfinished => False | Ret v => @ex state (fun s1' : state => and3 (@eq state s2 s1) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s1 s1')) | Act a => False | @Seq _ _ _ B p0 p1 => False | @Inject _ _ _ V K i p0 => False | WithInv p0 I0 ii e p1 => False end), or (@ex A (fun v : A => and6 (@eq schedule WithInvRet WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule WithInvRet (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
(* Goal: forall (s : schedule) (_ : @safe (mkWorld pr) A t s s1) (_ : @ex (proc this (mkWorld pr) A) (fun t2' : proc this (mkWorld pr) A => and (@eq (proc this W A) q (@WithInv this W A pr I ii pf t2')) (@step (mkWorld pr) A s1 t s s2 t2'))), or (@ex A (fun v : A => and6 (@eq schedule (WithInvStep s) WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule (WithInvStep s) (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
- move=>sc HI W A s1 s2 p q; case: p;
           do?[by case|by move=>?; case|by move=>???; case|by move=>????; case].
(* Goal: forall _ : or (@ex A (fun v : A => and6 (@eq schedule sc WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule sc (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))), @pstep W A s1 (@WithInv this W A pr I ii pf t) sc s2 q *)
(* Goal: forall _ : @pstep W A s1 (@WithInv this W A pr I ii pf t) sc s2 q, or (@ex A (fun v : A => and6 (@eq schedule sc WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule sc (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
  move=>pr I ii E p; case/(stepWithInv s1); first by case=>?; case.
  case=>sc'[t'][][]Z1 Z2 _ C1; subst q sc'.
(* Goal: forall (_ : @InMem state s1 (@Mem state (PredPredType state) (Coh (mkWorld (@ProtocolWithIndInv pr I ii))))) (_ : @pstep (mkWorld pr) A s1 t sc s2 t'), @InMem state s2 (@Mem state (PredPredType state) (Coh (mkWorld (@ProtocolWithIndInv pr I ii)))) *)
  by move/HI=>T; subst W; apply: with_inv_step. 
move=>W A s1 s2 t q; do?[by case|by move=>?; case|by move=>???; case].
case=>C; case: t=>//pr I ii E; case=>//=v _[s1'][Z1]Z2 Z3.
(* Goal: forall (_ : @InMem state s1 (@Mem state (PredPredType state) (Coh (mkWorld (@ProtocolWithIndInv pr I ii))))) (_ : @pstep (mkWorld pr) A s1 t sc s2 t'), @InMem state s2 (@Mem state (PredPredType state) (Coh (mkWorld (@ProtocolWithIndInv pr I ii)))) *)
by subst s1' s2 q; apply: Idle. 
Qed.

(*

[Inductive invariants and stepping]

The following lemma is the crux of wrapping into inductive invariants, as 
it leverages the proof of the fact that each transition preserves the invariant.

*)

Lemma pstep_inv A pr I (ii : InductiveInv pr I) s1 s2 sc
      (t t' : proc this (mkWorld pr) A):
(* Goal: forall (_ : match t with | Unfinished => True | Ret a => True | Act a => True | @Seq _ _ _ B p p0 => True | @Inject _ _ _ V K i p => True | WithInv p I0 ii e p0 => True end) (_ : match t with | Unfinished => False | Ret v => @ex state (fun s1' : state => and3 (@eq state s2 s1) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s1 s1')) | Act a => False | @Seq _ _ _ B p0 p1 => False | @Inject _ _ _ V K i p0 => False | WithInv p0 I0 ii e p1 => False end), or (@ex A (fun v : A => and6 (@eq schedule WithInvRet WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule WithInvRet (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
(* Goal: forall (s : schedule) (_ : @safe (mkWorld pr) A t s s1) (_ : @ex (proc this (mkWorld pr) A) (fun t2' : proc this (mkWorld pr) A => and (@eq (proc this W A) q (@WithInv this W A pr I ii pf t2')) (@step (mkWorld pr) A s1 t s s2 t2'))), or (@ex A (fun v : A => and6 (@eq schedule (WithInvStep s) WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule (WithInvStep s) (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
  s1 \In Coh (mkWorld (ProtocolWithIndInv ii)) ->
(* Goal: forall (_ : match t with | Unfinished => True | Ret a => True | Act a => True | @Seq _ _ _ B p p0 => True | @Inject _ _ _ V K i p => True | WithInv p I0 ii e p0 => True end) (_ : match t with | Unfinished => False | Ret v => @ex state (fun s1' : state => and3 (@eq state s2 s1) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s1 s1')) | Act a => False | @Seq _ _ _ B p0 p1 => False | @Inject _ _ _ V K i p0 => False | WithInv p0 I0 ii e p1 => False end), or (@ex A (fun v : A => and6 (@eq schedule WithInvRet WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule WithInvRet (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
(* Goal: forall (s : schedule) (_ : @safe (mkWorld pr) A t s s1) (_ : @ex (proc this (mkWorld pr) A) (fun t2' : proc this (mkWorld pr) A => and (@eq (proc this W A) q (@WithInv this W A pr I ii pf t2')) (@step (mkWorld pr) A s1 t s s2 t2'))), or (@ex A (fun v : A => and6 (@eq schedule (WithInvStep s) WithInvRet) (@eq (proc this (mkWorld pr) A) t (@Ret this (mkWorld pr) A v)) (@eq (proc this W A) q (@Ret this W A v)) (@eq state s2 s1) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))))) (@ex schedule (fun sc' : schedule => @ex (proc this (mkWorld pr) A) (fun t' : proc this (mkWorld pr) A => and5 (@eq schedule (WithInvStep s) (WithInvStep sc')) (@eq (proc this W A) q (@WithInv this W A pr I ii pf t')) (@eq world W (mkWorld (@ProtocolWithIndInv pr I ii))) (@InMem state s1 (@Mem state (PredPredType state) (Coh W))) (@pstep (mkWorld pr) A s1 t sc' s2 t')))) *)
  pstep s1 t sc s2 t' -> 
  s2 \In Coh (mkWorld (ProtocolWithIndInv ii)).
Proof. by move=>C1; case/pstep_network_sem/(with_inv_step C1)/step_coh. Qed.

End ProcessSemantics.
