better comments/documentation

[coinductive-monad.git] / src / Computation / Tactics.v

diff --git a/src/Computation/Tactics.v b/src/Computation/Tactics.v
new file mode 100644 (file)
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.