← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to tactics/extratactics.ml4

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
tactics/extratactics.ml4
 
1
(************************************************************************)
 
2
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
 
4
(*   \VV/  **************************************************************)
 
5
(*    //   *      This file is distributed under the terms of the       *)
 
6
(*         *       GNU Lesser General Public License Version 2.1        *)
 
7
(************************************************************************)
 
8
 
 
9
(*i camlp4deps: "parsing/grammar.cma" i*)
 
10
 
 
11
(* $Id: extratactics.ml4 11800 2009-01-18 18:34:15Z msozeau $ *)
 
12
 
 
13
open Pp
 
14
open Pcoq
 
15
open Genarg
 
16
open Extraargs
 
17
open Mod_subst
 
18
open Names
 
19
open Tacexpr
 
20
open Rawterm
 
21
open Tactics
 
22
 
 
23
(* Equality *)
 
24
open Equality
 
25
 
 
26
 
 
27
TACTIC EXTEND replace 
 
28
   ["replace" constr(c1) "with" constr(c2) in_arg_hyp(in_hyp) by_arg_tac(tac) ]
 
29
-> [ replace_in_clause_maybe_by c1 c2 (glob_in_arg_hyp_to_clause in_hyp) (Option.map Tacinterp.eval_tactic tac) ]
 
30
END
 
31
 
 
32
TACTIC EXTEND replace_term_left
 
33
  [ "replace"  "->" constr(c) in_arg_hyp(in_hyp) ]
 
34
  -> [ replace_multi_term (Some true) c (glob_in_arg_hyp_to_clause in_hyp)]
 
35
END
 
36
 
 
37
TACTIC EXTEND replace_term_right
 
38
  [ "replace"  "<-" constr(c) in_arg_hyp(in_hyp) ]
 
39
  -> [replace_multi_term (Some false) c (glob_in_arg_hyp_to_clause in_hyp)]
 
40
END
 
41
 
 
42
TACTIC EXTEND replace_term
 
43
  [ "replace" constr(c) in_arg_hyp(in_hyp) ]
 
44
  -> [ replace_multi_term None c (glob_in_arg_hyp_to_clause in_hyp) ]
 
45
END
 
46
 
 
47
let induction_arg_of_quantified_hyp = function
 
48
  | AnonHyp n -> ElimOnAnonHyp n
 
49
  | NamedHyp id -> ElimOnIdent (Util.dummy_loc,id)
 
50
 
 
51
(* Versions *_main must come first!! so that "1" is interpreted as a
 
52
   ElimOnAnonHyp and not as a "constr", and "id" is interpreted as a
 
53
   ElimOnIdent and not as "constr" *)
 
54
 
 
55
TACTIC EXTEND simplify_eq_main
 
56
| [ "simplify_eq" constr_with_bindings(c) ] ->
 
57
    [ dEq false (Some (ElimOnConstr c)) ]
 
58
END
 
59
TACTIC EXTEND simplify_eq
 
60
  [ "simplify_eq" ] -> [ dEq false None ]
 
61
| [ "simplify_eq" quantified_hypothesis(h) ] ->
 
62
    [ dEq false (Some (induction_arg_of_quantified_hyp h)) ]
 
63
END
 
64
TACTIC EXTEND esimplify_eq_main
 
65
| [ "esimplify_eq" constr_with_bindings(c) ] ->
 
66
    [ dEq true (Some (ElimOnConstr c)) ]
 
67
END
 
68
TACTIC EXTEND esimplify_eq
 
69
| [ "esimplify_eq" ] -> [ dEq true None ]
 
70
| [ "esimplify_eq" quantified_hypothesis(h) ] ->
 
71
    [ dEq true (Some (induction_arg_of_quantified_hyp h)) ]
 
72
END
 
73
 
 
74
TACTIC EXTEND discriminate_main
 
75
| [ "discriminate" constr_with_bindings(c) ] ->
 
76
    [ discr_tac false (Some (ElimOnConstr c)) ]
 
77
END
 
78
TACTIC EXTEND discriminate
 
79
| [ "discriminate" ] -> [ discr_tac false None ]
 
80
| [ "discriminate" quantified_hypothesis(h) ] ->
 
81
    [ discr_tac false (Some (induction_arg_of_quantified_hyp h)) ]
 
82
END
 
83
TACTIC EXTEND ediscriminate_main
 
84
| [ "ediscriminate" constr_with_bindings(c) ] ->
 
85
    [ discr_tac true (Some (ElimOnConstr c)) ]
 
86
END
 
87
TACTIC EXTEND ediscriminate
 
88
| [ "ediscriminate" ] -> [ discr_tac true None ]
 
89
| [ "ediscriminate" quantified_hypothesis(h) ] ->
 
90
    [ discr_tac true (Some (induction_arg_of_quantified_hyp h)) ]
 
91
END
 
92
 
 
93
let h_discrHyp id = h_discriminate_main (Term.mkVar id,NoBindings)
 
94
 
 
95
TACTIC EXTEND injection_main
 
96
| [ "injection" constr_with_bindings(c) ] ->
 
97
    [ injClause [] false (Some (ElimOnConstr c)) ]
 
98
END 
 
99
TACTIC EXTEND injection
 
100
| [ "injection" ] -> [ injClause [] false None ]
 
101
| [ "injection" quantified_hypothesis(h) ] -> 
 
102
    [ injClause [] false (Some (induction_arg_of_quantified_hyp h)) ]
 
103
END
 
104
TACTIC EXTEND einjection_main
 
105
| [ "einjection" constr_with_bindings(c) ] ->
 
106
    [ injClause [] true (Some (ElimOnConstr c)) ]
 
107
END
 
108
TACTIC EXTEND einjection
 
109
| [ "einjection" ] -> [ injClause [] true None ]
 
110
| [ "einjection" quantified_hypothesis(h) ] -> [ injClause [] true (Some (induction_arg_of_quantified_hyp h)) ]
 
111
END 
 
112
TACTIC EXTEND injection_as_main
 
113
| [ "injection" constr_with_bindings(c) "as" simple_intropattern_list(ipat)] ->
 
114
    [ injClause ipat false (Some (ElimOnConstr c)) ]
 
115
END 
 
116
TACTIC EXTEND injection_as
 
117
| [ "injection" "as" simple_intropattern_list(ipat)] ->
 
118
    [ injClause ipat false None ]
 
119
| [ "injection" quantified_hypothesis(h) "as" simple_intropattern_list(ipat) ] ->
 
120
    [ injClause ipat false (Some (induction_arg_of_quantified_hyp h)) ]
 
121
END 
 
122
TACTIC EXTEND einjection_as_main
 
123
| [ "einjection" constr_with_bindings(c) "as" simple_intropattern_list(ipat)] ->
 
124
    [ injClause ipat true (Some (ElimOnConstr c)) ]
 
125
END 
 
126
TACTIC EXTEND einjection_as
 
127
| [ "einjection" "as" simple_intropattern_list(ipat)] ->
 
128
    [ injClause ipat true None ]
 
129
| [ "einjection" quantified_hypothesis(h) "as" simple_intropattern_list(ipat) ] ->
 
130
    [ injClause ipat true (Some (induction_arg_of_quantified_hyp h)) ]
 
131
END
 
132
 
 
133
let h_injHyp id = h_injection_main (Term.mkVar id,NoBindings)
 
134
 
 
135
TACTIC EXTEND conditional_rewrite
 
136
| [ "conditional" tactic(tac) "rewrite" orient(b) constr_with_bindings(c) ]
 
137
    -> [ conditional_rewrite b (snd tac) (inj_open (fst c), snd c) ]
 
138
| [ "conditional" tactic(tac) "rewrite" orient(b) constr_with_bindings(c)
 
139
    "in" hyp(h) ]
 
140
    -> [ conditional_rewrite_in b h (snd tac) (inj_open (fst c), snd c) ]
 
141
END
 
142
 
 
143
TACTIC EXTEND dependent_rewrite
 
144
| [ "dependent" "rewrite" orient(b) constr(c) ] -> [ rewriteInConcl b c ]
 
145
| [ "dependent" "rewrite" orient(b) constr(c) "in" hyp(id) ]
 
146
    -> [ rewriteInHyp b c id ]
 
147
END
 
148
 
 
149
TACTIC EXTEND cut_rewrite
 
150
| [ "cutrewrite" orient(b) constr(eqn) ] -> [ cutRewriteInConcl b eqn ]
 
151
| [ "cutrewrite" orient(b) constr(eqn) "in" hyp(id) ]
 
152
    -> [ cutRewriteInHyp b eqn id ]
 
153
END
 
154
 
 
155
(* Contradiction *)
 
156
open Contradiction
 
157
 
 
158
TACTIC EXTEND absurd
 
159
 [ "absurd" constr(c) ] -> [ absurd c ]
 
160
END
 
161
 
 
162
TACTIC EXTEND contradiction
 
163
 [ "contradiction" constr_with_bindings_opt(c) ] -> [ contradiction c ]
 
164
END
 
165
 
 
166
(* AutoRewrite *)
 
167
 
 
168
open Autorewrite
 
169
(* J.F : old version 
 
170
TACTIC EXTEND autorewrite
 
171
  [ "autorewrite" "with" ne_preident_list(l) ] ->
 
172
    [ autorewrite Refiner.tclIDTAC l ]
 
173
| [ "autorewrite" "with" ne_preident_list(l) "using" tactic(t) ] ->
 
174
    [ autorewrite (snd t) l ]
 
175
| [ "autorewrite" "with" ne_preident_list(l) "in" hyp(id) ] ->
 
176
    [ autorewrite_in id Refiner.tclIDTAC l ]
 
177
| [ "autorewrite" "with" ne_preident_list(l) "in" hyp(id) "using" tactic(t) ] ->
 
178
    [ autorewrite_in id (snd t) l ]
 
179
END
 
180
*)
 
181
 
 
182
TACTIC EXTEND autorewrite
 
183
| [ "autorewrite" "with" ne_preident_list(l) in_arg_hyp(cl) ] ->
 
184
    [ auto_multi_rewrite  l (glob_in_arg_hyp_to_clause  cl) ]
 
185
| [ "autorewrite" "with" ne_preident_list(l) in_arg_hyp(cl) "using" tactic(t) ] ->
 
186
    [ 
 
187
      let cl =  glob_in_arg_hyp_to_clause cl in 
 
188
      auto_multi_rewrite_with (snd t) l cl
 
189
 
 
190
    ]
 
191
END
 
192
 
 
193
 
 
194
 
 
195
 
 
196
let add_rewrite_hint name ort t lcsr =
 
197
  let env = Global.env() and sigma = Evd.empty in
 
198
  let f c = Constrintern.interp_constr sigma env c, ort, t in
 
199
  add_rew_rules name (List.map f lcsr)
 
200
 
 
201
VERNAC COMMAND EXTEND HintRewrite
 
202
  [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ":" preident(b) ] ->
 
203
  [ add_rewrite_hint b o (Tacexpr.TacId []) l ]
 
204
| [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t)
 
205
    ":" preident(b) ] ->
 
