Commit 97c9080c authored by Robbert Krebbers's avatar Robbert Krebbers

Add monadic ;; and change level of do-notation to 100.

This way, we will be compabile with Iris's heap_lang, which puts ;;
at level 100.
parent ffb7f0cc
......@@ -865,23 +865,26 @@ Notation "(≫= f )" := (mbind f) (only parsing) : C_scope.
Notation "(≫=)" := (λ m f, mbind f m) (only parsing) : C_scope.
Notation "x ← y ; z" := (y = (λ x : _, z))
(at level 65, only parsing, right associativity) : C_scope.
(at level 100, only parsing, right associativity) : C_scope.
Infix "<$>" := fmap (at level 60, right associativity) : C_scope.
Notation "' ( x1 , x2 ) ← y ; z" :=
(y = (λ x : _, let ' (x1, x2) := x in z))
(at level 65, only parsing, right associativity) : C_scope.
(at level 100, z at level 200, only parsing, right associativity) : C_scope.
Notation "' ( x1 , x2 , x3 ) ← y ; z" :=
(y = (λ x : _, let ' (x1,x2,x3) := x in z))
(at level 65, only parsing, right associativity) : C_scope.
(at level 100, z at level 200, only parsing, right associativity) : C_scope.
Notation "' ( x1 , x2 , x3 , x4 ) ← y ; z" :=
(y = (λ x : _, let ' (x1,x2,x3,x4) := x in z))
(at level 65, only parsing, right associativity) : C_scope.
(at level 100, z at level 200, only parsing, right associativity) : C_scope.
Notation "' ( x1 , x2 , x3 , x4 , x5 ) ← y ; z" :=
(y = (λ x : _, let ' (x1,x2,x3,x4,x5) := x in z))
(at level 65, only parsing, right associativity) : C_scope.
(at level 100, z at level 200, only parsing, right associativity) : C_scope.
Notation "' ( x1 , x2 , x3 , x4 , x5 , x6 ) ← y ; z" :=
(y = (λ x : _, let ' (x1,x2,x3,x4,x5,x6) := x in z))
(at level 65, only parsing, right associativity) : C_scope.
(at level 100, z at level 200, only parsing, right associativity) : C_scope.
Notation "x ;; z" := (x = λ _, z)
(at level 100, z at level 200, only parsing, right associativity): C_scope.
Notation "ps .*1" := (fmap (M:=list) fst ps)
(at level 10, format "ps .*1").
......@@ -891,11 +894,10 @@ Notation "ps .*2" := (fmap (M:=list) snd ps)
Class MGuard (M : Type Type) :=
mguard: P {dec : Decision P} {A}, (P M A) M A.
Arguments mguard _ _ _ !_ _ _ / : assert.
Notation "'guard' P ; o" := (mguard P (λ _, o))
(at level 65, only parsing, right associativity) : C_scope.
Notation "'guard' P 'as' H ; o" := (mguard P (λ H, o))
(at level 65, only parsing, right associativity) : C_scope.
Notation "'guard' P ; z" := (mguard P (λ _, z))
(at level 100, z at level 200, only parsing, right associativity) : C_scope.
Notation "'guard' P 'as' H ; z" := (mguard P (λ H, z))
(at level 100, z at level 200, only parsing, right associativity) : C_scope.
(** * Operations on maps *)
(** In this section we define operational type classes for the operations
......
......@@ -797,7 +797,7 @@ Global Instance collection_guard `{CollectionMonad M} : MGuard M :=
Section collection_monad_base.
Context `{CollectionMonad M}.
Lemma elem_of_guard `{Decision P} {A} (x : A) (X : M A) :
x guard P; X P x X.
(x guard P; X) P x X.
Proof.
unfold mguard, collection_guard; simpl; case_match;
rewrite ?elem_of_empty; naive_solver.
......@@ -805,7 +805,7 @@ Section collection_monad_base.
Lemma elem_of_guard_2 `{Decision P} {A} (x : A) (X : M A) :
P x X x guard P; X.
Proof. by rewrite elem_of_guard. Qed.
Lemma guard_empty `{Decision P} {A} (X : M A) : guard P; X ¬P X .
Lemma guard_empty `{Decision P} {A} (X : M A) : (guard P; X) ¬P X .
Proof.
rewrite !elem_of_equiv_empty; setoid_rewrite elem_of_guard.
destruct (decide P); naive_solver.
......@@ -945,7 +945,7 @@ Section collection_monad.
Lemma collection_bind_singleton {A B} (f : A M B) x : {[ x ]} = f f x.
Proof. set_solver. Qed.
Lemma collection_guard_True {A} `{Decision P} (X : M A) : P guard P; X X.
Lemma collection_guard_True {A} `{Decision P} (X : M A) : P (guard P; X) X.
Proof. set_solver. Qed.
Lemma collection_fmap_compose {A B C} (f : A B) (g : B C) (X : M A) :
g f <$> X g <$> (f <$> X).
......
......@@ -1212,7 +1212,7 @@ End more_merge.
(** Properties of the zip_with function *)
Lemma map_lookup_zip_with {A B C} (f : A B C) (m1 : M A) (m2 : M B) i :
map_zip_with f m1 m2 !! i = x m1 !! i; y m2 !! i; Some (f x y).
map_zip_with f m1 m2 !! i = (x m1 !! i; y m2 !! i; Some (f x y)).
Proof.
unfold map_zip_with. rewrite lookup_merge by done.
by destruct (m1 !! i), (m2 !! i).
......
......@@ -3394,7 +3394,7 @@ Section zip_with.
Forall2 P l k → length (zip_with f l k) = length k.
Proof. induction 1; simpl; auto. Qed.
Lemma lookup_zip_with l k i :
zip_with f l k !! i = x ← l !! i; y ← k !! i; Some (f x y).
zip_with f l k !! i = (x ← l !! i; y ← k !! i; Some (f x y)).
Proof.
revert k i. induction l; intros [|??] [|?]; f_equal/=; auto.
by destruct (_ !! _).
......
......@@ -336,13 +336,13 @@ Tactic Notation "case_option_guard" :=
let H := fresh in case_option_guard as H.
Lemma option_guard_True {A} P `{Decision P} (mx : option A) :
P guard P; mx = mx.
P (guard P; mx) = mx.
Proof. intros. by case_option_guard. Qed.
Lemma option_guard_False {A} P `{Decision P} (mx : option A) :
¬P guard P; mx = None.
¬P (guard P; mx) = None.
Proof. intros. by case_option_guard. Qed.
Lemma option_guard_iff {A} P Q `{Decision P, Decision Q} (mx : option A) :
(P Q) guard P; mx = guard Q; mx.
(P Q) (guard P; mx) = guard Q; mx.
Proof. intros [??]. repeat case_option_guard; intuition. Qed.
Tactic Notation "simpl_option" "by" tactic3(tac) :=
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment