Commit 80dd7f76 authored by Dan Frumin's avatar Dan Frumin

Contextual refinement for the bit example

parent cce140f7
From iris.proofmode Require Import tactics.
From iris.algebra Require Import auth.
From iris.base_logic Require Import lib.auth.
From iris_logrel.F_mu_ref_conc Require Export examples.lock.
From iris_logrel.F_mu_ref_conc Require Import tactics rel_tactics soundness_binary relational_properties.
From iris.program_logic Require Import adequacy.
From iris_logrel.F_mu_ref_conc Require Import hax.
Definition bitτ : type :=
(TExists (TProd (TProd (TArrow (TVar 0) (TBool))
(TArrow (TVar 0) (TVar 0)))
(TVar 0))).
Definition bit_bool : val :=
PackV ((λ: "b", "b"), (λ: "b", BinOp Xor "b" (#v true)), #v true).
......@@ -17,35 +16,31 @@ Definition flip_nat : val := λ: "n",
Definition bit_nat : val :=
PackV ((λ: "b", BinOp Eq "b" (#n 0)), flip_nat, #nv 0).
Section bit_refinement.
Context `{logrelG Σ}.
Variable (Δ : list (prodC valC valC -n> iProp Σ)).
Definition bitτ : type :=
(TExists (TProd (TProd (TArrow (TVar 0) (TBool))
(TArrow (TVar 0) (TVar 0)))
(TVar 0))).
Lemma bit_bool_type Γ :
Lemma bit_bool_type Γ :
typed Γ bit_bool bitτ.
Proof. unfold bitτ. simpl. unlock. solve_typed.
(* TODO: solve_typed does not solve this one without simplifying/unlocking *)
Qed.
Proof. unfold bitτ. simpl. unlock. solve_typed.
(* TODO: solve_typed does not solve this one without simplifying/unlocking *)
Qed.
Hint Resolve bit_bool_type : typeable.
Hint Resolve bit_bool_type : typeable.
Lemma flip_nat_type Γ :
typed Γ flip_nat (TArrow TNat TNat).
Proof. solve_typed. Qed.
Lemma flip_nat_type Γ :
typed Γ flip_nat (TArrow TNat TNat).
Proof. solve_typed. Qed.
Hint Resolve flip_nat_type : typeable.
Lemma bit_nat_type Γ :
typed Γ bit_nat bitτ.
Proof.
unfold bitτ.
simpl. unlock.
solve_typed.
Qed.
Hint Resolve flip_nat_type : typeable.
Lemma bit_nat_type Γ :
typed Γ bit_nat bitτ.
Proof.
unfold bitτ.
simpl. unlock.
solve_typed.
Qed.
Section bit_refinement.
Context `{logrelG Σ}.
Variable (Δ : list (prodC valC valC -n> iProp Σ)).
Hint Resolve bit_nat_type : typeable.
......@@ -88,3 +83,10 @@ Section bit_refinement.
Qed.
End bit_refinement.
Theorem bit_ctx_refinement :
bit_bool ctx bit_nat : bitτ.
Proof.
eapply (logrel_ctxequiv logrelΣ); [solve_closed.. | intros ].
apply bit_prerefinement.
Qed.
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