206
  [ add_rewrite_hint b o t l ]
 
207
END
 
208
 
 
209
 
 
210
(* Refine *)
 
211
 
 
212
open Refine
 
213
 
 
214
TACTIC EXTEND refine
 
215
  [ "refine" casted_open_constr(c) ] -> [ refine c ]
 
216
END
 
217
 
 
218
let refine_tac = h_refine
 
219
 
 
220
(* Inversion lemmas (Leminv) *)
 
221
 
 
222
open Inv
 
223
open Leminv
 
224
 
 
225
VERNAC COMMAND EXTEND DeriveInversionClear
 
226
  [ "Derive" "Inversion_clear" ident(na) hyp(id) ]
 
227
  -> [ inversion_lemma_from_goal 1 na id Term.prop_sort false inv_clear_tac ]
 
228
 
 
229
| [ "Derive" "Inversion_clear" natural(n) ident(na) hyp(id) ]
 
230
  -> [ inversion_lemma_from_goal n na id Term.prop_sort false inv_clear_tac ]
 
231
 
 
232
| [ "Derive" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort(s) ]
 
233
  -> [ add_inversion_lemma_exn na c s false inv_clear_tac ]
 
234
 
 
235
| [ "Derive" "Inversion_clear" ident(na) "with" constr(c) ]
 
