add TODO list
[coinductive-monad.git] / Computation / Tactics.v
1 Require Import Computation.Monad.
2
3 (* decomposition lemma *)
4 Definition decomp (A:Set)(c:#A) : #A := 
5   match c with
6     | Return x => Return x
7     | Bind B f c => Bind f c
8   end.
9 Implicit Arguments decomp.
10
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. 
14 Qed. 
15
16 (* 1-, 2-, 3-, 4-, and 5-ary decompositions *)
17 Ltac uncomp comp :=
18   match goal with
19     | [ |- context[(comp ?X)] ] =>
20       pattern (comp X) at 1;
21       rewrite decomp_thm;
22       simpl
23     | [ |- context[(comp ?X ?Y)] ] =>
24       pattern (comp X Y) at 1;
25       rewrite decomp_thm;
26       simpl
27     | [ |- context[(comp ?X ?Y ?Z)] ] =>
28       pattern (comp X Y Z) at 1;
29       rewrite decomp_thm;
30       simpl
31     | [ |- context[(comp ?X ?Y ?Z ?R)] ] =>
32       pattern (comp X Y Z R) at 1;
33       rewrite decomp_thm;
34       simpl
35     | [ |- context[(comp ?X ?Y ?Z ?R ?Q)] ] =>
36       pattern (comp X Y Z R Q) at 1;
37       rewrite decomp_thm;
38       simpl
39   end.