X-Git-Url: http://git.megacz.com/?p=coinductive-monad.git;a=blobdiff_plain;f=Computation%2FTactics.v;fp=Computation%2FTactics.v;h=c7108178300e1528c74510d17f73b8e4639e76e6;hp=0000000000000000000000000000000000000000;hb=ad8905d391e4e2015b6525a81a3b5e1ad607439e;hpb=7439e43c33a10817e19e7a5f26435d2097dc262d

diff --git a/Computation/Tactics.v b/Computation/Tactics.v
new file mode 100644
index 0000000..c710817
--- /dev/null
+++ b/Computation/Tactics.v
@@ -0,0 +1,39 @@
+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.