Commit 0b645878 authored by Ralf Jung's avatar Ralf Jung

Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq

parents 66f99021 66f61d49
......@@ -393,6 +393,35 @@ Section cmra_monotone.
Proof. rewrite !cmra_valid_validN; eauto using validN_preserving. Qed.
End cmra_monotone.
(** * Transporting a CMRA equality *)
Definition cmra_transport {A B : cmraT} (H : A = B) (x : A) : B :=
eq_rect A id x _ H.
Section cmra_transport.
Context {A B : cmraT} (H : A = B).
Notation T := (cmra_transport H).
Global Instance cmra_transport_ne n : Proper (dist n ==> dist n) T.
Proof. by intros ???; destruct H. Qed.
Global Instance cmra_transport_proper : Proper (() ==> ()) T.
Proof. by intros ???; destruct H. Qed.
Lemma cmra_transport_op x y : T (x y) = T x T y.
Proof. by destruct H. Qed.
Lemma cmra_transport_unit x : T (unit x) = unit (T x).
Proof. by destruct H. Qed.
Lemma cmra_transport_validN n x : {n} (T x) {n} x.
Proof. by destruct H. Qed.
Lemma cmra_transport_valid x : (T x) x.
Proof. by destruct H. Qed.
Global Instance cmra_transport_timeless x : Timeless x Timeless (T x).
Proof. by destruct H. Qed.
Lemma cmra_transport_updateP (P : A Prop) (Q : B Prop) x :
x ~~>: P ( y, P y Q (T y)) T x ~~>: Q.
Proof. destruct H; eauto using cmra_updateP_weaken. Qed.
Lemma cmra_transport_updateP' (P : A Prop) x :
x ~~>: P T x ~~>: λ y, y', y = cmra_transport H y' P y'.
Proof. eauto using cmra_transport_updateP. Qed.
End cmra_transport.
(** * Instances *)
(** ** Discrete CMRA *)
Class RA A `{Equiv A, Unit A, Op A, Valid A, Minus A} := {
......
......@@ -3,8 +3,8 @@ Require Import algebra.functor.
Section cofe.
Context `{Countable K} {A : cofeT}.
Implicit Types m : gmap K A.
(* COFE *)
Instance map_dist : Dist (gmap K A) := λ n m1 m2,
i, m1 !! i ={n}= m2 !! i.
Program Definition map_chain (c : chain (gmap K A))
......@@ -36,44 +36,45 @@ Global Instance lookup_ne n k :
Proof. by intros m1 m2. Qed.
Global Instance lookup_proper k :
Proper (() ==> ()) (lookup k : gmap K A option A) := _.
Global Instance insert_ne (i : K) n :
Global Instance insert_ne i n :
Proper (dist n ==> dist n ==> dist n) (insert (M:=gmap K A) i).
Proof.
intros x y ? m m' ? j; destruct (decide (i = j)); simplify_map_equality;
[by constructor|by apply lookup_ne].
Qed.
Global Instance singleton_ne (i : K) n :
Global Instance singleton_ne i n :
Proper (dist n ==> dist n) (singletonM i : A gmap K A).
Proof. by intros ???; apply insert_ne. Qed.
Global Instance delete_ne (i : K) n :
Global Instance delete_ne i n :
Proper (dist n ==> dist n) (delete (M:=gmap K A) i).
Proof.
intros m m' ? j; destruct (decide (i = j)); simplify_map_equality;
[by constructor|by apply lookup_ne].
Qed.
Instance map_empty_timeless : Timeless ( : gmap K A).
Proof.
intros m Hm i; specialize (Hm i); rewrite lookup_empty in Hm |- *.
inversion_clear Hm; constructor.
Qed.
Global Instance map_lookup_timeless (m : gmap K A) i :
Timeless m Timeless (m !! i).
Global Instance map_lookup_timeless m i : Timeless m Timeless (m !! i).
Proof.
intros ? [x|] Hx; [|by symmetry; apply (timeless _)].
assert (m ={1}= <[i:=x]> m)
by (by symmetry in Hx; inversion Hx; cofe_subst; rewrite insert_id).
by rewrite (timeless m (<[i:=x]>m)) // lookup_insert.
Qed.
Global Instance map_insert_timeless (m : gmap K A) i x :
Global Instance map_insert_timeless m i x :
Timeless x Timeless m Timeless (<[i:=x]>m).
Proof.
intros ?? m' Hm j; destruct (decide (i = j)); simplify_map_equality.
{ by apply (timeless _); rewrite -Hm lookup_insert. }
by apply (timeless _); rewrite -Hm lookup_insert_ne.
Qed.
Global Instance map_singleton_timeless (i : K) (x : A) :
Global Instance map_singleton_timeless i x :
Timeless x Timeless ({[ i x ]} : gmap K A) := _.
End cofe.
Arguments mapC _ {_ _} _.
(* CMRA *)
......@@ -84,12 +85,14 @@ Instance map_op : Op (gmap K A) := merge op.
Instance map_unit : Unit (gmap K A) := fmap unit.
Instance map_validN : ValidN (gmap K A) := λ n m, i, {n} (m!!i).
Instance map_minus : Minus (gmap K A) := merge minus.
Lemma lookup_op m1 m2 i : (m1 m2) !! i = m1 !! i m2 !! i.
Proof. by apply lookup_merge. Qed.
Lemma lookup_minus m1 m2 i : (m1 m2) !! i = m1 !! i m2 !! i.
Proof. by apply lookup_merge. Qed.
Lemma lookup_unit m i : unit m !! i = unit (m !! i).
Proof. by apply lookup_fmap. Qed.
Lemma map_included_spec (m1 m2 : gmap K A) : m1 m2 i, m1 !! i m2 !! i.
Proof.
split.
......@@ -105,6 +108,7 @@ Proof.
* intros Hm; exists (m2 m1); intros i.
by rewrite lookup_op lookup_minus cmra_op_minus.
Qed.
Definition map_cmra_mixin : CMRAMixin (gmap K A).
Proof.
split.
......@@ -152,35 +156,32 @@ Proof.
* by intros m i; rewrite /= lookup_op lookup_empty (left_id_L None _).
* apply map_empty_timeless.
Qed.
End cmra.
Arguments mapRA _ {_ _} _.
Section properties.
Context `{Countable K} {A: cmraT}.
Context `{Countable K} {A : cmraT}.
Implicit Types m : gmap K A.
Implicit Types i : K.
Implicit Types a : A.
Lemma map_lookup_validN n m i x : {n} m m !! i ={n}= Some x {n} x.
Proof. by move=> /(_ i) Hm Hi; move:Hm; rewrite Hi. Qed.
Lemma map_insert_validN n m i x : {n} x {n} m {n} (<[i:=x]>m).
Proof. by intros ?? j; destruct (decide (i = j)); simplify_map_equality. Qed.
Lemma map_singleton_validN n i x : {n} ({[ i x ]} : gmap K A) {n} x.
Proof.
split; [|by intros; apply map_insert_validN, cmra_empty_valid].
by move=>/(_ i); simplify_map_equality.
Qed.
Lemma map_insert_op m1 m2 i x :
m2 !! i = None <[i:=x]>(m1 m2) = <[i:=x]>m1 m2.
Proof. by intros Hi; apply (insert_merge_l _ m1 m2); rewrite Hi. Qed.
Lemma map_validN_singleton n (i : K) (x : A) :
{n} x <-> {n} ({[ i x ]} : gmap K A).
Proof.
split.
- move=>Hx j. destruct (decide (i = j)); simplify_map_equality; done.
- move=>Hm. move: (Hm i). by simplify_map_equality.
Qed.
Lemma map_unit_singleton (i : K) (x : A) :
unit ({[ i x ]} : gmap K A) = {[ i unit x ]}.
Proof. apply map_fmap_singleton. Qed.
Lemma map_op_singleton (i : K) (x y : A) :
{[ i x ]} {[ i y ]} = ({[ i x y ]} : gmap K A).
Proof. by apply (merge_singleton _ _ _ x y). Qed.
......@@ -220,7 +221,7 @@ Lemma map_insert_updateP' (P : A → Prop) m i x :
Proof. eauto using map_insert_updateP. Qed.
Lemma map_insert_update m i x y : x ~~> y <[i:=x]>m ~~> <[i:=y]>m.
Proof.
rewrite !cmra_update_updateP; eauto using map_insert_updateP with congruence.
rewrite !cmra_update_updateP; eauto using map_insert_updateP with subst.
Qed.
Lemma map_singleton_updateP (P : A Prop) (Q : gmap K A Prop) i x :
......@@ -228,13 +229,9 @@ Lemma map_singleton_updateP (P : A → Prop) (Q : gmap K A → Prop) i x :
Proof. apply map_insert_updateP. Qed.
Lemma map_singleton_updateP' (P : A Prop) i x :
x ~~>: P {[ i x ]} ~~>: λ m', y, m' = {[ i y ]} P y.
Proof. eauto using map_singleton_updateP. Qed.
Proof. apply map_insert_updateP'. Qed.
Lemma map_singleton_update i (x y : A) : x ~~> y {[ i x ]} ~~> {[ i y ]}.
Proof.
rewrite !cmra_update_updateP=>?. eapply map_singleton_updateP; first eassumption.
by move=>? ->.
Qed.
Proof. apply map_insert_update. Qed.
Context `{Fresh K (gset K), !FreshSpec K (gset K)}.
Lemma map_updateP_alloc (Q : gmap K A Prop) m x :
......
This diff is collapsed.
......@@ -29,7 +29,7 @@ Module notations.
(* What about Arguments for hoare triples?. *)
(* The colons indicate binders. "let" is not consistent here though,
thing are only bound in the "in". *)
Notation "# n" := (Var n) (at level 1, format "# n") : lang_scope.
Notation "# n" := (ids (term:=expr) n) (at level 1, format "# n") : lang_scope.
Notation "! e" := (Load e%L) (at level 10, format "! e") : lang_scope.
Notation "'ref' e" := (Alloc e%L) (at level 30) : lang_scope.
Notation "e1 + e2" := (BinOp PlusOp e1%L e2%L)
......@@ -41,10 +41,12 @@ Module notations.
Notation "e1 = e2" := (BinOp EqOp e1%L e2%L) (at level 70) : lang_scope.
(* The unicode ← is already part of the notation "_ ← _; _" for bind. *)
Notation "e1 <- e2" := (Store e1%L e2%L) (at level 80) : lang_scope.
Notation "e1 ; e2" := (Seq e1%L e2%L) (at level 100) : lang_scope.
Notation "'let:' e1 'in' e2" := (Let e1%L e2%L) (at level 102) : lang_scope.
Notation "'λ:' e" := (Lam e%L) (at level 102) : lang_scope.
Notation "'rec::' e" := (Rec e%L) (at level 102) : lang_scope.
Notation "e1 ; e2" := (Seq e1%L e2%L)
(at level 100, e2 at level 200) : lang_scope.
Notation "'let:' e1 'in' e2" := (Let e1%L e2%L)
(at level 102, e2 at level 200) : lang_scope.
Notation "'λ:' e" := (Lam e%L) (at level 102, e at level 200) : lang_scope.
Notation "'rec::' e" := (Rec e%L) (at level 102, e at level 200) : lang_scope.
Notation "'if' e1 'then' e2 'else' e3" := (If e1%L e2%L e3%L)
(at level 200, e1, e2, e3 at level 200) : lang_scope.
End notations.
......
......@@ -53,16 +53,15 @@ Module LiftingTests.
(* TODO: once asimpl preserves notation, we don't need
FindPred' anymore. *)
(* FIXME: fix notation so that we do not need parenthesis or %L *)
Definition FindPred' n1 Sn1 n2 f : expr :=
Definition FindPred' (n1 Sn1 n2 f : expr) : expr :=
if Sn1 < n2 then f Sn1 else n1.
Definition FindPred n2 : expr :=
Definition FindPred (n2 : expr) : expr :=
rec:: (let: #1 + Lit 1 in FindPred' #2 #0 n2.[ren(+3)] #1)%L.
Definition Pred : expr :=
λ: (if #0 Lit 0 then Lit 0 else FindPred #0 (Lit 0))%L.
Lemma FindPred_spec n1 n2 E Q :
((n1 < n2) Q $ LitV (pred n2))
wp E (FindPred (Lit n2) (Lit n1)) Q.
( (n1 < n2) Q (LitV $ pred n2)) wp E (FindPred (Lit n2) (Lit n1)) Q.
Proof.
revert n1. apply löb_all_1=>n1.
rewrite -wp_rec //. asimpl.
......@@ -70,8 +69,12 @@ Module LiftingTests.
etransitivity; first (etransitivity; last eapply equiv_spec, later_and).
{ apply and_mono; first done. by rewrite -later_intro. }
apply later_mono.
(* Go on. *)
rewrite -(wp_let _ _ (FindPred' (Lit n1) #0 (Lit n2) (FindPred (Lit n2)))).
(* Go on *)
(* FIXME "rewrite -(wp_let _ _ (FindPred' n1 #0 n2 (FindPred n2)))" started to
fail after we changed # n to use ids instead of Var *)
pose proof (wp_let (Σ:=Σ) E (Lit n1 + Lit 1)%L
(FindPred' (Lit n1) #0 (Lit n2) (FindPred (Lit n2))) Q).
unfold Let, Lam in H; rewrite -H.
rewrite -wp_bin_op //. asimpl.
rewrite -(wp_bindi (IfCtx _ _)).
rewrite -!later_intro /=.
......
......@@ -26,10 +26,12 @@ Hint Extern 998 (_ = _) => f_equal : f_equal.
Hint Extern 999 => congruence : congruence.
Hint Extern 1000 => lia : lia.
Hint Extern 1000 => omega : omega.
Hint Extern 1001 => progress subst : subst. (** backtracking on this one will
be very bad, so use with care! *)
(** The tactic [intuition] expands to [intuition auto with *] by default. This
is rather efficient when having big hint databases, or expensive [Hint Extern]
declarations as the above. *)
declarations as the ones above. *)
Tactic Notation "intuition" := intuition auto.
(** A slightly modified version of Ssreflect's finishing tactic [done]. It
......
......@@ -6,144 +6,89 @@ Definition gid := positive.
Definition globalC (Σ : gid iFunctor) : iFunctor :=
iprodF (λ i, mapF gid (Σ i)).
Class InG Λ (Σ : gid iFunctor) (i : gid) (A : cmraT) :=
Class InG (Λ : language) (Σ : gid iFunctor) (i : gid) (A : cmraT) :=
inG : A = Σ i (laterC (iPreProp Λ (globalC Σ))).
Definition to_globalC {Λ Σ A}
(i : gid) `{!InG Λ Σ i A} (γ : gid) (a : A) : iGst Λ (globalC Σ) :=
iprod_singleton i {[ γ cmra_transport inG a ]}.
Definition own {Λ Σ A}
(i : gid) `{!InG Λ Σ i A} (γ : gid) (a : A) : iProp Λ (globalC Σ) :=
ownG (to_globalC i γ a).
Instance: Params (@to_globalC) 6.
Instance: Params (@own) 6.
Typeclasses Opaque to_globalC own.
Section global.
Context {Λ : language} {Σ : gid iFunctor} (i : gid) `{!InG Λ Σ i A}.
Implicit Types a : A.
Definition to_Σ (a : A) : Σ i (laterC (iPreProp Λ (globalC Σ))) :=
eq_rect A id a _ inG.
Definition to_globalC (γ : gid) `{!InG Λ Σ i A} (a : A) : iGst Λ (globalC Σ) :=
iprod_singleton i {[ γ to_Σ a ]}.
Definition own (γ : gid) (a : A) : iProp Λ (globalC Σ) :=
ownG (to_globalC γ a).
Definition from_Σ (b : Σ i (laterC (iPreProp Λ (globalC Σ)))) : A :=
eq_rect (Σ i _) id b _ (Logic.eq_sym inG).
Definition P_to_Σ (P : A Prop) (b : Σ i (laterC (iPreProp Λ (globalC Σ)))) : Prop
:= P (from_Σ b).
(* Properties of the transport. *)
Lemma to_from_Σ b :
to_Σ (from_Σ b) = b.
Proof.
rewrite /to_Σ /from_Σ. by destruct inG.
Qed.
(* Properties of to_globalC *)
Lemma globalC_op γ a1 a2 :
to_globalC γ (a1 a2) to_globalC γ a1 to_globalC γ a2.
Proof.
rewrite /to_globalC iprod_op_singleton map_op_singleton.
apply iprod_singleton_proper, (fin_maps.singleton_proper (M:=gmap _)).
by rewrite /to_Σ; destruct inG.
Qed.
Lemma globalC_validN n γ a :
{n} (to_globalC γ a) <-> {n} a.
Instance to_globalC_ne γ n : Proper (dist n ==> dist n) (to_globalC i γ).
Proof. by intros a a' Ha; apply iprod_singleton_ne; rewrite Ha. Qed.
Lemma to_globalC_validN n γ a : {n} (to_globalC i γ a) {n} a.
Proof.
rewrite /to_globalC.
rewrite -iprod_validN_singleton -map_validN_singleton.
by rewrite /to_Σ; destruct inG.
by rewrite /to_globalC
iprod_singleton_validN map_singleton_validN cmra_transport_validN.
Qed.
Lemma globalC_unit γ a :
unit (to_globalC γ a) to_globalC γ (unit a).
Lemma to_globalC_op γ a1 a2 :
to_globalC i γ (a1 a2) to_globalC i γ a1 to_globalC i γ a2.
Proof.
rewrite /to_globalC.
rewrite iprod_unit_singleton map_unit_singleton.
apply iprod_singleton_proper, (fin_maps.singleton_proper (M:=gmap _)).
by rewrite /to_Σ; destruct inG.
by rewrite /to_globalC iprod_op_singleton map_op_singleton cmra_transport_op.
Qed.
Global Instance globalC_timeless γ m : Timeless m Timeless (to_globalC γ m).
Lemma to_globalC_unit γ a : unit (to_globalC i γ a) to_globalC i γ (unit a).
Proof.
rewrite /to_globalC => ?.
apply iprod_singleton_timeless, map_singleton_timeless.
by rewrite /to_Σ; destruct inG.
by rewrite /to_globalC
iprod_unit_singleton map_unit_singleton cmra_transport_unit.
Qed.
(* Properties of the lifted frame-preserving updates *)
Lemma update_to_Σ a P :
a ~~>: P to_Σ a ~~>: P_to_Σ P.
Proof.
move=>Hu gf n Hf. destruct (Hu (from_Σ gf) n) as [a' Ha'].
{ move: Hf. rewrite /to_Σ /from_Σ. by destruct inG. }
exists (to_Σ a'). move:Hf Ha'.
rewrite /P_to_Σ /to_Σ /from_Σ. destruct inG. done.
Qed.
Instance to_globalC_timeless γ m : Timeless m Timeless (to_globalC i γ m).
Proof. rewrite /to_globalC; apply _. Qed.
(* Properties of own *)
Global Instance own_ne γ n : Proper (dist n ==> dist n) (own γ).
Global Instance own_ne γ n : Proper (dist n ==> dist n) (own i γ).
Proof. by intros m m' Hm; rewrite /own Hm. Qed.
Global Instance own_proper γ : Proper (() ==> ()) (own i γ) := ne_proper _.
Lemma own_op γ a1 a2 : own i γ (a1 a2) (own i γ a1 own i γ a2)%I.
Proof. by rewrite /own -ownG_op to_globalC_op. Qed.
Lemma always_own_unit γ a : ( own i γ (unit a))%I own i γ (unit a).
Proof. by rewrite /own -to_globalC_unit always_ownG_unit. Qed.
Lemma own_valid γ a : own i γ a a.
Proof.
intros m m' Hm; apply ownG_ne, iprod_singleton_ne, singleton_ne.
by rewrite /to_globalC /to_Σ; destruct inG.
rewrite /own ownG_valid; apply valid_mono=> ?; apply to_globalC_validN.
Qed.
Global Instance own_proper γ : Proper (() ==> ()) (own γ) := ne_proper _.
Lemma own_op γ a1 a2 : own γ (a1 a2) (own γ a1 own γ a2)%I.
Proof. rewrite /own -ownG_op. apply ownG_proper, globalC_op. Qed.
(* TODO: This also holds if we just have ✓a at the current step-idx, as Iris
assertion. However, the map_updateP_alloc does not suffice to show this. *)
Lemma own_alloc E a :
a True pvs E E ( γ, own γ a).
Proof.
intros Ha. set (P m := γ, m = to_globalC γ a).
rewrite -(pvs_mono _ _ ( m, P m ownG m)%I).
- rewrite -pvs_ownG_updateP_empty //; [].
subst P. eapply (iprod_singleton_updateP_empty i).
+ apply map_updateP_alloc' with (x:=to_Σ a).
by rewrite /to_Σ; destruct inG.
+ simpl. move=>? [γ [-> ?]]. exists γ. done.
- apply exist_elim=>m. apply const_elim_l=>-[p ->] {P}.
by rewrite -(exist_intro p).
Qed.
Lemma always_own_unit γ a : ( own γ (unit a))%I own γ (unit a).
Proof. rewrite /own -globalC_unit. by apply always_ownG_unit. Qed.
Lemma own_valid γ a : (own γ a) ( a).
Proof.
rewrite /own ownG_valid. apply uPred.valid_mono=>n.
by apply globalC_validN.
Qed.
Lemma own_valid_r' γ a : (own γ a) (own γ a a).
Lemma own_valid_r' γ a : own i γ a (own i γ a a).
Proof. apply (uPred.always_entails_r' _ _), own_valid. Qed.
Global Instance own_timeless γ a : Timeless a TimelessP (own i γ a).
Proof. unfold own; apply _. Qed.
Global Instance ownG_timeless γ a : Timeless a TimelessP (own γ a).
(* TODO: This also holds if we just have ✓ a at the current step-idx, as Iris
assertion. However, the map_updateP_alloc does not suffice to show this. *)
Lemma own_alloc E a : a True pvs E E ( γ, own i γ a).
Proof.
intros. apply ownG_timeless. apply _.
intros Ha.
rewrite -(pvs_mono _ _ ( m, ( γ, m = to_globalC i γ a) ownG m)%I).
* eapply pvs_ownG_updateP_empty, (iprod_singleton_updateP_empty i);
first (eapply map_updateP_alloc', cmra_transport_valid, Ha); naive_solver.
* apply exist_elim=>m; apply const_elim_l=>-[γ ->].
by rewrite -(exist_intro γ).
Qed.
Lemma pvs_updateP E γ a P :
a ~~>: P own γ a pvs E E ( a', P a' own γ a').
a ~~>: P own i γ a pvs E E ( a', P a' own i γ a').
Proof.
intros Ha. set (P' m := a', P a' m = to_globalC γ a').
rewrite -(pvs_mono _ _ ( m, P' m ownG m)%I).
- rewrite -pvs_ownG_updateP; first by rewrite /own.
rewrite /to_globalC. eapply iprod_singleton_updateP.
+ (* FIXME RJ: I tried apply... with instead of instantiate, that
does not work. *)
apply map_singleton_updateP'. instantiate (1:=P_to_Σ P).
by apply update_to_Σ.
+ simpl. move=>? [y [-> HP]]. exists (from_Σ y). split.
* move: HP. rewrite /P_to_Σ /from_Σ. by destruct inG.
* clear HP. rewrite /to_globalC to_from_Σ; done.
- apply exist_elim=>m. apply const_elim_l=>-[a' [HP ->]].
rewrite -(exist_intro a'). apply and_intro; last done.
by apply const_intro.
intros Ha.
rewrite -(pvs_mono _ _ ( m, ( b, m = to_globalC i γ b P b) ownG m)%I).
* eapply pvs_ownG_updateP, iprod_singleton_updateP;
first (eapply map_singleton_updateP', cmra_transport_updateP', Ha).
naive_solver.
* apply exist_elim=>m; apply const_elim_l=>-[a' [-> HP]].
rewrite -(exist_intro a'). by apply and_intro; [apply const_intro|].
Qed.
Lemma pvs_update E γ a a' : a ~~> a' own γ a pvs E E (own γ a').
Lemma pvs_update E γ a a' : a ~~> a' own i γ a pvs E E (own i γ a').
Proof.
intros; rewrite (pvs_updateP E _ _ (a' =)); last by apply cmra_update_updateP.
by apply pvs_mono, uPred.exist_elim=> m''; apply uPred.const_elim_l=> ->.
Qed.
End global.
......@@ -208,7 +208,7 @@ Arguments uPred_holds {_} _%I _ _.
Arguments uPred_entails _ _%I _%I.
Notation "P ⊑ Q" := (uPred_entails P%I Q%I) (at level 70) : C_scope.
Notation "(⊑)" := uPred_entails (only parsing) : C_scope.
Notation "■ φ" := (uPred_const φ) (at level 20) : uPred_scope.
Notation "■ φ" := (uPred_const φ%type) (at level 20) : uPred_scope.
Notation "'False'" := (uPred_const False) : uPred_scope.
Notation "'True'" := (uPred_const True) : uPred_scope.
Infix "∧" := uPred_and : uPred_scope.
......
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