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
(************************************************************************)
9
(* $Id: tactics.ml 12187 2009-06-13 19:36:59Z msozeau $ *)
52
match kind_of_term c with
53
Prod(_,_,t) -> count (n+1) t
54
| LetIn(_,a,_,t) -> count n (subst1 a t)
55
| Cast(c,_,_) -> count n c
59
let inj_with_occurrences e = (all_occurrences_expr,e)
61
let inj_open c = (Evd.empty,c)
63
let inj_occ (occ,c) = (occ,inj_open c)
65
let inj_red_expr = function
66
| Simpl lo -> Simpl (Option.map inj_occ lo)
67
| Fold l -> Fold (List.map inj_open l)
68
| Pattern l -> Pattern (List.map inj_occ l)
69
| (ExtraRedExpr _ | CbvVm | Red _ | Hnf | Cbv _ | Lazy _ | Unfold _ as c)
72
let inj_ebindings = function
73
| NoBindings -> NoBindings
74
| ImplicitBindings l -> ImplicitBindings (List.map inj_open l)
75
| ExplicitBindings l ->
76
ExplicitBindings (List.map (fun (l,id,c) -> (l,id,inj_open c)) l)
80
(*********************************************)
82
(*********************************************)
84
(****************************************)
85
(* General functions *)
86
(****************************************)
88
let string_of_inductive c =
89
try match kind_of_term c with
91
let (mib,mip) = Global.lookup_inductive ind_sp in
92
string_of_id mip.mind_typename
94
with Bound -> error "Bound head variable."
96
let rec head_constr_bound t =
97
let t = strip_outer_cast t in
98
let _,ccl = decompose_prod_assum t in
99
let hd,args = decompose_app ccl in
100
match kind_of_term hd with
101
| Const _ | Ind _ | Construct _ | Var _ -> (hd,args)
105
try head_constr_bound c with Bound -> error "Bound head variable."
107
(******************************************)
108
(* Primitive tactics *)
109
(******************************************)
111
let introduction = Tacmach.introduction
112
let refine = Tacmach.refine
113
let convert_concl = Tacmach.convert_concl
114
let convert_hyp = Tacmach.convert_hyp
115
let thin_body = Tacmach.thin_body
117
let error_clear_dependency env id = function
118
| Evarutil.OccurHypInSimpleClause None ->
119
errorlabstrm "" (pr_id id ++ str " is used in conclusion.")
120
| Evarutil.OccurHypInSimpleClause (Some id') ->
122
(pr_id id ++ strbrk " is used in hypothesis " ++ pr_id id' ++ str".")
123
| Evarutil.EvarTypingBreak ev ->
125
(str "Cannot remove " ++ pr_id id ++
126
strbrk " without breaking the typing of " ++
127
Printer.pr_existential env ev ++ str".")
131
with Evarutil.ClearDependencyError (id,err) ->
132
error_clear_dependency (pf_env gl) id err
134
let internal_cut_gen b d t gl =
135
try internal_cut b d t gl
136
with Evarutil.ClearDependencyError (id,err) ->
137
error_clear_dependency (pf_env gl) id err
139
let internal_cut = internal_cut_gen false
140
let internal_cut_replace = internal_cut_gen true
142
let internal_cut_rev_gen b d t gl =
143
try internal_cut_rev b d t gl
144
with Evarutil.ClearDependencyError (id,err) ->
145
error_clear_dependency (pf_env gl) id err
147
let internal_cut_rev = internal_cut_rev_gen false
148
let internal_cut_rev_replace = internal_cut_rev_gen true
150
(* Moving hypotheses *)
151
let move_hyp = Tacmach.move_hyp
153
let order_hyps = Tacmach.order_hyps
155
(* Renaming hypotheses *)
156
let rename_hyp = Tacmach.rename_hyp
158
(**************************************************************)
160
(**************************************************************)
162
let fresh_id_avoid avoid id =
163
next_global_ident_away true id avoid
165
let fresh_id avoid id gl =
166
fresh_id_avoid (avoid@(pf_ids_of_hyps gl)) id
168
(**************************************************************)
169
(* Fixpoints and CoFixpoints *)
170
(**************************************************************)
172
(* Refine as a fixpoint *)
173
let mutual_fix = Tacmach.mutual_fix
175
let fix ido n gl = match ido with
177
mutual_fix (fresh_id [] (Pfedit.get_current_proof_name ()) gl) n [] gl
179
mutual_fix id n [] gl
181
(* Refine as a cofixpoint *)
182
let mutual_cofix = Tacmach.mutual_cofix
184
let cofix ido gl = match ido with
186
mutual_cofix (fresh_id [] (Pfedit.get_current_proof_name ()) gl) [] gl
188
mutual_cofix id [] gl
190
(**************************************************************)
191
(* Reduction and conversion tactics *)
192
(**************************************************************)
194
type tactic_reduction = env -> evar_map -> constr -> constr
196
let pf_reduce_decl redfun where (id,c,ty) gl =
197
let redfun' = pf_reduce redfun gl in
200
if where = InHypValueOnly then
201
errorlabstrm "" (pr_id id ++ str "has no value.");
204
let b' = if where <> InHypTypeOnly then redfun' b else b in
205
let ty' = if where <> InHypValueOnly then redfun' ty else ty in
208
(* The following two tactics apply an arbitrary
209
reduction function either to the conclusion or to a
210
certain hypothesis *)
212
let reduct_in_concl (redfun,sty) gl =
213
convert_concl_no_check (pf_reduce redfun gl (pf_concl gl)) sty gl
215
let reduct_in_hyp redfun ((_,id),where) gl =
217
(pf_reduce_decl redfun where (pf_get_hyp gl id) gl) gl
219
let reduct_option redfun = function
220
| Some id -> reduct_in_hyp (fst redfun) id
221
| None -> reduct_in_concl redfun
223
(* The following tactic determines whether the reduction
224
function has to be applied to the conclusion or
225
to the hypotheses. *)
227
let redin_combinator redfun =
228
onClauses (reduct_option redfun)
230
(* Now we introduce different instances of the previous tacticals *)
231
let change_and_check cv_pb t env sigma c =
232
if is_fconv cv_pb env sigma t c then
235
errorlabstrm "convert-check-hyp" (str "Not convertible.")
237
(* Use cumulutavity only if changing the conclusion not a subterm *)
238
let change_on_subterm cv_pb t = function
239
| None -> change_and_check cv_pb t
240
| Some occl -> contextually false occl (change_and_check Reduction.CONV t)
242
let change_in_concl occl t =
243
reduct_in_concl ((change_on_subterm Reduction.CUMUL t occl),DEFAULTcast)
245
let change_in_hyp occl t id =
246
with_check (reduct_in_hyp (change_on_subterm Reduction.CONV t occl) id)
248
let change_option occl t = function
249
Some id -> change_in_hyp occl t id
250
| None -> change_in_concl occl t
252
let change occl c cls =
253
(match cls, occl with
254
({onhyps=(Some(_::_::_)|None)}
255
|{onhyps=Some(_::_);concl_occs=((false,_)|(true,_::_))}),
257
error "No occurrences expected when changing several hypotheses."
259
onClauses (change_option occl c) cls
261
(* Pour usage interne (le niveau User est pris en compte par reduce) *)
262
let red_in_concl = reduct_in_concl (red_product,DEFAULTcast)
263
let red_in_hyp = reduct_in_hyp red_product
264
let red_option = reduct_option (red_product,DEFAULTcast)
265
let hnf_in_concl = reduct_in_concl (hnf_constr,DEFAULTcast)
266
let hnf_in_hyp = reduct_in_hyp hnf_constr
267
let hnf_option = reduct_option (hnf_constr,DEFAULTcast)
268
let simpl_in_concl = reduct_in_concl (simpl,DEFAULTcast)
269
let simpl_in_hyp = reduct_in_hyp simpl
270
let simpl_option = reduct_option (simpl,DEFAULTcast)
271
let normalise_in_concl = reduct_in_concl (compute,DEFAULTcast)
272
let normalise_in_hyp = reduct_in_hyp compute
273
let normalise_option = reduct_option (compute,DEFAULTcast)
274
let normalise_vm_in_concl = reduct_in_concl (Redexpr.cbv_vm,VMcast)
275
let unfold_in_concl loccname = reduct_in_concl (unfoldn loccname,DEFAULTcast)
276
let unfold_in_hyp loccname = reduct_in_hyp (unfoldn loccname)
277
let unfold_option loccname = reduct_option (unfoldn loccname,DEFAULTcast)
278
let pattern_option l = reduct_option (pattern_occs l,DEFAULTcast)
280
(* A function which reduces accordingly to a reduction expression,
281
as the command Eval does. *)
283
let checking_fun = function
284
(* Expansion is not necessarily well-typed: e.g. expansion of t into x is
285
not well-typed in [H:(P t); x:=t |- G] because x is defined after H *)
286
| Fold _ -> with_check
287
| Pattern _ -> with_check
290
let reduce redexp cl goal =
291
let red = Redexpr.reduction_of_red_expr redexp in
293
(Fold _|Pattern _) -> with_check (redin_combinator red cl) goal
294
| _ -> redin_combinator red cl goal
296
(* Unfolding occurrences of a constant *)
298
let unfold_constr = function
299
| ConstRef sp -> unfold_in_concl [all_occurrences,EvalConstRef sp]
300
| VarRef id -> unfold_in_concl [all_occurrences,EvalVarRef id]
301
| _ -> errorlabstrm "unfold_constr" (str "Cannot unfold a non-constant.")
303
(*******************************************)
304
(* Introduction tactics *)
305
(*******************************************)
307
let id_of_name_with_default id = function
311
let hid = id_of_string "H"
312
let xid = id_of_string "X"
314
let default_id_of_sort = function Prop _ -> hid | Type _ -> xid
316
let default_id env sigma = function
318
let dft = default_id_of_sort (Typing.sort_of env sigma t) in
319
id_of_name_with_default dft name
320
| (name,Some b,_) -> id_of_name_using_hdchar env b name
322
(* Non primitive introduction tactics are treated by central_intro
323
There is possibly renaming, with possibly names to avoid and
324
possibly a move to do after the introduction *)
326
type intro_name_flag =
327
| IntroAvoid of identifier list
328
| IntroBasedOn of identifier * identifier list
329
| IntroMustBe of identifier
331
let find_name loc decl gl = function
333
(* this case must be compatible with [find_intro_names] below. *)
334
let id = fresh_id idl (default_id (pf_env gl) gl.sigma decl) gl in id
335
| IntroBasedOn (id,idl) -> fresh_id idl id gl
337
let id' = fresh_id [] id gl in
338
if id'<>id then user_err_loc (loc,"",pr_id id ++ str" is already used.");
341
(* Returns the names that would be created by intros, without doing
342
intros. This function is supposed to be compatible with an
343
iteration of [find_name] above. As [default_id] checks the sort of
344
the type to build hyp names, we maintain an environment to be able
345
to type dependent hyps. *)
346
let find_intro_names ctxt gl =
347
let _, res = List.fold_right
349
let wantedname,x,typdecl = decl in
351
let name = fresh_id idl (default_id env gl.sigma decl) gl in
352
let newenv = push_rel (wantedname,x,typdecl) env in
353
(newenv,(name::idl)))
354
ctxt (pf_env gl , []) in
357
let build_intro_tac id = function
358
| MoveToEnd true -> introduction id
359
| dest -> tclTHEN (introduction id) (move_hyp true id dest)
361
let rec intro_gen loc name_flag move_flag force_flag gl =
362
match kind_of_term (pf_concl gl) with
364
build_intro_tac (find_name loc (name,None,t) gl name_flag) move_flag gl
365
| LetIn (name,b,t,_) ->
366
build_intro_tac (find_name loc (name,Some b,t) gl name_flag) move_flag
369
if not force_flag then raise (RefinerError IntroNeedsProduct);
372
(reduce (Red true) onConcl)
373
(intro_gen loc name_flag move_flag force_flag) gl
374
with Redelimination ->
375
user_err_loc(loc,"Intro",str "No product even after head-reduction.")
377
let intro_mustbe_force id = intro_gen dloc (IntroMustBe id) no_move true
378
let intro_using id = intro_gen dloc (IntroBasedOn (id,[])) no_move false
379
let intro_force force_flag = intro_gen dloc (IntroAvoid []) no_move force_flag
380
let intro = intro_force false
381
let introf = intro_force true
383
let intro_avoiding l = intro_gen dloc (IntroAvoid l) no_move false
385
let introf_move_name destopt = intro_gen dloc (IntroAvoid []) destopt true
387
(**** Multiple introduction tactics ****)
389
let rec intros_using = function
391
| str::l -> tclTHEN (intro_using str) (intros_using l)
393
let intros = tclREPEAT (intro_force false)
395
let intro_erasing id = tclTHEN (thin [id]) (introduction id)
397
let rec get_next_hyp_position id = function
398
| [] -> error ("No such hypothesis: " ^ string_of_id id)
399
| (hyp,_,_) :: right ->
401
match right with (id,_,_)::_ -> MoveBefore id | [] -> MoveToEnd true
403
get_next_hyp_position id right
405
let thin_for_replacing l gl =
406
try Tacmach.thin l gl
407
with Evarutil.ClearDependencyError (id,err) -> match err with
408
| Evarutil.OccurHypInSimpleClause None ->
410
(str "Cannot change " ++ pr_id id ++ str ", it is used in conclusion.")
411
| Evarutil.OccurHypInSimpleClause (Some id') ->
413
(str "Cannot change " ++ pr_id id ++
414
strbrk ", it is used in hypothesis " ++ pr_id id' ++ str".")
415
| Evarutil.EvarTypingBreak ev ->
417
(str "Cannot change " ++ pr_id id ++
418
strbrk " without breaking the typing of " ++
419
Printer.pr_existential (pf_env gl) ev ++ str".")
421
let intro_replacing id gl =
422
let next_hyp = get_next_hyp_position id (pf_hyps gl) in
424
[thin_for_replacing [id]; introduction id; move_hyp true id next_hyp] gl
426
let intros_replacing ids gl =
427
let rec introrec = function
430
tclTHEN (tclORELSE (intro_replacing id) (intro_using id))
435
(* User-level introduction tactics *)
437
let intro_move idopt hto = match idopt with
438
| None -> intro_gen dloc (IntroAvoid []) hto true
439
| Some id -> intro_gen dloc (IntroMustBe id) hto true
441
let pf_lookup_hypothesis_as_renamed env ccl = function
442
| AnonHyp n -> pf_lookup_index_as_renamed env ccl n
443
| NamedHyp id -> pf_lookup_name_as_renamed env ccl id
445
let pf_lookup_hypothesis_as_renamed_gen red h gl =
446
let env = pf_env gl in
448
match pf_lookup_hypothesis_as_renamed env ccl h with
451
((fst (Redexpr.reduction_of_red_expr (Red true)))
452
env (project gl) ccl)
455
try aux (pf_concl gl)
456
with Redelimination -> None
458
let is_quantified_hypothesis id g =
459
match pf_lookup_hypothesis_as_renamed_gen true (NamedHyp id) g with
463
let msg_quantified_hypothesis = function
465
str "quantified hypothesis named " ++ pr_id id
467
int n ++ str (match n with 1 -> "st" | 2 -> "nd" | _ -> "th") ++
468
str " non dependent hypothesis"
470
let depth_of_quantified_hypothesis red h gl =
471
match pf_lookup_hypothesis_as_renamed_gen red h gl with
472
| Some depth -> depth
474
errorlabstrm "lookup_quantified_hypothesis"
475
(str "No " ++ msg_quantified_hypothesis h ++
476
strbrk " in current goal" ++
477
(if red then strbrk " even after head-reduction" else mt ()) ++
480
let intros_until_gen red h g =
481
tclDO (depth_of_quantified_hypothesis red h g) intro g
483
let intros_until_id id = intros_until_gen true (NamedHyp id)
484
let intros_until_n_gen red n = intros_until_gen red (AnonHyp n)
486
let intros_until = intros_until_gen true
487
let intros_until_n = intros_until_n_gen true
488
let intros_until_n_wored = intros_until_n_gen false
490
let try_intros_until tac = function
491
| NamedHyp id -> tclTHEN (tclTRY (intros_until_id id)) (tac id)
492
| AnonHyp n -> tclTHEN (intros_until_n n) (onLastHyp tac)
494
let rec intros_move = function
496
| (hyp,destopt) :: rest ->
497
tclTHEN (intro_gen dloc (IntroMustBe hyp) destopt false)
500
let dependent_in_decl a (_,c,t) =
502
| None -> dependent a t
503
| Some body -> dependent a body || dependent a t
505
(* Apply a tactic on a quantified hypothesis, an hypothesis in context
506
or a term with bindings *)
508
let onInductionArg tac = function
509
| ElimOnConstr (c,lbindc as cbl) ->
510
if isVar c & lbindc = NoBindings then
511
tclTHEN (tclTRY (intros_until_id (destVar c))) (tac cbl)
515
tclTHEN (intros_until_n n) (tclLAST_HYP (fun c -> tac (c,NoBindings)))
516
| ElimOnIdent (_,id) ->
517
(*Identifier apart because id can be quantified in goal and not typable*)
518
tclTHEN (tclTRY (intros_until_id id)) (tac (mkVar id,NoBindings))
520
(**************************)
521
(* Refinement tactics *)
522
(**************************)
524
let apply_type hdcty argl gl =
525
refine (applist (mkCast (Evarutil.mk_new_meta(),DEFAULTcast, hdcty),argl)) gl
527
let apply_term hdc argl gl =
528
refine (applist (hdc,argl)) gl
530
let bring_hyps hyps =
531
if hyps = [] then Refiner.tclIDTAC
534
let newcl = List.fold_right mkNamedProd_or_LetIn hyps (pf_concl gl) in
535
let f = mkCast (Evarutil.mk_new_meta(),DEFAULTcast, newcl) in
536
refine_no_check (mkApp (f, instance_from_named_context hyps)) gl)
538
let resolve_classes gl =
539
let env = pf_env gl and evd = project gl in
540
if evd = Evd.empty then tclIDTAC gl
542
let evd' = Typeclasses.resolve_typeclasses env (Evd.create_evar_defs evd) in
543
(tclTHEN (tclEVARS (Evd.evars_of evd')) tclNORMEVAR) gl
545
(**************************)
547
(**************************)
550
match kind_of_term (hnf_type_of gl c) with
552
let id=next_name_away_with_default "H" Anonymous (pf_ids_of_hyps gl) in
553
let t = mkProd (Anonymous, c, pf_concl gl) in
555
(internal_cut_rev id c)
556
(tclTHEN (apply_type t [mkVar id]) (thin [id]))
558
| _ -> error "Not a proposition or a type."
560
let cut_intro t = tclTHENFIRST (cut t) intro
562
(* cut_replacing �choue si l'hypoth�se � remplacer appara�t dans le
563
but, ou dans une autre hypoth�se *)
564
let cut_replacing id t tac =
565
tclTHENLAST (internal_cut_rev_replace id t)
566
(tac (refine_no_check (mkVar id)))
568
let cut_in_parallel l =
569
let rec prec = function
571
| h::t -> tclTHENFIRST (cut h) (prec t)
575
let error_uninstantiated_metas t clenv =
576
let na = meta_name clenv.evd (List.hd (Metaset.elements (metavars_of t))) in
577
let id = match na with Name id -> id | _ -> anomaly "unnamed dependent meta"
578
in errorlabstrm "" (str "Cannot find an instance for " ++ pr_id id ++ str".")
580
let clenv_refine_in with_evars ?(with_classes=true) id clenv gl =
581
let clenv = clenv_pose_dependent_evars with_evars clenv in
584
{ clenv with evd = Typeclasses.resolve_typeclasses ~fail:(not with_evars) clenv.env clenv.evd }
587
let new_hyp_typ = clenv_type clenv in
588
if not with_evars & occur_meta new_hyp_typ then
589
error_uninstantiated_metas new_hyp_typ clenv;
590
let new_hyp_prf = clenv_value clenv in
592
(tclEVARS (evars_of clenv.evd))
593
(cut_replacing id new_hyp_typ
594
(fun x gl -> refine_no_check new_hyp_prf gl)) gl
597
(********************************************)
598
(* Elimination tactics *)
599
(********************************************)
601
let last_arg c = match kind_of_term c with
604
| _ -> anomaly "last_arg"
607
modulo_conv_on_closed_terms = Some full_transparent_state;
608
use_metas_eagerly = true;
609
modulo_delta = empty_transparent_state;
612
let elimination_clause_scheme with_evars allow_K elimclause indclause gl =
614
(match kind_of_term (last_arg elimclause.templval.rebus) with
616
| _ -> errorlabstrm "elimination_clause"
617
(str "The type of elimination clause is not well-formed."))
619
let elimclause' = clenv_fchain indmv elimclause indclause in
620
res_pf elimclause' ~with_evars:with_evars ~allow_K:allow_K ~flags:elim_flags
623
(* cast added otherwise tactics Case (n1,n2) generates (?f x y) and
626
let type_clenv_binding wc (c,t) lbind =
627
clenv_type (make_clenv_binding wc (c,t) lbind)
630
* Elimination tactic with bindings and using an arbitrary
631
* elimination constant called elimc. This constant should end
632
* with a clause (x:I)(P .. ), where P is a bound variable.
633
* The term c is of type t, which is a product ending with a type
634
* matching I, lbindc are the expected terms for c arguments
637
let general_elim_clause elimtac (c,lbindc) (elimc,lbindelimc) gl =
638
let ct = pf_type_of gl c in
639
let t = try snd (pf_reduce_to_quantified_ind gl ct) with UserError _ -> ct in
640
let indclause = make_clenv_binding gl (c,t) lbindc in
641
let elimt = pf_type_of gl elimc in
642
let elimclause = make_clenv_binding gl (elimc,elimt) lbindelimc in
643
elimtac elimclause indclause gl
645
let general_elim with_evars c e ?(allow_K=true) =
646
general_elim_clause (elimination_clause_scheme with_evars allow_K) c e
648
(* Elimination tactic with bindings but using the default elimination
649
* constant associated with the type. *)
651
let find_eliminator c gl =
652
let (ind,t) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
653
lookup_eliminator ind (elimination_sort_of_goal gl)
655
let default_elim with_evars (c,_ as cx) gl =
656
general_elim with_evars cx (find_eliminator c gl,NoBindings) gl
658
let elim_in_context with_evars c = function
659
| Some elim -> general_elim with_evars c elim ~allow_K:true
660
| None -> default_elim with_evars c
662
let elim with_evars (c,lbindc as cx) elim =
663
match kind_of_term c with
664
| Var id when lbindc = NoBindings ->
665
tclTHEN (tclTRY (intros_until_id id))
666
(elim_in_context with_evars cx elim)
667
| _ -> elim_in_context with_evars cx elim
669
(* The simplest elimination tactic, with no substitutions at all. *)
671
let simplest_elim c = default_elim false (c,NoBindings)
673
(* Elimination in hypothesis *)
674
(* Typically, elimclause := (eq_ind ?x ?P ?H ?y ?Heq : ?P ?y)
675
indclause : forall ..., hyps -> a=b (to take place of ?Heq)
676
id : phi(a) (to take place of ?H)
677
and the result is to overwrite id with the proof of phi(b)
679
but this generalizes to any elimination scheme with one constructor
680
(e.g. it could replace id:A->B->C by id:C, knowing A/\B)
683
let clenv_fchain_in id elim_flags mv elimclause hypclause =
684
try clenv_fchain ~allow_K:false ~flags:elim_flags mv elimclause hypclause
685
with PretypeError (env,NoOccurrenceFound (op,_)) ->
686
(* Set the hypothesis name in the message *)
687
raise (PretypeError (env,NoOccurrenceFound (op,Some id)))
689
let elimination_in_clause_scheme with_evars id elimclause indclause gl =
691
match clenv_independent elimclause with
693
| _ -> errorlabstrm "elimination_clause"
694
(str "The type of elimination clause is not well-formed.") in
695
let elimclause' = clenv_fchain indmv elimclause indclause in
696
let hyp = mkVar id in
697
let hyp_typ = pf_type_of gl hyp in
698
let hypclause = mk_clenv_from_n gl (Some 0) (hyp, hyp_typ) in
700
clenv_fchain_in id elim_flags hypmv elimclause' hypclause in
701
let new_hyp_typ = clenv_type elimclause'' in
702
if eq_constr hyp_typ new_hyp_typ then
703
errorlabstrm "general_rewrite_in"
704
(str "Nothing to rewrite in " ++ pr_id id ++ str".");
705
clenv_refine_in with_evars id elimclause'' gl
707
let general_elim_in with_evars id =
708
general_elim_clause (elimination_in_clause_scheme with_evars id)
710
(* Case analysis tactics *)
712
let general_case_analysis_in_context with_evars (c,lbindc) gl =
713
let (mind,_) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
714
let sort = elimination_sort_of_goal gl in
716
if occur_term c (pf_concl gl) then make_case_dep else make_case_gen in
717
let elim = pf_apply case gl mind sort in
718
general_elim with_evars (c,lbindc) (elim,NoBindings) gl
720
let general_case_analysis with_evars (c,lbindc as cx) =
721
match kind_of_term c with
722
| Var id when lbindc = NoBindings ->
723
tclTHEN (tclTRY (intros_until_id id))
724
(general_case_analysis_in_context with_evars cx)
726
general_case_analysis_in_context with_evars cx
728
let simplest_case c = general_case_analysis false (c,NoBindings)
730
(* Apply a tactic below the products of the conclusion of a lemma *)
732
let descend_in_conjunctions with_evars tac exit c gl =
734
let (mind,t) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
735
match match_with_record (snd (decompose_prod t)) with
737
let n = (mis_constr_nargs mind).(0) in
738
let sort = elimination_sort_of_goal gl in
739
let elim = pf_apply make_case_gen gl mind sort in
741
(general_elim with_evars (c,NoBindings) (elim,NoBindings))
744
tclLAST_NHYPS n (fun l ->
746
(List.map (fun id -> tclTHEN (tac (mkVar id)) (thin l)) l))])
750
with RefinerError _|UserError _|Exit -> exit ()
752
(****************************************************)
753
(* Resolution tactics *)
754
(****************************************************)
756
(* Resolution with missing arguments *)
758
let check_evars sigma evm gl =
759
let origsigma = gl.sigma in
761
Evd.fold (fun ev evi acc ->
762
if not (Evd.mem origsigma ev) && not (Evd.is_defined sigma ev)
763
then Evd.add acc ev evi else acc)
766
if rest <> Evd.empty then
767
errorlabstrm "apply" (str"Uninstantiated existential variables: " ++
768
fnl () ++ pr_evar_map rest)
770
let general_apply with_delta with_destruct with_evars (c,lbind) gl0 =
772
if with_delta then default_unify_flags else default_no_delta_unify_flags in
773
(* The actual type of the theorem. It will be matched against the
774
goal. If this fails, then the head constant will be unfolded step by
776
let concl_nprod = nb_prod (pf_concl gl0) in
778
let rec try_main_apply c gl =
779
let thm_ty0 = nf_betaiota (project gl) (pf_type_of gl c) in
780
let try_apply thm_ty nprod =
781
let n = nb_prod thm_ty - nprod in
782
if n<0 then error "Applied theorem has not enough premisses.";
783
let clause = make_clenv_binding_apply gl (Some n) (c,thm_ty) lbind in
784
let res = Clenvtac.res_pf clause ~with_evars:with_evars ~flags:flags gl in
785
if not with_evars then check_evars (fst res).sigma evm gl0;
788
try try_apply thm_ty0 concl_nprod
789
with PretypeError _|RefinerError _|UserError _|Failure _ as exn ->
790
let rec try_red_apply thm_ty =
792
(* Try to head-reduce the conclusion of the theorem *)
793
let red_thm = try_red_product (pf_env gl) (project gl) thm_ty in
794
try try_apply red_thm concl_nprod
795
with PretypeError _|RefinerError _|UserError _|Failure _ ->
796
try_red_apply red_thm
797
with Redelimination ->
798
(* Last chance: if the head is a variable, apply may try
799
second order unification *)
800
try if concl_nprod <> 0 then try_apply thm_ty 0 else raise Exit
801
with PretypeError _|RefinerError _|UserError _|Failure _|Exit ->
802
if with_destruct then
803
descend_in_conjunctions with_evars
804
try_main_apply (fun _ -> raise exn) c gl
807
in try_red_apply thm_ty0
809
if evm = Evd.empty then try_main_apply c gl0
811
tclTHEN (tclEVARS (Evd.merge gl0.sigma evm)) (try_main_apply c) gl0
813
let rec apply_with_ebindings_gen b e = function
817
general_apply b b e cb
819
tclTHENLAST (general_apply b b e cb) (apply_with_ebindings_gen b e cbl)
821
let apply_with_ebindings cb = apply_with_ebindings_gen false false [cb]
822
let eapply_with_ebindings cb = apply_with_ebindings_gen false true [cb]
824
let apply_with_bindings (c,bl) =
825
apply_with_ebindings (inj_open c,inj_ebindings bl)
827
let eapply_with_bindings (c,bl) =
828
apply_with_ebindings_gen false true [inj_open c,inj_ebindings bl]
831
apply_with_ebindings (inj_open c,NoBindings)
833
let apply_list = function
834
| c::l -> apply_with_bindings (c,ImplicitBindings l)
837
(* Resolution with no reduction on the type (used ?) *)
839
let apply_without_reduce c gl =
840
let clause = mk_clenv_type_of gl c in
843
(* [apply_in hyp c] replaces
845
hyp : forall y1, ti -> t hyp : rho(u)
846
======================== with ============ and the =======
849
assuming that [c] has type [forall x1..xn -> t' -> u] for some [t]
850
unifiable with [t'] with unifier [rho]
853
let find_matching_clause unifier clause =
854
let rec find clause =
856
with exn when catchable_exception exn ->
857
try find (clenv_push_prod clause)
858
with NotExtensibleClause -> failwith "Cannot apply"
861
let progress_with_clause flags innerclause clause =
862
let ordered_metas = List.rev (clenv_independent clause) in
863
if ordered_metas = [] then error "Statement without assumptions.";
865
find_matching_clause (clenv_fchain mv ~flags clause) innerclause in
866
try list_try_find f ordered_metas
867
with Failure _ -> error "Unable to unify."
869
let apply_in_once_main flags innerclause (d,lbind) gl =
870
let thm = nf_betaiota gl.sigma (pf_type_of gl d) in
872
try progress_with_clause flags innerclause clause
874
try aux (clenv_push_prod clause)
875
with NotExtensibleClause -> raise err in
876
aux (make_clenv_binding gl (d,thm) lbind)
878
let apply_in_once with_delta with_destruct with_evars id ((sigma,d),lbind) gl0 =
880
if with_delta then default_unify_flags else default_no_delta_unify_flags in
881
let t' = pf_get_hyp_typ gl0 id in
882
let innerclause = mk_clenv_from_n gl0 (Some 0) (mkVar id,t') in
885
let clause = apply_in_once_main flags innerclause (c,lbind) gl in
886
let res = clenv_refine_in with_evars id clause gl in
887
if not with_evars then check_evars (fst res).sigma sigma gl0;
889
with exn when with_destruct ->
890
descend_in_conjunctions true aux (fun _ -> raise exn) c gl
892
if sigma = Evd.empty then aux d gl0
894
tclTHEN (tclEVARS (Evd.merge gl0.sigma sigma)) (aux d) gl0
899
(* A useful resolution tactic which, if c:A->B, transforms |- C into
903
Gamma |- c : A -> B Gamma |- ?2 : A
904
----------------------------------------
905
Gamma |- B Gamma |- ?1 : B -> C
906
-----------------------------------------------------
911
match eval hnf in ty with
912
?A -> ?B => cut B; [ idtac | apply c ]
916
let cut_and_apply c gl =
917
let goal_constr = pf_concl gl in
918
match kind_of_term (pf_hnf_constr gl (pf_type_of gl c)) with
919
| Prod (_,c1,c2) when not (dependent (mkRel 1) c2) ->
921
(apply_type (mkProd (Anonymous,c2,goal_constr)) [mkMeta(new_meta())])
922
(apply_term c [mkMeta (new_meta())]) gl
923
| _ -> error "lapply needs a non-dependent product."
925
(********************************************************************)
927
(********************************************************************)
929
let exact_check c gl =
930
let concl = (pf_concl gl) in
931
let ct = pf_type_of gl c in
932
if pf_conv_x_leq gl ct concl then
935
error "Not an exact proof."
937
let exact_no_check = refine_no_check
939
let vm_cast_no_check c gl =
940
let concl = pf_concl gl in
941
refine_no_check (Term.mkCast(c,Term.VMcast,concl)) gl
944
let exact_proof c gl =
945
(* on experimente la synthese d'ise dans exact *)
946
let c = Constrintern.interp_casted_constr (project gl) (pf_env gl) c (pf_concl gl)
947
in refine_no_check c gl
949
let (assumption : tactic) = fun gl ->
950
let concl = pf_concl gl in
951
let hyps = pf_hyps gl in
952
let rec arec only_eq = function
954
if only_eq then arec false hyps else error "No such assumption."
956
if (only_eq & eq_constr t concl)
957
or (not only_eq & pf_conv_x_leq gl t concl)
958
then refine_no_check (mkVar id) gl
959
else arec only_eq rest
963
(*****************************************************************)
964
(* Modification of a local context *)
965
(*****************************************************************)
967
(* This tactic enables the user to remove hypotheses from the signature.
968
* Some care is taken to prevent him from removing variables that are
969
* subsequently used in other hypotheses or in the conclusion of the
972
let clear ids = (* avant seul dyn_clear n'echouait pas en [] *)
973
if ids=[] then tclIDTAC else thin ids
975
let clear_body = thin_body
977
let clear_wildcards ids =
978
tclMAP (fun (loc,id) gl ->
979
try with_check (Tacmach.thin_no_check [id]) gl
980
with ClearDependencyError (id,err) ->
981
(* Intercept standard [thin] error message *)
982
Stdpp.raise_with_loc loc
983
(error_clear_dependency (pf_env gl) (id_of_string "_") err))
986
(* Takes a list of booleans, and introduces all the variables
987
* quantified in the goal which are associated with a value
988
* true in the boolean list. *)
990
let rec intros_clearing = function
992
| (false::tl) -> tclTHEN intro (intros_clearing tl)
995
[ intro; onLastHyp (fun id -> clear [id]); intros_clearing tl]
997
(* Modifying/Adding an hypothesis *)
999
let specialize mopt (c,lbind) g =
1001
if lbind = NoBindings then None, c
1003
let clause = make_clenv_binding g (c,pf_type_of g c) lbind in
1004
let clause = clenv_unify_meta_types clause in
1006
whd_stack (evars_of clause.evd) (clenv_value clause) in
1007
let nargs = List.length tstack in
1008
let tstack = match mopt with
1010
if m < nargs then list_firstn m tstack else tstack
1012
let rec chk = function
1014
| t::l -> if occur_meta t then [] else t :: chk l
1017
let term = applist(thd,tstack) in
1018
if occur_meta term then
1019
errorlabstrm "" (str "Cannot infer an instance for " ++
1020
pr_name (meta_name clause.evd (List.hd (collect_metas term))) ++
1022
Some (evars_of clause.evd), term
1025
(match evars with Some e -> tclEVARS e | _ -> tclIDTAC)
1026
(match kind_of_term (fst(decompose_app (snd(decompose_lam_assum c)))) with
1027
| Var id when List.mem id (pf_ids_of_hyps g) ->
1029
(fun g -> internal_cut_replace id (pf_type_of g term) g)
1030
(exact_no_check term)
1032
(fun g -> cut (pf_type_of g term) g)
1033
(exact_no_check term))
1036
(* Keeping only a few hypotheses *)
1039
let env = Global.env() in
1040
let ccl = pf_concl gl in
1042
fold_named_context_reverse (fun (clear,keep) (hyp,_,_ as decl) ->
1043
if List.mem hyp hyps
1044
or List.exists (occur_var_in_decl env hyp) keep
1045
or occur_var env hyp ccl
1046
then (clear,decl::keep)
1047
else (hyp::clear,keep))
1048
~init:([],[]) (pf_env gl)
1051
(************************)
1052
(* Introduction tactics *)
1053
(************************)
1055
let check_number_of_constructors expctdnumopt i nconstr =
1056
if i=0 then error "The constructors are numbered starting from 1.";
1057
begin match expctdnumopt with
1058
| Some n when n <> nconstr ->
1059
error ("Not an inductive goal with "^
1060
string_of_int n^plural n " constructor"^".")
1063
if i > nconstr then error "Not enough constructors."
1065
let constructor_tac with_evars expctdnumopt i lbind gl =
1066
let cl = pf_concl gl in
1067
let (mind,redcl) = pf_reduce_to_quantified_ind gl cl in
1069
Array.length (snd (Global.lookup_inductive mind)).mind_consnames in
1070
check_number_of_constructors expctdnumopt i nconstr;
1071
let cons = mkConstruct (ith_constructor_of_inductive mind i) in
1072
let apply_tac = general_apply true false with_evars (inj_open cons,lbind) in
1074
[convert_concl_no_check redcl DEFAULTcast; intros; apply_tac]) gl
1076
let one_constructor i = constructor_tac false None i
1078
(* Try to apply the constructor of the inductive definition followed by
1079
a tactic t given as an argument.
1080
Should be generalize in Constructor (Fun c : I -> tactic)
1083
let any_constructor with_evars tacopt gl =
1084
let t = match tacopt with None -> tclIDTAC | Some t -> t in
1085
let mind = fst (pf_reduce_to_quantified_ind gl (pf_concl gl)) in
1087
Array.length (snd (Global.lookup_inductive mind)).mind_consnames in
1088
if nconstr = 0 then error "The type has no constructors.";
1091
(fun i -> tclTHEN (constructor_tac with_evars None i NoBindings) t)
1092
(interval 1 nconstr)) gl
1094
let left_with_ebindings with_evars = constructor_tac with_evars (Some 2) 1
1095
let right_with_ebindings with_evars = constructor_tac with_evars (Some 2) 2
1096
let split_with_ebindings with_evars = constructor_tac with_evars (Some 1) 1
1098
let left l = left_with_ebindings false (inj_ebindings l)
1099
let simplest_left = left NoBindings
1101
let right l = right_with_ebindings false (inj_ebindings l)
1102
let simplest_right = right NoBindings
1104
let split l = split_with_ebindings false (inj_ebindings l)
1105
let simplest_split = split NoBindings
1108
(*****************************)
1109
(* Decomposing introductions *)
1110
(*****************************)
1112
let forward_general_multi_rewrite =
1113
ref (fun _ -> failwith "general_multi_rewrite undefined")
1115
let register_general_multi_rewrite f =
1116
forward_general_multi_rewrite := f
1118
let error_unexpected_extra_pattern loc nb pat =
1119
let s1,s2,s3 = match pat with
1120
| IntroIdentifier _ -> "name", (plural nb " introduction pattern"), "no"
1121
| _ -> "introduction pattern", "", "none" in
1122
user_err_loc (loc,"",str "Unexpected " ++ str s1 ++ str " (" ++
1123
(if nb = 0 then (str s3 ++ str s2) else
1124
(str "at most " ++ int nb ++ str s2)) ++ spc () ++
1125
str (if nb = 1 then "was" else "were") ++
1126
strbrk " expected in the branch).")
1128
let intro_or_and_pattern loc b ll l' tac id gl =
1130
let ind,_ = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
1131
let nv = mis_constr_nargs ind in
1132
let bracketed = b or not (l'=[]) in
1133
let rec adjust_names_length nb n = function
1134
| [] when n = 0 or not bracketed -> []
1135
| [] -> (dloc,IntroAnonymous) :: adjust_names_length nb (n-1) []
1136
| (loc',pat) :: _ as l when n = 0 ->
1137
if bracketed then error_unexpected_extra_pattern loc' nb pat;
1139
| ip :: l -> ip :: adjust_names_length nb (n-1) l in
1140
let ll = fix_empty_or_and_pattern (Array.length nv) ll in
1141
check_or_and_pattern_size loc ll (Array.length nv);
1143
(tclTHEN (simplest_case c) (clear [id]))
1144
(array_map2 (fun n l -> tac ((adjust_names_length n n l)@l'))
1145
nv (Array.of_list ll))
1148
let rewrite_hyp l2r id gl =
1150
!forward_general_multi_rewrite l2r false (inj_open (mkVar id),NoBindings) in
1151
let clear_var_and_eq c =
1152
tclTRY (tclTHEN (clear [id]) (tclTRY (clear [destVar c]))) in
1153
let t = pf_whd_betadeltaiota gl (pf_type_of gl (mkVar id)) in
1154
(* TODO: detect setoid equality? better detect the different equalities *)
1155
match match_with_equality_type t with
1156
| Some (hdcncl,[_;lhs;rhs]) ->
1157
if l2r & isVar lhs & not (occur_var (pf_env gl) (destVar lhs) rhs) then
1158
tclTHEN (rew_on l2r allClauses) (clear_var_and_eq lhs) gl
1159
else if not l2r & isVar rhs & not (occur_var (pf_env gl) (destVar rhs) lhs) then
1160
tclTHEN (rew_on l2r allClauses) (clear_var_and_eq rhs) gl
1162
tclTHEN (rew_on l2r onConcl) (tclTRY (clear [id])) gl
1163
| Some (hdcncl,[c]) ->
1164
let l2r = not l2r in (* equality of the form eq_true *)
1166
tclTHEN (rew_on l2r allClauses) (clear_var_and_eq c) gl
1168
tclTHEN (rew_on l2r onConcl) (tclTRY (clear [id])) gl
1170
error "Cannot find a known equation."
1172
let rec explicit_intro_names = function
1173
| (_, IntroIdentifier id) :: l ->
1174
id :: explicit_intro_names l
1175
| (_, (IntroWildcard | IntroAnonymous | IntroFresh _ | IntroRewrite _)) :: l ->
1176
explicit_intro_names l
1177
| (_, IntroOrAndPattern ll) :: l' ->
1178
List.flatten (List.map (fun l -> explicit_intro_names (l@l')) ll)
1182
(* We delay thinning until the completion of the whole intros tactic
1183
to ensure that dependent hypotheses are cleared in the right
1184
dependency order (see bug #1000); we use fresh names, not used in
1185
the tactic, for the hyps to clear *)
1186
let rec intros_patterns b avoid thin destopt = function
1187
| (loc, IntroWildcard) :: l ->
1189
(intro_gen loc (IntroAvoid(avoid@explicit_intro_names l)) no_move true)
1190
(onLastHyp (fun id ->
1192
(tclTHEN (clear [id]) (intros_patterns b avoid thin destopt l))
1193
(intros_patterns b avoid ((loc,id)::thin) destopt l)))
1194
| (loc, IntroIdentifier id) :: l ->
1196
(intro_gen loc (IntroMustBe id) destopt true)
1197
(intros_patterns b avoid thin destopt l)
1198
| (loc, IntroAnonymous) :: l ->
1200
(intro_gen loc (IntroAvoid (avoid@explicit_intro_names l))
1202
(intros_patterns b avoid thin destopt l)
1203
| (loc, IntroFresh id) :: l ->
1205
(intro_gen loc (IntroBasedOn (id, avoid@explicit_intro_names l))
1207
(intros_patterns b avoid thin destopt l)
1208
| (loc, IntroOrAndPattern ll) :: l' ->
1212
(intro_or_and_pattern loc b ll l'
1213
(intros_patterns b avoid thin destopt)))
1214
| (loc, IntroRewrite l2r) :: l ->
1216
(intro_gen loc (IntroAvoid(avoid@explicit_intro_names l)) no_move true)
1217
(onLastHyp (fun id ->
1219
(rewrite_hyp l2r id)
1220
(intros_patterns b avoid thin destopt l)))
1221
| [] -> clear_wildcards thin
1223
let intros_pattern = intros_patterns false [] []
1225
let intro_pattern destopt pat = intros_patterns false [] [] destopt [dloc,pat]
1227
let intro_patterns = function
1228
| [] -> tclREPEAT intro
1229
| l -> intros_pattern no_move l
1231
(**************************)
1232
(* Other cut tactics *)
1233
(**************************)
1235
let make_id s = fresh_id [] (default_id_of_sort s)
1237
let prepare_intros s ipat gl = match ipat with
1238
| None -> make_id s gl, tclIDTAC
1239
| Some (loc,ipat) -> match ipat with
1240
| IntroIdentifier id -> id, tclIDTAC
1241
| IntroAnonymous -> make_id s gl, tclIDTAC
1242
| IntroFresh id -> fresh_id [] id gl, tclIDTAC
1243
| IntroWildcard -> let id = make_id s gl in id, clear_wildcards [dloc,id]
1244
| IntroRewrite l2r ->
1245
let id = make_id s gl in
1246
id, !forward_general_multi_rewrite l2r false (inj_open (mkVar id),NoBindings) allClauses
1247
| IntroOrAndPattern ll -> make_id s gl,
1249
(intro_or_and_pattern loc true ll []
1250
(intros_patterns true [] [] no_move))
1252
let ipat_of_name = function
1254
| Name id -> Some (dloc, IntroIdentifier id)
1256
let allow_replace c gl = function (* A rather arbitrary condition... *)
1257
| Some (_, IntroIdentifier id) ->
1258
fst (decompose_app (snd (decompose_lam_assum c))) = mkVar id
1262
let assert_as first ipat c gl =
1263
match kind_of_term (hnf_type_of gl c) with
1265
let id,tac = prepare_intros s ipat gl in
1266
let repl = allow_replace c gl ipat in
1268
((if first then internal_cut_gen else internal_cut_rev_gen) repl id c)
1269
(if first then [tclIDTAC; tac] else [tac; tclIDTAC]) gl
1270
| _ -> error "Not a proposition or a type."
1272
let assert_tac na = assert_as true (ipat_of_name na)
1276
let as_tac id ipat = match ipat with
1277
| Some (loc,IntroRewrite l2r) ->
1278
!forward_general_multi_rewrite l2r false (inj_open (mkVar id),NoBindings) allClauses
1279
| Some (loc,IntroOrAndPattern ll) ->
1280
intro_or_and_pattern loc true ll [] (intros_patterns true [] [] no_move)
1283
(IntroIdentifier _ | IntroAnonymous | IntroFresh _ | IntroWildcard)) ->
1284
user_err_loc (loc,"", str "Disjunctive/conjunctive pattern expected")
1287
let general_apply_in with_delta with_destruct with_evars id lemmas ipat gl =
1289
(tclMAP (apply_in_once with_delta with_destruct with_evars id) lemmas)
1293
let apply_in simple with_evars = general_apply_in simple simple with_evars
1295
(**************************)
1296
(* Generalize tactics *)
1297
(**************************)
1299
let generalized_name c t ids cl = function
1301
if List.mem id ids then
1302
errorlabstrm "" (pr_id id ++ str " is already used");
1305
match kind_of_term c with
1307
(* Keep the name even if not occurring: may be used by intros later *)
1310
if noccurn 1 cl then Anonymous else
1311
(* On ne s'etait pas casse la tete : on avait pris pour nom de
1312
variable la premiere lettre du type, meme si "c" avait ete une
1313
constante dont on aurait pu prendre directement le nom *)
1314
named_hd (Global.env()) t Anonymous
1316
let generalize_goal gl i ((occs,c),na) cl =
1317
let t = pf_type_of gl c in
1318
let decls,cl = decompose_prod_n_assum i cl in
1319
let dummy_prod = it_mkProd_or_LetIn mkProp decls in
1320
let newdecls,_ = decompose_prod_n_assum i (subst_term c dummy_prod) in
1321
let cl' = subst_term_occ occs c (it_mkProd_or_LetIn cl newdecls) in
1322
let na = generalized_name c t (pf_ids_of_hyps gl) cl' na in
1325
let generalize_dep c gl =
1326
let env = pf_env gl in
1327
let sign = pf_hyps gl in
1328
let init_ids = ids_of_named_context (Global.named_context()) in
1329
let rec seek d toquant =
1330
if List.exists (fun (id,_,_) -> occur_var_in_decl env id d) toquant
1331
or dependent_in_decl c d then
1335
let to_quantify = Sign.fold_named_context seek sign ~init:[] in
1336
let to_quantify_rev = List.rev to_quantify in
1337
let qhyps = List.map (fun (id,_,_) -> id) to_quantify_rev in
1338
let tothin = List.filter (fun id -> not (List.mem id init_ids)) qhyps in
1340
match kind_of_term c with
1341
| Var id when mem_named_context id sign & not (List.mem id init_ids)
1345
let cl' = it_mkNamedProd_or_LetIn (pf_concl gl) to_quantify in
1346
let cl'' = generalize_goal gl 0 ((all_occurrences,c),Anonymous) cl' in
1347
let args = Array.to_list (instance_from_named_context to_quantify_rev) in
1349
(apply_type cl'' (c::args))
1350
(thin (List.rev tothin'))
1353
let generalize_gen lconstr gl =
1355
list_fold_right_i (generalize_goal gl) 0 lconstr (pf_concl gl) in
1356
apply_type newcl (List.map (fun ((_,c),_) -> c) lconstr) gl
1359
generalize_gen (List.map (fun c -> ((all_occurrences,c),Anonymous)) l)
1361
let revert hyps gl =
1362
tclTHEN (generalize (List.map mkVar hyps)) (clear hyps) gl
1364
(* Faudra-t-il une version avec plusieurs args de generalize_dep ?
1365
Cela peut-�tre troublant de faire "Generalize Dependent H n" dans
1366
"n:nat; H:n=n |- P(n)" et d'�chouer parce que H a disparu apr�s la
1367
g�n�ralisation d�pendante par n.
1369
let quantify lconstr =
1371
(fun com tac -> tclTHEN tac (tactic_com generalize_dep c))
1376
(* A dependent cut rule � la sequent calculus
1377
------------------------------------------
1378
Sera simplifiable le jour o� il y aura un let in primitif dans constr
1380
[letin_tac b na c (occ_hyp,occ_ccl) gl] transforms
1381
[...x1:T1(c),...,x2:T2(c),... |- G(c)] into
1382
[...x:T;Heqx:(x=c);x1:T1(x),...,x2:T2(x),... |- G(x)] if [b] is false or
1383
[...x:=c:T;x1:T1(x),...,x2:T2(x),... |- G(x)] if [b] is true
1385
[occ_hyp,occ_ccl] tells which occurrences of [c] have to be substituted;
1386
if [occ_hyp = []] and [occ_ccl = None] then [c] is substituted
1387
wherever it occurs, otherwise [c] is substituted only in hyps
1388
present in [occ_hyps] at the specified occurrences (everywhere if
1389
the list of occurrences is empty), and in the goal at the specified
1390
occurrences if [occ_goal] is not [None];
1392
if name = Anonymous, the name is build from the first letter of the type;
1394
The tactic first quantify the goal over x1, x2,... then substitute then
1395
re-intro x1, x2,... at their initial place ([marks] is internally
1396
used to remember the place of x1, x2, ...: it is the list of hypotheses on
1397
the left of each x1, ...).
1400
let out_arg = function
1401
| ArgVar _ -> anomaly "Unevaluated or_var variable"
1404
let occurrences_of_hyp id cls =
1405
let rec hyp_occ = function
1407
| (((b,occs),id'),hl)::_ when id=id' -> Some ((b,List.map out_arg occs),hl)
1408
| _::l -> hyp_occ l in
1409
match cls.onhyps with
1410
None -> Some (all_occurrences,InHyp)
1411
| Some l -> hyp_occ l
1413
let occurrences_of_goal cls =
1414
if cls.concl_occs = no_occurrences_expr then None
1415
else Some (on_snd (List.map out_arg) cls.concl_occs)
1417
let in_every_hyp cls = (cls.onhyps=None)
1420
(* Implementation with generalisation then re-intro: introduces noise *)
1423
let letin_abstract id c occs gl =
1424
let env = pf_env gl in
1425
let compute_dependency _ (hyp,_,_ as d) ctxt =
1428
match occurrences_of_hyp hyp occs with
1429
| None -> raise Not_found
1431
let newdecl = subst_term_occ_decl occ c d in
1432
if occ = [] & d = newdecl then
1433
if not (in_every_hyp occs)
1434
then raise (RefinerError (DoesNotOccurIn (c,hyp)))
1435
else raise Not_found
1437
(subst1_named_decl (mkVar id) newdecl, true)
1440
(fun ((id,_,_),dep) -> dep && occur_var_in_decl env id d) ctxt)
1443
let ctxt' = fold_named_context compute_dependency env ~init:[] in
1444
let compute_marks ((depdecls,marks as accu),lhyp) ((hyp,_,_) as d,b) =
1445
if b then ((d::depdecls,(hyp,lhyp)::marks), lhyp)
1446
else (accu, Some hyp) in
1447
let (depdecls,marks),_ = List.fold_left compute_marks (([],[]),None) ctxt' in
1448
let ccl = match occurrences_of_goal occs with
1449
| None -> pf_concl gl
1450
| Some occ -> subst1 (mkVar id) (subst_term_occ occ c (pf_concl gl))
1452
(depdecls,marks,ccl)
1454
let letin_tac with_eq name c occs gl =
1455
let x = id_of_name_using_hdchar (Global.env()) (pf_type_of gl c) name in
1457
if name = Anonymous then fresh_id [] x gl else
1458
if not (mem_named_context x (pf_hyps gl)) then x else
1459
error ("The variable "^(string_of_id x)^" is already declared") in
1460
let (depdecls,marks,ccl)= letin_abstract id c occs gl in
1461
let t = pf_type_of gl c in
1462
let tmpcl = List.fold_right mkNamedProd_or_LetIn depdecls ccl in
1463
let args = Array.to_list (instance_from_named_context depdecls) in
1464
let newcl = mkNamedLetIn id c t tmpcl in
1465
let lastlhyp = if marks=[] then None else snd (List.hd marks) in
1467
[ apply_type newcl args;
1468
thin (List.map (fun (id,_,_) -> id) depdecls);
1469
intro_gen (IntroMustBe id) lastlhyp false;
1470
if with_eq then tclIDTAC else thin_body [id];
1471
intros_move marks ] gl
1474
(* Implementation without generalisation: abbrev will be lost in hyps in *)
1475
(* in the extracted proof *)
1477
let letin_abstract id c (occs,check_occs) gl =
1478
let env = pf_env gl in
1479
let compute_dependency _ (hyp,_,_ as d) depdecls =
1480
match occurrences_of_hyp hyp occs with
1483
let newdecl = subst_term_occ_decl occ c d in
1484
if occ = (all_occurrences,InHyp) & d = newdecl then
1485
if check_occs & not (in_every_hyp occs)
1486
then raise (RefinerError (DoesNotOccurIn (c,hyp)))
1489
(subst1_named_decl (mkVar id) newdecl)::depdecls in
1490
let depdecls = fold_named_context compute_dependency env ~init:[] in
1491
let ccl = match occurrences_of_goal occs with
1492
| None -> pf_concl gl
1493
| Some occ -> subst1 (mkVar id) (subst_term_occ occ c (pf_concl gl)) in
1495
if depdecls = [] then no_move else MoveAfter(pi1(list_last depdecls)) in
1496
(depdecls,lastlhyp,ccl)
1498
let letin_tac_gen with_eq name c ty occs gl =
1500
let x = id_of_name_using_hdchar (Global.env()) (pf_type_of gl c) name in
1501
if name = Anonymous then fresh_id [] x gl else
1502
if not (mem_named_context x (pf_hyps gl)) then x else
1503
error ("The variable "^(string_of_id x)^" is already declared.") in
1504
let (depdecls,lastlhyp,ccl)= letin_abstract id c occs gl in
1505
let t = match ty with Some t -> t | None -> pf_type_of gl c in
1506
let newcl,eq_tac = match with_eq with
1507
| Some (lr,(loc,ido)) ->
1508
let heq = match ido with
1509
| IntroAnonymous -> fresh_id [id] (add_prefix "Heq" id) gl
1510
| IntroFresh heq_base -> fresh_id [id] heq_base gl
1511
| IntroIdentifier id -> id
1512
| _ -> error"Expect an introduction pattern naming one hypothesis." in
1513
let eqdata = build_coq_eq_data () in
1514
let args = if lr then [t;mkVar id;c] else [t;c;mkVar id]in
1515
let eq = applist (eqdata.eq,args) in
1516
let refl = applist (eqdata.refl, [t;mkVar id]) in
1517
mkNamedLetIn id c t (mkLetIn (Name heq, refl, eq, ccl)),
1519
(intro_gen loc (IntroMustBe heq) lastlhyp true)
1520
(thin_body [heq;id])
1522
mkNamedLetIn id c t ccl, tclIDTAC in
1524
[ convert_concl_no_check newcl DEFAULTcast;
1525
intro_gen dloc (IntroMustBe id) lastlhyp true;
1527
tclMAP convert_hyp_no_check depdecls ] gl
1529
let letin_tac with_eq name c ty occs =
1530
letin_tac_gen with_eq name c ty (occs,true)
1532
(* Tactics "pose proof" (usetac=None) and "assert" (otherwise) *)
1533
let forward usetac ipat c gl =
1536
let t = pf_type_of gl c in
1537
tclTHENFIRST (assert_as true ipat t) (exact_no_check c) gl
1539
tclTHENFIRST (assert_as true ipat c) tac gl
1541
let pose_proof na c = forward None (ipat_of_name na) c
1542
let assert_by na t tac = forward (Some tac) (ipat_of_name na) t
1544
(*****************************)
1546
(*****************************)
1548
(* The two following functions should already exist, but found nowhere *)
1549
(* Unfolds x by its definition everywhere *)
1550
let unfold_body x gl =
1551
let hyps = pf_hyps gl in
1553
match Sign.lookup_named x hyps with
1554
(_,Some xval,_) -> xval
1555
| _ -> errorlabstrm "unfold_body"
1556
(pr_id x ++ str" is not a defined hypothesis.") in
1557
let aft = afterHyp x gl in
1558
let hl = List.fold_right (fun (y,yval,_) cl -> (([],y),InHyp) :: cl) aft [] in
1559
let xvar = mkVar x in
1560
let rfun _ _ c = replace_term xvar xval c in
1562
[tclMAP (fun h -> reduct_in_hyp rfun h) hl;
1563
reduct_in_concl (rfun,DEFAULTcast)] gl
1565
(* Unfolds x by its definition everywhere and clear x. This may raise
1566
an error if x is not defined. *)
1567
let unfold_all x gl =
1568
let (_,xval,_) = pf_get_hyp gl x in
1569
(* If x has a body, simply replace x with body and clear x *)
1570
if xval <> None then tclTHEN (unfold_body x) (clear [x]) gl
1573
(*****************************)
1574
(* High-level induction *)
1575
(*****************************)
1578
* A "natural" induction tactic
1580
- [H0:T0, ..., Hi:Ti, hyp0:P->I(args), Hi+1:Ti+1, ..., Hn:Tn |-G] is the goal
1581
- [hyp0] is the induction hypothesis
1582
- we extract from [args] the variables which are not rigid parameters
1583
of the inductive type, this is [indvars] (other terms are forgotten);
1584
[indhyps] are the ones which actually are declared in context
1585
(done in [find_atomic_param_of_ind])
1586
- we look for all hyps depending of [hyp0] or one of [indvars]:
1587
this is [dephyps] of types [deptyps] respectively
1588
- [statuslist] tells for each hyps in [dephyps] after which other hyp
1589
fixed in the context they must be moved (when induction is done)
1590
- [hyp0succ] is the name of the hyp fixed in the context after which to
1591
move the subterms of [hyp0succ] in the i-th branch where it is supposed
1592
to be the i-th constructor of the inductive type.
1594
Strategy: (cf in [induction_from_context])
1595
- requantify and clear all [dephyps]
1596
- apply induction on [hyp0]
1597
- clear [indhyps] and [hyp0]
1598
- in the i-th subgoal, intro the arguments of the i-th constructor
1599
of the inductive type after [hyp0succ] (done in
1600
[induct_discharge]) let the induction hypotheses on top of the
1601
hyps because they may depend on variables between [hyp0] and the
1602
top. A counterpart is that the dep hyps programmed to be intro-ed
1603
on top must now be intro-ed after the induction hypotheses
1604
- move each of [dephyps] at the right place following the
1609
let check_unused_names names =
1610
if names <> [] & Flags.is_verbose () then
1612
(str"Unused introduction " ++ str (plural (List.length names) "pattern")
1613
++ str": " ++ prlist_with_sep spc pr_intro_pattern names)
1615
let rec first_name_buggy avoid gl (loc,pat) = match pat with
1616
| IntroOrAndPattern [] -> no_move
1617
| IntroOrAndPattern ([]::l) ->
1618
first_name_buggy avoid gl (loc,IntroOrAndPattern l)
1619
| IntroOrAndPattern ((p::_)::_) -> first_name_buggy avoid gl p
1620
| IntroWildcard -> no_move
1621
| IntroRewrite _ -> no_move
1622
| IntroIdentifier id -> MoveAfter id
1623
| IntroAnonymous | IntroFresh _ -> (* buggy *) no_move
1625
let consume_pattern avoid id gl = function
1626
| [] -> ((dloc, IntroIdentifier (fresh_id avoid id gl)), [])
1627
| (loc,IntroAnonymous)::names ->
1628
let avoid = avoid@explicit_intro_names names in
1629
((loc,IntroIdentifier (fresh_id avoid id gl)), names)
1630
| (loc,IntroFresh id')::names ->
1631
let avoid = avoid@explicit_intro_names names in
1632
((loc,IntroIdentifier (fresh_id avoid id' gl)), names)
1633
| pat::names -> (pat,names)
1635
let re_intro_dependent_hypotheses tophyp (lstatus,rstatus) =
1636
let newlstatus = (* if some IH has taken place at the top of hyps *)
1637
List.map (function (hyp,MoveToEnd true) -> (hyp,tophyp) | x -> x) lstatus
1640
(intros_move rstatus)
1641
(intros_move newlstatus)
1643
let update destopt tophyp = if destopt = no_move then tophyp else destopt
1645
type elim_arg_kind = RecArg | IndArg | OtherArg
1647
let induct_discharge statuslists destopt avoid' (avoid,ra) names gl =
1648
let avoid = avoid @ avoid' in
1649
let rec peel_tac ra names tophyp gl =
1651
| (RecArg,recvarname) ::
1652
(IndArg,hyprecname) :: ra' ->
1653
let recpat,names = match names with
1654
| [loc,IntroIdentifier id as pat] ->
1655
let id' = next_ident_away (add_prefix "IH" id) avoid in
1656
(pat, [dloc, IntroIdentifier id'])
1657
| _ -> consume_pattern avoid recvarname gl names in
1658
let hyprec,names = consume_pattern avoid hyprecname gl names in
1659
(* IH stays at top: we need to update tophyp *)
1660
(* This is buggy for intro-or-patterns with different first hypnames *)
1661
(* Would need to pass peel_tac as a continuation of intros_patterns *)
1662
(* (or to have hypotheses classified by blocks...) *)
1664
if tophyp=no_move then first_name_buggy avoid gl hyprec else tophyp
1667
[ intros_patterns true avoid [] (update destopt tophyp) [recpat];
1668
intros_patterns true avoid [] no_move [hyprec];
1669
peel_tac ra' names newtophyp] gl
1670
| (IndArg,hyprecname) :: ra' ->
1671
(* Rem: does not happen in Coq schemes, only in user-defined schemes *)
1672
let pat,names = consume_pattern avoid hyprecname gl names in
1673
tclTHEN (intros_patterns true avoid [] (update destopt tophyp) [pat])
1674
(peel_tac ra' names tophyp) gl
1675
| (RecArg,recvarname) :: ra' ->
1676
let pat,names = consume_pattern avoid recvarname gl names in
1677
tclTHEN (intros_patterns true avoid [] (update destopt tophyp) [pat])
1678
(peel_tac ra' names tophyp) gl
1679
| (OtherArg,_) :: ra' ->
1680
let pat,names = match names with
1681
| [] -> (dloc, IntroAnonymous), []
1682
| pat::names -> pat,names in
1683
tclTHEN (intros_patterns true avoid [] (update destopt tophyp) [pat])
1684
(peel_tac ra' names tophyp) gl
1686
check_unused_names names;
1687
re_intro_dependent_hypotheses tophyp statuslists gl
1689
peel_tac ra names no_move gl
1691
(* - le recalcul de indtyp � chaque it�ration de atomize_one est pour ne pas
1692
s'emb�ter � regarder si un letin_tac ne fait pas des
1693
substitutions aussi sur l'argument voisin *)
1695
(* Marche pas... faut prendre en compte l'occurrence pr�cise... *)
1697
let atomize_param_of_ind (indref,nparams) hyp0 gl =
1698
let tmptyp0 = pf_get_hyp_typ gl hyp0 in
1699
let typ0 = pf_apply reduce_to_quantified_ref gl indref tmptyp0 in
1700
let prods, indtyp = decompose_prod typ0 in
1701
let argl = snd (decompose_app indtyp) in
1702
let params = list_firstn nparams argl in
1703
(* le gl est important pour ne pas pr��valuer *)
1704
let rec atomize_one i avoid gl =
1706
let tmptyp0 = pf_get_hyp_typ gl hyp0 in
1707
(* If argl <> [], we expect typ0 not to be quantified, in order to
1708
avoid bound parameters... then we call pf_reduce_to_atomic_ind *)
1709
let indtyp = pf_apply reduce_to_atomic_ref gl indref tmptyp0 in
1710
let argl = snd (decompose_app indtyp) in
1711
let c = List.nth argl (i-1) in
1712
match kind_of_term c with
1713
| Var id when not (List.exists (occur_var (pf_env gl) id) avoid) ->
1714
atomize_one (i-1) ((mkVar id)::avoid) gl
1716
let x = fresh_id [] id gl in
1718
(letin_tac None (Name x) (mkVar id) None allClauses)
1719
(atomize_one (i-1) ((mkVar x)::avoid)) gl
1721
let id = id_of_name_using_hdchar (Global.env()) (pf_type_of gl c)
1723
let x = fresh_id [] id gl in
1725
(letin_tac None (Name x) c None allClauses)
1726
(atomize_one (i-1) ((mkVar x)::avoid)) gl
1730
atomize_one (List.length argl) params gl
1732
let find_atomic_param_of_ind nparams indtyp =
1733
let argl = snd (decompose_app indtyp) in
1734
let argv = Array.of_list argl in
1735
let params = list_firstn nparams argl in
1736
let indvars = ref Idset.empty in
1737
for i = nparams to (Array.length argv)-1 do
1738
match kind_of_term argv.(i) with
1740
when not (List.exists (occur_var (Global.env()) id) params) ->
1741
indvars := Idset.add id !indvars
1744
Idset.elements !indvars;
1747
(* [cook_sign] builds the lists [indhyps] of hyps that must be
1748
erased, the lists of hyps to be generalize [(hdeps,tdeps)] on the
1749
goal together with the places [(lstatus,rstatus)] where to re-intro
1750
them after induction. To know where to re-intro the dep hyp, we
1751
remember the name of the hypothesis [lhyp] after which (if the dep
1752
hyp is more recent than [hyp0]) or [rhyp] before which (if older
1753
than [hyp0]) its equivalent must be moved when the induction has
1754
been applied. Since computation of dependencies and [rhyp] is from
1755
more ancient (on the right) to more recent hyp (on the left) but
1756
the computation of [lhyp] progresses from the other way, [cook_hyp]
1757
is in two passes (an alternative would have been to write an
1758
higher-order algorithm). We use references to reduce
1759
the accumulation of arguments.
1761
To summarize, the situation looks like this
1763
Goal(n,x) -| H6:(Q n); x:A; H5:True; H4:(le O n); H3:(P n); H2:True; n:nat
1766
Induction hypothesis is H4 ([hyp0])
1767
Variable parameters of (le O n) is the singleton list with "n" ([indvars])
1768
Part of [indvars] really in context is the same ([indhyps])
1769
The dependent hyps are H3 and H6 ([dephyps])
1770
For H3 the memorized places are H5 ([lhyp]) and H2 ([rhyp])
1771
because these names are among the hyp which are fixed through the induction
1772
For H6 the neighbours are None ([lhyp]) and H5 ([rhyp])
1773
For H3, because on the right of H4, we remember rhyp (here H2)
1774
For H6, because on the left of H4, we remember lhyp (here None)
1775
For H4, we remember lhyp (here H5)
1777
The right neighbour is then translated into the left neighbour
1778
because move_hyp tactic needs the name of the hyp _after_ which we
1779
move the hyp to move.
1781
But, say in the 2nd subgoal of the hypotheses, the goal will be
1783
(m:nat)((P m)->(Q m)->(Goal m)) -> (P Sm)-> (Q Sm)-> (Goal Sm)
1784
^^^^^^^^^^^^^^^^^^^^^^^^^^^ ^^^^
1785
both go where H4 was goes where goes where
1788
We have to intro and move m and the recursive hyp first, but then
1789
where to move H3 ??? Only the hyp on its right is relevant, but we
1790
have to translate it into the name of the hyp on the left
1792
Note: this case where some hyp(s) in [dephyps] has(have) the same
1793
left neighbour as [hyp0] is the only problematic case with right
1794
neighbours. For the other cases (e.g. an hyp H1:(R n) between n and H2
1795
would have posed no problem. But for uniformity, we decided to use
1796
the right hyp for all hyps on the right of H4.
1798
Others solutions are welcome
1800
PC 9 fev 06: Adapted to accept multi argument principle with no
1801
main arg hyp. hyp0 is now optional, meaning that it is possible
1802
that there is no main induction hypotheses. In this case, we
1803
consider the last "parameter" (in [indvars]) as the limit between
1804
"left" and "right", BUT it must be included in indhyps.
1806
Other solutions are still welcome
1810
exception Shunt of identifier move_location
1812
let cook_sign hyp0_opt indvars env =
1815
| None -> List.hd (List.rev indvars), []
1816
| Some (hyp0,at_least_in_hyps) -> hyp0, at_least_in_hyps in
1817
(* First phase from L to R: get [indhyps], [decldep] and [statuslist]
1818
for the hypotheses before (= more ancient than) hyp0 (see above) *)
1819
let allindhyps = hyp0::indvars in
1820
let indhyps = ref [] in
1821
let decldeps = ref [] in
1822
let ldeps = ref [] in
1823
let rstatus = ref [] in
1824
let lstatus = ref [] in
1825
let before = ref true in
1826
let seek_deps env (hyp,_,_ as decl) rhyp =
1827
if hyp = hyp0 then begin
1829
(* If there was no main induction hypotheses, then hyp is one of
1830
indvars too, so add it to indhyps. *)
1831
(if hyp0_opt=None then indhyps := hyp::!indhyps);
1832
MoveToEnd false (* fake value *)
1833
end else if List.mem hyp indvars then begin
1834
(* warning: hyp can still occur after induction *)
1835
(* e.g. if the goal (t hyp hyp0) with other occs of hyp in t *)
1836
indhyps := hyp::!indhyps;
1839
if inhyps <> [] && List.mem hyp inhyps || inhyps = [] &&
1840
(List.exists (fun id -> occur_var_in_decl env id decl) allindhyps ||
1841
List.exists (fun (id,_,_) -> occur_var_in_decl env id decl) !decldeps)
1843
decldeps := decl::!decldeps;
1845
rstatus := (hyp,rhyp)::!rstatus
1847
ldeps := hyp::!ldeps; (* status computed in 2nd phase *)
1852
let _ = fold_named_context seek_deps env ~init:(MoveToEnd false) in
1853
(* 2nd phase from R to L: get left hyp of [hyp0] and [lhyps] *)
1854
let compute_lstatus lhyp (hyp,_,_) =
1855
if hyp = hyp0 then raise (Shunt lhyp);
1856
if List.mem hyp !ldeps then begin
1857
lstatus := (hyp,lhyp)::!lstatus;
1860
if List.mem hyp !indhyps then lhyp else MoveAfter hyp
1864
fold_named_context_reverse compute_lstatus ~init:(MoveToEnd true) env in
1865
raise (Shunt (MoveToEnd true)) (* ?? FIXME *)
1867
let statuslists = (!lstatus,List.rev !rstatus) in
1868
(statuslists, (if hyp0_opt=None then MoveToEnd true else lhyp0),
1869
!indhyps, !decldeps)
1873
The general form of an induction principle is the following:
1875
forall prm1 prm2 ... prmp, (induction parameters)
1876
forall Q1...,(Qi:Ti_1 -> Ti_2 ->...-> Ti_ni),...Qq, (predicates)
1877
branch1, branch2, ... , branchr, (branches of the principle)
1878
forall (x1:Ti_1) (x2:Ti_2) ... (xni:Ti_ni), (induction arguments)
1879
(HI: I prm1..prmp x1...xni) (optional main induction arg)
1880
-> (Qi x1...xni HI (f prm1...prmp x1...xni)).(conclusion)
1881
^^ ^^^^^^^^^^^^^^^^^^^^^^^^
1882
optional optional argument added if
1883
even if HI principle generated by functional
1884
present above induction, only if HI does not exist
1887
HI is not present when the induction principle does not come directly from an
1888
inductive type (like when it is generated by functional induction for
1889
example). HI is present otherwise BUT may not appear in the conclusion
1890
(dependent principle). HI and (f...) cannot be both present.
1892
Principles taken from functional induction have the final (f...).*)
1894
(* [rel_contexts] and [rel_declaration] actually contain triples, and
1895
lists are actually in reverse order to fit [compose_prod]. *)
1896
type elim_scheme = {
1897
elimc: constr with_ebindings option;
1899
indref: global_reference option;
1900
params: rel_context; (* (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *)
1901
nparams: int; (* number of parameters *)
1902
predicates: rel_context; (* (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...) *)
1903
npredicates: int; (* Number of predicates *)
1904
branches: rel_context; (* branchr,...,branch1 *)
1905
nbranches: int; (* Number of branches *)
1906
args: rel_context; (* (xni, Ti_ni) ... (x1, Ti_1) *)
1907
nargs: int; (* number of arguments *)
1908
indarg: rel_declaration option; (* Some (H,I prm1..prmp x1...xni)
1909
if HI is in premisses, None otherwise *)
1910
concl: types; (* Qi x1...xni HI (f...), HI and (f...)
1911
are optional and mutually exclusive *)
1912
indarg_in_concl: bool; (* true if HI appears at the end of conclusion *)
1913
farg_in_concl: bool; (* true if (f...) appears at the end of conclusion *)
1931
indarg_in_concl = false;
1932
farg_in_concl = false;
1936
(* Unification between ((elimc:elimt) ?i ?j ?k ?l ... ?m) and the
1937
hypothesis on which the induction is made *)
1938
let induction_tac with_evars (varname,lbind) typ scheme gl =
1939
let elimc,lbindelimc =
1940
match scheme.elimc with | Some x -> x | None -> error "No definition of the principle." in
1941
let elimt = scheme.elimt in
1942
let indclause = make_clenv_binding gl (mkVar varname,typ) lbind in
1944
make_clenv_binding gl
1945
(mkCast (elimc,DEFAULTcast, elimt),elimt) lbindelimc in
1946
elimination_clause_scheme with_evars true elimclause indclause gl
1948
let make_base n id =
1949
if n=0 or n=1 then id
1951
(* This extends the name to accept new digits if it already ends with *)
1953
id_of_string (atompart_of_id (make_ident (string_of_id id) (Some 0)))
1955
(* Builds two different names from an optional inductive type and a
1956
number, also deals with a list of names to avoid. If the inductive
1957
type is None, then hyprecname is IHi where i is a number. *)
1958
let make_up_names n ind_opt cname =
1959
let is_hyp = atompart_of_id cname = "H" in
1960
let base = string_of_id (make_base n cname) in
1961
let ind_prefix = "IH" in
1965
| None -> id_of_string ind_prefix
1966
| Some ind_id -> add_prefix ind_prefix (Nametab.id_of_global ind_id)
1967
else add_prefix ind_prefix cname in
1968
let hyprecname = make_base n base_ind in
1970
if n=1 (* Only one recursive argument *) or n=0 then []
1972
(* Forbid to use cname, cname0, hyprecname and hyprecname0 *)
1973
(* in order to get names such as f1, f2, ... *)
1975
(make_ident (string_of_id hyprecname) None) ::
1976
(make_ident (string_of_id hyprecname) (Some 0)) :: [] in
1977
if atompart_of_id cname <> "H" then
1978
(make_ident base (Some 0)) :: (make_ident base None) :: avoid
1980
id_of_string base, hyprecname, avoid
1982
let is_indhyp p n t =
1983
let l, c = decompose_prod t in
1984
let c,_ = decompose_app c in
1985
let p = p + List.length l in
1986
match kind_of_term c with
1987
| Rel k when p < k & k <= p + n -> true
1990
let chop_context n l =
1991
let rec chop_aux acc = function
1992
| n, (_,Some _,_ as h :: t) -> chop_aux (h::acc) (n, t)
1993
| 0, l2 -> (List.rev acc, l2)
1994
| n, (h::t) -> chop_aux (h::acc) (n-1, t)
1995
| _, [] -> anomaly "chop_context"
1999
let error_ind_scheme s =
2000
let s = if s <> "" then s^" " else s in
2001
error ("Cannot recognize "^s^"an induction scheme.")
2004
mkApp (build_coq_eq (), [| t; x; y |])
2007
mkApp ((build_coq_eq_data ()).refl, [| t; x |])
2010
mkApp (coq_constant "mkHEq" ["Logic";"JMeq"] "JMeq",
2014
mkApp (coq_constant "mkHEq" ["Logic";"JMeq"] "JMeq_refl",
2017
(* let id = lazy (coq_constant "mkHEq" ["Init";"Datatypes"] "id") *)
2019
(* let mkHEq t x u y = *)
2020
(* let ty = new_Type () in *)
2021
(* mkApp (coq_constant "mkHEq" ["Logic";"EqdepFacts"] "eq_dep", *)
2022
(* [| ty; mkApp (Lazy.force id, [|ty|]); t; x; u; y |]) *)
2024
(* let mkHRefl t x = *)
2025
(* let ty = new_Type () in *)
2026
(* mkApp (coq_constant "mkHEq" ["Logic";"EqdepFacts"] "eq_dep_intro", *)
2027
(* [| ty; mkApp (Lazy.force id, [|ty|]); t; x |]) *)
2029
let mkCoe a x p px y eq =
2030
mkApp (Option.get (build_coq_eq_data ()).rect, [| a; x; p; px; y; eq |])
2032
let lift_togethern n l =
2036
(lift n x :: acc, succ n))
2040
let lift_together l = lift_togethern 0 l
2042
let lift_list l = List.map (lift 1) l
2044
let ids_of_constr vars c =
2045
let rec aux vars c =
2046
match kind_of_term c with
2047
| Var id -> if List.mem id vars then vars else id :: vars
2049
(match kind_of_term f with
2052
let (mib,mip) = Global.lookup_inductive ind in
2053
array_fold_left_from mib.Declarations.mind_nparams
2055
| _ -> fold_constr aux vars c)
2056
| _ -> fold_constr aux vars c
2059
let make_abstract_generalize gl id concl dep ctx c eqs args refls =
2060
let meta = Evarutil.new_meta() in
2061
let term, typ = mkVar id, pf_get_hyp_typ gl id in
2062
let eqslen = List.length eqs in
2063
(* Abstract by the "generalized" hypothesis equality proof if necessary. *)
2066
mkProd (Anonymous, mkHEq (lift 1 c) (mkRel 1) typ term, lift 1 concl)
2069
(* Abstract by equalitites *)
2070
let eqs = lift_togethern 1 eqs in (* lift together and past genarg *)
2071
let abseqs = it_mkProd_or_LetIn ~init:(lift eqslen abshypeq) (List.map (fun x -> (Anonymous, None, x)) eqs) in
2072
(* Abstract by the "generalized" hypothesis. *)
2073
let genarg = mkProd (Name id, c, abseqs) in
2074
(* Abstract by the extension of the context *)
2075
let genctyp = it_mkProd_or_LetIn ~init:genarg ctx in
2076
(* The goal will become this product. *)
2077
let genc = mkCast (mkMeta meta, DEFAULTcast, genctyp) in
2078
(* Apply the old arguments giving the proper instantiation of the hyp *)
2079
let instc = mkApp (genc, Array.of_list args) in
2080
(* Then apply to the original instanciated hyp. *)
2081
let instc = mkApp (instc, [| mkVar id |]) in
2082
(* Apply the reflexivity proofs on the indices. *)
2083
let appeqs = mkApp (instc, Array.of_list refls) in
2084
(* Finaly, apply the reflexivity proof for the original hyp, to get a term of type gl again. *)
2085
let newc = if dep then mkApp (appeqs, [| mkHRefl typ term |]) else appeqs in
2088
let abstract_args gl id =
2089
let c = pf_get_hyp_typ gl id in
2090
let sigma = project gl in
2091
let env = pf_env gl in
2092
let concl = pf_concl gl in
2093
let dep = dependent (mkVar id) concl in
2094
let avoid = ref [] in
2096
let id = fresh_id !avoid (match name with Name n -> n | Anonymous -> id_of_string "gen_x") gl in
2097
avoid := id :: !avoid; id
2099
match kind_of_term c with
2101
(* Build application generalized w.r.t. the argument plus the necessary eqs.
2102
From env |- c : forall G, T and args : G we build
2103
(T[G'], G' : ctx, env ; G' |- args' : G, eqs := G'_i = G_i, refls : G' = G, vars to generalize)
2105
eqs are not lifted w.r.t. each other yet. (* will be needed when going to dependent indexes *)
2107
let aux (prod, ctx, ctxenv, c, args, eqs, refls, vars, env) arg =
2108
let (name, _, ty), arity =
2109
let rel, c = Reductionops.decomp_n_prod env sigma 1 prod in
2112
let argty = pf_type_of gl arg in
2113
let liftargty = lift (List.length ctx) argty in
2114
let convertible = Reductionops.is_conv_leq ctxenv sigma liftargty ty in
2115
match kind_of_term arg with
2116
| Var _ | Rel _ | Ind _ when convertible ->
2117
(subst1 arg arity, ctx, ctxenv, mkApp (c, [|arg|]), args, eqs, refls, vars, env)
2119
let name = get_id name in
2120
let decl = (Name name, None, ty) in
2121
let ctx = decl :: ctx in
2122
let c' = mkApp (lift 1 c, [|mkRel 1|]) in
2123
let args = arg :: args in
2124
let liftarg = lift (List.length ctx) arg in
2127
mkEq (lift 1 ty) (mkRel 1) liftarg, mkRefl argty arg
2129
mkHEq (lift 1 ty) (mkRel 1) liftargty liftarg, mkHRefl argty arg
2131
let eqs = eq :: lift_list eqs in
2132
let refls = refl :: refls in
2133
let vars = ids_of_constr vars arg in
2134
(arity, ctx, push_rel decl ctxenv, c', args, eqs, refls, vars, env)
2137
match kind_of_term f with
2140
let (mib,mip) = Global.lookup_inductive ind in
2141
let first = mib.Declarations.mind_nparams in
2142
let pars, args = array_chop first args in
2143
mkApp (f, pars), args
2146
let arity, ctx, ctxenv, c', args, eqs, refls, vars, env =
2147
Array.fold_left aux (pf_type_of gl f,[],env,f,[],[],[],[],env) args
2149
let args, refls = List.rev args, List.rev refls in
2150
Some (make_abstract_generalize gl id concl dep ctx c' eqs args refls,
2151
dep, succ (List.length ctx), vars)
2154
let abstract_generalize id ?(generalize_vars=true) gl =
2155
Coqlib.check_required_library ["Coq";"Logic";"JMeq"];
2156
let oldid = pf_get_new_id id gl in
2157
let newc = abstract_args gl id in
2159
| None -> tclIDTAC gl
2160
| Some (newc, dep, n, vars) ->
2163
tclTHENLIST [refine newc; rename_hyp [(id, oldid)]; tclDO n intro;
2164
generalize_dep (mkVar oldid)]
2166
tclTHENLIST [refine newc; clear [id]; tclDO n intro]
2168
if generalize_vars then tclTHEN tac
2169
(tclFIRST [revert (List.rev vars) ;
2170
tclMAP (fun id -> tclTRY (generalize_dep (mkVar id))) vars]) gl
2173
let dependent_pattern c gl =
2174
let cty = pf_type_of gl c in
2176
match kind_of_term cty with
2177
| App (f, args) -> Array.to_list args
2180
let varname c = match kind_of_term c with
2182
| _ -> id_of_string (hdchar (pf_env gl) c)
2184
let mklambda ty (c, id, cty) =
2185
let conclvar = subst_term_occ all_occurrences c ty in
2186
mkNamedLambda id cty conclvar
2188
let subst = (c, varname c, cty) :: List.rev_map (fun c -> (c, varname c, pf_type_of gl c)) deps in
2189
let concllda = List.fold_left mklambda (pf_concl gl) subst in
2190
let conclapp = applistc concllda (List.rev_map pi1 subst) in
2191
convert_concl_no_check conclapp DEFAULTcast gl
2194
let res = not (noccurn n c) in
2197
let list_filter_firsts f l =
2198
let rec list_filter_firsts_aux f acc l =
2200
| e::l' when f e -> list_filter_firsts_aux f (acc@[e]) l'
2203
list_filter_firsts_aux f [] l
2205
let count_rels_from n c =
2206
let rels = free_rels c in
2207
let cpt,rg = ref 0, ref n in
2208
while Intset.mem !rg rels do
2209
cpt:= !cpt+1; rg:= !rg+1;
2213
let count_nonfree_rels_from n c =
2214
let rels = free_rels c in
2215
if Intset.exists (fun x -> x >= n) rels then
2216
let cpt,rg = ref 0, ref n in
2217
while not (Intset.mem !rg rels) do
2218
cpt:= !cpt+1; rg:= !rg+1;
2221
else raise Not_found
2224
(* cuts a list in two parts, first of size n. Size must be greater than n *)
2226
let rec cut_list_aux acc n l =
2229
| [] -> assert false
2230
| e::l' -> cut_list_aux (acc@[e]) (n-1) l' in
2231
let res = cut_list_aux [] n l in
2235
(* This function splits the products of the induction scheme [elimt] into four
2237
- branches, easily detectable (they are not referred by rels in the subterm)
2238
- what was found before branches (acc1) that is: parameters and predicates
2239
- what was found after branches (acc3) that is: args and indarg if any
2240
if there is no branch, we try to fill in acc3 with args/indargs.
2241
We also return the conclusion.
2243
let decompose_paramspred_branch_args elimt =
2244
let rec cut_noccur elimt acc2 : rel_context * rel_context * types =
2245
match kind_of_term elimt with
2246
| Prod(nme,tpe,elimt') ->
2247
let hd_tpe,_ = decompose_app (snd (decompose_prod_assum tpe)) in
2248
if not (occur_rel 1 elimt') && isRel hd_tpe
2249
then cut_noccur elimt' ((nme,None,tpe)::acc2)
2250
else let acc3,ccl = decompose_prod_assum elimt in acc2 , acc3 , ccl
2251
| App(_, _) | Rel _ -> acc2 , [] , elimt
2252
| _ -> error_ind_scheme "" in
2253
let rec cut_occur elimt acc1 : rel_context * rel_context * rel_context * types =
2254
match kind_of_term elimt with
2255
| Prod(nme,tpe,c) when occur_rel 1 c -> cut_occur c ((nme,None,tpe)::acc1)
2256
| Prod(nme,tpe,c) -> let acc2,acc3,ccl = cut_noccur elimt [] in acc1,acc2,acc3,ccl
2257
| App(_, _) | Rel _ -> acc1,[],[],elimt
2258
| _ -> error_ind_scheme "" in
2259
let acc1, acc2 , acc3, ccl = cut_occur elimt [] in
2260
(* Particular treatment when dealing with a dependent empty type elim scheme:
2261
if there is no branch, then acc1 contains all hyps which is wrong (acc1
2262
should contain parameters and predicate only). This happens for an empty
2263
type (See for example Empty_set_ind, as False would actually be ok). Then
2264
we must find the predicate of the conclusion to separate params_pred from
2265
args. We suppose there is only one predicate here. *)
2266
if List.length acc2 <> 0 then acc1, acc2 , acc3, ccl
2268
let hyps,ccl = decompose_prod_assum elimt in
2269
let hd_ccl_pred,_ = decompose_app ccl in
2270
match kind_of_term hd_ccl_pred with
2271
| Rel i -> let acc3,acc1 = cut_list (i-1) hyps in acc1 , [] , acc3 , ccl
2272
| _ -> error_ind_scheme ""
2275
let exchange_hd_app subst_hd t =
2276
let hd,args= decompose_app t in mkApp (subst_hd,Array.of_list args)
2280
(* [rebuild_elimtype_from_scheme scheme] rebuilds the type of an
2281
eliminator from its [scheme_info]. The idea is to build variants of
2282
eliminator by modifying their scheme_info, then rebuild the
2283
eliminator type, then prove it (with tactics). *)
2284
let rebuild_elimtype_from_scheme (scheme:elim_scheme): types =
2286
match scheme.indarg with
2287
| None -> scheme.concl
2288
| Some x -> mkProd_or_LetIn x scheme.concl in
2289
let xihiconcl = it_mkProd_or_LetIn hiconcl scheme.args in
2290
let brconcl = it_mkProd_or_LetIn xihiconcl scheme.branches in
2291
let predconcl = it_mkProd_or_LetIn brconcl scheme.predicates in
2292
let paramconcl = it_mkProd_or_LetIn predconcl scheme.params in
2297
exception NoLastArgCcl
2299
(* Builds an elim_scheme from its type and calling form (const+binding). We
2300
first separate branches. We obtain branches, hyps before (params + preds),
2301
hyps after (args <+ indarg if present>) and conclusion. Then we proceed as
2304
- separate parameters and predicates in params_preds. For that we build:
2305
forall (x1:Ti_1)(xni:Ti_ni) (HI:I prm1..prmp x1...xni), DUMMY x1...xni HI/farg
2306
^^^^^^^^^^^^^^^^^^^^^^^^^ ^^^^^^^
2308
Free rels appearing in this term are parameters (branches should not
2309
appear, and the only predicate would have been Qi but we replaced it by
2310
DUMMY). We guess this heuristic catches all params. TODO: generalize to
2311
the case where args are merged with branches (?) and/or where several
2312
predicates are cited in the conclusion.
2314
- finish to fill in the elim_scheme: indarg/farg/args and finally indref. *)
2315
let compute_elim_sig ?elimc elimt =
2316
let params_preds,branches,args_indargs,conclusion =
2317
decompose_paramspred_branch_args elimt in
2319
let ccl = exchange_hd_app (mkVar (id_of_string "__QI_DUMMY__")) conclusion in
2320
let concl_with_args = it_mkProd_or_LetIn ccl args_indargs in
2321
let nparams = Intset.cardinal (free_rels concl_with_args) in
2322
let preds,params = cut_list (List.length params_preds - nparams) params_preds in
2324
(* A first approximation, further analysis will tweak it *)
2325
let res = ref { empty_scheme with
2326
(* This fields are ok: *)
2327
elimc = elimc; elimt = elimt; concl = conclusion;
2328
predicates = preds; npredicates = List.length preds;
2329
branches = branches; nbranches = List.length branches;
2330
farg_in_concl = isApp ccl && isApp (last_arg ccl);
2331
params = params; nparams = nparams;
2332
(* all other fields are unsure at this point. Including these:*)
2333
args = args_indargs; nargs = List.length args_indargs; } in
2335
(* Order of tests below is important. Each of them exits if successful. *)
2336
(* 1- First see if (f x...) is in the conclusion. *)
2337
if !res.farg_in_concl
2341
indarg_in_concl = false; farg_in_concl = true };
2344
(* 2- If no args_indargs (=!res.nargs at this point) then no indarg *)
2345
if !res.nargs=0 then raise Exit;
2346
(* 3- Look at last arg: is it the indarg? *)
2348
match List.hd args_indargs with
2349
| hiname,Some _,hi -> error_ind_scheme ""
2351
let hi_ind, hi_args = decompose_app hi in
2352
let hi_is_ind = (* hi est d'un type globalisable *)
2353
match kind_of_term hi_ind with
2354
| Ind (mind,_) -> true
2357
| Construct _ -> true
2359
let hi_args_enough = (* hi a le bon nbre d'arguments *)
2360
List.length hi_args = List.length params + !res.nargs -1 in
2361
(* FIXME: Ces deux tests ne sont pas suffisants. *)
2362
if not (hi_is_ind & hi_args_enough) then raise Exit (* No indarg *)
2363
else (* Last arg is the indarg *)
2365
indarg = Some (List.hd !res.args);
2366
indarg_in_concl = occur_rel 1 ccl;
2367
args = List.tl !res.args; nargs = !res.nargs - 1;
2370
raise Exit(* exit anyway *)
2371
with Exit -> (* Ending by computing indrev: *)
2372
match !res.indarg with
2373
| None -> !res (* No indref *)
2374
| Some ( _,Some _,_) -> error_ind_scheme ""
2375
| Some ( _,None,ind) ->
2376
let indhd,indargs = decompose_app ind in
2377
try {!res with indref = Some (global_of_constr indhd) }
2378
with _ -> error "Cannot find the inductive type of the inductive scheme.";;
2380
(* Check that the elimination scheme has a form similar to the
2381
elimination schemes built by Coq. Schemes may have the standard
2382
form computed from an inductive type OR (feb. 2006) a non standard
2383
form. That is: with no main induction argument and with an optional
2384
extra final argument of the form (f x y ...) in the conclusion. In
2385
the non standard case, naming of generated hypos is slightly
2387
let compute_elim_signature elimc elimt names_info ind_type_guess =
2388
let scheme = compute_elim_sig ~elimc:elimc elimt in
2389
let f,l = decompose_app scheme.concl in
2390
(* V�rifier que les arguments de Qi sont bien les xi. *)
2391
match scheme.indarg with
2392
| Some (_,Some _,_) -> error "Strange letin, cannot recognize an induction scheme."
2393
| None -> (* Non standard scheme *)
2395
let hd = fst (decompose_app c) in match kind_of_term hd with
2396
| Rel q when n < q & q <= n+scheme.npredicates -> IndArg
2397
| _ when hd = ind_type_guess & not scheme.farg_in_concl -> RecArg
2399
let rec check_branch p c =
2400
match kind_of_term c with
2401
| Prod (_,t,c) -> is_pred p t :: check_branch (p+1) c
2402
| LetIn (_,_,_,c) -> OtherArg :: check_branch (p+1) c
2403
| _ when is_pred p c = IndArg -> []
2404
| _ -> raise Exit in
2405
let rec find_branches p lbrch =
2407
| (_,None,t)::brs ->
2409
let lchck_brch = check_branch p t in
2410
let n = List.fold_left
2411
(fun n b -> if b=RecArg then n+1 else n) 0 lchck_brch in
2412
let recvarname, hyprecname, avoid =
2413
make_up_names n scheme.indref names_info in
2415
List.map (fun b -> (b,if b=IndArg then hyprecname else recvarname))
2417
(avoid,namesign) :: find_branches (p+1) brs
2418
with Exit-> error_ind_scheme "the branches of")
2419
| (_,Some _,_)::_ -> error_ind_scheme "the branches of"
2421
let indsign = Array.of_list (find_branches 0 (List.rev scheme.branches)) in
2424
| Some ( _,None,ind) -> (* Standard scheme from an inductive type *)
2425
let indhd,indargs = decompose_app ind in
2427
let hd = fst (decompose_app c) in match kind_of_term hd with
2428
| Rel q when n < q & q <= n+scheme.npredicates -> IndArg
2429
| _ when hd = indhd -> RecArg
2431
let rec check_branch p c = match kind_of_term c with
2432
| Prod (_,t,c) -> is_pred p t :: check_branch (p+1) c
2433
| LetIn (_,_,_,c) -> OtherArg :: check_branch (p+1) c
2434
| _ when is_pred p c = IndArg -> []
2435
| _ -> raise Exit in
2436
let rec find_branches p lbrch =
2438
| (_,None,t)::brs ->
2440
let lchck_brch = check_branch p t in
2441
let n = List.fold_left
2442
(fun n b -> if b=RecArg then n+1 else n) 0 lchck_brch in
2443
let recvarname, hyprecname, avoid =
2444
make_up_names n scheme.indref names_info in
2446
List.map (fun b -> (b,if b=IndArg then hyprecname else recvarname))
2448
(avoid,namesign) :: find_branches (p+1) brs
2449
with Exit -> error_ind_scheme "the branches of")
2450
| (_,Some _,_)::_ -> error_ind_scheme "the branches of"
2452
(* Check again conclusion *)
2454
let ccl_arg_ok = is_pred (p + scheme.nargs + 1) f = IndArg in
2456
list_lastn scheme.nargs indargs
2457
= extended_rel_list 0 scheme.args in
2458
if not (ccl_arg_ok & ind_is_ok) then
2459
error_ind_scheme "the conclusion of";
2462
let indsign = Array.of_list (find_branches 0 (List.rev scheme.branches)) in
2466
let find_elim_signature isrec elim hyp0 gl =
2467
let tmptyp0 = pf_get_hyp_typ gl hyp0 in
2468
let (elimc,elimt),ind = match elim with
2470
let mind,_ = pf_reduce_to_quantified_ind gl tmptyp0 in
2471
let s = elimination_sort_of_goal gl in
2473
if isrec then lookup_eliminator mind s
2474
else pf_apply make_case_gen gl mind s in
2475
let elimt = pf_type_of gl elimc in
2476
((elimc, NoBindings), elimt), mkInd mind
2477
| Some (elimc,lbind as e) ->
2478
let ind_type_guess,_ = decompose_app (snd (decompose_prod tmptyp0)) in
2479
(e, pf_type_of gl elimc), ind_type_guess in
2480
let indsign,elim_scheme =
2481
compute_elim_signature elimc elimt hyp0 ind in
2482
(indsign,elim_scheme)
2485
(* Instantiate all meta variables of elimclause using lid, some elts
2486
of lid are parameters (first ones), the other are
2487
arguments. Returns the clause obtained. *)
2488
let recolle_clenv scheme lid elimclause gl =
2489
let _,arr = destApp elimclause.templval.rebus in
2493
match kind_of_term x with
2495
| _ -> errorlabstrm "elimination_clause"
2496
(str "The type of the elimination clause is not well-formed."))
2498
let nmv = Array.length lindmv in
2499
let lidparams,lidargs = cut_list (scheme.nparams) lid in
2500
let nidargs = List.length lidargs in
2501
(* parameters correspond to first elts of lid. *)
2502
let clauses_params =
2503
list_map_i (fun i id -> mkVar id , pf_get_hyp_typ gl id , lindmv.(i))
2505
(* arguments correspond to last elts of lid. *)
2508
(fun i id -> mkVar id , pf_get_hyp_typ gl id , lindmv.(nmv-nidargs+i))
2511
match scheme.indarg with
2513
| Some (x,_,typx) -> []
2515
let clauses = clauses_params@clauses_args@clause_indarg in
2516
(* iteration of clenv_fchain with all infos we have. *)
2520
(* from_n (Some 0) means that x should be taken "as is" without
2521
trying to unify (which would lead to trying to apply it to
2522
evars if y is a product). *)
2523
let indclause = mk_clenv_from_n gl (Some 0) (x,y) in
2524
let elimclause' = clenv_fchain i acc indclause in
2529
(* Unification of the goal and the principle applied to meta variables:
2530
(elimc ?i ?j ?k...?l). This solves partly meta variables (and may
2531
produce new ones). Then refine with the resulting term with holes.
2533
let induction_tac_felim with_evars indvars scheme gl =
2534
let elimt = scheme.elimt in
2535
let elimc,lbindelimc =
2536
match scheme.elimc with | Some x -> x | None -> error "No definition of the principle." in
2537
(* elimclause contains this: (elimc ?i ?j ?k...?l) *)
2539
make_clenv_binding gl (mkCast (elimc,DEFAULTcast, elimt),elimt) lbindelimc in
2540
(* elimclause' is built from elimclause by instanciating all args and params. *)
2541
let elimclause' = recolle_clenv scheme indvars elimclause gl in
2542
(* one last resolution (useless?) *)
2543
let resolved = clenv_unique_resolver true elimclause' gl in
2544
clenv_refine with_evars resolved gl
2546
let apply_induction_in_context isrec hyp0 indsign indvars names induct_tac gl =
2547
let env = pf_env gl in
2548
let statlists,lhyp0,indhyps,deps = cook_sign hyp0 indvars env in
2549
let tmpcl = it_mkNamedProd_or_LetIn (pf_concl gl) deps in
2550
let names = compute_induction_names (Array.length indsign) names in
2551
let dephyps = List.map (fun (id,_,_) -> id) deps in
2554
(fun a (id,b,_) -> if b = None then (mkVar id)::a else a) [] deps in
2557
(* Generalize dependent hyps (but not args) *)
2558
if deps = [] then tclIDTAC else apply_type tmpcl deps_cstr;
2559
(* clear dependent hyps *)
2561
(* side-conditions in elim (resp case) schemes come last (resp first) *)
2562
(if isrec then tclTHENFIRSTn else tclTHENLASTn)
2563
(tclTHEN induct_tac (tclTRY (thin (List.rev indhyps))))
2565
(induct_discharge statlists lhyp0 (List.rev dephyps)) indsign names)
2569
(* Induction with several induction arguments, main differences with
2570
induction_from_context is that there is no main induction argument,
2571
so we chose one to be the positioning reference. On the other hand,
2572
all args and params must be given, so we help a bit the unifier by
2573
making the "pattern" by hand before calling induction_tac_felim
2574
FIXME: REUNIF AVEC induction_tac_felim? *)
2575
let induction_from_context_l isrec with_evars elim_info lid names gl =
2576
let indsign,scheme = elim_info in
2577
(* number of all args, counting farg and indarg if present. *)
2578
let nargs_indarg_farg = scheme.nargs
2579
+ (if scheme.farg_in_concl then 1 else 0)
2580
+ (if scheme.indarg <> None then 1 else 0) in
2581
(* Number of given induction args must be exact. *)
2582
if List.length lid <> nargs_indarg_farg + scheme.nparams then
2583
error "Not the right number of arguments given to induction scheme.";
2584
(* hyp0 is used for re-introducing hyps at the right place afterward.
2585
We chose the first element of the list of variables on which to
2586
induct. It is probably the first of them appearing in the
2588
let hyp0,indvars,lid_params =
2590
| [] -> anomaly "induction_from_context_l"
2592
let nargs_without_first = nargs_indarg_farg - 1 in
2593
let ivs,lp = cut_list nargs_without_first l in
2595
(* terms to patternify we must patternify indarg or farg if present in concl *)
2596
let lid_in_pattern =
2597
if scheme.indarg <> None & not scheme.indarg_in_concl then List.rev indvars
2598
else List.rev (hyp0::indvars) in
2599
let lidcstr = List.map (fun x -> mkVar x) lid_in_pattern in
2600
let realindvars = (* hyp0 is a real induction arg if it is not the
2601
farg in the conclusion of the induction scheme *)
2602
List.rev ((if scheme.farg_in_concl then indvars else hyp0::indvars) @ lid_params) in
2603
let induct_tac = tclTHENLIST [
2604
(* pattern to make the predicate appear. *)
2605
reduce (Pattern (List.map inj_with_occurrences lidcstr)) onConcl;
2606
(* Induction by "refine (indscheme ?i ?j ?k...)" + resolution of all
2607
possible holes using arguments given by the user (but the
2609
(* FIXME: Tester ca avec un principe dependant et non-dependant *)
2610
induction_tac_felim with_evars realindvars scheme
2612
apply_induction_in_context isrec
2613
None indsign (hyp0::indvars) names induct_tac gl
2615
let induction_from_context isrec with_evars elim_info (hyp0,lbind) names
2617
let indsign,scheme = elim_info in
2618
let indref = match scheme.indref with | None -> assert false | Some x -> x in
2619
let tmptyp0 = pf_get_hyp_typ gl hyp0 in
2620
let typ0 = pf_apply reduce_to_quantified_ref gl indref tmptyp0 in
2622
find_atomic_param_of_ind scheme.nparams (snd (decompose_prod typ0)) in
2623
let induct_tac = tclTHENLIST [
2624
induction_tac with_evars (hyp0,lbind) typ0 scheme;
2625
tclTRY (unfold_body hyp0);
2628
apply_induction_in_context isrec
2629
(Some (hyp0,inhyps)) indsign indvars names induct_tac gl
2631
exception TryNewInduct of exn
2633
let induction_with_atomization_of_ind_arg isrec with_evars elim names (hyp0,lbind) inhyps gl =
2634
let (indsign,scheme as elim_info) = find_elim_signature isrec elim hyp0 gl in
2635
if scheme.indarg = None then (* This is not a standard induction scheme (the
2636
argument is probably a parameter) So try the
2637
more general induction mechanism. *)
2638
induction_from_context_l isrec with_evars elim_info [hyp0] names gl
2640
let indref = match scheme.indref with | None -> assert false | Some x -> x in
2642
(atomize_param_of_ind (indref,scheme.nparams) hyp0)
2643
(induction_from_context isrec with_evars elim_info
2644
(hyp0,lbind) names inhyps) gl
2646
(* Induction on a list of induction arguments. Analyse the elim
2647
scheme (which is mandatory for multiple ind args), check that all
2648
parameters and arguments are given (mandatory too). *)
2649
let induction_without_atomization isrec with_evars elim names lid gl =
2650
let (indsign,scheme as elim_info) =
2651
find_elim_signature isrec elim (List.hd lid) gl in
2653
scheme.nparams + scheme.nargs
2654
+ (if scheme.farg_in_concl then 1 else 0)
2655
+ (if scheme.indarg <> None then 1 else 0)
2657
let nlid = List.length lid in
2658
if nlid <> awaited_nargs
2659
then error "Not the right number of induction arguments."
2660
else induction_from_context_l isrec with_evars elim_info lid names gl
2662
let enforce_eq_name id gl = function
2663
| (b,(loc,IntroAnonymous)) ->
2664
(b,(loc,IntroIdentifier (fresh_id [id] (add_prefix "Heq" id) gl)))
2665
| (b,(loc,IntroFresh heq_base)) ->
2666
(b,(loc,IntroIdentifier (fresh_id [id] heq_base gl)))
2670
let has_selected_occurrences = function
2673
cls.concl_occs <> all_occurrences_expr ||
2674
cls.onhyps <> None && List.exists (fun ((occs,_),hl) ->
2675
occs <> all_occurrences_expr || hl <> InHyp) (Option.get cls.onhyps)
2677
(* assume that no occurrences are selected *)
2678
let clear_unselected_context id inhyps cls gl =
2680
| None -> tclIDTAC gl
2682
if occur_var (pf_env gl) id (pf_concl gl) &&
2683
cls.concl_occs = no_occurrences_expr
2684
then errorlabstrm ""
2685
(str "Conclusion must be mentioned: it depends on " ++ pr_id id
2687
match cls.onhyps with
2689
let to_erase (id',_,_ as d) =
2690
if List.mem id' inhyps then (* if selected, do not erase *) None
2692
(* erase if not selected and dependent on id or selected hyps *)
2693
let test id = occur_var_in_decl (pf_env gl) id d in
2694
if List.exists test (id::inhyps) then Some id' else None in
2695
let ids = list_map_filter to_erase (pf_hyps gl) in
2697
| None -> tclIDTAC gl
2699
let new_induct_gen isrec with_evars elim (eqname,names) (c,lbind) cls gl =
2700
let inhyps = match cls with
2701
| Some {onhyps=Some hyps} -> List.map (fun ((_,id),_) -> id) hyps
2703
match kind_of_term c with
2704
| Var id when not (mem_named_context id (Global.named_context()))
2705
& lbind = NoBindings & not with_evars & eqname = None
2706
& not (has_selected_occurrences cls) ->
2708
(clear_unselected_context id inhyps cls)
2709
(induction_with_atomization_of_ind_arg
2710
isrec with_evars elim names (id,lbind) inhyps) gl
2712
let x = id_of_name_using_hdchar (Global.env()) (pf_type_of gl c)
2714
let id = fresh_id [] x gl in
2715
(* We need the equality name now *)
2716
let with_eq = Option.map (fun eq -> (false,eq)) eqname in
2717
(* TODO: if ind has predicate parameters, use JMeq instead of eq *)
2719
(letin_tac_gen with_eq (Name id) c None (Option.default allClauses cls,false))
2720
(induction_with_atomization_of_ind_arg
2721
isrec with_evars elim names (id,lbind) inhyps) gl
2723
(* Induction on a list of arguments. First make induction arguments
2724
atomic (using letins), then do induction. The specificity here is
2725
that all arguments and parameters of the scheme are given
2726
(mandatory for the moment), so we don't need to deal with
2727
parameters of the inductive type as in new_induct_gen. *)
2728
let new_induct_gen_l isrec with_evars elim (eqname,names) lc gl =
2729
if eqname <> None then
2730
errorlabstrm "" (str "Do not know what to do with " ++
2731
pr_intro_pattern (Option.get eqname));
2732
let newlc = ref [] in
2733
let letids = ref [] in
2734
let rec atomize_list l gl =
2738
match kind_of_term c with
2739
| Var id when not (mem_named_context id (Global.named_context()))
2741
let _ = newlc:= id::!newlc in
2746
id_of_name_using_hdchar (Global.env()) (pf_type_of gl c) Anonymous in
2748
let id = fresh_id [] x gl in
2749
let newl' = List.map (replace_term c (mkVar id)) l' in
2750
let _ = newlc:=id::!newlc in
2751
let _ = letids:=id::!letids in
2753
(letin_tac None (Name id) c None allClauses)
2754
(atomize_list newl') gl in
2758
(fun gl' -> (* recompute each time to have the new value of newlc *)
2759
induction_without_atomization isrec with_evars elim names !newlc gl') ;
2760
(* after induction, try to unfold all letins created by atomize_list
2761
FIXME: unfold_all does not exist anywhere else? *)
2762
(fun gl' -> (* recompute each time to have the new value of letids *)
2763
tclMAP (fun x -> tclTRY (unfold_all x)) !letids gl')
2768
let induct_destruct_l isrec with_evars lc elim names cls =
2769
(* Several induction hyps: induction scheme is mandatory *)
2773
errorlabstrm "" (strbrk "Induction scheme must be given when several induction hypothesis are given.\n" ++
2774
str "Example: induction x1 x2 x3 using my_scheme.") in
2778
match x with (* FIXME: should we deal with ElimOnIdent? *)
2779
| ElimOnConstr (x,NoBindings) -> x
2780
| _ -> error "Don't know where to find some argument.")
2784
"'in' clause not supported when several induction hypothesis are given.";
2785
new_induct_gen_l isrec with_evars elim names newlc
2787
(* Induction either over a term, over a quantified premisse, or over
2788
several quantified premisses (like with functional induction
2790
TODO: really unify induction with one and induction with several
2792
let induct_destruct isrec with_evars (lc,elim,names,cls) =
2793
assert (List.length lc > 0); (* ensured by syntax, but if called inside caml? *)
2794
if List.length lc = 1 then (* induction on one arg: use old mechanism *)
2797
(fun c -> new_induct_gen isrec with_evars elim names c cls)
2799
with (* If this fails, try with new mechanism but if it fails too,
2800
then the exception is the first one. *)
2802
(try induct_destruct_l isrec with_evars lc elim names cls
2804
else induct_destruct_l isrec with_evars lc elim names cls
2806
let induction_destruct isrec with_evars = function
2808
| [a] -> induct_destruct isrec with_evars a
2811
(induct_destruct isrec with_evars a)
2812
(tclMAP (induct_destruct false with_evars) l)
2814
let new_induct ev lc e idl cls = induct_destruct true ev (lc,e,idl,cls)
2815
let new_destruct ev lc e idl cls = induct_destruct false ev (lc,e,idl,cls)
2817
(* The registered tactic, which calls the default elimination
2818
* if no elimination constant is provided. *)
2820
(* Induction tactics *)
2822
(* This was Induction before 6.3 (induction only in quantified premisses) *)
2823
let raw_induct s = tclTHEN (intros_until_id s) (tclLAST_HYP simplest_elim)
2824
let raw_induct_nodep n = tclTHEN (intros_until_n n) (tclLAST_HYP simplest_elim)
2826
let simple_induct_id hyp = raw_induct hyp
2827
let simple_induct_nodep = raw_induct_nodep
2829
let simple_induct = function
2830
| NamedHyp id -> simple_induct_id id
2831
| AnonHyp n -> simple_induct_nodep n
2833
(* Destruction tactics *)
2835
let simple_destruct_id s =
2836
(tclTHEN (intros_until_id s) (tclLAST_HYP simplest_case))
2837
let simple_destruct_nodep n =
2838
(tclTHEN (intros_until_n n) (tclLAST_HYP simplest_case))
2840
let simple_destruct = function
2841
| NamedHyp id -> simple_destruct_id id
2842
| AnonHyp n -> simple_destruct_nodep n
2845
* Eliminations giving the type instead of the proof.
2846
* These tactics use the default elimination constant and
2847
* no substitutions at all.
2848
* May be they should be integrated into Elim ...
2851
let elim_scheme_type elim t gl =
2852
let clause = mk_clenv_type_of gl elim in
2853
match kind_of_term (last_arg clause.templval.rebus) with
2856
(* t is inductive, then CUMUL or CONV is irrelevant *)
2857
clenv_unify true Reduction.CUMUL t
2858
(clenv_meta_type clause mv) clause in
2859
res_pf clause' ~allow_K:true gl
2860
| _ -> anomaly "elim_scheme_type"
2862
let elim_type t gl =
2863
let (ind,t) = pf_reduce_to_atomic_ind gl t in
2864
let elimc = lookup_eliminator ind (elimination_sort_of_goal gl) in
2865
elim_scheme_type elimc t gl
2867
let case_type t gl =
2868
let (ind,t) = pf_reduce_to_atomic_ind gl t in
2869
let env = pf_env gl in
2870
let elimc = make_case_gen env (project gl) ind (elimination_sort_of_goal gl) in
2871
elim_scheme_type elimc t gl
2874
(* Some eliminations frequently used *)
2876
(* These elimination tactics are particularly adapted for sequent
2877
calculus. They take a clause as argument, and yield the
2878
elimination rule if the clause is of the form (Some id) and a
2879
suitable introduction rule otherwise. They do not depend on
2880
the name of the eliminated constant, so they can be also
2881
used on ad-hoc disjunctions and conjunctions introduced by
2883
-- Eduardo Gimenez (11/8/97)
2885
HH (29/5/99) replaces failures by specific error messages
2889
let t = pf_get_hyp_typ gl id in
2890
if is_conjunction (pf_hnf_constr gl t) then
2891
(tclTHEN (simplest_elim (mkVar id)) (tclDO 2 intro)) gl
2894
(str("Tactic andE expects "^(string_of_id id)^" is a conjunction."))
2899
| None -> simplest_split
2900
| Some ((_,id),_) -> andE id)
2904
let t = pf_get_hyp_typ gl id in
2905
if is_disjunction (pf_hnf_constr gl t) then
2906
(tclTHEN (simplest_elim (mkVar id)) intro) gl
2909
(str("Tactic orE expects "^(string_of_id id)^" is a disjunction."))
2914
| (Some ((_,id),_)) -> orE id
2915
| None -> (if b then right else left) NoBindings)
2919
let t = pf_get_hyp_typ gl id in
2920
if is_imp_term (pf_hnf_constr gl t) then
2921
let (dom, _, rng) = destProd (pf_hnf_constr gl t) in
2924
(apply_term (mkVar id) [mkMeta (new_meta())]) gl
2927
(str("Tactic impE expects "^(string_of_id id)^
2928
" is a an implication."))
2934
| Some ((_,id),_) -> impE id)
2937
(************************************************)
2938
(* Tactics related with logic connectives *)
2939
(************************************************)
2941
(* Reflexivity tactics *)
2943
let setoid_reflexivity = ref (fun _ -> assert false)
2944
let register_setoid_reflexivity f = setoid_reflexivity := f
2946
let reflexivity_red allowred gl =
2947
(* PL: usual reflexivity don't perform any reduction when searching
2948
for an equality, but we may need to do some when called back from
2949
inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *)
2950
let concl = if not allowred then pf_concl gl
2951
else whd_betadeltaiota (pf_env gl) (project gl) (pf_concl gl)
2953
match match_with_equality_type concl with
2955
| Some _ -> Some (one_constructor 1 NoBindings)
2957
let reflexivity gl =
2958
match reflexivity_red false gl with
2959
| None -> !setoid_reflexivity gl
2960
| Some tac -> tac gl
2962
let intros_reflexivity = (tclTHEN intros reflexivity)
2964
(* Symmetry tactics *)
2966
(* This tactic first tries to apply a constant named sym_eq, where eq
2967
is the name of the equality predicate. If this constant is not
2968
defined and the conclusion is a=b, it solves the goal doing (Cut
2969
b=a;Intro H;Case H;Constructor 1) *)
2971
let setoid_symmetry = ref (fun _ -> assert false)
2972
let register_setoid_symmetry f = setoid_symmetry := f
2974
let symmetry_red allowred gl =
2975
(* PL: usual symmetry don't perform any reduction when searching
2976
for an equality, but we may need to do some when called back from
2977
inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *)
2978
let concl = if not allowred then pf_concl gl
2979
else whd_betadeltaiota (pf_env gl) (project gl) (pf_concl gl)
2981
match match_with_equation concl with
2983
| Some (hdcncl,args) -> Some (fun gl ->
2984
let hdcncls = string_of_inductive hdcncl in
2988
(convert_concl_no_check concl DEFAULTcast)
2989
(apply (pf_parse_const gl ("sym_"^hdcncls))) gl
2991
let symc = match args with
2992
| [t1; c1; t2; c2] -> mkApp (hdcncl, [| t2; c2; t1; c1 |])
2993
| [typ;c1;c2] -> mkApp (hdcncl, [| typ; c2; c1 |])
2994
| [c1;c2] -> mkApp (hdcncl, [| c2; c1 |])
2997
tclTHENFIRST (cut symc)
3000
tclLAST_HYP simplest_case;
3001
one_constructor 1 NoBindings ])
3006
match symmetry_red false gl with
3007
| None -> !setoid_symmetry gl
3008
| Some tac -> tac gl
3010
let setoid_symmetry_in = ref (fun _ _ -> assert false)
3011
let register_setoid_symmetry_in f = setoid_symmetry_in := f
3013
let symmetry_in id gl =
3014
let ctype = pf_type_of gl (mkVar id) in
3015
let sign,t = decompose_prod_assum ctype in
3016
match match_with_equation t with
3017
| None -> !setoid_symmetry_in id gl
3018
| Some (hdcncl,args) ->
3019
let symccl = match args with
3020
| [t1; c1; t2; c2] -> mkApp (hdcncl, [| t2; c2; t1; c1 |])
3021
| [typ;c1;c2] -> mkApp (hdcncl, [| typ; c2; c1 |])
3022
| [c1;c2] -> mkApp (hdcncl, [| c2; c1 |])
3023
| _ -> assert false in
3024
tclTHENS (cut (it_mkProd_or_LetIn symccl sign))
3025
[ intro_replacing id;
3026
tclTHENLIST [ intros; symmetry; apply (mkVar id); assumption ] ]
3029
let intros_symmetry =
3032
| None -> tclTHEN intros symmetry
3033
| Some ((_,id),_) -> symmetry_in id)
3035
(* Transitivity tactics *)
3037
(* This tactic first tries to apply a constant named trans_eq, where eq
3038
is the name of the equality predicate. If this constant is not
3039
defined and the conclusion is a=b, it solves the goal doing
3041
[Cut x2=x3; [Intros e1 e2; Case e2;Assumption
3047
let setoid_transitivity = ref (fun _ _ -> assert false)
3048
let register_setoid_transitivity f = setoid_transitivity := f
3050
let transitivity_red allowred t gl =
3051
(* PL: usual transitivity don't perform any reduction when searching
3052
for an equality, but we may need to do some when called back from
3053
inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *)
3054
let concl = if not allowred then pf_concl gl
3055
else whd_betadeltaiota (pf_env gl) (project gl) (pf_concl gl)
3057
match match_with_equation concl with
3059
| Some (hdcncl,args) -> Some (fun gl ->
3060
let hdcncls = string_of_inductive hdcncl in
3063
apply_list [(pf_parse_const gl ("trans_"^hdcncls));t] gl
3065
let eq1, eq2 = match args with
3066
| [typ1;c1;typ2;c2] -> let typt = pf_type_of gl t in
3067
( mkApp(hdcncl, [| typ1; c1; typt ;t |]),
3068
mkApp(hdcncl, [| typt; t; typ2; c2 |]) )
3070
( mkApp (hdcncl, [| typ; c1; t |]),
3071
mkApp (hdcncl, [| typ; t; c2 |]) )
3073
( mkApp (hdcncl, [| c1; t|]),
3074
mkApp (hdcncl, [| t; c2 |]) )
3077
tclTHENFIRST (cut eq2)
3078
(tclTHENFIRST (cut eq1)
3081
tclLAST_HYP simplest_case;
3085
let transitivity t gl =
3086
match transitivity_red false t gl with
3087
| None -> !setoid_transitivity t gl
3088
| Some tac -> tac gl
3090
let intros_transitivity n = tclTHEN intros (transitivity n)
3092
(* tactical to save as name a subproof such that the generalisation of
3093
the current goal, abstracted with respect to the local signature,
3096
let interpretable_as_section_decl d1 d2 = match d1,d2 with
3097
| (_,Some _,_), (_,None,_) -> false
3098
| (_,Some b1,t1), (_,Some b2,t2) -> eq_constr b1 b2 & eq_constr t1 t2
3099
| (_,None,t1), (_,_,t2) -> eq_constr t1 t2
3101
let abstract_subproof name tac gl =
3102
let current_sign = Global.named_context()
3103
and global_sign = pf_hyps gl in
3106
(fun (id,_,_ as d) (s1,s2) ->
3107
if mem_named_context id current_sign &
3108
interpretable_as_section_decl (Sign.lookup_named id current_sign) d
3109
then (s1,push_named_context_val d s2)
3110
else (add_named_decl d s1,s2))
3111
global_sign (empty_named_context,empty_named_context_val) in
3112
let na = next_global_ident_away false name (pf_ids_of_hyps gl) in
3113
let concl = it_mkNamedProd_or_LetIn (pf_concl gl) sign in
3114
if occur_existential concl then
3115
error "\"abstract\" cannot handle existentials.";
3117
start_proof na (Global, Proof Lemma) secsign concl (fun _ _ -> ());
3118
let _,(const,_,kind,_) =
3120
by (tclCOMPLETE (tclTHEN (tclDO (List.length sign) intro) tac));
3121
let r = cook_proof ignore in
3122
delete_current_proof (); r
3125
(delete_current_proof(); raise e)
3126
in (* Faudrait un peu fonctionnaliser cela *)
3127
let cd = Entries.DefinitionEntry const in
3128
let con = Declare.declare_internal_constant na (cd,IsProof Lemma) in
3129
constr_of_global (ConstRef con)
3133
List.rev (Array.to_list (instance_from_named_context sign))))
3136
let tclABSTRACT name_op tac gl =
3137
let s = match name_op with
3139
| None -> add_suffix (get_current_proof_name ()) "_subproof"
3141
abstract_subproof s tac gl
3144
let admit_as_an_axiom gl =
3145
let current_sign = Global.named_context()
3146
and global_sign = pf_hyps gl in
3149
(fun (id,_,_ as d) (s1,s2) ->
3150
if mem_named_context id current_sign &
3151
interpretable_as_section_decl (Sign.lookup_named id current_sign) d
3152
then (s1,add_named_decl d s2)
3153
else (add_named_decl d s1,s2))
3154
global_sign (empty_named_context,empty_named_context) in
3155
let name = add_suffix (get_current_proof_name ()) "_admitted" in
3156
let na = next_global_ident_away false name (pf_ids_of_hyps gl) in
3157
let concl = it_mkNamedProd_or_LetIn (pf_concl gl) sign in
3158
if occur_existential concl then error"\"admit\" cannot handle existentials.";
3160
let cd = Entries.ParameterEntry (concl,false) in
3161
let con = Declare.declare_internal_constant na (cd,IsAssumption Logical) in
3162
constr_of_global (ConstRef con)
3166
List.rev (Array.to_list (instance_from_named_context sign))))
3169
let unify ?(state=full_transparent_state) x y gl =
3172
{default_unify_flags with
3173
modulo_delta = state;
3174
modulo_conv_on_closed_terms = Some state}
3176
let evd = w_unify false (pf_env gl) Reduction.CONV
3177
~flags x y (Evd.create_evar_defs (project gl))
3178
in tclEVARS (Evd.evars_of evd) gl
3179
with _ -> tclFAIL 0 (str"Not unifiable") gl
added
removed
tactics/tactics.ml
