Commit cae9dd85 authored by Ralf Jung's avatar Ralf Jung

add sugar for defining SPreds, this also makes them print nicer in some cases

parent f6d457c4
......@@ -376,7 +376,7 @@ Module Type IRIS_CORE (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
(* Local Obligation Tactic := intros; resp_set || eauto with typeclass_instances. *)
Program Definition box : Props -> Props :=
fun P => m[(fun w => mkSPred (fun n => P (1 w) n) _ _)].
fun P => m[(fun w => p[(fun n => P (1 w) n)] )].
Next Obligation.
exact: bpred.
Qed.
......@@ -582,7 +582,7 @@ Module Type IRIS_CORE (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
forall w' k (HLt : (S k) < n) (Hp : P w' (S k)), P w' (S (S k)).
Program Definition timeless P : Props :=
m[(fun w => mkSPred (fun n => timelessP P w n) _ _)].
m[(fun w => p[(fun n => timelessP P w n)] )].
Next Obligation.
move=>? ? ? ?. exfalso. omega.
Qed.
......@@ -696,8 +696,8 @@ Module Type IRIS_CORE (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
Local Obligation Tactic := idtac.
(** General Ownership - used to show that the other assertions make sense **)
Program Definition own: Wld -n> Props :=
n[(fun w0 => m[(fun w => wr, (w0 · wr) === w )] )].
Program Definition own: Wld -> Props :=
fun w0 => m[(fun w => wr, (w0 · wr) === w )].
Next Obligation.
intros. move=>wr0 wr1 EQwr. apply intEq_dist; last reflexivity.
apply cmra_op_dist; first reflexivity. assumption.
......@@ -718,12 +718,39 @@ Module Type IRIS_CORE (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
apply sp_eq_iff. rewrite -Hequ. rewrite assoc (comm w) -assoc.
apply cmra_op_dist; first reflexivity. assumption.
Qed.
Next Obligation.
move=>n w0 w1 Heq w m HLt. destruct m; first reflexivity.
Arguments own _ : simpl never.
Global Instance own_dist n:
Proper (dist n ==> dist n) own.
Proof.
move=>w0 w1 Heq w m HLt. destruct m; first reflexivity.
split; case=>wd; move/sp_eq_iff=>Heqd; exists wd; apply sp_eq_iff; rewrite -Heqd;
(apply cmra_op_dist; last reflexivity); eapply mono_dist; first eassumption; eassumption || symmetry; eassumption.
Qed.
Global Instance own_equiv : Proper (equiv ==> equiv) own.
Proof.
eapply dist_equiv; now apply _.
Qed.
Lemma own_sc (u v : Wld):
own (u · v) == own u * own v.
Proof.
move => w n; destruct n; first (split; intro; exact:bpred). split; simpl.
- move => [wr Hwr].
exists (u, v · wr); split; last split.
+ split; now rewrite -Hwr -assoc.
+ exists (1u). now rewrite ra_op_unit2.
+ exists wr; reflexivity.
- move : w => [wu wr] [[w1 w2] [Hw] [[w1r Hw1r] [w2r Hw2r]]].
exists (w1r · w2r). rewrite -assoc (assoc v) (comm v) -assoc. rewrite -Hw. split.
(* RJ: Simplification here is not nice... *)
+ rewrite [ra_op]lock /= -lock. simpl in Hw1r, Hw2r. rewrite -Hw1r -Hw2r.
rewrite !assoc. reflexivity.
+ rewrite [ra_op]lock /=. simpl in Hw1r, Hw2r. rewrite -Hw1r -Hw2r.
rewrite !assoc. split; reflexivity.
Qed.
Program Definition inv i : Props -n> Props :=
n[(fun P => m[(fun w => Pr, Invs w i === Some (Pr · (ra_ag_inj (ı' (halved P)))) )] )].
Next Obligation.
......@@ -769,7 +796,7 @@ Module Type IRIS_CORE (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
Program Definition inv_own i P: Props :=
r, own (fdStrongUpdate i (Some (ra_ag_inj (ı' (halved P)))) fdEmpty, r).
Next Obligation.
intros. move=>r1 r2 EQr. apply (met_morph_nonexp own). split; first reflexivity.
intros. move=>r1 r2 EQr. apply (own_dist). split; first reflexivity.
exact EQr.
Qed.
......@@ -825,14 +852,13 @@ Module Type IRIS_CORE (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
Program Definition own_state σ: Props :=
I, g, own (I, (ex_own σ, g)).
Next Obligation.
intros. move=>g1 g2 EQg. cbv beta. apply met_morph_nonexp.
intros. move=>g1 g2 EQg. cbv beta. apply own_dist.
split; first reflexivity. split; first reflexivity.
simpl. assumption.
Qed.
Next Obligation.
intros. move=>I1 I2 EQI. cbv beta. apply xist_dist=>r.
rewrite {1 3}/met_morph /mkNMorph {1 4}/morph.
apply met_morph_nonexp.
apply own_dist.
split; last reflexivity. simpl. assumption.
Qed.
......@@ -877,14 +903,13 @@ Module Type IRIS_CORE (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
Program Definition own_ghost g: Props :=
I, S, own (I, (S, g)).
Next Obligation.
intros. move=>g1 g2 EQr. cbv beta. apply met_morph_nonexp.
intros. move=>g1 g2 EQr. apply own_dist.
split; first reflexivity. split; last reflexivity.
simpl. assumption.
Qed.
Next Obligation.
intros. move=>I1 I2 EQI. cbv beta. apply xist_dist=>S.
rewrite {1 3}/met_morph /mkNMorph {1 4}/morph.
apply met_morph_nonexp.
apply own_dist.
split; last reflexivity. simpl. assumption.
Qed.
......@@ -915,6 +940,13 @@ Module Type IRIS_CORE (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
rewrite ->Hg1, Hg2. apply pordR. exact Heq.
Qed.
Lemma ownL_something:
valid(xist ownL).
Proof.
move=>w n. destruct n; first exact:bpred. exists (Res w).
simpl. reflexivity.
Qed.
End Ownership.
End IRIS_CORE.
......
......@@ -48,7 +48,7 @@ Section Agreement.
Global Instance ra_agree_valid : RA_valid _ := compose valid_sp ra_ag_v.
Global Program Instance ra_ag_op : RA_op _ :=
fun x y => ag_inj (mkSPred (fun n => ra_ag_v x n /\ ra_ag_v y n /\ ra_ag_ts x n = n = ra_ag_ts y n) _ _) (ra_ag_ts x) _.
fun x y => ag_inj p[(fun n => ra_ag_v x n /\ ra_ag_v y n /\ ra_ag_ts x n = n = ra_ag_ts y n)] (ra_ag_ts x) _.
Next Obligation.
split; last split; exact:dist_bound||exact:bpred.
Qed.
......@@ -384,7 +384,7 @@ Section Agreement.
(* We need to provide a CMRAExt. *)
Program Definition ra_ag_cmra_extend_elem (me they part rem: ra_agree) n (Hdist: me = n = they) (Heq: they == rem · part) :=
ag_inj (mkSPred (fun m => ra_ag_v me m \/ (m <= n /\ ra_ag_v part m)) _ _)
ag_inj p[(fun m => ra_ag_v me m \/ (m <= n /\ ra_ag_v part m))]
(fun m => if le_lt_dec m n then ra_ag_ts part m else ra_ag_ts me m) _.
Next Obligation.
left. exact:bpred.
......
......@@ -26,6 +26,7 @@ Qed.
Notation "'mkType' R" := (@Build_Setoid _ R _) (at level 10).
Arguments equiv {_ _} !_ !_ /.
Arguments const {_ _} _ _ /.
Class Associative {T} `{eqT : Setoid T} (op : T -> T -> T) :=
assoc : forall t1 t2 t3, op t1 (op t2 t3) == op (op t1 t2) t3.
......
......@@ -976,7 +976,7 @@ Section CMRA.
| None => True end.
Global Program Instance finmap_cmra_valid: CMRA_valid (I -f> T) :=
fun f => mkSPred (finmap_cmra_valid_op f) _ _.
fun f => p[(finmap_cmra_valid_op f)].
Next Obligation.
move=>i. destruct (f i); last tauto.
exact: bpred.
......
......@@ -10,12 +10,18 @@ Section Definitions.
bpred : spred 0;
dpred : dclosed spred }.
End Definitions.
Arguments dpred {s} {n m} _ _.
Arguments mkSPred _ _ _.
Notation "'p[(' f ')]'" := (mkSPred f _ _).
Section Props.
Definition sp_constF (P: Prop) :=
fun n => match n with
| O => True
| S _ => P end.
Program Definition sp_const P :=
mkSPred (sp_constF P) _ _.
p[(sp_constF P)].
Next Obligation.
move=>n m Hle. destruct m, n; simpl; tauto || inversion Hle.
Qed.
......@@ -63,7 +69,7 @@ Section Definitions.
Proof. by apply EQP. Qed.
Program Definition sp_compl (σ : chain SPred) (σc : cchain σ) :=
mkSPred (fun n => σ n n) _ _.
p[(fun n => σ n n)].
Next Obligation.
apply bpred.
Qed.
......@@ -115,7 +121,7 @@ Section Definitions.
| S n => p n
end.
Program Definition later_sp (p : SPred) :=
mkSPred (laterF p) _ _.
p[(laterF p)].
Next Obligation.
intros [| m] [| n] HLe; simpl; try tauto; [now inversion HLe |].
intros HP; eapply dpred; [| eassumption]; auto with arith.
......@@ -168,16 +174,14 @@ Section Definitions.
eapply HP; eassumption || symmetry; eassumption.
Qed.
End Definitions.
Arguments dpred {s} {n m} _ _.
End Props.
Section SPredBI.
Local Obligation Tactic := intros; eauto with typeclass_instances.
(* Standard interpretations of propositional connectives. *)
Global Program Instance top_sp : topBI SPred :=
mkSPred (fun _ => True) _ _. (* this behaves nicer than sp_c *)
p[(fun _ => True)]. (* this behaves nicer than sp_c *)
Next Obligation.
repeat intro. exact I.
Qed.
......@@ -189,7 +193,7 @@ Section SPredBI.
Global Program Instance and_sp : andBI SPred :=
fun P Q =>
mkSPred (fun n => P n /\ Q n) _ _.
p[(fun n => P n /\ Q n)].
Next Obligation.
split; now apply bpred.
Qed.
......@@ -198,7 +202,7 @@ Section SPredBI.
Qed.
Global Program Instance or_sp : orBI SPred :=
fun P Q =>
mkSPred (fun n => P n \/ Q n) _ _.
p[(fun n => P n \/ Q n)].
Next Obligation.
left. now apply bpred.
Qed.
......@@ -278,7 +282,7 @@ Section SPredBI.
Global Program Instance impl_sp : implBI SPred :=
fun P Q =>
mkSPred (fun n => forall m, m <= n -> P m -> Q m) _ _.
p[(fun n => forall m, m <= n -> P m -> Q m)].
Next Obligation.
destruct m; last omega.
apply bpred.
......@@ -310,7 +314,7 @@ Section SPredBI.
(* Quantifiers. *)
Global Program Instance all_sp : allBI SPred :=
fun T eqT mT cmT R =>
mkSPred (fun n => forall t, R t n) _ _.
p[(fun n => forall t, R t n)].
Next Obligation.
apply bpred.
Qed.
......@@ -325,7 +329,7 @@ Section SPredBI.
end.
Global Program Instance xist_sp : xistBI SPred :=
fun T eqT mT cmT R =>
mkSPred (xist_spF R) _ _.
p[(xist_spF R)].
Next Obligation.
exact I.
Qed.
......@@ -387,7 +391,7 @@ End SPredBI.
Section SPredEq.
Global Program Instance sp_eq : eqBI SPred :=
fun U {eqU mU cmU u1 u2} => mkSPred (fun n => u1 = n = u2) _ _.
fun U {eqU mU cmU u1 u2} => p[(fun n => u1 = n = u2)].
Next Obligation.
exact:dist_bound.
Qed.
......
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