diff options
author | Jason Gross <jgross@mit.edu> | 2018-02-17 12:24:35 -0500 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2018-02-17 12:24:35 -0500 |
commit | dca499851304f78831476f6f7706f942b38e761d (patch) | |
tree | be083431431d21f95779ed849d9e213b25bd1a0c /src/Util | |
parent | 770646a916c9feb8333340b655c0ba4142b755a4 (diff) |
Add always_invert_Some
Diffstat (limited to 'src/Util')
-rw-r--r-- | src/Util/Option.v | 32 |
1 files changed, 32 insertions, 0 deletions
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 |