Skip to content
Snippets Groups Projects
Commit 96588154 authored by Ralf Jung's avatar Ralf Jung
Browse files

simplify wsat a bit

parent a4b217f3
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
iris_derived_rules.v
+ 1
− 2
View file @ 96588154
......@@ -55,8 +55,7 @@ Module Type IRIS_DERIVED_RULES (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C)
□(timeless P) ⊑ vs m m (▹P) P.
Proof.
apply vsIntro. etransitivity; last by eapply pvsTimeless.
apply and_pord; last reflexivity.
apply box_elim.
rewrite ->box_elim. reflexivity.
Qed.
Lemma vsTrans P Q R m1 m2 m3 (HMS : m2 ⊑ m1 ∪ m3) :
......
iris_meta.v
+ 7
− 8
View file @ 96588154
......@@ -169,12 +169,12 @@ Module Type IRIS_META (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
edestruct (adequacy_ht (w:=w) (k:=S k') HT HSN') as [ws' [φs' [HSWTP HWS]]]; clear HT HSN'.
- rewrite -!plus_n_Sm. eexists ex_unit. reflexivity.
- rewrite -!plus_n_Sm. hnf. eexists fdEmpty. intro.
assert (pv: (CMRA.cmra_valid wt) (S (n + k'))).
split.
{ rewrite /wt /=. split_conjs.
- move=>i. exact I.
- exact I.
- assumption. }
exists pv. split.
split.
+ rewrite /wt. reflexivity.
+ move=>i agP Heq. exfalso. rewrite /wt /= in Heq. exact Heq.
- do 3 eexists. split; [eassumption|]. eassumption.
......@@ -432,14 +432,13 @@ Module Type IRIS_META (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
{ clear -HStUnit. rewrite /State (comm w1) -assoc. simpl. simpl in HStUnit.
rewrite HStUnit. reflexivity. }
clear HStUnit.
assert (pv': cmra_valid (w1 · w2' · comp_finmap wf rs) (S (S k))).
{ clear- pv HSt Heqw HLt.
split; last split.
+ clear- pv HSt Heqw HLt.
destruct pv as [HIVal [HSVal HRVal]]. rewrite /w2'.
split; last split; last 1 first.
- assumption.
- assumption.
- simpl in HSt. rewrite HSt. exact I. }
exists pv'. split.
* assumption.
* assumption.
* simpl in HSt. by rewrite HSt.
+ rewrite HSt. reflexivity.
+ assumption.
Qed.
......
iris_plog.v
+ 12
− 27
View file @ 96588154
......@@ -136,24 +136,24 @@ Module Type IRIS_PLOG (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
(* RJ: Possible simplification: Could we match on (Invs wt i) instead of asking for
a proof of an equality? The proofs end up having to reason about an equality
anyway, so it may or may not end up actually simplifying anything. *)
Definition wsatTotal n' σ s m wt :=
exists pv : (cmra_valid wt (S n')),
(State wt ⊑ ex_own σ) /\
forall i agP (Heq: (Invs wt) i = S n' = Some agP),
match (i ∈ m)%de, s i with
| true , Some w => let P := ra_ag_unInj agP (S n') in unhalved (ı P) w n'
| false, None => True
| _ , _ => False
end.
Definition wsatTotal n' σ (s: nat -f> Wld) m wt :=
(cmra_valid wt (S n')) /\
(State wt ⊑ ex_own σ) /\
forall i agP (Heq: (Invs wt) i = S n' = Some agP),
match (i ∈ m)%de, s i with
| true , Some w => let P := ra_ag_unInj agP (S n') in unhalved (ı P) w n'
| false, None => True
| _ , _ => False
end.
Global Instance wsatTotal_proper n' σ s:
Proper (equiv ==> dist (S n') ==> equiv) (wsatTotal n' σ s).
Proof.
apply proper_sym_impl_iff_2; try apply _; [].
move=>m1 m2 EQm wt1 wt2 EQwt. move=>[pv [HS HI]].
assert (pv': cmra_valid wt2 (S n')).
split.
{ eapply spredNE, pv. apply cmra_valid_dist. assumption. }
exists pv'. split.
split.
{ rewrite <-HS. apply pordR. destruct EQwt as [_ [HwtS _]].
symmetry. exact HwtS. }
move=>i agP Heq.
......@@ -169,7 +169,7 @@ Module Type IRIS_PLOG (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
intros HLe (pv & Hσ & H).
assert (pv': cmra_valid wt (S n'1)).
{ eapply dpred, pv. omega. }
exists pv'.
split; first assumption.
split; [assumption|]. move => {Hσ} i agP Heq.
case HagP':(Invs wt i) => [agP'|]; last first.
{ exfalso. rewrite HagP' in Heq. exact Heq. }
......@@ -231,15 +231,6 @@ Module Type IRIS_PLOG (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
exact:comp_finmap_le.
Qed.
(* Lemma wsat_state {σ m u w k} :
wsat σ m u w (S k) -> fst u == ex_own σ \/ fst u == 1.
Proof.
move: u=>[ux ug]; move=>[rs [ [ Hv Heq] _] ] {m w k}; move: Hv Heq.
move: (comp_map _)=> [rsx rsg] [Hv _] {rs}; move: Hv.
rewrite ra_op_prod_fst 2![fst _]/=.
by case: ux; case: rsx; auto.
Qed.*)
End WorldSatisfaction.
(* Simple view lemma. *)
......@@ -315,12 +306,6 @@ Module Type IRIS_PLOG (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
Section WeakestPre.
(* RJ this should now be captured by the generic instance for discrete metrics.
Instance LP_isval : LimitPreserving is_value.
Proof.
intros σ σc HC; apply HC.
Qed. *)
Local Obligation Tactic := intros; eauto with typeclass_instances.
Definition safeExpr e σ :=
......
iris_vs_rules.v
+ 21
− 23
View file @ 96588154
......@@ -33,28 +33,26 @@ Module Type IRIS_VS_RULES (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP:
(inv i P) ⊑ pvs (de_sing i) de_emp (▹P).
Proof.
intros w n HInv.
destruct n; first exact:bpred. intros ?; intros.
destruct n; first exact:bpred. repeat intro.
destruct HInv as [Pr HInv].
destruct HE as [rs [pv [HS HM]]].
case HLu:(Invs w i) => [μ |] ; simpl in HInv; last first.
{ exfalso. rewrite HLu in HInv. destruct HInv. }
destruct HE as [rs [pv [HS HM]]]. simpl in HInv.
move:(HM i (ra_ag_inj (ı' (halved P)))). case/(_ _)/Wrap.
{ clear -HLu HInv pv HLe. eapply world_invs_extract; first assumption; last first.
{ clear -HInv pv HLe. eapply world_invs_extract; first assumption; last first.
- eapply mono_dist, HInv. omega.
- etransitivity; last eapply comp_finmap_le. exists wf. now rewrite comm. }
rewrite /de_sing. erewrite de_in_true by de_tauto.
erewrite de_in_true by de_tauto.
destruct (rs i) as [wi |] eqn: HLr; last by move=>[]. move=>HP.
exists (w · wi). split.
{ simpl. eapply propsMW; first (eexists; reflexivity). eapply spredNE, HP.
simpl. rewrite isoR. reflexivity. }
clear HLu HInv HP.
clear HInv HP.
exists (fdStrongUpdate i None rs). intros wt.
assert (Heqwt: comp_finmap (w · wf) rs == wt).
{ rewrite /wt (comm _ wi) -assoc (comp_finmap_move wi).
rewrite (comm wi) -comp_finmap_remove; last now rewrite HLr. reflexivity. }
assert (pv': (cmra_valid wt) (S (S k))).
split.
{ eapply spredNE, pv. rewrite -Heqwt. reflexivity. }
exists pv'. split.
split.
- rewrite /= -Heqwt. assumption.
- move=>j agP Hlu. rewrite (comm de_emp) de_emp_union. move:(HM j agP)=>{HM}.
case/(_ _)/Wrap.
......@@ -63,11 +61,11 @@ Module Type IRIS_VS_RULES (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP:
+ erewrite de_in_true by de_tauto.
destruct (dec_eq i j) as [EQ|NEQ].
{ exfalso. subst j. move:(HD i) Hm. clear. de_tauto. }
erewrite fdStrongUpdate_neq by assumption. tauto.
erewrite fdStrongUpdate_neq by assumption. done.
+ destruct (dec_eq i j) as [EQ|NEQ].
{ move=>_. subst j. rewrite fdStrongUpdate_eq. exact I. }
{ move=>_. subst j. rewrite fdStrongUpdate_eq. done. }
erewrite de_in_false by de_tauto.
erewrite fdStrongUpdate_neq by assumption. tauto.
erewrite fdStrongUpdate_neq by assumption. done.
Qed.
Lemma pvsClose i P :
......@@ -94,9 +92,9 @@ Module Type IRIS_VS_RULES (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP:
move=>_. reflexivity. }
rewrite -(comm w) -(comp_finmap_move w) assoc (comm _ (1w)) ra_op_unit.
reflexivity. }
assert (pv': (cmra_valid wt) (S (S k))).
split.
{ eapply spredNE, pv. rewrite -Heqwt. reflexivity. }
exists pv'. split.
split.
- rewrite /State -Heqwt. assumption.
- move=>j agP Hlu. destruct (dec_eq i j) as [EQ|NEQ].
+ subst j. erewrite de_in_true by de_tauto.
......@@ -111,8 +109,8 @@ Module Type IRIS_VS_RULES (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP:
+ move:(HM j agP)=>{HM}. case/(_ _)/Wrap.
{ rewrite Heqwt. assumption. }
rewrite comm de_emp_union. destruct (j ∈ mf) eqn:Hjin.
* erewrite de_in_true by de_tauto. erewrite fdStrongUpdate_neq by assumption. tauto.
* erewrite de_in_false by de_tauto. erewrite fdStrongUpdate_neq by assumption. tauto.
* erewrite de_in_true by de_tauto. by erewrite fdStrongUpdate_neq.
* erewrite de_in_false by de_tauto. by erewrite fdStrongUpdate_neq.
Qed.
Lemma pvsTrans P m1 m2 m3 (HMS : m2 ⊑ m1 ∪ m3) :
......@@ -189,10 +187,10 @@ Module Type IRIS_VS_RULES (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP:
+ simpl. exists (exist _ _ HP). simpl.
eexists. now erewrite comm.
+ exists rs. simpl. rewrite comp_finmap_move. clear HP Hgval.
assert (pv':(cmra_valid ((I0, (S0, g1 · g')) · comp_finmap wf rs)) (S (S k))).
split.
{ split; last split; try assumption; [].
now rewrite ->assoc in HVal1. }
exists pv'. split; assumption.
done.
Qed.
Program Definition inv' m : Props -n> {n : nat | n ∈ m = true } -n> Props :=
......@@ -234,13 +232,13 @@ Module Type IRIS_VS_RULES (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP:
apply dist_refl. symmetry. eapply ra_ag_dupl. }
exists (fdStrongUpdate i (Some w) rs). simpl. simpl in HLi.
rewrite comp_finmap_move. erewrite <-comp_finmap_add by (now apply equivR). rewrite (comm _ w).
assert (pv': cmra_valid (w' · (w · comp_finmap wf rs)) (S (S k))).
{ destruct pv as [pvI pvR]. split.
- rewrite /w' /=. move=>j /=. destruct (dec_eq i j).
+ subst j. rewrite HLi /=. exact I.
split.
{ destruct pv as [pvI pvR]. split.
- rewrite /w' /= =>j /=. destruct (dec_eq i j).
+ subst j. rewrite HLi /=. done.
+ exact:(pvI j).
- rewrite assoc /w' /= !ra_op_unit. exact pvR. }
exists pv'. split.
split.
- rewrite /State assoc /w' /= ra_op_unit. assumption.
- move=>j agP Heq. destruct (dec_eq i j) as [EQ|NEQ].
+ subst j. erewrite de_in_true by de_tauto. rewrite fdStrongUpdate_eq.
......
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