A fixpoint definition using `rec`

theories/examples/Y.v

@@ -10,6 +10,9 @@ Definition Knot : val := λ: "f",
   let: "z" := ref bot
   in "z" <- (λ: "x", "f" (!"z" #()));; !"z" #().
 
+Definition F : val := rec: "f" "g" :=
+  "g" ("f" "g").
+
 Section contents.
   Context `{logrelG Σ}.
   Lemma Y_semtype Δ Γ A :
@@ -58,6 +61,58 @@ Section contents.
     iApply (bin_log_related_app with "Hff").
     by iApply "IH".
   Qed.
+
+  Lemma FIX_Y Δ Γ A :
+    {⊤,⊤;Δ;Γ} ⊨ F ≤log≤ Y : TArrow (TArrow A A) A.
+  Proof.
+    unlock Y F. simpl.
+    iApply bin_log_related_arrow; eauto.
+    iAlways. iIntros (f1 f2) "#Hff".
+    rel_let_r.
+    iLöb as "IH".
+    rel_let_l. rel_let_r.
+    iApply (bin_log_related_app with "Hff").
+    by iApply "IH".
+  Qed.
+
+  Lemma Y_FIX Δ Γ A :
+    {⊤,⊤;Δ;Γ} ⊨ Y ≤log≤ F : TArrow (TArrow A A) A.
+  Proof.
+    unlock Y F. simpl.
+    iApply bin_log_related_arrow; eauto.
+    iAlways. iIntros (f1 f2) "#Hff".
+    rel_let_l.
+    iLöb as "IH".
+    rel_let_l. rel_let_r.
+    iApply (bin_log_related_app with "Hff").
+    by iApply "IH".
+  Qed.
+
+  Lemma FIX_prefixpoint Δ Γ α β (v : val) :
+    □ ({Δ;Γ} ⊨ v ≤log≤ v : ((α → β) → α → β)) -∗
+    {Δ;Γ} ⊨ v (F v) ≤log≤ F v : (α → β).
+  Proof.
+    iIntros "#Hv".
+    unlock F. simpl.
+    rel_let_r.
+    iApply (bin_log_related_app with "Hv").
+    iApply (bin_log_related_app with "[] Hv").
+    iApply binary_fundamental.
+    solve_typed.
+  Qed.
+
+  Lemma FIX_postfixpoint Δ Γ α β (v : val) :
+    □ ({Δ;Γ} ⊨ v ≤log≤ v : ((α → β) → α → β)) -∗
+    {Δ;Γ} ⊨ F v ≤log≤ v (F v) : (α → β).
+  Proof.
+    iIntros "#Hv".
+    unlock F. simpl.
+    rel_let_l.
+    iApply (bin_log_related_app with "Hv").
+    iApply (bin_log_related_app with "[] Hv").
+    iApply binary_fundamental.
+    solve_typed.
+  Qed.
 End contents.
 
 Theorem Y_typesafety f e' τ thp σ σ' :