From 58c3a75f9a15d1a9345b6fda72e943ee175aa768 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 14 Jun 2012 11:28:07 +0200
Subject: [PATCH] Add a tactic to simplify expressions in the option monad.

---
 theories/option.v | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/theories/option.v b/theories/option.v
index 5f61dbeb..3fbbf81a 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -129,6 +129,18 @@ Instance option_join: MJoin option := λ A x,
   end.
 Instance option_fmap: FMap option := @option_map.
 
+Ltac simplify_options := repeat
+  match goal with
+  | _ => progress simplify_eqs
+  | H : mbind (M:=option) ?f ?o = ?x |- _ =>
+    change (option_bind _ _ f o = x) in H;
+    destruct o; simpl in H; try discriminate
+  | H : context [ ?o = _ ] |- mbind (M:=option) ?f ?o = ?x =>
+    change (option_bind _ _ f o = x);
+    erewrite H by eauto;
+    simpl
+  end.
+
 Lemma option_fmap_is_Some {A B} (f : A → B) (x : option A) : is_Some x ↔ is_Some (f <$> x).
 Proof. destruct x; split; intros [??]; subst; compute; eauto; discriminate. Qed.
 Lemma option_fmap_is_None {A B} (f : A → B) (x : option A) : x = None ↔ f <$> x = None.
-- 
GitLab