coqpl.v 2.68 KB
 Dan Frumin committed Jan 03, 2018 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 ``````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'". `````` Dan Frumin committed Jan 06, 2018 19 `````` rel_store_r. rel_seq_r. `````` Dan Frumin committed Jan 03, 2018 20 21 22 23 `````` rel_load_l. rel_load_r. iApply bin_log_related_nat. Qed. `````` Dan Frumin committed Jan 06, 2018 24 `````` Definition bitT : type := ∃: TVar 0 × (TVar 0 → TVar 0) × (TVar 0 → Bool). `````` Dan Frumin committed Jan 03, 2018 25 26 `````` Definition bit_bool : val := `````` Dan Frumin committed Jan 03, 2018 27 `````` pack (#true, (λ: "b", ¬ "b"), (λ: "b", "b")). `````` Dan Frumin committed Jan 03, 2018 28 29 `````` Definition bit_nat : val := `````` Dan Frumin committed Jan 03, 2018 30 `````` pack (#1, (λ: "n", if: ("n" = #0) then #1 else #0), (λ: "b", "b" = #1)). `````` Dan Frumin committed Jan 03, 2018 31 32 33 34 35 36 37 38 39 `````` 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. `````` Dan Frumin committed Jan 06, 2018 40 41 42 43 44 `````` 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. `````` Dan Frumin committed Jan 03, 2018 45 `````` Proof. `````` Dan Frumin committed Jan 06, 2018 46 `````` unlock bit_bool bit_nat; simpl. `````` Dan Frumin committed Jan 03, 2018 47 48 49 `````` iApply (bin_log_related_pack _ R). repeat iApply bin_log_related_pair. - rel_finish. `````` Dan Frumin committed Jan 06, 2018 50 `````` - rel_arrow_val. simpl. `````` Dan Frumin committed Jan 03, 2018 51 `````` iIntros "!#" (v1 v2). `````` Dan Frumin committed Jan 06, 2018 52 `````` iIntros ([b [? ?]]); simplify_eq/=. `````` Dan Frumin committed Jan 03, 2018 53 54 55 `````` rel_rec_l. rel_rec_r. rel_op_l. rel_op_r. destruct b; simpl; rel_if_r; rel_finish. `````` Dan Frumin committed Jan 06, 2018 56 `````` - rel_arrow_val. simpl. `````` Dan Frumin committed Jan 03, 2018 57 `````` iIntros "!#" (v1 v2). `````` Dan Frumin committed Jan 06, 2018 58 `````` iIntros ([b [? ?]]); simplify_eq/=. `````` Dan Frumin committed Jan 03, 2018 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 `````` 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". `````` Dan Frumin committed Jan 06, 2018 77 `````` rel_arrow. `````` Dan Frumin committed Jan 03, 2018 78 79 `````` iIntros "!#" (f1 f2) "#Hf". rel_let_l; rel_let_r. `````` Dan Frumin committed Jan 06, 2018 80 `````` iApply bin_log_related_seq; auto. `````` Dan Frumin committed Jan 03, 2018 81 82 83 84 85 86 87 88 89 90 91 `````` - 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.``````