236
  -> [ add_inversion_lemma_exn na c (Rawterm.RProp Term.Null) false inv_clear_tac ]
 
237
END
 
238
 
 
239
open Term
 
240
open Rawterm
 
241
 
 
242
VERNAC COMMAND EXTEND DeriveInversion
 
243
| [ "Derive" "Inversion" ident(na) "with" constr(c) "Sort" sort(s) ]
 
244
  -> [ add_inversion_lemma_exn na c s false inv_tac ]
 
245
 
 
246
| [ "Derive" "Inversion" ident(na) "with" constr(c) ]
 
247
  -> [ add_inversion_lemma_exn na c (RProp Null) false inv_tac ]
 
248
 
 
249
| [ "Derive" "Inversion" ident(na) hyp(id) ]
 
250
  -> [ inversion_lemma_from_goal 1 na id Term.prop_sort false inv_tac ]
 
251
 
 
252
| [ "Derive" "Inversion" natural(n) ident(na) hyp(id) ]
 
253
  -> [ inversion_lemma_from_goal n na id Term.prop_sort false inv_tac ]
 
254
END
 
255
 
 
256
VERNAC COMMAND EXTEND DeriveDependentInversion
 
257
| [ "Derive" "Dependent" "Inversion" ident(na) "with" constr(c) "Sort" sort(s) ]
 
