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

diff --git a/Recursion/Tactics.v b/Recursion/Tactics.v
deleted file mode 100644
index bf441df..0000000
--- a/Recursion/Tactics.v
+++ /dev/null
@@ -1,39 +0,0 @@
-Require Import Recursion.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.