Mercurial > cpdt > repo

annotate src/CpdtTactics.v @ 345:518c8994a715

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
One more axiom avoidance example
author Adam Chlipala <adam@chlipala.net>
date Wed, 19 Oct 2011 10:00:07 -0400
parents d5787b70cf48
children d1276004eec9
rev   line source
adam@297 1 (* Copyright (c) 2008-2011, 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@204 51 | [ H : ?F ?X = ?F ?Y |- ?G ] =>
adamc@204 52 (assert (X = Y); [ assumption | fail 1 ])
adamc@204 53 || (injection H;
adamc@204 54 match goal with
adamc@204 55 | [ |- X = Y -> G ] =>
adamc@204 56 try clear H; intros; try subst
adamc@204 57 end)
adamc@204 58 | [ H : ?F ?X ?U = ?F ?Y ?V |- ?G ] =>
adamc@204 59 (assert (X = Y); [ assumption
adamc@204 60 | assert (U = V); [ assumption | fail 1 ] ])
adamc@204 61 || (injection H;
adamc@204 62 match goal with
adamc@204 63 | [ |- U = V -> X = Y -> G ] =>
adamc@204 64 try clear H; intros; try subst
adamc@204 65 end)
adamc@59 66
adamc@99 67 | [ H : ?F _ |- _ ] => invert H F
adamc@99 68 | [ H : ?F _ _ |- _ ] => invert H F
adamc@99 69 | [ H : ?F _ _ _ |- _ ] => invert H F
adamc@99 70 | [ H : ?F _ _ _ _ |- _ ] => invert H F
adamc@99 71 | [ H : ?F _ _ _ _ _ |- _ ] => invert H F
adamc@176 72
adamc@176 73 | [ H : existT _ ?T _ = existT _ ?T _ |- _ ] => generalize (inj_pair2 _ _ _ _ _ H); clear H
adamc@176 74 | [ H : existT _ _ _ = existT _ _ _ |- _ ] => inversion H; clear H
adamc@179 75
adamc@179 76 | [ H : Some _ = Some _ |- _ ] => injection H; clear H
adamc@50 77 end.
adamc@50 78
adamc@2 79 Ltac rewriteHyp :=
adamc@2 80 match goal with
adamc@183 81 | [ H : _ |- _ ] => rewrite H; auto; [idtac]
adamc@2 82 end.
adamc@2 83
adamc@2 84 Ltac rewriterP := repeat (rewriteHyp; autorewrite with cpdt in *).
adamc@2 85
adamc@2 86 Ltac rewriter := autorewrite with cpdt in *; rewriterP.
adamc@2 87
adamc@2 88 Hint Rewrite app_ass : cpdt.
adamc@2 89
adamc@59 90 Definition done (T : Type) (x : T) := True.
adamc@2 91
adamc@59 92 Ltac inster e trace :=
adamc@59 93 match type of e with
adamc@59 94 | forall x : _, _ =>
adamc@59 95 match goal with
adamc@59 96 | [ H : _ |- _ ] =>
adamc@59 97 inster (e H) (trace, H)
adamc@59 98 | _ => fail 2
adamc@59 99 end
adamc@59 100 | _ =>
adamc@59 101 match trace with
adamc@59 102 | (_, _) =>
adamc@59 103 match goal with
adamc@59 104 | [ H : done (trace, _) |- _ ] => fail 1
adamc@59 105 | _ =>
adamc@59 106 let T := type of e in
adamc@59 107 match type of T with
adamc@59 108 | Prop =>
adamc@59 109 generalize e; intro;
adamc@59 110 assert (done (trace, tt)); [constructor | idtac]
adamc@59 111 | _ =>
adamc@59 112 all ltac:(fun X =>
adamc@59 113 match goal with
adamc@59 114 | [ H : done (_, X) |- _ ] => fail 1
adamc@59 115 | _ => idtac
adamc@59 116 end) trace;
adamc@59 117 let i := fresh "i" in (pose (i := e);
adamc@59 118 assert (done (trace, i)); [constructor | idtac])
adamc@59 119 end
adamc@59 120 end
adamc@59 121 end
adamc@59 122 end.
adamc@59 123
adamc@65 124 Ltac un_done :=
adamc@65 125 repeat match goal with
adamc@65 126 | [ H : done _ |- _ ] => clear H
adamc@65 127 end.
adamc@65 128
adam@297 129 Require Import JMeq.
adam@297 130
adamc@88 131 Ltac crush' lemmas invOne :=
adamc@184 132 let sintuition := simpl in *; intuition; try subst; repeat (simplHyp invOne; intuition; try subst); try congruence in
adamc@184 133 let rewriter := autorewrite with cpdt in *;
adamc@184 134 repeat (match goal with
adam@297 135 | [ H : ?P |- _ ] =>
adam@297 136 match P with
adam@297 137 | context[JMeq] => fail 1
adam@297 138 | _ => (rewrite H; [])
adam@297 139 || (rewrite H; [ | solve [ crush' lemmas invOne ] ])
adam@297 140 || (rewrite H; [ | solve [ crush' lemmas invOne ] | solve [ crush' lemmas invOne ] ])
adam@297 141 end
adamc@184 142 end; autorewrite with cpdt in *)
adamc@184 143 in (sintuition; rewriter;
adamc@183 144 match lemmas with
adamc@183 145 | false => idtac
adamc@183 146 | _ => repeat ((app ltac:(fun L => inster L L) lemmas || appHyps ltac:(fun L => inster L L));
adamc@183 147 repeat (simplHyp invOne; intuition)); un_done
adamc@184 148 end; sintuition; rewriter; sintuition; try omega; try (elimtype False; omega)).
adamc@59 149
adamc@88 150 Ltac crush := crush' false fail.
adamc@85 151
adamc@213 152 Require Import Program.Equality.
adamc@85 153
adamc@85 154 Ltac dep_destruct E :=
adamc@213 155 let x := fresh "x" in
adamc@213 156 remember E as x; simpl in x; dependent destruction x;
adamc@213 157 try match goal with
adamc@213 158 | [ H : _ = E |- _ ] => rewrite <- H in *; clear H
adamc@213 159 end.
adamc@118 160
adamc@118 161 Ltac clear_all :=
adamc@118 162 repeat match goal with
adamc@118 163 | [ H : _ |- _ ] => clear H
adamc@118 164 end.
adamc@256 165
adamc@262 166 Ltac guess v H :=
adamc@256 167 repeat match type of H with
adamc@256 168 | forall x : ?T, _ =>
adamc@256 169 match type of T with
adamc@256 170 | Prop =>
adamc@256 171 (let H' := fresh "H'" in
adamc@256 172 assert (H' : T); [
adamc@262 173 solve [ eauto 6 ]
adamc@256 174 | generalize (H H'); clear H H'; intro H ])
adamc@256 175 || fail 1
adamc@256 176 | _ =>
adamc@262 177 (generalize (H v); clear H; intro H)
adamc@262 178 || let x := fresh "x" in
adamc@256 179 evar (x : T);
adamc@256 180 let x' := eval cbv delta [x] in x in
adamc@256 181 clear x; generalize (H x'); clear H; intro H
adamc@256 182 end
adamc@256 183 end.
adamc@256 184
adamc@262 185 Ltac guessKeep v H :=
adamc@256 186 let H' := fresh "H'" in
adamc@262 187 generalize H; intro H'; guess v H'.