28
then begin Pp.msg strm;Pp.pp_flush () end
34
let do_observe_tac s tac g =
35
try let v = tac g in (* msgnl (goal ++ fnl () ++ (str s)++(str " ")++(str "finished")); *) v
37
let goal = begin try (Printer.pr_goal (sig_it g)) with _ -> assert false end in
38
msgnl (str "observation "++ s++str " raised exception " ++
39
Cerrors.explain_exn e ++ str " on goal " ++ goal );
42
let observe_tac_stream s tac g =
44
then do_observe_tac s tac g
47
let observe_tac s tac g = observe_tac_stream (str s) tac g
49
(* let tclTRYD tac = *)
50
(* if !Flags.debug || do_observe () *)
51
(* then (fun g -> try (\* do_observe_tac "" *\)tac g with _ -> tclIDTAC g) *)
55
let list_chop ?(msg="") n l =
58
with Failure (msg') ->
62
let make_refl_eq type_of_t t =
63
let refl_equal_term = Lazy.force refl_equal in
64
mkApp(refl_equal_term,[|type_of_t;t|])
69
proving_tac : (identifier list -> Tacmach.tactic);
70
is_valid : constr -> bool
73
type ptes_info = pte_info Idmap.t
75
type 'a dynamic_info =
78
rec_hyps : identifier list ;
79
eq_hyps : identifier list;
83
type body_info = constr dynamic_info
86
let finish_proof dynamic_infos g =
93
Tacmach.refine_no_check c
96
Tacmach.thin_no_check l
99
let cut_replacing id t tac :tactic=
101
[ tclTHEN (thin_no_check [id]) (introduction_no_check id);
105
let intro_erasing id = tclTHEN (thin [id]) (introduction id)
109
let rec_hyp_id = id_of_string "rec_hyp"
111
let is_trivial_eq t =
112
match kind_of_term t with
113
| App(f,[|_;t1;t2|]) when eq_constr f (Lazy.force eq) ->
118
let rec incompatible_constructor_terms t1 t2 =
119
let c1,arg1 = decompose_app t1
120
and c2,arg2 = decompose_app t2
122
(not (eq_constr t1 t2)) &&
123
isConstruct c1 && isConstruct c2 &&
125
not (eq_constr c1 c2) ||
126
List.exists2 incompatible_constructor_terms arg1 arg2
129
let is_incompatible_eq t =
130
match kind_of_term t with
131
| App(f,[|_;t1;t2|]) when eq_constr f (Lazy.force eq) ->
132
incompatible_constructor_terms t1 t2
135
let change_hyp_with_using msg hyp_id t tac : tactic =
137
let prov_id = pf_get_new_id hyp_id g in
139
((* observe_tac msg *) (assert_by (Name prov_id) t (tclCOMPLETE tac)))
142
(* observe_tac "change_hyp_with_using thin" *) (thin [hyp_id]);
143
(* observe_tac "change_hyp_with_using rename " *) (h_rename [prov_id,hyp_id])
149
let prove_trivial_eq h_id context (type_of_term,term) =
150
let nb_intros = List.length context in
153
tclDO nb_intros intro; (* introducing context *)
156
fst (list_chop ~msg:"prove_trivial_eq : " nb_intros (pf_ids_of_hyps g))
159
(mkApp(Lazy.force refl_equal,[|type_of_term;term|]))::
160
(List.map mkVar context_hyps)
162
let to_refine = applist(mkVar h_id,List.rev context_hyps') in
168
let isAppConstruct t =
170
then isConstruct (fst (destApp t))
173
let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta *)
174
let clos_norm_flags flgs env sigma t =
175
Closure.norm_val (Closure.create_clos_infos flgs env) (Closure.inject (Reductionops.nf_evar sigma t)) in
176
clos_norm_flags Closure.betaiotazeta Environ.empty_env Evd.empty
179
let change_eq env sigma hyp_id (context:Sign.rel_context) x t end_of_type =
182
(* observe (str ("Not treating ( "^msg^" )") ++ pr_lconstr t ); *)
186
let eq_constr = Reductionops.is_conv env sigma in
187
if not (noccurn 1 end_of_type)
188
then nochange "dependent"; (* if end_of_type depends on this term we don't touch it *)
189
if not (isApp t) then nochange "not an equality";
190
let f_eq,args = destApp t in
191
if not (eq_constr f_eq (Lazy.force eq)) then nochange "not an equality";
194
and t1_typ = args.(0)
196
if not (closed0 t1) then nochange "not a closed lhs";
197
let rec compute_substitution sub t1 t2 =
198
(* observe (str "compute_substitution : " ++ pr_lconstr t1 ++ str " === " ++ pr_lconstr t2); *)
201
let t2 = destRel t2 in
204
let t1' = Intmap.find t2 sub in
205
if not (eq_constr t1 t1') then nochange "twice bound variable";
211
else if isAppConstruct t1 && isAppConstruct t2
214
let c1,args1 = destApp t1
215
and c2,args2 = destApp t2
217
if not (eq_constr c1 c2) then anomaly "deconstructing equation";
218
array_fold_left2 compute_substitution sub args1 args2
221
if (eq_constr t1 t2) then sub else nochange "cannot solve"
223
let sub = compute_substitution Intmap.empty t1 t2 in
224
let end_of_type_with_pop = pop end_of_type in (*the equation will be removed *)
225
let new_end_of_type =
226
(* Ugly hack to prevent Map.fold order change between ocaml-3.08.3 and ocaml-3.08.4
227
Can be safely replaced by the next comment for Ocaml >= 3.08.4
229
let sub' = Intmap.fold (fun i t acc -> (i,t)::acc) sub [] in
230
let sub'' = List.sort (fun (x,_) (y,_) -> Pervasives.compare x y) sub' in
231
List.fold_left (fun end_of_type (i,t) -> lift 1 (substnl [t] (i-1) end_of_type))
235
let old_context_length = List.length context + 1 in
237
mkLetIn(Anonymous,make_refl_eq t1_typ t1,t,
238
mkApp(mkVar hyp_id,Array.init old_context_length (fun i -> mkRel (old_context_length - i)))
241
let new_type_of_hyp,ctxt_size,witness_fun =
243
(fun i (end_of_type,ctxt_size,witness_fun) ((x',b',t') as decl) ->
245
let witness = Intmap.find i sub in
246
if b' <> None then anomaly "can not redefine a rel!";
247
(pop end_of_type,ctxt_size,mkLetIn(x',witness,t',witness_fun))
249
(mkProd_or_LetIn decl end_of_type, ctxt_size + 1, mkLambda_or_LetIn decl witness_fun)
252
(new_end_of_type,0,witness_fun)
255
let new_type_of_hyp =
256
Reductionops.nf_betaiota Evd.empty new_type_of_hyp in
257
let new_ctxt,new_end_of_type =
258
Sign.decompose_prod_n_assum ctxt_size new_type_of_hyp
260
let prove_new_hyp : tactic =
262
(tclDO ctxt_size intro)
264
let all_ids = pf_ids_of_hyps g in
265
let new_ids,_ = list_chop ctxt_size all_ids in
266
let to_refine = applist(witness_fun,List.rev_map mkVar new_ids) in
271
change_hyp_with_using "prove_pattern_simplification" hyp_id new_type_of_hyp prove_new_hyp
273
(* observe (str "In " ++ Ppconstr.pr_id hyp_id ++ *)
274
(* str "removing an equation " ++ fnl ()++ *)
275
(* str "old_typ_of_hyp :=" ++ *)
276
(* Printer.pr_lconstr_env *)
278
(* (it_mkProd_or_LetIn ~init:end_of_type ((x,None,t)::context)) *)
280
(* str "new_typ_of_hyp := "++ *)
281
(* Printer.pr_lconstr_env env new_type_of_hyp ++ fnl () *)
282
(* ++ str "old context := " ++ pr_rel_context env context ++ fnl () *)
283
(* ++ str "new context := " ++ pr_rel_context env new_ctxt ++ fnl () *)
284
(* ++ str "old type := " ++ pr_lconstr end_of_type ++ fnl () *)
285
(* ++ str "new type := " ++ pr_lconstr new_end_of_type ++ fnl () *)
287
new_ctxt,new_end_of_type,simpl_eq_tac
290
let is_property ptes_info t_x full_type_of_hyp =
293
let pte,args = destApp t_x in
294
if isVar pte && array_for_all closed0 args
297
let info = Idmap.find (destVar pte) ptes_info in
298
info.is_valid full_type_of_hyp
299
with Not_found -> false
304
match kind_of_term t with
309
let h_reduce_with_zeta =
313
with Rawterm.rDelta = false;
318
let rewrite_until_var arg_num eq_ids : tactic =
319
(* tests if the declares recursive argument is neither a Constructor nor
320
an applied Constructor since such a form for the recursive argument
321
will break the Guard when trying to save the Lemma.
324
let _,args = destApp (pf_concl g) in
325
not ((isConstruct args.(arg_num)) || isAppConstruct args.(arg_num))
327
let rec do_rewrite eq_ids g =
332
| [] -> anomaly "Cannot find a way to prove recursive property";
335
(tclTRY (Equality.rewriteRL (mkVar eq_id)))
342
let rec_pte_id = id_of_string "Hrec"
343
let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
344
let coq_False = Coqlib.build_coq_False () in
345
let coq_True = Coqlib.build_coq_True () in
346
let coq_I = Coqlib.build_coq_I () in
347
let rec scan_type context type_of_hyp : tactic =
348
if isLetIn type_of_hyp then
349
let real_type_of_hyp = it_mkProd_or_LetIn ~init:type_of_hyp context in
350
let reduced_type_of_hyp = nf_betaiotazeta real_type_of_hyp in
351
(* length of context didn't change ? *)
352
let new_context,new_typ_of_hyp =
353
Sign.decompose_prod_n_assum (List.length context) reduced_type_of_hyp
358
(Tacticals.onHyp hyp_id)
360
scan_type new_context new_typ_of_hyp
363
else if isProd type_of_hyp
366
let (x,t_x,t') = destProd type_of_hyp in
367
let actual_real_type_of_hyp = it_mkProd_or_LetIn ~init:t' context in
368
if is_property ptes_infos t_x actual_real_type_of_hyp then
370
let pte,pte_args = (destApp t_x) in
371
let (* fix_info *) prove_rec_hyp = (Idmap.find (destVar pte) ptes_infos).proving_tac in
372
let popped_t' = pop t' in
373
let real_type_of_hyp = it_mkProd_or_LetIn ~init:popped_t' context in
374
let prove_new_type_of_hyp =
375
let context_length = List.length context in
378
tclDO context_length intro;
380
let context_hyps_ids =
381
fst (list_chop ~msg:"rec hyp : context_hyps"
382
context_length (pf_ids_of_hyps g))
384
let rec_pte_id = pf_get_new_id rec_pte_id g in
386
applist(mkVar hyp_id,
387
List.rev_map mkVar (rec_pte_id::context_hyps_ids)
390
(* observe_tac "rec hyp " *)
392
(assert_tac (Name rec_pte_id) t_x)
394
(* observe_tac "prove rec hyp" *) (prove_rec_hyp eq_hyps);
395
(* observe_tac "prove rec hyp" *)
404
(* observe_tac "hyp rec" *)
405
(change_hyp_with_using "rec_hyp_tac" hyp_id real_type_of_hyp prove_new_type_of_hyp);
406
scan_type context popped_t'
409
else if eq_constr t_x coq_False then
411
(* observe (str "Removing : "++ Ppconstr.pr_id hyp_id++ *)
412
(* str " since it has False in its preconds " *)
414
raise TOREMOVE; (* False -> .. useless *)
416
else if is_incompatible_eq t_x then raise TOREMOVE (* t_x := C1 ... = C2 ... *)
417
else if eq_constr t_x coq_True (* Trivial => we remove this precons *)
419
(* observe (str "In "++Ppconstr.pr_id hyp_id++ *)
420
(* str " removing useless precond True" *)
422
let popped_t' = pop t' in
423
let real_type_of_hyp =
424
it_mkProd_or_LetIn ~init:popped_t' context
427
let nb_intro = List.length context in
429
tclDO nb_intro intro;
432
fst (list_chop ~msg:"removing True : context_hyps "nb_intro (pf_ids_of_hyps g))
435
applist (mkVar hyp_id,
436
List.rev (coq_I::List.map mkVar context_hyps)
444
change_hyp_with_using "prove_trivial" hyp_id real_type_of_hyp
445
((* observe_tac "prove_trivial" *) prove_trivial);
446
scan_type context popped_t'
448
else if is_trivial_eq t_x
449
then (* t_x := t = t => we remove this precond *)
450
let popped_t' = pop t' in
451
let real_type_of_hyp =
452
it_mkProd_or_LetIn ~init:popped_t' context
454
let _,args = destApp t_x in
457
change_hyp_with_using
461
((* observe_tac "prove_trivial_eq" *) (prove_trivial_eq hyp_id context (args.(0),args.(1))));
462
scan_type context popped_t'
467
let new_context,new_t',tac = change_eq env sigma hyp_id context x t_x t' in
470
(scan_type new_context new_t')
471
with Failure "NoChange" ->
472
(* Last thing todo : push the rel in the context and continue *)
473
scan_type ((x,None,t_x)::context) t'
480
scan_type [] (Typing.type_of env sigma (mkVar hyp_id)), [hyp_id]
485
let clean_goal_with_heq ptes_infos continue_tac dyn_infos =
488
and sigma = project g
492
fun (hyps_tac,new_hyps) hyp_id ->
493
let hyp_tac,new_hyp =
494
clean_hyp_with_heq ptes_infos dyn_infos.eq_hyps hyp_id env sigma
496
(tclTHEN hyp_tac hyps_tac),new_hyp@new_hyps
504
nb_rec_hyps = List.length new_hyps
510
(* observe_tac "clean_hyp_with_heq continue" *) (continue_tac new_infos)
514
let heq_id = id_of_string "Heq"
516
let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos =
518
let heq_id = pf_get_new_id heq_id g in
519
let nb_first_intro = nb_prod - 1 - dyn_infos.nb_rec_hyps in
522
(* We first introduce the variables *)
523
tclDO nb_first_intro (intro_avoiding dyn_infos.rec_hyps);
524
(* Then the equation itself *)
525
introduction_no_check heq_id;
526
(* Then the new hypothesis *)
527
tclMAP introduction_no_check dyn_infos.rec_hyps;
528
(* observe_tac "after_introduction" *)(fun g' ->
529
(* We get infos on the equations introduced*)
530
let new_term_value_eq = pf_type_of g' (mkVar heq_id) in
531
(* compute the new value of the body *)
533
match kind_of_term new_term_value_eq with
534
| App(f,[| _;_;args2 |]) -> args2
536
observe (str "cannot compute new term value : " ++ pr_gls g' ++ fnl () ++ str "last hyp is" ++
537
pr_lconstr_env (pf_env g') new_term_value_eq
539
anomaly "cannot compute new term value"
544
replace_term term (mkRel 1) dyn_infos.info
547
let new_body = pf_nf_betaiota g' (mkApp(fun_body,[| new_term_value |])) in
551
eq_hyps = heq_id::dyn_infos.eq_hyps
554
clean_goal_with_heq ptes_infos continue_tac new_infos g'
560
let my_orelse tac1 tac2 g =
564
(* observe (str "using snd tac since : " ++ Cerrors.explain_exn e); *)
567
let instanciate_hyps_with_args (do_prove:identifier list -> tactic) hyps args_id =
568
let args = Array.of_list (List.map mkVar args_id) in
569
let instanciate_one_hyp hid =
571
( (* we instanciate the hyp if possible *)
573
let prov_hid = pf_get_new_id hid g in
575
pose_proof (Name prov_hid) (mkApp(mkVar hid,args));
577
h_rename [prov_hid,hid]
581
if not then we are in a mutual function block
582
and this hyp is a recursive hyp on an other function.
584
We are not supposed to use it while proving this
585
principle so that we can trash it
589
(* observe (str "Instanciation: removing hyp " ++ Ppconstr.pr_id hid); *)
597
tclMAP (fun hyp_id -> h_reduce_with_zeta (Tacticals.onHyp hyp_id)) hyps;
603
tclMAP (fun hyp_id -> h_reduce_with_zeta (Tacticals.onHyp hyp_id)) hyps;
604
tclMAP instanciate_one_hyp hyps;
607
List.fold_right Idset.add (pf_ids_of_hyps g) Idset.empty
610
List.filter (fun id -> Idset.mem id all_g_hyps_id) hyps
612
do_prove remaining_hyps g
617
(interactive_proof:bool)
618
(fnames:constant list)
622
let rec build_proof_aux do_finalize dyn_infos : tactic =
624
(* observe (str "proving on " ++ Printer.pr_lconstr_env (pf_env g) term);*)
625
match kind_of_term dyn_infos.info with
626
| Case(ci,ct,t,cb) ->
627
let do_finalize_t dyn_info' =
629
let t = dyn_info'.info in
630
let dyn_infos = {dyn_info' with info =
631
mkCase(ci,ct,t,cb)} in
632
let g_nb_prod = nb_prod (pf_concl g) in
633
let type_of_term = pf_type_of g t in
635
make_refl_eq type_of_term t
639
h_generalize (term_eq::(List.map mkVar dyn_infos.rec_hyps));
640
thin dyn_infos.rec_hyps;
641
pattern_option [(false,[1]),t] None;
644
let g'_nb_prod = nb_prod (pf_concl g') in
645
let nb_instanciate_partial = g'_nb_prod - g_nb_prod in
646
observe_tac "treat_new_case"
649
nb_instanciate_partial
650
(build_proof do_finalize)
658
build_proof do_finalize_t {dyn_infos with info = t} g
661
match kind_of_term( pf_concl g) with
666
let (id,_,_) = pf_last_hyp g' in
669
(mkApp(dyn_infos.info,[|mkVar id|]))
671
let new_infos = {dyn_infos with info = new_term} in
672
let do_prove new_hyps =
673
build_proof do_finalize
676
nb_rec_hyps = List.length new_hyps
679
(* observe_tac "Lambda" *) (instanciate_hyps_with_args do_prove new_infos.rec_hyps [id]) g'
680
(* build_proof do_finalize new_infos g' *)
683
do_finalize dyn_infos g
686
build_proof do_finalize {dyn_infos with info = t} g
687
| Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ ->
688
do_finalize dyn_infos g
690
let f,args = decompose_app dyn_infos.info in
692
match kind_of_term f with
693
| App _ -> assert false (* we have collected all the app in decompose_app *)
694
| Var _ | Construct _ | Rel _ | Evar _ | Meta _ | Ind _ | Sort _ | Prod _ ->
700
build_proof_args do_finalize new_infos g
701
| Const c when not (List.mem c fnames) ->
707
(* Pp.msgnl (str "proving in " ++ pr_lconstr_env (pf_env g) dyn_infos.info); *)
708
build_proof_args do_finalize new_infos g
710
do_finalize dyn_infos g
713
Reductionops.nf_beta Evd.empty dyn_infos.info in
714
build_proof do_finalize {dyn_infos with info = new_term}
718
{ dyn_infos with info = nf_betaiotazeta dyn_infos.info }
723
(fun hyp_id -> h_reduce_with_zeta (Tacticals.onHyp hyp_id))
725
h_reduce_with_zeta Tacticals.onConcl;
726
build_proof do_finalize new_infos
730
build_proof do_finalize {dyn_infos with info = b } g
731
| Case _ | Fix _ | CoFix _ ->
732
let new_finalize dyn_infos =
735
info = dyn_infos.info,args
738
build_proof_args do_finalize new_infos
740
build_proof new_finalize {dyn_infos with info = f } g
743
error ( "Anonymous local (co)fixpoints are not handled yet")
745
| Prod _ -> error "Prod"
749
info = nf_betaiotazeta dyn_infos.info
755
(fun hyp_id -> h_reduce_with_zeta (Tacticals.onHyp hyp_id))
757
h_reduce_with_zeta Tacticals.onConcl;
758
build_proof do_finalize new_infos
760
| Rel _ -> anomaly "Free var in goal conclusion !"
761
and build_proof do_finalize dyn_infos g =
762
(* observe (str "proving with "++Printer.pr_lconstr dyn_infos.info++ str " on goal " ++ pr_gls g); *)
763
observe_tac "build_proof" (build_proof_aux do_finalize dyn_infos) g
764
and build_proof_args do_finalize dyn_infos (* f_args' args *) :tactic =
766
let (f_args',args) = dyn_infos.info in
771
do_finalize {dyn_infos with info = f_args'} g
773
(* observe (str "build_proof_args with arg := "++ pr_lconstr_env (pf_env g) arg++ *)
775
(* pr_goal (Tacmach.sig_it g) *)
777
let do_finalize dyn_infos =
778
let new_arg = dyn_infos.info in
782
{dyn_infos with info = (mkApp(f_args',[|new_arg|])), args}
785
build_proof do_finalize
786
{dyn_infos with info = arg }
789
(* observe_tac "build_proof_args" *) (tac ) g
791
let do_finish_proof dyn_infos =
792
(* tclTRYD *) (clean_goal_with_heq
794
finish_proof dyn_infos)
796
(* observe_tac "build_proof" *)
797
(build_proof (clean_goal_with_heq ptes_infos do_finish_proof) dyn_infos)
810
(* Proof of principles from structural functions *)
812
isSort (snd (decompose_prod t))
814
let is_pte (_,_,t) = is_pte_type t
819
type static_fix_info =
826
body_with_param : constr;
832
let prove_rec_hyp_for_struct fix_info =
833
(fun eq_hyps -> tclTHEN
834
(rewrite_until_var (fix_info.idx) eq_hyps)
836
let _,pte_args = destApp (pf_concl g) in
838
mkApp(mkVar fix_info.name,array_get_start pte_args)
840
refine rec_hyp_proof g
843
let prove_rec_hyp fix_info =
844
{ proving_tac = prove_rec_hyp_for_struct fix_info
846
is_valid = fun _ -> true
852
let generalize_non_dep hyp g =
853
(* observe (str "rec id := " ++ Ppconstr.pr_id hyp); *)
855
let env = Global.env () in
856
let hyp_typ = pf_type_of g (mkVar hyp) in
858
Environ.fold_named_context_reverse (fun (clear,keep) (hyp,_,_ as decl) ->
860
or List.exists (occur_var_in_decl env hyp) keep
861
or occur_var env hyp hyp_typ
862
or Termops.is_section_variable hyp (* should be dangerous *)
863
then (clear,decl::keep)
864
else (hyp::clear,keep))
865
~init:([],[]) (pf_env g)
867
(* observe (str "to_revert := " ++ prlist_with_sep spc Ppconstr.pr_id to_revert); *)
869
((* observe_tac "h_generalize" *) (h_generalize (List.map mkVar to_revert) ))
870
((* observe_tac "thin" *) (thin to_revert))
873
let id_of_decl (na,_,_) = (Nameops.out_name na)
874
let var_of_decl decl = mkVar (id_of_decl decl)
877
(generalize (List.map mkVar idl))
880
let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
881
(* observe (str "nb_args := " ++ str (string_of_int nb_args)); *)
882
(* observe (str "nb_params := " ++ str (string_of_int nb_params)); *)
883
(* observe (str "rec_args_num := " ++ str (string_of_int (rec_args_num + 1) )); *)
884
let f_def = Global.lookup_constant (destConst f) in
885
let eq_lhs = mkApp(f,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i))) in
887
force (Option.get f_def.const_body)
889
let params,f_body_with_params = decompose_lam_n nb_params f_body in
890
let (_,num),(_,_,bodies) = destFix f_body_with_params in
891
let fnames_with_params =
892
let params = Array.init nb_params (fun i -> mkRel(nb_params - i)) in
893
let fnames = List.rev (Array.to_list (Array.map (fun f -> mkApp(f,params)) fnames)) in
896
(* observe (str "fnames_with_params " ++ prlist_with_sep fnl pr_lconstr fnames_with_params); *)
897
(* observe (str "body " ++ pr_lconstr bodies.(num)); *)
898
let f_body_with_params_and_other_fun = substl fnames_with_params bodies.(num) in
899
(* observe (str "f_body_with_params_and_other_fun " ++ pr_lconstr f_body_with_params_and_other_fun); *)
900
let eq_rhs = nf_betaiotazeta (mkApp(compose_lam params f_body_with_params_and_other_fun,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i)))) in
901
(* observe (str "eq_rhs " ++ pr_lconstr eq_rhs); *)
902
let type_ctxt,type_of_f = Sign.decompose_prod_n_assum (nb_params + nb_args)
903
(Typeops.type_of_constant_type (Global.env()) f_def.const_type) in
904
let eqn = mkApp(Lazy.force eq,[|type_of_f;eq_lhs;eq_rhs|]) in
905
let lemma_type = it_mkProd_or_LetIn ~init:eqn type_ctxt in
906
let f_id = id_of_label (con_label (destConst f)) in
907
let prove_replacement =
910
tclDO (nb_params + rec_args_num + 1) intro;
911
(* observe_tac "" *) (fun g ->
912
let rec_id = pf_nth_hyp_id g 1 in
914
[(* observe_tac "generalize_non_dep in generate_equation_lemma" *) (generalize_non_dep rec_id);
915
(* observe_tac "h_case" *) (h_case false (mkVar rec_id,Rawterm.NoBindings));
916
intros_reflexivity] g
921
(*i The next call to mk_equation_id is valid since we are constructing the lemma
924
(mk_equation_id f_id)
925
(Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem))
928
Pfedit.by (prove_replacement);
929
Command.save_named false
934
let do_replace params rec_arg_num rev_args_id f fun_num all_funs g =
937
let finfos = find_Function_infos (destConst f) in
938
mkConst (Option.get finfos.equation_lemma)
939
with (Not_found | Option.IsNone as e) ->
940
let f_id = id_of_label (con_label (destConst f)) in
941
(*i The next call to mk_equation_id is valid since we will construct the lemma
944
let equation_lemma_id = (mk_equation_id f_id) in
945
generate_equation_lemma all_funs f fun_num (List.length params) (List.length rev_args_id) rec_arg_num;
949
let finfos = find_Function_infos (destConst f) in
952
equation_lemma = Some (match Nametab.locate (make_short_qualid equation_lemma_id) with
954
| _ -> Util.anomaly "Not a constant"
960
Tacinterp.constr_of_id (pf_env g) equation_lemma_id
962
let nb_intro_to_do = nb_prod (pf_concl g) in
964
(tclDO nb_intro_to_do intro)
967
let just_introduced = nLastHyps nb_intro_to_do g' in
968
let just_introduced_id = List.map (fun (id,_,_) -> id) just_introduced in
969
tclTHEN (Equality.rewriteLR equation_lemma) (revert just_introduced_id) g'
973
let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams : tactic =
975
let princ_type = pf_concl g in
976
let princ_info = compute_elim_sig princ_type in
978
let avoid = ref (pf_ids_of_hyps g) in
982
Name id -> fresh_id !avoid (string_of_id id)
983
| Anonymous -> fresh_id !avoid "H"
985
avoid := new_id :: !avoid;
994
let princ_info : elim_scheme =
996
params = List.map fresh_decl princ_info.params;
997
predicates = List.map fresh_decl princ_info.predicates;
998
branches = List.map fresh_decl princ_info.branches;
999
args = List.map fresh_decl princ_info.args
1002
let get_body const =
1003
match (Global.lookup_constant const ).const_body with
1005
let body = force b in
1006
Tacred.cbv_norm_flags
1007
(Closure.RedFlags.mkflags [Closure.RedFlags.fZETA])
1011
| None -> error ( "Cannot define a principle over an axiom ")
1013
let fbody = get_body fnames.(fun_num) in
1014
let f_ctxt,f_body = decompose_lam fbody in
1015
let f_ctxt_length = List.length f_ctxt in
1016
let diff_params = princ_info.nparams - f_ctxt_length in
1017
let full_params,princ_params,fbody_with_full_params =
1020
let princ_params,full_params =
1021
list_chop diff_params princ_info.params
1023
(full_params, (* real params *)
1024
princ_params, (* the params of the principle which are not params of the function *)
1025
substl (* function instanciated with real params *)
1026
(List.map var_of_decl full_params)
1030
let f_ctxt_other,f_ctxt_params =
1031
list_chop (- diff_params) f_ctxt in
1032
let f_body = compose_lam f_ctxt_other f_body in
1033
(princ_info.params, (* real params *)
1034
[],(* all params are full params *)
1035
substl (* function instanciated with real params *)
1036
(List.map var_of_decl princ_info.params)
1040
(* observe (str "full_params := " ++ *)
1041
(* prlist_with_sep spc (fun (na,_,_) -> Ppconstr.pr_id (Nameops.out_name na)) *)
1044
(* observe (str "princ_params := " ++ *)
1045
(* prlist_with_sep spc (fun (na,_,_) -> Ppconstr.pr_id (Nameops.out_name na)) *)
1048
(* observe (str "fbody_with_full_params := " ++ *)
1049
(* pr_lconstr fbody_with_full_params *)
1051
let all_funs_with_full_params =
1052
Array.map (fun f -> applist(f, List.rev_map var_of_decl full_params)) all_funs
1054
let fix_offset = List.length princ_params in
1055
let ptes_to_fix,infos =
1056
match kind_of_term fbody_with_full_params with
1057
| Fix((idxs,i),(names,typess,bodies)) ->
1058
let bodies_with_all_params =
1061
Reductionops.nf_betaiota Evd.empty
1062
(applist(substl (List.rev (Array.to_list all_funs_with_full_params)) body,
1063
List.rev_map var_of_decl princ_params))
1070
let types = prod_applist types (List.rev_map var_of_decl princ_params) in
1071
{ idx = idxs.(i) - fix_offset;
1072
name = Nameops.out_name (fresh_id names.(i));
1074
offset = fix_offset;
1077
(fst (decompose_lam bodies.(i))) - fix_offset;
1078
body_with_param = bodies_with_all_params.(i);
1084
let pte_to_fix,rev_info =
1086
(fun i (acc_map,acc_info) (pte,_,_) ->
1087
let infos = info_array.(i) in
1088
let type_args,_ = decompose_prod infos.types in
1089
let nargs = List.length type_args in
1090
let f = applist(mkConst fnames.(i), List.rev_map var_of_decl princ_info.params) in
1091
let first_args = Array.init nargs (fun i -> mkRel (nargs -i)) in
1092
let app_f = mkApp(f,first_args) in
1093
let pte_args = (Array.to_list first_args)@[app_f] in
1094
let app_pte = applist(mkVar (Nameops.out_name pte),pte_args) in
1095
let body_with_param,num =
1096
let body = get_body fnames.(i) in
1097
let body_with_full_params =
1098
Reductionops.nf_betaiota Evd.empty (
1099
applist(body,List.rev_map var_of_decl full_params))
1101
match kind_of_term body_with_full_params with
1102
| Fix((_,num),(_,_,bs)) ->
1103
Reductionops.nf_betaiota Evd.empty
1108
(Array.to_list all_funs_with_full_params))
1110
List.rev_map var_of_decl princ_params))
1112
| _ -> error "Not a mutual block"
1116
types = compose_prod type_args app_pte;
1117
body_with_param = body_with_param;
1121
(* observe (str "binding " ++ Ppconstr.pr_id (Nameops.out_name pte) ++ *)
1122
(* str " to " ++ Ppconstr.pr_id info.name); *)
1123
(Idmap.add (Nameops.out_name pte) info acc_map,info::acc_info)
1127
(List.rev princ_info.predicates)
1129
pte_to_fix,List.rev rev_info
1130
| _ -> Idmap.empty,[]
1132
let mk_fixes : tactic =
1133
let pre_info,infos = list_chop fun_num infos in
1134
match pre_info,infos with
1136
| _, this_fix_info::others_infos ->
1137
let other_fix_infos =
1139
(fun fi -> fi.name,fi.idx + 1 ,fi.types)
1140
(pre_info@others_infos)
1142
if other_fix_infos = []
1144
(* observe_tac ("h_fix") *) (h_fix (Some this_fix_info.name) (this_fix_info.idx +1))
1146
h_mutual_fix false this_fix_info.name (this_fix_info.idx + 1)
1148
| _ -> anomaly "Not a valid information"
1150
let first_tac : tactic = (* every operations until fix creations *)
1152
[ (* observe_tac "introducing params" *) (intros_using (List.rev_map id_of_decl princ_info.params));
1153
(* observe_tac "introducing predictes" *) (intros_using (List.rev_map id_of_decl princ_info.predicates));
1154
(* observe_tac "introducing branches" *) (intros_using (List.rev_map id_of_decl princ_info.branches));
1155
(* observe_tac "building fixes" *) mk_fixes;
1158
let intros_after_fixes : tactic =
1160
let ctxt,pte_app = (Sign.decompose_prod_assum (pf_concl gl)) in
1161
let pte,pte_args = (decompose_app pte_app) in
1163
let pte = try destVar pte with _ -> anomaly "Property is not a variable" in
1164
let fix_info = Idmap.find pte ptes_to_fix in
1165
let nb_args = fix_info.nb_realargs in
1168
(* observe_tac ("introducing args") *) (tclDO nb_args intro);
1169
(fun g -> (* replacement of the function by its body *)
1170
let args = nLastHyps nb_args g in
1171
let fix_body = fix_info.body_with_param in
1172
(* observe (str "fix_body := "++ pr_lconstr_env (pf_env gl) fix_body); *)
1173
let args_id = List.map (fun (id,_,_) -> id) args in
1179
Reductionops.nf_betaiota Evd.empty
1180
(applist(fix_body,List.rev_map mkVar args_id));
1186
(* observe_tac "do_replace" *)
1189
(fix_info.idx + List.length princ_params)
1190
(args_id@(List.map (fun (id,_,_) -> Nameops.out_name id ) princ_params))
1191
(all_funs.(fix_info.num_in_block))
1192
fix_info.num_in_block
1195
(* observe_tac "do_replace" *)
1196
(* (do_replace princ_info.params fix_info.idx args_id *)
1197
(* (List.hd (List.rev pte_args)) fix_body); *)
1201
(Array.to_list fnames)
1202
(Idmap.map prove_rec_hyp ptes_to_fix)
1204
let prove_tac branches =
1207
rec_hyps = branches;
1208
nb_rec_hyps = List.length branches
1211
(* observe_tac "cleaning" *) (clean_goal_with_heq
1212
(Idmap.map prove_rec_hyp ptes_to_fix)
1216
(* observe (str "branches := " ++ *)
1217
(* prlist_with_sep spc (fun decl -> Ppconstr.pr_id (id_of_decl decl)) princ_info.branches ++ fnl () ++ *)
1218
(* str "args := " ++ prlist_with_sep spc Ppconstr.pr_id args_id *)
1221
(* observe_tac "instancing" *) (instanciate_hyps_with_args prove_tac
1222
(List.rev_map id_of_decl princ_info.branches)
1229
let nb_args = min (princ_info.nargs) (List.length ctxt) in
1232
tclDO nb_args intro;
1233
(fun g -> (* replacement of the function by its body *)
1234
let args = nLastHyps nb_args g in
1235
let args_id = List.map (fun (id,_,_) -> id) args in
1241
Reductionops.nf_betaiota Evd.empty
1242
(applist(fbody_with_full_params,
1243
(List.rev_map var_of_decl princ_params)@
1244
(List.rev_map mkVar args_id)
1249
let fname = destConst (fst (decompose_app (List.hd (List.rev pte_args)))) in
1251
[unfold_in_concl [(all_occurrences,Names.EvalConstRef fname)];
1255
(Array.to_list fnames)
1256
(Idmap.map prove_rec_hyp ptes_to_fix)
1258
let prove_tac branches =
1261
rec_hyps = branches;
1262
nb_rec_hyps = List.length branches
1266
(Idmap.map prove_rec_hyp ptes_to_fix)
1270
instanciate_hyps_with_args prove_tac
1271
(List.rev_map id_of_decl princ_info.branches)
1289
(* Proof of principles of general functions *)
1290
let h_id = Recdef.h_id
1291
and hrec_id = Recdef.hrec_id
1292
and acc_inv_id = Recdef.acc_inv_id
1293
and ltof_ref = Recdef.ltof_ref
1294
and acc_rel = Recdef.acc_rel
1295
and well_founded = Recdef.well_founded
1296
and delayed_force = Recdef.delayed_force
1297
and h_intros = Recdef.h_intros
1298
and list_rewrite = Recdef.list_rewrite
1299
and evaluable_of_global_reference = Recdef.evaluable_of_global_reference
1305
let prove_with_tcc tcc_lemma_constr eqs : tactic =
1306
match !tcc_lemma_constr with
1307
| None -> anomaly "No tcc proof !!"
1310
(* let hid = next_global_ident_away true h_id (pf_ids_of_hyps gls) in *)
1311
(* let ids = hid::pf_ids_of_hyps gls in *)
1314
(* generalize [lemma]; *)
1316
(* Elim.h_decompose_and (mkVar hid); *)
1317
tclTRY(list_rewrite true eqs);
1319
(* let ids' = pf_ids_of_hyps g in *)
1320
(* let ids = List.filter (fun id -> not (List.mem id ids)) ids' in *)
1323
Eauto.gen_eauto false (false,5) [] (Some [])
1328
let backtrack_eqs_until_hrec hrec eqs : tactic =
1330
let eqs = List.map mkVar eqs in
1332
tclFIRST (List.map Equality.rewriteRL eqs )
1334
let _,hrec_concl = decompose_prod (pf_type_of gls (mkVar hrec)) in
1335
let f_app = array_last (snd (destApp hrec_concl)) in
1336
let f = (fst (destApp f_app)) in
1337
let rec backtrack : tactic =
1339
let f_app = array_last (snd (destApp (pf_concl g))) in
1340
match kind_of_term f_app with
1341
| App(f',_) when eq_constr f' f -> tclIDTAC g
1342
| _ -> tclTHEN rewrite backtrack g
1348
let build_clause eqs =
1352
(fun id -> (Rawterm.all_occurrences_expr,id),InHyp)
1355
Tacexpr.concl_occs = Rawterm.no_occurrences_expr
1358
let rec rewrite_eqs_in_eqs eqs =
1367
(Format.sprintf "rewrite %s in %s " (string_of_id eq) (string_of_id id))
1368
(tclTRY (Equality.general_rewrite_in true all_occurrences id (mkVar eq) false))
1373
(rewrite_eqs_in_eqs eqs)
1375
let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic =
1379
backtrack_eqs_until_hrec hrec eqs;
1380
(* observe_tac ("new_prove_with_tcc ( applying "^(string_of_id hrec)^" )" ) *)
1381
(tclTHENS (* We must have exactly ONE subgoal !*)
1382
(apply (mkVar hrec))
1385
keep (tcc_hyps@eqs);
1386
apply (Lazy.force acc_inv);
1390
unfold_in_concl [(all_occurrences, evaluable_of_global_reference (delayed_force ltof_ref))] g
1393
observe_tac "rew_and_finish"
1395
[tclTRY(Recdef.list_rewrite false (List.map mkVar eqs));
1396
observe_tac "rewrite_eqs_in_eqs" (rewrite_eqs_in_eqs eqs);
1397
(observe_tac "finishing using"
1400
Eauto.eauto_with_bases
1403
[Lazy.force refl_equal]
1404
[Auto.Hint_db.empty empty_transparent_state false]
1416
let is_valid_hypothesis predicates_name =
1417
let predicates_name = List.fold_right Idset.add predicates_name Idset.empty in
1421
let pte,_ = destApp typ in
1423
then Idset.mem (destVar pte) predicates_name
1427
let rec is_valid_hypothesis typ =
1429
match kind_of_term typ with
1430
| Prod(_,pte,typ') -> is_pte pte && is_valid_hypothesis typ'
1435
let prove_principle_for_gen
1436
(f_ref,functional_ref,eq_ref) tcc_lemma_ref is_mes
1437
rec_arg_num rec_arg_type relation gl =
1438
let princ_type = pf_concl gl in
1439
let princ_info = compute_elim_sig princ_type in
1441
let avoid = ref (pf_ids_of_hyps gl) in
1445
| Name id -> fresh_id !avoid (string_of_id id)
1446
| Anonymous -> fresh_id !avoid "H"
1448
avoid := new_id :: !avoid;
1451
let fresh_decl (na,b,t) = (fresh_id na,b,t) in
1452
let princ_info : elim_scheme =
1454
params = List.map fresh_decl princ_info.params;
1455
predicates = List.map fresh_decl princ_info.predicates;
1456
branches = List.map fresh_decl princ_info.branches;
1457
args = List.map fresh_decl princ_info.args
1463
(fun b -> Recdef.tclUSER_if_not_mes tclIDTAC b None)
1464
else fun _ -> prove_with_tcc tcc_lemma_ref []
1466
let real_rec_arg_num = rec_arg_num - princ_info.nparams in
1467
let npost_rec_arg = princ_info.nargs - real_rec_arg_num + 1 in
1469
(* str "princ_type := " ++ pr_lconstr princ_type ++ fnl () ++ *)
1470
(* str "princ_info.nparams := " ++ int princ_info.nparams ++ fnl () ++ *)
1472
(* str "princ_info.nargs := " ++ int princ_info.nargs ++ fnl () ++ *)
1473
(* str "rec_arg_num := " ++ int rec_arg_num ++ fnl() ++ *)
1474
(* str "real_rec_arg_num := " ++ int real_rec_arg_num ++ fnl () ++ *)
1475
(* str "npost_rec_arg := " ++ int npost_rec_arg ); *)
1476
let (post_rec_arg,pre_rec_arg) =
1477
Util.list_chop npost_rec_arg princ_info.args
1480
match List.rev post_rec_arg with
1481
| (Name id,_,_)::_ -> id
1484
(* observe (str "rec_arg_id := " ++ pr_lconstr (mkVar rec_arg_id)); *)
1485
let subst_constrs = List.map (fun (na,_,_) -> mkVar (Nameops.out_name na)) (pre_rec_arg@princ_info.params) in
1486
let relation = substl subst_constrs relation in
1487
let input_type = substl subst_constrs rec_arg_type in
1488
let wf_thm_id = Nameops.out_name (fresh_id (Name (id_of_string "wf_R"))) in
1489
let acc_rec_arg_id =
1490
Nameops.out_name (fresh_id (Name (id_of_string ("Acc_"^(string_of_id rec_arg_id)))))
1493
tclTHEN (h_generalize (List.map mkVar l)) (clear l)
1495
let fix_id = Nameops.out_name (fresh_id (Name hrec_id)) in
1496
let prove_rec_arg_acc g =
1497
((* observe_tac "prove_rec_arg_acc" *)
1500
(assert_by (Name wf_thm_id)
1501
(mkApp (delayed_force well_founded,[|input_type;relation|]))
1502
(fun g -> (* observe_tac "prove wf" *) (tclCOMPLETE (wf_tac is_mes)) g))
1505
(* "apply wf_thm" *)
1506
h_simplest_apply (mkApp(mkVar wf_thm_id,[|mkVar rec_arg_id|]))
1513
let args_ids = List.map (fun (na,_,_) -> Nameops.out_name na) princ_info.args in
1515
match !tcc_lemma_ref with
1516
| None -> anomaly ( "No tcc proof !!")
1517
| Some lemma -> lemma
1519
(* let rec list_diff del_list check_list = *)
1520
(* match del_list with *)
1524
(* if List.mem f check_list then *)
1525
(* list_diff r check_list *)
1527
(* f::(list_diff r check_list) *)
1529
let tcc_list = ref [] in
1531
let hyps = pf_ids_of_hyps gls in
1533
next_global_ident_away true
1534
(id_of_string "prov")
1541
Elim.h_decompose_and (mkVar hid);
1543
let new_hyps = pf_ids_of_hyps g in
1544
tcc_list := List.rev (list_subtract new_hyps (hid::hyps));
1558
observe_tac "start_tac" start_tac;
1560
(List.rev_map (fun (na,_,_) -> Nameops.out_name na)
1561
(princ_info.args@princ_info.branches@princ_info.predicates@princ_info.params)
1563
(* observe_tac "" *) (assert_by
1564
(Name acc_rec_arg_id)
1565
(mkApp (delayed_force acc_rel,[|input_type;relation;mkVar rec_arg_id|]))
1568
(* observe_tac "reverting" *) (revert (List.rev (acc_rec_arg_id::args_ids)));
1569
(* (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl () ++ *)
1570
(* str "fix arg num" ++ int (List.length args_ids + 1) ); tclIDTAC g); *)
1571
(* observe_tac "h_fix " *) (h_fix (Some fix_id) (List.length args_ids + 1));
1572
(* (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl() ++ pr_lconstr_env (pf_env g ) (pf_type_of g (mkVar fix_id) )); tclIDTAC g); *)
1573
h_intros (List.rev (acc_rec_arg_id::args_ids));
1574
Equality.rewriteLR (mkConst eq_ref);
1575
(* observe_tac "finish" *) (fun gl' ->
1577
let _,args = destApp (pf_concl gl') in
1580
let body_info rec_hyps =
1582
nb_rec_hyps = List.length rec_hyps;
1583
rec_hyps = rec_hyps;
1591
delayed_force acc_inv_id,
1592
[|input_type;relation;mkVar rec_arg_id|]
1596
let acc_inv = lazy (mkApp(Lazy.force acc_inv, [|mkVar acc_rec_arg_id|])) in
1597
let predicates_names =
1598
List.map (fun (na,_,_) -> Nameops.out_name na) princ_info.predicates
1603
(* msgnl (str "tcc_list := "++ prlist_with_sep spc Ppconstr.pr_id !tcc_list); *)
1604
(* msgnl (str "princ_info.args := "++ prlist_with_sep spc Ppconstr.pr_id (List.map (fun (na,_,_) -> (Nameops.out_name na)) princ_info.args)); *)
1605
(* msgnl (str "princ_info.params := "++ prlist_with_sep spc Ppconstr.pr_id (List.map (fun (na,_,_) -> (Nameops.out_name na)) princ_info.params)); *)
1606
(* msgnl (str "acc_rec_arg_id := "++ Ppconstr.pr_id acc_rec_arg_id); *)
1607
(* msgnl (str "eqs := "++ prlist_with_sep spc Ppconstr.pr_id eqs); *)
1609
(* observe_tac "new_prove_with_tcc" *)
1611
is_mes acc_inv fix_id
1613
(!tcc_list@(List.map
1614
(fun (na,_,_) -> (Nameops.out_name na))
1615
(princ_info.args@princ_info.params)
1616
)@ ([acc_rec_arg_id])) eqs
1620
is_valid = is_valid_hypothesis predicates_names
1623
let ptes_info : pte_info Idmap.t =
1633
let make_proof rec_hyps =
1638
(body_info rec_hyps)
1640
(* observe_tac "instanciate_hyps_with_args" *)
1641
(instanciate_hyps_with_args
1643
(List.map (fun (na,_,_) -> Nameops.out_name na) princ_info.branches)
added
removed
contrib/funind/functional_principles_proofs.ml
