Commit dd076083 authored by Dan Frumin's avatar Dan Frumin

Tweak the CoqPL examples a bit

parent 7f00eebc
......@@ -16,12 +16,12 @@ Section refinement.
{Δ;Γ} !#l log (#l' <- #1;; !#l') : TNat.
Proof.
iIntros "Hl Hl'".
rel_store_r. rel_pure_r _.
rel_store_r. rel_seq_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 bitT : type := : TVar 0 × (TVar 0 TVar 0) × (TVar 0 Bool).
Definition bit_bool : val :=
pack (#true, (λ: "b", ¬ "b"), (λ: "b", "b")).
......@@ -37,22 +37,25 @@ Section refinement.
Instance R_persistent ww : Persistent (R ww).
Proof. apply _. Qed.
Lemma bit_prerefinement Δ Γ :
{Δ;Γ} bit_bool log bit_nat : bitτ.
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.
unfold bit_bool, bit_nat; simpl. (* we need this to compute the coercion from values to expression *)
unlock bit_bool bit_nat; simpl.
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].
- rel_arrow_val. simpl.
iIntros "!#" (v1 v2).
iIntros ([b [? ?]]); simplify_eq/=. unlock; simpl.
iIntros ([b [? ?]]); simplify_eq/=.
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.
- rel_arrow_val. simpl.
iIntros "!#" (v1 v2).
iIntros ([b [? ?]]); simplify_eq/=. unlock; simpl.
iIntros ([b [? ?]]); simplify_eq/=.
rel_rec_l. rel_rec_r.
rel_op_r.
destruct b; rel_finish.
......@@ -71,10 +74,10 @@ Section refinement.
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.
rel_arrow.
iIntros "!#" (f1 f2) "#Hf".
rel_let_l; rel_let_r.
iApply (bin_log_related_seq with "[Hf]"); auto.
iApply bin_log_related_seq; auto.
- iApply (bin_log_related_app with "Hf").
iApply bin_log_related_unit.
- rel_load_l_atomic;
......
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