Require Import Computation.Monad. (* decomposition lemma *) Definition decomp (A:Set)(c:#A) : #A := match c with | Return x => Return x | Bind B f c => Bind f c end. Implicit Arguments decomp. (* decomposition theorem: we can always decompose *) Theorem decomp_thm : forall (A:Set)(c:#A), c = decomp c. intros A l; case l; simpl; trivial. Qed. (* 1-, 2-, 3-, 4-, and 5-ary decompositions *) Ltac uncomp comp := match goal with | [ |- context[(comp ?X)] ] => pattern (comp X) at 1; rewrite decomp_thm; simpl | [ |- context[(comp ?X ?Y)] ] => pattern (comp X Y) at 1; rewrite decomp_thm; simpl | [ |- context[(comp ?X ?Y ?Z)] ] => pattern (comp X Y Z) at 1; rewrite decomp_thm; simpl | [ |- context[(comp ?X ?Y ?Z ?R)] ] => pattern (comp X Y Z R) at 1; rewrite decomp_thm; simpl | [ |- context[(comp ?X ?Y ?Z ?R ?Q)] ] => pattern (comp X Y Z R Q) at 1; rewrite decomp_thm; simpl end.