258
  -> [ add_inversion_lemma_exn na c s true dinv_tac ]
 
259
    END
 
260
 
 
261
VERNAC COMMAND EXTEND DeriveDependentInversionClear
 
262
| [ "Derive" "Dependent" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort(s) ]
 
263
  -> [ add_inversion_lemma_exn na c s true dinv_clear_tac ]
 
264
END
 
265
 
 
266
(* Subst *)
 
267
 
 
268
TACTIC EXTEND subst
 
269
| [ "subst" ne_var_list(l) ] -> [ subst l ]
 
270
| [ "subst" ] -> [ subst_all ]
 
271
END
 
272
 
 
273
open Evar_tactics
 
274
 
 
275
(* evar creation *)
 
276
 
 
277
TACTIC EXTEND evar
 
278
  [ "evar" "(" ident(id) ":" lconstr(typ) ")" ] -> [ let_evar (Name id) typ ]
 
279
| [ "evar" constr(typ) ] -> [ let_evar Anonymous typ ]
 
280
END
 
281
 
 
282
open Tacexpr
 
283
open Tacticals
 
284
 
 
285
TACTIC EXTEND instantiate
 
286
  [ "instantiate" "(" integer(i) ":=" raw(c) ")" hloc(hl) ] ->
 
287
    [instantiate i c hl  ]
 
288
| [ "instantiate" ] -> [ tclNORMEVAR ]
 
289
END
 
290
 
 
291
 
 
292
(** Nijmegen "step" tactic for setoid rewriting *)
 
293
 
 
294
open Tactics
 
295
open Tactics
 
296
open Libnames
 
297
open Rawterm
 
298
open Summary
 
299
open Libobject
 
300
open Lib
 
301
 
 
302
(* Registered lemmas are expected to be of the form
 
303
     x R y -> y == z -> x R z    (in the right table)
 
304
     x R y -> x == z -> z R y    (in the left table)
 
305
*)
 
306
 
 
307
let transitivity_right_table = ref []
 
308
let transitivity_left_table = ref []
 
309
 
 
310
(* [step] tries to apply a rewriting lemma; then apply [tac] intended to
 
311
   complete to proof of the last hypothesis (assumed to state an equality) *)
 
312
 
 
313
let step left x tac =
 
314
  let l =
 
315
    List.map (fun lem ->
 
316
      tclTHENLAST
 
317
      (apply_with_bindings (lem, ImplicitBindings [x]))
 
318
        tac)
 
319
      !(if left then transitivity_left_table else transitivity_right_table)
 
320
  in
 
321
  tclFIRST l
 
322
 
 
323
(* Main function to push lemmas in persistent environment *)
 
324
 
 
325
let cache_transitivity_lemma (_,(left,lem)) =
 
326
  if left then  
 
327
    transitivity_left_table  := lem :: !transitivity_left_table
 
328
  else
 
329
    transitivity_right_table := lem :: !transitivity_right_table
 
330
  
 
331
let subst_transitivity_lemma (_,subst,(b,ref)) = (b,subst_mps subst ref)
 
332
 
 
333
let (inTransitivity,_) =
 
