From 5db4f38c9f9ae44a6dd576128b284ea101a96a33 Mon Sep 17 00:00:00 2001
From: Dmitrii Mikhailovskii <mikhaylovskiy.dmitriy@gmail.com>
Date: Sat, 22 May 2021 01:43:46 +0300
Subject: [PATCH] relations: rewrite transitive closure with dependent types

---
 eventstructure.v | 40 ++++++++++++++++++----
 monad.v          | 14 ++++----
 relations.v      | 87 +++++++++++++++++++++++++++++++++---------------
 3 files changed, 101 insertions(+), 40 deletions(-)

diff --git a/eventstructure.v b/eventstructure.v
index 5a0d4eee..ae3bca21 100644
--- a/eventstructure.v
+++ b/eventstructure.v
@@ -3,7 +3,7 @@ From RelationAlgebra Require Import lattice monoid rel kat_tac.
 From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat seq path.
 From mathcomp Require Import eqtype choice order finmap fintype finfun.
 From monae Require Import hierarchy monad_model.
-From event_struct Require Import utilities relations wftype ident inhtype.
+From event_struct Require Import utilities relations wftype ident inhtype monad.
 
 (******************************************************************************)
 (* This file contains the definitions of:                                     *)
@@ -575,7 +575,7 @@ Qed.
 
 (* TODO: consider to generalize this lemma and move to `relations.v` *)
 Lemma fica_gt :
-  (@sfrel _ monad.id_ndmorph E (strictify E _ fica)) ≦ (>%O : rel E).
+  (@sfrel _ monad.id_ndmorph E (strictify _ fica)) ≦ (>%O : rel E).
 Proof. 
   rewrite strictify_weq.
   (* TODO: can ssreflect rewrite do setoid rewrites? *)
@@ -594,8 +594,19 @@ Proof. by []. Qed.
 Lemma ica_le e1 e2 : ica e1 e2 -> e1 <= e2.
 Proof. exact: fica_ge. Qed.
 
+Definition sica e1 e2 := e1 \in (strictify _ fica e2).
+
+Lemma sica_lt e1 e2 : sica e1 e2 -> e1 < e2.
+Proof. exact: fica_gt. Qed.
+
+Definition dep_fica (e1 : E) : ModelNondet.list {e : E | e < e1} :=
+  map (fun e => eqtype.Sub (val e) (@sica_lt (val e) e1 (valP e)))
+    (seq_in ((strictify _ fica) e1)).
+
+Import monad_lib.Monad_of_ret_bind ModelMonad.ListMonad.
+
 (* Causality relation *)
-Definition ca : rel E := (rt_closure fica_gt)°.
+Definition ca : rel E := (rt_closure id_ndmorph dep_fica)°.
 
 Lemma closureP e1 e2 :
   reflect (clos_refl_trans _ ica e1 e2) (ca e1 e2).
@@ -614,8 +625,25 @@ Proof.
     by apply /rel_weq_m; rewrite -strictify_weq.
   rewrite rel_qmk_m.
   rewrite -itr_qmk -str_itr.
-  rewrite -clos_refl_trans_hrel_str.
-  apply /reflect_weq/rt_closureP.
+  rewrite -clos_refl_trans_hrel_str /= /hrel_cnv /dhrel_cnv.
+  have: (strictify ModelNondet.list fica) =1 f_ _ dep_fica.
+  { move=> ?.
+    rewrite /dep_fica /f_ /= /Actm /= /Map /bind /comp /ret /= /ret_component.
+    by rewrite -seq.map_comp flatten_map1 val_seq_in. }
+  move=> DH.
+  have: forall x y, clos_refl_trans E
+      (@sfrel _ id_ndmorph _ (strictify _ fica)) x y <->
+    clos_refl_trans E (@sfrel _ id_ndmorph _ (f_ _ dep_fica)) x y.
+  { move=> x y. split.
+    { elim=> //=.
+      { rewrite /sfrel /=. move=> z h H. apply: rt_step. by rewrite -DH. }
+      move=> z h l ? IHzh ? IHhl. apply: rt_trans. exact: IHzh. done. }
+    elim=> //=.
+    { rewrite /sfrel /=. move=> z h H. apply: rt_step. by rewrite DH. }
+    move=> z h l ? IHzh ? IHhl. apply: rt_trans. exact: IHzh. done. }
+  move=> H x y. split.
+  { move=> HH. by apply /rt_closureP/H. }
+  by move=> /rt_closureP /H.
 Qed.
 
 Lemma closure_n1P e1 e2 :
@@ -708,7 +736,7 @@ Proof.
   by apply/H/ica0.
 Qed.
 
-Definition seqpred_ca := wsuffix fica_gt.
+Definition seqpred_ca := wsuffix _ dep_fica.
 
 Lemma seqpred_ca_in e1 e2 : e1 \in seqpred_ca e2 = ca e1 e2.
 Proof. by []. Qed.
