From 3ba684d7a8d860864cb995b816961867732c76de Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Dani=C3=ABl=20Louwrink?= <daniel.louwrink@gmail.com>
Date: Tue, 21 Apr 2020 18:19:51 +0200
Subject: [PATCH] add copy-, fix arrow typing rule
---
theories/logrel/copying.v | 95 +++++++++++++++++++++++++++++++++++--
theories/logrel/ltyping.v | 47 ------------------
theories/logrel/subtyping.v | 6 +++
theories/logrel/types.v | 24 ++--------
4 files changed, 99 insertions(+), 73 deletions(-)
diff --git a/theories/logrel/copying.v b/theories/logrel/copying.v
index ae11d94..79bc1a6 100644
--- a/theories/logrel/copying.v
+++ b/theories/logrel/copying.v
@@ -1,22 +1,34 @@
-From actris.logrel Require Import types subtyping.
+From actris.logrel Require Import ltyping types subtyping.
From actris.channel Require Import channel.
From iris.base_logic.lib Require Import invariants.
From iris.proofmode Require Import tactics.
-From iris.heap_lang Require Import proofmode.
+From iris.heap_lang Require Import notation proofmode.
+From iris.bi.lib Require Export core.
+
+(* TODO: Coq fails to infer what the Σ should be if I move some of these
+definitions out of the section or into a different section with its own Context
+declaration. *)
Section copying.
Context `{heapG Σ, chanG Σ}.
Implicit Types A : lty Σ.
Implicit Types S : lsty Σ.
+ (* We define the copyability of semantic types in terms of subtyping. *)
Definition copyable (A : lty Σ) : iProp Σ :=
A <: copy A.
- (* Subtyping for `copy` *)
+ (* Subtyping for `copy` and `copy-` *)
Lemma lty_le_copy A :
⊢ copy A <: A.
Proof. by iIntros (v) "!> #H". Qed.
+ Lemma lty_le_copy_minus A :
+ copyable A -∗ copy- A <: A.
+ Proof.
+ iIntros "#HA". iIntros (v) "!> #Hv".
+ Admitted.
+
(* Copyability of types *)
Lemma lty_unit_copyable :
⊢ copyable ().
@@ -35,6 +47,10 @@ Section copying.
⊢ copyable (copy A).
Proof. iIntros (v) "!> #Hv !>". iFrame "Hv". Qed.
+ Lemma lty_copyminus_copyable A :
+ ⊢ copyable (copy- A).
+ Proof. iIntros (v) "!> #Hv !>". iFrame "Hv". Qed.
+
Lemma lty_any_copyable :
⊢ copyable any.
Proof. iIntros (v) "!> #Hv !>". iFrame "Hv". Qed.
@@ -47,7 +63,7 @@ Section copying.
⊢ copyable (mutex A).
Proof. iIntros (v) "!> #Hv !>". iFrame "Hv". Qed.
- (* Commuting rules for `copy` and other type formers *)
+ (* Rules about combining `copy` and other type formers *)
Lemma lty_prod_copy_comm A B :
⊢ copy A * copy B <:> copy (A * B).
Proof.
@@ -87,7 +103,76 @@ Section copying.
iIntros (v) "!> Hv".
rewrite /lty_rec {2}fixpoint_unfold.
(* iEval (rewrite fixpoint_unfold) *)
- (* Rewriting goes crazy here *)
+ (* TODO: Rewriting goes crazy here *)
Admitted.
+ (* TODO: Get rid of side condition that x does not appear in Γ *)
+ Lemma env_split_copy Γ Γ1 Γ2 (x : string) A:
+ Γ !! x = None →
+ copyable A -∗
+ env_split Γ Γ1 Γ2 -∗
+ env_split (<[x:=A]> Γ) (<[x:=A]> Γ1) (<[x:=A]> Γ2).
+ Proof.
+ iIntros (HΓx) "#Hcopy #Hsplit". iIntros (vs) "!> HΓ".
+ iPoseProof (big_sepM_insert with "HΓ") as "[Hv HΓ]"; first by assumption.
+ iDestruct "Hv" as (v ?) "HA". iDestruct ("Hcopy" with "HA") as "#HA'".
+ iDestruct ("Hsplit" with "HΓ") as "[HΓ1 HΓ2]".
+ iSplitL "HΓ1"; iApply big_sepM_insert_2; simpl; eauto.
+ Qed.
+
+ Definition env_copy (Γ Γ' : gmap string (lty Σ)) : iProp Σ :=
+ □ ∀ vs, env_ltyped Γ vs -∗ □ env_ltyped Γ' vs.
+
+ Lemma env_copy_empty : ⊢ env_copy ∅ ∅.
+ Proof. iIntros (vs) "!> _ !> ". by rewrite /env_ltyped. Qed.
+
+ Lemma env_copy_extend x A Γ Γ' :
+ Γ !! x = None →
+ env_copy Γ Γ' -∗
+ env_copy (<[x:=A]> Γ) Γ'.
+ Proof.
+ iIntros (HΓ) "#Hcopy". iIntros (vs) "!> Hvs". rewrite /env_ltyped.
+ iDestruct (big_sepM_insert with "Hvs") as "[_ Hvs]"; first by assumption.
+ iApply ("Hcopy" with "Hvs").
+ Qed.
+
+ Lemma env_copy_extend_copy x A Γ Γ' :
+ Γ !! x = None →
+ Γ' !! x = None →
+ copyable A -∗
+ env_copy Γ Γ' -∗
+ env_copy (<[x:=A]> Γ) (<[x:=A]> Γ').
+ Proof.
+ iIntros (HΓx HΓ'x) "#HA #Hcopy". iIntros (vs) "!> Hvs". rewrite /env_ltyped.
+ iDestruct (big_sepM_insert with "Hvs") as "[HA2 Hvs]"; first done.
+ iDestruct ("Hcopy" with "Hvs") as "#Hvs'".
+ iDestruct "HA2" as (v ?) "HA2".
+ iDestruct ("HA" with "HA2") as "#HA3".
+ iIntros "!>". iApply big_sepM_insert; first done. iSplitL; eauto.
+ Qed.
+
+ (* TODO: Maybe move this back to `typing.v` (requires restructuring to avoid
+ circular dependencies). *)
+ (* Typing rule for introducing copyable functions *)
+ Lemma ltyped_rec Γ Γ' f x e A1 A2 :
+ env_copy Γ Γ' -∗
+ (<[f:=(A1 → A2)%lty]>(<[x:=A1]>Γ') ⊨ e : A2) -∗
+ Γ ⊨ (rec: f x := e) : A1 → A2.
+ Proof.
+ iIntros "#Hcopy #He". iIntros (vs) "!> HΓ /=". iApply wp_fupd. wp_pures.
+ iDestruct ("Hcopy" with "HΓ") as "HΓ".
+ iMod (fupd_mask_mono with "HΓ") as "#HΓ"; first done.
+ iModIntro. iLöb as "IH".
+ iIntros (v) "!> HA1". wp_pures. set (r := RecV f x _).
+ iDestruct ("He" $!(binder_insert f r (binder_insert x v vs))
+ with "[HΓ HA1]") as "He'".
+ { iApply (env_ltyped_insert with "IH").
+ iApply (env_ltyped_insert with "HA1 HΓ"). }
+ destruct x as [|x], f as [|f]; rewrite /= -?subst_map_insert //.
+ destruct (decide (x = f)) as [->|].
+ - by rewrite subst_subst delete_idemp insert_insert -subst_map_insert.
+ - rewrite subst_subst_ne // -subst_map_insert.
+ by rewrite -delete_insert_ne // -subst_map_insert.
+ Qed.
+
End copying.
diff --git a/theories/logrel/ltyping.v b/theories/logrel/ltyping.v
index a38fc22..70df4cd 100755
--- a/theories/logrel/ltyping.v
+++ b/theories/logrel/ltyping.v
@@ -126,53 +126,6 @@ Section Environment.
iApply env_split_comm. iApply env_split_left; first by assumption.
by iApply env_split_comm.
Qed.
-
- (* FIXME: copy *)
- (* (* TODO: Get rid of side condition that x does not appear in Γ *) *)
- (* Lemma env_split_copy Γ Γ1 Γ2 (x : string) A: *)
- (* Γ !! x = None → *)
- (* LTyCopy A → *)
- (* env_split Γ Γ1 Γ2 -∗ *)
- (* env_split (<[x:=A]> Γ) (<[x:=A]> Γ1) (<[x:=A]> Γ2). *)
- (* Proof. *)
- (* iIntros (Hcopy HΓx) "#Hsplit". iIntros (vs) "!> HΓ". *)
- (* iPoseProof (big_sepM_insert with "HΓ") as "[Hv HΓ]"; first by assumption. *)
- (* iDestruct "Hv" as (v ?) "#HAv". *)
- (* iDestruct ("Hsplit" with "HΓ") as "[HΓ1 HΓ2]". *)
- (* iSplitL "HΓ1"; iApply big_sepM_insert_2; simpl; eauto. *)
- (* Qed. *)
-
- (* TODO: Prove lemmas about this *)
- Definition env_copy (Γ Γ' : gmap string (lty Σ)) : iProp Σ :=
- □ ∀ vs, env_ltyped Γ vs -∗ □ env_ltyped Γ' vs.
-
- Lemma env_copy_empty : ⊢ env_copy ∅ ∅.
- Proof. iIntros (vs) "!> _ !> ". by rewrite /env_ltyped. Qed.
-
- Lemma env_copy_extend x A Γ Γ' :
- Γ !! x = None →
- env_copy Γ Γ' -∗
- env_copy (<[x:=A]> Γ) Γ'.
- Proof.
- iIntros (HΓ) "#Hcopy". iIntros (vs) "!> Hvs". rewrite /env_ltyped.
- iDestruct (big_sepM_insert with "Hvs") as "[_ Hvs]"; first by assumption.
- iApply ("Hcopy" with "Hvs").
- Qed.
-
- (* FIXME: copy *)
- (* Lemma env_copy_extend_copy x A Γ Γ' : *)
- (* Γ !! x = None → *)
- (* Γ' !! x = None → *)
- (* LTyCopy A → *)
- (* env_copy Γ Γ' -∗ *)
- (* env_copy (<[x:=A]> Γ) (<[x:=A]> Γ'). *)
- (* Proof. *)
- (* iIntros (HΓx HΓ'x HcopyA) "#Hcopy". iIntros (vs) "!> Hvs". rewrite /env_ltyped. *)
- (* iDestruct (big_sepM_insert with "Hvs") as "[HA Hvs]"; first done. *)
- (* iDestruct ("Hcopy" with "Hvs") as "#Hvs'". *)
- (* iDestruct "HA" as (v ?) "#HA". *)
- (* iIntros "!>". iApply big_sepM_insert; first done. iSplitL; eauto. *)
- (* Qed. *)
End Environment.
(* The semantic typing judgement *)
diff --git a/theories/logrel/subtyping.v b/theories/logrel/subtyping.v
index d0991da..3947c26 100644
--- a/theories/logrel/subtyping.v
+++ b/theories/logrel/subtyping.v
@@ -59,6 +59,12 @@ Section subtype.
Lemma lty_bi_le_trans A1 A2 A3 : ⊢ A1 <:> A2 -∗ A2 <:> A3 -∗ A1 <:> A3.
Proof. iIntros "#[H11 H12] #[H21 H22]". iSplit; by iApply lty_le_trans. Qed.
+ Lemma lty_le_copy A B :
+ A <: B -∗ copy A <: copy B.
+ Proof.
+ iIntros "#Hsub". iIntros (v) "!> #HA !>".
+ iApply ("Hsub" with "HA").
+ Qed.
Lemma lty_le_arr A11 A12 A21 A22 :
▷ (A21 <: A11) -∗ ▷ (A12 <: A22) -∗
diff --git a/theories/logrel/types.v b/theories/logrel/types.v
index 8b0ef80..c205602 100644
--- a/theories/logrel/types.v
+++ b/theories/logrel/types.v
@@ -2,6 +2,7 @@ From stdpp Require Import pretty.
From actris.utils Require Import switch.
From actris.logrel Require Export ltyping session_types.
From actris.channel Require Import proto proofmode.
+From iris.bi.lib Require Export core.
From iris.heap_lang Require Export lifting metatheory.
From iris.base_logic.lib Require Import invariants.
From iris.heap_lang.lib Require Import assert.
@@ -14,6 +15,7 @@ Section types.
Definition lty_bool : lty Σ := Lty (λ w, ∃ b : bool, ⌜ w = #b âŒ)%I.
Definition lty_int : lty Σ := Lty (λ w, ∃ n : Z, ⌜ w = #n âŒ)%I.
Definition lty_copy (A : lty Σ) : lty Σ := Lty (λ w, □ (A w))%I.
+ Definition lty_copyminus (A : lty Σ) : lty Σ := Lty (λ w, coreP (A w)).
Definition lty_arr (A1 A2 : lty Σ) : lty Σ := Lty (λ w,
∀ v, ▷ A1 v -∗ WP w v {{ A2 }})%I.
(* TODO: Make a non-linear version of prod, using ∧ *)
@@ -55,6 +57,7 @@ End types.
Notation "()" := lty_unit : lty_scope.
Notation "'copy' A" := (lty_copy A) (at level 10) : lty_scope.
+Notation "'copy-' A" := (lty_copyminus A) (at level 10) : lty_scope.
Notation "A → B" := (lty_copy (lty_arr A B)) : lty_scope.
Notation "A ⊸ B" := (lty_arr A B) (at level 99, B at level 200, right associativity) : lty_scope.
Infix "*" := lty_prod : lty_scope.
@@ -206,27 +209,6 @@ Section properties.
- by iApply ltyped_lam=> //=.
Qed.
- Lemma ltyped_rec Γ Γ' f x e A1 A2 :
- env_copy Γ Γ' -∗
- (<[f:=(A1 → A2)%lty]>(<[x:=A1]>Γ') ⊨ e : A2) -∗
- Γ ⊨ (rec: f x := e) : A1 → A2.
- Proof.
- iIntros "#Hcopy #He". iIntros (vs) "!> HΓ /=". iApply wp_fupd. wp_pures.
- iDestruct ("Hcopy" with "HΓ") as "HΓ".
- iMod (fupd_mask_mono with "HΓ") as "#HΓ"; first done.
- iModIntro. iLöb as "IH".
- iIntros (v) "!> HA1". wp_pures. set (r := RecV f x _).
- iDestruct ("He" $!(binder_insert f r (binder_insert x v vs))
- with "[HΓ HA1]") as "He'".
- { iApply (env_ltyped_insert with "IH").
- iApply (env_ltyped_insert with "HA1 HΓ"). }
- destruct x as [|x], f as [|f]; rewrite /= -?subst_map_insert //.
- destruct (decide (x = f)) as [->|].
- - by rewrite subst_subst delete_idemp insert_insert -subst_map_insert.
- - rewrite subst_subst_ne // -subst_map_insert.
- by rewrite -delete_insert_ne // -subst_map_insert.
- Qed.
-
Fixpoint lty_arr_list (As : list (lty Σ)) (B : lty Σ) : lty Σ :=
match As with
| [] => B
--
GitLab