From iris.proofmode Require Import tactics. From iris_logrel Require Import logrel. Section refinement. Context `{logrelG Σ}. Notation D := (prodC valC valC -n> iProp Σ). Program Definition valrel' : (val * val → iProp Σ) → D := fun f => λne x, f x. Solve Obligations with solve_proper. Definition valrel (f : val → val → iProp Σ) : D := valrel' \$ λ vv, f (vv.1) (vv.2). Lemma test_goal Δ Γ (l l' : loc) : l ↦ᵢ #1 -∗ l' ↦ₛ #0 -∗ {Δ;Γ} ⊨ !#l ≤log≤ (#l' <- #1;; !#l') : TNat. Proof. iIntros "Hl Hl'". rel_store_r. rel_seq_r. rel_load_l. rel_load_r. iApply bin_log_related_nat. Qed. Definition bitT : type := ∃: TVar 0 × (TVar 0 → TVar 0) × (TVar 0 → Bool). Definition bit_bool : val := pack (#true, (λ: "b", ¬ "b"), (λ: "b", "b")). Definition bit_nat : val := pack (#1, (λ: "n", if: ("n" = #0) then #1 else #0), (λ: "b", "b" = #1)). Definition f (b : bool) : nat := if b then 1 else 0. (* R ⊆ Bool × Nat = { (true, 1), (false, 0) }*) Definition R : D := valrel \$ λ v1 v2, (∃ b : bool, ⌜v1 = #b⌝ ∗ ⌜v2 = #(f b)⌝)%I. Instance R_persistent ww : Persistent (R ww). Proof. apply _. Qed. Ltac rel_arrow_val := iApply bin_log_related_arrow_val; try by unlock. Ltac rel_arrow := iApply bin_log_related_arrow; auto. Lemma bit_refinement Δ Γ : {Δ;Γ} ⊨ bit_bool ≤log≤ bit_nat : bitT. Proof. unlock bit_bool bit_nat; simpl. iApply (bin_log_related_pack _ R). repeat iApply bin_log_related_pair. - rel_finish. - rel_arrow_val. simpl. iIntros "!#" (v1 v2). iIntros ([b [? ?]]); simplify_eq/=. rel_rec_l. rel_rec_r. rel_op_l. rel_op_r. destruct b; simpl; rel_if_r; rel_finish. - rel_arrow_val. simpl. iIntros "!#" (v1 v2). iIntros ([b [? ?]]); simplify_eq/=. rel_rec_l. rel_rec_r. rel_op_r. destruct b; rel_finish. Qed. Definition N : namespace := nroot.@"PL".@"Coq". Lemma higher_order_stateful Δ Γ : {Δ;Γ} ⊨ let: "x" := ref #1 in (λ: "f", "f" #();; !"x") ≤log≤ (λ: "f", "f" #();; #1) : ((Unit → Unit) → TNat). Proof. rel_alloc_l as l "Hl". rel_let_l. iMod (inv_alloc N _ (l ↦ᵢ #1)%I with "Hl") as "#Hinv". rel_arrow. iIntros "!#" (f1 f2) "#Hf". rel_let_l; rel_let_r. iApply bin_log_related_seq; auto. - iApply (bin_log_related_app with "Hf"). iApply bin_log_related_unit. - rel_load_l_atomic; iInv N as "Hl" "Hcl"; iModIntro. iExists #1. iNext. iFrame "Hl". simpl. iIntros "Hl". iMod ("Hcl" with "Hl") as "_". iApply bin_log_related_nat. Qed. End refinement.