Mercurial > cpdt > repo

comparison src/CpdtTactics.v @ 375:d1276004eec9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Finish pass over LogicProg; change [crush] to take advantage of new [Hint Rewrite] syntax that uses database [core] by default
author Adam Chlipala <adam@chlipala.net>
date Mon, 26 Mar 2012 16:55:59 -0400
parents d5787b70cf48
children 76e1dfcb86eb
comparison
equal deleted inserted replaced
374:f3146d40c2a1 375:d1276004eec9
79 Ltac rewriteHyp := 79 Ltac rewriteHyp :=
80 match goal with 80 match goal with
81 | [ H : _ |- _ ] => rewrite H; auto; [idtac] 81 | [ H : _ |- _ ] => rewrite H; auto; [idtac]
82 end. 82 end.
83 83
84 Ltac rewriterP := repeat (rewriteHyp; autorewrite with cpdt in *). 84 Ltac rewriterP := repeat (rewriteHyp; autorewrite with core in *).
85 85
86 Ltac rewriter := autorewrite with cpdt in *; rewriterP. 86 Ltac rewriter := autorewrite with core in *; rewriterP.
87 87
88 Hint Rewrite app_ass : cpdt. 88 Hint Rewrite app_ass.
89 89
90 Definition done (T : Type) (x : T) := True. 90 Definition done (T : Type) (x : T) := True.
91 91
92 Ltac inster e trace := 92 Ltac inster e trace :=
93 match type of e with 93 match type of e with
128 128
129 Require Import JMeq. 129 Require Import JMeq.
130 130
131 Ltac crush' lemmas invOne := 131 Ltac crush' lemmas invOne :=
132 let sintuition := simpl in *; intuition; try subst; repeat (simplHyp invOne; intuition; try subst); try congruence in 132 let sintuition := simpl in *; intuition; try subst; repeat (simplHyp invOne; intuition; try subst); try congruence in
133 let rewriter := autorewrite with cpdt in *; 133 let rewriter := autorewrite with core in *;
134 repeat (match goal with 134 repeat (match goal with
135 | [ H : ?P |- _ ] => 135 | [ H : ?P |- _ ] =>
136 match P with 136 match P with
137 | context[JMeq] => fail 1 137 | context[JMeq] => fail 1
138 | _ => (rewrite H; []) 138 | _ => (rewrite H; [])
139 || (rewrite H; [ | solve [ crush' lemmas invOne ] ]) 139 || (rewrite H; [ | solve [ crush' lemmas invOne ] ])
140 || (rewrite H; [ | solve [ crush' lemmas invOne ] | solve [ crush' lemmas invOne ] ]) 140 || (rewrite H; [ | solve [ crush' lemmas invOne ] | solve [ crush' lemmas invOne ] ])
141 end 141 end
142 end; autorewrite with cpdt in *) 142 end; autorewrite with core in *)
143 in (sintuition; rewriter; 143 in (sintuition; rewriter;
144 match lemmas with 144 match lemmas with
145 | false => idtac 145 | false => idtac
146 | _ => repeat ((app ltac:(fun L => inster L L) lemmas || appHyps ltac:(fun L => inster L L)); 146 | _ => repeat ((app ltac:(fun L => inster L L) lemmas || appHyps ltac:(fun L => inster L L));
147 repeat (simplHyp invOne; intuition)); un_done 147 repeat (simplHyp invOne; intuition)); un_done