diff options
| author |  Jason Gross <jgross@mit.edu> | 2018-09-27 17:51:56 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2018-09-27 17:51:56 -0400 |
| commit | df57a6bea2fa2ccf14a280193741082b304b3925 (patch) | |
| tree | c26583b0e1eebdbdf9ccf70e0aaf1ec04d613cd6 /src/Util | |
| parent | c33a4250e81e47245b83f8793710d6270c2a1c58 (diff) | |
Add some option bind lemmas
Diffstat (limited to 'src/Util')
| -rw-r--r-- | src/Util/Option.v | 7 |
1 files changed, 7 insertions, 0 deletions
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) : |