10
let is_rec_info scheme_info =
11
let test_branche min acc (_,_,br) =
14
Sign.it_mkProd_or_LetIn mkProp (fst (Sign.decompose_prod_assum br)) in
15
let free_rels_in_br = Termops.free_rels new_branche in
16
let max = min + scheme_info.Tactics.npredicates in
17
Util.Intset.exists (fun i -> i >= min && i< max) free_rels_in_br
20
Util.list_fold_left_i test_branche 1 false (List.rev scheme_info.Tactics.branches)
23
let choose_dest_or_ind scheme_info =
24
if is_rec_info scheme_info
25
then Tactics.new_induct false
26
else Tactics.new_destruct false
29
let functional_induction with_clean c princl pat =
30
let f,args = decompose_app c in
32
let princ,bindings, princ_type =
34
| None -> (* No principle is given let's find the good one *)
36
match kind_of_term f with
39
let finfo = (* we first try to find out a graph on f *)
40
try find_Function_infos c'
42
errorlabstrm "" (str "Cannot find induction information on "++
43
Printer.pr_lconstr (mkConst c') )
45
match Tacticals.elimination_sort_of_goal g with
46
| InProp -> finfo.prop_lemma
47
| InSet -> finfo.rec_lemma
48
| InType -> finfo.rect_lemma
50
let princ = (* then we get the principle *)
51
try mkConst (Option.get princ_option )
53
(*i If there is not default lemma defined then,
54
we cross our finger and try to find a lemma named f_ind
55
(or f_rec, f_rect) i*)
57
Indrec.make_elimination_ident
58
(id_of_label (con_label c'))
59
(Tacticals.elimination_sort_of_goal g)
62
mkConst(const_of_id princ_name )
63
with Not_found -> (* This one is neither defined ! *)
64
errorlabstrm "" (str "Cannot find induction principle for "
65
++Printer.pr_lconstr (mkConst c') )
67
(princ,Rawterm.NoBindings, Tacmach.pf_type_of g princ)
68
| _ -> raise (UserError("",str "functional induction must be used with a function" ))
71
| Some ((princ,binding)) ->
72
princ,binding,Tacmach.pf_type_of g princ
74
let princ_infos = Tactics.compute_elim_sig princ_type in
75
let args_as_induction_constr =
77
if princ_infos.Tactics.farg_in_concl
80
List.map (fun c -> Tacexpr.ElimOnConstr (c,NoBindings)) (args@c_list)
82
let princ' = Some (princ,bindings) in
86
try Idset.add (destVar a) acc
92
let old_idl = List.fold_right Idset.add (Tacmach.pf_ids_of_hyps g) Idset.empty in
93
let old_idl = Idset.diff old_idl princ_vars in
94
let subst_and_reduce g =
100
if Idset.mem id old_idl then failwith "subst_and_reduce";
103
(Tacmach.pf_ids_of_hyps g)
108
with Rawterm.rDelta = false;
112
(Tacticals.tclMAP (fun id -> Tacticals.tclTRY (Equality.subst [id])) idl )
113
(Hiddentac.h_reduce flag Tacticals.allClauses)
115
else Tacticals.tclIDTAC g
121
args_as_induction_constr
133
| Wf of Topconstr.constr_expr * identifier option * Topconstr.constr_expr list
134
| Mes of Topconstr.constr_expr * identifier option * Topconstr.constr_expr list
137
type newfixpoint_expr =
138
identifier * annot * Topconstr.local_binder list * Topconstr.constr_expr * Topconstr.constr_expr
140
let rec abstract_rawconstr c = function
142
| Topconstr.LocalRawDef (x,b)::bl -> Topconstr.mkLetInC(x,b,abstract_rawconstr c bl)
143
| Topconstr.LocalRawAssum (idl,k,t)::bl ->
144
List.fold_right (fun x b -> Topconstr.mkLambdaC([x],k,t,b)) idl
145
(abstract_rawconstr c bl)
147
let interp_casted_constr_with_implicits sigma env impls c =
148
(* Constrintern.interp_rawconstr_with_implicits sigma env [] impls c *)
149
Constrintern.intern_gen false sigma env ~impls:([],impls)
150
~allow_patvar:false ~ltacvars:([],[]) c
154
Construct a fixpoint as a Rawterm
157
let build_newrecursive
159
let env0 = Global.env()
160
and sigma = Evd.empty
162
let (rec_sign,rec_impls) =
164
(fun (env,impls) ((_,recname),_,bl,arityc,_) ->
165
let arityc = Command.generalize_constr_expr arityc bl in
166
let arity = Constrintern.interp_type sigma env0 arityc in
168
if Impargs.is_implicit_args()
169
then Impargs.compute_implicits env0 arity
171
let impls' =(recname,(Constrintern.Recursive,[],impl,Notation.compute_arguments_scope arity))::impls in
172
(Environ.push_named (recname,None,arity) env, impls'))
173
(env0,[]) lnameargsardef in
175
(* Declare local notations *)
176
let fs = States.freeze() in
180
(fun (_,_,bl,_,def) ->
181
let def = abstract_rawconstr def bl in
182
interp_casted_constr_with_implicits
183
sigma rec_sign rec_impls def
187
States.unfreeze fs; raise e in
188
States.unfreeze fs; def
193
let compute_annot (name,annot,args,types,body) =
194
let names = List.map snd (Topconstr.names_of_local_assums args) in
197
if List.length names > 1 then
199
(dummy_loc,"Function",
200
Pp.str "the recursive argument needs to be specified");
201
let new_annot = (id_of_name (List.hd names)) in
202
(name,Struct new_annot,args,types,body)
203
| Some r -> (name,r,args,types,body)
206
(* Checks whether or not the mutual bloc is recursive *)
207
let rec is_rec names =
208
let names = List.fold_right Idset.add names Idset.empty in
209
let check_id id names = Idset.mem id names in
210
let rec lookup names = function
211
| RVar(_,id) -> check_id id names
212
| RRef _ | REvar _ | RPatVar _ | RSort _ | RHole _ | RDynamic _ -> false
213
| RCast(_,b,_) -> lookup names b
214
| RRec _ -> error "RRec not handled"
215
| RIf(_,b,_,lhs,rhs) ->
216
(lookup names b) || (lookup names lhs) || (lookup names rhs)
217
| RLetIn(_,na,t,b) | RLambda(_,na,_,t,b) | RProd(_,na,_,t,b) ->
218
lookup names t || lookup (Nameops.name_fold Idset.remove na names) b
219
| RLetTuple(_,nal,_,t,b) -> lookup names t ||
222
(fun acc na -> Nameops.name_fold Idset.remove na acc)
227
| RApp(_,f,args) -> List.exists (lookup names) (f::args)
228
| RCases(_,_,_,el,brl) ->
229
List.exists (fun (e,_) -> lookup names e) el ||
230
List.exists (lookup_br names) brl
231
and lookup_br names (_,idl,_,rt) =
232
let new_names = List.fold_right Idset.remove idl names in
237
let prepare_body (name,annot,args,types,body) rt =
238
let n = (Topconstr.local_binders_length args) in
239
(* Pp.msgnl (str "nb lambda to chop : " ++ str (string_of_int n) ++ fnl () ++Printer.pr_rawconstr rt); *)
240
let fun_args,rt' = chop_rlambda_n n rt in
244
let derive_inversion fix_names =
246
(* we first transform the fix_names identifier into their corresponding constant *)
247
let fix_names_as_constant =
248
List.map (fun id -> destConst (Tacinterp.constr_of_id (Global.env ()) id)) fix_names
251
Then we check that the graphs have been defined
252
If one of the graphs haven't been defined
255
List.iter (fun c -> ignore (find_Function_infos c)) fix_names_as_constant ;
257
Invfun.derive_correctness
258
Functional_principles_types.make_scheme
260
fix_names_as_constant
261
(*i The next call to mk_rel_id is valid since we have just construct the graph
262
Ensures by : register_built
265
(fun id -> destInd (Tacinterp.constr_of_id (Global.env ()) (mk_rel_id id)))
270
(str "Cannot built inversion information" ++
271
if do_observe () then Cerrors.explain_exn e else mt ())
274
let warning_error names e =
276
| Building_graph e ->
278
(str "Cannot define graph(s) for " ++
279
h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++
280
if do_observe () then (spc () ++ Cerrors.explain_exn e) else mt ())
281
| Defining_principle e ->
283
(str "Cannot define principle(s) for "++
284
h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++
285
if do_observe () then Cerrors.explain_exn e else mt ())
288
let error_error names e =
290
| Building_graph e ->
292
(str "Cannot define graph(s) for " ++
293
h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++
294
if do_observe () then (spc () ++ Cerrors.explain_exn e) else mt ())
297
let generate_principle on_error
298
is_general do_built fix_rec_l recdefs interactive_proof
299
(continue_proof : int -> Names.constant array -> Term.constr array -> int ->
300
Tacmach.tactic) : unit =
301
let names = List.map (function ((_, name),_,_,_,_) -> name) fix_rec_l in
302
let fun_bodies = List.map2 prepare_body fix_rec_l recdefs in
303
let funs_args = List.map fst fun_bodies in
304
let funs_types = List.map (function (_,_,_,types,_) -> types) fix_rec_l in
306
(* We then register the Inductive graphs of the functions *)
307
Rawterm_to_relation.build_inductive names funs_args funs_types recdefs;
311
(*i The next call to mk_rel_id is valid since we have just construct the graph
312
Ensures by : do_built
314
let f_R_mut = Ident (dummy_loc,mk_rel_id (List.nth names 0)) in
317
(pr_reference f_R_mut++str ": Not an inductive type!")
321
let fname_kn (fname,_,_,_,_) =
322
let f_ref = Ident fname in
324
(pr_reference f_ref++str ": Not an inductive type!")
328
let funs_kn = Array.of_list (List.map fname_kn fix_rec_l) in
332
let princ = destConst (Indrec.lookup_eliminator (ind_kn,i) (InProp)) in
333
let princ_type = Typeops.type_of_constant (Global.env()) princ
335
Functional_principles_types.generate_functional_principle
342
(continue_proof 0 [|funs_kn.(i)|])
347
Array.iter (add_Function is_general) funs_kn;
353
let register_struct is_rec fixpoint_exprl =
354
match fixpoint_exprl with
355
| [((_,fname),_,bl,ret_type,body),_] when not is_rec ->
356
Command.declare_definition
358
(Decl_kinds.Global,Flags.boxed_definitions (),Decl_kinds.Definition)
365
Command.build_recursive fixpoint_exprl (Flags.boxed_definitions())
367
let generate_correction_proof_wf f_ref tcc_lemma_ref
368
is_mes functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation
369
(_: int) (_:Names.constant array) (_:Term.constr array) (_:int) : Tacmach.tactic =
370
Functional_principles_proofs.prove_principle_for_gen
371
(f_ref,functional_ref,eq_ref)
372
tcc_lemma_ref is_mes rec_arg_num rec_arg_type relation
375
let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas args ret_type body
378
let type_of_f = Command.generalize_constr_expr ret_type args in
383
(Topconstr.names_of_local_assums args)
387
if List.length names = 1 then 1
388
else error "Recursive argument must be specified"
390
list_index (Name wf_arg) names
396
(None,(Ident (dummy_loc,fname))) ,
399
| _,Anonymous -> assert false
400
| _,Name e -> (Topconstr.mkIdentC e)
402
(Topconstr.names_of_local_assums args)
406
Topconstr.CApp (dummy_loc,(None,Topconstr.mkRefC (Qualid (dummy_loc,(qualid_of_string "Logic.eq")))),
407
[(f_app_args,None);(body,None)])
409
let eq = Command.generalize_constr_expr unbounded_eq args in
410
let hook f_ref tcc_lemma_ref functional_ref eq_ref rec_arg_num rec_arg_type
414
(generate_correction_proof_wf f_ref tcc_lemma_ref is_mes
415
functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation
417
derive_inversion [fname]
422
Recdef.recursive_definition
423
is_mes fname rec_impls
432
let register_mes fname rec_impls wf_mes_expr wf_arg using_lemmas args ret_type body =
433
let wf_arg_type,wf_arg =
438
| [Topconstr.LocalRawAssum ([(_,Name x)],k,t)] -> t,x
439
| _ -> error "Recursive argument must be specified"
446
| Topconstr.LocalRawAssum(l,k,t) ->
448
(function (_,Name id) -> id = wf_args | _ -> false)
454
| Topconstr.LocalRawAssum(_,k,t) -> t,wf_args
456
with Not_found -> assert false
459
let make_dir l = make_dirpath (List.map id_of_string (List.rev l)) in
460
Libnames.Qualid (dummy_loc,Libnames.qualid_of_sp
461
(Libnames.make_path (make_dir ["Arith";"Wf_nat"]) (id_of_string "ltof")))
465
Topconstr.mkAppC(wf_mes_expr,[Topconstr.mkIdentC wf_arg]) in
466
Topconstr.mkLambdaC ([(dummy_loc,Name wf_arg)],Topconstr.default_binder_kind,wf_arg_type,applied_mes)
468
let wf_rel_from_mes =
469
Topconstr.mkAppC(Topconstr.mkRefC ltof,[wf_arg_type;fun_from_mes])
471
register_wf ~is_mes:true fname rec_impls wf_rel_from_mes (Some wf_arg)
472
using_lemmas args ret_type body
475
let do_generate_principle on_error register_built interactive_proof fixpoint_exprl =
476
let recdefs,rec_impls = build_newrecursive fixpoint_exprl in
478
match fixpoint_exprl with
479
| [(((_,name),Some (Wf (wf_rel,wf_x,using_lemmas)),args,types,body))] ->
490
then register_wf name rec_impls wf_rel wf_x using_lemmas args types body pre_hook;
492
| [(((_,name),Some (Mes (wf_mes,wf_x,using_lemmas)),args,types,body))] ->
503
then register_mes name rec_impls wf_mes wf_x using_lemmas args types body pre_hook;
507
List.map (function ((_,name),_,_,_,_) -> name) fixpoint_exprl
509
let is_one_rec = is_rec fix_names in
510
let old_fixpoint_exprl =
513
| (name,Some (Struct id),args,types,body),_ ->
515
try Some (dummy_loc, id), Topconstr.CStructRec
517
raise (UserError("",str "Cannot find argument " ++
520
(name,annot,args,types,body),(None:Vernacexpr.decl_notation)
521
| (name,None,args,types,body),recdef ->
522
let names = (Topconstr.names_of_local_assums args) in
523
if is_one_rec recdef && List.length names > 1 then
525
(dummy_loc,"Function",
526
Pp.str "the recursive argument needs to be specified in Function")
528
let loc, na = List.hd names in
529
(name,(Some (loc, Nameops.out_name na), Topconstr.CStructRec),args,types,body),
530
(None:Vernacexpr.decl_notation)
531
| (_,Some (Wf _),_,_,_),_ | (_,Some (Mes _),_,_,_),_->
533
("Cannot use mutual definition with well-founded recursion or measure")
535
(List.combine fixpoint_exprl recdefs)
537
(* ok all the expressions are structural *)
539
List.map (function ((_,name),_,_,_,_) -> name) fixpoint_exprl
541
let is_rec = List.exists (is_rec fix_names) recdefs in
542
if register_built then register_struct is_rec old_fixpoint_exprl;
550
(Functional_principles_proofs.prove_princ_for_struct interactive_proof);
551
if register_built then derive_inversion fix_names;
557
let rec add_args id new_args b =
561
| Libnames.Ident(loc,fname) when fname = id ->
562
CAppExpl(dummy_loc,(None,r),new_args)
565
| CFix _ | CCoFix _ -> anomaly "add_args : todo"
566
| CArrow(loc,b1,b2) ->
567
CArrow(loc,add_args id new_args b1, add_args id new_args b2)
568
| CProdN(loc,nal,b1) ->
570
List.map (fun (nal,k,b2) -> (nal,k,add_args id new_args b2)) nal,
571
add_args id new_args b1)
572
| CLambdaN(loc,nal,b1) ->
574
List.map (fun (nal,k,b2) -> (nal,k,add_args id new_args b2)) nal,
575
add_args id new_args b1)
576
| CLetIn(loc,na,b1,b2) ->
577
CLetIn(loc,na,add_args id new_args b1,add_args id new_args b2)
578
| CAppExpl(loc,(pf,r),exprl) ->
581
| Libnames.Ident(loc,fname) when fname = id ->
582
CAppExpl(loc,(pf,r),new_args@(List.map (add_args id new_args) exprl))
583
| _ -> CAppExpl(loc,(pf,r),List.map (add_args id new_args) exprl)
585
| CApp(loc,(pf,b),bl) ->
586
CApp(loc,(pf,add_args id new_args b),
587
List.map (fun (e,o) -> add_args id new_args e,o) bl)
588
| CCases(loc,sty,b_option,cel,cal) ->
589
CCases(loc,sty,Option.map (add_args id new_args) b_option,
590
List.map (fun (b,(na,b_option)) ->
591
add_args id new_args b,
592
(na,Option.map (add_args id new_args) b_option)) cel,
593
List.map (fun (loc,cpl,e) -> (loc,cpl,add_args id new_args e)) cal
595
| CLetTuple(loc,nal,(na,b_option),b1,b2) ->
596
CLetTuple(loc,nal,(na,Option.map (add_args id new_args) b_option),
597
add_args id new_args b1,
598
add_args id new_args b2
601
| CIf(loc,b1,(na,b_option),b2,b3) ->
602
CIf(loc,add_args id new_args b1,
603
(na,Option.map (add_args id new_args) b_option),
604
add_args id new_args b2,
605
add_args id new_args b3
611
| CCast(loc,b1,CastConv(ck,b2)) ->
612
CCast(loc,add_args id new_args b1,CastConv(ck,add_args id new_args b2))
613
| CCast(loc,b1,CastCoerce) ->
614
CCast(loc,add_args id new_args b1,CastCoerce)
615
| CRecord _ -> anomaly "add_args : CRecord"
616
| CNotation _ -> anomaly "add_args : CNotation"
617
| CGeneralization _ -> anomaly "add_args : CGeneralization"
619
| CDelimiters _ -> anomaly "add_args : CDelimiters"
620
| CDynamic _ -> anomaly "add_args : CDynamic"
621
exception Stop of Topconstr.constr_expr
624
(* [chop_n_arrow n t] chops the [n] first arrows in [t]
625
Acts on Topconstr.constr_expr
627
let rec chop_n_arrow n t =
629
then t (* If we have already removed all the arrows then return the type *)
630
else (* If not we check the form of [t] *)
632
| Topconstr.CArrow(_,_,t) -> (* If we have an arrow, we discard it and recall [chop_n_arrow] *)
634
| Topconstr.CProdN(_,nal_ta',t') -> (* If we have a forall, to result are possible :
635
either we need to discard more than the number of arrows contained
636
in this product declaration then we just recall [chop_n_arrow] on
637
the remaining number of arrow to chop and [t'] we discard it and
638
recall [chop_n_arrow], either this product contains more arrows
639
than the number we need to chop and then we return the new type
644
let rec aux (n:int) = function
646
| (nal,k,t'')::nal_ta' ->
647
let nal_l = List.length nal in
650
aux (n - nal_l) nal_ta'
653
Topconstr.CProdN(dummy_loc,
654
((snd (list_chop n nal)),k,t'')::nal_ta',t')
660
chop_n_arrow new_n t'
663
| _ -> anomaly "Not enough products"
666
let rec get_args b t : Topconstr.local_binder list *
667
Topconstr.constr_expr * Topconstr.constr_expr =
669
| Topconstr.CLambdaN (loc, (nal_ta), b') ->
672
(List.fold_left (fun n (nal,_,_) ->
673
n+List.length nal) 0 nal_ta )
675
let nal_tas,b'',t'' = get_args b' (chop_n_arrow n t) in
676
(List.map (fun (nal,k,ta) ->
677
(Topconstr.LocalRawAssum (nal,k,ta))) nal_ta)@nal_tas, b'',t''
682
let make_graph (f_ref:global_reference) =
686
begin try c,Global.lookup_constant c
688
raise (UserError ("",str "Cannot find " ++ Printer.pr_lconstr (mkConst c)) )
690
| _ -> raise (UserError ("", str "Not a function reference") )
693
match c_body.const_body with
694
| None -> error "Cannot build a graph over an axiom !"
696
let env = Global.env () in
697
let body = (force b) in
698
let extern_body,extern_type =
701
(Constrextern.extern_constr false env body,
702
Constrextern.extern_type false env
703
(Typeops.type_of_constant_type env c_body.const_type)
708
let (nal_tas,b,t) = get_args extern_body extern_type in
711
| Topconstr.CFix(loc,l_id,fixexprl) ->
714
(fun (id,(n,recexp),bl,t,b) ->
715
let loc, rec_id = Option.get n in
720
| Topconstr.LocalRawDef (na,_)-> []
721
| Topconstr.LocalRawAssum (nal,_,_) ->
724
CRef(Libnames.Ident(loc, Nameops.out_name n)))
730
let b' = add_args (snd id) new_args b in
731
(id, Some (Struct rec_id),nal_tas@bl,t,b')
737
let id = id_of_label (con_label c) in
738
[((dummy_loc,id),None,nal_tas,t,b)]
740
do_generate_principle error_error false false expr_list;
741
(* We register the infos *)
742
let mp,dp,_ = repr_con c in
744
(fun ((_,id),_,_,_,_) -> add_Function false (make_con mp dp (label_of_id id)))
748
(* let make_graph _ = assert false *)
750
let do_generate_principle = do_generate_principle warning_error true
added
removed
contrib/funind/indfun.ml
