primed RrHP, RrTP, RrXP, RrSP

Author: Carmine Abate

Alternative2FR.v

@@ -123,9 +123,9 @@ Proof.
 Qed.
 
 
-Theorem alternative_RrSP : RrSP <-> RrSP_a.
+Theorem alternative_RrSP' : RrSP' <-> RrSP_a.
 Proof.
-  rewrite RrSP_a_contra, <- RrSC_RrSP. 
+  rewrite RrSP_a_contra, <- RrSC_RrSP'. 
   split; intro Hr.
   + intros I ρ δ [Ct Hct].
     specialize (Hr Ct  (fun P m => psem (Ct [P↓]) m) ). 
@@ -314,9 +314,9 @@ Proof.
     exists Cs. now rewrite not_ex_forall_not.
 Qed. 
 
-Theorem alternative_RrHP : RrHP <-> RrHP_a.
+Theorem alternative_RrHP' : RrHP' <-> RrHP_a.
 Proof.
-  rewrite <- RrHC_RrHP, RrHP_a_contra. 
+  rewrite <- RrHC_RrHP', RrHP_a_contra. 
   split; intro Hr.
   + intros I ρ δ [Ct Ht].
     destruct (Hr Ct) as [Cs Hs].

Criteria.v

@@ -450,7 +450,7 @@ Definition RrTC :=
     (forall P, sem tgt (Ct [P↓]) (f P)) ->
     exists Cs, (forall P, sem src (Cs [P]) (f P)).
 
-Lemma RrTC_RrTP : RrTC <-> RrTP.
+Lemma RrTC_RrTP : RrTC <-> RrTP'.
 Proof.
   split.
   - intros HRrTC R. rewrite contra.
@@ -550,9 +550,9 @@ Definition RrSC : Prop :=
     (forall P, spref (f P) (sem tgt (Ct [P↓]))) ->
     exists Cs,  (forall P, spref (f P) (sem src (Cs [P]))).
 
-Theorem RrSC_RrSP : RrSC <-> RrSP.
+Theorem RrSC_RrSP' : RrSC <-> RrSP'.
 Proof.
-  unfold RrSP, RrSC. split.
+  unfold RrSP', RrSC. split.
   - intros h R h0 Ct f h1. specialize (h Ct f h1).
     destruct h as [Cs h]. now apply (h0 Cs f h).
   - intros h Ct f h0. apply NNPP. intros ff.
@@ -665,9 +665,9 @@ Definition RrXC : Prop :=
     (forall P, spref_x (f P) (sem tgt (Ct [P↓]))) ->
     exists Cs,  (forall P, spref_x (f P) (sem src (Cs [P]))).
 
-Theorem RrXC_RrXP : RrXC <-> RrXP.
+Theorem RrXC_RrXP' : RrXC <-> RrXP'.
 Proof.
-  unfold RrXP, RrXC. split.
+  unfold RrXP', RrXC. split.
   - intros h R h0 Ct f h1. specialize (h Ct f h1).
     destruct h as [Cs h]. now apply (h0 Cs f h). 
   - intros h Ct f h0. apply NNPP. intros ff.
@@ -725,9 +725,9 @@ Qed.
 Definition RrHC : Prop :=
   forall Ct, exists Cs,  (forall P, sem src (Cs [P]) = sem tgt (Ct [P ↓])).
 
-Theorem RrHC_RrHP : RrHC <-> RrHP.
+Theorem RrHC_RrHP' : RrHC <-> RrHP'.
 Proof.
-  unfold RrHP, RrHC. split.
+  unfold RrHP', RrHC. split.
   - intros h R hcs Ct. destruct (h Ct) as [Cs h0]; clear h.
     specialize (hcs Cs).
     assert (hh :  (fun P : par src => sem src (Cs [P])) =

Robustdef.v

@@ -233,7 +233,7 @@ Qed.
 (** *Robust Preservation of arbitrary-Relational Properties *)
 
 
-Definition RrTP : Prop :=
+Definition RrTP' : Prop :=
   forall R : (par src  ->  trace) -> Prop,
     (forall Cs f,  (forall P, sem src (Cs [P]) (f P)) -> R f) ->
     (forall Ct f,  (forall P, sem tgt (Ct [P↓]) (f P)) -> R f). 
@@ -274,7 +274,7 @@ Qed.
 
 (** *Robust Preservation of arbitrary Relational Safety Properties*)
 
-Definition RrSP : Prop :=
+Definition RrSP' : Prop :=
   forall R : (par src -> (finpref -> Prop)) -> Prop,
      (forall Cs f, (forall P, spref (f P) (sem src (Cs [P]))) -> R f) ->
      (forall Ct f, (forall P, spref (f P) (sem tgt (Ct [P↓]))) -> R f).
@@ -311,7 +311,7 @@ Qed.
 
 (** *Robust Preservation of arbitrary Relational XSafety Properties*)
 
-Definition RrXP : Prop :=
+Definition RrXP' : Prop :=
   forall R : (par src -> (xpref -> Prop)) -> Prop,
      (forall Cs f, (forall P, spref_x (f P) (sem src (Cs [P]))) -> R f) ->
      (forall Ct f, (forall P, spref_x (f P) (sem tgt (Ct [P↓]))) -> R f).
@@ -325,7 +325,7 @@ Definition R2rHP : Prop :=
 
 (** *Robust Preservation of arbitrary Relational HyperProperties*)
 
-Definition RrHP : Prop :=
+Definition RrHP' : Prop :=
   forall R : (par src  ->  prop) -> Prop,
     (forall Cs, R (fun P  => sem src (Cs [ P] ) )) ->
     (forall Ct, R (fun P  => sem tgt (Ct [ (P ↓)]) )).