Mercurial > cpdt > repo

annotate src/Tactics.v @ 199:cadeb49dc1ef

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fix typo
author Adam Chlipala <adamc@hcoop.net>
date Mon, 01 Dec 2008 08:32:20 -0500
parents 699fd70c04a7
children df289eb8ef76
rev   line source
adamc@2 1 (* Copyright (c) 2008, Adam Chlipala
adamc@2 2 *
adamc@2 3 * This work is licensed under a
adamc@2 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
adamc@2 5 * Unported License.
adamc@2 6 * The license text is available at:
adamc@2 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
adamc@2 8 *)
adamc@2 9
adamc@85 10 Require Import Eqdep List.
adamc@2 11
adamc@38 12 Require Omega.
adamc@38 13
adamc@59 14 Set Implicit Arguments.
adamc@59 15
adamc@2 16
adamc@66 17 Ltac inject H := injection H; clear H; intros; try subst.
adamc@51 18
adamc@59 19 Ltac appHyps f :=
adamc@50 20 match goal with
adamc@59 21 | [ H : _ |- _ ] => f H
adamc@59 22 end.
adamc@59 23
adamc@59 24 Ltac inList x ls :=
adamc@59 25 match ls with
adamc@59 26 | x => idtac
adamc@84 27 | (_, x) => idtac
adamc@59 28 | (?LS, _) => inList x LS
adamc@59 29 end.
adamc@59 30
adamc@59 31 Ltac app f ls :=
adamc@59 32 match ls with
adamc@59 33 | (?LS, ?X) => f X || app f LS || fail 1
adamc@59 34 | _ => f ls
adamc@59 35 end.
adamc@59 36
adamc@59 37 Ltac all f ls :=
adamc@59 38 match ls with
adamc@59 39 | (?LS, ?X) => f X; all f LS
adamc@59 40 | (_, _) => fail 1
adamc@59 41 | _ => f ls
adamc@59 42 end.
adamc@59 43
adamc@59 44 Ltac simplHyp invOne :=
adamc@99 45 let invert H F :=
adamc@99 46 inList F invOne; (inversion H; fail)
adamc@99 47 || (inversion H; [idtac]; clear H; try subst) in
adamc@59 48 match goal with
adamc@59 49 | [ H : ex _ |- _ ] => destruct H
adamc@59 50
adamc@160 51 | [ H : ?F ?X = ?F ?Y |- _ ] => injection H;
adamc@51 52 match goal with
adamc@160 53 | [ |- F X = F Y -> _ ] => fail 1
adamc@85 54 | [ |- _ = _ -> _ ] => try clear H; intros; try subst
adamc@51 55 end
adamc@51 56 | [ H : ?F _ _ = ?F _ _ |- _ ] => injection H;
adamc@51 57 match goal with
adamc@85 58 | [ |- _ = _ -> _ = _ -> _ ] => try clear H; intros; try subst
adamc@51 59 end
adamc@59 60
adamc@99 61 | [ H : ?F _ |- _ ] => invert H F
adamc@99 62 | [ H : ?F _ _ |- _ ] => invert H F
adamc@99 63 | [ H : ?F _ _ _ |- _ ] => invert H F
adamc@99 64 | [ H : ?F _ _ _ _ |- _ ] => invert H F
adamc@99 65 | [ H : ?F _ _ _ _ _ |- _ ] => invert H F
adamc@176 66
adamc@176 67 | [ H : existT _ ?T _ = existT _ ?T _ |- _ ] => generalize (inj_pair2 _ _ _ _ _ H); clear H
adamc@176 68 | [ H : existT _ _ _ = existT _ _ _ |- _ ] => inversion H; clear H
adamc@179 69
adamc@179 70 | [ H : Some _ = Some _ |- _ ] => injection H; clear H
adamc@50 71 end.
adamc@50 72
adamc@2 73 Ltac rewriteHyp :=
adamc@2 74 match goal with
adamc@183 75 | [ H : _ |- _ ] => rewrite H; auto; [idtac]
adamc@2 76 end.
adamc@2 77
adamc@2 78 Ltac rewriterP := repeat (rewriteHyp; autorewrite with cpdt in *).
adamc@2 79
adamc@2 80 Ltac rewriter := autorewrite with cpdt in *; rewriterP.
adamc@2 81
adamc@2 82 Hint Rewrite app_ass : cpdt.
adamc@2 83
adamc@59 84 Definition done (T : Type) (x : T) := True.
adamc@2 85
adamc@59 86 Ltac inster e trace :=
adamc@59 87 match type of e with
adamc@59 88 | forall x : _, _ =>
adamc@59 89 match goal with
adamc@59 90 | [ H : _ |- _ ] =>
adamc@59 91 inster (e H) (trace, H)
adamc@59 92 | _ => fail 2
adamc@59 93 end
adamc@59 94 | _ =>
adamc@59 95 match trace with
adamc@59 96 | (_, _) =>
adamc@59 97 match goal with
adamc@59 98 | [ H : done (trace, _) |- _ ] => fail 1
adamc@59 99 | _ =>
adamc@59 100 let T := type of e in
adamc@59 101 match type of T with
adamc@59 102 | Prop =>
adamc@59 103 generalize e; intro;
adamc@59 104 assert (done (trace, tt)); [constructor | idtac]
adamc@59 105 | _ =>
adamc@59 106 all ltac:(fun X =>
adamc@59 107 match goal with
adamc@59 108 | [ H : done (_, X) |- _ ] => fail 1
adamc@59 109 | _ => idtac
adamc@59 110 end) trace;
adamc@59 111 let i := fresh "i" in (pose (i := e);
adamc@59 112 assert (done (trace, i)); [constructor | idtac])
adamc@59 113 end
adamc@59 114 end
adamc@59 115 end
adamc@59 116 end.
adamc@59 117
adamc@65 118 Ltac un_done :=
adamc@65 119 repeat match goal with
adamc@65 120 | [ H : done _ |- _ ] => clear H
adamc@65 121 end.
adamc@65 122
adamc@88 123 Ltac crush' lemmas invOne :=
adamc@184 124 let sintuition := simpl in *; intuition; try subst; repeat (simplHyp invOne; intuition; try subst); try congruence in
adamc@184 125 let rewriter := autorewrite with cpdt in *;
adamc@184 126 repeat (match goal with
adamc@184 127 | [ H : _ |- _ ] => (rewrite H; [])
adamc@184 128 || (rewrite H; [ | solve [ crush' lemmas invOne ] ])
adamc@184 129 || (rewrite H; [ | solve [ crush' lemmas invOne ] | solve [ crush' lemmas invOne ] ])
adamc@184 130 end; autorewrite with cpdt in *)
adamc@184 131 in (sintuition; rewriter;
adamc@183 132 match lemmas with
adamc@183 133 | false => idtac
adamc@183 134 | _ => repeat ((app ltac:(fun L => inster L L) lemmas || appHyps ltac:(fun L => inster L L));
adamc@183 135 repeat (simplHyp invOne; intuition)); un_done
adamc@184 136 end; sintuition; rewriter; sintuition; try omega; try (elimtype False; omega)).
adamc@59 137
adamc@88 138 Ltac crush := crush' false fail.
adamc@85 139
adamc@85 140 Theorem dep_destruct : forall (T : Type) (T' : T -> Type) x (v : T' x) (P : T' x -> Prop),
adamc@85 141 (forall x' (v' : T' x') (Heq : x' = x), P (match Heq in (_ = x) return (T' x) with
adamc@85 142 | refl_equal => v'
adamc@85 143 end))
adamc@85 144 -> P v.
adamc@85 145 intros.
adamc@85 146 generalize (H _ v (refl_equal _)); trivial.
adamc@85 147 Qed.
adamc@85 148
adamc@85 149 Ltac dep_destruct E :=
adamc@85 150 let doit A :=
adamc@85 151 let T := type of A in
adamc@85 152 generalize dependent E;
adamc@85 153 let e := fresh "e" in
adamc@85 154 intro e; pattern e;
adamc@85 155 apply (@dep_destruct T);
adamc@85 156 let x := fresh "x" with v := fresh "v" in
adamc@85 157 intros x v; destruct v; crush;
adamc@85 158 let bestEffort Heq E tac :=
adamc@85 159 repeat match goal with
adamc@85 160 | [ H : context[E] |- _ ] =>
adamc@85 161 match H with
adamc@85 162 | Heq => fail 1
adamc@85 163 | _ => generalize dependent H
adamc@85 164 end
adamc@85 165 end;
adamc@85 166 generalize Heq; tac Heq; clear Heq; intro Heq;
adamc@85 167 rewrite (UIP_refl _ _ Heq); intros in
adamc@85 168 repeat match goal with
adamc@85 169 | [ Heq : ?X = ?X |- _ ] =>
adamc@85 170 generalize (UIP_refl _ _ Heq); intro; subst; clear Heq
adamc@85 171 | [ Heq : ?E = _ |- _ ] => bestEffort Heq E ltac:(fun E => rewrite E)
adamc@85 172 | [ Heq : _ = ?E |- _ ] => bestEffort Heq E ltac:(fun E => rewrite <- E)
adamc@85 173 end
adamc@85 174 in match type of E with
adamc@173 175 | _ ?A => doit A
adamc@85 176 | _ _ ?A => doit A
adamc@173 177 | _ _ _ ?A => doit A
adamc@85 178 end.
adamc@118 179
adamc@118 180 Ltac clear_all :=
adamc@118 181 repeat match goal with
adamc@118 182 | [ H : _ |- _ ] => clear H
adamc@118 183 end.