diff --git a/theory/common/rewriting_system.v b/theory/common/rewriting_system.v index 405eb81f..077da3b6 100644 --- a/theory/common/rewriting_system.v +++ b/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. diff --git a/theory/common/utils.v b/theory/common/utils.v index 1674fc82..eae17494 100644 --- a/theory/common/utils.v +++ b/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. + diff --git a/theory/concur/eventstructure.v b/theory/concur/eventstructure.v index d7d5d2bd..0e75211c 100644 --- a/theory/concur/eventstructure.v +++ b/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. diff --git a/theory/concur/transitionsystem.v b/theory/concur/transitionsystem.v index 1499485d..50e4bf4b 100644 --- a/theory/concur/transitionsystem.v +++ b/theory/concur/transitionsystem.v @@ -86,17 +86,18 @@ Structure add_label := Add { add_po : E; add_write : E; + add_lb_init : (add_lb != Init) && (add_lb != Eps); add_pred_in_dom : add_po \in dom; add_write_in_dom : add_write \in dom; add_write_consist : flab add_write \>> add_lb ; }. Coercion of_add_label := fun - '(Add l p w _ _ _) => mk_edescr l p w. + '(Add l p w _ _ _ _) => mk_edescr l p w. Lemma of_add_label_inj : injective of_add_label. Proof. - case=> ??? +++ [??? +++ [le pe we]]. + case=> ??? ++++ [??? ++++ [le pe we]]. move: le pe we; (do ? case :_ /)=> *; congr Add; exact/eq_irrelevance. Qed. @@ -158,6 +159,23 @@ Lemma add_fed0 : add_fed ident0 = {| lab_prj := Init; fpo_prj := ident0; frf_prj := ident0 |}. Proof. rewrite add_fedE lt_eqF=> //; [ exact/fed0| exact/i0_fresh_seq ]. Qed. +Fact add_lab_Init : + [forall e : finsupp add_fed, (add_lab (val e) == Init) ==> (val e == \i0)]. +Proof. + apply/forallP=> [[/= x]]; rewrite add_labE; case: ifP=> /=. + - case/andP: (add_lb_init al)=> /negbTE-> //. + by move=> *; apply/implyP=> /eqP/lab_Init->. +Qed. + +Fact add_lab_Eps : + [forall e : finsupp add_fed, add_lab (val e) != Eps]. +Proof. + apply/forallP=> [[/= x]]; rewrite add_labE; case: ifP=> /=. + - case/andP: (add_lb_init al)=> ? /negbTE-> //. + rewrite finsupp_with /=; case: ifP=> ?; rewrite ?inE; + [move=> ? /andP[*]| move->=> /= ?]; by rewrite lab_Eps // -fed_dom. +Qed. + Fact add_fpo_dom : [forall e : finsupp add_fed, add_fpo (val e) \in fresh_id :: dom]. Proof. @@ -223,6 +241,8 @@ Definition add_event := (path_fresh_seq dom_sorted) nfresh_dom0 add_fed0 + add_lab_Init + add_lab_Eps add_fpo_dom add_frf_dom add_fpo_le @@ -314,15 +334,16 @@ End AddEvent. Section NreadConsist. -Context (ces : cexec_event_struct) (pr : E) (l : label). +Context (es : exec_event_struct) (pr : E) (l : label). -Notation domain := (dom ces). +Notation domain := (dom es). Notation fresh_id := (fresh_seq domain). Hypothesis pr_mem : pr \in domain. Hypothesis nr : ~~ Label.is_read l. +Hypothesis ni : ~~ Label.is_init l && ~~ Label.is_eps l. -Fact add_nread_synch : lab ces ident0 \>> l. +Fact add_nread_synch : lab es ident0 \>> l. Proof. rewrite lab0 /Label.synch. case H: l=> //; symmetry; apply/contraPF. @@ -330,9 +351,9 @@ Proof. by rewrite /Label.is_read H. Qed. -Let add_label_nread := Add pr_mem dom0 add_nread_synch. +Definition add_label_nread := Add ni pr_mem dom0 add_nread_synch. -Lemma consist_nread : +(*Lemma consist_nread : dom_consistency (add_event add_label_nread). Proof. apply/consist_add_event=> //=; first (by case: ces); exact/cf0. Qed. @@ -342,7 +363,7 @@ Proof. rewrite /add_new_event; case: ifP=> // _. - by case ces. by rewrite ?consist_nread //. -Qed. +Qed.*) End NreadConsist. @@ -368,7 +389,16 @@ Notation "es1 '~>' es2" := (tr es1 es2) (at level 0). Definition ltr (ed : edescr E label) es1 es2 := exists2 al, es2 = @add_event disp _ V es1 al & ed = al. -Notation "es1 '~(' l ')~>' es2" := (ltr es2 es2) (at level 0). +Notation "es1 '~(' l ')~>' es2" := (ltr l es1 es2) (at level 0). + +Lemma ltr_add es (l : edescr E label) (al : add_label es) : + l = al -> es ~(l)~> @add_event disp _ V es al. +Proof. by exists al. Qed. + +Lemma ltr_po es1 l es2 : + es1 ~(l)~> es2 -> fpo_prj l \in dom es1. +Proof. by case: l=> /= > [[> ? [?->]]]. Qed. + Section Equivalence. @@ -405,11 +435,8 @@ Qed. Definition eqv := exlab is_iso. -Lemma eqv_refl : 1 ≦ eqv. -Proof. - move=> ??->. exists id; do ? split=> //; last exact/inv_bij; - rewrite ?map_id // => ? /=; by rewrite edescr_map_id. -Qed. +Lemma is_iso_id es : is_iso id es es. +Proof. split=> // [x/=|]; last exact/inv_bij; by rewrite edescr_map_id. Qed. Lemma is_iso_comp es1 es2 es3 f g : is_iso f es1 es2 -> is_iso g es2 es3 -> @@ -442,7 +469,7 @@ End Equivalence. Notation "e1 ~~ e2" := (eqv e1 e2) (at level 20). -Notation fresh_id1 es := (fresh_seq (dom es)). +Notation fresh_id1 es := (fresh_seq (dom es)). Notation fresh_id2 es := (fresh_seq (fresh_seq (dom es) :: dom es)). Lemma is_iso_swap es1 es2 f e1 e2 : @@ -473,27 +500,42 @@ Qed. Arguments Add {_ _ _ _} _ _ _. -Lemma comm_eqv_tr : - diamond_commute eqv tr. +Lemma iso_swap_eqv es1 es2 es3 f g l : + let: h := swap f (fresh_id1 es1) (g (fresh_id1 es3)) in + cancel g f -> es1 ~(l)~> es2 -> is_iso f es1 es3 -> + exists es4, [/\ es3 ~(edescr_map h l)~> es4 & is_iso h es2 es4]. Proof. - move=> es es3 ? /[swap][][[al ap aw apd awd awc]]->. - case=> f /[dup][[_ [g? c]]] I. - have NI: g (fresh_id1 es3) \notin dom es. + move=> c [[al ap aw ni apd awd awc ->->/= I]]. + have NI: g (fresh_id1 es3) \notin dom es1. - rewrite -(mem_map (bij_inj (proj2 I))) c (iso_dom I) fresh_seq_notin //. exact/dom_sorted. move/(is_iso_swap (fresh_seq_notin dom_sorted) NI): I. - set h := (swap f (fresh_id1 es) (g (fresh_id1 es3))). - move=> /[dup] I [ l /[dup] /bij_inj ? b]. - have H: forall e, e \in dom es -> h e \in dom es3=> [e|]. - by rewrite -(iso_dom I) mem_map. - have [: a1 a2 a3] @s4: add_label es3 := Add al (h ap) (h aw) a1 a2 a3. + set h := (swap f (fresh_id1 es1) (g (fresh_id1 es3))). + move=> /[dup][[L /[dup] /bij_inj ? b I]]. + have H: forall e, e \in dom es1 -> h e \in dom es3=> [e|]. + - by rewrite -(iso_dom I) mem_map. + have [: a1 a2 a3 a4] @a5: add_label es3 := Add al (h ap) (h aw) a1 a2 a3 a4. + - by rewrite ni. 1,2: by apply/H; rewrite (apd, awd). - - move: awc; move: (l aw)=> /=; rewrite /lab. - by case L1: (fed _ aw)=> /=; case L2: (fed es3 (f aw))=> -> /=. - exists (add_event s4); [by exists s4 | exists h]. + - move: awc; move: (L aw)=> /=; rewrite /lab. + by case L1: (fed _ aw)=> /=; case L2: (fed es3 (f aw))=> -> /=. + exists (add_event a5); split; first by exists a5. (do ? split)=> // x /=. - rewrite ?fed_add_eventE /= -[fresh_id1 _]c -(swap1 f (fresh_id1 es)). - rewrite -/h (bij_eq b); case: ifP=> // ?; exact/l. + rewrite ?fed_add_eventE /= -[fresh_id1 _]c -(swap1 f (fresh_id1 es1)). + rewrite -/h (bij_eq b); case: ifP=> // ?; exact/L. +Qed. + +Lemma exlab_tr : tr ≡ exlab ltr. +Proof. by move=> ??; split=> [[l ->]|[?[l ->]]]; do ? exists l. Qed. + +Lemma comm_eqv_tr : + diamond_commute eqv tr. +Proof. + move=> es1 es2 ? [f /[dup][[? [g ? c I]]]]; rewrite (exlab_tr _ _). + case=> l /(iso_swap_eqv c)/(_ I)[es4 [??]]. + set h := (swap f (fresh_id1 es1) (g (fresh_id1 es2))). + exists es4; last by exists h. + rewrite (exlab_tr _ _); by exists (edescr_map h l). Qed. Lemma swap_dom es e : e \in dom es -> @@ -509,9 +551,9 @@ Lemma add_add (es : exec_event_struct) exists al : add_label (add_event al1), al = al2 :> edescr E label. Proof. - case: al2=> l p w ap aw ?. - have [:a1 a2 a3] @al : add_label (add_event al1) := - Add l p w a1 a2 a3; try by rewrite ?inE (ap, aw) orbT. + case: al2=> l p w ni ap aw ?. + have [:a1 a2 a3 a4] @al : add_label (add_event al1) := + Add l p w a1 a2 a3 a4; try by rewrite ?inE ?ni ?(ap, aw) ?orbT. - by rewrite /= lab_add_eventE (lt_eqF (fresh_seq_lt dom_sorted aw)). by exists al; rewrite ?(swap_dom (lexx _)). Qed. @@ -525,7 +567,7 @@ Lemma swap_add es is_iso (swap id (fresh_id1 es) (fresh_id2 es)) (add_event al3) (add_event al4) . Proof. - case: al1 al3 al2 al4=> ??????[/=???+++] [??????[/=???+++ E1 E2]]. + case: al1 al3 al2 al4=> ???????[/=???++++] [???????[/=???++++ E1 E2]]. case: E1 E2; do 3? case:_/; case; (do 3? case:_/)=>*. do ? split; last exact/bij_swap/inv_bij. move=> x /=; rewrite /comp !fed_add_eventE /=. @@ -542,19 +584,26 @@ Proof. by rewrite fsfun_dflt /= -?swap_not_eq // fed_dom I. Qed. -Lemma comm_ltr l1 l2 : - eqv_diamond_commute (ltr l1) (ltr l2) eqv. +Lemma iso_swap es1 es2 es3 l1 l2 : + es1 ~(l1)~> es2 -> + es1 ~(l2)~> es3 -> + exists es4 es4', + [/\ es2 ~(l2)~> es4, + es3 ~(l1)~> es4' & + is_iso (swap id (fresh_id1 es1) (fresh_id2 es1)) es4 es4']. Proof. - move=> es ?? [al1 -> /[swap][[al2->]]]. - case: (add_add al1 al2)=> al3 /[dup]? <-->. - case: (add_add al2 al1)=> al4 /[dup]? <-->. - exists (add_event al3), (add_event al4). - split; [by exists al3| by exists al4|]. - exists (swap id (fresh_id1 es) (fresh_id2 es)); exact/swap_add. + case=> x ->-> [y ->->]. + case: (add_add x y)=> a4; case: (add_add y x)=> a4' ??. + exists (add_event a4), (add_event a4'). + split; by [exists a4| exists a4'| apply/swap_add]. Qed. -Lemma exlab_tr : tr ≡ exlab ltr. -Proof. by move=> ??; split=> [[l ->]|[?[l ->]]]; do ? exists l. Qed. +Lemma comm_ltr l1 l2 : + eqv_diamond_commute (ltr l1) (ltr l2) eqv. +Proof. + move=> es1 ?? /iso_swap/[apply][[x [y [*]]]]. + by exists x, y; split=> //; exists (swap id (fresh_id1 es1) (fresh_id2 es1)). +Qed. End Confluence. diff --git a/theory/lang/regmachine.v b/theory/lang/regmachine.v index 0535e701..5798c505 100644 --- a/theory/lang/regmachine.v +++ b/theory/lang/regmachine.v @@ -1,8 +1,9 @@ +From RelationAlgebra Require Import lattice monoid rel kat kat_tac kleene. From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat seq. -From mathcomp Require Import eqtype choice finfun finmap tuple. +From mathcomp Require Import eqtype choice finfun finmap tuple order. From monae Require Import hierarchy monad_model. From eventstruct Require Import utils eventstructure inhtype. -From eventstruct Require Import transitionsystem ident. +From eventstruct Require Import transitionsystem ident rewriting_system. (******************************************************************************) (* Here we want to define big-step semaintics of simple register machine in *) @@ -55,8 +56,6 @@ Open Scope fmap_scope. Open Scope do_notation. Open Scope exec_eventstruct_scope. -Import Label.Syntax. - Local Notation M := ModelMonad.ListMonad.t. Context {disp} {E : identType disp} {Val : inhType}. @@ -79,11 +78,28 @@ Inductive instr := | CJmp of Reg & nat | Stop. -Definition seqprog := seq instr. +Definition eq_instr st st' := + match st, st' with + | WriteReg x r, WriteReg y s => [&& x == y & r == s] + | ReadLoc x l, ReadLoc y m => [&& x == y & l == m] + | WriteLoc x l, WriteLoc y m => [&& x == y & l == m] + | CJmp r n, CJmp s m => [&& r == s & n == m] + | Stop , Stop => true + | _ , _ => false + end. + +Lemma eqinstrP : Equality.axiom eq_instr. +Proof. + case=> [??|??|??|??|][]*/=; (try by constructor); + by apply/(iffP andP)=> [[/eqP->/eqP]->|[->->]]. +Qed. + +Canonical instr_eqMixin := EqMixin eqinstrP. +Canonical instr_eqType := Eval hnf in EqType instr instr_eqMixin. -Definition empty_prog : seqprog := [::]. +Definition prog := seq instr. -Definition parprog := seq seqprog. +Definition empty_prog : prog := [::]. Record thrd_state := Thrd_state { ip : nat; @@ -105,54 +121,74 @@ Canonical thrd_state_eqType := Definition init_state : thrd_state := {| ip := 0; regmap := [fsfun with inh] |}. Record config := Config { - evstr : cexec_event_struct; - trhdmap :> {fsfun E -> (thrd_state * nat)%type with (init_state, 0)} + evstr :> exec_event_struct; + thrdmap : {fsfun E -> thrd_state with init_state} }. -Notation inth := (nth Stop). +Definition eq_config c c' := + (evstr c == evstr c') && (thrdmap c == thrdmap c'). + +Lemma eqconfigP : Equality.axiom eq_config. +Proof. + by move=> [??] [??]; apply: (iffP andP)=> /= [[/eqP + /eqP]|[]] => <-<-. +Qed. + +Canonical config_eqMixin := EqMixin eqconfigP. +Canonical config_eqType := Eval hnf in EqType config config_eqMixin. + +Coercion thrdmap : config >-> fsfun. -Definition thrd_sem (pgm : seqprog) (st : thrd_state) : - (option (@Lab unit Val) * (Val -> thrd_state))%type := +Definition thrd_prositions := + let fix thrd_pos s n pgm := + match pgm with + | [::] => s + | ins :: pgm => + if ins == Stop then + thrd_pos (n :: s) n.+1 pgm + else thrd_pos s n pgm + end in + thrd_pos [::] 1%N. + +Definition prog_sem (pgm : prog) (st : thrd_state) : + seq (@Lab unit Val * (Val -> thrd_state)) := let: {| ip := ip; regmap := rmap |} := st in - if ip == 0 then - (Some ThreadStart, fun=> {| ip := 1; regmap := rmap |}) + if ip == 0%N then do + ip <- thrd_prositions pgm : M _; + [:: (ThreadStart, + fun _ => {| ip := ip.+1; + regmap := rmap |})] else - match inth pgm ip.-1 with - | WriteReg v r => (None, + match nth Stop pgm ip.-1 with + | WriteReg v r => [:: (Eps, fun _ => {| ip := ip.+1; - regmap := [fsfun rmap with r |-> v] |}) - | ReadLoc r x => (Some (Read x __), + regmap := [fsfun rmap with r |-> v] |})] + | ReadLoc r x => [:: (Read x __, fun v => {| ip := ip.+1; - regmap := [fsfun rmap with r |-> v] |}) - | WriteLoc v x => (Some (Write x v), + regmap := [fsfun rmap with r |-> v] |})] + | WriteLoc v x => [:: (Write x v, fun _ => {| ip := ip.+1; - regmap := rmap |}) - | CJmp r n => (None, + regmap := rmap |})] + | CJmp r n => [:: (Eps, fun _ => {| ip := if rmap r != inh then n.+1 else ip.+1; - regmap := rmap |} ) - | Stop => (None, fun=> st) + regmap := rmap |} )] + | Stop => [:: (Eps, fun=> st)] end. -Definition ltr_thrd_sem (l : option (@Lab Val Val)) pgm st1 st2 : bool := - match thrd_sem pgm st1, l with - | (Some (Write x v), st), Some (Write y u) => [&& x == y, v == u & st inh == st2] - | (Some (Read x _), st), Some (Read y u) => (x == y) && (st u == st2) - | (Some ThreadStart, st), Some ThreadStart => st inh == st2 - | (None , st), None => st inh == st2 - | _, _ => false - end. +Section AddHole. -Variable (es : cexec_event_struct). -Notation ffpo := (fpo es). +Variable (es : exec_event_struct). +Notation ffpred := (fpo es). Notation ffrf := (frf es). Notation fresh_id := (fresh_seq (dom es)). -(* Arguments add_label_of_Nread {_ _ _ _} _ {_}. *) +Arguments add_label_nread {_ _ _ _ _} _. -Lemma ws_mem x w : +Lemma ws_mem x w : w \in [events of es | is_write & with_loc x] -> w \in dom es. Proof. by rewrite ?inE mem_filter => /andP[?->]. Qed. +Import Label.Syntax. + Lemma ws_wpred x w : w \in [events of es | is_write & with_loc x] -> (lab es w) \>> (Read x (odflt inh (value es w))). @@ -165,77 +201,510 @@ Proof. by rewrite !eq_refl. Qed. -Definition es_seq x {pr} : (seq (exec_event_struct * E)) := +Definition es_seq x pr : (seq (exec_event_struct * Val)) := if pr \in dom es =P true is ReflectT pr_mem then [seq let: wr := sval w in let: w_in := valP w in let: read_lab := Read x (odflt inh (value es wr)) in ( - add_new_event + add_event {| add_lb := read_lab; + add_lb_init := erefl; add_pred_in_dom := pr_mem; add_write_in_dom := ws_mem w_in; add_write_consist := ws_wpred w_in; |}, - wr + (odflt inh (value es wr)) ) | w <- seq_in [events of es | is_write & with_loc x]] else [::]. -Definition ces_seq_aux x pr := - [seq estr_w <- @es_seq x pr | - let: (estr, w) := estr_w in - ~~ (cf estr fresh_id w)]. - -Lemma mem_ces_seq_aux x pr ces: - ces \in (@ces_seq_aux x pr) -> dom_consistency ces.1. -Proof. - case: ces => ces w; rewrite mem_filter /= /es_seq => /andP[?]. - case: eqP=> // ? /mapP[?? [/[dup] C -> ws]]. - move: C. rewrite /add_new_event; case: ifP=> _ C; first by case: es. - apply/consist_add_event=> /=; first by case: es. - by rewrite -C -ws. -Qed. - -Definition ces_seq x pr := - [seq - let: ces_w := sval ces_w_mem in - let: (ces, w) := ces_w in - let: ces_mem := valP ces_w_mem in - (Consist _ (mem_ces_seq_aux ces_mem), odflt inh (value es w)) | - ces_w_mem <- seq_in (@ces_seq_aux x pr)]. - -Arguments consist_new_nread {_ _ _}. - -Definition add_hole - (l : @Lab unit Val) pr : - seq (cexec_event_struct * Val) := +Definition add_hole (l : @Lab unit Val) pr : + seq (exec_event_struct * Val) := if pr \in dom es =P true is ReflectT pr_mem then match l with - | Write x v => - [:: (Consist _ (consist_new_nread es pr (Write x v) pr_mem erefl), v)] + | Read x _ => es_seq x pr + | Write x v => + [:: (add_event (add_label_nread (Write x v) pr_mem erefl erefl), v)] | ThreadStart => - [:: (Consist _ (consist_new_nread es pr ThreadStart pr_mem erefl), inh)] - | Read x __ => ces_seq x pr - | _ => [::] + [:: (add_event (add_label_nread ThreadStart pr_mem erefl erefl), inh)] + | ThreadEnd => + [:: (add_event (add_label_nread ThreadEnd pr_mem erefl erefl), inh)] + | _ => [::] end else [::]. -Variable prog : parprog. +End AddHole. -Definition fresh_tid (c : config) := - foldr maxn 0 [seq (snd x).+1 | x <- fgraph (fmap_of_fsfun c)]. +Variable pgm : prog. Definition eval_step (c : config) pr : seq config := - let: Config es tmap := c in - let: (conf, tid) := tmap pr in - let: tid := if pr \in dom es then tid else fresh_tid c in - let: (l, cont_st) := thrd_sem (nth empty_prog prog tid) conf in - if l is Some l then do - ev <- add_hole l pr : M _; - let '(e, v) := ev in - [:: Config e [fsfun c with fresh_id |-> (cont_st v, tid)]] - else - [:: Config es [fsfun c with pr |-> (cont_st inh, tid)]]. + if pr \in dom c then + do prg_st <- prog_sem pgm (c pr) : M _; + let: (l, cont_st) := prg_st in + if l != Eps then do + ev <- add_hole c l pr : M _; + let '(e, v) := ev in + [:: Config e [fsfun c with fresh_seq (dom c) |-> cont_st v]] + else + [:: Config c [fsfun c with pr |-> cont_st inh]] + else [::]. + +End RegMachine. + +Notation fresh_id1 es := (fresh_seq (dom es)). +Notation fresh_id2 es := (fresh_seq (fresh_seq (dom es) :: dom es)). + +Module AddHole. + +Section AddHoleConfl. + +Open Scope fmap_scope. +Open Scope do_notation. +Open Scope exec_eventstruct_scope. + +Context {disp} {E : identType disp} {Val : inhType}. + +(*Notation n := (@n val).*) +Notation exec_event_struct := (fin_exec_event_struct E Val). +Notation cexec_event_struct := (cexec_event_struct E Val). + +Definition ltr (l : (@Lab unit Val) * E * Val) es es' + := (es', l.2) \in add_hole es l.1.1 l.1.2. + +Definition tr es es' := exists (l : (@Lab unit Val)) (pr : E) (v : Val), + (es', v) \in add_hole es l pr. + +Notation "e1 '~(' l ',' pr ',' v ')~>' e2" := (ltr (l, pr, v) e1 e2) (at level 20). + +Lemma exlab_tr : tr ≡ exlab ltr. +Proof. + move=> ??; split=> [[l [pr [v]]]|[[[l pr v]]]] ?; + by [exists (l, pr, v)| exists l, pr, v]. +Qed. + +Notation "e1 '~>' e2" := (tr e1 e2). + +Definition fill_hole (l : @Lab unit Val) (v : Val) := + match l with + | Read x _ => Read x v + | Write x v => Write x v + | ThreadStart => ThreadStart + | ThreadEnd => ThreadEnd + | Eps => Eps + | Init => Init + end. + +Definition mk_hole (l : @Lab Val Val) := + match l with + | Read x v => Read x tt + | Write x v => Write x v + | ThreadStart => ThreadStart + | ThreadEnd => ThreadEnd + | Eps => Eps + | Init => Init + end. + +Lemma fill_mk_hole l : fill_hole (mk_hole l) (odflt inh (Label.value l)) = l. +Proof. by case: l. Qed. + +Import Label.Syntax. + +Arguments add_nread_synch {_ _ _ _} _. + +Lemma ltrP {es1 es2 la pr v} : + reflect + (exists (l : edescr E Lab), + [/\ AddEvent.ltr l es1 es2, + fpo_prj l = pr, + fill_hole la v = lab_prj l & + odflt inh (Label.value (lab_prj l)) = v]) + (es1 ~(la, pr, v)~> es2). +Proof. + apply: (iffP idP). + - rewrite /ltr /= /add_hole; case: eqP=> // p. + case: la=> //=. + - move=> l ?; rewrite /es_seq; case: eqP=> // ?. + rewrite seq_inE=> /mapP=> [[[/= e p' I [-> El]]]]. + exists (mk_edescr (Read l v) pr e); split=> //. + apply/AddEvent.ltr_add=> /=; by rewrite El. + 1-3: move=>>; rewrite ?inE=> /eqP [-><-]; + eexists (mk_edescr _ pr \i0); split=> //; + exact/AddEvent.ltr_add. + rewrite /ltr /==> [[[/= l p w [+ <-]]]]. + move=> /[dup][[[/= ??? + ??? _ []]]]; move=> /[swap]{1 2}<- ni ??. + move=> /[dup] /AddEvent.ltr_po /= Ip /[swap]++/[swap]. + rewrite /add_hole; case: eqP=> [?|]; last by rewrite Ip. + case: la=> /=. + - move=> la _ <- /= _ [[l' p' w' +++++ [el ep ew]]]. + case: _ / ep el ew; (do ? case: _ /)=> ?? wd wc ->. + rewrite /es_seq; case: eqP=> [?|]; last by rewrite Ip. + apply/mapP. + have I: w \in [events of es1 | is_write & with_loc la]. + - move: wc; rewrite mem_filter wd /= /is_write /= /with_loc /= /loc /=. + case: (lab es1 w)=> //= > /andP[/eqP->]; by rewrite eq_refl. + exists (exist _ w I); first by rewrite seq_in_mem. + apply/congr2=> /=; first (apply/congr1/of_add_label_inj=> /=); + by rewrite /value /= (synch_val _ _ _ _ wc). + 1-3: move=>> <- /=-> [al -> Eal]; rewrite ?inE; apply/eqP; + congr (_, _); apply/congr1/of_add_label_inj=> /=; + rewrite -Eal; apply/congr1; case: al Eal=> /= ?? aw ??? /[swap][[<-?->]]; + rewrite /(_ \>> _); case: (lab es1 aw =P Init); last (by case: (lab _ _)); + by move/lab_Init. + all: move=> E'; by rewrite E' eq_refl ?andbF in ni. +Qed. + +Definition eqv := (@AddEvent.eqv disp E Val). + +Lemma iso_swap l1 pr1 v1 l2 pr2 v2 es1 es2 es3: + es1 ~(l1, pr1, v1)~> es2 -> + es1 ~(l2, pr2, v2)~> es3 -> + exists es4 es4', + [/\ es2 ~(l2, pr2, v2)~> es4, + es3 ~(l1, pr1, v1)~> es4' & + AddEvent.is_iso (swap id (fresh_id1 es1) (fresh_id2 es1)) es4 es4']. +Proof. + case/ltrP=> la1 [/AddEvent.iso_swap L ??? /ltrP[la2 [/L]]]. + case=> es4 [es4' [l*]]; exists es4, es4'. + split=> //; apply/ltrP; by [exists la2| exists la1]. +Qed. + +Lemma comm_ltr l1 l2 : eqv_diamond_commute (ltr l1) (ltr l2) eqv. +Proof. + move=> es1 ?? /iso_swap/[apply][[es4 [es4' [*]]]]. + by exists es4, es4'; split=> //; exists (swap id (fresh_id1 es1) (fresh_id2 es1)). +Qed. + +Lemma iso_swap_eqv l1 pr1 v1 f g es1 es2 es3: + let: h := swap f (fresh_id1 es1) (g (fresh_id1 es3)) in + es1 ~(l1, pr1, v1)~> es2 -> + AddEvent.is_iso f es1 es3 -> + cancel g f -> + exists es4, + [/\ es3 ~(l1, h pr1, v1)~> es4 & + AddEvent.is_iso h es2 es4]. +Proof. + case/ltrP=> al [/AddEvent.iso_swap_eqv L H1 H2 H3 {L}/L/[apply]]. + set h := (swap f (fresh_id1 es1) (g (fresh_id1 es3))). + case=> es4 [[al' -> Le ?]]; exists (add_event al'); split=> //. + apply/ltrP; exists (edescr_map h al); split=> //. + - by exists al'. + - rewrite Le; by case: (al') (al) H1 Le=> /= > I ??? [/=> <- [?]]. + 1,2: by move: H2 H3; case: (al). +Qed. + +Lemma comm_eqv_tr : + diamond_commute eqv tr. +Proof. + move=> es1 es2 ?; rewrite (exlab_tr _ _)=> [[f /[dup] [[_ [g ? c I]]]]]. + set h := swap f (fresh_id1 es1) (g (fresh_id1 es2)). + case=> [[[l pr v /iso_swap_eqv/(_ I c)[es4 [??]]]]]. + exists es4; last by exists h. + by rewrite (exlab_tr _ _); exists (l, h pr, v). +Qed. + +Lemma ltr_fresh es1 es2 l v pr : + es1 ~(l, pr, v)~> es2 -> fresh_id2 es1 = fresh_id1 es2. +Proof. by move/ltrP=> [? [[? ->]]]. Qed. + +Lemma ltr_dom es1 es2 l v pr : + es1 ~(l, pr, v)~> es2 -> pr \in dom es1. +Proof. by rewrite /ltr /add_hole; case: eqP. Qed. + +Lemma ltr_dom2 es1 es2 l v pr : + es1 ~(l, pr, v)~> es2 -> dom es2 = fresh_id1 es1 :: dom es1. +Proof. by move/ltrP=> [? [[? ->]]]. Qed. + +End AddHoleConfl. + +End AddHole. + +Module Prog. + +Section ProgConfl. + +Open Scope fmap_scope. +Open Scope do_notation. +Open Scope exec_eventstruct_scope. + +Context {Val : inhType}. + +Variable pgm : prog (Val := Val). + +Definition ltr (l : (@Lab unit Val) * Val) st st' := + (l.1, st') \in [seq (x.1, x.2 l.2) | x <- prog_sem pgm st]. + +Notation "e1 '~(' l ',' v ')~>' e2" := (ltr (l, v) e1 e2) (at level 20). + +Lemma Eps_det st st1 st2 v u l: + st ~(Eps, v)~> st1 -> + st ~(l , u)~> st2 -> + ((st1 = st2) * (l = Eps))%type. +Proof. + case: st=> /=; rewrite /ltr /==> ??; case: ifP=> //. + - move=> ? L; exfalso; move: L; by elim: (thrd_prositions pgm). + by case: (nth Stop pgm _.-1)=> //= > ?; rewrite ?inE=> /eqP[-> /eqP [->]]. +Qed. + +End ProgConfl. + +End Prog. + +Module RegMachine. + +Section RegMachineConfl. + +Import Order.LTheory. + +Open Scope fmap_scope. +Open Scope do_notation. +Open Scope exec_eventstruct_scope. +Open Scope order_scope. + +Local Notation M := ModelMonad.ListMonad.t. + +Context {disp} {E : identType disp} {Val : inhType}. + +(*Notation n := (@n val).*) +Notation exec_event_struct := (fin_exec_event_struct E Val). +Notation cexec_event_struct := (cexec_event_struct E Val). + +Variable pgm : prog (Val := Val). + +Implicit Type c : @config disp E Val. + +Notation eval_step := (eval_step pgm (disp := disp) (E := E)). +Notation Progltr := (Prog.ltr pgm). + +Definition ltr pr (c c' : config) := c' \in eval_step c pr. + +Notation "c1 '~(' pr ')~>' c2" := (ltr pr c1 c2) (at level 20). + +Definition tr := exlab ltr. + +Definition is_iso (f : E -> E) c c' := + AddEvent.is_iso f c c' /\ {in dom c, c =1 c' \o f}. + +Lemma is_iso_id c : is_iso id c c. +Proof. split=> //; exact/AddEvent.is_iso_id. Qed. + +Definition eqv := exlab is_iso. + +Lemma eqvcc c : eqv c c. +Proof. exists id; exact/is_iso_id. Qed. + +Lemma eqv_symm : Symmetric eqv. +Proof. + move=> ?? [f [/[dup][[? [g /[dup] c1 /AddEvent.is_iso_can L /[dup]]]]]]. + move=> {L}/L L c2 /[dup] /L ? I D; exists g; split=> // x. + rewrite -(AddEvent.iso_dom I) -{1}[x]c2 (mem_map (can_inj c1))=> /D /=. + by rewrite c2. +Qed. + +Lemma eqv_evstr c c': eqv c c' -> AddEvent.eqv c c'. +Proof. case=> f []; by exists f. Qed. + +Definition silent_ltr pr c c' := + [/\ Progltr (Eps, inh) (c pr) (c' pr), + pr \in dom c, + [fsfun c with pr |-> c' pr] = c' & + c = c' :> exec_event_struct]. + +Lemma silent_det c c1 c2 pr : + silent_ltr pr c c1 -> + silent_ltr pr c c2 -> + c1 = c2. +Proof. + case=> /Prog.Eps_det L +++ [{L}/L<-]. + case: c1 c2=> /= e1 t1 [/= e2 t2 ? <-<- ? <-<-]. + by rewrite fsfun_with. +Qed. + +Definition non_silent_ltr pr c c' := + exists l v, + [/\ Progltr (l, v) (c pr) (c' (fresh_id1 c)), + l != Eps, + [fsfun c with fresh_id1 c |-> c' (fresh_id1 c)] = c' & + AddHole.ltr (l, pr, v) c c']. + +Lemma non_silent_dom pr c c' : + non_silent_ltr pr c c' -> pr \in dom c. +Proof. by case=> ? [? [??? /AddHole.ltr_dom]]. Qed. + +Lemma silent_dom pr c c' : + silent_ltr pr c c' -> pr \in dom c. +Proof. by case. Qed. + +Lemma ltrP c c' pr : + reflect (silent_ltr pr c c' \/ non_silent_ltr pr c c') + (c ~(pr)~> c'). +Proof. + apply: (iffP idP); rewrite /ltr /eval_step. + - case: ifP=> D //. + have: forall v l st, + (l, st) \in [seq (x.1, x.2 v) | x <- prog_sem pgm (c pr)] -> + Progltr (l, v) (c pr) st by []. + elim: (prog_sem pgm (c pr))=> //=. + move=> [l cont /= conts] IHp H; rewrite do_cons mem_cat=> /orP[]. + - move: H; case: (l =P Eps)=> /= [->/(_ inh Eps (cont inh) (mem_head _ _))|]. + - rewrite ?inE=> P /eqP->; left. + split=> //=; by rewrite fsfun_with. + move=> /eqP ? H /do_mem[[es v ?]]. + rewrite ?inE=> /eqP->; right; exists l, v. + split=> //=; rewrite ?fsfun_with //; exact/H/mem_head. + by apply/IHp=> ??? I; apply/H; rewrite ?inE I. + have H: forall v l st, Progltr (l, v) (c pr) st -> + (l, st) \in [seq (x.1, x.2 v) | x <- prog_sem pgm (c pr)] by []. + case: ifP=> [?|/[swap][[/silent_dom|/non_silent_dom]]->] //. + case=> [|[l[v]]][]; rewrite /Prog.ltr /=; + elim: (prog_sem pgm (c pr))=> //= [][la cont ? /=]; + rewrite do_cons mem_cat; move=> IHp. + - rewrite ?inE=> /orP[/eqP|/IHp/[apply]/[apply]/[apply]->//]. + case=><-->; rewrite eq_refl /= ?inE /eq_op /= /eq_config /==>?<-<-; + by rewrite ?eq_refl. + rewrite ?inE=> /orP[/eqP[->+->]|/IHp/[apply]/[apply]/[apply]->//]. + move=> E1 E2 ?. apply/orP; left; apply/do_mem; exists (evstr c', v)=> //. + by rewrite ?inE /eq_op /= /eq_config /= -E1 E2 ?eq_refl. +Qed. + +Lemma rltrP c c' pr : + ((1 + (silent_ltr pr : hrel _ _))%ra c c' \/ + (1 + (non_silent_ltr pr : hrel _ _))%ra c c') <-> + ((1 + (ltr pr : hrel _ _))%ra c c'). +Proof. + split=> [[|][->|]|[->|/ltrP[]]] *; try by (right + left). + - by right; apply/ltrP; left. + - by right; apply/ltrP; right. + all: by do ? (left + right). +Qed. + +Lemma comm_nnltr {pr1 pr2}: + eqv_rdiamond_commute (non_silent_ltr pr1) (non_silent_ltr pr2) eqv. +Proof. + apply/diamond_rdiamod. + move=> c1 c2 c3 [l [v [?? E1 /[dup]/AddHole.ltr_fresh fr ]]]. + move=> /[dup]/AddHole.ltr_dom I1 /AddHole.iso_swap L [m [u [?? E2]]]. + move=> /[dup]/AddHole.ltr_fresh fr' /[dup] /AddHole.ltr_dom I2 {L}/L. + case=> es4 [es4' [???]]. + have N: (fresh_id1 c1) == (fresh_id2 c1) = false. + - by apply/negbTE/eqP=> /(@fresh_iter _ _ 1 2). + exists (Config es4 [fsfun c2 with fresh_id2 c1 |-> c3 (fresh_id1 c1)]), + (Config es4' [fsfun c3 with fresh_id2 c1 |-> c2 (fresh_id1 c1)]). + split=> /=. + - exists m, u; split=> //=; rewrite -?fr fsfun_with //. + rewrite -E1 fsfun_withE (lt_eqF (fresh_seq_lt dom_sorted I2)) //. + - exists l, v; split=> //=; rewrite -?fr' ?fsfun_with //. + rewrite -E2 fsfun_withE (lt_eqF (fresh_seq_lt dom_sorted I1)) //. + exists (swap id (fresh_id1 c1) (fresh_id2 c1)); split=> //= x. + rewrite -E1 -E2 /=; rewrite fsfun_withE; case: ifP=> [/eqP->|N1]. + - rewrite swap2 ?fsfun_withE eq_refl N //. + rewrite fsfun_withE; case: ifP=> [/eqP->|N2]. + - by rewrite swap1 ?fsfun_with. + by rewrite -swap_not_eq // ?fsfun_withE ?(N1, N2). +Qed. + +Lemma comm_ssltr {pr1 pr2}: + eqv_rdiamond_commute (silent_ltr pr1) (silent_ltr pr2) eqv. +Proof. + move=> c1 c2 c3. + case: (pr1 =P pr2)=> [-> /silent_det/[apply]->|/eqP/negbTE N]. + - exists c3, c3; split; last (exact/eqvcc); by left. + case=> [? D1 C1 E1 [? D2 C2 E2]]. + exists (Config c2 [fsfun c2 with pr2 |-> c3 pr2]), + (Config c3 [fsfun c3 with pr1 |-> c2 pr1]). + split; rewrite -1?C1 -1?C2 ?fsfun_with. + - right; split=> //=; rewrite -?E1 // fsfun_with //. + - rewrite -C1 fsfun_withE eq_sym N //. + by rewrite -{1}C1. + - right; split=> //=; rewrite -?E2 // fsfun_with //. + - rewrite -C2 fsfun_withE N //. + by rewrite -{1}C2. + exists id; rewrite -E1 -E2; split=> /=; first exact/AddEvent.is_iso_id. + move=> ?; rewrite /= ?fsfun_withE; case: ifP=> [/eqP->|//]. + by rewrite eq_sym N. +Qed. + +Lemma comm_nsltr {pr1 pr2}: + eqv_rdiamond_commute (non_silent_ltr pr1) (silent_ltr pr2) eqv. +Proof. + apply/diamond_rdiamod. + move=> c1 c2 c3 [l [v [p1 N C1 L [p2 I2 C2 Ec]]]]. + do ? exists (Config c2 + [fsfun c1 with pr2 |-> c3 pr2, + fresh_id1 c1 |-> c2 (fresh_id1 c1)]). + split=> //=; last exact/eqvcc. + - split=> //=. + - rewrite -{1}C1 ?fsfun_withE eq_refl; case: ifP=> //. + by rewrite (lt_eqF (fresh_seq_lt dom_sorted I2)). + - by rewrite (AddHole.ltr_dom2 L) ?inE I2. + by rewrite fsfun_with -{1}C1. + exists l, v; split=> //=; rewrite -?Ec // ?fsfun_withE. + - rewrite eq_refl eq_sym (lt_eqF (fresh_seq_lt dom_sorted I2)). + rewrite -C2 fsfun_withE. + by case: ifP p2 p1 N=> // /eqP-> /Prog.Eps_det/[apply]->. + rewrite eq_refl eq_sym ((lt_eqF (fresh_seq_lt dom_sorted I2))). + rewrite -{1}C2; apply/fsfunP=> ?; rewrite ?fsfun_withE. + case: ifP=> // /eqP->. + by rewrite eq_sym ((lt_eqF (fresh_seq_lt dom_sorted I2))). +Qed. + +Lemma comm_ltr pr1 pr2 : eqv_rdiamond_commute (ltr pr1) (ltr pr2) eqv. +Proof. + move=> ??? /ltrP[] t1 /ltrP[] t2. + - case: (comm_ssltr t1 t2)=> s4 [s4' [*]]. + 2: case: ((comm_nsltr t2 t1))=> s4' [s4 [?? /eqv_symm ?]]. + 3: case: (comm_nsltr t1 t2)=> s4 [s4' [*]]. + 4: case: (comm_nnltr t1 t2)=> s4 [s4' [*]]. + all: exists s4, s4'; split=> //; apply/rltrP; by (left + right). +Qed. + +Lemma comm_tr_eqv : diamond_commute eqv tr. +Proof. + move=> c1 c3 c2 /[swap][] [pr T]. + have In : pr \in dom c1 by move: T; rewrite /ltr /eval_step; case: ifP. + case/ltrP: T=> [[?? T C [f [/[dup] L [_ b] C1]]]|]. + - exists (Config c3 [fsfun c3 with f pr |-> c2 pr]). + - exists (f pr); apply/ltrP; left; split=> //=. + - move: (C1 _ In)=> /=<-. by rewrite fsfun_with. + - rewrite -(AddEvent.iso_dom L) mem_map //; exact/bij_inj. + by rewrite fsfun_with. + exists f; split=> //= [|?]; rewrite -C // => D. + rewrite /= -T ?fsfun_withE eq_refl (bij_eq b). + by move: (C1 _ D)=> /=->. + case=> l [v [?? E1 /[dup] T /AddHole.iso_swap_eqv L]]. + case=> [f /[dup][[/[dup] Is[? /[dup] bf [g c' c _]]]]] [] /L/(_ c)[es4 []]. + set h := swap f (fresh_id1 c1) (g (fresh_id1 c3))=> ?? /[dup]C /(_ pr) /= Eq. + exists (Config es4 [fsfun c3 with fresh_id1 c3 |-> c2 (fresh_id1 c1)]). + - exists (h pr); apply/ltrP; right; exists l, v; split=> //=. + - rewrite fsfun_with /h -swap_not_eq -?Eq //; apply/eqP; move: In=> /[swap]. + - by move->=>/(negP (fresh_seq_notin dom_sorted)). + move->; rewrite -[dom c1](mapK c') mem_map; last exact/can_inj. + by rewrite (AddEvent.iso_dom Is)=> /(negP (fresh_seq_notin dom_sorted)). + by rewrite fsfun_with. + exists h; split=> // x /=; rewrite -{1}E1 /h /swap fsfun_withE. + case: ifP=> [|]; first rewrite c fsfun_with //. + have D: dom c2 = fresh_id1 c1 :: dom c1 by apply/(AddHole.ltr_dom2 T). + case: ifP=> [/eqP->|N1]; rewrite D ?inE=>-> /=. + - rewrite -[dom c1](mapK c') mem_map; last exact/can_inj. + by rewrite (AddEvent.iso_dom Is)=> /(negP (fresh_seq_notin dom_sorted)). + by move/C=> /=->; rewrite fsfun_withE -[fresh_id1 _]c (bij_eq bf) N1. +Qed. + +Theorem ltr_confl : eqv_rconfluent tr eqv. +Proof. + apply/(eqv_comm_union _ _ _ eqv_symm _ comm_ltr comm_tr_eqv). + - move=> ??? [f [L1 D1 [g [L2 D2]]]]; exists (g \o f); split. + - exact/(AddEvent.is_iso_comp L1 L2). + move=> ? /[dup] D /D1 /=->; apply/D2. + rewrite -(AddEvent.iso_dom L1) mem_map //; exact/bij_inj/(L1.2). + move=> ??->; exact/eqvcc. +Qed. + +End RegMachineConfl. End RegMachine. + + + + +