From 49eefc7b82f4939e9cedf5363af2a889c666fdcb Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 23 Feb 2017 11:26:50 -0500 Subject: Add invert_Some; add nat_N_Z to push_Zof_N --- src/Util/Option.v | 9 +++++++++ 1 file changed, 9 insertions(+) (limited to 'src/Util/Option.v') 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 _)). -- cgit v1.2.3