Commit da7d64da authored by Ralf Jung's avatar Ralf Jung

adjust for lemma names in std++

parent 2d6dcfd9
......@@ -185,12 +185,6 @@ Proof. rewrite /is_safe /reducible /=. eauto 10 using head_prim_step. Qed.
Lemma prim_step_safe e σ κ e' σ' efs : prim_step e σ κ e' σ' efs is_safe e σ.
Proof. rewrite /is_safe /reducible /=. eauto 10. Qed.
(* FIXME move to std++ *)
Lemma bool_decide_true' P `{!Decision P}: bool_decide P = true P.
Proof. intros Heq. eapply bool_decide_unpack. rewrite Heq //. Qed.
Lemma bool_decide_false' P `{!Decision P}: bool_decide P = false ¬P.
Proof. move=> Heq /bool_decide_spec HP. destruct (bool_decide P); done. Qed.
Lemma val_is_unboxed_erased v :
val_is_unboxed (erase_val v) val_is_unboxed v.
Proof.
......@@ -204,7 +198,7 @@ Lemma vals_compare v1 v2 :
bool_decide (vals_compare_safe v1 v2) = true
(v1 = v2) (erase_val v1 = erase_val v2).
Proof.
move=> /bool_decide_true'.
move=> /bool_decide_true_2.
destruct v1, v2; rewrite /= /lit_is_unboxed;
repeat (done || (by intros [[] | []]) || simpl; case_match).
Qed.
......@@ -222,9 +216,9 @@ Lemma decide_vals_compare_safe_contradiction v1 b1 v2 b2 :
False.
Proof.
intros.
destruct b1, b2; try done; (eapply bool_decide_false'; first done);
destruct b1, b2; try done; (eapply bool_decide_false_2; first done);
apply vals_compare_safe_erase;
eapply bool_decide_true'; done.
eapply bool_decide_true_2; done.
Qed.
(** if un_op_eval succeeds on erased value,
......
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