1 Require Import Computation.Monad.
3 (* decomposition lemma *)
4 Definition decomp (A:Set)(c:#A) : #A :=
7 | Bind B f c => Bind f c
9 Implicit Arguments decomp.
11 (* decomposition theorem: we can always decompose *)
12 Theorem decomp_thm : forall (A:Set)(c:#A), c = decomp c.
13 intros A l; case l; simpl; trivial.
16 (* 1-, 2-, 3-, 4-, and 5-ary decompositions *)
19 | [ |- context[(comp ?X)] ] =>
20 pattern (comp X) at 1;
23 | [ |- context[(comp ?X ?Y)] ] =>
24 pattern (comp X Y) at 1;
27 | [ |- context[(comp ?X ?Y ?Z)] ] =>
28 pattern (comp X Y Z) at 1;
31 | [ |- context[(comp ?X ?Y ?Z ?R)] ] =>
32 pattern (comp X Y Z R) at 1;
35 | [ |- context[(comp ?X ?Y ?Z ?R ?Q)] ] =>
36 pattern (comp X Y Z R Q) at 1;