334
  declare_object {(default_object "TRANSITIVITY-STEPS") with
 
335
    cache_function = cache_transitivity_lemma;
 
336
    open_function = (fun i o -> if i=1 then cache_transitivity_lemma o);
 
337
    subst_function = subst_transitivity_lemma;
 
338
    classify_function = (fun (_,o) -> Substitute o);       
 
339
    export_function = (fun x -> Some x) }
 
340
 
 
341
(* Synchronisation with reset *)
 
342
 
 
343
let freeze () = !transitivity_left_table, !transitivity_right_table
 
344
 
 
345
let unfreeze (l,r) = 
 
346
  transitivity_left_table := l;
 
347
  transitivity_right_table := r
 
348
 
 
349
let init () = 
 
350
  transitivity_left_table := [];
 
351
  transitivity_right_table := []
 
352
 
 
353
let _ = 
 
354
  declare_summary "transitivity-steps"
 
355
    { freeze_function = freeze;
 
356
      unfreeze_function = unfreeze;
 
357
      init_function = init;
 
358
      survive_module = false; 
 
359
      survive_section = false }
 
360
 
 
361
(* Main entry points *)
 
362
 
 
363
let add_transitivity_lemma left lem =
 
364
 let lem' = Constrintern.interp_constr Evd.empty (Global.env ()) lem in
 
365
  add_anonymous_leaf (inTransitivity (left,lem'))
 
366
 
 
367
(* Vernacular syntax *)
 
368
 
 
369
TACTIC EXTEND stepl
 
370
| ["stepl" constr(c) "by" tactic(tac) ] -> [ step true c (snd tac) ]
 
371
| ["stepl" constr(c) ] -> [ step true c tclIDTAC ]
 
372
END
 
373
 
 
374
TACTIC EXTEND stepr
 
375
| ["stepr" constr(c) "by" tactic(tac) ] -> [ step false c (snd tac) ]
 
376
| ["stepr" constr(c) ] -> [ step false c tclIDTAC ]
 
377
END
 
378
 
 
379
VERNAC COMMAND EXTEND AddStepl
 
380
| [ "Declare" "Left" "Step" constr(t) ] ->
 
381
    [ add_transitivity_lemma true t ]
 
382
END
 
383
 
 
384
VERNAC COMMAND EXTEND AddStepr
 
385
| [ "Declare" "Right" "Step" constr(t) ] ->
 
386
    [ add_transitivity_lemma false t ]
 
387
END
 
388
 
 
389
VERNAC COMMAND EXTEND ImplicitTactic
 
390
| [ "Declare" "Implicit" "Tactic" tactic(tac) ] ->
 
391
    [ Tacinterp.declare_implicit_tactic (Tacinterp.interp tac) ]
 
392
END
 
393
 
 
394
 
 
395
 
 
396
 
 
397
(*spiwack : Vernac commands for retroknowledge *)
 
398
 
 
399
VERNAC COMMAND EXTEND RetroknowledgeRegister
 
400
 | [ "Register" constr(c) "as" retroknowledge_field(f) "by" constr(b)] -> 
 
401
           [ let tc = Constrintern.interp_constr Evd.empty (Global.env ()) c in
 
402
             let tb = Constrintern.interp_constr Evd.empty (Global.env ()) b in
 
403
             Global.register f tc tb ]
 
404
END
 
405
 
 
406
 
 
407
 
 
408
(* sozeau: abs/gen for induction on instantiated dependent inductives, using "Ford" induction as 
 
409
  defined by Conor McBride *)
 
410
TACTIC EXTEND generalize_eqs
 
411
| ["generalize_eqs" hyp(id) ] -> [ abstract_generalize id ~generalize_vars:false ]
 
412
END
 
413
TACTIC EXTEND generalize_eqs_vars
 
414
| ["generalize_eqs_vars" hyp(id) ] -> [ abstract_generalize id ~generalize_vars:true ]
 
415
END
 
416
 
 
417
TACTIC EXTEND dependent_pattern
 
418
| ["dependent_pattern" constr(c) ] -> [ dependent_pattern c ]
 
419
END
 
420
 
 
421
TACTIC EXTEND resolve_classes
 
422
| ["resolve_classes" ] -> [ resolve_classes ]
 
423
END