Commit feb92c6e authored by Dan Frumin's avatar Dan Frumin

Clean up the bit refinement a bit

parent 737361de
......@@ -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.
......
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