From f6cca3e1fa9c35b5580846fce5dd42006cfaec86 Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Thu, 31 Jan 2019 16:07:13 +0100
Subject: [PATCH] A reasonable-ish version of the fundamental lemma
---
theories/logic/model.v | 7 +++
theories/typing/fundamental.v | 80 +++++++++++++++--------------------
theories/typing/interp.v | 5 +++
theories/typing/types.v | 13 +++---
4 files changed, 53 insertions(+), 52 deletions(-)
diff --git a/theories/logic/model.v b/theories/logic/model.v
index 7dcfb67..5dfc08b 100644
--- a/theories/logic/model.v
+++ b/theories/logic/model.v
@@ -63,6 +63,10 @@ Section semtypes.
Proper ((=) ==> (=) ==> dist n ==> dist n) (interp_expr E).
Proof. solve_proper. Qed.
+ Global Instance interp_expr_proper E e e' :
+ Proper ((≡) ==> (≡)) (interp_expr E e e').
+ Proof. apply ne_proper=>n. by apply interp_expr_ne. Qed.
+
Definition lty2_unit : lty2 := Lty2 (λ w1 w2, ⌜ w1 = #() ∧ w2 = #() âŒ%I).
Definition lty2_bool : lty2 := Lty2 (λ w1 w2, ∃ b : bool, ⌜ w1 = #b ∧ w2 = #b âŒ)%I.
Definition lty2_int : lty2 := Lty2 (λ w1 w2, ∃ n : Z, ⌜ w1 = #n ∧ w2 = #n âŒ)%I.
@@ -119,6 +123,9 @@ Section semtypes.
apply lty2_car_ne; eauto.
Qed.
+ Lemma lty_rec_unfold (C : lty2C -n> lty2C) : lty2_rec C ≡ lty2_rec1 C (lty2_rec C).
+ Proof. apply fixpoint_unfold. Qed.
+
End semtypes.
(* Nice notations *)
diff --git a/theories/typing/fundamental.v b/theories/typing/fundamental.v
index 5e1137c..fe5b2c6 100644
--- a/theories/typing/fundamental.v
+++ b/theories/typing/fundamental.v
@@ -6,6 +6,7 @@ From reloc.logic.proofmode Require Export tactics spec_tactics.
From reloc.typing Require Export interp.
From iris.proofmode Require Export tactics.
+From Autosubst Require Import Autosubst.
Section fundamental.
Context `{relocG Σ}.
@@ -381,9 +382,6 @@ Section fundamental.
destruct op; inversion Hopv'; simplify_eq/=; eauto.
Qed.
- (* TODO *)
-
- From Autosubst Require Import Autosubst.
Lemma bin_log_related_tapp' Δ Γ e e' τ τ' :
({Δ;Γ} ⊨ e ≤log≤ e' : TForall τ) -∗
{Δ;Γ} ⊨ (TApp e) ≤log≤ (TApp e') : τ.[τ'/].
@@ -394,52 +392,53 @@ Section fundamental.
rel_bind_ap e e' "IH" v v' "IH".
iDestruct ("IH" $! (interp τ' Δ)) as "#IH".
iApply refines_ret'; auto.
- admit.
- Admitted.
+ by rewrite -interp_subst.
+ Qed.
-(*
- Lemma bin_log_related_tapp (τi : D) Δ Γ e e' τ :
- {Δ;Γ} ⊨ e ≤log≤ e' : TForall τ -∗
- {τi::Δ;⤉Γ} ⊨ TApp e ≤log≤ TApp e' : τ.
+ Lemma bin_log_related_tapp (τi : lty2) Δ Γ e e' τ :
+ ({Δ;Γ} ⊨ e ≤log≤ e' : TForall τ) -∗
+ {τi::Δ;⤉Γ} ⊨ (TApp e) ≤log≤ (TApp e') : τ.
Proof.
- rewrite bin_log_related_eq.
+ rewrite /bin_log_related refines_eq.
iIntros "IH".
iIntros (vvs Ï) "#Hs #HΓ"; iIntros (j K) "Hj /=".
- wp_bind (env_subst _ e).
- tp_bind j (env_subst _ e').
+ iModIntro. wp_bind (subst_map _ e).
+ tp_bind j (subst_map _ e').
iSpecialize ("IH" with "Hs [HΓ] Hj").
- { by rewrite interp_env_ren. }
- iMod "IH" as "IH /=". iModIntro.
+ { by rewrite interp_ren. }
+ iMod "IH" as "IH /=".
iApply (wp_wand with "IH").
iIntros (v). iDestruct 1 as (v') "[Hj #IH]".
iMod ("IH" $! Ï„i with "Hj"); auto.
Qed.
- Lemma bin_log_related_fold Δ Γ e e' τ :
- {Δ;Γ} ⊨ e ≤log≤ e' : τ.[(TRec τ)/] -∗
- {Δ;Γ} ⊨ Fold e ≤log≤ Fold e' : TRec τ.
+ Lemma bin_log_related_unfold Δ Γ e e' τ :
+ ({Δ;Γ} ⊨ e ≤log≤ e' : TRec τ) -∗
+ {Δ;Γ} ⊨ rec_unfold e ≤log≤ rec_unfold e' : τ.[(TRec τ)/].
Proof.
iIntros "IH".
rel_bind_ap e e' "IH" v v' "IH".
- value_case.
- rewrite fixpoint_unfold /= -interp_subst.
- iExists (_, _); eauto.
+ iEval (rewrite lty_rec_unfold /lty2_car /=) in "IH".
+ change (lty2_rec _) with (interp (TRec τ) Δ).
+ unfold rec_unfold. unlock. (* TODO WHY?????? *)
+ rel_pure_l. rel_pure_r.
+ value_case. by rewrite -interp_subst.
Qed.
- Lemma bin_log_related_unfold Δ Γ e e' τ :
- {Δ;Γ} ⊨ e ≤log≤ e' : TRec τ -∗
- {Δ;Γ} ⊨ Unfold e ≤log≤ Unfold e' : τ.[(TRec τ)/].
+ Lemma bin_log_related_fold Δ Γ e e' τ :
+ ({Δ;Γ} ⊨ e ≤log≤ e' : τ.[(TRec τ)/]) -∗
+ {Δ;Γ} ⊨ e ≤log≤ e' : TRec τ.
Proof.
iIntros "IH".
rel_bind_ap e e' "IH" v v' "IH".
- rewrite /= fixpoint_unfold /=.
- change (fixpoint _) with (interp ⊤ (TRec τ) Δ).
- iDestruct "IH" as ([w w']) "#[% Hiz]"; simplify_eq/=.
- rel_unfold_l.
- rel_unfold_r.
- value_case. by rewrite -interp_subst.
+ value_case.
+ iModIntro.
+ iEval (rewrite lty_rec_unfold /lty2_car /=).
+ change (lty2_rec _) with (interp (TRec τ) Δ).
+ by rewrite -interp_subst.
Qed.
+(*
Lemma bin_log_related_pack' Δ Γ e e' τ τ' :
{Δ;Γ} ⊨ e ≤log≤ e' : τ.[τ'/] -∗
{Δ;Γ} ⊨ Pack e ≤log≤ Pack e' : TExists τ.
@@ -501,7 +500,7 @@ Section fundamental.
rewrite (interp_weaken [] [τi] Δ _ τ2) /=.
eauto.
Qed.
-
+*)
Theorem binary_fundamental Δ Γ e τ :
Γ ⊢ₜ e : τ → ({Δ;Γ} ⊨ e ≤log≤ e : τ)%I.
@@ -521,30 +520,19 @@ Section fundamental.
- by iApply bin_log_related_injr.
- by iApply (bin_log_related_case with "[] []").
- by iApply (bin_log_related_if with "[] []").
- - assert (Closed (x :b: f :b: dom (gset string) Γ) e).
- { apply typed_X_closed in Ht.
- rewrite !dom_insert_binder in Ht.
- revert Ht. destruct x,f; cbn-[union];
- (* TODO: why is simple rewriting is not sufficient here? *)
- erewrite ?(left_id ∅); eauto.
- all: apply _. }
- iApply (bin_log_related_rec with "[]"); eauto.
+ - iApply (bin_log_related_rec with "[]"); eauto.
- by iApply (bin_log_related_app with "[] []").
- - assert (Closed (dom _ Γ) e).
- { apply typed_X_closed in Ht.
- pose (K:=(dom_fmap (asubst (ren (+1))) Γ (D:=stringset))).
- fold_leibniz. by rewrite -K. }
- iApply bin_log_related_tlam; eauto.
+ - iApply bin_log_related_tlam; eauto.
- by iApply bin_log_related_tapp'.
- by iApply bin_log_related_fold.
- by iApply bin_log_related_unfold.
- - by iApply bin_log_related_pack'.
- - iApply (bin_log_related_unpack with "[]"); eauto.
+ (* - by iApply bin_log_related_pack'. *)
+ (* - iApply (bin_log_related_unpack with "[]"); eauto. *)
- by iApply bin_log_related_fork.
- by iApply bin_log_related_alloc.
- by iApply bin_log_related_load.
- by iApply (bin_log_related_store with "[]").
- by iApply (bin_log_related_CAS with "[] []").
Qed.
-*)
+
End fundamental.
diff --git a/theories/typing/interp.v b/theories/typing/interp.v
index 2d79b91..00e4fa5 100644
--- a/theories/typing/interp.v
+++ b/theories/typing/interp.v
@@ -169,4 +169,9 @@ Section interp_ren.
destruct (Γ !! x); auto; simpl. f_equiv.
symmetry. apply (interp_ren_up []).
Qed.
+
+ Lemma interp_subst Δ2 τ τ' :
+ interp τ (interp τ' Δ2 :: Δ2) ≡ interp (τ.[τ'/]) Δ2.
+ Proof. Admitted.
+
End interp_ren.
diff --git a/theories/typing/types.v b/theories/typing/types.v
index 2dad64f..450dc50 100644
--- a/theories/typing/types.v
+++ b/theories/typing/types.v
@@ -116,7 +116,7 @@ Inductive typed (Γ : stringmap type) : expr → type → Prop :=
| If_typed e0 e1 e2 Ï„ :
Γ ⊢ₜ e0 : TBool → Γ ⊢ₜ e1 : τ → Γ ⊢ₜ e2 : τ → Γ ⊢ₜ If e0 e1 e2 : τ
| Rec_typed f x e Ï„1 Ï„2 :
- <[x:=τ1]>(<[f:=TArrow τ1 τ2]>Γ) ⊢ₜ e : τ2 →
+ <[f:=TArrow τ1 τ2]>(<[x:=τ1]>Γ) ⊢ₜ e : τ2 →
Γ ⊢ₜ Rec f x e : TArrow τ1 τ2
| App_typed e1 e2 Ï„1 Ï„2 :
Γ ⊢ₜ e1 : TArrow τ1 τ2 → Γ ⊢ₜ e2 : τ1 → Γ ⊢ₜ App e1 e2 : τ2
@@ -127,16 +127,17 @@ Inductive typed (Γ : stringmap type) : expr → type → Prop :=
Γ ⊢ₜ e #() : τ.[τ'/]
| TFold e τ : Γ ⊢ₜ e : τ.[TRec τ/] → Γ ⊢ₜe : TRec τ
| TUnfold e τ : Γ ⊢ₜ e : TRec τ → Γ ⊢ₜ rec_unfold e : τ.[TRec τ/]
- | TPack e τ τ' : Γ ⊢ₜ e : τ.[τ'/] → Γ ⊢ₜ e : TExists τ
- | TUnpack e1 e2 τ τ2 : Γ ⊢ₜ e1 : TExists τ →
- (subst (ren (+1%nat)) <$> Γ) ⊢ₜ e2 : TArrow τ (subst (ren (+1%nat)) τ2) →
- Γ ⊢ₜ unpack e1 e2 : τ2
+ (* | TPack e τ τ' : Γ ⊢ₜ e : τ.[τ'/] → Γ ⊢ₜ e : TExists τ *)
+ (* | TUnpack e1 e2 τ τ2 : Γ ⊢ₜ e1 : TExists τ → *)
+ (* (subst (ren (+1%nat)) <$> Γ) ⊢ₜ e2 : TArrow τ (subst (ren (+1%nat)) τ2) → *)
+ (* Γ ⊢ₜ unpack e1 e2 : τ2 *)
| TFork e : Γ ⊢ₜ e : TUnit → Γ ⊢ₜ Fork e : TUnit
| TAlloc e τ : Γ ⊢ₜ e : τ → Γ ⊢ₜ Alloc e : Tref τ
| TLoad e τ : Γ ⊢ₜ e : Tref τ → Γ ⊢ₜ Load e : τ
| TStore e e' τ : Γ ⊢ₜ e : Tref τ → Γ ⊢ₜ e' : τ → Γ ⊢ₜ Store e e' : TUnit
| TCAS e1 e2 e3 Ï„ :
- EqType τ → Γ ⊢ₜ e1 : Tref τ → Γ ⊢ₜ e2 : τ → Γ ⊢ₜ e3 : τ →
+ EqType τ → UnboxedType τ →
+ Γ ⊢ₜ e1 : Tref τ → Γ ⊢ₜ e2 : τ → Γ ⊢ₜ e3 : τ →
Γ ⊢ₜ CAS e1 e2 e3 : TBool
where "Γ ⊢ₜ e : τ" := (typed Γ e τ).
--
GitLab