Mercurial > cpdt > repo

comparison src/Tactics.v @ 59:1a664ff9d2d1

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Beefed-up crush, with auto-inversion and lemma instantiation
author Adam Chlipala <adamc@hcoop.net>
date Tue, 30 Sep 2008 13:11:39 -0400
parents 9ceee967b1fc
children 739c2818d6e2
comparison
equal deleted inserted replaced
58:1946586b9da7 59:1a664ff9d2d1
9 9
10 Require Import List. 10 Require Import List.
11 11
12 Require Omega. 12 Require Omega.
13 13
14 Set Implicit Arguments.
15
14 16
15 Ltac inject H := injection H; clear H; intros; subst. 17 Ltac inject H := injection H; clear H; intros; subst.
16 18
17 Ltac simplHyp := 19 Ltac appHyps f :=
18 match goal with 20 match goal with
21 | [ H : _ |- _ ] => f H
22 end.
23
24 Ltac inList x ls :=
25 match ls with
26 | x => idtac
27 | (?LS, _) => inList x LS
28 end.
29
30 Ltac app f ls :=
31 match ls with
32 | (?LS, ?X) => f X || app f LS || fail 1
33 | _ => f ls
34 end.
35
36 Ltac all f ls :=
37 match ls with
38 | (?LS, ?X) => f X; all f LS
39 | (_, _) => fail 1
40 | _ => f ls
41 end.
42
43 Ltac simplHyp invOne :=
44 match goal with
45 | [ H : ex _ |- _ ] => destruct H
46
19 | [ H : ?F _ = ?F _ |- _ ] => injection H; 47 | [ H : ?F _ = ?F _ |- _ ] => injection H;
20 match goal with 48 match goal with
21 | [ |- _ = _ -> _ ] => clear H; intros; subst 49 | [ |- _ = _ -> _ ] => clear H; intros; subst
22 end 50 end
23 | [ H : ?F _ _ = ?F _ _ |- _ ] => injection H; 51 | [ H : ?F _ _ = ?F _ _ |- _ ] => injection H;
24 match goal with 52 match goal with
25 | [ |- _ = _ -> _ = _ -> _ ] => clear H; intros; subst 53 | [ |- _ = _ -> _ = _ -> _ ] => clear H; intros; subst
26 end 54 end
55
56 | [ H : ?F _ |- _ ] => inList F invOne; inversion H; [idtac]; clear H; subst
57 | [ H : ?F _ _ |- _ ] => inList F invOne; inversion H; [idtac]; clear H; subst
27 end. 58 end.
28 59
29 Ltac rewriteHyp := 60 Ltac rewriteHyp :=
30 match goal with 61 match goal with
31 | [ H : _ |- _ ] => rewrite H 62 | [ H : _ |- _ ] => rewrite H
35 66
36 Ltac rewriter := autorewrite with cpdt in *; rewriterP. 67 Ltac rewriter := autorewrite with cpdt in *; rewriterP.
37 68
38 Hint Rewrite app_ass : cpdt. 69 Hint Rewrite app_ass : cpdt.
39 70
40 Ltac sintuition := simpl in *; intuition; try simplHyp; try congruence. 71 Definition done (T : Type) (x : T) := True.
41 72
42 Ltac crush := sintuition; rewriter; sintuition; try omega. 73 Ltac inster e trace :=
74 match type of e with
75 | forall x : _, _ =>
76 match goal with
77 | [ H : _ |- _ ] =>
78 inster (e H) (trace, H)
79 | _ => fail 2
80 end
81 | _ =>
82 match trace with
83 | (_, _) =>
84 match goal with
85 | [ H : done (trace, _) |- _ ] => fail 1
86 | _ =>
87 let T := type of e in
88 match type of T with
89 | Prop =>
90 generalize e; intro;
91 assert (done (trace, tt)); [constructor | idtac]
92 | _ =>
93 all ltac:(fun X =>
94 match goal with
95 | [ H : done (_, X) |- _ ] => fail 1
96 | _ => idtac
97 end) trace;
98 let i := fresh "i" in (pose (i := e);
99 assert (done (trace, i)); [constructor | idtac])
100 end
101 end
102 end
103 end.
104
105 Ltac crush' lemmas invOne :=
106 let sintuition := simpl in *; intuition; repeat (simplHyp invOne; intuition); try congruence
107 in (sintuition; rewriter;
108 repeat ((app ltac:(fun L => inster L L) lemmas || appHyps ltac:(fun L => inster L L));
109 repeat (simplHyp invOne; intuition));
110 sintuition; try omega).
111
112 Ltac crush := crush' tt fail.