Commit f51fa027 authored by Ralf Jung's avatar Ralf Jung

prove pvsOpen and pvsClose

On branch hackgreement
	modified:   coq-ho/iris_core.v
no changes added to commit (use "git add" and/or "git commit -a")
parent f4fca45b
......@@ -87,11 +87,11 @@ Module Type IRIS_CORE (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
Implicit Types (P Q : Props) (w : Wld) (n i k : nat) (r : res) (g : RL.res) (σ : state).
Definition Invs (w: Wld) := fst w.
Definition Invs (w: Wld) := Mfst w.
Arguments Invs !w /.
Definition State (w: Wld) := fst (snd w).
Definition State (w: Wld) := Mfst (Msnd w).
Arguments State !w /.
Definition Res (w: Wld) := snd (snd w).
Definition Res (w: Wld) := Msnd (Msnd w).
Arguments Res !w /.
(* Simple view lemmas. *)
......@@ -175,12 +175,38 @@ Module Type IRIS_CORE (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
reflexivity.
Qed.
Lemma finmap_invs_le (I1 I2: nat -f> ra_agree PreProp) i (μ: ra_agree PreProp):
I1 i = Some μ -> I1 I2 ->
exists μ', μ μ' /\ I2 i = Some μ'.
Lemma world_invs_valid w1 w2 μ i n:
cmra_valid w1 n -> w2 w1 -> Invs w2 i = n = Some μ -> cmra_valid μ n.
Proof.
move=>Heq Hord. specialize (Hord i). rewrite Heq in Hord. destruct (I2 i) as [μ'|]; last contradiction.
exists μ'. split; last reflexivity. exact Hord.
move=>Hval Hle Heq. destruct w1 as [I1 [S1 g1]], w2 as [I2 [S2 g2]]. destruct Hval as [Hval _]. simpl in Heq. apply ra_pord_iff_prod_pord in Hle.
destruct Hle as [Hle _]. simpl in Hle.
apply ra_pord_iff_ext_pord in Hle.
clear S1 g1 S2 g2. specialize (Hval i). specialize (Hle i).
destruct n; first exact:bpred.
destruct (I2 i); last contradiction Heq.
destruct (I1 i); last contradiction Hle. simpl in Hle.
simpl in Heq. eapply spredNE.
- rewrite -Heq. reflexivity.
- eapply cmra_valid_ord; eassumption.
Qed.
Lemma world_invs_extract w1 w2 μ μ' i n:
cmra_valid w1 n -> w2 w1 -> Invs w2 i = n = Some (μ' · μ) ->
Invs w1 i = n = Some μ.
Proof.
move=> Hval [w' Hleq] Hlu. unfold Invs. rewrite -Hleq.
simpl morph. rewrite ra_op_prod_fst {1}/ra_op /ra_op_finprod fdComposeRed.
destruct n; first exact:dist_bound.
rewrite /Invs /= in Hlu. destruct (fst w2 i) as [μ2|] eqn:Hw2; last contradiction Hlu.
destruct (fst w' i) as [μ1|] eqn:Hw1; simpl in *.
- rewrite Hlu assoc (comm _ μ). apply ra_ag_prod_dist. eapply world_invs_valid; first eexact Hval; first reflexivity.
rewrite -Hleq. rewrite /Invs. simpl morph. instantiate (1:=i).
rewrite ra_op_prod_fst {1}/ra_op /ra_op_finprod fdComposeRed. rewrite Hw2 Hw1. simpl.
now rewrite Hlu (comm μ) assoc.
- rewrite Hlu comm. apply ra_ag_prod_dist. eapply world_invs_valid; first eexact Hval; first reflexivity.
rewrite -Hleq. rewrite /Invs. simpl morph. instantiate (1:=i).
rewrite ra_op_prod_fst {1}/ra_op /ra_op_finprod fdComposeRed. rewrite Hw2 Hw1. simpl.
now rewrite comm.
Qed.
End FinmapInvs.
......@@ -556,9 +582,9 @@ Module Type IRIS_CORE (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
{ rewrite /snd ra_op_unit. reflexivity. }
simpl. move=>j. rewrite /ra_op /ra_op_finprod fdComposeRed.
destruct (dec_eq i j).
+ subst j. rewrite fdStrongUpdate_eq. unfold Invs, fst in Heq.
+ subst j. rewrite fdStrongUpdate_eq. simpl in Heq.
destruct (I i) as [Ii|]; last contradiction Heq.
rewrite /finprod_op. do 3 red. do 3 red in Heq.
rewrite /finprod_op. simpl in *.
rewrite Heq=>{Heq}. apply dist_refl. rewrite assoc (comm _ Pr) -assoc.
rewrite ra_ag_dupl. reflexivity.
+ erewrite fdStrongUpdate_neq by assumption. destruct (I j); reflexivity.
......
Require Import Ssreflect.ssreflect Omega.
Require Import Ssreflect.ssreflect Ssreflect.ssrfun Omega.
Require Import world_prop core_lang lang iris_core.
Require Import ModuRes.DecEnsemble ModuRes.RA ModuRes.CMRA ModuRes.SPred ModuRes.SPred ModuRes.BI ModuRes.PreoMet ModuRes.Finmap ModuRes.RAConstr ModuRes.Agreement ModuRes.Lists.
......@@ -73,7 +73,7 @@ Module Type IRIS_PLOG (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
rewrite /comp_finmap in IH. apply IH.
Qed.
Lemma comp_finmap_move w0 w1 f:
Lemma comp_finmap_move w1 w0 f:
comp_finmap (w0 · w1) f == comp_finmap w0 f · w1.
Proof.
rewrite /comp_finmap. revert f. apply:fdRect.
......@@ -123,13 +123,15 @@ Module Type IRIS_PLOG (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
Lemma world_inv_val {w} {s : nat -f> Wld} {n}:
let wt := comp_finmap w s in
forall (pv: cmra_valid wt n) {i agP} (Heq: (Invs wt) i = Some agP), cmra_valid agP n.
forall (pv: cmra_valid wt n) {i agP} (Heq: (Invs wt) i = n = Some agP), cmra_valid agP n.
Proof.
intros wt pv i agP Heq.
destruct wt as [I O]. destruct pv as [HIval _]. specialize (HIval i).
simpl Invs in Heq. destruct (I i).
- eapply spredNE, HIval. apply cmra_valid_dist. inversion Heq. reflexivity.
- discriminate.
- eapply spredNE, HIval. apply cmra_valid_dist.
destruct n; first exact:dist_bound.
exact Heq.
- destruct n; first exact:bpred. destruct Heq.
Qed.
(* It may be possible to use "later_sp" here, but let's avoid indirections where possible. *)
......@@ -140,7 +142,7 @@ Module Type IRIS_PLOG (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
let wt := comp_finmap w s in
exists pv : (cmra_valid wt n),
(State wt ex_own σ) /\
forall i agP (Heq: (Invs wt) i = Some agP),
forall i agP (Heq: (Invs wt) i = n = Some agP),
match (i m)%de, s i with
| true , Some w => let P := ra_ag_unInj agP n (HVal:=world_inv_val pv Heq) in
unhalved (ı P) w n'
......@@ -157,12 +159,20 @@ Module Type IRIS_PLOG (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
intros (s & pv & Hσ & H).
exists s. exists (dpred (m := S n2) HLe pv).
split; [assumption|]. move => {Hσ} i agP Heq.
move:(H i agP Heq)=>{H}.
case HagP':(Invs (comp_finmap w s) i) => [agP'|]; last first.
{ exfalso. rewrite HagP' in Heq. exact Heq. }
move:(H i agP'). case/(_ _)/Wrap; last move=>{H} Heq'.
{ now apply equivR. }
destruct (s i) as [ws|], (i m)%de; simpl; tauto || (try contradiction); []=>H.
eapply spredNE; last first.
- eapply dpred; last exact H. omega.
- specialize (halve_eq (T:=Props) n2)=>Huneq. apply Huneq=>{Huneq H ws}.
apply met_morph_nonexp. symmetry. apply ra_ag_unInj_move. omega.
apply met_morph_nonexp. move:(Heq). rewrite HagP' in Heq=>Heq''.
etransitivity.
+ symmetry. eapply ra_ag_unInj_move. omega.
+ eapply ra_ag_unInj_dist. simpl in Heq'. exact Heq.
Grab Existential Variables.
{ eapply dpred; first eassumption. eapply world_inv_val; eassumption. }
Qed.
Global Instance wsat_dist n σ : Proper (equiv ==> dist n ==> dist n) (wsat σ).
......@@ -179,15 +189,11 @@ Module Type IRIS_PLOG (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
{ rewrite <-HS. apply pordR. destruct Hwt as [_ [HwtS _]].
symmetry. exact HwtS. }
move=>i agP Heq.
edestruct (fdLookup_in_dist_strong (f2 := Invs (comp_finmap w1 s)) (n:=m) Heq) as [agP' [Heq' HagPeq]].
{ rewrite -Hwt. reflexivity. }
specialize (HI _ _ Heq'). rewrite -EQm. destruct (i m1)%de; last exact HI.
move:(HI i agP). case/(_ _)/Wrap; last move=>{HI} Heq' HI.
{ rewrite -Heq. rewrite Hwt. reflexivity. }
rewrite -EQm. destruct (i m1)%de; last exact HI.
destruct (s i); last exact HI.
simpl. simpl in HI.
eapply spredNE, HI.
specialize (halve_eq (T:=Props) m)=>Huneq. apply Huneq=>{Huneq HS}.
apply met_morph_nonexp. eapply ra_ag_unInj_dist.
symmetry. assumption.
simpl. simpl in HI. erewrite ra_ag_unInj_pi. eassumption.
Qed.
Global Instance wsat_equiv σ : Proper (equiv ==> equiv ==> equiv) (wsat σ).
......
This diff is collapsed.
......@@ -28,7 +28,7 @@ Section Agreement.
Global Instance ra_agree_unit : RA_unit ra_agree := fun x => x.
Global Program Instance cmra_agree_valid : CMRA_valid _ :=
fun x => match x with
| ag_inj valid _ _ => valid
| ag_inj v _ _ => v
end.
Global Instance ra_agree_valid : RA_valid _ := compose valid_sp cmra_agree_valid.
......@@ -445,7 +445,13 @@ Section Agreement.
{ exact HVal2. }
Qed.
Lemma ra_ag_inj_unInj x n {HVal: cmra_valid x n} t d:
Lemma ra_ag_unInj_pi x n {HVal1: cmra_valid x n} {HVal2: cmra_valid x n}:
ra_ag_unInj x n (HVal:=HVal1) = ra_ag_unInj x n (HVal:=HVal2).
Proof.
ra_ag_destr. rewrite /ra_ag_unInj. pi.
Qed.
Lemma ra_ag_inj_unInj_ext x n {HVal: cmra_valid x n} t d:
d · ra_ag_inj t = n = x -> ra_ag_unInj x n (HVal:=HVal) = n = t.
Proof.
rewrite comm.
......
......@@ -76,9 +76,13 @@ Notation "de1 \ de2" := (de_minus de1 de2) (at level 35) : de_scope.
Notation "de1 # de2" := (de1 de2 == de_emp) (at level 70) : de_scope.
(* Some automation *)
Ltac de_unfold := unfold de_cap, de_cup, de_minus, de_compl; unlock.
Ltac de_in_destr := repeat progress (simpl; unfold const;
repeat (match goal with [ |- context[?t ?de] ] => destruct (t de) end)).
Ltac de_unfold := unfold de_cap, de_cup, de_minus, de_compl; unlock; simpl.
Ltac de_in_destr := repeat progress
(simpl; unfold const;
repeat (match goal with
| [ |- context[?t ?de] ] => destruct (t de)
| [ |- context[dec_eq ?i ?j] ] => destruct (dec_eq i j); first try subst j; try contradiction_eq
end)).
Ltac de_tauto := de_unfold; de_in_destr; rewrite ?de_ft_eq ?de_tf_eq ?de_tt_eq ?de_ff_eq; repeat (split || intro); (reflexivity || discriminate || tauto).
Ltac de_auto_eq := destruct_conjs;
let t := fresh "t" in move=>t;
......@@ -148,6 +152,54 @@ Section DecEnsembleProps.
Global Instance de_compl_equiv: Proper (equiv ==> equiv) (@de_compl T).
Proof. do 3 intro. de_auto_eq. Qed.
Lemma de_in_true de t: (* This looks stupid, but it is useful to get de_tauto started. *)
t de = true -> t de = true.
Proof.
tauto.
Qed.
Lemma de_in_false de t: (* This looks stupid, but it is useful to get de_tauto started. *)
t de = false -> t de = false.
Proof.
tauto.
Qed.
Lemma de_union_true de1 de2 t:
t de1 = true -> t (de1 de2) = true.
Proof.
intros. de_tauto.
Qed.
Lemma de_union_true2 de1 de2 t:
t de2 = true -> t (de1 de2) = true.
Proof.
intros. de_tauto.
Qed.
Lemma de_union_false de1 de2 t:
t de1 = false -> t de2 = false -> t (de1 de2) = false.
Proof.
intros. de_tauto.
Qed.
Lemma de_isect_true de1 de2 t:
t de1 = true -> t de2 = true -> t (de1 de2) = true.
Proof.
intros. de_tauto.
Qed.
Lemma de_isect_false de1 de2 t:
t de1 = false -> t (de1 de2) = false.
Proof.
intros. de_tauto.
Qed.
Lemma de_isect_false2 de1 de2 t:
t de2 = false -> t (de1 de2) = false.
Proof.
intros. de_tauto.
Qed.
End DecEnsembleProps.
Section DecEqEnsemble.
......@@ -161,21 +213,19 @@ Section DecEqEnsemble.
Lemma de_sing_union de t:
de_sing t de == de_set de t true.
Proof.
move=>t'. rewrite /de_sing /de_set /=. de_unfold =>/=. destruct (dec_eq t t'); de_tauto.
de_auto_eq.
Qed.
Lemma de_set_eq de t b:
t de_set de t b = b.
Proof.
simpl. rewrite DecEq_refl. reflexivity.
de_tauto.
Qed.
Lemma de_set_neq de t b t':
t <> t' -> t' de_set de t b = t' de.
Proof.
move=>Hneq. simpl.
destruct (dec_eq t t') as [EQ|NEQ]; first contradiction.
reflexivity.
intros. de_tauto.
Qed.
End DecEqEnsemble.
......
......@@ -252,23 +252,6 @@ Section FinDom.
now apply HEqf.
Qed.
Lemma fdLookup_in_dist_strong {f1 f2 : K -f> V} {n k v}:
f1 k = Some v -> f1 = S n = f2 ->
exists v', f2 k = Some v' /\ v = S n = v'.
Proof.
move=>EQk EQf. specialize (EQf k). rewrite EQk in EQf.
destruct (f2 k) as [v'|].
- exists v'. split; first reflexivity. exact EQf.
- destruct EQf.
Qed.
Lemma fdLookup_notin_dist_strong {f1 f2 : K -f> V} {n k}:
f1 k = None -> f1 = S n = f2 -> f2 k = None.
Proof.
move=>EQk EQf. specialize (EQf k). rewrite EQk in EQf.
destruct (f2 k); last reflexivity. destruct EQf.
Qed.
Definition finmap_chainx (σ : chain (K -f> V)) {σc : cchain σ} x : chain (option V) :=
fun n => (σ n) x.
......
......@@ -56,6 +56,10 @@ Proof.
move=>n1 n2. decide equality.
Qed.
Ltac contradiction_eq := match goal with
| [ H : ?i <> ?i |- _ ] => exfalso; now apply H
end.
(* Well-founded induction. *)
Definition wf_nat_ind := well_founded_induction Wf_nat.lt_wf.
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