/
tactics.ml
3886 lines (3440 loc) · 147 KB
/
tactics.ml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Pp
open Errors
open Util
open Names
open Nameops
open Term
open Vars
open Context
open Termops
open Namegen
open Declarations
open Inductiveops
open Reductionops
open Environ
open Globnames
open Evd
open Pfedit
open Tacred
open Genredexpr
open Tacmach
open Logic
open Clenv
open Clenvtac
open Refiner
open Tacticals
open Hipattern
open Coqlib
open Tacexpr
open Decl_kinds
open Evarutil
open Indrec
open Pretype_errors
open Unification
open Locus
open Locusops
open Misctypes
open Proofview.Notations
exception Bound
let nb_prod x =
let rec count n c =
match kind_of_term c with
Prod(_,_,t) -> count (n+1) t
| LetIn(_,a,_,t) -> count n (subst1 a t)
| Cast(c,_,_) -> count n c
| _ -> n
in count 0 x
let inj_with_occurrences e = (AllOccurrences,e)
let dloc = Loc.ghost
let typ_of = Retyping.get_type_of
(* Option for 8.2 compatibility *)
open Goptions
let dependent_propositions_elimination = ref true
let use_dependent_propositions_elimination () =
!dependent_propositions_elimination
&& Flags.version_strictly_greater Flags.V8_2
let _ =
declare_bool_option
{ optsync = true;
optdepr = false;
optname = "dependent-propositions-elimination tactic";
optkey = ["Dependent";"Propositions";"Elimination"];
optread = (fun () -> !dependent_propositions_elimination) ;
optwrite = (fun b -> dependent_propositions_elimination := b) }
let _ =
declare_bool_option
{ optsync = true;
optdepr = false;
optname = "trigger bugged context matching compatibility";
optkey = ["Tactic";"Compat";"Context"];
optread = (fun () -> !Flags.tactic_context_compat) ;
optwrite = (fun b -> Flags.tactic_context_compat := b) }
let tactic_infer_flags = {
Pretyping.use_typeclasses = true;
Pretyping.use_unif_heuristics = true;
Pretyping.use_hook = Some solve_by_implicit_tactic;
Pretyping.fail_evar = true;
Pretyping.expand_evars = true }
let finish_evar_resolution env initial_sigma (sigma,c) =
let sigma =
Pretyping.solve_remaining_evars tactic_infer_flags env initial_sigma sigma
in Evd.evar_universe_context sigma, nf_evar sigma c
(*********************************************)
(* Tactics *)
(*********************************************)
(****************************************)
(* General functions *)
(****************************************)
let head_constr_bound t =
let t = strip_outer_cast t in
let _,ccl = decompose_prod_assum t in
let hd,args = decompose_app ccl in
match kind_of_term hd with
| Const _ | Ind _ | Construct _ | Var _ -> hd
| Proj (p, _) -> mkConst p
| _ -> raise Bound
let head_constr c =
try head_constr_bound c with Bound -> error "Bound head variable."
(******************************************)
(* Primitive tactics *)
(******************************************)
let introduction = Tacmach.introduction
let refine = Tacmach.refine
let convert_concl = Tacmach.convert_concl
let convert_hyp = Tacmach.convert_hyp
let thin_body = Tacmach.thin_body
let convert_gen pb x y gl =
try tclEVARS (pf_apply Evd.conversion gl pb x y) gl
with Reduction.NotConvertible ->
tclFAIL_lazy 0 (lazy (str"Not convertible"))
(* Adding more information in this message, even under the lazy, can result in huge *)
(* blowups, time and spacewise... (see autos used in DoubleCyclic.) 2.3s against 15s. *)
(* ++ Printer.pr_constr_env env x ++ *)
(* str" and " ++ Printer.pr_constr_env env y)) *)
gl
let convert = convert_gen Reduction.CONV
let convert_leq = convert_gen Reduction.CUMUL
let error_clear_dependency env id = function
| Evarutil.OccurHypInSimpleClause None ->
errorlabstrm "" (pr_id id ++ str " is used in conclusion.")
| Evarutil.OccurHypInSimpleClause (Some id') ->
errorlabstrm ""
(pr_id id ++ strbrk " is used in hypothesis " ++ pr_id id' ++ str".")
| Evarutil.EvarTypingBreak ev ->
errorlabstrm ""
(str "Cannot remove " ++ pr_id id ++
strbrk " without breaking the typing of " ++
Printer.pr_existential env ev ++ str".")
let thin l gl =
try thin l gl
with Evarutil.ClearDependencyError (id,err) ->
error_clear_dependency (pf_env gl) id err
let internal_cut_gen b d t gl =
try internal_cut b d t gl
with Evarutil.ClearDependencyError (id,err) ->
error_clear_dependency (pf_env gl) id err
let internal_cut = internal_cut_gen false
let internal_cut_replace = internal_cut_gen true
let internal_cut_rev_gen b d t gl =
try internal_cut_rev b d t gl
with Evarutil.ClearDependencyError (id,err) ->
error_clear_dependency (pf_env gl) id err
let internal_cut_rev_replace = internal_cut_rev_gen true
(* Moving hypotheses *)
let move_hyp = Tacmach.move_hyp
(* Renaming hypotheses *)
let rename_hyp = Tacmach.rename_hyp
(**************************************************************)
(* Fresh names *)
(**************************************************************)
let fresh_id_in_env avoid id env =
next_ident_away_in_goal id (avoid@ids_of_named_context (named_context env))
let fresh_id avoid id gl =
fresh_id_in_env avoid id (pf_env gl)
let new_fresh_id avoid id gl =
fresh_id_in_env avoid id (Proofview.Goal.env gl)
(**************************************************************)
(* Fixpoints and CoFixpoints *)
(**************************************************************)
(* Refine as a fixpoint *)
let mutual_fix = Tacmach.mutual_fix
let fix ido n gl = match ido with
| None ->
mutual_fix (fresh_id [] (Pfedit.get_current_proof_name ()) gl) n [] 0 gl
| Some id ->
mutual_fix id n [] 0 gl
(* Refine as a cofixpoint *)
let mutual_cofix = Tacmach.mutual_cofix
let cofix ido gl = match ido with
| None ->
mutual_cofix (fresh_id [] (Pfedit.get_current_proof_name ()) gl) [] 0 gl
| Some id ->
mutual_cofix id [] 0 gl
(**************************************************************)
(* Reduction and conversion tactics *)
(**************************************************************)
type tactic_reduction = env -> evar_map -> constr -> constr
let pf_reduce_decl redfun where (id,c,ty) gl =
let redfun' = pf_reduce redfun gl in
match c with
| None ->
if where == InHypValueOnly then
errorlabstrm "" (pr_id id ++ str "has no value.");
(id,None,redfun' ty)
| Some b ->
let b' = if where != InHypTypeOnly then redfun' b else b in
let ty' = if where != InHypValueOnly then redfun' ty else ty in
(id,Some b',ty')
(* Possibly equip a reduction with the occurrences mentioned in an
occurrence clause *)
let error_illegal_clause () =
error "\"at\" clause not supported in presence of an occurrence clause."
let error_illegal_non_atomic_clause () =
error "\"at\" clause not supported in presence of a non atomic \"in\" clause."
let error_occurrences_not_unsupported () =
error "Occurrences not supported for this reduction tactic."
let bind_change_occurrences occs = function
| None -> None
| Some c -> Some (Redexpr.out_with_occurrences (occs,c))
let bind_red_expr_occurrences occs nbcl redexp =
let has_at_clause = function
| Unfold l -> List.exists (fun (occl,_) -> occl != AllOccurrences) l
| Pattern l -> List.exists (fun (occl,_) -> occl != AllOccurrences) l
| Simpl (Some (occl,_)) -> occl != AllOccurrences
| _ -> false in
if occs == AllOccurrences then
if nbcl > 1 && has_at_clause redexp then
error_illegal_non_atomic_clause ()
else
redexp
else
match redexp with
| Unfold (_::_::_) ->
error_illegal_clause ()
| Unfold [(occl,c)] ->
if occl != AllOccurrences then
error_illegal_clause ()
else
Unfold [(occs,c)]
| Pattern (_::_::_) ->
error_illegal_clause ()
| Pattern [(occl,c)] ->
if occl != AllOccurrences then
error_illegal_clause ()
else
Pattern [(occs,c)]
| Simpl (Some (occl,c)) ->
if occl != AllOccurrences then
error_illegal_clause ()
else
Simpl (Some (occs,c))
| CbvVm (Some (occl,c)) ->
if occl != AllOccurrences then
error_illegal_clause ()
else
CbvVm (Some (occs,c))
| CbvNative (Some (occl,c)) ->
if occl != AllOccurrences then
error_illegal_clause ()
else
CbvNative (Some (occs,c))
| Red _ | Hnf | Cbv _ | Lazy _ | Cbn _
| ExtraRedExpr _ | Fold _ | Simpl None | CbvVm None | CbvNative None ->
error_occurrences_not_unsupported ()
| Unfold [] | Pattern [] ->
assert false
(* The following two tactics apply an arbitrary
reduction function either to the conclusion or to a
certain hypothesis *)
let reduct_in_concl (redfun,sty) gl =
convert_concl_no_check (pf_reduce redfun gl (pf_concl gl)) sty gl
let reduct_in_hyp redfun (id,where) gl =
convert_hyp_no_check
(pf_reduce_decl redfun where (pf_get_hyp gl id) gl) gl
let revert_cast (redfun,kind as r) =
if kind == DEFAULTcast then (redfun,REVERTcast) else r
let reduct_option redfun = function
| Some id -> reduct_in_hyp (fst redfun) id
| None -> reduct_in_concl (revert_cast redfun)
(** Versions with evars to maintain the unification of universes resulting
from conversions. *)
let tclWITHEVARS f k gl =
let evm, c' = pf_apply f gl in
tclTHEN (tclEVARS evm) (k c') gl
let e_reduct_in_concl (redfun,sty) gl =
tclWITHEVARS
(fun env sigma -> redfun env sigma (pf_concl gl))
(fun c -> convert_concl_no_check c sty) gl
let e_pf_reduce_decl (redfun : e_reduction_function) where (id,c,ty) env sigma =
match c with
| None ->
if where == InHypValueOnly then
errorlabstrm "" (pr_id id ++ str "has no value.");
let sigma',ty' = redfun env sigma ty in
sigma', (id,None,ty')
| Some b ->
let sigma',b' = if where != InHypTypeOnly then redfun env sigma b else sigma, b in
let sigma',ty' = if where != InHypValueOnly then redfun env sigma ty else sigma', ty in
sigma', (id,Some b',ty')
let e_reduct_in_hyp redfun (id,where) gl =
tclWITHEVARS
(e_pf_reduce_decl redfun where (pf_get_hyp gl id))
convert_hyp_no_check gl
(* Now we introduce different instances of the previous tacticals *)
let change_and_check cv_pb t env sigma c =
let evd, b = infer_conv ~pb:cv_pb env sigma t c in
if b then evd, t
else
errorlabstrm "convert-check-hyp" (str "Not convertible.")
(* Use cumulativity only if changing the conclusion not a subterm *)
let change_on_subterm cv_pb t = function
| None -> change_and_check cv_pb t
| Some occl ->
e_contextually false occl
(fun subst -> change_and_check Reduction.CONV (replace_vars (Id.Map.bindings subst) t))
let change_in_concl occl t =
e_reduct_in_concl ((change_on_subterm Reduction.CUMUL t occl),DEFAULTcast)
let change_in_hyp occl t id =
with_check (e_reduct_in_hyp (change_on_subterm Reduction.CONV t occl) id)
let change_option occl t = function
| Some id -> change_in_hyp occl t id
| None -> change_in_concl occl t
let change chg c cls gl =
let cls = concrete_clause_of (fun () -> pf_ids_of_hyps gl) cls in
tclMAP (function
| OnHyp (id,occs,where) ->
change_option (bind_change_occurrences occs chg) c (Some (id,where))
| OnConcl occs ->
change_option (bind_change_occurrences occs chg) c None)
cls gl
(* Pour usage interne (le niveau User est pris en compte par reduce) *)
let red_in_concl = reduct_in_concl (red_product,REVERTcast)
let red_in_hyp = reduct_in_hyp red_product
let red_option = reduct_option (red_product,REVERTcast)
let hnf_in_concl = reduct_in_concl (hnf_constr,REVERTcast)
let hnf_in_hyp = reduct_in_hyp hnf_constr
let hnf_option = reduct_option (hnf_constr,REVERTcast)
let simpl_in_concl = reduct_in_concl (simpl,REVERTcast)
let simpl_in_hyp = reduct_in_hyp simpl
let simpl_option = reduct_option (simpl,REVERTcast)
let normalise_in_concl = reduct_in_concl (compute,REVERTcast)
let normalise_in_hyp = reduct_in_hyp compute
let normalise_option = reduct_option (compute,REVERTcast)
let normalise_vm_in_concl = reduct_in_concl (Redexpr.cbv_vm,VMcast)
let unfold_in_concl loccname = reduct_in_concl (unfoldn loccname,REVERTcast)
let unfold_in_hyp loccname = reduct_in_hyp (unfoldn loccname)
let unfold_option loccname = reduct_option (unfoldn loccname,DEFAULTcast)
let pattern_option l = reduct_option (pattern_occs l,DEFAULTcast)
(* The main reduction function *)
let reduction_clause redexp cl =
let nbcl = List.length cl in
List.map (function
| OnHyp (id,occs,where) ->
(Some (id,where), bind_red_expr_occurrences occs nbcl redexp)
| OnConcl occs ->
(None, bind_red_expr_occurrences occs nbcl redexp)) cl
let reduce redexp cl goal =
let cl = concrete_clause_of (fun () -> pf_ids_of_hyps goal) cl in
let redexps = reduction_clause redexp cl in
let tac = tclMAP (fun (where,redexp) ->
reduct_option
(Redexpr.reduction_of_red_expr (pf_env goal) redexp) where) redexps in
match redexp with
| Fold _ | Pattern _ -> with_check tac goal
| _ -> tac goal
(* Unfolding occurrences of a constant *)
let unfold_constr = function
| ConstRef sp -> unfold_in_concl [AllOccurrences,EvalConstRef sp]
| VarRef id -> unfold_in_concl [AllOccurrences,EvalVarRef id]
| _ -> errorlabstrm "unfold_constr" (str "Cannot unfold a non-constant.")
(*******************************************)
(* Introduction tactics *)
(*******************************************)
let id_of_name_with_default id = function
| Anonymous -> id
| Name id -> id
let hid = Id.of_string "H"
let xid = Id.of_string "X"
let default_id_of_sort = function Prop _ -> hid | Type _ -> xid
let default_id env sigma = function
| (name,None,t) ->
let dft = default_id_of_sort (Typing.sort_of env sigma t) in
id_of_name_with_default dft name
| (name,Some b,_) -> id_of_name_using_hdchar env b name
(* Non primitive introduction tactics are treated by central_intro
There is possibly renaming, with possibly names to avoid and
possibly a move to do after the introduction *)
type intro_name_flag =
| IntroAvoid of Id.t list
| IntroBasedOn of Id.t * Id.t list
| IntroMustBe of Id.t
let find_name loc decl x gl = match x with
| IntroAvoid idl ->
(* this case must be compatible with [find_intro_names] below. *)
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
new_fresh_id idl (default_id env sigma decl) gl
| IntroBasedOn (id,idl) -> new_fresh_id idl id gl
| IntroMustBe id ->
(* When name is given, we allow to hide a global name *)
let ids_of_hyps = Tacmach.New.pf_ids_of_hyps gl in
let id' = next_ident_away id ids_of_hyps in
if not (Id.equal id' id) then user_err_loc (loc,"",pr_id id ++ str" is already used.");
id'
(* Returns the names that would be created by intros, without doing
intros. This function is supposed to be compatible with an
iteration of [find_name] above. As [default_id] checks the sort of
the type to build hyp names, we maintain an environment to be able
to type dependent hyps. *)
let find_intro_names ctxt gl =
let _, res = List.fold_right
(fun decl acc ->
let wantedname,x,typdecl = decl in
let env,idl = acc in
let name = fresh_id idl (default_id env gl.sigma decl) gl in
let newenv = push_rel (wantedname,x,typdecl) env in
(newenv,(name::idl)))
ctxt (pf_env gl , []) in
List.rev res
let build_intro_tac id dest tac = match dest with
| MoveLast -> Tacticals.New.tclTHEN (Proofview.V82.tactic (introduction id)) (tac id)
| dest -> Tacticals.New.tclTHENLIST [Proofview.V82.tactic (introduction id); Proofview.V82.tactic (move_hyp true id dest); tac id]
let rec intro_then_gen loc name_flag move_flag force_flag dep_flag tac =
Proofview.Goal.raw_enter begin fun gl ->
let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in
let concl = nf_evar (Proofview.Goal.sigma gl) concl in
match kind_of_term concl with
| Prod (name,t,u) when not dep_flag || (dependent (mkRel 1) u) ->
let name = find_name loc (name,None,t) name_flag gl in
build_intro_tac name move_flag tac
| LetIn (name,b,t,u) when not dep_flag || (dependent (mkRel 1) u) ->
let name = find_name loc (name,Some b,t) name_flag gl in
build_intro_tac name move_flag tac
| _ ->
begin if not force_flag then Proofview.tclZERO (RefinerError IntroNeedsProduct)
(* Note: red_in_concl includes betaiotazeta and this was like *)
(* this since at least V6.3 (a pity *)
(* that intro do betaiotazeta only when reduction is needed; and *)
(* probably also a pity that intro does zeta *)
else Proofview.tclUNIT ()
end <*>
Proofview.tclORELSE
(Tacticals.New.tclTHEN (Proofview.V82.tactic hnf_in_concl)
(intro_then_gen loc name_flag move_flag false dep_flag tac))
begin function
| RefinerError IntroNeedsProduct ->
Proofview.tclZERO (Loc.add_loc (Errors.UserError("Intro",str "No product even after head-reduction.")) loc)
| e -> Proofview.tclZERO e
end
end
let intro_gen loc n m f d = intro_then_gen loc n m f d (fun _ -> Proofview.tclUNIT ())
let intro_mustbe_force id = intro_gen dloc (IntroMustBe id) MoveLast true false
let intro_using id = intro_gen dloc (IntroBasedOn (id,[])) MoveLast false false
let intro_then = intro_then_gen dloc (IntroAvoid []) MoveLast false false
let intro = intro_gen dloc (IntroAvoid []) MoveLast false false
let introf = intro_gen dloc (IntroAvoid []) MoveLast true false
let intro_avoiding l = intro_gen dloc (IntroAvoid l) MoveLast false false
let intro_then_force = intro_then_gen dloc (IntroAvoid []) MoveLast true false
(**** Multiple introduction tactics ****)
let rec intros_using = function
| [] -> Proofview.tclUNIT()
| str::l -> Tacticals.New.tclTHEN (intro_using str) (intros_using l)
let intros = Tacticals.New.tclREPEAT intro
let intro_forthcoming_then_gen loc name_flag move_flag dep_flag tac =
let rec aux ids =
Proofview.tclORELSE
begin
intro_then_gen loc name_flag move_flag false dep_flag
(fun id -> aux (id::ids))
end
begin function
| RefinerError IntroNeedsProduct ->
tac ids
| e -> Proofview.tclZERO e
end
in
aux []
let rec get_next_hyp_position id = function
| [] -> raise (RefinerError (NoSuchHyp id))
| (hyp,_,_) :: right ->
if Id.equal hyp id then
match right with (id,_,_)::_ -> MoveBefore id | [] -> MoveLast
else
get_next_hyp_position id right
let thin_for_replacing l gl =
try Tacmach.thin l gl
with Evarutil.ClearDependencyError (id,err) -> match err with
| Evarutil.OccurHypInSimpleClause None ->
errorlabstrm ""
(str "Cannot change " ++ pr_id id ++ str ", it is used in conclusion.")
| Evarutil.OccurHypInSimpleClause (Some id') ->
errorlabstrm ""
(str "Cannot change " ++ pr_id id ++
strbrk ", it is used in hypothesis " ++ pr_id id' ++ str".")
| Evarutil.EvarTypingBreak ev ->
errorlabstrm ""
(str "Cannot change " ++ pr_id id ++
strbrk " without breaking the typing of " ++
Printer.pr_existential (pf_env gl) ev ++ str".")
let intro_replacing id gl =
let next_hyp = get_next_hyp_position id (pf_hyps gl) in
tclTHENLIST
[thin_for_replacing [id]; introduction id; move_hyp true id next_hyp] gl
let intros_replacing ids =
let rec introrec = function
| [] -> Proofview.tclUNIT()
| id::tl ->
Tacticals.New.tclTHEN (Tacticals.New.tclORELSE (Proofview.V82.tactic (intro_replacing id)) (intro_using id))
(introrec tl)
in
introrec ids
(* User-level introduction tactics *)
let intro_move idopt hto = match idopt with
| None -> intro_gen dloc (IntroAvoid []) hto true false
| Some id -> intro_gen dloc (IntroMustBe id) hto true false
let pf_lookup_hypothesis_as_renamed env ccl = function
| AnonHyp n -> Detyping.lookup_index_as_renamed env ccl n
| NamedHyp id -> Detyping.lookup_name_as_displayed env ccl id
let pf_lookup_hypothesis_as_renamed_gen red h gl =
let env = pf_env gl in
let rec aux ccl =
match pf_lookup_hypothesis_as_renamed env ccl h with
| None when red ->
aux
((fst (Redexpr.reduction_of_red_expr env (Red true)))
env (project gl) ccl)
| x -> x
in
try aux (pf_concl gl)
with Redelimination -> None
let is_quantified_hypothesis id g =
match pf_lookup_hypothesis_as_renamed_gen true (NamedHyp id) g with
| Some _ -> true
| None -> false
let msg_quantified_hypothesis = function
| NamedHyp id ->
str "quantified hypothesis named " ++ pr_id id
| AnonHyp n ->
int n ++ str (match n with 1 -> "st" | 2 -> "nd" | _ -> "th") ++
str " non dependent hypothesis"
let depth_of_quantified_hypothesis red h gl =
match pf_lookup_hypothesis_as_renamed_gen red h gl with
| Some depth -> depth
| None ->
errorlabstrm "lookup_quantified_hypothesis"
(str "No " ++ msg_quantified_hypothesis h ++
strbrk " in current goal" ++
(if red then strbrk " even after head-reduction" else mt ()) ++
str".")
let intros_until_gen red h =
Proofview.Goal.enter begin fun gl ->
let n = Tacmach.New.of_old (depth_of_quantified_hypothesis red h) gl in
Tacticals.New.tclDO n (if red then introf else intro)
end
let intros_until_id id = intros_until_gen false (NamedHyp id)
let intros_until_n_gen red n = intros_until_gen red (AnonHyp n)
let intros_until = intros_until_gen true
let intros_until_n = intros_until_n_gen true
let tclCHECKVAR id gl = ignore (pf_get_hyp gl id); tclIDTAC gl
let try_intros_until_id_check id =
Tacticals.New.tclORELSE (intros_until_id id) (Proofview.V82.tactic (tclCHECKVAR id))
let try_intros_until tac = function
| NamedHyp id -> Tacticals.New.tclTHEN (try_intros_until_id_check id) (tac id)
| AnonHyp n -> Tacticals.New.tclTHEN (intros_until_n n) (Tacticals.New.onLastHypId tac)
let rec intros_move = function
| [] -> Proofview.tclUNIT ()
| (hyp,destopt) :: rest ->
Tacticals.New.tclTHEN (intro_gen dloc (IntroMustBe hyp) destopt false false)
(intros_move rest)
let dependent_in_decl a (_,c,t) =
match c with
| None -> dependent a t
| Some body -> dependent a body || dependent a t
(* Apply a tactic on a quantified hypothesis, an hypothesis in context
or a term with bindings *)
let onOpenInductionArg tac = function
| ElimOnConstr cbl ->
tac cbl
| ElimOnAnonHyp n ->
Tacticals.New.tclTHEN
(intros_until_n n)
(Tacticals.New.onLastHyp (fun c -> tac (Evd.empty,(c,NoBindings))))
| ElimOnIdent (_,id) ->
(* A quantified hypothesis *)
Tacticals.New.tclTHEN
(try_intros_until_id_check id)
(tac (Evd.empty,(mkVar id,NoBindings)))
let onInductionArg tac = function
| ElimOnConstr cbl ->
tac cbl
| ElimOnAnonHyp n ->
Tacticals.New.tclTHEN (intros_until_n n) (Tacticals.New.onLastHyp (fun c -> tac (c,NoBindings)))
| ElimOnIdent (_,id) ->
(* A quantified hypothesis *)
Tacticals.New.tclTHEN (try_intros_until_id_check id) (tac (mkVar id,NoBindings))
let map_induction_arg f = function
| ElimOnConstr (sigma,(c,bl)) -> ElimOnConstr (f (sigma,c),bl)
| ElimOnAnonHyp n -> ElimOnAnonHyp n
| ElimOnIdent id -> ElimOnIdent id
(**************************)
(* Refinement tactics *)
(**************************)
let apply_type hdcty argl gl =
refine (applist (mkCast (Evarutil.mk_new_meta(),DEFAULTcast, hdcty),argl)) gl
let bring_hyps hyps =
if List.is_empty hyps then Tacticals.New.tclIDTAC
else
Proofview.Goal.raw_enter begin fun gl ->
let env = Proofview.Goal.env gl in
let concl = Tacmach.New.pf_nf_concl gl in
let newcl = List.fold_right mkNamedProd_or_LetIn hyps concl in
let args = Array.of_list (instance_from_named_context hyps) in
Proofview.Refine.refine begin fun h ->
let (h, ev) = Proofview.Refine.new_evar h env newcl in
(h, (mkApp (ev, args)))
end
end
(**************************)
(* Cut tactics *)
(**************************)
let cut c =
Proofview.Goal.raw_enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
let concl = Tacmach.New.pf_nf_concl gl in
let is_sort =
try
(** Backward compat: ensure that [c] is well-typed. *)
let typ = Typing.type_of env sigma c in
let typ = whd_betadeltaiota env sigma typ in
match kind_of_term typ with
| Sort _ -> true
| _ -> false
with e when Pretype_errors.precatchable_exception e -> false
in
if is_sort then
let id = next_name_away_with_default "H" Anonymous (Tacmach.New.pf_ids_of_hyps gl) in
(** Backward compat: normalize [c]. *)
let c = local_strong whd_betaiota sigma c in
Proofview.Refine.refine begin fun h ->
let (h, f) = Proofview.Refine.new_evar h env (mkArrow c (Vars.lift 1 concl)) in
let (h, x) = Proofview.Refine.new_evar h env c in
let f = mkLambda (Name id, c, mkApp (Vars.lift 1 f, [|mkRel 1|])) in
(h, mkApp (f, [|x|]))
end
else
Tacticals.New.tclZEROMSG (str "Not a proposition or a type.")
end
let cut_intro t = Tacticals.New.tclTHENFIRST (cut t) intro
(* [assert_replacing id T tac] adds the subgoals of the proof of [T]
before the current goal
id:T0 id:T0 id:T
===== ------> tac(=====) + ====
G T G
It fails if the hypothesis to replace appears in the goal or in
another hypothesis.
*)
let assert_replacing id t tac = tclTHENFIRST (internal_cut_replace id t) tac
(* [cut_replacing id T tac] adds the subgoals of the proof of [T]
after the current goal
id:T0 id:T id:T0
===== ------> ==== + tac(=====)
G G T
It fails if the hypothesis to replace appears in the goal or in
another hypothesis.
*)
let cut_replacing id t tac = tclTHENLAST (internal_cut_rev_replace id t) tac
let error_uninstantiated_metas t clenv =
let na = meta_name clenv.evd (List.hd (Metaset.elements (metavars_of t))) in
let id = match na with Name id -> id | _ -> anomaly (Pp.str "unnamed dependent meta")
in errorlabstrm "" (str "Cannot find an instance for " ++ pr_id id ++ str".")
(* For a clenv expressing some lemma [C[?1:T1,...,?n:Tn] : P] and some
goal [G], [clenv_refine_in] returns [n+1] subgoals, the [n] last
ones (resp [n] first ones if [sidecond_first] is [true]) being the
[Ti] and the first one (resp last one) being [G] whose hypothesis
[id] is replaced by P using the proof given by [tac] *)
let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true) id clenv gl =
let clenv = clenv_pose_dependent_evars with_evars clenv in
let clenv =
if with_classes then
{ clenv with evd = Typeclasses.resolve_typeclasses ~fail:(not with_evars) clenv.env clenv.evd }
else clenv
in
let new_hyp_typ = clenv_type clenv in
if not with_evars && occur_meta new_hyp_typ then
error_uninstantiated_metas new_hyp_typ clenv;
let new_hyp_prf = clenv_value clenv in
tclTHEN
(tclEVARS clenv.evd)
((if sidecond_first then assert_replacing else cut_replacing)
id new_hyp_typ (refine_no_check new_hyp_prf)) gl
(********************************************)
(* Elimination tactics *)
(********************************************)
let last_arg c = match kind_of_term c with
| App (f,cl) ->
Array.last cl
| _ -> anomaly (Pp.str "last_arg")
let nth_arg i c =
if Int.equal i (-1) then last_arg c else
match kind_of_term c with
| App (f,cl) -> cl.(i)
| _ -> anomaly (Pp.str "nth_arg")
let index_of_ind_arg t =
let rec aux i j t = match kind_of_term t with
| Prod (_,t,u) ->
(* heuristic *)
if isInd (fst (decompose_app t)) then aux (Some j) (j+1) u
else aux i (j+1) u
| _ -> match i with
| Some i -> i
| None -> error "Could not find inductive argument of elimination scheme."
in aux None 0 t
let elimination_clause_scheme with_evars ?(flags=elim_flags ()) i elimclause indclause gl =
let indmv =
(match kind_of_term (nth_arg i elimclause.templval.rebus) with
| Meta mv -> mv
| _ -> errorlabstrm "elimination_clause"
(str "The type of elimination clause is not well-formed."))
in
let elimclause' = clenv_fchain ~flags indmv elimclause indclause in
res_pf elimclause' ~with_evars:with_evars ~flags gl
(*
* Elimination tactic with bindings and using an arbitrary
* elimination constant called elimc. This constant should end
* with a clause (x:I)(P .. ), where P is a bound variable.
* The term c is of type t, which is a product ending with a type
* matching I, lbindc are the expected terms for c arguments
*)
type eliminator = {
elimindex : int option; (* None = find it automatically *)
elimbody : constr with_bindings
}
let general_elim_clause_gen elimtac indclause elim gl =
let (elimc,lbindelimc) = elim.elimbody in
let elimt = pf_type_of gl elimc in
let i =
match elim.elimindex with None -> index_of_ind_arg elimt | Some i -> i in
let elimclause = pf_apply make_clenv_binding gl (elimc,elimt) lbindelimc in
elimtac i elimclause indclause gl
let general_elim_clause elimtac (c,lbindc) elim gl =
let ct = pf_type_of gl c in
let t = try snd (pf_reduce_to_quantified_ind gl ct) with UserError _ -> ct in
let indclause = pf_apply make_clenv_binding gl (c,t) lbindc in
general_elim_clause_gen elimtac indclause elim gl
let general_elim with_evars c e =
general_elim_clause (elimination_clause_scheme with_evars) c e
(* Case analysis tactics *)
let general_case_analysis_in_context with_evars (c,lbindc) gl =
let (mind,_) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
let sort = elimination_sort_of_goal gl in
let sigma, elim =
if occur_term c (pf_concl gl) then
pf_apply build_case_analysis_scheme gl mind true sort
else
pf_apply build_case_analysis_scheme_default gl mind sort in
tclTHEN (tclEVARS sigma)
(general_elim with_evars (c,lbindc)
{elimindex = None; elimbody = (elim,NoBindings)}) gl
let general_case_analysis with_evars (c,lbindc as cx) =
match kind_of_term c with
| Var id when lbindc == NoBindings ->
Tacticals.New.tclTHEN (try_intros_until_id_check id)
(Proofview.V82.tactic (general_case_analysis_in_context with_evars cx))
| _ ->
Proofview.V82.tactic (general_case_analysis_in_context with_evars cx)
let simplest_case c = general_case_analysis false (c,NoBindings)
(* Elimination tactic with bindings but using the default elimination
* constant associated with the type. *)
exception IsRecord
let is_record mind = (Global.lookup_mind (fst mind)).mind_record
let find_ind_eliminator ind s gl =
let gr = lookup_eliminator ind s in
let evd, c = pf_apply Evd.fresh_global gl gr in
evd, c
let find_eliminator c gl =
let ((ind,u),t) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
if is_record ind <> None then raise IsRecord;
let evd, c = find_ind_eliminator ind (elimination_sort_of_goal gl) gl in
evd, {elimindex = None; elimbody = (c,NoBindings)}
let default_elim with_evars (c,_ as cx) =
Proofview.tclORELSE
(Proofview.Goal.enter begin fun gl ->
let evd, elim = Tacmach.New.of_old (find_eliminator c) gl in
Proofview.V82.tactic (tclTHEN (tclEVARS evd) (general_elim with_evars cx elim))
end)
begin function
| IsRecord ->
(* For records, induction principles aren't there by default
anymore. Instead, we do a case analysis instead. *)
general_case_analysis with_evars cx
| e -> Proofview.tclZERO e
end
let elim_in_context with_evars c = function
| Some elim ->
Proofview.V82.tactic (general_elim with_evars c {elimindex = Some (-1); elimbody = elim})
| None -> default_elim with_evars c
let elim with_evars (c,lbindc as cx) elim =
match kind_of_term c with
| Var id when lbindc == NoBindings ->
Tacticals.New.tclTHEN (try_intros_until_id_check id)
(elim_in_context with_evars cx elim)
| _ ->
elim_in_context with_evars cx elim
(* The simplest elimination tactic, with no substitutions at all. *)
let simplest_elim c = default_elim false (c,NoBindings)
(* Elimination in hypothesis *)
(* Typically, elimclause := (eq_ind ?x ?P ?H ?y ?Heq : ?P ?y)
indclause : forall ..., hyps -> a=b (to take place of ?Heq)
id : phi(a) (to take place of ?H)
and the result is to overwrite id with the proof of phi(b)
but this generalizes to any elimination scheme with one constructor
(e.g. it could replace id:A->B->C by id:C, knowing A/\B)
*)
let clenv_fchain_in id ?(flags=elim_flags ()) mv elimclause hypclause =
try clenv_fchain ~flags mv elimclause hypclause
with PretypeError (env,evd,NoOccurrenceFound (op,_)) ->
(* Set the hypothesis name in the message *)
raise (PretypeError (env,evd,NoOccurrenceFound (op,Some id)))
let elimination_in_clause_scheme with_evars ?(flags=elim_flags ()) id i elimclause indclause gl =
let indmv = destMeta (nth_arg i elimclause.templval.rebus) in
let hypmv =
try match List.remove Int.equal indmv (clenv_independent elimclause) with
| [a] -> a
| _ -> failwith ""
with Failure _ -> errorlabstrm "elimination_clause"
(str "The type of elimination clause is not well-formed.") in
let elimclause' = clenv_fchain ~flags indmv elimclause indclause in
let hyp = mkVar id in
let hyp_typ = pf_type_of gl hyp in
let hypclause = mk_clenv_from_n gl (Some 0) (hyp, hyp_typ) in
let elimclause'' = clenv_fchain_in id ~flags hypmv elimclause' hypclause in
let new_hyp_typ = clenv_type elimclause'' in
if eq_constr hyp_typ new_hyp_typ then
errorlabstrm "general_rewrite_in"
(str "Nothing to rewrite in " ++ pr_id id ++ str".");
clenv_refine_in with_evars id elimclause'' gl
(* Apply a tactic below the products of the conclusion of a lemma *)
type conjunction_status =
| DefinedRecord of constant option list
| NotADefinedRecordUseScheme of constr
let make_projection env sigma params cstr sign elim i n c u =
let elim = match elim with
| NotADefinedRecordUseScheme elim ->
(* bugs: goes from right to left when i increases! *)
let (na,b,t) = List.nth cstr.cs_args i in
let b = match b with None -> mkRel (i+1) | Some b -> b in
let branch = it_mkLambda_or_LetIn b cstr.cs_args in
if
(* excludes dependent projection types *)
noccur_between 1 (n-i-1) t
(* excludes flexible projection types *)
&& not (isEvar (fst (whd_betaiota_stack sigma t)))
then
let t = lift (i+1-n) t in
let abselim = beta_applist (elim,params@[t;branch]) in
let c = beta_applist (abselim, [mkApp (c, extended_rel_vect 0 sign)]) in