From iris.proofmode Require Import tactics. From iris_logrel Require Import logrel examples.lock. Definition bitτ : type := (TExists (TProd (TProd (TVar 0) (TArrow (TVar 0) (TVar 0))) (TArrow (TVar 0) (TBool)))). Hint Unfold bitτ : typeable. Definition bit_bool : val := PackV (#true, (λ: "b", "b" ⊕ #true), (λ: "b", "b")). Definition flip_nat : val := λ: "n", if: "n" = #0 then #1 else #0. Definition bit_nat : val := PackV (#1, flip_nat, (λ: "b", "b" = #1)). (** * Typeability *) (** ** Boolean bit *) 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. Hint Resolve bit_bool_type : typeable. (** ** Integer bit *) 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 bit_nat_type : typeable. Section bit_refinement. Context `{logrelG Σ}. Variable (Δ : list (prodC valC valC -n> iProp Σ)). Definition bitf (b : bool) : nat := match b with | true => 1 | false => 0 end. (* This is the graph of the `bitf` function *) Program Definition bitτi : prodC valC valC -n> iProp Σ := λne vv, (∃ b : bool, ⌜vv.1 = #b⌝ ∗ ⌜vv.2 = #(bitf b)⌝)%I. Next Obligation. solve_proper. Qed. Instance bitτi_persistent ww : Persistent (bitτi ww). Proof. apply _. Qed. Lemma bit_prerefinement Γ : {Δ;Γ} ⊨ bit_bool ≤log≤ bit_nat : bitτ. Proof. unfold bit_bool, bit_nat; simpl. (* we need this to compute the coercion from values to expression *) iApply (bin_log_related_pack bitτi). repeat iApply bin_log_related_pair. - rel_vals; simpl; eauto. (* TODO: make a rel_finish tactic or change rel_vals *) - unfold flip_nat. 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_l. rel_op_r. destruct b; simpl; rel_if_r; rel_vals; simpl; eauto. - 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_vals; simpl; eauto. 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. Definition heapify : val := λ: "b", Unpack "b" \$ λ: "b'", let: "init" := Fst (Fst "b'") in let: "flip" := Snd (Fst "b'") in let: "view" := Snd "b'" in let: "x" := ref "init" in let: "l" := newlock #() in let: "flip_ref" := λ: <>, acquire "l";; "x" <- "flip" (!"x");; release "l" in let: "view_ref" := λ: <>, "view" (!"x") in Pack (#(), "flip_ref", "view_ref"). Lemma heapify_type Γ : typed Γ heapify (TArrow bitτ bitτ). Proof. unfold bitτ. unfold heapify. unlock. repeat (econstructor; solve_typed). (* TODO: solve_typed does not work by itself :( *) Qed. Hint Resolve heapify_type : typeable. Section heapify_refinement. Context `{logrelG Σ}. Variable (Δ : list (prodC valC valC -n> iProp Σ)). Notation D := (prodC valC valC -n> iProp Σ). Lemma heapify_refinement_ez Γ b1 b2 : {Δ;Γ} ⊨ b1 ≤log≤ b2 : bitτ -∗ {Δ;Γ} ⊨ heapify b1 ≤log≤ heapify b2 : bitτ. Proof. iIntros "Hb1b2". iApply bin_log_related_app; eauto. iApply binary_fundamental; eauto with typeable. Qed. End heapify_refinement. Theorem bit_heapify_ctx_refinement : ∅ ⊨ heapify bit_bool ≤ctx≤ heapify bit_nat : bitτ. Proof. eapply (logrel_ctxequiv logrelΣ); [solve_closed.. | intros ]. iStartProof. iApply heapify_refinement_ez; eauto. iApply bit_prerefinement. Qed.