Commit 6c4e6ece by Jonas Kastberg

### Defined conversion functions from ktele to tele

parent 9fc2519f
 ... ... @@ -42,10 +42,11 @@ Inductive ltys {Σ} : ktele Σ → Type := | LTysS {k} {binder} (K : lty Σ k) : ltys (binder K) → ltys (KTeleS binder). Arguments ltys : clear implicits. Definition ktele_app {Σ} {kt : ktele Σ} {T} (f : kt -k> T) : ltys kt → T := λ Ks, (fix rec {kt} (Ks : ltys kt) : (kt -k> T) → T := match Ks in ltys kt return (kt -k> T) → T with Definition ktele_app {Σ} {kt : ktele Σ} {T} (f : kt -k> T) : ltys Σ kt → T := λ Ks, (fix rec {kt} (Ks : ltys Σ kt) : (kt -k> T) → T := match Ks in ltys _ kt return (kt -k> T) → T with | LTysO => λ t : T, t | LTysS K Ks => λ f, rec Ks (f K) end) kt Ks f. ... ... @@ -56,15 +57,15 @@ Arguments ktele_app {_} {!_ _} _ !_ /. (* Local Coercion ktele_app : ktele_fun >-> Funclass. *) (** Inversion lemma for [tele_arg] *) Lemma ltys_inv {Σ} {kt : ktele Σ} (Ks : ltys kt) : match kt as kt return ltys kt → Prop with Lemma ltys_inv {Σ} {kt : ktele Σ} (Ks : ltys Σ kt) : match kt as kt return ltys _ kt → Prop with | KTeleO => λ Ks, Ks = LTysO | KTeleS f => λ Ks, ∃ K Ks', Ks = LTysS K Ks' end Ks. Proof. induction Ks; eauto. Qed. Lemma ltys_O_inv {Σ} (Ks : ltys (@KTeleO Σ)) : Ks = LTysO. Lemma ltys_O_inv {Σ} (Ks : ltys Σ (@KTeleO Σ)) : Ks = LTysO. Proof. exact (ltys_inv Ks). Qed. Lemma ltys_S_inv {Σ} {X} {f : lty Σ X → ktele Σ} (Ks : ltys (KTeleS f)) : Lemma ltys_S_inv {Σ} {X} {f : lty Σ X → ktele Σ} (Ks : ltys Σ (KTeleS f)) : ∃ K Ks', Ks = LTysS K Ks'. Proof. exact (ltys_inv Ks). Qed. (* ... ... @@ -93,16 +94,16 @@ Lemma ktele_fmap_app {Σ} {T U} {kt : ktele Σ} (F : T → U) (t : kt -k> T) (x Proof. apply ktele_map_app. Qed. *) (** Operate below [tele_fun]s with argument telescope [kt]. *) Fixpoint ktele_bind {Σ} {U} {kt : ktele Σ} : (ltys kt → U) → kt -k> U := match kt as kt return (ltys kt → U) → kt -k> U with Fixpoint ktele_bind {Σ} {U} {kt : ktele Σ} : (ltys Σ kt → U) → kt -k> U := match kt as kt return (ltys _ kt → U) → kt -k> U with | KTeleO => λ F, F LTysO | @KTeleS _ k b => λ (F : ltys (KTeleS b) → U) (K : lty Σ k), (* b x -t> U *) | @KTeleS _ k b => λ (F : ltys Σ (KTeleS b) → U) (K : lty Σ k), (* b x -t> U *) ktele_bind (λ Ks, F (LTysS K Ks)) end. Arguments ktele_bind {_} {_ !_} _ /. (* Show that tele_app ∘ tele_bind is the identity. *) Lemma ktele_app_bind {Σ} {U} {kt : ktele Σ} (f : ltys kt → U) K : Lemma ktele_app_bind {Σ} {U} {kt : ktele Σ} (f : ltys Σ kt → U) K : ktele_app (ktele_bind f) K = f K. Proof. induction kt as [|k b IH]; simpl in *. ... ... @@ -117,6 +118,13 @@ Fixpoint ktele_to_tele {Σ} (kt : ktele Σ) : tele := | KTeleS b => TeleS (λ x, ktele_to_tele (b x)) end. Fixpoint ltys_to_tele_args {Σ} {kt} (Ks : ltys Σ kt) : tele_arg (ktele_to_tele kt) := match Ks with | LTysO => TargO | LTysS K Ks => TargS K (ltys_to_tele_args Ks) end. (* (** We can define the identity function and composition of the [-t>] function *) ... ...
 ... ... @@ -9,7 +9,7 @@ Bind Scope lmsg_scope with lmsg. Definition lty_msg_exist {Σ} {k} (M : lty Σ k → lmsg Σ) : lmsg Σ := (∃ X, M X)%msg. Definition lty_msg_texist {Σ} {kt : ktele Σ} (M : ltys kt → lmsg Σ) : lmsg Σ := Definition lty_msg_texist {Σ} {kt : ktele Σ} (M : ltys Σ kt → lmsg Σ) : lmsg Σ := ktele_fold (@lty_msg_exist Σ) (λ x, x) (ktele_bind M). Definition lty_msg_base {Σ} (A : ltty Σ) (S : lsty Σ) : lmsg Σ := ... ...
 ... ... @@ -268,21 +268,21 @@ Section subtyping_rules. Proof. iIntros "!>". iApply (iProto_le_exist_intro_r). Qed. (* Elimination rules need inhabited variant of telescopes in the model *) Lemma lty_le_texist_elim_l {kt : ktele Σ} (M : ltys kt → lmsg Σ) S : Lemma lty_le_texist_elim_l {kt : ktele Σ} (M : ltys Σ kt → lmsg Σ) S : (∀ Xs, ( M Xs) <: S) -∗ ( M Xs) <: S. Proof. Admitted. Lemma lty_le_texist_elim_r {kt : ktele Σ} (M : ltys kt → lmsg Σ) S : Lemma lty_le_texist_elim_r {kt : ktele Σ} (M : ltys Σ kt → lmsg Σ) S : (∀ Xs, S <: ( M Xs)) -∗ S <: ( M Xs). Proof. Admitted. Lemma lty_le_texist_intro_l {kt : ktele Σ} (M : ltys kt → lmsg Σ) Ks : Lemma lty_le_texist_intro_l {kt : ktele Σ} (M : ltys Σ kt → lmsg Σ) Ks : ⊢ ( M Xs) <: ( M Ks). Proof. Admitted. Lemma lty_le_texist_intro_r {kt : ktele Σ} (M : ltys kt → lmsg Σ) Ks : Lemma lty_le_texist_intro_r {kt : ktele Σ} (M : ltys Σ kt → lmsg Σ) Ks : ⊢ ( M Ks) <: ( M Xs). Proof. Admitted. ... ...
 ... ... @@ -28,7 +28,7 @@ Definition lty_forall `{heapG Σ} {k} (C : lty Σ k → ltty Σ) : ltty Σ := Ltty (λ w, ∀ A, WP w #() {{ ltty_car (C A) }})%I. Definition lty_exist {Σ k} (C : lty Σ k → ltty Σ) : ltty Σ := Ltty (λ w, ∃ A, ▷ ltty_car (C A) w)%I. Definition lty_texist {Σ} {kt : ktele Σ} (C : ltys kt → ltty Σ) : ltty Σ := Definition lty_texist {Σ} {kt : ktele Σ} (C : ltys Σ kt → ltty Σ) : ltty Σ := ktele_fold (@lty_exist Σ) (λ x, x) (ktele_bind C). Definition lty_ref_mut `{heapG Σ} (A : ltty Σ) : ltty Σ := Ltty (λ w, ... ...
 ... ... @@ -258,11 +258,11 @@ Section properties. iApply env_ltyped_delete=> //. Qed. Lemma texist_exist {kt : ktele Σ} (C : ltys kt → ltty Σ) v : Lemma texist_exist {kt : ktele Σ} (C : ltys Σ kt → ltty Σ) v : ltty_car (lty_texist C) v -∗ (∃ X, ▷ ltty_car (C X) v). Proof. Admitted. Lemma ltyped_unpack' {kt} Γ1 Γ2 Γ3 x e1 e2 (C : ltys kt → ltty Σ) B : Lemma ltyped_unpack' {kt} Γ1 Γ2 Γ3 x e1 e2 (C : ltys Σ kt → ltty Σ) B : (Γ1 ⊨ e1 : lty_texist C ⫤ Γ2) -∗ (∀ Ys, binder_insert x (C Ys) Γ2 ⊨ e2 : B ⫤ Γ3) -∗ Γ1 ⊨ (let: x := e1 in e2) : B ⫤ binder_delete x Γ3. ... ... @@ -487,6 +487,10 @@ Section properties. Section with_chan. Context `{chanG Σ}. Lemma chan_texist_exist {kt : ktele Σ} c (M : ktele_to_tele kt → lmsg Σ) : ltty_car (chan ( M (ltys_to_tele_args Xs) )) c -∗ c ↣ ( M Xs). Proof. Admitted. Definition chanalloc : val := λ: "u", let: "cc" := new_chan #() in "cc". Lemma ltyped_chanalloc S : ⊢ ∅ ⊨ chanalloc : () → (chan S * chan (lty_dual S)). ... ... @@ -539,7 +543,7 @@ Section properties. Qed. Lemma ltyped_recv_poly {kt : ktele Σ} Γ1 Γ2 (c : string) (x : string) (e : expr) (A : ltys kt → ltty Σ) (S : ltys kt → lsty Σ) (B : ltty Σ) : (A : ltys Σ kt → ltty Σ) (S : ltys Σ kt → lsty Σ) (B : ltty Σ) : ⊢ (∀ Ys, binder_insert x (A Ys) (<[c := (chan (S Ys))%lty ]> Γ1) ⊨ e : B ⫤ Γ2) -∗ <[c := (chan ( ∃.. Xs, TY A Xs; S Xs))%lty]> Γ1 ⊨ (let: x := recv c in e) : B ⫤ binder_delete x Γ2. ... ... @@ -549,6 +553,8 @@ Section properties. { by apply lookup_insert. } rewrite Heq. rewrite delete_insert; last by admit. iDestruct (chan_texist_exist v' with "[Hc]") as "Hc". { admit. } wp_apply (recv_spec with "[Hc]"). { admit. } iIntros (Xs) "[Hc HC]". ... ...
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!