Quelle functional_principles_proofs.ml
Sprache: SML
(************************************************************************) (* * The Rocq Prover / The Rocq Development Team *) (* v * Copyright INRIA, CNRS and contributors *) (* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (* * (see LICENSE file for the text of the license) *) (************************************************************************)
open Printer open CErrors open Util open Constr open Context open Termops open EConstr open Vars open Namegen open Names open Pp open Tactics open Induction open Indfun_common open Libnames open Context.Rel.Declaration
module RelDecl = Context.Rel.Declaration
(* funind does not support univ poly *) open UnsafeMonomorphic
let list_chop ?(msg = "") n l = tryList.chop n l with Failure msg' -> failwith (msg ^ msg')
let pop t = Vars.lift (-1) t
let make_refl_eq constructor type_of_t t = (* let refl_equal_term = Lazy.force refl_equal in *)
mkApp (constructor, [|type_of_t; t|])
type pte_info =
{proving_tac : Id.t list -> unit Proofview.tactic; is_valid : constr -> bool}
let observe_tac s =
observe_tac ~header:(str "observation") (fun _ _ -> Pp.str s)
let finish_proof dynamic_infos = observe_tac "finish" assumption let thin = clear let eq_constr sigma u v = EConstr.eq_constr_nounivs sigma u v
let is_trivial_eq sigma t = let res = try match EConstr.kind sigma t with
| App (f, [|_; t1; t2|]) when eq_constr sigma f (Lazy.force eq) ->
eq_constr sigma t1 t2
| App (f, [|t1; a1; t2; a2|]) when eq_constr sigma f (jmeq ()) ->
eq_constr sigma t1 t2 && eq_constr sigma a1 a2
| _ -> false with e when CErrors.noncritical e -> false in (* observe (str "is_trivial_eq " ++ Printer.pr_lconstr t ++ (if res then str " true" else str " false")); *)
res
let is_incompatible_eq env sigma t = let res = try match EConstr.kind sigma t with
| App (f, [|_; t1; t2|]) when eq_constr sigma f (Lazy.force eq) ->
incompatible_constructor_terms sigma t1 t2
| App (f, [|u1; t1; u2; t2|]) when eq_constr sigma f (jmeq ()) ->
eq_constr sigma u1 u2 && incompatible_constructor_terms sigma t1 t2
| _ -> false with e when CErrors.noncritical e -> false in if res then observe (fun () -> str "is_incompatible_eq " ++ pr_leconstr_env env sigma t);
res
let pf_get_new_id id env =
next_ident_away id (Id.Set.of_list (Termops.ids_of_named_context env))
let prove_trivial_eq h_id context (constructor, type_of_term, term) = let nb_intros = List.length context in
Tacticals.tclTHENLIST
[ Tacticals.tclDO nb_intros intro
; (* introducing context *)
Proofview.Goal.enter (fun g -> let hyps = Proofview.Goal.hyps g in let context_hyps =
fst
(list_chop ~msg:"prove_trivial_eq : " nb_intros
(ids_of_named_context hyps)) in let context_hyps' =
mkApp (constructor, [|type_of_term; term|])
:: List.map mkVar context_hyps in let to_refine = applist (mkVar h_id, List.rev context_hyps') in
Tactics.exact_check to_refine) ]
let find_rectype env sigma c = let t, l = decompose_app_list sigma (Reductionops.whd_betaiotazeta env sigma c) in match EConstr.kind sigma t with
| Ind ind -> (t, l)
| Construct _ -> (t, l)
| _ -> raise Not_found
let isAppConstruct env sigma t = try let t', l = find_rectype env sigma t in
observe
(fun () -> str "isAppConstruct : "
++ Printer.pr_leconstr_env env sigma t
++ str " -> "
++ Printer.pr_leconstr_env env sigma (applist (t', l)) ); true with Not_found -> false
exception NoChange
let change_eq env sigma hyp_id (context : rel_context) x t end_of_type = let nochange ?t' msg =
observe
(fun () -> str ("Not treating ( " ^ msg ^ " )")
++ pr_leconstr_env env sigma t
++ str " "
++ match t' with
| None -> str ""
| Some t -> Printer.pr_leconstr_env env sigma t ); raise NoChange in let eq_constr c1 c2 = try
ignore (Evarconv.unify_delay env sigma c1 c2); true with Evarconv.UnableToUnify _ -> false in ifnot (noccurn sigma 1 end_of_type) then nochange "dependent"; (* if end_of_type depends on this term we don't touch it *) ifnot (isApp sigma t) then nochange "not an equality"; let f_eq, args = destApp sigma t in let constructor, t1, t2, t1_typ = try if eq_constr f_eq (Lazy.force eq) then let t1 = (args.(1), args.(0)) and t2 = (args.(2), args.(0)) and t1_typ = args.(0) in
(Lazy.force refl_equal, t1, t2, t1_typ) elseif eq_constr f_eq (jmeq ()) then
(jmeq_refl (), (args.(1), args.(0)), (args.(3), args.(2)), args.(0)) else nochange "not an equality" with e when CErrors.noncritical e -> nochange "not an equality" in ifnot (closed0 sigma (fst t1) && closed0 sigma (snd t1)) then
nochange "not a closed lhs"; let rec compute_substitution sub t1 t2 = (* observe (str "compute_substitution : " ++ pr_lconstr t1 ++ str " === " ++ pr_lconstr t2); *) if isRel sigma t2 then ( let t2 = destRel sigma t2 in try let t1' = Int.Map.find t2 sub in ifnot (eq_constr t1 t1') then nochange "twice bound variable"; sub with Not_found ->
assert (closed0 sigma t1);
Int.Map.add t2 t1 sub ) elseif isAppConstruct env sigma t1 && isAppConstruct env sigma t2 thenbegin let c1, args1 = find_rectype env sigma t1 and c2, args2 = find_rectype env sigma t2 in ifnot (eq_constr c1 c2) then nochange "cannot solve (diff)"; List.fold_left2 compute_substitution sub args1 args2 end elseif eq_constr t1 t2 thensub else
nochange
~t':(make_refl_eq constructor (Reductionops.whd_all env sigma t1) t2) "cannot solve (diff)" in letsub = compute_substitution Int.Map.empty (snd t1) (snd t2) in letsub = compute_substitution sub (fst t1) (fst t2) in let end_of_type_with_pop = pop end_of_type in (*the equation will be removed *) let new_end_of_type = (* Ugly hack to prevent Map.fold order change between ocaml-3.08.3 and ocaml-3.08.4 Can be safely replaced by the next comment for Ocaml >= 3.08.4
*) letsub = Int.Map.bindings subin List.fold_left
(fun end_of_type (i, t) -> liftn 1 i (substnl [t] (i - 1) end_of_type))
end_of_type_with_pop sub in let old_context_length = List.length context + 1 in let witness_fun =
mkLetIn
( make_annot Anonymous ERelevance.relevant
, make_refl_eq constructor t1_typ (fst t1)
, t
, mkApp
( mkVar hyp_id
, Array.init old_context_length (fun i ->
mkRel (old_context_length - i)) ) ) in let new_type_of_hyp, ctxt_size, witness_fun = List.fold_left_i
(fun i (end_of_type, ctxt_size, witness_fun) decl -> try let witness = Int.Map.find i subin if is_local_def decl then anomaly (Pp.str "can not redefine a rel!");
( pop end_of_type
, ctxt_size
, mkLetIn
( RelDecl.get_annot decl
, witness
, RelDecl.get_type decl
, witness_fun ) ) with Not_found ->
( mkProd_or_LetIn decl end_of_type
, ctxt_size + 1
, mkLambda_or_LetIn decl witness_fun ))
1
(new_end_of_type, 0, witness_fun)
context in let new_type_of_hyp = Reductionops.nf_betaiota env sigma new_type_of_hyp in let new_ctxt, new_end_of_type =
decompose_prod_n_decls sigma ctxt_size new_type_of_hyp in let prove_new_hyp = letopen Tacticals in letopen Tacmach in
tclTHEN (tclDO ctxt_size intro)
(Proofview.Goal.enter (fun g -> let all_ids = pf_ids_of_hyps g in let new_ids, _ = list_chop ctxt_size all_ids in let to_refine = applist (witness_fun, List.rev_map mkVar new_ids) in let evm, _ =
Typing.type_of (Proofview.Goal.env g) (Proofview.Goal.sigma g)
to_refine in
tclTHEN (Proofview.Unsafe.tclEVARS evm) (Tactics.exact_check to_refine))) in let simpl_eq_tac =
change_hyp_with_using "prove_pattern_simplification" hyp_id new_type_of_hyp
prove_new_hyp in (* observe (str "In " ++ Ppconstr.pr_id hyp_id ++ *) (* str "removing an equation " ++ fnl ()++ *) (* str "old_typ_of_hyp :=" ++ *) (* Printer.pr_lconstr_env *) (* env *) (* (it_mkProd_or_LetIn ~init:end_of_type ((x,None,t)::context)) *) (* ++ fnl () ++ *) (* str "new_typ_of_hyp := "++ *) (* Printer.pr_lconstr_env env new_type_of_hyp ++ fnl () *) (* ++ str "old context := " ++ pr_rel_context env context ++ fnl () *) (* ++ str "new context := " ++ pr_rel_context env new_ctxt ++ fnl () *) (* ++ str "old type := " ++ pr_lconstr end_of_type ++ fnl () *) (* ++ str "new type := " ++ pr_lconstr new_end_of_type ++ fnl () *) (* ); *)
(new_ctxt, new_end_of_type, simpl_eq_tac)
let is_property sigma (ptes_info : ptes_info) t_x full_type_of_hyp = if isApp sigma t_x then let pte, args = destApp sigma t_x in if isVar sigma pte && Array.for_all (closed0 sigma) args then try let info = Id.Map.find (destVar sigma pte) ptes_info in
info.is_valid full_type_of_hyp with Not_found -> false elsefalse elsefalse
let isLetIn sigma t = match EConstr.kind sigma t with LetIn _ -> true | _ -> false
let h_reduce_with_zeta cl =
reduce (Genredexpr.Cbv {Redops.all_flags with Genredexpr.rDelta = false}) cl
let rewrite_until_var arg_num eq_ids : unit Proofview.tactic = letopen Tacticals in (* tests if the declares recursive argument is neither a Constructor nor an applied Constructor since such a form for the recursive argument will break the Guard when trying to save the Lemma.
*) let test_var g = let sigma = Proofview.Goal.sigma g in let env = Proofview.Goal.env g in let _, args = destApp sigma (Proofview.Goal.concl g) in not (isConstruct sigma args.(arg_num) || isAppConstruct env sigma args.(arg_num)) in let rec do_rewrite eq_ids =
Proofview.Goal.enter (fun g -> if test_var g then Proofview.tclUNIT () else match eq_ids with
| [] ->
anomaly (Pp.str "Cannot find a way to prove recursive property.")
| eq_id :: eq_ids ->
tclTHEN
(tclTRY (Equality.rewriteRL (mkVar eq_id)))
(do_rewrite eq_ids)) in
do_rewrite eq_ids
let rec_pte_id = Id.of_string "Hrec"
let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = let rocq_False =
EConstr.of_constr
(UnivGen.constr_of_monomorphic_global env @@ Rocqlib.lib_ref "core.False.type") in let rocq_True =
EConstr.of_constr
(UnivGen.constr_of_monomorphic_global env @@ Rocqlib.lib_ref "core.True.type") in let rocq_I =
EConstr.of_constr
(UnivGen.constr_of_monomorphic_global env @@ Rocqlib.lib_ref "core.True.I") in letopen Tacticals in let rec scan_type context type_of_hyp : unit Proofview.tactic = if isLetIn sigma type_of_hyp then let real_type_of_hyp = it_mkProd_or_LetIn type_of_hyp context in let reduced_type_of_hyp =
Reductionops.nf_betaiotazeta env sigma real_type_of_hyp in (* length of context didn't change ? *) let new_context, new_typ_of_hyp =
decompose_prod_n_decls sigma (List.length context) reduced_type_of_hyp in
tclTHENLIST
[ h_reduce_with_zeta (Locusops.onHyp hyp_id)
; scan_type new_context new_typ_of_hyp ] elseif isProd sigma type_of_hyp then let x, t_x, t' = destProd sigma type_of_hyp in let actual_real_type_of_hyp = it_mkProd_or_LetIn t' context in if is_property sigma ptes_infos t_x actual_real_type_of_hyp then let pte, pte_args = destApp sigma t_x in let(* fix_info *) prove_rec_hyp =
(Id.Map.find (destVar sigma pte) ptes_infos).proving_tac in let popped_t' = pop t'in let real_type_of_hyp = it_mkProd_or_LetIn popped_t' context in let prove_new_type_of_hyp = let context_length = List.length context in
tclTHENLIST
[ tclDO context_length intro
; Proofview.Goal.enter (fun g -> let hyps = Proofview.Goal.hyps g in let context_hyps_ids =
fst
(list_chop ~msg:"rec hyp : context_hyps" context_length
(ids_of_named_context hyps)) in let rec_pte_id = pf_get_new_id rec_pte_id hyps in let to_refine =
applist
( mkVar hyp_id
, List.rev_map mkVar (rec_pte_id :: context_hyps_ids) ) in (* observe_tac "rec hyp " *)
tclTHENS
(assert_before (Name rec_pte_id) t_x)
[ (* observe_tac "prove rec hyp" *)
prove_rec_hyp eq_hyps
; (* observe_tac "prove rec hyp" *)
Tactics.exact_check to_refine ]) ] in
tclTHENLIST
[ (* observe_tac "hyp rec" *)
change_hyp_with_using "rec_hyp_tac" hyp_id real_type_of_hyp
prove_new_type_of_hyp
; scan_type context popped_t' ] elseif eq_constr sigma t_x rocq_False then (* observe (str "Removing : "++ Ppconstr.pr_id hyp_id++ *) (* str " since it has False in its preconds " *) (* ); *) raise TOREMOVE (* False -> .. useless *) elseif is_incompatible_eq env sigma t_x thenraise TOREMOVE (* t_x := C1 ... = C2 ... *) elseif
eq_constr sigma t_x rocq_True (* Trivial => we remove this precons *) then (* observe (str "In "++Ppconstr.pr_id hyp_id++ *) (* str " removing useless precond True" *) (* ); *) let popped_t' = pop t'in let real_type_of_hyp = it_mkProd_or_LetIn popped_t' context in let prove_trivial = let nb_intro = List.length context in
tclTHENLIST
[ tclDO nb_intro intro
; Proofview.Goal.enter (fun g -> let hyps = Proofview.Goal.hyps g in let context_hyps =
fst
(list_chop ~msg:"removing True : context_hyps " nb_intro
(ids_of_named_context hyps)) in let to_refine =
applist
( mkVar hyp_id
, List.rev (rocq_I :: List.map mkVar context_hyps) ) in
Tactics.exact_check to_refine) ] in
tclTHENLIST
[ change_hyp_with_using "prove_trivial" hyp_id real_type_of_hyp (* observe_tac "prove_trivial" *) prove_trivial
; scan_type context popped_t' ] elseif is_trivial_eq sigma t_x then (* t_x := t = t => we remove this precond *) let popped_t' = pop t'in let real_type_of_hyp = it_mkProd_or_LetIn popped_t' context in let hd, args = destApp sigma t_x in let get_args hd args = if eq_constr sigma hd (Lazy.force eq) then
(Lazy.force refl_equal, args.(0), args.(1)) else (jmeq_refl (), args.(0), args.(1)) in
tclTHENLIST
[ change_hyp_with_using "prove_trivial_eq" hyp_id real_type_of_hyp
((* observe_tac "prove_trivial_eq" *)
prove_trivial_eq hyp_id context (get_args hd args))
; scan_type context popped_t' ] else try let new_context, new_t', tac =
change_eq env sigma hyp_id context x t_x t' in
tclTHEN tac (scan_type new_context new_t') with NoChange -> (* Last thing todo : push the rel in the context and continue *)
scan_type (LocalAssum (x, t_x) :: context) t' else tclIDTAC in try (scan_type [] (Typing.type_of_variable env hyp_id), [hyp_id]) with TOREMOVE -> (thin [hyp_id], [])
let clean_goal_with_heq ptes_infos continue_tac (dyn_infos : body_info) = letopen Tacticals in
Proofview.Goal.enter (fun g -> let env = Proofview.Goal.env g in let sigma = Proofview.Goal.sigma g in let tac, new_hyps = List.fold_left
(fun (hyps_tac, new_hyps) hyp_id -> let hyp_tac, new_hyp =
clean_hyp_with_heq ptes_infos dyn_infos.eq_hyps hyp_id env sigma in
(tclTHEN hyp_tac hyps_tac, new_hyp @ new_hyps))
(tclIDTAC, []) dyn_infos.rec_hyps in let new_infos =
{dyn_infos with rec_hyps = new_hyps; nb_rec_hyps = List.length new_hyps} in
tclTHENLIST
[ tac
; (* observe_tac "clean_hyp_with_heq continue" *)
continue_tac new_infos ])
let heq_id = Id.of_string "Heq"
let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos = letopen Tacticals in
Proofview.Goal.enter (fun g -> let nb_first_intro = nb_prod - 1 - dyn_infos.nb_rec_hyps in
tclTHENLIST
[ (* We first introduce the variables *)
tclDO nb_first_intro
(intro_avoiding (Id.Set.of_list dyn_infos.rec_hyps))
; (* Then the equation itself *)
intro_using_then heq_id (* we get the fresh name with onLastHypId *)
(fun _ -> Proofview.tclUNIT ())
; onLastHypId (fun heq_id ->
tclTHENLIST
[ (* Then the new hypothesis *)
tclMAP introduction dyn_infos.rec_hyps
; observe_tac "after_introduction"
(Proofview.Goal.enter (fun g' -> let env = Proofview.Goal.env g' in let sigma = Proofview.Goal.sigma g' in (* We get infos on the equations introduced*) let new_term_value_eq =
Tacmach.pf_get_hyp_typ heq_id g' in (* compute the new value of the body *) let new_term_value = match EConstr.kind sigma new_term_value_eq with
| App (f, [|_; _; args2|]) -> args2
| _ ->
observe
(fun () -> str "cannot compute new term value : "
++ Tacmach.pr_gls g' ++ fnl ()
++ str "last hyp is"
++ pr_leconstr_env env sigma new_term_value_eq );
anomaly (Pp.str "cannot compute new term value.") in
tclTYPEOFTHEN term (fun sigma termtyp -> let fun_body =
mkLambda
( make_annot Anonymous ERelevance.relevant
, termtyp
, Termops.replace_term sigma term (mkRel 1)
dyn_infos.info ) in let new_body =
Reductionops.nf_betaiota env sigma
(mkApp (fun_body, [|new_term_value|])) in let new_infos =
{ dyn_infos with
info = new_body
; eq_hyps = heq_id :: dyn_infos.eq_hyps } in
clean_goal_with_heq ptes_infos continue_tac
new_infos))) ]) ])
let instantiate_hyps_with_args (do_prove : Id.t list -> unit Proofview.tactic)
hyps args_id = let args = Array.of_list (List.map mkVar args_id) in letopen Tacticals in let instantiate_one_hyp hid =
tclORELSE0 (* we instantiate the hyp if possible *)
(Proofview.Goal.enter (fun g -> let prov_hid = Tacmach.pf_get_new_id hid g in let c = mkApp (mkVar hid, args) in (* Check typing *)
tclTYPEOFTHEN c (fun _ _ ->
tclTHENLIST
[ pose_proof (Name prov_hid) c
; thin [hid]
; rename_hyp [(prov_hid, hid)] ]))) (* if not then we are in a mutual function block and this hyp is a recursive hyp on an other function.
We are not supposed to use it while proving this principle so that we can trash it
*) (* observe (str "Instantiation: removing hyp " ++ Ppconstr.pr_id hid); *)
(thin [hid]) in ifList.is_empty args_id then
tclTHENLIST
[ tclMAP (fun hyp_id -> h_reduce_with_zeta (Locusops.onHyp hyp_id)) hyps
; do_prove hyps ] else
tclTHENLIST
[ tclMAP (fun hyp_id -> h_reduce_with_zeta (Locusops.onHyp hyp_id)) hyps
; tclMAP instantiate_one_hyp hyps
; Proofview.Goal.enter (fun g -> let all_g_hyps_id = List.fold_right Id.Set.add
(Tacmach.pf_ids_of_hyps g)
Id.Set.empty in let remaining_hyps = List.filter (fun id -> Id.Set.mem id all_g_hyps_id) hyps in
do_prove remaining_hyps) ]
let build_proof (interactive_proof : bool) (fnames : Constant.t list) ptes_infos
dyn_infos : unit Proofview.tactic = letopen Tacticals in let rec build_proof_aux do_finalize dyn_infos : unit Proofview.tactic =
Proofview.Goal.enter (fun g -> let env = Proofview.Goal.env g in let sigma = Proofview.Goal.sigma g in (* observe (str "proving on " ++ Printer.pr_lconstr_env (pf_env g) term);*) match EConstr.kind sigma dyn_infos.info with
| Case (ci, u, pms, ct, iv, t, cb) -> let do_finalize_t dyn_info' =
Proofview.Goal.enter (fun g -> let t = dyn_info'.info in let dyn_infos =
{dyn_info' with info = mkCase (ci, u, pms, ct, iv, t, cb)} in let g_nb_prod =
nb_prod (Proofview.Goal.sigma g) (Proofview.Goal.concl g) in
tclTYPEOFTHEN t (fun _ type_of_term -> let term_eq =
make_refl_eq (Lazy.force refl_equal) type_of_term t in
tclTHENLIST
[ Generalize.generalize (term_eq :: List.map mkVar dyn_infos.rec_hyps)
; thin dyn_infos.rec_hyps
; pattern_option [(Locus.AllOccurrencesBut [1], t)] None
; observe_tac "toto"
(tclTHENLIST
[ Simple.case t
; Proofview.Goal.enter (fun g' -> let g'_nb_prod =
nb_prod (Proofview.Goal.sigma g')
(Proofview.Goal.concl g') in let nb_instantiate_partial =
g'_nb_prod - g_nb_prod in
observe_tac "treat_new_case"
(treat_new_case ptes_infos
nb_instantiate_partial
(build_proof do_finalize) t dyn_infos))
]) ])) in
build_proof do_finalize_t {dyn_infos with info = t}
| Lambda (n, t, b) -> ( match EConstr.kind sigma (Proofview.Goal.concl g) with
| Prod _ ->
tclTHEN intro
(Proofview.Goal.enter (fun g' -> letopen Context.Named.Declaration in let id = Tacmach.pf_last_hyp g' |> get_id in let new_term =
Reductionops.nf_betaiota (Proofview.Goal.env g')
(Proofview.Goal.sigma g')
(mkApp (dyn_infos.info, [|mkVar id|])) in let new_infos = {dyn_infos with info = new_term} in let do_prove new_hyps =
build_proof do_finalize
{ new_infos with
rec_hyps = new_hyps
; nb_rec_hyps = List.length new_hyps } in (* observe_tac "Lambda" *)
instantiate_hyps_with_args do_prove new_infos.rec_hyps [id] (* build_proof do_finalize new_infos g' *)))
| _ -> do_finalize dyn_infos )
| Cast (t, _, _) -> build_proof do_finalize {dyn_infos with info = t}
| Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _
|Int _ | Float _ | String _ ->
do_finalize dyn_infos
| App (_, _) -> ( let f, args = decompose_app_list sigma dyn_infos.info in match EConstr.kind sigma f with
| Int _ -> user_err Pp.(str "integer cannot be applied")
| Float _ -> user_err Pp.(str "float cannot be applied")
| String _ -> user_err Pp.(str "string cannot be applied")
| Array _ -> user_err Pp.(str "array cannot be applied")
| App _ ->
assert false(* we have collected all the app in decompose_app *)
| Proj _ -> assert false(*FIXME*)
| Var _ | Construct _ | Rel _ | Evar _ | Meta _ | Ind _ | Sort _
|Prod _ -> let new_infos = {dyn_infos with info = (f, args)} in
build_proof_args env sigma do_finalize new_infos
| Const (c, _) when not (List.exists (fun kn -> Environ.QConstant.equal env c kn) fnames) -> let new_infos = {dyn_infos with info = (f, args)} in (* Pp.msgnl (str "proving in " ++ pr_lconstr_env (pf_env g) dyn_infos.info); *)
build_proof_args env sigma do_finalize new_infos
| Const _ -> do_finalize dyn_infos
| Lambda _ -> let new_term = Reductionops.nf_beta env sigma dyn_infos.info in
build_proof do_finalize {dyn_infos with info = new_term}
| LetIn _ -> let new_infos =
{ dyn_infos with
info = Reductionops.nf_betaiotazeta env sigma dyn_infos.info } in
tclTHENLIST
[ tclMAP
(fun hyp_id -> h_reduce_with_zeta (Locusops.onHyp hyp_id))
dyn_infos.rec_hyps
; h_reduce_with_zeta Locusops.onConcl
; build_proof do_finalize new_infos ]
| Cast (b, _, _) -> build_proof do_finalize {dyn_infos with info = b}
| Case _ | Fix _ | CoFix _ -> let new_finalize dyn_infos = let new_infos = {dyn_infos with info = (dyn_infos.info, args)} in
build_proof_args env sigma do_finalize new_infos in
build_proof new_finalize {dyn_infos with info = f} )
| Fix _ | CoFix _ ->
user_err Pp.(str "Anonymous local (co)fixpoints are not handled yet")
| Proj _ -> user_err Pp.(str "Prod")
| Prod _ -> do_finalize dyn_infos
| LetIn _ -> let new_infos =
{ dyn_infos with
info = Reductionops.nf_betaiotazeta env sigma dyn_infos.info } in
tclTHENLIST
[ tclMAP
(fun hyp_id -> h_reduce_with_zeta (Locusops.onHyp hyp_id))
dyn_infos.rec_hyps
; h_reduce_with_zeta Locusops.onConcl
; build_proof do_finalize new_infos ]
| Rel _ -> anomaly (Pp.str "Free var in goal conclusion!")
| Array _ -> CErrors.user_err Pp.(str "Arrays not handled yet")) and build_proof do_finalize dyn_infos = (* observe (str "proving with "++Printer.pr_lconstr dyn_infos.info++ str " on goal " ++ pr_gls g); *)
Indfun_common.observe_tac ~header:(str "observation")
(fun env sigma ->
str "build_proof with " ++ pr_leconstr_env env sigma dyn_infos.info)
(build_proof_aux do_finalize dyn_infos) and build_proof_args env sigma do_finalize dyn_infos : unit Proofview.tactic = (* f_args' args *)
Proofview.Goal.enter (fun g -> let f_args', args = dyn_infos.info in let tac = match args with
| [] -> do_finalize {dyn_infos with info = f_args'}
| arg :: args -> (* observe (str "build_proof_args with arg := "++ pr_lconstr_env (pf_env g) arg++ *) (* fnl () ++ *) (* pr_goal (Tacmach.sig_it g) *) (* ); *) let do_finalize dyn_infos = let new_arg = dyn_infos.info in (* tclTRYD *)
build_proof_args env sigma do_finalize
{dyn_infos with info = (mkApp (f_args', [|new_arg|]), args)} in
build_proof do_finalize {dyn_infos with info = arg} in (* observe_tac "build_proof_args" *) tac) in let do_finish_proof dyn_infos = (* tclTRYD *) clean_goal_with_heq ptes_infos finish_proof dyn_infos in (* observe_tac "build_proof" *)
build_proof (clean_goal_with_heq ptes_infos do_finish_proof) dyn_infos
(* Proof of principles from structural functions *)
type static_fix_info =
{ idx : int
; name : Id.t
; types : types
; offset : int
; nb_realargs : int
; body_with_param : constr
; num_in_block : int }
let prove_rec_hyp_for_struct fix_info eq_hyps = letopen Tacticals in
tclTHEN
(rewrite_until_var fix_info.idx eq_hyps)
(Proofview.Goal.enter (fun g -> let _, pte_args =
destApp (Proofview.Goal.sigma g) (Proofview.Goal.concl g) in let rec_hyp_proof =
mkApp (mkVar fix_info.name, array_get_start pte_args) in
Tactics.exact_check rec_hyp_proof))
let generate_equation_lemma env evd fnames f fun_num nb_params nb_args rec_args_num
= letopen Tacticals in (* observe (str "nb_args := " ++ str (string_of_int nb_args)); *) (* observe (str "nb_params := " ++ str (string_of_int nb_params)); *) (* observe (str "rec_args_num := " ++ str (string_of_int (rec_args_num + 1) )); *) let f_def = Environ.lookup_constant (fst (destConst evd f)) env in let eq_lhs =
mkApp
( f
, Array.init (nb_params + nb_args) (fun i ->
mkRel (nb_params + nb_args - i)) ) in let f_body = match f_def.const_body with
| Def d -> d
| OpaqueDef _ | Primitive _ | Symbol _ | Undef _ ->
CErrors.user_err (Pp.str "Definition without a body") in let f_body = EConstr.of_constr f_body in let params, f_body_with_params = decompose_lambda_n evd nb_params f_body in let (_, num), (_, _, bodies) = destFix evd f_body_with_params in let fnames_with_params = let params = Array.init nb_params (fun i -> mkRel (nb_params - i)) in let fnames = List.rev (Array.to_list (Array.map (fun f -> mkApp (f, params)) fnames)) in
fnames in (* observe (str "fnames_with_params " ++ prlist_with_sep fnl pr_lconstr fnames_with_params); *) (* observe (str "body " ++ pr_lconstr bodies.(num)); *) let f_body_with_params_and_other_fun =
substl fnames_with_params bodies.(num) in (* observe (str "f_body_with_params_and_other_fun " ++ pr_lconstr f_body_with_params_and_other_fun); *) let eq_rhs =
Reductionops.nf_betaiotazeta env evd
(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 (* observe (str "eq_rhs " ++ pr_lconstr eq_rhs); *) let (type_ctxt, type_of_f), evd = let evd, t = Typing.type_of ~refresh:true env evd f in
(decompose_prod_n_decls evd (nb_params + nb_args) t, evd) in let eqn = mkApp (Lazy.force eq, [|type_of_f; eq_lhs; eq_rhs|]) in let lemma_type = it_mkProd_or_LetIn eqn type_ctxt in (* Pp.msgnl (str "lemma type " ++ Printer.pr_lconstr lemma_type ++ fnl () ++ str "f_body " ++ Printer.pr_lconstr f_body); *) let f_id = Label.to_id (Constant.label (fst (destConst evd f))) in let prove_replacement =
tclTHENLIST
[ tclDO (nb_params + rec_args_num + 1) intro
; observe_tac ""
(onNthHypId 1 (fun rec_id ->
tclTHENLIST
[ observe_tac "generalize_non_dep in generate_equation_lemma"
(generalize_non_dep rec_id)
; observe_tac "h_case" (simplest_case (mkVar rec_id))
; intros_reflexivity ])) ] in
(*i The next call to mk_equation_id is valid since we are
constructing the lemma Ensures by: obvious i*) let info = Declare.Info.make () in let cinfo =
Declare.CInfo.make ~name:(mk_equation_id f_id) ~typ:lemma_type () in let lemma = Declare.Proof.start ~cinfo ~info evd in let lemma, _ = Declare.Proof.by prove_replacement lemma in let (_ : _ list) =
Declare.Proof.save_regular ~proof:lemma ~opaque:Vernacexpr.Transparent
~idopt:None in
evd
let do_replace (evd : Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num
all_funs =
Proofview.Goal.enter (fun g -> let env = Proofview.Goal.env g in let equation_lemma = try let finfos = match find_Function_infos (fst (destConst !evd f)) (*FIXME*) with
| None -> raise Not_found
| Some finfos -> finfos in
mkConst (Option.get finfos.equation_lemma) with (Not_found | Option.IsNone) as e -> let f_id = Label.to_id (Constant.label (fst (destConst !evd f))) in (*i The next call to mk_equation_id is valid since we will construct the lemma Ensures by: obvious
i*) let equation_lemma_id = mk_equation_id f_id in
evd :=
generate_equation_lemma env !evd all_funs f fun_num (List.length params)
(List.length rev_args_id) rec_arg_num; let _ = match e with
| Option.IsNone -> let finfos = match find_Function_infos (fst (destConst !evd f)) with
| None -> raise Not_found
| Some finfos -> finfos in
update_Function
{ finfos with
equation_lemma =
Some
( match
Nametab.locate (qualid_of_ident equation_lemma_id) with
| GlobRef.ConstRef c -> c
| _ -> CErrors.anomaly (Pp.str "Not a constant.") ) }
| _ -> () in (* let res = Constrintern.construct_reference (pf_hyps g) equation_lemma_id in *) let env = Global.env () in let evd', res =
Evd.fresh_global env !evd
(Option.get (Constrintern.locate_reference
(qualid_of_ident equation_lemma_id))) in
evd := evd'; let sigma, _ =
Typing.type_of ~refresh:true env !evd res in
evd := sigma;
res in let nb_intro_to_do =
nb_prod (Proofview.Goal.sigma g) (Proofview.Goal.concl g) in letopen Tacticals in letopen Proofview.Notations in
tclTHEN
(tclDO nb_intro_to_do intro)
(Proofview.Goal.enter (fun g' -> let just_introduced = Tacticals.nLastDecls g' nb_intro_to_do in letopen Context.Named.Declaration in let just_introduced_id = List.map get_id just_introduced in (* Hack to synchronize the goal with the global env *)
(Proofview.Unsafe.tclSETENV (Global.env ())) <*>
(Equality.rewriteLR equation_lemma) <*>
(revert just_introduced_id))))
let prove_princ_for_struct (evd : Evd.evar_map ref) interactive_proof fun_num
fnames all_funs _nparams : unit Proofview.tactic = letopen Tacticals in
Proofview.Goal.enter (fun g -> let princ_type = Proofview.Goal.concl g in let env = Proofview.Goal.env g in let sigma = Proofview.Goal.sigma g in (* Pp.msgnl (str "princ_type " ++ Printer.pr_lconstr princ_type); *) (* Pp.msgnl (str "all_funs "); *) (* Array.iter (fun c -> Pp.msgnl (Printer.pr_lconstr c)) all_funs; *) let princ_info = compute_elim_sig sigma princ_type in let fresh_id = let avoid = ref (Tacmach.pf_ids_of_hyps g) in fun na -> let new_id = match na with
| Name id -> fresh_id !avoid (Id.to_string id)
| Anonymous -> fresh_id !avoid "H" in
avoid := new_id :: !avoid;
Name new_id in let fresh_decl = RelDecl.map_name fresh_id in let princ_info : elim_scheme =
{ princ_info with
params = List.map fresh_decl princ_info.params
; predicates = List.map fresh_decl princ_info.predicates
; branches = List.map fresh_decl princ_info.branches
; args = List.map fresh_decl princ_info.args } in let get_body const = let env = Global.env () in let body = Environ.lookup_constant const env in match body.Declarations.const_body with
| Def body -> let sigma = Evd.from_env env in
Tacred.cbv_norm_flags ~strong:true
(RedFlags.mkflags [RedFlags.fZETA])
env sigma (EConstr.of_constr body)
| Undef _ | Primitive _ | Symbol _ | OpaqueDef _ -> user_err Pp.(str "Cannot define a principle over an axiom ") in let fbody = get_body fnames.(fun_num) in let f_ctxt, f_body = decompose_lambda sigma fbody in let f_ctxt_length = List.length f_ctxt in let diff_params = princ_info.nparams - f_ctxt_length in let full_params, princ_params, fbody_with_full_params = if diff_params > 0 then let princ_params, full_params =
list_chop diff_params princ_info.params in
( full_params
, (* real params *)
princ_params
, (* the params of the principle which are not params of the function *)
substl (* function instantiated with real params *)
(List.map var_of_decl full_params)
f_body ) else let f_ctxt_other, f_ctxt_params = list_chop (-diff_params) f_ctxt in let f_body = compose_lam f_ctxt_other f_body in
( princ_info.params
, (* real params *)
[]
, (* all params are full params *)
substl (* function instantiated with real params *)
(List.map var_of_decl princ_info.params)
f_body ) in
observe
(fun () -> str "full_params := "
++ prlist_with_sep spc
(RelDecl.get_name %> Nameops.Name.get_id %> Ppconstr.pr_id)
full_params );
observe
(fun () -> str "princ_params := "
++ prlist_with_sep spc
(RelDecl.get_name %> Nameops.Name.get_id %> Ppconstr.pr_id)
princ_params );
observe
(fun () -> str "fbody_with_full_params := "
++ pr_leconstr_env (Global.env ()) !evd fbody_with_full_params ); let all_funs_with_full_params =
Array.map
(fun f -> applist (f, List.rev_map var_of_decl full_params))
all_funs in let fix_offset = List.length princ_params in let ptes_to_fix, infos = match EConstr.kind sigma fbody_with_full_params with
| Fix ((idxs, i), (names, typess, bodies)) -> let bodies_with_all_params =
Array.map
(fun body ->
Reductionops.nf_betaiota env sigma
(applist
( substl
(List.rev (Array.to_list all_funs_with_full_params))
body
, List.rev_map var_of_decl princ_params )))
bodies in let info_array =
Array.mapi
(fun i types -> let types =
prod_applist sigma types
(List.rev_map var_of_decl princ_params) in
{ idx = idxs.(i) - fix_offset
; name = Nameops.Name.get_id (fresh_id names.(i).binder_name)
; types
; offset = fix_offset
; nb_realargs = List.length (fst (decompose_lambda sigma bodies.(i)))
- fix_offset
; body_with_param = bodies_with_all_params.(i)
; num_in_block = i })
typess in let pte_to_fix, rev_info = List.fold_left_i
(fun i (acc_map, acc_info) decl -> let pte = RelDecl.get_name decl in let infos = info_array.(i) in let type_args, _ = decompose_prod sigma infos.types in let nargs = List.length type_args in let f =
applist
( mkConst fnames.(i)
, List.rev_map var_of_decl princ_info.params ) in let first_args =
Array.init nargs (fun i -> mkRel (nargs - i)) in let app_f = mkApp (f, first_args) in let pte_args = Array.to_list first_args @ [app_f] in let app_pte =
applist (mkVar (Nameops.Name.get_id pte), pte_args) in let body_with_param, num = let body = get_body fnames.(i) in let body_with_full_params =
Reductionops.nf_betaiota env sigma
(applist (body, List.rev_map var_of_decl full_params)) in match EConstr.kind sigma body_with_full_params with
| Fix ((_, num), (_, _, bs)) ->
( Reductionops.nf_betaiota env sigma
(applist
( substl
(List.rev
(Array.to_list all_funs_with_full_params))
bs.(num)
, List.rev_map var_of_decl princ_params ))
, num )
| _ -> user_err Pp.(str "Not a mutual block") in let info =
{ infos with
types = compose_prod type_args app_pte
; body_with_param
; num_in_block = num } in (* observe (str "binding " ++ Ppconstr.pr_id (Nameops.Name.get_id pte) ++ *) (* str " to " ++ Ppconstr.pr_id info.name); *)
( Id.Map.add (Nameops.Name.get_id pte) info acc_map
, info :: acc_info ))
0 (Id.Map.empty, [])
(List.rev princ_info.predicates) in
(pte_to_fix, List.rev rev_info)
| _ -> (Id.Map.empty, []) in let mk_fixes : unit Proofview.tactic = let pre_info, infos = list_chop fun_num infos in match (pre_info, infos) with
| _, [] -> Proofview.tclUNIT ()
| _, this_fix_info :: others_infos -> let other_fix_infos = List.map
(fun fi -> (fi.name, fi.idx + 1, fi.types))
(pre_info @ others_infos) in ifList.is_empty other_fix_infos then if this_fix_info.idx + 1 = 0 then Proofview.tclUNIT () (* Someone tries to defined a principle on a fully parametric definition declared as a fixpoint (strange but ....) *) else
Indfun_common.observe_tac ~header:(str "observation")
(fun _ _ -> str "h_fix " ++ int (this_fix_info.idx + 1))
(fix this_fix_info.name (this_fix_info.idx + 1)) else
Tactics.mutual_fix this_fix_info.name (this_fix_info.idx + 1)
other_fix_infos 0 in let first_tac : unit Proofview.tactic = (* every operations until fix creations *) (* names are already refreshed *)
tclTHENLIST
[ observe_tac "introducing params"
(intros_mustbe_force (List.rev_map id_of_decl princ_info.params))
; observe_tac "introducing predicates"
(intros_mustbe_force
(List.rev_map id_of_decl princ_info.predicates))
; observe_tac "introducing branches"
(intros_mustbe_force
(List.rev_map id_of_decl princ_info.branches))
; observe_tac "building fixes" mk_fixes ] in let intros_after_fixes : unit Proofview.tactic =
Proofview.Goal.enter (fun gl -> let sigma = Proofview.Goal.sigma gl in let ccl = Proofview.Goal.concl gl in let ctxt, pte_app = decompose_prod_decls sigma ccl in let pte, pte_args = decompose_app_list sigma pte_app in try let pte = try destVar sigma pte with DestKO -> anomaly (Pp.str "Property is not a variable.") in let fix_info = Id.Map.find pte ptes_to_fix in let nb_args = fix_info.nb_realargs in
tclTHENLIST
[ (* observe_tac ("introducing args") *)
tclDO nb_args intro
; Proofview.Goal.enter (fun g -> (* replacement of the function by its body *) let args = Tacticals.nLastDecls g nb_args in let fix_body = fix_info.body_with_param in (* observe (str "fix_body := "++ pr_lconstr_env (pf_env gl) fix_body); *) letopen Context.Named.Declaration in let args_id = List.map get_id args in let dyn_infos =
{ nb_rec_hyps = -100
; rec_hyps = []
; info =
Reductionops.nf_betaiota (Proofview.Goal.env g)
(Proofview.Goal.sigma g)
(applist (fix_body, List.rev_map mkVar args_id))
; eq_hyps = [] } in
tclTHENLIST
[ observe_tac "do_replace"
(do_replace evd full_params
(fix_info.idx + List.length princ_params)
( args_id
@ List.map
(RelDecl.get_name %> Nameops.Name.get_id)
princ_params )
all_funs.(fix_info.num_in_block)
fix_info.num_in_block all_funs)
; (let do_prove =
build_proof interactive_proof
(Array.to_list fnames)
(Id.Map.map prove_rec_hyp ptes_to_fix) in let prove_tac branches = let dyn_infos =
{ dyn_infos with
rec_hyps = branches
; nb_rec_hyps = List.length branches } in
observe_tac "cleaning"
(clean_goal_with_heq
(Id.Map.map prove_rec_hyp ptes_to_fix)
do_prove dyn_infos) in (* observe (str "branches := " ++ *) (* prlist_with_sep spc (fun decl -> Ppconstr.pr_id (id_of_decl decl)) princ_info.branches ++ fnl () ++ *) (* str "args := " ++ prlist_with_sep spc Ppconstr.pr_id args_id *)
(* ); *) (* observe_tac "instancing" *)
instantiate_hyps_with_args prove_tac
(List.rev_map id_of_decl princ_info.branches)
(List.rev args_id)) ]) ] with Not_found -> let nb_args = min princ_info.nargs (List.length ctxt) in
tclTHENLIST
[ tclDO nb_args intro
; Proofview.Goal.enter (fun g -> let env = Proofview.Goal.env g in let sigma = Proofview.Goal.sigma g in (* replacement of the function by its body *) let args = Tacticals.nLastDecls g nb_args in letopen Context.Named.Declaration in let args_id = List.map get_id args in let dyn_infos =
{ nb_rec_hyps = -100
; rec_hyps = []
; info =
Reductionops.nf_betaiota env sigma
(applist
( fbody_with_full_params
, List.rev_map var_of_decl princ_params
@ List.rev_map mkVar args_id ))
; eq_hyps = [] } in let fname =
destConst sigma
(fst
(decompose_app_list sigma (List.hd (List.rev pte_args)))) in
tclTHENLIST
[ unfold_in_concl
[ ( Locus.AllOccurrences
, Evaluable.EvalConstRef (fst fname) ) ]
; (let do_prove =
build_proof interactive_proof
(Array.to_list fnames)
(Id.Map.map prove_rec_hyp ptes_to_fix) in let prove_tac branches = let dyn_infos =
{ dyn_infos with
rec_hyps = branches
; nb_rec_hyps = List.length branches } in
clean_goal_with_heq
(Id.Map.map prove_rec_hyp ptes_to_fix)
do_prove dyn_infos in
instantiate_hyps_with_args prove_tac
(List.rev_map id_of_decl princ_info.branches)
(List.rev args_id)) ]) ]) in
tclTHEN first_tac intros_after_fixes)
(* Proof of principles of general functions *) (* let hrec_id = Recdef.hrec_id *) (* and acc_inv_id = Recdef.acc_inv_id *) (* and ltof_ref = Recdef.ltof_ref *) (* and acc_rel = Recdef.acc_rel *) (* and well_founded = Recdef.well_founded *) (* and list_rewrite = Recdef.list_rewrite *) (* and evaluable_of_global_reference = Recdef.evaluable_of_global_reference *)
let prove_with_tcc tcc_lemma_constr eqs : unit Proofview.tactic = letopen Tacticals in match !tcc_lemma_constr with
| Undefined -> anomaly (Pp.str "No tcc proof !!")
| Value lemma -> (* let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in *) (* let ids = hid::pf_ids_of_hyps gls in *)
tclTHENLIST
[ (* generalize [lemma]; *) (* h_intro hid; *) (* Elim.h_decompose_and (mkVar hid); *)
tclTRY (list_rewrite true eqs)
; (* (fun g -> *) (* let ids' = pf_ids_of_hyps g in *) (* let ids = List.filter (fun id -> not (List.mem id ids)) ids' in *) (* rewrite *) (* ) *)
Eauto.gen_eauto ~depth:5 [] (Some []) ]
| Not_needed -> Proofview.tclUNIT ()
let backtrack_eqs_until_hrec hrec eqs : unit Proofview.tactic = letopen Tacticals in
Proofview.Goal.enter (fun gls -> let sigma = Proofview.Goal.sigma gls in let eqs = List.map mkVar eqs in let rewrite = tclFIRST (List.map Equality.rewriteRL eqs) in let _, hrec_concl =
decompose_prod sigma (Tacmach.pf_get_hyp_typ hrec gls) in let f_app = Array.last (snd (destApp sigma hrec_concl)) in let f = fst (destApp sigma f_app) in let rec backtrack () : unit Proofview.tactic =
Proofview.Goal.enter (fun g -> let sigma = Proofview.Goal.sigma gls in let f_app =
Array.last (snd (destApp sigma (Proofview.Goal.concl g))) in match EConstr.kind sigma f_app with
| App (f', _) when eq_constr sigma f' f -> Proofview.tclUNIT ()
| _ -> tclTHEN rewrite (backtrack ())) in
backtrack ())
let rec rewrite_eqs_in_eqs eqs = letopen Tacticals in match eqs with
| [] -> Proofview.tclUNIT ()
| eq :: eqs ->
tclTHEN
(tclMAP
(fun id ->
observe_tac
(Format.sprintf "rewrite %s in %s " (Id.to_string eq)
(Id.to_string id))
(tclTRY
(Equality.general_rewrite ~where:(Some id) ~l2r:true Locus.AllOccurrences ~freeze:true (* dep proofs also: *) ~dep:true ~with_evars:false (mkVar eq, Tactypes.NoBindings))))
eqs)
(rewrite_eqs_in_eqs eqs)
let is_valid_hypothesis sigma predicates_name = let predicates_name = List.fold_right Id.Set.add predicates_name Id.Set.empty in let is_pte typ = if isApp sigma typ then let pte, _ = destApp sigma typ in if isVar sigma pte then Id.Set.mem (destVar sigma pte) predicates_name elsefalse elsefalse in let rec is_valid_hypothesis typ =
is_pte typ
|| match EConstr.kind sigma typ with
| Prod (_, pte, typ') -> is_pte pte && is_valid_hypothesis typ'
| _ -> false in
is_valid_hypothesis
let prove_principle_for_gen (f_ref, functional_ref, eq_ref) tcc_lemma_ref is_mes
rec_arg_num rec_arg_type relation =
Proofview.Goal.enter (fun gl -> let sigma = Proofview.Goal.sigma gl in let princ_type = Proofview.Goal.concl gl in let princ_info = compute_elim_sig sigma princ_type in let fresh_id = let avoid = ref (Tacmach.pf_ids_of_hyps gl) in fun na -> let new_id = match na with
| Name id -> fresh_id !avoid (Id.to_string id)
| Anonymous -> fresh_id !avoid "H" in
avoid := new_id :: !avoid;
Name new_id in let fresh_decl = map_name fresh_id in let princ_info : elim_scheme =
{ princ_info with
params = List.map fresh_decl princ_info.params
; predicates = List.map fresh_decl princ_info.predicates
; branches = List.map fresh_decl princ_info.branches
; args = List.map fresh_decl princ_info.args } in let wf_tac = if is_mes thenfun b ->
Recdef.tclUSER_if_not_mes Tacticals.tclIDTAC b None elsefun _ -> prove_with_tcc tcc_lemma_ref [] in let real_rec_arg_num = rec_arg_num - princ_info.nparams in let npost_rec_arg = princ_info.nargs - real_rec_arg_num + 1 in (* observe ( *) (* str "princ_type := " ++ pr_lconstr princ_type ++ fnl () ++ *) (* str "princ_info.nparams := " ++ int princ_info.nparams ++ fnl () ++ *)
(* str "princ_info.nargs := " ++ int princ_info.nargs ++ fnl () ++ *) (* str "rec_arg_num := " ++ int rec_arg_num ++ fnl() ++ *) (* str "real_rec_arg_num := " ++ int real_rec_arg_num ++ fnl () ++ *) (* str "npost_rec_arg := " ++ int npost_rec_arg ); *) let post_rec_arg, pre_rec_arg =
Util.List.chop npost_rec_arg princ_info.args in let rec_arg_id = matchList.rev post_rec_arg with
| ( LocalAssum ({binder_name = Name id}, _)
| LocalDef ({binder_name = Name id}, _, _) )
:: _ ->
id
| _ -> assert false in (* observe (str "rec_arg_id := " ++ pr_lconstr (mkVar rec_arg_id)); *) let subst_constrs = List.map
(get_name %> Nameops.Name.get_id %> mkVar)
(pre_rec_arg @ princ_info.params) in let relation = substl subst_constrs relation in let input_type = substl subst_constrs rec_arg_type in let wf_thm_id =
Nameops.Name.get_id (fresh_id (Name (Id.of_string "wf_R"))) in let acc_rec_arg_id =
Nameops.Name.get_id
(fresh_id (Name (Id.of_string ("Acc_" ^ Id.to_string rec_arg_id)))) in letopen Tacticals in let revert l =
tclTHEN (Generalize.generalize (List.map mkVar l)) (clear l) in let fix_id = Nameops.Name.get_id (fresh_id (Name hrec_id)) in let prove_rec_arg_acc = (* observe_tac "prove_rec_arg_acc" *)
tclCOMPLETE
(tclTHEN
(assert_by (Name wf_thm_id)
(mkApp (delayed_force well_founded, [|input_type; relation|])) (* observe_tac "prove wf" *)
(tclCOMPLETE (wf_tac is_mes)))
((* observe_tac *) (* "apply wf_thm" *)
Tactics.Simple.apply
(mkApp (mkVar wf_thm_id, [|mkVar rec_arg_id|])))) in let args_ids = List.map (get_name %> Nameops.Name.get_id) princ_info.args in let lemma = match !tcc_lemma_ref with
| Undefined -> user_err Pp.(str "No tcc proof !!")
| Value lemma -> EConstr.of_constr lemma
| Not_needed ->
EConstr.of_constr
( UnivGen.constr_of_monomorphic_global (Global.env ())
@@ Rocqlib.lib_ref "core.True.I" ) in (* let rec list_diff del_list check_list = *) (* match del_list with *) (* [] -> *) (* [] *) (* | f::r -> *) (* if List.mem f check_list then *) (* list_diff r check_list *) (* else *) (* f::(list_diff r check_list) *) (* in *) let tcc_list = ref [] in let start_tac =
Proofview.Goal.enter (fun gls -> let hyps = Tacmach.pf_ids_of_hyps gls in let hid =
next_ident_away_in_goal (Global.env ()) (Id.of_string "prov")
(Id.Set.of_list hyps) in
tclTHENLIST
[ Generalize.generalize [lemma]
; Simple.intro hid
; Elim.h_decompose_and (mkVar hid)
; Proofview.Goal.enter (fun g -> let new_hyps = Tacmach.pf_ids_of_hyps g in
tcc_list := List.rev (List.subtract Id.equal new_hyps (hid :: hyps)); ifList.is_empty !tcc_list thenbegin
tcc_list := [hid];
Proofview.tclUNIT () end else clear [hid]) ]) in
tclTHENLIST
[ observe_tac "start_tac" start_tac
; h_intros
(List.rev_map
(get_name %> Nameops.Name.get_id)
( princ_info.args @ princ_info.branches @ princ_info.predicates
@ princ_info.params ))
; assert_by (Name acc_rec_arg_id)
(mkApp
( delayed_force acc_rel
, [|input_type; relation; mkVar rec_arg_id|] ))
prove_rec_arg_acc
; revert (List.rev (acc_rec_arg_id :: args_ids))
; fix fix_id (List.length args_ids + 1)
; h_intros (List.rev (acc_rec_arg_id :: args_ids))
; Equality.rewriteLR (mkConst eq_ref)
; Proofview.Goal.enter (fun gl' -> let body = let _, args =
destApp (Proofview.Goal.sigma gl') (Proofview.Goal.concl gl') in
Array.last args in let body_info rec_hyps =
{ nb_rec_hyps = List.length rec_hyps
; rec_hyps
; eq_hyps = []
; info = body }
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.13 Sekunden
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
