From feb92c6e1855216126e1ac5f27ae2ae564c45581 Mon Sep 17 00:00:00 2001 From: Dan Frumin Date: Sat, 2 Dec 2017 21:05:56 +0100 Subject: [PATCH] Clean up the bit refinement a bit --- theories/examples/bit.v | 28 ++++++++++++---------------- 1 file changed, 12 insertions(+), 16 deletions(-) diff --git a/theories/examples/bit.v b/theories/examples/bit.v index d630d25..b5f8fac 100644 --- a/theories/examples/bit.v +++ b/theories/examples/bit.v @@ -60,30 +60,26 @@ Section bit_refinement. Instance bitτi_persistent ww : Persistent (bitτi ww). Proof. apply _. Qed. - Lemma bit_prerefinement Γ E1 : - {E1,E1;Δ;Γ} ⊨ bit_bool ≤log≤ bit_nat : bitτ. + Lemma bit_prerefinement Γ E : + {E;Δ;Γ} ⊨ 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. + - 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. - iAlways. iIntros (v1 v2) "/= #Hi". - iDestruct "Hi" as (b) "[% %]"; simplify_eq. - unlock. - rel_rec_l. - rel_rec_r. - rel_op_l; simpl. - rel_op_r; simpl. + 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. - iAlways. iIntros (v1 v2) "/= Hi". - iDestruct "Hi" as (b) "[% %]"; simplify_eq. - unlock. - rel_rec_l. - rel_rec_r. + iIntros "!#" (v1 v2) "/=". (* TODO: notation for LitV? *) + iIntros ([b [? ?]]); simplify_eq/=. unlock; simpl. + rel_rec_l. rel_rec_r. rel_op_r. - rel_vals; destruct b; simpl; eauto. + destruct b; rel_vals; simpl; eauto. Qed. End bit_refinement. -- GitLab