|
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@2
|
10 Require Import 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@59
|
27 | (?LS, _) => inList x LS
|
|
adamc@59
|
28 end.
|
|
adamc@59
|
29
|
|
adamc@59
|
30 Ltac app f ls :=
|
|
adamc@59
|
31 match ls with
|
|
adamc@59
|
32 | (?LS, ?X) => f X || app f LS || fail 1
|
|
adamc@59
|
33 | _ => f ls
|
|
adamc@59
|
34 end.
|
|
adamc@59
|
35
|
|
adamc@59
|
36 Ltac all f ls :=
|
|
adamc@59
|
37 match ls with
|
|
adamc@59
|
38 | (?LS, ?X) => f X; all f LS
|
|
adamc@59
|
39 | (_, _) => fail 1
|
|
adamc@59
|
40 | _ => f ls
|
|
adamc@59
|
41 end.
|
|
adamc@59
|
42
|
|
adamc@59
|
43 Ltac simplHyp invOne :=
|
|
adamc@59
|
44 match goal with
|
|
adamc@59
|
45 | [ H : ex _ |- _ ] => destruct H
|
|
adamc@59
|
46
|
|
adamc@51
|
47 | [ H : ?F _ = ?F _ |- _ ] => injection H;
|
|
adamc@51
|
48 match goal with
|
|
adamc@66
|
49 | [ |- _ = _ -> _ ] => clear H; intros; try subst
|
|
adamc@51
|
50 end
|
|
adamc@51
|
51 | [ H : ?F _ _ = ?F _ _ |- _ ] => injection H;
|
|
adamc@51
|
52 match goal with
|
|
adamc@66
|
53 | [ |- _ = _ -> _ = _ -> _ ] => clear H; intros; try subst
|
|
adamc@51
|
54 end
|
|
adamc@59
|
55
|
|
adamc@66
|
56 | [ H : ?F _ |- _ ] => inList F invOne; inversion H; [idtac]; clear H; try subst
|
|
adamc@66
|
57 | [ H : ?F _ _ |- _ ] => inList F invOne; inversion H; [idtac]; clear H; try subst
|
|
adamc@50
|
58 end.
|
|
adamc@50
|
59
|
|
adamc@2
|
60 Ltac rewriteHyp :=
|
|
adamc@2
|
61 match goal with
|
|
adamc@2
|
62 | [ H : _ |- _ ] => rewrite H
|
|
adamc@2
|
63 end.
|
|
adamc@2
|
64
|
|
adamc@2
|
65 Ltac rewriterP := repeat (rewriteHyp; autorewrite with cpdt in *).
|
|
adamc@2
|
66
|
|
adamc@2
|
67 Ltac rewriter := autorewrite with cpdt in *; rewriterP.
|
|
adamc@2
|
68
|
|
adamc@2
|
69 Hint Rewrite app_ass : cpdt.
|
|
adamc@2
|
70
|
|
adamc@59
|
71 Definition done (T : Type) (x : T) := True.
|
|
adamc@2
|
72
|
|
adamc@59
|
73 Ltac inster e trace :=
|
|
adamc@59
|
74 match type of e with
|
|
adamc@59
|
75 | forall x : _, _ =>
|
|
adamc@59
|
76 match goal with
|
|
adamc@59
|
77 | [ H : _ |- _ ] =>
|
|
adamc@59
|
78 inster (e H) (trace, H)
|
|
adamc@59
|
79 | _ => fail 2
|
|
adamc@59
|
80 end
|
|
adamc@59
|
81 | _ =>
|
|
adamc@59
|
82 match trace with
|
|
adamc@59
|
83 | (_, _) =>
|
|
adamc@59
|
84 match goal with
|
|
adamc@59
|
85 | [ H : done (trace, _) |- _ ] => fail 1
|
|
adamc@59
|
86 | _ =>
|
|
adamc@59
|
87 let T := type of e in
|
|
adamc@59
|
88 match type of T with
|
|
adamc@59
|
89 | Prop =>
|
|
adamc@59
|
90 generalize e; intro;
|
|
adamc@59
|
91 assert (done (trace, tt)); [constructor | idtac]
|
|
adamc@59
|
92 | _ =>
|
|
adamc@59
|
93 all ltac:(fun X =>
|
|
adamc@59
|
94 match goal with
|
|
adamc@59
|
95 | [ H : done (_, X) |- _ ] => fail 1
|
|
adamc@59
|
96 | _ => idtac
|
|
adamc@59
|
97 end) trace;
|
|
adamc@59
|
98 let i := fresh "i" in (pose (i := e);
|
|
adamc@59
|
99 assert (done (trace, i)); [constructor | idtac])
|
|
adamc@59
|
100 end
|
|
adamc@59
|
101 end
|
|
adamc@59
|
102 end
|
|
adamc@59
|
103 end.
|
|
adamc@59
|
104
|
|
adamc@65
|
105 Ltac un_done :=
|
|
adamc@65
|
106 repeat match goal with
|
|
adamc@65
|
107 | [ H : done _ |- _ ] => clear H
|
|
adamc@65
|
108 end.
|
|
adamc@65
|
109
|
|
adamc@59
|
110 Ltac crush' lemmas invOne :=
|
|
adamc@66
|
111 let sintuition := simpl in *; intuition; try subst; repeat (simplHyp invOne; intuition; try subst); try congruence
|
|
adamc@59
|
112 in (sintuition; rewriter;
|
|
adamc@59
|
113 repeat ((app ltac:(fun L => inster L L) lemmas || appHyps ltac:(fun L => inster L L));
|
|
adamc@59
|
114 repeat (simplHyp invOne; intuition));
|
|
adamc@80
|
115 un_done; sintuition; try omega; try (elimtype False; omega)).
|
|
adamc@59
|
116
|
|
adamc@59
|
117 Ltac crush := crush' tt fail.
|
