From 1bed793ba92bb48e3231deb73601f492c0622b2a Mon Sep 17 00:00:00 2001 From: Dan Frumin Date: Sun, 10 Dec 2017 18:48:05 +0100 Subject: [PATCH] Example: Landin's knot is equivalent to the Y combinator --- _CoqProject | 1 + theories/examples/Y.v | 42 +++++++++++++++++++++++++++++++++++-- theories/examples/bot.v | 23 ++++++++++++++++++++ theories/examples/or.v | 2 +- theories/examples/symbol.v | 4 ---- theories/examples/various.v | 14 +------------ 6 files changed, 66 insertions(+), 20 deletions(-) create mode 100644 theories/examples/bot.v diff --git a/_CoqProject b/_CoqProject index 24956e7..1719227 100644 --- a/_CoqProject +++ b/_CoqProject @@ -27,6 +27,7 @@ theories/logrel/soundness_binary.v theories/logrel.v theories/examples/lock.v theories/examples/ticket_lock.v +theories/examples/bot.v theories/examples/counter.v theories/examples/lateearlychoice.v theories/examples/par.v diff --git a/theories/examples/Y.v b/theories/examples/Y.v index b22b210..7b55328 100644 --- a/theories/examples/Y.v +++ b/theories/examples/Y.v @@ -1,11 +1,15 @@ From iris.proofmode Require Import tactics. -From iris_logrel Require Export logrel. +From iris_logrel Require Export logrel examples.bot. -(* Semantic typeability of the Y combinator *) +(* Semantic typeability of the Y combinator and the Landin's knot *) Definition Y : val := λ: "f", (λ: "x", "f" ("x" "x")) (λ: "x", "f" ("x" "x")). +Definition Knot : val := λ: "f", + let: "z" := ref bot + in "z" <- (λ: "x", "f" (!"z" #()));; !"z" #(). + Section contents. Context `{logrelG Σ}. Lemma Y_semtype Δ Γ A : @@ -20,6 +24,40 @@ Section contents. iApply (bin_log_related_app with "Hff"). by iApply "IH". Qed. + + Lemma KNOT_Y Δ Γ A : + {⊤,⊤;Δ;Γ} ⊨ Knot ≤log≤ Y : TArrow (TArrow A A) A. + Proof. + unlock Y Knot. simpl. + iApply bin_log_related_arrow; eauto. + iAlways. iIntros (f1 f2) "#Hff". + rel_let_l. rel_let_r. + rel_alloc_l as z "Hz". rel_let_l. + rel_store_l. + rel_let_l. + iLöb as "IH". + rel_let_r. + rel_load_l. rel_let_l. + iApply (bin_log_related_app with "Hff"). + by iApply "IH". + Qed. + + Lemma Y_KNOT Δ Γ A : + {⊤,⊤;Δ;Γ} ⊨ Y ≤log≤ Knot : TArrow (TArrow A A) A. + Proof. + unlock Y Knot. simpl. + iApply bin_log_related_arrow; eauto. + iAlways. iIntros (f1 f2) "#Hff". + rel_let_l. rel_let_r. + rel_alloc_r as z "Hz". rel_let_r. + rel_store_r. + rel_let_r. + iLöb as "IH". + rel_let_l. + rel_load_r. rel_let_r. + iApply (bin_log_related_app with "Hff"). + by iApply "IH". + Qed. End contents. Theorem Y_typesafety f e' τ thp σ σ' : diff --git a/theories/examples/bot.v b/theories/examples/bot.v new file mode 100644 index 0000000..6f45701 --- /dev/null +++ b/theories/examples/bot.v @@ -0,0 +1,23 @@ +From iris.proofmode Require Import tactics. +From iris_logrel Require Export logrel. + +Definition bot : val := rec: "bot" <> := "bot" #(). + +Lemma bot_typed Γ τ : + Γ ⊢ₜ bot : TArrow TUnit τ. +Proof. solve_typed. Qed. +Hint Resolve bot_typed : typeable. + +Section contents. + Context `{logrelG Σ}. + Lemma bot_l ϕ Δ Γ E K t τ : + (ϕ -∗ {E;Δ;Γ} ⊨ fill K (bot #()) ≤log≤ t : τ) -∗ + {E;Δ;Γ} ⊨ fill K (bot #()) ≤log≤ t : τ. + Proof. + iIntros "Hlog". + iLöb as "IH". + rel_rec_l. + unlock bot; simpl_subst/=. + iApply ("IH" with "Hlog"). + Qed. +End contents. diff --git a/theories/examples/or.v b/theories/examples/or.v index a133f40..6638a26 100644 --- a/theories/examples/or.v +++ b/theories/examples/or.v @@ -15,7 +15,7 @@ where every v_i is well-typed Unit -> Unit *) From iris.proofmode Require Import tactics. -From iris_logrel Require Export logrel examples.various (* for bot *). +From iris_logrel Require Export logrel examples.bot. Definition or : val := λ: "e1" "e2", let: "x" := ref #0 in diff --git a/theories/examples/symbol.v b/theories/examples/symbol.v index 22cf4e7..0cba747 100644 --- a/theories/examples/symbol.v +++ b/theories/examples/symbol.v @@ -75,10 +75,6 @@ Definition nth : val := rec: "nth" "l" "n" := else "nth" (Snd "xs") ("n" - #1) end. -Lemma bot_typed Γ τ : - Γ ⊢ₜ bot : TArrow TUnit τ. -Proof. solve_typed. Qed. -Hint Resolve bot_typed : typeable. Lemma nth_typed Γ τ : Γ ⊢ₜ nth : TArrow (LIST τ) (TArrow TNat τ). Proof. diff --git a/theories/examples/various.v b/theories/examples/various.v index 754b8aa..e67b225 100644 --- a/theories/examples/various.v +++ b/theories/examples/various.v @@ -4,7 +4,7 @@ *) From iris.proofmode Require Import tactics. From iris.algebra Require Import csum agree excl. -From iris_logrel Require Import logrel examples.lock examples.counter. +From iris_logrel Require Export logrel examples.lock examples.counter examples.bot. Section refinement. Context `{logrelG Σ}. @@ -219,18 +219,6 @@ Section refinement. rel_vals; eauto. } Qed. - Definition bot : val := rec: "bot" <> := "bot" #(). - Lemma bot_l ϕ Δ Γ E K t τ : - (ϕ -∗ {E;Δ;Γ} ⊨ fill K (bot #()) ≤log≤ t : τ) -∗ - {E;Δ;Γ} ⊨ fill K (bot #()) ≤log≤ t : τ. - Proof. - iIntros "Hlog". - iLöb as "IH". - rel_rec_l. - unlock bot; simpl_subst/=. - iApply ("IH" with "Hlog"). - Qed. - (* /Sort of/ a well-bracketedness example. Without locking in the first expression, the callback can reenter the body in a forked thread to change the value of x -- 2.26.2