(** the option monad (for partial functions) *) Definition bind {A B:Type} (v:option A)(f:A->option B) : option B := match v with Some x => f x | None => None end. Notation "x '<-' e1 ; e2 " := (bind e1 (fun x => e2)) (right associativity, at level 60). (** binding a pair of variables *) Definition bind2 {A B C:Type}(v:option(A*B)) (f: A->B->option C) :option C:= match v with Some(a,b) => f a b | None => None end. Notation "x ',,' y '<-2' e1 ; e2 " := (bind2 e1 (fun x y => e2)) (right associativity, at level 60). Lemma bind_decompose {A B:Type} {v:option A}{f:A->option B} {b}: bind v f = Some b -> exists x, v = Some x /\ f x = Some b. Proof. intros; destruct v. simpl in H. exists a;auto. simpl in H. discriminate. Qed. Ltac unbind H x Hx Hfx:= destruct (bind_decompose H) as [x [Hx Hfx]]. Require Import Arith. Goal forall on i , x <- on ; Some (S x) = Some i -> i > 0. intros. unbind H x Hx H8. injection H8. intro;subst i;auto with arith. Qed. Ltac find_deep_bind a := match a with bind ?a _ => find_deep_bind a | bind2 ?a _ => find_deep_bind a | _ => a end. (** the following tactic works on an hypothesis H : v <-- e1; e2 = Some r unbind_hyp H x H0 decomposes H into : x : B H : e2 [x/v] = Some r H0 : e1 = Some x Similar Behvior with bind2 *) Ltac unbind_hyp H v Heq := match type of H with | bind ?a ?b = Some _ => let c := find_deep_bind a in (case_eq c; [intros v Heq | intros Heq]; rewrite Heq in H; [simpl in H | discriminate H]) | bind2 ?a ?b = Some _ => let c := find_deep_bind a in case_eq c; [intros v Heq | intros Heq]; rewrite Heq in H; [simpl in H | discriminate H] end.