Commit 2d4a91cb authored by Dan Frumin's avatar Dan Frumin

Common root for the specN and rootN namespaces

parent 80dd7f76
......@@ -29,13 +29,12 @@ Section compatibility.
Context `{logrelG Σ}.
Lemma bin_log_related_par Δ Γ E e1 e2 e1' e2' τ1 τ2 :
specN E
logN E
logrelN E
{E,E;Δ;Γ} e1 log e1' : TArrow TUnit τ1 -
{E,E;Δ;Γ} e2 log e2' : TArrow TUnit τ2 -
{E,E;Δ;Γ} par e1 e2 log par e1' e2' : TProd τ1 τ2.
Proof.
iIntros (??) "He1 He2".
iIntros (?) "He1 He2".
iApply (bin_log_related_app with "[He1] He2").
iApply (bin_log_related_app with "[] He1").
iApply binary_fundamental_masked; eauto with typeable.
......
......@@ -87,7 +87,7 @@ Section masked.
Qed.
Lemma bin_log_related_fst Δ Γ e e' τ1 τ2 :
specN E
logrelN E
{E,E;Δ;Γ} e log e' : TProd τ1 τ2 -
{E,E;Δ;Γ} Fst e log Fst e' : τ1.
Proof.
......@@ -104,7 +104,7 @@ Section masked.
Qed.
Lemma bin_log_related_snd Δ Γ e e' τ1 τ2 :
specN E
logrelN E
{E,E;Δ;Γ} e log e' : TProd τ1 τ2 -
{E,E;Δ;Γ} Snd e log Snd e' : τ2.
Proof.
......@@ -210,7 +210,7 @@ Section masked.
Qed.
Lemma bin_log_related_injl Δ Γ e e' τ1 τ2 :
specN E
logrelN E
{E,E;Δ;Γ} e log e' : τ1 -
{E,E;Δ;Γ} InjL e log InjL e' : (TSum τ1 τ2).
Proof.
......@@ -224,7 +224,7 @@ Section masked.
Qed.
Lemma bin_log_related_injr Δ Γ e e' τ1 τ2 :
specN E
logrelN E
{E,E;Δ;Γ} e log e' : τ2 -
{E,E;Δ;Γ} InjR e log InjR e' : TSum τ1 τ2.
Proof.
......@@ -238,7 +238,7 @@ Section masked.
Qed.
Lemma bin_log_related_case Δ Γ e0 e1 e2 e0' e1' e2' τ1 τ2 τ3 :
specN E
logrelN E
{E,E;Δ;Γ} e0 log e0' : TSum τ1 τ2 -
{E,E;Δ;Γ} e1 log e1' : TArrow τ1 τ3 -
{E,E;Δ;Γ} e2 log e2' : TArrow τ2 τ3 -
......@@ -275,7 +275,7 @@ Section masked.
Qed.
Lemma bin_log_related_if Δ Γ e0 e1 e2 e0' e1' e2' τ :
specN E
logrelN E
{E,E;Δ;Γ} e0 log e0' : TBool -
{E,E;Δ;Γ} e1 log e1' : τ -
{E,E;Δ;Γ} e2 log e2' : τ -
......@@ -295,7 +295,7 @@ Section masked.
Qed.
Lemma bin_log_related_nat_binop Δ Γ op e1 e2 e1' e2' τ :
specN E
logrelN E
binop_nat_res_type op = Some τ
{E,E;Δ;Γ} e1 log e1' : TNat -
{E,E;Δ;Γ} e2 log e2' : TNat -
......@@ -318,7 +318,7 @@ Section masked.
Qed.
Lemma bin_log_related_bool_binop Δ Γ op e1 e2 e1' e2' τ :
specN E
logrelN E
binop_bool_res_type op = Some τ
{E,E;Δ;Γ} e1 log e1' : TBool -
{E,E;Δ;Γ} e2 log e2' : TBool -
......@@ -343,7 +343,7 @@ Section masked.
Lemma bin_log_related_tlam Δ Γ e e' τ :
Closed (dom _ Γ) e
Closed (dom _ Γ) e'
specN E
logrelN E
( (τi : D), ⌜∀ ww, PersistentP (τi ww) ({E,E;(τi::Δ);Autosubst_Classes.subst (ren (+1)) <$> Γ} e log e' : τ)) -
{E,E;Δ;Γ} TLam e log TLam e' : TForall τ.
Proof.
......@@ -420,7 +420,7 @@ Section masked.
Qed.
Lemma bin_log_related_unfold Δ Γ e e' τ :
specN E
logrelN E
{E,E;Δ;Γ} e log e' : TRec τ -
{E,E;Δ;Γ} Unfold e log Unfold e' : τ.[(TRec τ)/].
Proof.
......@@ -473,7 +473,7 @@ Section masked.
Qed.
Lemma bin_log_related_unpack Δ Γ e1 e1' e2 e2' τ τ2
(Hmasked : specN E) :
(Hmasked : logrelN E) :
{E,E;Δ;Γ} e1 log e1' : TExists τ -
( (τi : D), ⌜∀ ww, PersistentP (τi ww) {E,E;τi::Δ;Autosubst_Classes.subst (ren (+1)) <$> Γ} e2 log e2' : TArrow τ (Autosubst_Classes.subst (ren (+1)) τ2)) -
{E,E;Δ;Γ} Unpack e1 e2 log Unpack e1' e2' : τ2.
......@@ -504,7 +504,7 @@ Section masked.
Qed.
Lemma bin_log_related_fork Δ Γ e e' :
specN E
logrelN E
{E,E;Δ;Γ} e log e' : TUnit -
{E,E;Δ;Γ} Fork e log Fork e' : TUnit.
Proof.
......@@ -522,7 +522,7 @@ Section masked.
Qed.
Lemma bin_log_related_alloc Δ Γ e e' τ :
specN E
logrelN E
{E,E;Δ;Γ} e log e' : τ -
{E,E;Δ;Γ} Alloc e log Alloc e' : Tref τ.
Proof.
......@@ -543,13 +543,12 @@ Section masked.
Qed.
Lemma bin_log_related_load Δ Γ e e' τ :
specN E
logN E
logrelN E
{E,E;Δ;Γ} e log e' : (Tref τ) -
{E,E;Δ;Γ} Load e log Load e' : τ.
Proof.
rewrite bin_log_related_eq.
iIntros (??) "IH".
iIntros (?) "IH".
iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
smart_bind j (env_subst _ e) (env_subst _ e') "IH" v v' "IH".
iDestruct "IH" as ([l l']) "[% Hinv]"; simplify_eq/=.
......@@ -565,14 +564,13 @@ Section masked.
Qed.
Lemma bin_log_related_store Δ Γ e1 e2 e1' e2' τ :
specN E
logN E
logrelN E
{E,E;Δ;Γ} e1 log e1' : (Tref τ) -
{E,E;Δ;Γ} e2 log e2' : τ -
{E,E;Δ;Γ} Store e1 e2 log Store e1' e2' : TUnit.
Proof.
rewrite bin_log_related_eq.
iIntros (??) "IH1 IH2".
iIntros (?) "IH1 IH2".
iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
smart_bind j (env_subst _ e1) (env_subst _ e1') "IH1" v v' "IH1".
smart_bind j (env_subst _ e2) (env_subst _ e2') "IH2" w w' "#IH2".
......@@ -590,15 +588,14 @@ Section masked.
Lemma bin_log_related_CAS Δ Γ e1 e2 e3 e1' e2' e3' τ
(HEqτ : EqType τ) :
specN E
logN E
logrelN E
{E,E;Δ;Γ} e1 log e1' : Tref τ -
{E,E;Δ;Γ} e2 log e2' : τ -
{E,E;Δ;Γ} e3 log e3' : τ -
{E,E;Δ;Γ} CAS e1 e2 e3 log CAS e1' e2' e3' : TBool.
Proof.
rewrite bin_log_related_eq.
iIntros (??) "IH1 IH2 IH3".
iIntros (?) "IH1 IH2 IH3".
iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
smart_bind j (env_subst _ e1) (env_subst _ e1') "IH1" v v' "IH1".
smart_bind j (env_subst _ e2) (env_subst _ e2') "IH2" w w' "#IH2".
......@@ -630,11 +627,10 @@ Section masked.
Qed.
Theorem binary_fundamental_masked Δ Γ e τ :
specN E
logN E
logrelN E
Γ ⊢ₜ e : τ ({E,E;Δ;Γ} e log e : τ)%I.
Proof.
intros HspecN HlogN Ht. iInduction Ht as [] "IH" forall (Δ).
intros HlogN Ht. iInduction Ht as [] "IH" forall (Δ).
- by iApply bin_log_related_var.
- iApply bin_log_related_unit.
- by iApply bin_log_related_nat.
......
......@@ -34,7 +34,7 @@ Ltac solve_proper ::=
(solve_proper_unfold + idtac);
solve [repeat first [eassumption | auto_equiv] ].
Definition logN : namespace := nroot .@ "logN".
Definition logN : namespace := logrelN .@ "logN".
(** interp : is a unary logical relation. *)
Section logrel.
......
......@@ -5,7 +5,8 @@ From iris_logrel.F_mu_ref_conc Require Export rules notation.
From iris.proofmode Require Import tactics.
Import uPred.
Definition specN := nroot .@ "spec".
Definition logrelN := nroot .@ "logrel".
Definition specN := logrelN .@ "spec".
(** The CMRA for the heap of the specification. *)
Definition tpoolUR : ucmraT := gmapUR nat (exclR exprC).
......
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