coqpl.v 2.67 KB
Newer Older
Dan Frumin's avatar
Dan Frumin committed
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'".
19
    rel_store_r. rel_seq_r.
Dan Frumin's avatar
Dan Frumin committed
20 21 22 23
    rel_load_l. rel_load_r.
    iApply bin_log_related_nat.
  Qed.

24
  Definition bitT : type := : TVar 0 × (TVar 0  TVar 0) × (TVar 0  Bool).
Dan Frumin's avatar
Dan Frumin committed
25 26

  Definition bit_bool : val :=
Dan Frumin's avatar
Dan Frumin committed
27
    pack (#true, (λ: "b", ¬ "b"), (λ: "b", "b")).
Dan Frumin's avatar
Dan Frumin committed
28 29

  Definition bit_nat : val :=
Dan Frumin's avatar
Dan Frumin committed
30
    pack (#1, (λ: "n", if: ("n" = #0) then #1 else #0), (λ: "b", "b" = #1)).
Dan Frumin's avatar
Dan Frumin committed
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.

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's avatar
Dan Frumin committed
45
  Proof.
46
    unlock bit_bool bit_nat; simpl.
47
    iApply (bin_log_related_pack R).
Dan Frumin's avatar
Dan Frumin committed
48 49
    repeat iApply bin_log_related_pair.
    - rel_finish.
50
    - rel_arrow_val. simpl.
Dan Frumin's avatar
Dan Frumin committed
51
      iIntros "!#" (v1 v2).
52
      iIntros ([b [? ?]]); simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
53 54 55
      rel_rec_l. rel_rec_r.
      rel_op_l. rel_op_r.
      destruct b; simpl; rel_if_r; rel_finish.
56
    - rel_arrow_val. simpl.
Dan Frumin's avatar
Dan Frumin committed
57
      iIntros "!#" (v1 v2).
58
      iIntros ([b [? ?]]); simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
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".
77
    rel_arrow.
Dan Frumin's avatar
Dan Frumin committed
78 79
    iIntros "!#" (f1 f2) "#Hf".
    rel_let_l; rel_let_r.
Dan Frumin's avatar
Dan Frumin committed
80
    iApply bin_log_related_seq'; auto.
Dan Frumin's avatar
Dan Frumin committed
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.