Skip to content

Commit

Permalink
rename one law
Browse files Browse the repository at this point in the history
  • Loading branch information
@affeldt-aist
affeldt-aist committed Jul 11, 2024
1 parent 500baea commit b1cbcc8
Show file tree
Hide file tree
Showing 6 changed files with 24 additions and 24 deletions.
2 changes: 1 addition & 1 deletion array_lib.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -35,7 +35,7 @@ Lemma aswapxx i : aswap i i = skip :> M unit.
Proof.
rewrite /aswap agetget.
under eq_bind do rewrite aputput.
by rewrite agetputskip.
by rewrite agetput.
Qed.

End aswap.
Expand Down
2 changes: 1 addition & 1 deletion example_nqueens.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -81,7 +81,7 @@ apply/esym; rewrite /safe2.
set f := fun x => get >>= (fun uds => let (ok, uds') := safe1 uds x in put uds' >> Ret ok) : M _.
rewrite -(@foldr_universal_ext _ _ _ _ f) //;
[apply/esym|move=> cr {}crs; apply/esym].
by rewrite /start2 /f /= -bindA getputskip bindskipf.
by rewrite /start2 /f /= -bindA getput bindskipf.
(* definition of safe1 *)
transitivity
(get >>= (fun uds =>
Expand Down
10 changes: 5 additions & 5 deletions hierarchy.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -826,7 +826,7 @@ HB.mixin Record isMonadNondet (M : UU0 -> UU0) of 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}.
HB.structure Definition MonadCINondet := {M of MonadAltCI M & MonadNondet M }.

Section nondet_big.
Variables (M : nondetMonad) (A : UU0).
Expand Down Expand Up @@ -946,7 +946,7 @@ HB.mixin Record isMonadState (S : UU0) (M : UU0 -> UU0) of Monad M := {
put : S -> M unit ;
putput : forall s s', put s >> put s' = put s' ;
putget : forall s, put s >> get = put s >> Ret s ;
getputskip : get >>= put = skip ;
getput : get >>= put = skip ;
getget : forall (A : UU0) (k : S -> S -> M A),
get >>= (fun s => get >>= k s) = get >>= fun s => k s s }.

Expand Down Expand Up @@ -1058,7 +1058,7 @@ HB.mixin Record isMonadArray (S : UU0) (I : eqType) (M : UU0 -> UU0)
aputput : forall i s s', aput i s >> aput i s' = aput i s' ;
aputget : forall i s (A : UU0) (k : S -> M A), aput i s >> aget i >>= k =
aput i s >> k s ;
agetputskip : forall i, aget i >>= aput i = skip ;
agetput : forall i, aget i >>= aput i = skip ;
agetget : forall i (A : UU0) (k : S -> S -> M A),
aget i >>= (fun s => aget i >>= k s) = aget i >>= fun s => k s s ;
agetC : forall i j (A : UU0) (k : S -> S -> M A),
Expand All @@ -1076,7 +1076,7 @@ HB.structure Definition MonadArray (S : UU0) (I : eqType) :=

#[short(type=plusArrayMonad)]
HB.structure Definition MonadPlusArray (S : UU0) (I : eqType) :=
{ M of MonadPlus M & isMonadArray S I M}.
{ M of MonadPlus M & isMonadArray S I M }.

Variant loc (ml_type : Type) (locT : eqType) : ml_type -> Type :=
mkloc T : locT -> loc locT T.
Expand Down Expand Up @@ -1188,7 +1188,7 @@ HB.mixin Record isMonadStateTrace (S T : UU0) (M : UU0 -> UU0) of Monad M := {
st_mark : T -> M unit ;
st_putput : forall s s', st_put s >> st_put s' = st_put s' ;
st_putget : forall s, st_put s >> st_get = st_put s >> Ret s ;
st_getputskip : st_get >>= st_put = skip ;
st_getput : st_get >>= st_put = skip ;
st_getget : forall (A : UU0) (k : S -> S -> M A),
st_get >>= (fun s => st_get >>= k s) = st_get >>= fun s => k s s ;
st_putmark : forall s e, st_put s >> st_mark e = st_mark e >> st_put s ;
Expand Down
24 changes: 12 additions & 12 deletions monad_model.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -844,12 +844,12 @@ Let putput : forall s s', put s >> put s' = put s'.
Proof. by []. Qed.
Let putget : forall s, put s >> get = put s >> Ret s.
Proof. by []. Qed.
Let getputskip : get >>= put = skip.
Let getput : get >>= put = skip.
Proof. by []. Qed.
Let getget : forall (A : UU0) (k : S -> S -> M A), get >>= (fun s => get >>= k s) = get >>= fun s => k s s.
Proof. by []. Qed.
HB.instance Definition _ := isMonadState.Build S (StateMonad.acto S)
putput putget getputskip getget.
putput putget getput getget.
End state.
End State.
HB.export State.
Expand Down Expand Up @@ -970,7 +970,7 @@ Let st_putput : forall s s', st_put s >> st_put s' = st_put s'.
Proof. by []. Qed.
Let st_putget : forall s, st_put s >> st_get = st_put s >> Ret s.
Proof. by []. Qed.
Let st_getputskip : st_get >>= st_put = skip.
Let st_getput : st_get >>= st_put = skip.
Proof. by move=> *; apply boolp.funext => -[]. Qed.
Let st_getget : forall (A : UU0) (k : S -> S -> M A),
st_get >>= (fun s => st_get >>= k s) = st_get >>= fun s => k s s.
Expand All @@ -981,7 +981,7 @@ Let st_getmark : forall e (k : _ -> M S), st_get >>= (fun v => st_mark e >> k v)
st_mark e >> st_get >>= k.
Proof. by []. Qed.
HB.instance Definition _ := @isMonadStateTrace.Build S T (StateMonad.acto (S * seq T)%type)
st_get st_put st_mark st_putput st_putget st_getputskip st_getget st_putmark st_getmark.
st_get st_put st_mark st_putput st_putget st_getput st_getget st_putmark st_getmark.
End st.
End ModelStateTrace.
HB.export ModelStateTrace.
Expand Down Expand Up @@ -1336,7 +1336,7 @@ rewrite 2!bindE /=; apply/fsetP => /= x; apply/bigfcupP'/bigfcupP'.
exact/fset1P.
apply/imfsetP => /=; exists (tt, s) => //; exact/fset1P.
Qed.
Let getputskip : get >>= put = skip.
Let getput : get >>= put = skip.
Proof.
rewrite boolp.funeqE => s.
rewrite bindE /skip /= /Ret; apply/fsetP => /= x; apply/bigfcupP'/idP.
Expand Down Expand Up @@ -1366,7 +1366,7 @@ rewrite 2!bindE; apply/fsetP => x; apply/bigfcupP'/bigfcupP'.
Qed.

HB.instance Definition _ := isMonadState.Build
S (acto S) putput putget getputskip getget.
S (acto S) putput putget getput getget.

End state.

Expand Down Expand Up @@ -1474,7 +1474,7 @@ Proof.
rewrite state_bindE; apply boolp.funext => a/=.
by rewrite /aput insert_same.
Qed.
Let agetputskip i : aget i >>= aput i = skip.
Let agetput i : aget i >>= aput i = skip.
Proof.
rewrite state_bindE; apply boolp.funext => a/=.
by rewrite /aput insert_same2.
Expand All @@ -1500,7 +1500,7 @@ by rewrite state_bindE/= {1}/insert (negbTE ij).
Qed.
HB.instance Definition _ := Monad.on M.
HB.instance Definition _ := isMonadArray.Build
S I M aputput aputget agetputskip agetget agetC aputC aputgetC.
S I M aputput aputget agetput agetget agetC aputC aputgetC.
End modelarray.
End ModelArray.
HB.export ModelArray.
Expand Down Expand Up @@ -1548,7 +1548,7 @@ apply boolp.funext => a/=; rewrite !bindE /bind set_bindE.
rewrite set_bindE/= bigcup_bigcup !bigcup_set1/= /aput /ModelArray.aput.
by rewrite bindretf/= insert_same.
Qed.
Let agetputskip i : aget i >>= aput i = skip.
Let agetput i : aget i >>= aput i = skip.
Proof.
apply boolp.funext => a/=; rewrite bindE /bind set_bindE bigcup_set1/=.
by rewrite /aput /ModelArray.aput insert_same2.
Expand Down Expand Up @@ -1587,7 +1587,7 @@ rewrite !bindE /bind/= !set_bindE !bigcup_set1/= /aput /ModelArray.aput/=.
by rewrite bindE /bind/= set_bindE bigcup_set1/= {1}/insert (negbTE ij).
Qed.
HB.instance Definition _ := isMonadArray.Build
S I acto aputput aputget agetputskip agetget agetC aputC aputgetC.
S I acto aputput aputget agetput agetget agetC aputC aputgetC.
Let bindfailf : BindLaws.left_zero bind (fun A _ => @set_fail _).
Proof.
by move=> A B/= g; apply boolp.funext => a/=; rewrite /bind bindfailf.
Expand Down Expand Up @@ -1698,7 +1698,7 @@ Let aputput i s s' : aput i s >> aput i s' = aput i s'. Proof. by []. Qed.
Let aputget i s (A : UU0) (k : S -> M A) :
aput i s >> aget i >>= k = aput i s >> k s.
Proof. by []. Qed.
Let agetputskip i : aget i >>= aput i = skip. Proof. by []. Qed.
Let agetput i : aget i >>= aput i = skip. Proof. by []. Qed.
Let agetget i (A : UU0) (k : S -> S -> M A) :
aget i >>= (fun s => aget i >>= k s) = aget i >>= fun s => k s s.
Proof. by []. Qed.
Expand All @@ -1713,7 +1713,7 @@ Let aputgetC i j u (A : UU0) (k : S -> M A) : i != j ->
aput i u >> aget j >>= k = aget j >>= (fun v => aput i u >> k v).
Proof. by []. Qed.
HB.instance Definition _ := isMonadArray.Build
S I acto aputput aputget agetputskip agetget agetC aputC aputgetC.
S I acto aputput aputget agetput agetget agetC aputC aputgetC.
Let fail A := tt : M A.
Let bindfailf : BindLaws.left_zero bind fail.
Proof. by []. Qed.
Expand Down
2 changes: 1 addition & 1 deletion monad_transformer.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -616,7 +616,7 @@ elim: n => [|n ih].
rewrite loop0.
rewrite (_ : sumn (iota 0 0) = 0) //.
rewrite -[LHS]bindskipf.
rewrite -getputskip.
rewrite -getput.
rewrite bindA.
bind_ext => a.
rewrite addn0.
Expand Down
8 changes: 4 additions & 4 deletions state_lib.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -45,7 +45,7 @@ rewrite /protect.
under eq_bind do rewrite bindA bindretf.
rewrite /overwrite.
under eq_bind do rewrite -bindA putput.
by rewrite -bindA getputskip bindskipf.
by rewrite -bindA getput bindskipf.
Qed.

Example test_nonce0 (M : stateMonad nat) : M nat :=
Expand All @@ -67,7 +67,7 @@ elim: n => [|n ih].
rewrite loop0.
rewrite (_ : sumn (iota 0 0) = 0) //.
rewrite -[LHS]bindskipf.
rewrite -getputskip.
rewrite -getput.
rewrite bindA.
bind_ext => a.
rewrite addn0.
Expand All @@ -83,7 +83,7 @@ End stateloop_examples.

Lemma getput_prepend (S : UU0) (M : nondetStateMonad S) A (m : M A) :
m = get >>= (fun x => put x >> m).
Proof. by rewrite -{2}(bindskipf m) -bindA getputskip 2!bindskipf. Qed.
Proof. by rewrite -{2}(bindskipf m) -bindA getput 2!bindskipf. Qed.

Section state_commute.

Expand Down Expand Up @@ -676,7 +676,7 @@ Definition tick : M unit := get >>= (put \o succn).

Lemma tick_fusion n : rep n tick = get >>= (put \o addn n).
Proof.
elim: n => [|n ih]; first by rewrite /= -getputskip.
elim: n => [|n ih]; first by rewrite /= -getput.
rewrite /= /tick ih.
rewrite bindA.
bind_ext => m.
Expand Down

0 comments on commit b1cbcc8

Please sign in to comment.