Commit 301abfd3 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Make names for compatibility rules consistent with syntactic rules.

parent 3faf90cb
......@@ -28,21 +28,21 @@ Section compatibility.
Implicit Types A B : sem_ty Σ.
Implicit Types C : sem_ty Σ sem_ty Σ.
Lemma sem_typed_var Γ (x : string) A : Γ !! x = Some A Γ x : A.
Lemma Var_sem_typed Γ (x : string) A : Γ !! x = Some A Γ x : A.
Proof.
iIntros (HΓx vs) "!# #HΓ /=".
iDestruct (env_sem_typed_lookup with "HΓ") as (v ->) "HA"; first done.
by iApply wp_value.
Qed.
Lemma sem_typed_unit Γ : Γ #() : ().
Lemma Unit_sem_typed Γ : Γ #() : ().
Proof. iIntros (vs) "!# _ /=". by iApply wp_value. Qed.
Lemma sem_typed_bool Γ (b : bool) : Γ #b : sem_ty_bool.
Lemma Bool_sem_typed Γ (b : bool) : Γ #b : sem_ty_bool.
Proof. iIntros (vs) "!# _ /=". iApply wp_value. rewrite /sem_ty_car /=. eauto. Qed.
Lemma sem_typed_int Γ (n : Z) : Γ #n : sem_ty_int.
Lemma Int_sem_typed Γ (n : Z) : Γ #n : sem_ty_int.
Proof. iIntros (vs) "!# _ /=". iApply wp_value. rewrite /sem_ty_car /=. eauto. Qed.
Lemma sem_typed_pair Γ e1 e2 A1 A2 :
Lemma Pair_sem_typed Γ e1 e2 A1 A2 :
(Γ e1 : A1) - (Γ e2 : A2) - Γ (e1,e2) : A1 * A2.
Proof.
iIntros "#H1 #H2" (vs) "!# #HΓ /=".
......@@ -50,32 +50,32 @@ Section compatibility.
wp_apply (wp_wand with "(H1 [//])"); iIntros (w1) "#HA1".
wp_pures. iExists w1, w2. auto.
Qed.
Lemma sem_typed_fst Γ e A1 A2 : (Γ e : A1 * A2) - Γ Fst e : A1.
Lemma Fst_sem_typed Γ e A1 A2 : (Γ e : A1 * A2) - Γ Fst e : A1.
Proof.
iIntros "#H" (vs) "!# #HΓ /=".
wp_apply (wp_wand with "(H [//])"); iIntros (w).
iDestruct 1 as (w1 w2 ->) "[??]". by wp_pures.
Qed.
Lemma sem_typed_snd Γ e A1 A2 : (Γ e : A1 * A2) - Γ Snd e : A2.
Lemma Snd_sem_typed Γ e A1 A2 : (Γ e : A1 * A2) - Γ Snd e : A2.
Proof.
iIntros "#H" (vs) "!# #HΓ /=".
wp_apply (wp_wand with "(H [//])"); iIntros (w).
iDestruct 1 as (w1 w2 ->) "[??]". by wp_pures.
Qed.
Lemma sem_typed_injl Γ e A1 A2 : (Γ e : A1) - Γ InjL e : A1 + A2.
Lemma InjL_sem_typed Γ e A1 A2 : (Γ e : A1) - Γ InjL e : A1 + A2.
Proof.
iIntros "#H" (vs) "!# #HΓ /=".
wp_apply (wp_wand with "(H [//])"); iIntros (w) "#HA".
wp_pures. iLeft. iExists w. auto.
Qed.
Lemma sem_typed_injr Γ e A1 A2 : (Γ e : A2) - Γ InjR e : A1 + A2.
Lemma InjR_sem_typed Γ e A1 A2 : (Γ e : A2) - Γ InjR e : A1 + A2.
Proof.
iIntros "#H" (vs) "!# #HΓ /=".
wp_apply (wp_wand with "(H [//])"); iIntros (w) "#HA".
wp_pures. iRight. iExists w. auto.
Qed.
Lemma sem_typed_case Γ e e1 e2 A1 A2 B :
Lemma Case_sem_typed Γ e e1 e2 A1 A2 B :
(Γ e : A1 + A2) - (Γ e1 : A1 B) - (Γ e2 : A2 B) -
Γ Case e e1 e2 : B.
Proof.
......@@ -87,7 +87,7 @@ Section compatibility.
wp_apply (wp_wand with "(H2 [//])"); iIntros (v) "#HAB". by iApply "HAB".
Qed.
Lemma sem_typed_rec Γ f x e A1 A2 :
Lemma Rec_sem_typed Γ f x e A1 A2 :
(binder_insert f (A1 A2)%sem_ty (binder_insert x A1 Γ) e : A2) -
Γ (rec: f x := e) : A1 A2.
Proof.
......@@ -102,7 +102,7 @@ Section compatibility.
by rewrite -delete_insert_ne // -subst_map_insert.
Qed.
Lemma sem_typed_app Γ e1 e2 A1 A2 :
Lemma App_sem_typed Γ e1 e2 A1 A2 :
(Γ e1 : A1 A2) - (Γ e2 : A1) - Γ e1 e2 : A2.
Proof.
iIntros "#H1 #H2" (vs) "!# #HΓ /=".
......@@ -110,23 +110,23 @@ Section compatibility.
wp_apply (wp_wand with "(H1 [//])"); iIntros (v) "#HA". by iApply "HA".
Qed.
Lemma sem_typed_tlam Γ e C : ( A, Γ e : C A) - Γ (Λ: e) : A, C A.
Lemma TLam_sem_typed Γ e C : ( A, Γ e : C A) - Γ (Λ: e) : A, C A.
Proof.
iIntros "#H" (vs) "!# #HΓ /=". wp_pures.
iIntros "!#" (A) "/=". wp_pures. by iApply ("H" $! A).
Qed.
Lemma sem_typed_tapp Γ e C A : (Γ e : A, C A) - Γ e <_> : C A.
Lemma TApp_sem_typed Γ e C A : (Γ e : A, C A) - Γ e <_> : C A.
Proof.
iIntros "#H" (vs) "!# #HΓ /=".
wp_apply (wp_wand with "(H [//])"); iIntros (w) "#HB". by iApply ("HB" $! A).
Qed.
Lemma sem_typed_pack Γ e C A : (Γ e : C A) - Γ e : A, C A.
Lemma Pack_sem_typed Γ e C A : (Γ e : C A) - Γ e : A, C A.
Proof.
iIntros "#H" (vs) "!# #HΓ /=".
wp_apply (wp_wand with "(H [//])"); iIntros (w) "#HB". by iExists A.
Qed.
Lemma sem_typed_unpack Γ x e1 e2 C B :
Lemma Unpack_sem_typed Γ x e1 e2 C B :
(Γ e1 : A, C A) - ( A, binder_insert x (C A) Γ e2 : B) -
Γ (unpack: x := e1 in e2) : B.
Proof.
......@@ -138,7 +138,7 @@ Section compatibility.
auto.
Qed.
Lemma sem_typed_alloc Γ e A : (Γ e : A) - Γ ref e : ref A.
Lemma Alloc_sem_typed Γ e A : (Γ e : A) - Γ ref e : ref A.
Proof.
iIntros "#H" (vs) "!# #HΓ /=".
wp_bind (subst_map _ e). iApply (wp_wand with "(H [//])"); iIntros (w) "HA".
......@@ -147,14 +147,14 @@ Section compatibility.
{ iExists w. iFrame. }
iModIntro. iExists l; auto.
Qed.
Lemma sem_typed_load Γ e A : (Γ e : ref A) - Γ ! e : A.
Lemma Load_sem_typed Γ e A : (Γ e : ref A) - Γ ! e : A.
Proof.
iIntros "#H" (vs) "!# #HΓ /=".
wp_bind (subst_map _ e). iApply (wp_wand with "(H [//])"); iIntros (w).
iDestruct 1 as (l ->) "#?".
iInv (tyN.@l) as (v) "[>Hl HA]". wp_load. eauto 10.
Qed.
Lemma sem_typed_store Γ e1 e2 A :
Lemma Store_sem_typed Γ e1 e2 A :
(Γ e1 : ref A) - (Γ e2 : A) - Γ (e1 <- e2) : ().
Proof.
iIntros "#H1 #H2" (vs) "!# #HΓ /=".
......@@ -162,7 +162,7 @@ Section compatibility.
wp_apply (wp_wand with "(H1 [//])"); iIntros (w1); iDestruct 1 as (l ->) "#?".
iInv (tyN.@l) as (v) "[>Hl _]". wp_store. eauto 10.
Qed.
Lemma sem_typed_faa Γ e1 e2 :
Lemma FAA_sem_typed Γ e1 e2 :
(Γ e1 : ref sem_ty_int) - (Γ e2 : sem_ty_int) - Γ FAA e1 e2 : sem_ty_int.
Proof.
iIntros "#H1 #H2" (vs) "!# #HΓ /=".
......@@ -171,7 +171,7 @@ Section compatibility.
iInv (tyN.@l) as (v) "[>Hl Hv]"; iDestruct "Hv" as (n') "> ->".
wp_faa. iModIntro. eauto 10.
Qed.
Lemma sem_typed_cmpxchg Γ A e1 e2 e3 :
Lemma CmpXchg_sem_typed Γ A e1 e2 e3 :
SemTyUnboxed A
(Γ e1 : ref A) - (Γ e2 : A) - (Γ e3 : A) - Γ CmpXchg e1 e2 e3 : A * sem_ty_bool.
Proof.
......@@ -184,14 +184,14 @@ Section compatibility.
(iSplitL; [by eauto 12 with iFrame | iExists _, _; eauto]).
Qed.
Lemma sem_typed_un_op Γ e op A B :
Lemma UnOp_sem_typed Γ e op A B :
SemTyUnOp op A B (Γ e : A) - Γ UnOp op e : B.
Proof.
intros ?. iIntros "#H" (vs) "!# #HΓ /=".
wp_apply (wp_wand with "(H [//])"); iIntros (v) "#HA".
iDestruct (sem_ty_un_op with "HA") as (w ?) "#HB". by wp_unop.
Qed.
Lemma sem_typed_bin_op Γ e1 e2 op A1 A2 B :
Lemma BinOp_sem_typed Γ e1 e2 op A1 A2 B :
SemTyBinOp op A1 A2 B (Γ e1 : A1) - (Γ e2 : A2) - Γ BinOp op e1 e2 : B.
Proof.
intros. iIntros "#H1 #H2" (vs) "!# #HΓ /=".
......@@ -200,7 +200,7 @@ Section compatibility.
iDestruct (sem_ty_bin_op with "HA1 HA2") as (w ?) "#HB". by wp_binop.
Qed.
Lemma sem_typed_if Γ e e1 e2 B :
Lemma If_sem_typed Γ e e1 e2 B :
(Γ e : sem_ty_bool) - (Γ e1 : B) - (Γ e2 : B) -
Γ (if: e then e1 else e2) : B.
Proof.
......@@ -209,7 +209,7 @@ Section compatibility.
wp_apply (wp_wand with "(H [//])"); iIntros (w). iDestruct 1 as ([]) "->"; by wp_if.
Qed.
Lemma sem_typed_fork Γ e : (Γ e : ()) - Γ Fork e : ().
Lemma Fork_sem_typed Γ e : (Γ e : ()) - Γ Fork e : ().
Proof.
iIntros "#H" (vs) "!# #HΓ /=".
wp_apply wp_fork; last done. by iApply (wp_wand with "(H [//])").
......
......@@ -33,38 +33,38 @@ Section fundamental.
interp_env Γ ρ e : τ ρ.
Proof.
intros Htyped. iInduction Htyped as [] "IH" forall (ρ); simpl in *.
- iApply sem_typed_var. by apply lookup_interp_env.
- iApply sem_typed_unit.
- iApply sem_typed_bool.
- iApply sem_typed_int.
- by iApply sem_typed_pair.
- by iApply sem_typed_fst.
- by iApply sem_typed_snd.
- by iApply sem_typed_injl.
- by iApply sem_typed_injr.
- by iApply sem_typed_case.
- iApply sem_typed_rec. iSpecialize ("IH" $! ρ).
- iApply Var_sem_typed. by apply lookup_interp_env.
- iApply Unit_sem_typed.
- iApply Bool_sem_typed.
- iApply Int_sem_typed.
- by iApply Pair_sem_typed.
- by iApply Fst_sem_typed.
- by iApply Snd_sem_typed.
- by iApply InjL_sem_typed.
- by iApply InjR_sem_typed.
- by iApply Case_sem_typed.
- iApply Rec_sem_typed. iSpecialize ("IH" $! ρ).
by rewrite !interp_env_binder_insert.
- by iApply sem_typed_app.
- iApply sem_typed_tlam; iIntros (A). iSpecialize ("IH" $! (A :: ρ)).
- by iApply App_sem_typed.
- iApply TLam_sem_typed; iIntros (A). iSpecialize ("IH" $! (A :: ρ)).
by rewrite interp_env_ty_lift /=; last lia.
- rewrite interp_ty_subst /=; last lia.
iApply (sem_typed_tapp with "IH").
- iApply sem_typed_pack. iSpecialize ("IH" $! ρ).
iApply (TApp_sem_typed with "IH").
- iApply Pack_sem_typed. iSpecialize ("IH" $! ρ).
by rewrite interp_ty_subst; last lia.
- iApply (sem_typed_unpack with "IH"); iIntros (A).
- iApply (Unpack_sem_typed with "IH"); iIntros (A).
iSpecialize ("IH1" $! (A :: ρ)).
rewrite interp_env_binder_insert.
rewrite interp_env_ty_lift /=; last lia.
by rewrite interp_ty_lift /=; last lia.
- by iApply sem_typed_alloc.
- by iApply sem_typed_load.
- by iApply sem_typed_store.
- by iApply sem_typed_faa.
- by iApply sem_typed_cmpxchg.
- by iApply sem_typed_un_op.
- by iApply sem_typed_bin_op.
- by iApply sem_typed_if.
- by iApply sem_typed_fork.
- by iApply Alloc_sem_typed.
- by iApply Load_sem_typed.
- by iApply Store_sem_typed.
- by iApply FAA_sem_typed.
- by iApply CmpXchg_sem_typed.
- by iApply UnOp_sem_typed.
- by iApply BinOp_sem_typed.
- by iApply If_sem_typed.
- by iApply Fork_sem_typed.
Qed.
End fundamental.
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