diff options
| author |  Jason Gross <jgross@mit.edu> | 2018-04-18 15:54:11 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2018-04-18 15:54:11 -0400 |
| commit | 476cf88ac2279956ca496a67902235a5d0704812 (patch) | |
| tree | 488be119fb0e1a5250c42102e83d4b105627223d /src/Util/Option.v | |
| parent | e3dd9ae19ea08b8cbe3c6532ffb6b4d4e3e2ab38 (diff) | |
Fix a proof
Diffstat (limited to 'src/Util/Option.v')
| -rw-r--r-- | src/Util/Option.v | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/src/Util/Option.v b/src/Util/Option.v index 96014448b..b9e64910c 100644 --- a/src/Util/Option.v +++ b/src/Util/Option.v @@ -66,8 +66,11 @@ Lemma option_rect_false_returns_true_iff (f:T->bool) {Proper_f:Proper(R==>eq)f} (o:option T) : option_rect (fun _ => bool) f false o = true <-> exists s:T, option_eq R o (Some s) /\ f s = true. Proof. - unfold option_rect; break_match; repeat intuition (destruct_head ex; eauto); try discriminate. - { repeat esplit; simpl; easy. } + unfold option_rect; break_match; repeat intuition (destruct_head ex; eauto); + solve [ congruence + | repeat esplit; simpl; easy + | match goal with [H : f _ = true |- f _ = true ] => + solve [rewrite <- H; eauto] end ]. Qed. Lemma option_rect_false_returns_true_iff_eq |