Require Import Vbase Classical extralib.
Require Import fslassn fslassnsem fslassnlemmas fslmodel.
Require Import permission GpsSepAlg.
Require Import Setoid Program.
Open Scope string_scope.
Set Implicit Arguments.
Additional lemmas about FSL assertions.
Basic lemmmas
Lemma exact_label_emp PS PSg: ∀ lbl, HlabeledExact (@hemp PS PSg) lbl.
Proof.
eby ins; eexists _, _; split.
Qed.
Lemma assn_sem_star PS PSg (P Q: assn PS PSg) h:
assn_sem (P &*& Q) h ↔ h ≠ Hundef ∧ ∃ hp hq, h = hp +!+ hq ∧ assn_sem P hp ∧ assn_sem Q hq.
Proof.
eby split; ins; desf; repeat eexists.
Qed.
Setoid compatibility
Lemma implies_refl PS PSg (P: assn PS PSg) : implies P P.
Proof. done. Qed.
Lemma implies_star_l PS PSg (P Q R: assn PS PSg) : implies P Q → implies (Astar P R) (Astar Q R).
Proof.
red; ins; desf; repeat eexists; eauto.
Qed.
Lemma implies_star_r PS PSg (P Q R: assn PS PSg) : implies P Q → implies (Astar R P) (Astar R Q).
Proof.
red; ins; desf; repeat eexists; eauto.
Qed.
Lemma implies_star PS PSg (P Q P' Q': assn PS PSg):
implies P P' → implies Q Q' → implies (P &*& Q) (P' &*& Q').
Proof.
ins; eapply implies_trans; split.
eby apply implies_star_l.
by apply implies_star_r.
Qed.
Lemma implies_trans2 PS PSg: ∀ x y z : assn PS PSg, implies x y → implies y z → implies x z.
Proof.
unfold implies; eauto.
Qed.
Global Add Parametric Relation PS PSg : (assn PS PSg) (@implies PS PSg)
reflexivity proved by (@implies_refl PS PSg)
transitivity proved by (@implies_trans2 PS PSg)
as implies_rel.
Global Add Parametric Morphism PS PSg : (@implies PS PSg)
with signature (@implies PS PSg) --> (@implies PS PSg) ++> impl
as implies_morphism.
Proof. unfold impl, implies; ins; eauto. Qed.
Global Add Parametric Morphism PS PSg : (@Astar PS PSg)
with signature (@implies PS PSg) ==> (@implies PS PSg) ==> (@implies PS PSg)
as Astar_morphism.
Proof. eauto using implies_star. Qed.
Ltac fold_implies :=
match goal with |- ∀ _ : heap ?PS ?PSg, assn_sem ?P _ → assn_sem ?Q _ ⇒ fold (@implies PS PSg P Q) end.
Ltac refl_implies :=
match goal with |- implies ?A ?B ⇒ let X := fresh in cut (A = B); [by intro X; rewrite X | ] end.
Definition equivalent PS PSg (P Q: assn PS PSg) := implies P Q ∧ implies Q P.
Lemma equivalent_refl PS PSg (P: assn PS PSg): equivalent P P.
Proof.
split; apply implies_refl.
Qed.
Lemma equivalent_trans PS PSg: ∀ x y z : assn PS PSg, equivalent x y → equivalent y z → equivalent x z.
Proof.
unfold equivalent; ins; desf; eauto using implies_trans2.
Qed.
Lemma equivalent_sym PS PSg (P Q: assn PS PSg): equivalent P Q → equivalent Q P.
Proof.
unfold equivalent; tauto.
Qed.
Global Add Parametric Relation PS PSg : (assn PS PSg) (@equivalent PS PSg)
reflexivity proved by (@equivalent_refl PS PSg)
symmetry proved by (@equivalent_sym PS PSg)
transitivity proved by (@equivalent_trans PS PSg)
as equivalence_rel.
Global Add Parametric Morphism PS PSg : (@implies PS PSg)
with signature (@equivalent PS PSg) ==> (@equivalent PS PSg) ==> iff
as implies_morphism'.
Proof. unfold iff, equivalent, implies; split; ins; desf; eauto. Qed.
Global Add Parametric Morphism PS PSg : (@Astar PS PSg)
with signature (@equivalent PS PSg) ==> (@equivalent PS PSg) ==> (@equivalent PS PSg)
as Astar_morphism'.
Proof. unfold equivalent; ins; desc; split; eauto using implies_star. Qed.
Implication lemmas
Lemma false_implies PS PSg (P: assn PS PSg): implies Afalse P.
Proof.
red; ins.
Qed.
Lemma implies_true PS PSg (P: assn PS PSg): implies P Atrue.
Proof.
red; ins.
split; ins.
eby eapply assn_sem_def.
Qed.
Lemma implies_sim PS PSg (P Q: assn PS PSg) : Asim P Q → implies P Q.
Proof. by red; ins; apply (sim_assn_sem H). Qed.
Lemma Arel_split1 PS PSg x v PP :
@implies PS PSg (Arel x PP)
(Astar (Arel x PP) (Arel x (mupd (fun _ ⇒ Afalse) v (PP v)))).
Proof.
unfold mupd; red; ins; desf; repeat eexists; ins.
rewrite hplus_unfold; desf; f_equal; ins.
by extensionality y; ins; unfold hupd; desf; desf; ins; f_equal;
extensionality z; unfold Remp; desf; desf;
eapply assn_mod_eqI1; ins; apply assn_norm_star_emp.
by apply gres_plus_total_emp_l.
destruct n; unnw; split.
by ins; unfold hupd; desf; desf; ins; repeat split; ins; desf; vauto.
by rewrite gres_plus_emp_r.
Qed.
Lemma Arainit_split1 PS PSg x :
@implies PS PSg (Arainit x)
(Astar (Arainit x) (Arainit x)).
Proof.
unfold mupd; red; ins; desf; repeat eexists; ins.
rewrite hplus_unfold; desf; f_equal; ins.
by extensionality y; ins; unfold hupd; desf; desf; ins; f_equal;
extensionality z; unfold Remp; desf; desf;
eapply assn_mod_eqI1; ins; apply assn_norm_star_emp.
by apply gres_plus_total_emp_l.
destruct n; unnw; split.
by ins; unfold hupd; desf; desf; ins; repeat split; ins; desf; vauto.
by rewrite gres_plus_emp_r.
Qed.
Lemma Arainit_split2 PS PSg x :
@implies PS PSg (Astar (Arainit x) (Arainit x)) (Arainit x).
Proof.
unfold mupd; red; ins; desf; repeat eexists; ins.
rewrite hplus_unfold; desf; f_equal; ins.
by extensionality y; ins; unfold hupd; desf; desf; ins; f_equal;
extensionality z; unfold Remp; desf; desf;
eapply assn_mod_eqI1; ins; apply assn_norm_star_emp.
by apply gres_plus_total_emp_l.
destruct n; unnw; split.
by ins; unfold hupd; desf; desf; ins; repeat split; ins; desf; vauto.
by rewrite gres_plus_emp_r.
Qed.
Lemma Arel_split11 PS PSg x PP :
implies (Arel x PP)
(@Astar PS PSg (Arel x PP) (Arel x PP)).
Proof.
unfold mupd; red; ins; desf; repeat eexists; ins.
rewrite hplus_unfold; desf; f_equal; ins.
by extensionality y; ins; unfold hupd; desf; desf; ins; f_equal;
extensionality z; unfold Remp; desf; desf;
eapply assn_mod_eqI1; ins; apply assn_norm_star_emp.
by apply gres_plus_total_emp_l.
destruct n; unnw; split.
by ins; unfold hupd; desf; desf; ins; repeat split; ins; desf; vauto.
by rewrite gres_plus_emp_r.
Qed.
Lemma Armw_acq_split1 PS PSg x PP QQ :
(∀ v, QQ v = Aemp ∨ PP v = Afalse ∧ QQ v = Afalse) →
@implies PS PSg (Armwacq x PP) (Astar (Armwacq x PP) (Aacq x QQ)).
Proof.
unfold mupd; red; ins; desf; repeat eexists; ins.
rewrite hplus_unfold; desf; f_equal; ins.
by extensionality y; ins; unfold hupd; desf; desf; ins; f_equal;
extensionality z; unfold Remp; desf; desf;
eapply assn_mod_eqI1; ins; apply assn_norm_star_emp.
by apply gres_plus_total_emp_l.
destruct n; unnw; split.
2: by rewrite gres_plus_emp_r.
ins; unfold hupd; desf; desf; ins; repeat split; ins; desf; vauto.
destruct (H v) as [->|[->->]]; vauto.
Qed.
Lemma Armw_acq_split2 PS PSg x PP QQ :
(∀ v, QQ v = Aemp ∨ PP v = Afalse ∧ QQ v = Afalse) →
@implies PS PSg (Astar (Armwacq x PP) (Aacq x QQ)) (Armwacq x PP).
Proof.
unfold mupd; red; ins; desf; repeat eexists; ins.
rewrite hplus_unfold; desf; f_equal; ins.
by extensionality y; ins; unfold hupd; desf; desf; ins; f_equal;
extensionality z; unfold Remp; desf; desf;
eapply assn_mod_eqI1; ins; apply assn_norm_star_emp.
by apply gres_plus_total_emp_l.
destruct n; unnw; split.
2: by rewrite gres_plus_emp_r.
ins; unfold hupd; desf; desf; ins; repeat split; ins; desf; vauto.
destruct (H v) as [->|[->->]]; vauto.
Qed.
Equivalence lemmas
Lemma star_false PS PSg (P: assn PS PSg): equivalent (P &*& Afalse) Afalse.
Proof.
split.
by red; ins; desf.
by apply false_implies.
Qed.
Lemma false_star PS PSg (P: assn PS PSg): equivalent (Afalse &*& P) Afalse.
Proof.
split.
by red; ins; desf.
by apply false_implies.
Qed.
Lemma equivalent_sim PS PSg (P Q: assn PS PSg) : Asim P Q → equivalent P Q.
Proof.
by split; red; ins; apply (sim_assn_sem H).
Qed.
Lemma equivalent_starC PS PSg (A B: assn PS PSg): equivalent (A &*& B) (B &*& A).
Proof.
apply equivalent_sim, Asim_starC.
Qed.
Lemma equivalent_starA PS PSg (A B C: assn PS PSg): equivalent ((A &*& B) &*& C) (A &*& B &*& C).
Proof.
apply equivalent_sim, Asim_starA.
Qed.
Lemma equivalent_starAC PS PSg (B A C: assn PS PSg): equivalent (A &*& B &*& C) (B &*& A &*& C).
Proof.
apply equivalent_sim, Asim_starAC.
Qed.
Lemma equivalent_star_l PS PSg (P Q R: assn PS PSg) : equivalent P Q → equivalent (Astar P R) (Astar Q R).
Proof.
by ins; rewrite H; apply equivalent_refl.
Qed.
Lemma equivalent_star_r PS PSg (P Q R: assn PS PSg) : equivalent P Q → equivalent (Astar R P) (Astar R Q).
Proof.
by ins; rewrite H; apply equivalent_refl.
Qed.
Lemma equivalent_star PS PSg (P Q P' Q': assn PS PSg):
equivalent P P' → equivalent Q Q' → equivalent (P &*& Q) (P' &*& Q').
Proof.
ins; rewrite H, H0; apply equivalent_refl.
Qed.
Lemma star_emp_l PS PSg (P: assn PS PSg): equivalent P (Aemp &*& P).
Proof.
split.
× red; ins.
repeat eexists; eauto.
eby eapply assn_sem_def.
by rewrite hplus_emp_l.
× red; ins; desf.
by rewrite hplus_emp_l.
Qed.
Lemma star_emp_r PS PSg (P: assn PS PSg): equivalent P (P &*& Aemp).
Proof.
split.
× red; ins.
repeat eexists; eauto.
eby eapply assn_sem_def.
by rewrite hplus_emp_r.
× red; ins; desf.
by rewrite hplus_emp_r.
Qed.
Lemma star_exists PS PSg (P: assn PS PSg) Q:
equivalent (P &*& Aexists Q) (Aexists (fun x ⇒ P &*& Q x)).
Proof.
split; red; ins; desf.
× rewrite assn_sem_exists in *; ins; desf.
eexists _, _; eauto.
× rewrite assn_sem_exists in *; ins; desf.
eexists _, _; do 3 (split; try done).
rewrite assn_sem_exists; eauto.
Qed.
Lemma star_exists2 PS PSg P (Q : assn PS PSg):
equivalent (Aexists P &*& Q) (Aexists (fun x ⇒ P x &*& Q)).
Proof.
rewrite equivalent_starC, star_exists.
split; red; ins; desf; rewrite assn_sem_exists in *; ins; desf;
∃ x, h2, h1; repeat split; try done; apply hplusC.
Qed.
Lemma Arel_split PS PSg x v PP :
@equivalent PS PSg (Arel x PP)
(Astar (Arel x PP) (Arel x (mupd (fun _ ⇒ Afalse) v (PP v)))).
Proof.
split; try by apply Arel_split1.
red; ins; desf.
rewrite hplus_hsingl; ins.
× repeat f_equal; exten; ins; desf.
+ apply AsimD, assn_norm_ok.
rewrite e; unfold mupd; desf; desf.
+ apply AsimD, assn_norm_ok, assn_norm_star_emp.
× split; ins; vauto.
red; ins; unfold mupd; desf; desf; eauto.
Qed.
Lemma Arainit_split PS PSg x :
@equivalent PS PSg (Arainit x)
(Astar (Arainit x) (Arainit x)).
Proof.
split; eauto using Arainit_split1, Arainit_split2.
Qed.
Lemma Arel_duplicate PS PSg x PP :
equivalent (Arel x PP)
(@Astar PS PSg (Arel x PP) (Arel x PP)).
Proof.
split; [by apply Arel_split11 | ].
red; ins; desf.
rewrite hplus_hsingl; ins.
2: by split; ins; vauto.
f_equal; exten; ins; unfold hupd; desf; desf.
f_equal; exten; ins; desf.
rewrite assn_norm_emp; apply AsimD, Asim_star_empD.
split; apply Asim_refl.
Qed.
Lemma Armw_acq_split PS PSg x PP QQ :
(∀ v, QQ v = Aemp ∨ PP v = Afalse ∧ QQ v = Afalse) →
@equivalent PS PSg (Armwacq x PP) (Astar (Armwacq x PP) (Aacq x QQ)).
Proof.
split; eauto using Armw_acq_split1, Armw_acq_split2.
Qed.
Lemma Armw_duplicate PS PSg x PP :
@equivalent PS PSg (Armwacq x PP) (Armwacq x PP &*& Armwacq x PP).
Proof.
split; red; ins; desf.
× eexists _, _; repeat split; try edone.
rewrite hplus_hsingl; ins.
2: by split; ins; vauto.
f_equal; exten; ins; unfold hupd; desf; desf.
× rewrite hplus_hsingl; ins.
2: by split; ins; vauto.
f_equal; exten; ins; unfold hupd; desf; desf.
Qed.
Lemma Aacq_split PS PSg x PP QQ :
@equivalent PS PSg (Aacq x (fun x ⇒ PP x &*& QQ x)) (Aacq x PP &*& Aacq x QQ).
Proof.
split; red; ins; desf; [ eexists _, _ ; repeat split; try edone | ];
rewrite hplus_hsingl; try split; ins; vauto;
f_equal; exten; ins; unfold hupd; desf; ins; f_equal; exten; ins;
apply AsimD; apply Asim_star; apply Asim_norm_l, Asim_refl.
Qed.
Lemma nabla_emp PS PSg: equivalent (Anabla (@Aemp PS PSg)) Aemp.
Proof.
split.
× red; ins; desf.
unfold hemp, Hsim, HFsim, HVsim in *; desf; ins.
f_equal; exten; ins.
specialize (H3 x); desf.
× red; ins; desf. split.
by apply exact_label_emp.
eexists; repeat split; try edone.
by apply Hsim_refl.
by apply exact_label_emp.
Qed.
Lemma triangle_emp PS PSg: equivalent (Atriangle (@Aemp PS PSg)) Aemp.
Proof.
split.
× red; ins; desf.
unfold hemp, Hsim, HFsim, HVsim in *; desf; ins.
f_equal; exten; ins.
specialize (H3 x); desf.
× red; ins; desf. split.
by apply exact_label_emp.
eexists; repeat split; try edone.
by apply Hsim_refl.
by apply exact_label_emp.
Qed.
Lemma triangle_exists PS PSg (P: val → assn PS PSg):
equivalent (Atriangle (Aexists P)) (Aexists (fun x ⇒ Atriangle (P x))).
Proof.
split.
× red. intros h SEM.
apply assn_sem_exists.
ins; desf.
apply assn_sem_exists in SEM0; desf.
eexists; split; try done.
eexists; repeat (split; try edone).
× red. intros h SEM.
apply assn_sem_exists in SEM; desf.
ins; desf.
split; try done.
eexists; split.
eby apply assn_sem_exists; eexists.
eauto.
Qed.
Lemma triangle_star_dist PS PSg (P Q: assn PS PSg):
equivalent (Atriangle (Astar P Q)) (Astar (Atriangle P) (Atriangle Q)).
Proof.
unfold equivalent, implies; split; ins; desf.
{
∃ (lupd h1 HLtriangle), (lupd h2 HLtriangle); repeat (apply conj).
by red in H; desf.
{ rewrite <- lupd_hplus_dist.
eapply exact_label_sim; eauto.
apply lupd_label.
by red in H1; desf.
eapply Hsim_sym, Hsim_trans; eauto.
apply lupd_sim.
red in H1; desf.
}
eby eapply lupd_label, assn_sem_def.
{ eexists;repeat split; try edone.
eby eapply Hsim_sym, lupd_sim, assn_sem_def.
apply exact_label_hplus_dist in H2; desf.
}
eby eapply lupd_label, assn_sem_def.
{
eexists;repeat split; try edone.
eby eapply Hsim_sym, lupd_sim, assn_sem_def.
apply exact_label_hplus_dist in H2; desf.
}
}
{
split.
by apply exact_label_hplus_dist_inv.
assert (S: Hsim (hplus h1 h2) (hplus h'0 h')) by (by apply hplus_sim).
eexists; split.
× eexists _, _; repeat apply conj; try exact H3; try exact H6.
2: edone.
red in S; desf; congruence.
× split; try done.
apply exact_label_hplus_dist_inv; try done.
red in S; desf; congruence.
}
Qed.
Update permission, as most commonly used, i.e.,
both Rel and RMWAcq permision are parametrized by the same invariant.
Definition RMW PS PSg l QQ := @Arel PS PSg l QQ &*& @Armwacq PS PSg l QQ &*& Arainit l.
Lemma RMW_split PS PSg x (QQ: val → assn PS PSg):
equivalent (RMW x QQ) (RMW x QQ &*& RMW x QQ).
Proof.
unfold RMW.
rewrite !equivalent_starA, !(equivalent_starAC (Arel _ _)).
rewrite Arel_duplicate at 1; rewrite equivalent_starA.
do 2 apply equivalent_star_r.
rewrite (equivalent_starAC (Armwacq _ _)).
rewrite Armw_duplicate at 1; rewrite equivalent_starA.
do 2 apply equivalent_star_r.
by apply Arainit_split.
Qed.
Lemma RMW_rel_split PS PSg v l (QQ: val → assn PS PSg):
equivalent (RMW l QQ) (Arel l (mupd (fun _ ⇒ Afalse) v (QQ v)) &*& (RMW l QQ)).
Proof.
unfold RMW.
rewrite <- !equivalent_starA.
repeat apply equivalent_star_l.
rewrite equivalent_starC.
apply Arel_split.
Qed.
Lemma RMW_acq_split PS PSg x (QQ: val → assn PS PSg):
equivalent (RMW x QQ) ((Aacq x (fun _ ⇒ Aemp) &*& Arainit x) &*& RMW x QQ).
Proof.
unfold RMW; rewrite equivalent_starA.
rewrite <- !(equivalent_starAC (Arainit x)), <- Arainit_split.
rewrite (equivalent_starAC (Arel x QQ)).
apply equivalent_star_r.
rewrite <- equivalent_starA, (equivalent_starC (Aacq _ _)), <- Armw_acq_split; eauto.
by apply equivalent_refl.
Qed.
Lemmas about defined connectives
Lemma assn_sem_not PS PSg (P: assn PS PSg) h:
assn_sem (Anot P) h ↔ (h ≠ Hundef ∧ ¬ assn_sem P h).
Proof.
split; ins; desf.
Qed.
Lemma assn_sem_conj PS PSg (P Q: assn PS PSg) h:
assn_sem (Aconj P Q) h ↔ assn_sem P h ∧ assn_sem Q h.
Proof.
unfold Aconj; rewrite assn_sem_not, assn_sem_disj, !assn_sem_not; split; intros; desf.
× apply not_or_and in H0; desf.
apply not_and_or in H0; apply not_and_or in H1; desf.
by split; apply NNPP.
× split; [eby eapply assn_sem_def | intro; desf].
Qed.
This page has been generated by coqdoc