Mercurial > cpdt > repo

comparison src/Tactics.v @ 262:de53c8bcfa8d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
OpSem code
author Adam Chlipala <adamc@hcoop.net>
date Mon, 28 Dec 2009 12:35:44 -0500
parents 4293dd6912cd
children b441010125d4
comparison
equal deleted inserted replaced
261:0a644d7004d5 262:de53c8bcfa8d
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 159
160 Ltac guess tac H := 160 Ltac guess v H :=
161 repeat match type of H with 161 repeat match type of H with
162 | forall x : ?T, _ => 162 | forall x : ?T, _ =>
163 match type of T with 163 match type of T with
164 | Prop => 164 | Prop =>
165 (let H' := fresh "H'" in 165 (let H' := fresh "H'" in
166 assert (H' : T); [ 166 assert (H' : T); [
167 solve [ tac ] 167 solve [ eauto 6 ]
168 | generalize (H H'); clear H H'; intro H ]) 168 | generalize (H H'); clear H H'; intro H ])
169 || fail 1 169 || fail 1
170 | _ => 170 | _ =>
171 let x := fresh "x" in 171 (generalize (H v); clear H; intro H)
172 || let x := fresh "x" in
172 evar (x : T); 173 evar (x : T);
173 let x' := eval cbv delta [x] in x in 174 let x' := eval cbv delta [x] in x in
174 clear x; generalize (H x'); clear H; intro H 175 clear x; generalize (H x'); clear H; intro H
175 end 176 end
176 end. 177 end.
177 178
178 Ltac guessKeep tac H := 179 Ltac guessKeep v H :=
179 let H' := fresh "H'" in 180 let H' := fresh "H'" in
180 generalize H; intro H'; guess tac H'. 181 generalize H; intro H'; guess v H'.