From dca499851304f78831476f6f7706f942b38e761d Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sat, 17 Feb 2018 12:24:35 -0500 Subject: Add always_invert_Some --- src/Util/Option.v | 32 ++++++++++++++++++++++++++++++++ 1 file changed, 32 insertions(+) (limited to 'src/Util/Option.v') diff --git a/src/Util/Option.v b/src/Util/Option.v index a5b19ae4a..851421bed 100644 --- a/src/Util/Option.v +++ b/src/Util/Option.v @@ -172,6 +172,38 @@ Proof. refine (exist _ _ (option_leq_to_eq_to_leq _)). Qed. +Definition always_invert_Some {A} (x : option A) (pf : x <> None) : A + := match x return x <> None -> A with + | Some v => fun _ => v + | None => fun pf => False_rect _ (pf eq_refl) + end pf. + +Lemma push_always_invert_Some' {A B} (f : A -> B) (x : option A) + (pf : x <> None) + (pf' : option_map f x <> None) + : f (always_invert_Some x pf) = always_invert_Some (option_map f x) pf'. +Proof. + destruct x; [ reflexivity | congruence ]. +Qed. + +Definition pull_always_invert_Some {A B} (f : A -> B) (x : option A) + (pf : option_map f x <> None) + : f (always_invert_Some x (fun H => pf (f_equal (option_map f) H))) + = always_invert_Some (option_map f x) pf + := push_always_invert_Some' f x _ pf. + +Lemma option_map_neq_None_iff {A B} (f : A -> B) x + : x <> None <-> option_map f x <> None. +Proof. destruct x; cbn in *; split; congruence. Qed. + +Definition push_always_invert_Some {A B} (f : A -> B) (x : option A) + (pf : x <> None) + : f (always_invert_Some x pf) + = always_invert_Some (option_map f x) + (proj1 (option_map_neq_None_iff f x) pf) + := push_always_invert_Some' f x pf _. + + Ltac inversion_option_step := match goal with | [ H : Some _ = Some _ |- _ ] => apply option_leq_to_eq in H; unfold option_eq in H -- cgit v1.2.3