Commit 817c0816 authored by Robbert Krebbers's avatar Robbert Krebbers

Separate parameters for language and global functor.

This way we can more easily state lemmas for concrete languages for
arbitrary global functors.
parent 2184e92e
......@@ -57,14 +57,13 @@ iris/viewshifts.v
iris/wsat.v
iris/ownership.v
iris/weakestpre.v
iris/language.v
iris/pviewshifts.v
iris/resources.v
iris/hoare.v
iris/parameter.v
iris/language.v
iris/functor.v
iris/tests.v
barrier/heap_lang.v
barrier/parameter.v
barrier/lifting.v
barrier/sugar.v
barrier/tests.v
......@@ -390,8 +390,10 @@ Section Language.
Definition ectx_step e1 σ1 e2 σ2 (ef: option expr) :=
K e1' e2', e1 = fill K e1' e2 = fill K e2'
prim_step e1' σ1 e2' σ2 ef.
Global Program Instance heap_lang : Language expr value state := {|
Program Canonical Structure heap_lang : language := {|
language.expr := expr;
language.val := value;
language.state := state;
of_val := v2e;
to_val := e2v;
language.atomic := atomic;
......
Require Import prelude.gmap iris.lifting.
Require Export iris.weakestpre barrier.parameter.
Require Export iris.weakestpre barrier.heap_lang.
Import uPred.
Section lifting.
Implicit Types P : iProp Σ.
Implicit Types Q : ival Σ iProp Σ.
Context {Σ : iFunctor}.
Implicit Types P : iProp heap_lang Σ.
Implicit Types Q : val heap_lang iProp heap_lang Σ.
(** Bind. *)
Lemma wp_bind {E e} K Q :
......@@ -162,7 +163,8 @@ Qed.
(** Base axioms for core primitives of the language: Stateless reductions *)
Lemma wp_fork E e :
wp coPset_all e (λ _, True) wp E (Fork e) (λ v, (v = LitUnitV)).
wp coPset_all e (λ _, True : iProp heap_lang Σ)
wp E (Fork e) (λ v, (v = LitUnitV)).
Proof.
etransitivity; last eapply wp_lift_pure_step with
(φ := λ e' ef, e' = LitUnit ef = Some e);
......@@ -178,7 +180,7 @@ Proof.
apply forall_intro=>e2. apply forall_intro=>ef.
apply impl_intro_l. apply const_elim_l. intros [-> ->].
(* FIXME RJ This is ridicolous. *)
transitivity (True wp coPset_all e (λ _ : ival Σ, True))%I;
transitivity (True wp coPset_all e (λ _, True : iProp heap_lang Σ))%I;
first by rewrite left_id.
apply sep_mono; last reflexivity.
rewrite -wp_value'; last reflexivity.
......
Require Export barrier.heap_lang.
Require Import iris.parameter.
Canonical Structure Σ := iParam_const heap_lang unitRA.
......@@ -17,8 +17,9 @@ Definition LetCtx (K1 : ectx) (e2 : {bind expr}) := AppRCtx (LamV e2) K1.
Definition SeqCtx (K1 : ectx) (e2 : expr) := LetCtx K1 (e2.[ren(+1)]).
Section suger.
Implicit Types P : iProp Σ.
Implicit Types Q : ival Σ iProp Σ.
Context {Σ : iFunctor}.
Implicit Types P : iProp heap_lang Σ.
Implicit Types Q : val heap_lang iProp heap_lang Σ.
(** Proof rules for the sugar *)
Lemma wp_lam E ef e v Q :
......
......@@ -25,19 +25,16 @@ Module LangTests.
Qed.
End LangTests.
Module ParamTests.
Print Assumptions Σ.
End ParamTests.
Module LiftingTests.
Implicit Types P : iProp Σ.
Implicit Types Q : ival Σ iProp Σ.
Context {Σ : iFunctor}.
Implicit Types P : iProp heap_lang Σ.
Implicit Types Q : val heap_lang iProp heap_lang Σ.
(* TODO RJ: Some syntactic sugar for language expressions would be nice. *)
Definition e3 := Load (Var 0).
Definition e2 := Seq (Store (Var 0) (Plus (Load $ Var 0) (LitNat 1))) e3.
Definition e := Let (Alloc (LitNat 1)) e2.
Goal σ E, (ownP σ) (wp E e (λ v, (v = LitNatV 2))).
Goal σ E, (ownP σ : iProp heap_lang Σ) (wp E e (λ v, (v = LitNatV 2))).
Proof.
move=> σ E. rewrite /e.
rewrite -wp_let. rewrite -wp_alloc_pst; last done.
......@@ -121,7 +118,9 @@ Module LiftingTests.
+ done.
Qed.
Goal E, True wp E (Let (App Pred (LitNat 42)) (App Pred (Var 0))) (λ v, (v = LitNatV 40)).
Goal E,
(True : iProp heap_lang Σ)
wp E (Let (App Pred (LitNat 42)) (App Pred (Var 0))) (λ v, (v = LitNatV 40)).
Proof.
intros E. rewrite -wp_let. rewrite -Pred_spec -!later_intro.
asimpl. (* TODO RJ: Can we somehow make it so that Pred gets folded again? *)
......
......@@ -7,9 +7,10 @@ Local Hint Extern 10 (✓{_} _) =>
solve_validN.
Section adequacy.
Context {Σ : iParam}.
Implicit Types e : iexpr Σ.
Implicit Types Q : ival Σ iProp Σ.
Context {Λ : language} {Σ : iFunctor}.
Implicit Types e : expr Λ.
Implicit Types Q : val Λ iProp Λ Σ.
Implicit Types m : iGst Λ Σ.
Transparent uPred_holds.
Notation wptp n := (Forall3 (λ e Q r, uPred_holds (wp coPset_all e Q) n r)).
......
Require Export modures.cmra.
Structure iFunctor := IFunctor {
ifunctor_car :> cofeT cmraT;
ifunctor_empty A : Empty (ifunctor_car A);
ifunctor_identity A : CMRAIdentity (ifunctor_car A);
ifunctor_map {A B} (f : A -n> B) : ifunctor_car A -n> ifunctor_car B;
ifunctor_map_ne {A B} n : Proper (dist n ==> dist n) (@ifunctor_map A B);
ifunctor_map_id {A : cofeT} (x : ifunctor_car A) : ifunctor_map cid x x;
ifunctor_map_compose {A B C} (f : A -n> B) (g : B -n> C) x :
ifunctor_map (g f) x ifunctor_map g (ifunctor_map f x);
ifunctor_map_mono {A B} (f : A -n> B) : CMRAMonotone (ifunctor_map f)
}.
Existing Instances ifunctor_empty ifunctor_identity.
Existing Instances ifunctor_map_ne ifunctor_map_mono.
Lemma ifunctor_map_ext (Σ : iFunctor) {A B} (f g : A -n> B) m :
( x, f x g x) ifunctor_map Σ f m ifunctor_map Σ g m.
Proof.
by intros; apply equiv_dist=> n; apply ifunctor_map_ne=> ?; apply equiv_dist.
Qed.
Program Definition iFunctor_const (icmra : cmraT) {icmra_empty : Empty icmra}
{icmra_identity : CMRAIdentity icmra} : iFunctor :=
{| ifunctor_car A := icmra; ifunctor_map A B f := cid |}.
Solve Obligations with done.
\ No newline at end of file
Require Export iris.weakestpre iris.viewshifts.
Definition ht {Σ} (E : coPset) (P : iProp Σ)
(e : iexpr Σ) (Q : ival Σ iProp Σ) : iProp Σ :=
Definition ht {Λ Σ} (E : coPset) (P : iProp Λ Σ)
(e : expr Λ) (Q : val Λ iProp Λ Σ) : iProp Λ Σ :=
( (P wp E e (λ v, pvs E E (Q v))))%I.
Instance: Params (@ht) 2.
Instance: Params (@ht) 3.
Notation "{{ P } } e @ E {{ Q } }" := (ht E P e Q)
(at level 74, format "{{ P } } e @ E {{ Q } }") : uPred_scope.
......@@ -11,27 +11,27 @@ Notation "{{ P } } e @ E {{ Q } }" := (True ⊑ ht E P e Q)
(at level 74, format "{{ P } } e @ E {{ Q } }") : C_scope.
Section hoare.
Context {Σ : iParam}.
Implicit Types P : iProp Σ.
Implicit Types Q : ival Σ iProp Σ.
Implicit Types v : ival Σ.
Context {Λ : language} {Σ : iFunctor}.
Implicit Types P : iProp Λ Σ.
Implicit Types Q : val Λ iProp Λ Σ.
Implicit Types v : val Λ.
Import uPred.
Global Instance ht_ne E n :
Proper (dist n ==> eq ==> pointwise_relation _ (dist n) ==> dist n) (@ht Σ E).
Proper (dist n ==> eq==>pointwise_relation _ (dist n) ==> dist n) (@ht Λ Σ E).
Proof. by intros P P' HP e ? <- Q Q' HQ; rewrite /ht HP; setoid_rewrite HQ. Qed.
Global Instance ht_proper E :
Proper (() ==> eq ==> pointwise_relation _ () ==> ()) (@ht Σ E).
Proper (() ==> eq ==> pointwise_relation _ () ==> ()) (@ht Λ Σ E).
Proof. by intros P P' HP e ? <- Q Q' HQ; rewrite /ht HP; setoid_rewrite HQ. Qed.
Lemma ht_mono E P P' Q Q' e :
P P' ( v, Q' v Q v) {{ P' }} e @ E {{ Q' }} {{ P }} e @ E {{ Q }}.
Proof. by intros HP HQ; rewrite /ht -HP; setoid_rewrite HQ. Qed.
Global Instance ht_mono' E :
Proper (flip () ==> eq ==> pointwise_relation _ () ==> ()) (@ht Σ E).
Proper (flip () ==> eq ==> pointwise_relation _ () ==> ()) (@ht Λ Σ E).
Proof. by intros P P' HP e ? <- Q Q' HQ; apply ht_mono. Qed.
Lemma ht_val E v :
{{ True }} of_val v @ E {{ λ v', (v = v') }}.
{{ True : iProp Λ Σ }} of_val v @ E {{ λ v', (v = v') }}.
Proof.
apply (always_intro' _ _), impl_intro_l.
by rewrite -wp_value -pvs_intro; apply const_intro.
......
......@@ -8,12 +8,14 @@ Local Notation "{{ P } } ef ?@ E {{ Q } }" :=
(at level 74, format "{{ P } } ef ?@ E {{ Q } }") : C_scope.
Section lifting.
Context {Σ : iParam}.
Implicit Types e : iexpr Σ.
Context {Λ : language} {Σ : iFunctor}.
Implicit Types e : expr Λ.
Implicit Types P : iProp Λ Σ.
Implicit Types R : val Λ iProp Λ Σ.
Import uPred.
Lemma ht_lift_step E1 E2
(φ : iexpr Σ istate Σ option (iexpr Σ) Prop) P P' Q1 Q2 R e1 σ1 :
(φ : expr Λ state Λ option (expr Λ) Prop) P P' Q1 Q2 R e1 σ1 :
E1 E2 to_val e1 = None
reducible e1 σ1
( e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef φ e2 σ2 ef)
......@@ -42,8 +44,7 @@ Proof.
rewrite {1}/ht -always_wand_impl always_elim wand_elim_r; apply wp_mono=>v.
by apply const_intro.
Qed.
Lemma ht_lift_atomic E
(φ : iexpr Σ istate Σ option (iexpr Σ) Prop) P e1 σ1 :
Lemma ht_lift_atomic E (φ : expr Λ state Λ option (expr Λ) Prop) P e1 σ1 :
atomic e1
reducible e1 σ1
( e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef φ e2 σ2 ef)
......@@ -68,7 +69,7 @@ Proof.
rewrite -(exist_intro σ2) -(exist_intro ef) (of_to_val e2) //.
by rewrite -always_and_sep_r'; apply and_intro; try apply const_intro.
Qed.
Lemma ht_lift_pure_step E (φ : iexpr Σ option (iexpr Σ) Prop) P P' Q e1 :
Lemma ht_lift_pure_step E (φ : expr Λ option (expr Λ) Prop) P P' Q e1 :
to_val e1 = None
( σ1, reducible e1 σ1)
( σ1 e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef σ1 = σ2 φ e2 ef)
......@@ -94,7 +95,7 @@ Proof.
by apply const_intro.
Qed.
Lemma ht_lift_pure_determistic_step E
(φ : iexpr Σ option (iexpr Σ) Prop) P P' Q e1 e2 ef :
(φ : expr Λ option (expr Λ) Prop) P P' Q e1 e2 ef :
to_val e1 = None
( σ1, reducible e1 σ1)
( σ1 e2' σ2 ef', prim_step e1 σ1 e2' σ2 ef' σ1 = σ2 e2 = e2' ef = ef')
......
Require Export modures.base.
Require Export modures.cmra.
Class Language (E V St : Type) := {
of_val : V E;
to_val : E option V;
atomic : E Prop;
prim_step : E St E St option E Prop;
Structure language := Language {
expr : Type;
val : Type;
state : Type;
of_val : val expr;
to_val : expr option val;
atomic : expr Prop;
prim_step : expr state expr state option expr Prop;
to_of_val v : to_val (of_val v) = Some v;
of_to_val e v : to_val e = Some v of_val v = e;
values_stuck e σ e' σ' ef : prim_step e σ e' σ' ef to_val e = None;
......@@ -14,31 +17,43 @@ Class Language (E V St : Type) := {
prim_step e1 σ1 e2 σ2 ef
is_Some (to_val e2)
}.
Arguments of_val {_} _.
Arguments to_val {_} _.
Arguments atomic {_} _.
Arguments prim_step {_} _ _ _ _ _.
Arguments to_of_val {_} _.
Arguments of_to_val {_} _ _ _.
Arguments values_stuck {_} _ _ _ _ _ _.
Arguments atomic_not_value {_} _ _.
Arguments atomic_step {_} _ _ _ _ _ _ _.
Canonical Structure istateC Σ := leibnizC (state Σ).
Definition cfg (Λ : language) := (list (expr Λ) * state Λ)%type.
Section language.
Context `{Language E V St}.
Context {Λ : language}.
Implicit Types v : val Λ.
Definition reducible (e : E) (σ : St) :=
Definition reducible (e : expr Λ) (σ : state Λ) :=
e' σ' ef, prim_step e σ e' σ' ef.
Inductive step (ρ1 ρ2 : cfg Λ) : Prop :=
| step_atomic e1 σ1 e2 σ2 ef t1 t2 :
ρ1 = (t1 ++ e1 :: t2, σ1)
ρ2 = (t1 ++ e2 :: t2 ++ option_list ef, σ2)
prim_step e1 σ1 e2 σ2 ef
step ρ1 ρ2.
Lemma reducible_not_val e σ : reducible e σ to_val e = None.
Proof. intros (?&?&?&?); eauto using values_stuck. Qed.
Lemma atomic_of_val v : ¬atomic (of_val v).
Proof.
by intros Hat; apply atomic_not_value in Hat; rewrite to_of_val in Hat.
Qed.
Global Instance: Injective (=) (=) of_val.
Global Instance: Injective (=) (=) (@of_val Λ).
Proof. by intros v v' Hv; apply (injective Some); rewrite -!to_of_val Hv. Qed.
Definition cfg : Type := (list E * St)%type.
Inductive step (ρ1 ρ2 : cfg) : Prop :=
| step_atomic e1 σ1 e2 σ2 ef t1 t2 :
ρ1 = (t1 ++ e1 :: t2, σ1)
ρ2 = (t1 ++ e2 :: t2 ++ option_list ef, σ2)
prim_step e1 σ1 e2 σ2 ef
step ρ1 ρ2.
Record is_ctx (K : E E) := IsCtx {
Record is_ctx (K : expr Λ expr Λ) := IsCtx {
is_ctx_value e : to_val e = None to_val (K e) = None;
is_ctx_step_preserved e1 σ1 e2 σ2 ef :
prim_step e1 σ1 e2 σ2 ef prim_step (K e1) σ1 (K e2) σ2 ef;
......
......@@ -7,14 +7,15 @@ Local Hint Extern 10 (✓{_} _) =>
solve_validN.
Section lifting.
Context {Σ : iParam}.
Implicit Types v : ival Σ.
Implicit Types e : iexpr Σ.
Implicit Types σ : istate Σ.
Context {Λ : language} {Σ : iFunctor}.
Implicit Types v : val Λ.
Implicit Types e : expr Λ.
Implicit Types σ : state Λ.
Implicit Types Q : val Λ iProp Λ Σ.
Transparent uPred_holds.
Lemma wp_lift_step E1 E2
(φ : iexpr Σ istate Σ option (iexpr Σ) Prop) Q e1 σ1 :
(φ : expr Λ state Λ option (expr Λ) Prop) Q e1 σ1 :
E1 E2 to_val e1 = None
reducible e1 σ1
( e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef φ e2 σ2 ef)
......@@ -35,7 +36,7 @@ Proof.
{ rewrite (commutative _ r2) -(associative _); eauto using wsat_le. }
by exists r1', r2'; split_ands; [| |by intros ? ->].
Qed.
Lemma wp_lift_pure_step E (φ : iexpr Σ option (iexpr Σ) Prop) Q e1 :
Lemma wp_lift_pure_step E (φ : expr Λ option (expr Λ) Prop) Q e1 :
to_val e1 = None
( σ1, reducible e1 σ1)
( σ1 e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef σ1 = σ2 φ e2 ef)
......
......@@ -2,15 +2,17 @@ Require Export modures.logic iris.resources.
Require Import modures.cofe_solver.
Module iProp.
Definition F (Σ : iParam) (A B : cofeT) : cofeT := uPredC (resRA Σ (laterC A)).
Definition map {Σ : iParam} {A1 A2 B1 B2 : cofeT}
(f : (A2 -n> A1) * (B1 -n> B2)) : F Σ A1 B1 -n> F Σ A2 B2 :=
Definition F (Λ : language) (Σ : iFunctor) (A B : cofeT) : cofeT :=
uPredC (resRA Λ Σ (laterC A)).
Definition map {Λ : language} {Σ : iFunctor} {A1 A2 B1 B2 : cofeT}
(f : (A2 -n> A1) * (B1 -n> B2)) : F Λ Σ A1 B1 -n> F Λ Σ A2 B2 :=
uPredC_map (resRA_map (laterC_map (f.1))).
Definition result Σ : solution (F Σ).
Definition result Λ Σ : solution (F Λ Σ).
Proof.
apply (solver.result _ (@map Σ)).
* intros A B P. rewrite /map /= -{2}(uPred_map_id P). apply uPred_map_ext=>r {P} /=.
rewrite -{2}(res_map_id r). apply res_map_ext=>{r} r /=. by rewrite later_map_id.
apply (solver.result _ (@map Λ Σ)).
* intros A B P. rewrite /map /= -{2}(uPred_map_id P). apply uPred_map_ext=> r.
rewrite /= -{2}(res_map_id r); apply res_map_ext=>{r} r /=.
by rewrite later_map_id.
* intros A1 A2 A3 B1 B2 B3 f g f' g' P. rewrite /map /=.
rewrite -uPred_map_compose. apply uPred_map_ext=>{P} r /=.
rewrite -res_map_compose. apply res_map_ext=>{r} r /=.
......@@ -21,22 +23,24 @@ Qed.
End iProp.
(* Solution *)
Definition iPreProp (Σ : iParam) : cofeT := iProp.result Σ.
Notation iRes Σ := (res Σ (laterC (iPreProp Σ))).
Notation iResRA Σ := (resRA Σ (laterC (iPreProp Σ))).
Notation iWld Σ := (mapRA positive (agreeRA (laterC (iPreProp Σ)))).
Notation iPst Σ := (exclRA (istateC Σ)).
Notation iGst Σ := (icmra Σ (laterC (iPreProp Σ))).
Definition iProp (Σ : iParam) : cofeT := uPredC (iResRA Σ).
Definition iProp_unfold {Σ} : iProp Σ -n> iPreProp Σ := solution_fold _.
Definition iProp_fold {Σ} : iPreProp Σ -n> iProp Σ := solution_unfold _.
Lemma iProp_fold_unfold {Σ} (P : iProp Σ) : iProp_fold (iProp_unfold P) P.
Definition iPreProp (Λ : language) (Σ : iFunctor) : cofeT := iProp.result Λ Σ.
Notation iRes Λ Σ := (res Λ Σ (laterC (iPreProp Λ Σ))).
Notation iResRA Λ Σ := (resRA Λ Σ (laterC (iPreProp Λ Σ))).
Notation iWld Λ Σ := (mapRA positive (agreeRA (laterC (iPreProp Λ Σ)))).
Notation iPst Λ := (exclRA (istateC Λ)).
Notation iGst Λ Σ := (ifunctor_car Σ (laterC (iPreProp Λ Σ))).
Definition iProp (Λ : language) (Σ : iFunctor) : cofeT := uPredC (iResRA Λ Σ).
Definition iProp_unfold {Λ Σ} : iProp Λ Σ -n> iPreProp Λ Σ := solution_fold _.
Definition iProp_fold {Λ Σ} : iPreProp Λ Σ -n> iProp Λ Σ := solution_unfold _.
Lemma iProp_fold_unfold {Λ Σ} (P : iProp Λ Σ) : iProp_fold (iProp_unfold P) P.
Proof. apply solution_unfold_fold. Qed.
Lemma iProp_unfold_fold {Σ} (P : iPreProp Σ) : iProp_unfold (iProp_fold P) P.
Lemma iProp_unfold_fold {Λ Σ} (P : iPreProp Λ Σ) :
iProp_unfold (iProp_fold P) P.
Proof. apply solution_fold_unfold. Qed.
Bind Scope uPred_scope with iProp.
Instance iProp_fold_inj n Σ : Injective (dist n) (dist n) (@iProp_fold Σ).
Instance iProp_fold_inj n Λ Σ : Injective (dist n) (dist n) (@iProp_fold Λ Σ).
Proof. by intros X Y H; rewrite -(iProp_unfold_fold X) H iProp_unfold_fold. Qed.
Instance iProp_unfold_inj n Σ : Injective (dist n) (dist n) (@iProp_unfold Σ).
Instance iProp_unfold_inj n Λ Σ :
Injective (dist n) (dist n) (@iProp_unfold Λ Σ).
Proof. by intros X Y H; rewrite -(iProp_fold_unfold X) H iProp_fold_unfold. Qed.
Require Export iris.model.
Definition inv {Σ} (i : positive) (P : iProp Σ) : iProp Σ :=
Definition inv {Λ Σ} (i : positive) (P : iProp Λ Σ) : iProp Λ Σ :=
uPred_own (Res {[ i to_agree (Later (iProp_unfold P)) ]} ).
Arguments inv {_} _ _%I.
Definition ownP {Σ} (σ : istate Σ) : iProp Σ := uPred_own (Res (Excl σ) ).
Definition ownG {Σ} (m : iGst Σ) : iProp Σ := uPred_own (Res m).
Instance: Params (@inv) 2.
Instance: Params (@ownP) 1.
Instance: Params (@ownG) 1.
Arguments inv {_ _} _ _%I.
Definition ownP {Λ Σ} (σ: state Λ) : iProp Λ Σ := uPred_own (Res (Excl σ) ).
Definition ownG {Λ Σ} (m : iGst Λ Σ) : iProp Λ Σ := uPred_own (Res m).
Instance: Params (@inv) 3.
Instance: Params (@ownP) 2.
Instance: Params (@ownG) 2.
Typeclasses Opaque inv ownG ownP.
Section ownership.
Context {Σ : iParam}.
Implicit Types r : iRes Σ.
Implicit Types σ : istate Σ.
Implicit Types P : iProp Σ.
Implicit Types m : iGst Σ.
Context {Λ : language} {Σ : iFunctor}.
Implicit Types r : iRes Λ Σ.
Implicit Types σ : state Λ.
Implicit Types P : iProp Λ Σ.
Implicit Types m : iGst Λ Σ.
(* Invariants *)
Global Instance inv_contractive i : Contractive (@inv Σ i).
Global Instance inv_contractive i : Contractive (@inv Λ Σ i).
Proof.
intros n P Q HPQ.
apply (_: Proper (_ ==> _) iProp_unfold), Later_contractive in HPQ.
......@@ -36,18 +36,18 @@ Lemma inv_sep_dup i P : inv i P ≡ (inv i P ★ inv i P)%I.
Proof. apply (uPred.always_sep_dup' _). Qed.
(* physical state *)
Lemma ownP_twice σ1 σ2 : (ownP σ1 ownP σ2 : iProp Σ) False.
Lemma ownP_twice σ1 σ2 : (ownP σ1 ownP σ2 : iProp Λ Σ) False.
Proof.
rewrite /ownP -uPred.own_op Res_op.
by apply uPred.own_invalid; intros (_&?&_).
Qed.
Global Instance ownP_timeless σ : TimelessP (ownP σ).
Global Instance ownP_timeless σ : TimelessP (@ownP Λ Σ σ).
Proof. rewrite /ownP; apply _. Qed.
(* ghost state *)
Global Instance ownG_ne n : Proper (dist n ==> dist n) (@ownG Σ).
Global Instance ownG_ne n : Proper (dist n ==> dist n) (@ownG Λ Σ).
Proof. by intros m m' Hm; unfold ownG; rewrite Hm. Qed.
Global Instance ownG_proper : Proper (() ==> ()) (@ownG Σ) := ne_proper _.
Global Instance ownG_proper : Proper (() ==> ()) (@ownG Λ Σ) := ne_proper _.
Lemma ownG_op m1 m2 : ownG (m1 m2) (ownG m1 ownG m2)%I.
Proof. by rewrite /ownG -uPred.own_op Res_op !(left_id _ _). Qed.
Lemma always_ownG_unit m : ( ownG (unit m))%I ownG (unit m).
......
Require Export modures.cmra iris.language.
Structure iParam := IParam {
iexpr : Type;
ival : Type;
istate : Type;
ilanguage : Language iexpr ival istate;
icmra : cofeT cmraT;
icmra_empty A : Empty (icmra A);
icmra_identity A : CMRAIdentity (icmra A);
icmra_map {A B} (f : A -n> B) : icmra A -n> icmra B;
icmra_map_ne {A B} n : Proper (dist n ==> dist n) (@icmra_map A B);
icmra_map_id {A : cofeT} (x : icmra A) : icmra_map cid x x;
icmra_map_compose {A B C} (f : A -n> B) (g : B -n> C) x :
icmra_map (g f) x icmra_map g (icmra_map f x);
icmra_map_mono {A B} (f : A -n> B) : CMRAMonotone (icmra_map f)
}.
Existing Instances ilanguage.
Existing Instances icmra_empty icmra_identity.
Existing Instances icmra_map_ne icmra_map_mono.
Canonical Structure istateC Σ := leibnizC (istate Σ).
Lemma icmra_map_ext (Σ : iParam) {A B} (f g : A -n> B) m :
( x, f x g x) icmra_map Σ f m icmra_map Σ g m.
Proof.
by intros ?; apply equiv_dist=> n; apply icmra_map_ne=> ?; apply equiv_dist.
Qed.
Program Definition iParam_const {iexpr ival istate : Type}
(ilanguage : Language iexpr ival istate)
(icmra : cmraT)
{icmra_empty : Empty icmra} {icmra_identity : CMRAIdentity icmra} : iParam :=
{|
iexpr := iexpr; ival := ival; istate := istate;
icmra A := icmra; icmra_map A B f := cid
|}.
Solve Obligations with done.
\ No newline at end of file
......@@ -7,38 +7,38 @@ Local Hint Extern 10 (✓{_} _) =>
repeat match goal with H : wsat _ _ _ _ |- _ => apply wsat_valid in H end;
solve_validN.
Program Definition pvs {Σ} (E1 E2 : coPset) (P : iProp Σ) : iProp Σ :=
Program Definition pvs {Λ Σ} (E1 E2 : coPset) (P : iProp Λ Σ) : iProp Λ Σ :=
{| uPred_holds n r1 := rf k Ef σ,
1 < k n (E1 E2) Ef =
wsat k (E1 Ef) σ (r1 rf)
r2, P k r2 wsat k (E2 Ef) σ (r2 rf) |}.
Next Obligation.
intros Σ E1 E2 P r1 r2 n HP Hr rf k Ef σ ?? Hwsat; simpl in *.
intros Λ Σ E1 E2 P r1 r2 n HP Hr rf k Ef σ ?? Hwsat; simpl in *.
apply HP; auto. by rewrite (dist_le _ _ _ _ Hr); last lia.
Qed.
Next Obligation. intros Σ E1 E2 P r rf k Ef σ; simpl in *; lia. Qed.
Next Obligation. intros Λ Σ E1 E2 P r rf k Ef σ; simpl in *; lia. Qed.
Next Obligation.
intros Σ E1 E2 P r1 r2 n1 n2 HP [r3 ?] Hn ? rf k Ef σ ?? Hws; setoid_subst.
intros Λ Σ E1 E2 P r1 r2 n1 n2 HP [r3 ?] Hn ? rf k Ef σ ?? Hws; setoid_subst.
destruct (HP (r3rf) k Ef σ) as (r'&?&Hws'); rewrite ?(associative op); auto.
exists (r' r3); rewrite -(associative _); split; last done.
apply uPred_weaken with r' k; eauto using cmra_included_l.
Qed.
Arguments pvs {_} _ _ _%I : simpl never.
Instance: Params (@pvs) 3.
Arguments pvs {_ _} _ _ _%I : simpl never.
Instance: Params (@pvs) 4.
Section pvs.
Context {Σ : iParam}.
Implicit Types P Q : iProp Σ.
Implicit Types m : iGst Σ.
Context {Λ : language} {Σ : iFunctor}.
Implicit Types P Q : iProp Λ Σ.
Implicit Types m : iGst Λ Σ.
Transparent uPred_holds.
Global Instance pvs_ne E1 E2 n : Proper (dist n ==> dist n) (@pvs Σ E1 E2).
Global Instance pvs_ne E1 E2 n : Proper (dist n ==> dist n) (@pvs