Tactics.v 4.92 KB
Newer Older
1 2 3 4 5 6 7 8 9
(* Copyright (c) 2008, Adam Chlipala
 * 
 * This work is licensed under a
 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
 * Unported License.
 * The license text is available at:
 *   http://creativecommons.org/licenses/by-nc-nd/3.0/
 *)

10
Require Import Eqdep List.
11

Adam Chlipala's avatar
Adam Chlipala committed
12 13
Require Omega.

14 15
Set Implicit Arguments.

16

17
Ltac inject H := injection H; clear H; intros; try subst.
18

19 20 21 22 23 24 25 26
Ltac appHyps f :=
  match goal with
    | [ H : _ |- _ ] => f H
  end.

Ltac inList x ls :=
  match ls with
    | x => idtac
27
    | (_, x) => idtac
28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44
    | (?LS, _) => inList x LS
  end.

Ltac app f ls :=
  match ls with
    | (?LS, ?X) => f X || app f LS || fail 1
    | _ => f ls
  end.

Ltac all f ls :=
  match ls with
    | (?LS, ?X) => f X; all f LS
    | (_, _) => fail 1
    | _ => f ls
  end.

Ltac simplHyp invOne :=
45 46 47
  let invert H F :=
    inList F invOne; (inversion H; fail)
    || (inversion H; [idtac]; clear H; try subst) in
Adam Chlipala's avatar
Adam Chlipala committed
48
  match goal with
49 50
    | [ H : ex _ |- _ ] => destruct H

51 52
    | [ H : ?F _ = ?F _ |- _ ] => injection H;
      match goal with
53
        | [ |- _ = _ -> _ ] => try clear H; intros; try subst
54 55 56
      end
    | [ H : ?F _ _ = ?F _ _ |- _ ] => injection H;
      match goal with
57
        | [ |- _ = _ -> _ = _ -> _ ] => try clear H; intros; try subst
58
      end
59

60 61 62 63 64
    | [ H : ?F _ |- _ ] => invert H F
    | [ H : ?F _ _ |- _ ] => invert H F
    | [ H : ?F _ _ _ |- _ ] => invert H F
    | [ H : ?F _ _ _ _ |- _ ] => invert H F
    | [ H : ?F _ _ _ _ _ |- _ ] => invert H F
Adam Chlipala's avatar
Adam Chlipala committed
65 66
  end.

67 68 69 70 71 72 73 74 75 76 77
Ltac rewriteHyp :=
  match goal with
    | [ H : _ |- _ ] => rewrite H
  end.

Ltac rewriterP := repeat (rewriteHyp; autorewrite with cpdt in *).

Ltac rewriter := autorewrite with cpdt in *; rewriterP.

Hint Rewrite app_ass : cpdt.

78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111
Definition done (T : Type) (x : T) := True.

Ltac inster e trace :=
  match type of e with
    | forall x : _, _ =>
      match goal with
        | [ H : _ |- _ ] =>
          inster (e H) (trace, H)
        | _ => fail 2
      end
    | _ =>
      match trace with
        | (_, _) =>
          match goal with
            | [ H : done (trace, _) |- _ ] => fail 1
            | _ =>
              let T := type of e in
                match type of T with
                  | Prop =>
                    generalize e; intro;
                      assert (done (trace, tt)); [constructor | idtac]
                  | _ =>
                    all ltac:(fun X =>
                      match goal with
                        | [ H : done (_, X) |- _ ] => fail 1
                        | _ => idtac
                      end) trace;
                    let i := fresh "i" in (pose (i := e);
                      assert (done (trace, i)); [constructor | idtac])
                end
          end
      end
  end.

112 113 114 115 116
Ltac un_done :=
  repeat match goal with
           | [ H : done _ |- _ ] => clear H
         end.

117
Ltac crush' lemmas invOne :=
118
  let sintuition := simpl in *; intuition; try subst; repeat (simplHyp invOne; intuition; try subst); try congruence
119
    in (sintuition; rewriter;
120 121 122
      match lemmas with
        | false => idtac
        | _ => repeat ((app ltac:(fun L => inster L L) lemmas || appHyps ltac:(fun L => inster L L));
123 124 125
          repeat (simplHyp invOne; intuition)); un_done
      end; sintuition; try omega; try (elimtype False; omega)).

126
Ltac crush := crush' false fail.
127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165

Theorem dep_destruct : forall (T : Type) (T' : T -> Type) x (v : T' x) (P : T' x -> Prop),
  (forall x' (v' : T' x') (Heq : x' = x), P (match Heq in (_ = x) return (T' x) with
                                               | refl_equal => v'
                                             end))
  -> P v.
  intros.
  generalize (H _ v (refl_equal _)); trivial.
Qed.

Ltac dep_destruct E :=
  let doit A :=
    let T := type of A in
      generalize dependent E;
        let e := fresh "e" in
          intro e; pattern e;
            apply (@dep_destruct T);
              let x := fresh "x" with v := fresh "v"  in
                intros x v; destruct v; crush;
                  let bestEffort Heq E tac :=
                    repeat match goal with
                             | [ H : context[E] |- _ ] =>
                               match H with
                                 | Heq => fail 1
                                 | _ => generalize dependent H
                               end
                           end;
                    generalize Heq; tac Heq; clear Heq; intro Heq;
                      rewrite (UIP_refl _ _ Heq); intros in
                  repeat match goal with
                           | [ Heq : ?X = ?X |- _ ] =>
                             generalize (UIP_refl _ _ Heq); intro; subst; clear Heq
                           | [ Heq : ?E = _ |- _ ] => bestEffort Heq E ltac:(fun E => rewrite E)
                           | [ Heq : _ = ?E |- _ ] => bestEffort Heq E ltac:(fun E => rewrite <- E)
                         end
                  in match type of E with
                       | _ _ ?A => doit A
                       | _ ?A => doit A
                     end.