diff --git a/monad.v b/monad.v
index 73b8a481..7766b68c 100644
--- a/monad.v
+++ b/monad.v
@@ -42,12 +42,12 @@ Lemma join_morph (M N : monad) (η: M ≈> N) :
     η a (Join m) = Join (η (N a) ((M # (η a)) m)).
 Proof. case: η => cpmm; by case. Qed.
 
-Lemma bind_morph (T : Type) (M N : monad) (η : M ≈> N) (m : M T) (k : T -> M T) :
-  η T (m >>= k) = (η T m) >>= (fun x => η T (k x)).
+Lemma bind_morph (T T' : Type) (M N : monad) (η : M ≈> N) (m : M T) (k : T -> M T') :
+  η T' (m >>= k) = (η T m) >>= (fun x => η T' (k x)).
 Proof.
   rewrite /Bind join_morph.
   rewrite <- monad_lib.fmap_oE.
-  fold (comp (η (N T)) (M # (η T \o k)) m).
+  fold (comp (η (N T')) (M # (η T' \o k)) m).
   by rewrite -natural. 
 Qed.
 
@@ -103,7 +103,7 @@ Section ListMonadMorphismTheory.
 Import NDMonadMorphism.Syntax.
 Import ModelNondet ModelMonad ListMonad.
 
-Context {T : eqType}.
+Context {T T' : eqType}.
 Variable (M : nondetMonad) (η : M ≈> ModelNondet.list).
 
 Lemma ret_morph_list (x : T) :
@@ -136,8 +136,8 @@ Lemma mem_alt (x : T) (m n : M T) :
   x \in η T (Alt m n) = (x \in η T m) || (x \in η T n).
 Proof. by rewrite alt_morph mem_cat. Qed.
 
-Lemma mem_bindP (s : M T) (k : T -> M T) (y : T) :
-  reflect (exists2 x, x \in η T s & y \in η T (k x)) (y \in η T (s >>= k)).
+Lemma mem_bindP (s : M T) (k : T -> M T') (y : T') :
+  reflect (exists2 x, x \in η T s & y \in η T' (k x)) (y \in η T' (s >>= k)).
 Proof.
   apply /(iffP idP).
   { rewrite bind_morph => /flatten_mapP.
@@ -145,7 +145,7 @@ Proof.
     rewrite mem_seq1 => /eqP -> ymx.
     by exists x. }
   move => [] x xs ymx. rewrite bind_morph.
-  apply /flatten_mapP. exists (η T (k x)) => //.
+  apply /flatten_mapP. exists (η T' (k x)) => //.
   apply /flatten_mapP. exists x => //. exact: mem_head.
 Qed.
 
diff --git a/relations.v b/relations.v
index 28003432..658930ef 100644
--- a/relations.v
+++ b/relations.v
@@ -57,22 +57,25 @@ Definition sfrel {M : nondetMonad} {η : M ≈> List}
 
 Section Strictify.
 
-Context (T : eqType).
-Variable  (M : nondetMonad) (η : M ≈> List).
-Implicit Type (f : T -> M T).
+Context {disp : unit} {T : wfType disp}.
+Variable  (M : nondetMonad) (f : forall (x : T), M {y : T | y < x}) (η : M ≈> List).
+Implicit Type (f : forall (x : T), M {y : T | y < x}).
+
+Definition f_ : T -> M T :=
+  fun x => (M # val) (f x).
 
-Definition strictify f : T -> M T :=
-  fun x => mfilter M (f x) (fun y => x != y).
+Definition strictify (g : T -> M T) : T -> M T :=
+  fun x => mfilter M (g x) (fun y => x != y).
 
-Lemma strictify_weq f :
-  @sfrel M η T (strictify f) ≡ (@sfrel M η T f \ eq_op).
+Lemma strictify_weq (g : T -> M T) :
+  @sfrel M η T (strictify g) ≡ (@sfrel M η T g \ eq_op).
 Proof. 
   move=> x y; rewrite /sfrel /strictify /mfilter /=.
   by rewrite mem_mfilter andbC. 
 Qed.
 
-Lemma strictify_leq f : 
-  @sfrel M η T (strictify f) ≦ @sfrel M η T f.
+Lemma strictify_leq g :
+  @sfrel M η T (strictify g) ≦ @sfrel M η T g.
 Proof. by rewrite strictify_weq; lattice. Qed.
 
 End Strictify. 
@@ -83,10 +86,12 @@ Section WfRTClosure.
 
 Context {disp : unit} {T : wfType disp}.
 
-Variable (M : nondetMonad) (η : M ≈> List) (f : T -> M T).
+Variable (M : nondetMonad) (η : M ≈> List) (f : forall (x : T), M {y : T | y < x}).
 
 (* Hypothesis descend : forall x y, y \in f x -> y < x. *)
-Hypothesis descend : @sfrel M η T f ≦ (>%O).
+(* Hypothesis descend : @sfrel M η T f ≦ (>%O). *)
+
+
 
 (* A hack to get around a bug in Equations 
  * (see https://github.com/mattam82/Coq-Equations/issues/241).
@@ -97,12 +102,7 @@ Hypothesis descend : @sfrel M η T f ≦ (>%O).
  Definition suffix_aux (x : T) (rec : forall y : T, y < x -> M T) := 
   let ys := f x in 
   let ps := ys >>= (fun x => 
-    if x \in η T ys =P true is ReflectT pf then
-      rec x (descend _ _ pf)
-    else
-      Fail
-  ) in 
-  Alt ys ps.
+    rec (val x) (valP x)) in Alt ((M # val) ys) ps.
 
 (* strict suffix of an element `x`, i.e. a set { y | x R y } *)
 Equations suffix (x : T) : M T by wf x (<%O : rel T) := 
@@ -124,32 +124,65 @@ Definition rt_closure : {dhrel T & T} :=
 (*       THEORY                                                               *)
 (* ************************************************************************** *)
 
+Import monad_lib.Monad_of_ret_bind ModelMonad.ListMonad.
+
+Lemma dec x y : x \in η T (f_ _ f y) -> x < y.
+Proof.
+  have H: η T ((M # val) (f y)) = ((η T) \o (M # val)) (f y) by [].
+  have: (x \in η T (f_ M f y)) = (x \in map val (η _ (f y))).
+  { rewrite /f_ H -natural /= /Actm /= /Map /bind /ret /= /ret_component /comp.
+    by rewrite flatten_map1. }
+  by move=> ->=> /mapP [z]; case z=> {}z Hz /= _ ->.
+Qed.
+
+Lemma strict_lt n k : k \in η T (strictify M (f_ _ f) n) -> k < n.
+Proof. rewrite mem_mfilter => /andP[] ??. by rewrite dec. Qed.
+
+Lemma val_mem y x : x \in η _ (f y) -> val x \in η T (f_ _ f y).
+Proof.
+  have HH: η T ((M # val) (f y)) = ((η T) \o (M # val)) (f y) by [].
+  rewrite HH -natural /= /Actm /= /Map /bind /ret /= /ret_component /comp.
+  rewrite flatten_map1 => H. by apply map_f.
+Qed.
+
+Lemma mon_in x y (p : x < y) :
+  x \in η _ (f_ _ f y) -> exist _ x p \in η _ (f y).
+Proof.
+  move=> H. rewrite /=.
+  have: η {y0 : T | y0 < y} (f y) = pmap insub (η T (f_ M f y)).
+  { have: η T ((M # val) (f y)) = (η T \o (M # val)) (f y) by [].
+    rewrite /f_ => ->. rewrite -natural /Actm /= /Map /bind /comp flatten_map1.
+    elim: (η {y0 : T | y0 < y} (f y))=> //= z s IHs.
+    by rewrite -IHs /oapp valK. }
+  move=> ->. by rewrite mem_pmap_sub.
+Qed.
+
 Lemma t_closure_1nP x y : 
-  reflect (clos_trans_1n T (@sfrel M η T f) x y) (t_closure x y).
+  reflect (clos_trans_1n T (@sfrel M η _ (f_ _ f)) x y) (t_closure x y).
 Proof.
   rewrite /t_closure. funelim (suffix x)=> /=. 
   apply /(iffP idP); rewrite mem_alt /sfrel /=.
-  { move=> /orP[|/mem_bindP[z]] //; first exact: t1n_step.
-    case: eqP=> // S /descend yz /X tr. 
-    move: (tr yz) => H.
-    by apply: t1n_trans; first exact: S. }
+  { move=> /orP[|/mem_bindP[z PP]] //; first exact: t1n_step.
+    move: (val_mem x z PP) => S /X H. apply: t1n_trans; first exact: S.
+    by apply: H; exact: dec. }
   move: X=> /[swap] [[?->//|{}y ? /[dup] ? L /[swap]]].
   move=> /[apply] H; apply/orP; right; apply/mem_bindP.
-  exists y=> //. case: eqP => // /descend yz. exact: H.
+  eexists; first by apply: mon_in (L); exact: (dec y x L).
+  move=> /=. by apply: H; first exact: (dec y x L).
 Qed.
 
 Lemma t_closureP x y :
-  reflect (clos_trans T (@sfrel M η T f) x y) (t_closure x y).
+  reflect (clos_trans T (@sfrel M η _ (f_ _ f)) x y) (t_closure x y).
 Proof.
   apply /(equivP (t_closure_1nP x y)).
   symmetry; exact: clos_trans_t1n_iff.
 Qed.
 
 Lemma clos_trans_gt : 
-  clos_trans T (@sfrel M η T f) ≦ (>%O : rel T).
+  clos_trans T (@sfrel M η _ (f_ _ f)) ≦ (>%O : rel T).
 Proof. 
   move=> ??; rewrite/sfrel /=.
-  elim=> [y z /descend | x y z _ ] //=.
+  elim=> [y z /dec | x y z _ ] //=.
   move=> /[swap] _ /[swap]; exact: lt_trans.
 Qed.
 
@@ -169,7 +202,7 @@ Proof.
 Qed.
 
 Lemma rt_closureP x y :
-  reflect (clos_refl_trans T (@sfrel M η T f) x y) (rt_closure x y).
+  reflect (clos_refl_trans T (@sfrel M η _ (f_ _ f)) x y) (rt_closure x y).
 Proof.
   apply /equivP; last first.
   { rewrite clos_refl_transE clos_refl_hrel_qmk.