Skip to content

relations: rewrite transitive closure with dependent types #97

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open

relations: rewrite transitive closure with dependent types #97

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
40 changes: 34 additions & 6 deletions eventstructure.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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: *)
Expand Down Expand Up @@ -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? *)
Expand All @@ -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).
Expand All @@ -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 :
Expand Down Expand Up @@ -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.
Expand Down
14 changes: 7 additions & 7 deletions monad.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.

Expand Down Expand Up @@ -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) :
Expand Down Expand Up @@ -136,16 +136,16 @@ 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.
move => [] l /flatten_mapP [] x xs.
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.

Expand Down
87 changes: 60 additions & 27 deletions relations.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand All @@ -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).
Expand All @@ -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) :=
Expand All @@ -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.

Expand All @@ -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.
Expand Down