better comments/documentation

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

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