Temporary PR with confluence proof

theory/common/rewriting_system.v

@@ -208,6 +208,45 @@ Qed.
 
 End EqvRewriting. 
 
+Section EqvRRewriting.
+
+Context {S : Type} (r e : hrel S S).
+
+Hypothesis eqv_trans : Transitive e.
+Hypothesis eqv_symm  : Symmetric e.
+Hypothesis eqv_refl  : 1 ≦ e.
+
+Definition eqv_rdiamond_confluent := forall s1 s2 s3, 
+  r s1 s2 -> r s1 s3 -> 
+  exists s4 s4', [/\ r^? s2 s4, r^? s3 s4' & e s4 s4'].
+
+Definition eqv_rconfluent := forall s1 s2 s3,
+  r^* s1 s2 -> r^* s1 s3 -> 
+  exists s4 s4', [/\ r^* s2 s4, r^* s3 s4' & e s4 s4'].
+
+Hypothesis edconfl : eqv_rdiamond_confluent.
+Hypothesis edcomm : diamond_commute e r.
+
+Theorem rconfl_eqv : eqv_rconfluent.
+Proof.
+  suff: eqv_confluent (r^?) e.
+  - move=> C ???; rewrite ?(str_itr r _ _) ?(itr_qmk r _ _).
+    move=>/C/[apply][[s4 [s4' [*]]]]; exists s4, s4'.
+    by split=> //; rewrite ?(str_itr r _ _) ?(itr_qmk r _ _).
+  apply/confl_eqv=> //.
+  - move=> s1 s2 s3 [-> [->| ?]|R [<-|/(edconfl _ _ _ R)]] //.
+    - exists s3, s3; split; by [left|left|apply/eqv_refl].
+    - exists s3, s3; split; by [right|left|apply/eqv_refl].
+    exists s2, s2; split; by [left|right|apply/eqv_refl].
+  move=> ? s2 ? E [<-|/edcomm-/(_ _ E)[s4 *]].
+  - exists s2=> //; by left.
+  exists s4=> //; by right.
+Qed.
+
+
+End EqvRRewriting.
+
+
 Definition exlab {T L : Type} (r : L -> hrel T T) : hrel T T := 
   fun t1 t2 => exists l, r l t1 t2.
 
@@ -220,18 +259,32 @@ Hypothesis eqv_trans : Transitive e.
 Hypothesis eqv_symm  : Symmetric e.
 Hypothesis eqv_refl  : 1 ≦ e.
 
+Definition eqv_rdiamond_commute (r1 r2 e : hrel S S) := forall s1 s2 s3, 
+   r1 s1 s2 -> r2 s1 s3 -> 
+   exists s4 s4', [/\ r2^? s2 s4, r1^? s3 s4' & e s4 s4'].
+
 Definition eqv_diamond_commute (r1 r2 e : hrel S S) := forall s1 s2 s3, 
    r1 s1 s2 -> r2 s1 s3 -> 
    exists s4 s4', [/\ r2 s2 s4, r1 s3 s4' & e s4 s4'].
 
+Lemma diamond_rdiamod r1 r2 : 
+  eqv_diamond_commute r1 r2 e -> eqv_rdiamond_commute r1 r2 e.
+Proof.
+  move=> D ??? /D/[apply][[s4 [s4' [*]]]].
+  exists s4, s4'; split=> //; by right.
+Qed.
 
-Hypothesis ledrr : forall l1 l2, (eqv_diamond_commute (r l1) (r l2) e).
+Hypothesis ledrr : forall l1 l2, (eqv_rdiamond_commute (r l1) (r l2) e).
 Hypothesis leder  : diamond_commute e (exlab r).
 
-Theorem eqv_comm_union : eqv_confluent (exlab r) e.
+Lemma rexlab : exlab (fun l => (r l)^?) ≦ (exlab r)^?.
+Proof. move=> ?? /= [l [->|]]; [left|right] =>//; by exists l. Qed.
+
+
+Theorem eqv_comm_union : eqv_rconfluent (exlab r) e.
 Proof.
-  apply/confl_eqv => // ???[l1 /ledrr C [l2 /C [s4 [s4' [*]]]]].
-  - exists s4, s4'; do ? split=> //; by [exists l2| exists l1].
+  apply/rconfl_eqv => // ???[l1 /ledrr C [l2 /C [s4 [s4' [*]]]]].
+  - exists s4, s4'; do ? split=> //; apply/rexlab; by [exists l2| exists l1].
 Qed.
 
 End EqvLabRewriting.
@@ -252,7 +305,7 @@ Hypothesis eqv_trans : Transitive e.
 Hypothesis eqv_symm  : Symmetric e.
 Hypothesis eqv_refl  : 1 ≦ e.
 
-Hypothesis ledrr : forall l1 l2, eqv_diamond_commute (r l1) (r l2) e.
+Hypothesis ledrr : forall l1 l2, eqv_rdiamond_commute (r l1) (r l2) e.
 Hypothesis leder : diamond_commute e (exlab r).
 
 Definition eqv_respect_p := [p] ⋅ e ≦ e ⋅ [p].
@@ -268,13 +321,22 @@ Hypothesis eqv_r : r_respect_p.
 Lemma r_exlab l: r l ≦ exlab r.
 Proof. by exists l. Qed.
 
-Theorem sub_eqv_comm_union : eqv_confluent (exlab (sub \o r)) e.
+Lemma rsub l : sub ((r l)^?) ≦ ((sub \o r) l)^? .
+Proof. by move=> ?? [[-> ?|??]]; (left + right). Qed.
+
+Lemma eqv_rr l1 l2 s1 s2 s3 s: 
+  sub (r l1) s1 s2 -> 
+  sub (r l2) s1 s3 ->
+  (r l2)^? s2 s -> p s.
+Proof. by move=> /[dup][[/=? /andP[?? /eqv_r/[apply] H [<-|/H]]]]. Qed.
+
+Theorem sub_eqv_comm_union : eqv_rconfluent (exlab (sub \o r)) e.
 Proof.
   apply/eqv_comm_union=> //.
-  - move=> ????? /= /[dup] /eqv_r R[/ledrr] E /andP[??] /[dup]/R P[/E[s4 [x]]].
+  - move=> ????? /[dup] /eqv_rr R[/ledrr] E /andP[??] /[dup]/R P[/E[s4 [x]]].
     case=> /[dup] /P ps4 ?? /[dup] ?.
     have/eqv_p[??[->??/andP[??]]]: ([p] ⋅ e) s4 x by exists s4.
-    exists s4, x; do ? split=> //; exact/andP.
+    exists s4, x; do ? split=> //; apply/rsub; split=> //; exact/andP.
   move=> s1 s2 s /= /[dup] ? /leder E [? [/r_exlab /E [x [l ?? /andP[??]]]]].
   have/eqv_p[??[->?]]: ([p] ⋅ e) s  x  by exists s.
   have/eqv_p[??[->?]]: ([p] ⋅ e) s1 s2 by exists s1.

theory/common/utils.v

@@ -1,6 +1,7 @@
 From Coq Require Import Relations.
 From mathcomp Require Import ssreflect ssrbool ssrnat ssrfun eqtype.
 From mathcomp Require Import seq path fingraph fintype.
+From monae Require Import hierarchy monad_model.
 
 Set Implicit Arguments.
 Unset Printing Implicit Defensive.
@@ -235,3 +236,25 @@ Definition orelpre (f : T -> option rT) (r : rel rT) : simpl_rel T :=
   [rel x y | match f x, f y with Some x, Some y => r x y | _, _ => false end].
 
 End OptionUtils.
+
+Open Scope do_notation.
+Local Notation M := ModelMonad.ListMonad.t.
+
+Lemma do_mem (T S : eqType) (x : S) (s : M T) (f : T -> M S) : 
+  reflect (exists2 y, y \in s & x \in f y) 
+  (x \in do y <- s; f y).
+Proof.
+  apply: (iffP idP)=> //=;
+    rewrite /Bind /= /ModelMonad.ListMonad.bind /Actm /=;
+    rewrite /monad_lib.Monad_of_ret_bind.Map /ModelMonad.ListMonad.ret /=;
+    rewrite /ModelMonad.ListMonad.bind /= /ModelMonad.ListMonad.ret_component;
+    have->: 
+     flatten [seq (cons^~ [::] \o [eta f]) i | i <- s] 
+     = map f s by (elim: s=> //= ??->).
+    all: by rewrite ?map_id // => /flatten_mapP.
+Qed.
+
+Lemma do_cons (T S : Type) (s : T) (ss : M T) (f : T -> seq S) : 
+  (do y <- (s :: ss : M _); f y) = (f s ++ do y <- ss; f y).
+Proof. by []. Qed.
+

theory/concur/eventstructure.v

@@ -67,6 +67,24 @@ Inductive Lab {RVal WVal : Type} :=
 | Init
 | Eps.
 
+Definition eqlab (RVal WVal : eqType) : rel (@Lab RVal WVal) :=
+  fun l1 l2 => 
+    match l1, l2 with
+    | Read  x a  , Read  y b     => [&& a == b & x == y]
+    | Write x a  , Write y b     => [&& a == b & x == y]
+    | ThreadEnd  , ThreadEnd     => true
+    | ThreadStart, ThreadStart   => true
+    | Init       , Init          => true
+    | Eps        , Eps           => true
+    | _, _                       => false
+    end.
+
+Lemma eq_labP (RVal WVal : eqType) : Equality.axiom (eqlab RVal WVal).
+Proof.
+  case=> [v x [] * /=|v x []* /=|[]|[]|[]|[]]; try constructor=>//;
+  by apply: (iffP andP)=> [[/eqP->/eqP->]|[->->]].
+Qed.
+
 Module Label.
 Section Label. 
 
@@ -108,24 +126,6 @@ Definition is_init : pred Lab :=
 Definition is_eps : pred Lab := 
   fun l => if l is Eps then true else false.
 
-Definition eq_lab : rel Lab :=
-  fun l1 l2 => 
-    match l1, l2 with
-    | Read  x a  , Read  y b     => [&& a == b & x == y]
-    | Write x a  , Write y b     => [&& a == b & x == y]
-    | ThreadEnd  , ThreadEnd     => true
-    | ThreadStart, ThreadStart   => true
-    | Init       , Init          => true
-    | Eps        , Eps           => true
-    | _, _                       => false
-    end.
-
-Lemma eq_labP : Equality.axiom eq_lab.
-Proof.
-  case=> [v x [] * /=|v x []* /=|[]|[]|[]|[]]; try constructor=>//;
-  by apply: (iffP andP)=> [[/eqP->/eqP->]|[->->]].
-Qed.
-
 Definition eq_loc : rel Lab := 
   orelpre loc eq_op.
 
@@ -149,16 +149,13 @@ Definition synch (l1 l2 : Lab) :=
   | _, _ => false
   end.
 
-(* Lemma rf_thrdend w : write_read_from w ThreadEnd = false. *)
-(* Proof. by case: w. Qed. *)
-
 End Label.
 
 Module Exports.
 Section Label.
-Context {V : eqType}.
-Canonical Lab_eqMixin := EqMixin (@eq_labP V).
-Canonical Lab_eqType  := Eval hnf in EqType (@Lab V V) Lab_eqMixin.
+Context {RVal WVal : eqType}.
+Canonical Lab_eqMixin := EqMixin (eq_labP RVal WVal).
+Canonical Lab_eqType  := Eval hnf in EqType (@Lab RVal WVal) Lab_eqMixin.
 End Label.
 End Exports. 
 
@@ -171,6 +168,10 @@ End Label.
 Export Label.Exports. 
 Import Label.Syntax. 
 
+Lemma synch_val Val l x v : 
+  l \>> (Read x v) -> Label.value (Val := Val) l = Some v.
+Proof. by case: l=> //=> /andP[?/eqP->]. Qed.
+
 (* ************************************************************************* *)
 (*     Event Descriptor                                                      *)
 (* ************************************************************************* *)
@@ -285,7 +286,10 @@ Structure fin_exec_event_struct := Pack {
                             fpo_prj := ident0 ;
                             frf_prj := ident0 ;
                          |};
-
+  _          : [forall e : finsupp fed,
+                 (lab (val e) == Init) ==> ((val e) == \i0)];
+
+  _          : [forall e : finsupp fed, lab (val e) != Eps];
   _          : [forall e : finsupp fed, fpo (val e) \in dom];
   _          : [forall e : finsupp fed, frf (val e) \in dom];
 
@@ -305,8 +309,8 @@ Proof.
   have S: finsupp fed0 =i [:: \i0] => [?|].
   - by rewrite /fed0 finsupp_with /= finsupp0 ?inE orbF.
   have F: fed0 \i0 = mk_edescr Init \i0 \i0 by rewrite ?fsfun_with.
-  have [: a1 a2 a3 a4 a5 a6 a7 a8 a9] @evstr : 
-  fin_exec_event_struct := Pack dom0 fed0 a1 a2 a3 a4 a5 a6 a7 a8 a9;
+  have [: a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11] @evstr : 
+  fin_exec_event_struct := Pack dom0 fed0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11;
   rewrite /dom0 ?inE ?eq_refl //.
   - by apply/eqP/fsetP=> ?; rewrite S seq_fsetE.
   all: by apply/forallP=> [[/= x]]; rewrite S ?inE=> /eqP-> /[! F]/=.
@@ -326,13 +330,13 @@ Definition eq_es (es es' : fin_exec_event_struct E Val) : bool :=
 Lemma eqesP : Equality.axiom eq_es.
 Proof.
   move=> x y; apply: (iffP idP)=> [|->]; last by rewrite /eq_es ?eq_refl.
-  case: x=> dom1 fed1 lab1 fpo1 frf1 df1 ds1 di1. 
-  rewrite {}/lab1 {}/fpo1 {}/frf1=> li1 pc1 f1 g1 rc1 rc1'.
-  case: y=> dom2 fed2 lab2 fpo2 frf2 df2 ds2 di2.
-  rewrite {}/lab2 {}/fpo2 {}/frf2=> li2 pc2 f2 g2 rc2 rc2'.
+  case: x=> dom1 fed1 lab1 fpo1 frf1 df1 ds1 di1 dii1. 
+  rewrite {}/lab1 {}/fpo1 {}/frf1=> li1 pc1 f1 g1 l1 rc1 rc1'.
+  case: y=> dom2 fed2 lab2 fpo2 frf2 df2 ds2 di2 dii2.
+  rewrite {}/lab2 {}/fpo2 {}/frf2=> li2 pc2 f2 g2 l2 rc2 rc2'.
   case/andP=> /= /eqP E1 /eqP E2. 
-  move: df1 ds1 di1 li1 pc1 f1 g1 rc1 rc1'. 
-  move: df2 ds2 di2 li2 pc2 f2 g2 rc2 rc2'. 
+  move: df1 ds1 di1 li1 pc1 f1 g1 l1 rc1 rc1' dii1. 
+  move: df2 ds2 di2 li2 pc2 f2 g2 l2 rc2 rc2' dii2. 
   move: E1 E2; do 2 (case: _ /). 
   move=> *; congr Pack; exact/eq_irrelevance.
 Qed.
@@ -375,7 +379,7 @@ Definition is_thrdend : pred E :=
   Label.is_thrdend \o lab. 
 
 Definition eq_lab : rel E :=
-  relpre lab Label.eq_lab.  
+  relpre lab (eqlab Val Val).  
 
 Definition eq_loc : rel E := 
   relpre lab Label.eq_loc.  
@@ -471,12 +475,27 @@ Notation fresh_id := (fresh_seq dom).
 Lemma lab0 : lab ident0 = Init.
 Proof. by rewrite labE; case es=> ???????? H ??? /=; rewrite H. Qed.
 
+Lemma lab_Init e : lab e = Init -> e = \i0.
+Proof.
+  rewrite labE; case es=> ? fed ??????? /= /forallP H ?????? /eqP.
+  case: (boolP (e \in finsupp fed))=> [L|?].
+  - by move/implyP: (H [` L])=> /[apply] /eqP.
+  by rewrite fsfun_dflt.
+Qed.
+
 Lemma lab_fresh : lab fresh_id = Eps.
 Proof. 
   rewrite /lab fsfun_dflt // fed_dom fresh_seq_notin //.
   exact/dom_sorted.
 Qed.
 
+Lemma lab_Eps e : e \in dom -> lab e != Eps.
+Proof.
+  case: es=> ????? I ???? /=; rewrite /eventstructure.lab /=.
+  move/forallP; rewrite -(@seq_fsetE tt) -(eqP I)=> + ????? L.
+  by move/(_ [` L]).
+Qed.
+
 Lemma i0_fresh : \i0 < fresh_id.
 Proof. exact/i0_fresh_seq. Qed.
 
@@ -491,7 +510,7 @@ Lemma fpo_dom e:
   e \in dom -> fpo e \in dom.
 Proof.
   rewrite fed_dom_mem.
-  case: es=> /=; rewrite /eventstructure.fpo /==>> ???? /forallP H ???? L.
+  case: es=> /=; rewrite /eventstructure.fpo /==>> ?????? /forallP H ???? L.
   exact/(H [` L]).
 Qed.
 
@@ -501,7 +520,7 @@ Proof. by move=> ndom; rewrite /fpo fsfun_dflt // fed_dom ndom. Qed.
 Lemma fpo_le e : fpo e <= e.
 Proof.
   rewrite /fpo; case (boolP (e \in finsupp fed)).
-  - case: es=> ??????????? H ?? /= eI. 
+  - case: es=> ????????????? H ?? /= eI. 
     rewrite -[e]/(fsval [` eI]).
     move: H=> /forallP H; exact: H.
   by move=> ndom; rewrite fsfun_dflt.  
@@ -525,7 +544,7 @@ Lemma frf_dom e:
   e \in dom -> frf e \in dom.
 Proof.
   rewrite fed_dom_mem.
-  case: es=> /=; rewrite /eventstructure.frf /==>> ????? /forallP H ??? L.
+  case: es=> /=; rewrite /eventstructure.frf /==>> ??????? /forallP H ??? L.
   exact/(H [` L]).
 Qed.
 
@@ -535,7 +554,7 @@ Proof. by move=> ndom; rewrite /frf fsfun_dflt // fed_dom ndom. Qed.
 Lemma frf_le e : frf e <= e.
 Proof.
   rewrite /frf; case (boolP (e \in finsupp fed)).
-  - case: es=> ???????????? H ? /= eI. 
+  - case: es=> ?????????????? H ? /= eI. 
     rewrite -[e]/(fsval [` eI]).
     move: H=> /forallP H; exact: H.
   by move=> ndom; rewrite fsfun_dflt.  
@@ -544,7 +563,7 @@ Qed.
 Lemma frf_sync e : lab (frf e) \>> lab e. 
 Proof.
   rewrite /lab /fed /frf; case (boolP (e \in finsupp fed)).
-  - case: es=> ????????????? H /= eI. 
+  - case: es=> ??????????????? H /= eI. 
     rewrite -[e]/(fsval [` eI]).
     move: H=> /forallP H; exact: H.
   by move=> ndom; rewrite !fsfun_dflt.