Skip to content

Commit

Permalink
rm lock, use & short hand
Browse files Browse the repository at this point in the history
  • Loading branch information
@affeldt-aist
affeldt-aist committed Jul 8, 2024
1 parent abbe377 commit f4d1170
Show file tree
Hide file tree
Showing 6 changed files with 26 additions and 30 deletions.
2 changes: 1 addition & 1 deletion example_relabeling.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -89,7 +89,7 @@ transitivity (do x0 <- relabel u;
(do x <- assert q x1; (Ret \o ucat) x));
m x0 x))%Do; last first.
bind_ext => u'; rewrite bind_fmap bindA; bind_ext => sS.
rewrite 4!bindA; bind_ext => x; rewrite 2!bindretf !bindA.
rewrite 4!bindA; bind_ext => x; rewrite 2!bindretf bindA.
by under eq_bind do rewrite bindretf.
rewrite -H1.
rewrite [in LHS]/drBin bind_fmap [in LHS]/bassert /= ![in LHS]bindA.
Expand Down
2 changes: 1 addition & 1 deletion fail_lib.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1431,7 +1431,7 @@ Lemma guard_splits {T A : UU0} (p : pred T) (t : seq T) (f : seq T * seq T -> M
splits t >>= (fun x => guard (all p x.1) >> guard (all p x.2) >> f x).
Proof.
rewrite -plus_commute//.
elim: t => [|h t ih] in p f *; first by rewrite 2!bindretf guardT bindmskip.
elim: t => [|h t ih] in p f *; first by rewrite /= !bindretf.
rewrite [LHS]/= guard_and 2!bindA ih /= plus_commute//.
rewrite bindA; bind_ext => -[a b] /=.
rewrite !alt_bindDl !bindretf /= !guard_and !bindA !alt_bindDr.
Expand Down
Binary file modified hier.png
View file
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
27 changes: 12 additions & 15 deletions hierarchy.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -721,27 +721,26 @@ Arguments fail {_} {_}.
Section guard_assert.
Variable M : failMonad.

Definition guard (b : bool) : M unit := locked (if b then skip else fail).
Definition guard (b : bool) : M unit := if b then skip else fail.

Lemma guardPn (b : bool) : if_spec b skip fail (~~ b) b (guard b).
Proof. by rewrite /guard; unlock; case: ifPn => ?; constructor. Qed.
Proof. by rewrite /guard; case: ifPn => ?; constructor. Qed.

Lemma guardT : guard true = skip. Proof. by rewrite /guard; unlock. Qed.
Lemma guardT : guard true = skip. Proof. by []. Qed.

Lemma guardF : guard false = fail. Proof. by rewrite /guard; unlock. Qed.
Lemma guardF : guard false = fail. Proof. by []. Qed.

(* guard distributes over conjunction *)
Lemma guard_and a b : guard (a && b) = guard a >> guard b.
Proof.
move: a b => -[|] b /=; by [rewrite guardT bindskipf | rewrite guardF bindfailf].
by move: a b => -[|] b /=; [rewrite bindskipf | rewrite bindfailf].
Qed.

Definition assert {A : UU0} (p : pred A) (a : A) : M A :=
locked (guard (p a) >> Ret a).
Definition assert {A : UU0} (p : pred A) (a : A) : M A := guard (p a) >> Ret a.

Lemma assertE {A : UU0} (p : pred A) (a : A) :
assert p a = guard (p a) >> Ret a.
Proof. by rewrite /assert; unlock. Qed.
Proof. by []. Qed.

Lemma assertT {A : UU0} (a : A) : assert xpredT a = Ret a.
Proof. by rewrite assertE guardT bindskipf. Qed.
Expand Down Expand Up @@ -778,8 +777,8 @@ case: guardPn => Hb.
Qed.

End guard_assert.
Arguments assert {M} {A}.
Arguments guard {M}.
Arguments assert {M} {A} : simpl never.
Arguments guard {M} : simpl never.

HB.mixin Record isMonadAlt (M : UU0 -> UU0) of Monad M := {
alt : forall T : UU0, M T -> M T -> M T ;
Expand Down Expand Up @@ -824,8 +823,7 @@ HB.mixin Record isMonadNondet (M : UU0 -> UU0) of MonadFail M & MonadAlt M := {
altmfail : @BindLaws.right_id M (@fail M) (@alt M) }.

#[short(type=nondetMonad)]
HB.structure Definition MonadNondet :=
{M of isMonadNondet M & MonadFail M & MonadAlt M}.
HB.structure Definition MonadNondet := {M of isMonadNondet M & }.

#[short(type=nondetCIMonad)]
HB.structure Definition MonadCINondet := {M of MonadAltCI M & MonadNondet M}.
Expand Down Expand Up @@ -1074,7 +1072,7 @@ HB.mixin Record isMonadArray (S : UU0) (I : eqType) (M : UU0 -> UU0)

#[short(type=arrayMonad)]
HB.structure Definition MonadArray (S : UU0) (I : eqType) :=
{ M of isMonadArray S I M & isMonad M & isFunctor M }.
{ M of isMonadArray S I M & }.

#[short(type=plusArrayMonad)]
HB.structure Definition MonadPlusArray (S : UU0) (I : eqType) :=
Expand Down Expand Up @@ -1311,8 +1309,7 @@ HB.mixin Record isMonadAltProb {R : realType} (M : UU0 -> UU0)

#[short(type=altProbMonad)]
HB.structure Definition MonadAltProb {R : realType} :=
{ M of isMonadAltProb R M & isFunctor M & isMonad M & isMonadAlt M &
isMonadAltCI M & isMonadProb R M & isMonadConvex R M }.
{ M of isMonadAltProb R M & }.

Section altprob_lemmas.
Context {R : realType}.
Expand Down
2 changes: 1 addition & 1 deletion impredicative_set/ifail_lib.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,7 @@ From Equations Require Import Equations.
(* defined as a Fixpoint using insert [1, Sect. 3] *)
(* select s == nondeterministically splits the list s into a *)
(* pair of one chosen element and the rest *)
(* [2, Sect. 3.2] *)
(* [3, Sect. 4.4] [2, Sect. 3.2] *)
(* uperm s == nondeterministically computes a permutation of s, *)
(* defined using unfoldM and select [2, Sect. 3.2] *)
(* splits s == split a list nondeterministically *)
Expand Down
23 changes: 11 additions & 12 deletions impredicative_set/ihierarchy.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -701,27 +701,27 @@ Arguments fail {_} {_}.
Section guard_assert.
Variable M : failMonad.

Definition guard (b : bool) : M unit := locked (if b then skip else fail).
Definition guard (b : bool) : M unit := if b then skip else fail.

Lemma guardPn (b : bool) : if_spec b skip fail (~~ b) b (guard b).
Proof. by rewrite /guard; unlock; case: ifPn => ?; constructor. Qed.
Proof. by rewrite /guard; case: ifPn => ?; constructor. Qed.

Lemma guardT : guard true = skip. Proof. by rewrite /guard; unlock. Qed.
Lemma guardT : guard true = skip. Proof. by []. Qed.

Lemma guardF : guard false = fail. Proof. by rewrite /guard; unlock. Qed.
Lemma guardF : guard false = fail. Proof. by []. Qed.

(* guard distributes over conjunction *)
Lemma guard_and a b : guard (a && b) = guard a >> guard b.
Proof.
move: a b => -[|] b /=; by [rewrite guardT bindskipf | rewrite guardF bindfailf].
by move: a b => -[|] b /=; [rewrite bindskipf | rewrite bindfailf].
Qed.

Definition assert {A : UU0} (p : pred A) (a : A) : M A :=
locked (guard (p a) >> Ret a).
guard (p a) >> Ret a.

Lemma assertE {A : UU0} (p : pred A) (a : A) :
assert p a = guard (p a) >> Ret a.
Proof. by rewrite /assert; unlock. Qed.
Proof. by []. Qed.

Lemma assertT {A : UU0} (a : A) : assert xpredT a = Ret a.
Proof. by rewrite assertE guardT bindskipf. Qed.
Expand Down Expand Up @@ -758,8 +758,8 @@ case: guardPn => Hb.
Qed.

End guard_assert.
Arguments assert {M} {A}.
Arguments guard {M}.
Arguments assert {M} {A} : simpl never.
Arguments guard {M} : simpl never.

HB.mixin Record isMonadAlt (M : UU0 -> UU0) of Monad M := {
alt : forall T : UU0, M T -> M T -> M T ;
Expand Down Expand Up @@ -804,8 +804,7 @@ HB.mixin Record isMonadNondet (M : UU0 -> UU0) of MonadFail M & MonadAlt M := {
altmfail : @BindLaws.right_id M (@fail M) (@alt M) }.

#[short(type=nondetMonad)]
HB.structure Definition MonadNondet :=
{M of isMonadNondet M & MonadFail M & MonadAlt M}.
HB.structure Definition MonadNondet := {M of isMonadNondet M & }.

#[short(type=nondetCIMonad)]
HB.structure Definition MonadCINondet := {M of MonadAltCI M & MonadNondet M}.
Expand Down Expand Up @@ -1054,7 +1053,7 @@ HB.mixin Record isMonadArray (S : UU0) (I : eqType) (M : UU0 -> UU0)

#[short(type=arrayMonad)]
HB.structure Definition MonadArray (S : UU0) (I : eqType) :=
{ M of isMonadArray S I M & isMonad M & isFunctor M }.
{ M of isMonadArray S I M & }.

#[short(type=plusArrayMonad)]
HB.structure Definition MonadPlusArray (S : UU0) (I : eqType) :=
Expand Down

0 comments on commit f4d1170

Please sign in to comment.