Commit 7b70c9db authored by Dan Frumin's avatar Dan Frumin

Simplify the bit proof a bit

parent 4f7441e0
From iris.proofmode Require Import tactics. (* Always import this first? *)
From iris.algebra Require Import agree.
From iris_logrel.F_mu_ref_conc Require Import tactics rel_tactics soundness_binary relational_properties.
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))).
Hint Unfold bitτ : typeable.
Definition bit_bool : val :=
PackV ((λ: "b", "b"), (λ: "b", "b" true), #v true).
......@@ -16,18 +20,19 @@ Definition flip_nat : val := λ: "n",
Definition bit_nat : val :=
PackV ((λ: "b", "b" = 0), flip_nat, #nv 0).
(** * 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 Γ :
......@@ -37,15 +42,21 @@ Proof.
simpl. unlock.
solve_typed.
Qed.
Hint Resolve bit_nat_type : typeable.
Section bit_refinement.
Context `{logrelG Σ}.
Context `{HagΣ: inG Σ (agreeR natC)}.
Variable (Δ : list (prodC valC valC -n> iProp Σ)).
Hint Resolve bit_nat_type : typeable.
Definition bitf (b : bool) : nat :=
match b with
| true => 0
| false => 1
end.
Program Definition bitτi : prodC valC valC -n> iProp Σ := λne vv,
(vv.1 = #v true vv.2 = #nv 0 vv.1 = #v false vv.2 = #nv 1)%I.
( b, vv.1 = #v b vv.2 = #nv (bitf b))%I.
Next Obligation. solve_proper. Qed.
Instance bitτi_persistent ww : PersistentP (bitτi ww).
......@@ -56,27 +67,25 @@ Section bit_refinement.
Proof.
simpl.
iApply (bin_log_related_pack _ bitτi).
iApply bin_log_related_pair.
iApply bin_log_related_pair.
repeat iApply bin_log_related_pair.
- iApply bin_log_related_arrow; try by unlock.
iAlways. iIntros ([v1 v2]) "/= #%".
iAlways. iIntros ([v1 v2]) "/= #Hi".
iDestruct "Hi" as (b) "[% %]"; simplify_eq.
unlock.
rel_rec_l.
rel_rec_r.
destruct H0 as [Hv | Hv]; inversion Hv; subst; clear.
(* ^ TODO simplify_eq does not work *)
all: rel_op_r.
all: rel_vals; simpl; eauto.
rel_op_r.
rel_vals; destruct b; simpl; eauto.
- unfold flip_nat.
iApply bin_log_related_arrow; try by unlock.
iAlways. iIntros ([v1 v2]) "/= #%".
iAlways. iIntros ([v1 v2]) "/= #Hi".
iDestruct "Hi" as (b) "[% %]"; simplify_eq.
unlock.
rel_rec_l.
rel_rec_r.
destruct H0 as [Hv | Hv]; inversion Hv; subst; clear.
(* ^ TODO simplify_eq does not work *)
all: rel_op_l; simpl.
all: rel_op_r; simpl.
rel_op_l; simpl.
rel_op_r; simpl.
destruct b; simpl.
+ rel_if_true_r. rel_vals; simpl; eauto.
+ rel_if_false_r. rel_vals; simpl; eauto.
- rel_vals; simpl; eauto.
......
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