Mercurial > cpdt > repo

comparison src/Tactics.v @ 256:4293dd6912cd

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Prosified Extensional
author Adam Chlipala <adamc@hcoop.net>
date Wed, 16 Dec 2009 15:31:54 -0500
parents c4b1c0de7af9
children de53c8bcfa8d
comparison
equal deleted inserted replaced
255:05250878e4ca 256:4293dd6912cd
154 154
155 Ltac clear_all := 155 Ltac clear_all :=
156 repeat match goal with 156 repeat match goal with
157 | [ H : _ |- _ ] => clear H 157 | [ H : _ |- _ ] => clear H
158 end. 158 end.
159
160 Ltac guess tac H :=
161 repeat match type of H with
162 | forall x : ?T, _ =>
163 match type of T with
164 | Prop =>
165 (let H' := fresh "H'" in
166 assert (H' : T); [
167 solve [ tac ]
168 | generalize (H H'); clear H H'; intro H ])
169 || fail 1
170 | _ =>
171 let x := fresh "x" in
172 evar (x : T);
173 let x' := eval cbv delta [x] in x in
174 clear x; generalize (H x'); clear H; intro H
175 end
176 end.
177
178 Ltac guessKeep tac H :=
179 let H' := fresh "H'" in
180 generalize H; intro H'; guess tac H'.