diff options
-rw-r--r-- | src/Util/Option.v | 9 | ||||
-rw-r--r-- | src/Util/ZUtil.v | 2 |
2 files changed, 10 insertions, 1 deletions
diff --git a/src/Util/Option.v b/src/Util/Option.v index c67efcb1a..c26d6cca3 100644 --- a/src/Util/Option.v +++ b/src/Util/Option.v @@ -138,6 +138,15 @@ Proof. rewrite <- (option_leq_to_eq_to_leq p), <- (option_leq_to_eq_to_leq q); simpl; reflexivity. Qed. +Definition invert_Some {A} (x : option A) : match x with + | Some _ => A + | None => unit + end + := match x with + | Some x' => x' + | None => tt + end. + Lemma invert_eq_Some {A x y} (p : Some x = Some y) : { pf : x = y | @option_eq_to_leq A (Some x) (Some y) pf = p }. Proof. refine (exist _ _ (option_leq_to_eq_to_leq _)). diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 581ced889..04638a0c8 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -132,7 +132,7 @@ Hint Rewrite Nat2Z.id N2Z.id : zsimplify. Hint Rewrite Nat2Z.id : push_Zof_nat. Hint Rewrite N2Z.id : push_Zto_N. Hint Rewrite N2Z.id : pull_Zof_N. -Hint Rewrite N2Z.inj_pos N2Z.inj_abs_N N2Z.inj_add N2Z.inj_mul N2Z.inj_sub_max N2Z.inj_succ N2Z.inj_pred_max N2Z.inj_min N2Z.inj_max N2Z.inj_div N2Z.inj_quot N2Z.inj_rem N2Z.inj_div2 N2Z.inj_pow N2Z.inj_0 : push_Zof_N. +Hint Rewrite N2Z.inj_pos N2Z.inj_abs_N N2Z.inj_add N2Z.inj_mul N2Z.inj_sub_max N2Z.inj_succ N2Z.inj_pred_max N2Z.inj_min N2Z.inj_max N2Z.inj_div N2Z.inj_quot N2Z.inj_rem N2Z.inj_div2 N2Z.inj_pow N2Z.inj_0 nat_N_Z : push_Zof_N. Hint Rewrite N2Z.inj_compare N2Z.inj_testbit : pull_Zof_N. Hint Rewrite <- N2Z.inj_abs_N N2Z.inj_add N2Z.inj_mul N2Z.inj_sub_max N2Z.inj_succ N2Z.inj_pred_max N2Z.inj_min N2Z.inj_max N2Z.inj_div N2Z.inj_quot N2Z.inj_rem N2Z.inj_div2 N2Z.inj_pow : pull_Zof_N. Hint Rewrite Nat2Z.inj_0 Nat2Z.inj_succ Nat2Z.inj_abs_nat Nat2Z.inj_add Nat2Z.inj_mul Nat2Z.inj_sub_max Nat2Z.inj_pred_max Nat2Z.inj_min Nat2Z.inj_max Zabs2Nat.id_abs Zabs2Nat.id : push_Zof_nat. |