Computation/Tactics.v

   1 Require Import Computation.Monad.
   2
   3 (* decomposition lemma *)
   4 Definition decomp (A:Set)(c:#A) : #A :=
   5   match c with
   6     | Return x => Return x
   7     | Bind B f c => Bind f c
   8   end.
   9 Implicit Arguments decomp.
  10
  11 (* decomposition theorem: we can always decompose *)
  12 Theorem decomp_thm : forall (A:Set)(c:#A), c = decomp c.
  13   intros A l; case l; simpl; trivial.
  14 Qed.
  15
  16 (* 1-, 2-, 3-, 4-, and 5-ary decompositions *)
  17 Ltac uncomp comp :=
  18   match goal with
  19     | [ |- context[(comp ?X)] ] =>
  20       pattern (comp X) at 1;
  21       rewrite decomp_thm;
  22       simpl
  23     | [ |- context[(comp ?X ?Y)] ] =>
  24       pattern (comp X Y) at 1;
  25       rewrite decomp_thm;
  26       simpl
  27     | [ |- context[(comp ?X ?Y ?Z)] ] =>
  28       pattern (comp X Y Z) at 1;
  29       rewrite decomp_thm;
  30       simpl
  31     | [ |- context[(comp ?X ?Y ?Z ?R)] ] =>
  32       pattern (comp X Y Z R) at 1;
  33       rewrite decomp_thm;
  34       simpl
  35     | [ |- context[(comp ?X ?Y ?Z ?R ?Q)] ] =>
  36       pattern (comp X Y Z R Q) at 1;
  37       rewrite decomp_thm;
  38       simpl
  39   end.