Commit 4014e9e9 authored by Dan Frumin's avatar Dan Frumin

Add coqpl examples

parent 706b659a
......@@ -48,3 +48,4 @@ theories/tests/typetest.v
theories/tests/ghosttp.v
theories/tests/tactics.v
theories/tests/tactics2.v
theories/examples/coqpl.v
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_pure_r _.
rel_load_l. rel_load_r.
iApply bin_log_related_nat.
Qed.
Definition bitτ : type := : TVar 0 × (TVar 0 TVar 0) × (TVar 0 Bool).
Definition bit_bool : val :=
pack (#true, (λ: "b", "b" #true), (λ: "b", "b")).
Definition flip_nat : val := λ: "n",
if: ("n" = #0) then #1 else #0.
Definition bit_nat : val :=
pack (#1, flip_nat, (λ: "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.
Lemma bit_prerefinement Δ Γ :
{Δ;Γ} bit_bool log bit_nat : bitτ.
Proof.
unfold bit_bool, bit_nat, flip_nat; simpl. (* we need this to compute the coercion from values to expression *)
iApply (bin_log_related_pack _ R).
repeat iApply bin_log_related_pair.
- rel_finish.
- iApply bin_log_related_arrow_val; try by unlock. cbn-[R].
iIntros "!#" (v1 v2) "/=".
iIntros ([b [? ?]]); simplify_eq/=. unlock; simpl.
rel_rec_l. rel_rec_r.
rel_op_l. rel_op_r.
destruct b; simpl; rel_if_r; rel_finish.
- iApply bin_log_related_arrow_val; try by unlock.
iIntros "!#" (v1 v2) "/=". (* TODO: notation for LitV? *)
iIntros ([b [? ?]]); simplify_eq/=. unlock; simpl.
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".
iApply bin_log_related_arrow; auto.
iIntros "!#" (f1 f2) "#Hf".
rel_let_l; rel_let_r.
iApply (bin_log_related_seq with "[Hf]"); 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.
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