From df57a6bea2fa2ccf14a280193741082b304b3925 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 27 Sep 2018 17:51:56 -0400 Subject: Add some option bind lemmas --- src/Util/Option.v | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'src/Util') diff --git a/src/Util/Option.v b/src/Util/Option.v index 5d53223c2..7a9923d69 100644 --- a/src/Util/Option.v +++ b/src/Util/Option.v @@ -116,6 +116,13 @@ Global Instance Proper_option_rect_nd_changevalue : Proper (RB ==> option_eq RA ==> RB) (@option_rect A (fun _ => B) some). Proof. cbv; repeat (intro || break_match || f_equiv || intuition congruence). Qed. +Lemma bind_zero_l {A B} f : @bind A B None f = None. +Proof. reflexivity. Qed. +Lemma bind_zero_r {A B} v : @bind A B v (fun _ => None) = None. +Proof. destruct v; reflexivity. Qed. +Lemma bind_zero_r_ext {A B} v f : (forall v, f v = None) -> @bind A B v f = None. +Proof. destruct v; cbn; auto. Qed. + Lemma option_rect_false_returns_true_iff {T} {R} {reflexiveR:Reflexive R} (f:T->bool) {Proper_f:Proper(R==>eq)f} (o:option T) : -- cgit v1.2.3