diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-02-23 11:26:50 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-02-23 11:26:50 -0500 |
| commit | 49eefc7b82f4939e9cedf5363af2a889c666fdcb (patch) | |
| tree | e890ad91f28398a0346c553a33a16b818b237695 | |
| parent | aec88b301612febe75744b3ed2b2a128dddd498a (diff) | |
Add invert_Some; add nat_N_Z to push_Zof_N
| -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. |