Require Import Vbase List Classical ClassicalDescription.
Require Import permission GpsSepAlg.
Require Import fslassn fslassnsem fslmodel.
Require Import fslassnlemmas fslassnlemmas2.
Set Implicit Arguments.
Separating the normal and non-normal parts of cooompound labels:
Definition normalize_lbl lbl :=
match lbl with
| Some HLCnormal | Some HLCtriangledot | Some HLCnabladot | Some HLCdiamonddot ⇒ Some HLCnormal
| Some HLCtriangle | Some HLCnabla | Some HLCdiamond ⇒ None
| None ⇒ None
end.
Definition denormalize_lbl lbl :=
match lbl with
| Some HLCnormal ⇒ None
| Some HLCtriangle | Some HLCtriangledot ⇒ Some HLCtriangle
| Some HLCnabla | Some HLCnabladot ⇒ Some HLCnabla
| Some HLCdiamond | Some HLCdiamonddot ⇒ Some HLCdiamond
| None ⇒ None
end.
Lemma label_split lbl: lbl = ohlplus (normalize_lbl lbl) (denormalize_lbl lbl).
Lemma normalize_lbl_dist lbl1 lbl2 :
normalize_lbl (ohlplus lbl1 lbl2) = ohlplus (normalize_lbl lbl1) (normalize_lbl lbl2).
Separating the normal and non-normal parts of the heap:
Program Definition normalize_hv PS PSg (hv : HeapVal PS PSg) : HeapVal PS PSg:=
match hv with
| HVnone ⇒ HVnone
| HVuval lbl ⇒
match excluded_middle_informative (lbl = HLnormal) return HeapVal PS PSg with
| left _ ⇒ HVuval lbl
| right _ ⇒ HVnone
end
| HVval v Perm pNormal pTriangle pNabla _
⇒ match excluded_middle_informative (pNormal ≠ Pzero Perm) return HeapVal PS PSg with
| left _ ⇒ HVval v Perm pNormal (Pzero Perm) (Pzero Perm) _
| right _ ⇒ HVnone
end
| HVra PP QQ isrmw permlbl initlbl
⇒ HVra PP QQ isrmw (normalize_lbl permlbl) (normalize_lbl initlbl)
end.
Program Definition denormalize_hv PS PSg (hv : HeapVal PS PSg) : HeapVal PS PSg:=
match hv with
| HVnone ⇒ HVnone
| HVuval lbl ⇒
match excluded_middle_informative (lbl = HLnormal) return HeapVal PS PSg with
| left _ ⇒ HVnone
| right _ ⇒ HVuval lbl
end
| HVval v Perm pNormal pTriangle pNabla _
⇒ match excluded_middle_informative (pTriangle ## pNabla ≠ Pzero Perm) return HeapVal PS PSg with
| left _ ⇒ HVval v Perm (Pzero Perm) pTriangle pNabla _
| right _ ⇒ HVnone
end
| HVra PP QQ isrmw permlbl initlbl
⇒ if isrmw
then HVra PP QQ isrmw (denormalize_lbl permlbl) (denormalize_lbl initlbl)
else HVra PP Remp isrmw (denormalize_lbl permlbl) (denormalize_lbl initlbl)
end.
Definition normal_part PS PSg (h : heap PS PSg) :=
match h with
| Hundef ⇒ Hundef
| Hdef hf hfg ⇒ Hdef (fun x ⇒ normalize_hv (hf x)) hfg
end.
Definition triangled_part PS PSg (h : heap PS PSg) :=
match h with
| Hundef ⇒ Hundef
| Hdef hf hfg ⇒ Hdef (fun x ⇒ denormalize_hv (hf x)) gres_emp
end.
Heap splits into normal and non-normal part.
Normal part of a sum is the sum of normal parts.
Lemma normal_part_hplus_dist PS PSg (h1 h2 : heap PS PSg):
h1 +!+ h2 ≠ Hundef → normal_part (h1 +!+ h2) = normal_part h1 +!+ normal_part h2.
Normal part really is labeled by only normal label.
Lemma normal_part_is_normal PS PSg (h : heap PS PSg):
h ≠ Hundef → HlabeledExact (normal_part h) HLnormal.
Opaque Aexists Aconj Adisj.
Inductive modality_free_positive PS PSg : (assn PS PSg) → Prop :=
| MFPtrue: modality_free_positive Atrue
| MFPemp: modality_free_positive Aemp
| MFPpt: ∀ Perm psIN p OK E E', modality_free_positive (Apt Perm psIN p OK E E')
| MFPptu: ∀ E, modality_free_positive (Aptu E)
| MFPrainit: ∀ E, modality_free_positive (Arainit E)
| MFPrel: ∀ E Q, modality_free_positive (Arel E Q)
| MFPacq: ∀ E Q, modality_free_positive (Aacq E Q)
| MFPrmwacq: ∀ E Q, modality_free_positive (Armwacq E Q)
| MFPghost: ∀ PCM pcmIN E g, modality_free_positive (Aghost PCM pcmIN E g)
| MPFconj: ∀ P Q, modality_free_positive P → modality_free_positive Q
→ modality_free_positive (Aconj P Q)
| MFPdisj: ∀ P Q, modality_free_positive P → modality_free_positive Q
→ modality_free_positive (Adisj P Q)
| MFPstar: ∀ P Q, modality_free_positive P → modality_free_positive Q
→ modality_free_positive (Astar P Q)
| MFPforall: ∀ PP, (∀ x, modality_free_positive (PP x))
→ modality_free_positive (Aforall PP)
| MFPexists: ∀ PP, (∀ x, modality_free_positive (PP x))
→ modality_free_positive (Aexists PP).
Modality-free positive assertions talk only about the normal part of the heap.
Lemma MFPassn_cares_only_about_normal_part PS PSg (F: assn PS PSg) (MFP: modality_free_positive F) h :
assn_sem F h → assn_sem F (normal_part h).
Main theorem: modality-free positive assertions are normalizable.
This page has been generated by coqdoc