Commit b1e5fb0c authored by Dan Frumin's avatar Dan Frumin

Add a Y-combinator as an example

parent 494b6695
......@@ -42,6 +42,7 @@ theories/examples/various.v
theories/examples/or.v
theories/examples/symbol.v
theories/examples/generative.v
theories/examples/Y.v
theories/tests/typetest.v
theories/tests/tactics.v
theories/tests/tactics2.v
From iris.proofmode Require Import tactics.
From iris_logrel Require Export logrel.
(* Semantic typeability of the Y combinator *)
Definition Y : val :=
λ: "f", (λ: "x", "f" ("x" "x")) (λ: "x", "f" ("x" "x")).
Section contents.
Context `{logrelG Σ}.
Lemma Y_semtype Δ Γ A :
{,;Δ;Γ} Y log Y : TArrow (TArrow A A) A.
Proof.
unlock Y. simpl.
iApply bin_log_related_arrow_val; eauto.
Typeclasses Opaque interp. (* TODO *)
iAlways. iIntros (f1 f2) "#Hff".
rel_let_l. rel_let_r.
iLöb as "IH".
rel_let_l. rel_let_r.
iApply bin_log_related_app.
- iApply (related_ret ).
iApply (interp_ret ); eauto using to_of_val.
simpl. iApply "Hff".
- iApply "IH".
Qed.
End contents.
Theorem Y_typesafety f e' τ thp σ σ' :
⊢ₜ f : TArrow τ τ
rtc step ([Y f], σ) (thp, σ') e' thp
is_Some (to_val e') reducible e' σ'.
Proof.
intros Hf Hst He'.
eapply (logrel_typesafety logrelΣ [] (Y f)); eauto.
intros. iApply bin_log_related_app.
- iApply Y_semtype.
- iApply binary_fundamental; eauto.
Qed.
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