diff --git a/theories/examples/bit.v b/theories/examples/bit.v index d630d25be97908600d4c735549a76a314254a2da..b5f8fac90c70f39af0bddd00c74fb7599d06ed15 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.