diff --git a/_CoqProject b/_CoqProject index 24956e7004adbce820c0554e75fe82e79bab0eb4..171922776790384c6c28f2cc85fc74aa7732ac83 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 b22b210337391955f92a9f4f4e99d8b7205cbe0a..7b5532810417dafd32cd8fd317528358965e2b57 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 0000000000000000000000000000000000000000..6f457015ca41f76ad221afa04ae7dcdd11909cfb --- /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 a133f40887982113c55fd9b58715f3449b4526af..6638a26c168fc253d9bc65863e4e3971ce1ee4b7 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 22cf4e706aea2a34150e1e1e782c2751fc423ca2..0cba7475dd206381a09bf5ddf2899cbca0bb1e31 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 754b8aac31548ed966773536d2289154bf283ac6..e67b22518718baff24524ea6e88c704af8437a0b 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