+++ /dev/null
-Require Import Recursion.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.