X-Git-Url: http://git.megacz.com/?p=coinductive-monad.git;a=blobdiff_plain;f=src%2FComputation%2FTactics.v;fp=src%2FComputation%2FTactics.v;h=67ed175a2318b6d581450273b556f1e6e6b35cbe;hp=0000000000000000000000000000000000000000;hb=1ff31872c2b89ffb4c6c6250b1d51436b6b1400f;hpb=bb471fbb694313a6aa61816752bd179b3af6711d

diff --git a/src/Computation/Tactics.v b/src/Computation/Tactics.v
new file mode 100644
index 0000000..67ed175
--- /dev/null
+++ b/src/Computation/Tactics.v
@@ -0,0 +1,39 @@
+Require Import Computation.Monad.
+
+(** A 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.
+
+(** A 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; you should use this *)
+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.