open Printer open CErrors open Util open Constr open EConstr open Vars open Namegen open Names open Pp open Tacmach open Termops open Tacticals open Tactics open Indfun_common open Libnames open Globnames open Context.Rel.Declaration module RelDecl = Context.Rel.Declaration (* let msgnl = Pp.msgnl *) (* let observe strm = if do_observe () then Pp.msg_debug strm else () let do_observe_tac s tac g = try let v = tac g in (* msgnl (goal ++ fnl () ++ (str s)++(str " ")++(str "finished")); *) v with e -> let e = ExplainErr.process_vernac_interp_error e in let goal = begin try (Printer.pr_goal g) with _ -> assert false end in msg_debug (str "observation "++ s++str " raised exception " ++ Errors.print e ++ str " on goal " ++ goal ); raise e;; let observe_tac_stream s tac g = if do_observe () then do_observe_tac s tac g else tac g let observe_tac s tac g = observe_tac_stream (str s) tac g *) let pr_leconstr_fp = let sigma, env = Pfedit.get_current_context () in Printer.pr_leconstr_env env sigma let debug_queue = Stack.create () let rec print_debug_queue e = if not (Stack.is_empty debug_queue) then begin let lmsg,goal = Stack.pop debug_queue in let _ = match e with | Some e -> Feedback.msg_debug (hov 0 (lmsg ++ (str " raised exception " ++ CErrors.print e) ++ str " on goal" ++ fnl() ++ goal)) | None -> begin Feedback.msg_debug (str " from " ++ lmsg ++ str " on goal" ++ fnl() ++ goal); end in print_debug_queue None ; end let observe strm = if do_observe () then Feedback.msg_debug strm else () let do_observe_tac s tac g = let goal = Printer.pr_goal g in let lmsg = (str "observation : ") ++ s in Stack.push (lmsg,goal) debug_queue; try let v = tac g in ignore(Stack.pop debug_queue); v with reraise -> let reraise = CErrors.push reraise in if not (Stack.is_empty debug_queue) then print_debug_queue (Some (fst (ExplainErr.process_vernac_interp_error reraise))); iraise reraise let observe_tac_stream s tac g = if do_observe () then do_observe_tac s tac g else tac g let observe_tac s = observe_tac_stream (str s) let list_chop ?(msg="") n l = try List.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 -> Tacmach.tactic); is_valid : constr -> bool } type ptes_info = pte_info Id.Map.t type 'a dynamic_info = { nb_rec_hyps : int; rec_hyps : Id.t list ; eq_hyps : Id.t list; info : 'a } type body_info = constr dynamic_info let finish_proof dynamic_infos g = observe_tac "finish" (Proofview.V82.of_tactic assumption) g let refine c = Tacmach.refine c let thin l = Proofview.V82.of_tactic (Tactics.clear l) let eq_constr sigma u v = EConstr.eq_constr_nounivs sigma u v let is_trivial_eq sigma t = let res = try begin 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 end 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 rec incompatible_constructor_terms sigma t1 t2 = let c1,arg1 = decompose_app sigma t1 and c2,arg2 = decompose_app sigma t2 in (not (eq_constr sigma t1 t2)) && isConstruct sigma c1 && isConstruct sigma c2 && ( not (eq_constr sigma c1 c2) || List.exists2 (incompatible_constructor_terms sigma) arg1 arg2 ) let is_incompatible_eq 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 (str "is_incompatible_eq " ++ pr_leconstr_fp t); res let change_hyp_with_using msg hyp_id t tac : tactic = fun g -> let prov_id = pf_get_new_id hyp_id g in tclTHENS ((* observe_tac msg *) Proofview.V82.of_tactic (assert_by (Name prov_id) t (Proofview.V82.tactic (tclCOMPLETE tac)))) [tclTHENLIST [ (* observe_tac "change_hyp_with_using thin" *) (thin [hyp_id]); (* observe_tac "change_hyp_with_using rename " *) (Proofview.V82.of_tactic (rename_hyp [prov_id,hyp_id])) ]] g exception TOREMOVE let prove_trivial_eq h_id context (constructor,type_of_term,term) = let nb_intros = List.length context in tclTHENLIST [ tclDO nb_intros (Proofview.V82.of_tactic intro); (* introducing context *) (fun g -> let context_hyps = fst (list_chop ~msg:"prove_trivial_eq : " nb_intros (pf_ids_of_hyps g)) 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 refine to_refine g ) ] let find_rectype env sigma c = let (t, l) = decompose_app sigma (Reductionops.whd_betaiotazeta sigma c) in match EConstr.kind sigma t with | Ind ind -> (t, l) | Construct _ -> (t,l) | _ -> raise Not_found let isAppConstruct ?(env=Global.env ()) sigma t = try let t',l = find_rectype env sigma t in observe (str "isAppConstruct : " ++ Printer.pr_leconstr_env env sigma t ++ str " -> " ++ Printer.pr_leconstr_env env sigma (applist (t',l))); true with Not_found -> false let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta *) Reductionops.clos_norm_flags CClosure.betaiotazeta Environ.empty_env Evd.empty exception NoChange let change_eq env sigma hyp_id (context:rel_context) x t end_of_type = let nochange ?t' msg = begin observe (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; end in let eq_constr c1 c2 = Evarconv.e_conv env (ref sigma) c1 c2 in if not (noccurn sigma 1 end_of_type) then nochange "dependent"; (* if end_of_type depends on this term we don't touch it *) if not (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) else if (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 if not ((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 begin try let t1' = Int.Map.find t2 sub in if not (eq_constr t1 t1') then nochange "twice bound variable"; sub with Not_found -> assert (closed0 sigma t1); Int.Map.add t2 t1 sub end else if isAppConstruct sigma t1 && isAppConstruct sigma t2 then begin let c1,args1 = find_rectype env sigma t1 and c2,args2 = find_rectype env sigma t2 in if not (eq_constr c1 c2) then nochange "cannot solve (diff)"; List.fold_left2 compute_substitution sub args1 args2 end else if (eq_constr t1 t2) then sub else nochange ~t':(make_refl_eq constructor (Reductionops.whd_all env sigma t1) t2) "cannot solve (diff)" in let sub = compute_substitution Int.Map.empty (snd t1) (snd t2) in let sub = 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 *) let sub = Int.Map.bindings sub in 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(Anonymous,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 sub in if is_local_def decl then anomaly (Pp.str "can not redefine a rel!"); (pop end_of_type,ctxt_size,mkLetIn (RelDecl.get_name 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_assum sigma ctxt_size new_type_of_hyp in let prove_new_hyp : tactic = tclTHEN (tclDO ctxt_size (Proofview.V82.of_tactic intro)) (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, _ = pf_apply Typing.type_of g to_refine in tclTHEN (Refiner.tclEVARS evm) (refine to_refine) g ) 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 else false else false let isLetIn sigma t = match EConstr.kind sigma t with | LetIn _ -> true | _ -> false let h_reduce_with_zeta cl = Proofview.V82.of_tactic (reduce (Genredexpr.Cbv {Redops.all_flags with Genredexpr.rDelta = false; }) cl) let rewrite_until_var arg_num eq_ids : tactic = (* 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 = project g in let _,args = destApp sigma (pf_concl g) in not ((isConstruct sigma args.(arg_num)) || isAppConstruct sigma args.(arg_num)) in let rec do_rewrite eq_ids g = if test_var g then tclIDTAC g else match eq_ids with | [] -> anomaly (Pp.str "Cannot find a way to prove recursive property."); | eq_id::eq_ids -> tclTHEN (tclTRY (Proofview.V82.of_tactic (Equality.rewriteRL (mkVar eq_id)))) (do_rewrite eq_ids) g 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 coq_False = EConstr.of_constr (Universes.constr_of_global @@ Coqlib.build_coq_False ()) in let coq_True = EConstr.of_constr (Universes.constr_of_global @@ Coqlib.build_coq_True ()) in let coq_I = EConstr.of_constr (Universes.constr_of_global @@ Coqlib.build_coq_I ()) in let rec scan_type context type_of_hyp : 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 = nf_betaiotazeta real_type_of_hyp in (* length of context didn't change ? *) let new_context,new_typ_of_hyp = decompose_prod_n_assum 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 ] else if isProd sigma type_of_hyp then begin 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 begin 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 (Proofview.V82.of_tactic intro); (fun g -> let context_hyps_ids = fst (list_chop ~msg:"rec hyp : context_hyps" context_length (pf_ids_of_hyps g)) in let rec_pte_id = pf_get_new_id rec_pte_id g in let to_refine = applist(mkVar hyp_id, List.rev_map mkVar (rec_pte_id::context_hyps_ids) ) in (* observe_tac "rec hyp " *) (tclTHENS (Proofview.V82.of_tactic (assert_before (Name rec_pte_id) t_x)) [ (* observe_tac "prove rec hyp" *) (prove_rec_hyp eq_hyps); (* observe_tac "prove rec hyp" *) (refine to_refine) ]) g ) ] 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' ] end else if eq_constr sigma t_x coq_False then begin (* observe (str "Removing : "++ Ppconstr.pr_id hyp_id++ *) (* str " since it has False in its preconds " *) (* ); *) raise TOREMOVE; (* False -> .. useless *) end else if is_incompatible_eq sigma t_x then raise TOREMOVE (* t_x := C1 ... = C2 ... *) else if eq_constr sigma t_x coq_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 (Proofview.V82.of_tactic intro); (fun g -> let context_hyps = fst (list_chop ~msg:"removing True : context_hyps "nb_intro (pf_ids_of_hyps g)) in let to_refine = applist (mkVar hyp_id, List.rev (coq_I::List.map mkVar context_hyps) ) in refine to_refine g ) ] 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' ] else if 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 begin 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' end end else tclIDTAC in try scan_type [] (Typing.unsafe_type_of env sigma (mkVar hyp_id)), [hyp_id] with TOREMOVE -> thin [hyp_id],[] let clean_goal_with_heq ptes_infos continue_tac (dyn_infos:body_info) = fun g -> let env = pf_env g and sigma = project 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) ] g let heq_id = Id.of_string "Heq" let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos = 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 (Proofview.V82.of_tactic (intro_avoiding (Id.Set.of_list dyn_infos.rec_hyps))); (* Then the equation itself *) Proofview.V82.of_tactic (intro_using heq_id); onLastHypId (fun heq_id -> tclTHENLIST [ (* Then the new hypothesis *) tclMAP (fun id -> Proofview.V82.of_tactic (introduction ~check:false id)) dyn_infos.rec_hyps; observe_tac "after_introduction" (fun g' -> (* We get infos on the equations introduced*) let new_term_value_eq = pf_unsafe_type_of g' (mkVar heq_id) in (* compute the new value of the body *) let new_term_value = match EConstr.kind (project g') new_term_value_eq with | App(f,[| _;_;args2 |]) -> args2 | _ -> observe (str "cannot compute new term value : " ++ pr_gls g' ++ fnl () ++ str "last hyp is" ++ pr_leconstr_env (pf_env g') (project g') new_term_value_eq ); anomaly (Pp.str "cannot compute new term value.") in let fun_body = mkLambda(Anonymous, pf_unsafe_type_of g' term, Termops.replace_term (project g') term (mkRel 1) dyn_infos.info ) in let new_body = pf_nf_betaiota g' (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 g' )]) ] g let my_orelse tac1 tac2 g = try tac1 g with e when CErrors.noncritical e -> (* observe (str "using snd tac since : " ++ CErrors.print e); *) tac2 g let instanciate_hyps_with_args (do_prove:Id.t list -> tactic) hyps args_id = let args = Array.of_list (List.map mkVar args_id) in let instanciate_one_hyp hid = my_orelse ( (* we instanciate the hyp if possible *) fun g -> let prov_hid = pf_get_new_id hid g in let c = mkApp(mkVar hid,args) in let evm, _ = pf_apply Typing.type_of g c in tclTHENLIST[ Refiner.tclEVARS evm; Proofview.V82.of_tactic (pose_proof (Name prov_hid) c); thin [hid]; Proofview.V82.of_tactic (rename_hyp [prov_hid,hid]) ] g ) ( (* 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 *) (fun g -> (* observe (str "Instanciation: removing hyp " ++ Ppconstr.pr_id hid); *) thin [hid] g ) ) in if List.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 instanciate_one_hyp hyps; (fun g -> let all_g_hyps_id = List.fold_right Id.Set.add (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 g ) ] let build_proof (interactive_proof:bool) (fnames:Constant.t list) ptes_infos dyn_infos : tactic = let rec build_proof_aux do_finalize dyn_infos : tactic = fun g -> let env = pf_env g in let sigma = project g in (* observe (str "proving on " ++ Printer.pr_lconstr_env (pf_env g) term);*) match EConstr.kind sigma dyn_infos.info with | Case(ci,ct,t,cb) -> let do_finalize_t dyn_info' = fun g -> let t = dyn_info'.info in let dyn_infos = {dyn_info' with info = mkCase(ci,ct,t,cb)} in let g_nb_prod = nb_prod (project g) (pf_concl g) in let type_of_term = pf_unsafe_type_of g t in let term_eq = make_refl_eq (Lazy.force refl_equal) type_of_term t in tclTHENLIST [ Proofview.V82.of_tactic (generalize (term_eq::(List.map mkVar dyn_infos.rec_hyps))); thin dyn_infos.rec_hyps; Proofview.V82.of_tactic (pattern_option [Locus.AllOccurrencesBut [1],t] None); (fun g -> observe_tac "toto" ( tclTHENLIST [Proofview.V82.of_tactic (Simple.case t); (fun g' -> let g'_nb_prod = nb_prod (project g') (pf_concl g') in let nb_instanciate_partial = g'_nb_prod - g_nb_prod in observe_tac "treat_new_case" (treat_new_case ptes_infos nb_instanciate_partial (build_proof do_finalize) t dyn_infos) g' ) ]) g ) ] g in build_proof do_finalize_t {dyn_infos with info = t} g | Lambda(n,t,b) -> begin match EConstr.kind sigma (pf_concl g) with | Prod _ -> tclTHEN (Proofview.V82.of_tactic intro) (fun g' -> let open Context.Named.Declaration in let id = pf_last_hyp g' |> get_id in let new_term = pf_nf_betaiota 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" *) (instanciate_hyps_with_args do_prove new_infos.rec_hyps [id]) g' (* build_proof do_finalize new_infos g' *) ) g | _ -> do_finalize dyn_infos g end | Cast(t,_,_) -> build_proof do_finalize {dyn_infos with info = t} g | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ -> do_finalize dyn_infos g | App(_,_) -> let f,args = decompose_app sigma dyn_infos.info in begin match EConstr.kind sigma f with | 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 do_finalize new_infos g | Const (c,_) when not (List.mem_f Constant.equal c 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 do_finalize new_infos g | Const _ -> do_finalize dyn_infos g | Lambda _ -> let new_term = Reductionops.nf_beta env sigma dyn_infos.info in build_proof do_finalize {dyn_infos with info = new_term} g | LetIn _ -> let new_infos = { dyn_infos with info = nf_betaiotazeta 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 ] g | Cast(b,_,_) -> build_proof do_finalize {dyn_infos with info = b } g | Case _ | Fix _ | CoFix _ -> let new_finalize dyn_infos = let new_infos = { dyn_infos with info = dyn_infos.info,args } in build_proof_args do_finalize new_infos in build_proof new_finalize {dyn_infos with info = f } g end | 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 g | LetIn _ -> let new_infos = { dyn_infos with info = nf_betaiotazeta 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 ] g | Rel _ -> anomaly (Pp.str "Free var in goal conclusion!") and build_proof do_finalize dyn_infos g = (* observe (str "proving with "++Printer.pr_lconstr dyn_infos.info++ str " on goal " ++ pr_gls g); *) observe_tac_stream (str "build_proof with " ++ pr_leconstr_fp dyn_infos.info ) (build_proof_aux do_finalize dyn_infos) g and build_proof_args do_finalize dyn_infos (* f_args' args *) :tactic = fun g -> let (f_args',args) = dyn_infos.info in let tac : tactic = fun g -> match args with | [] -> do_finalize {dyn_infos with info = f_args'} g | 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 do_finalize {dyn_infos with info = (mkApp(f_args',[|new_arg|])), args} ) in build_proof do_finalize {dyn_infos with info = arg } g in (* observe_tac "build_proof_args" *) (tac ) g 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 = (fun eq_hyps -> tclTHEN (rewrite_until_var (fix_info.idx) eq_hyps) (fun g -> let _,pte_args = destApp (project g) (pf_concl g) in let rec_hyp_proof = mkApp(mkVar fix_info.name,array_get_start pte_args) in refine rec_hyp_proof g )) let prove_rec_hyp fix_info = { proving_tac = prove_rec_hyp_for_struct fix_info ; is_valid = fun _ -> true } let generalize_non_dep hyp g = (* observe (str "rec id := " ++ Ppconstr.pr_id hyp); *) let hyps = [hyp] in let env = Global.env () in let hyp_typ = pf_unsafe_type_of g (mkVar hyp) in let to_revert,_ = let open Context.Named.Declaration in Environ.fold_named_context_reverse (fun (clear,keep) decl -> let decl = map_named_decl EConstr.of_constr decl in let hyp = get_id decl in if Id.List.mem hyp hyps || List.exists (Termops.occur_var_in_decl env (project g) hyp) keep || Termops.occur_var env (project g) hyp hyp_typ || Termops.is_section_variable hyp (* should be dangerous *) then (clear,decl::keep) else (hyp::clear,keep)) ~init:([],[]) (pf_env g) in (* observe (str "to_revert := " ++ prlist_with_sep spc Ppconstr.pr_id to_revert); *) tclTHEN ((* observe_tac "h_generalize" *) (Proofview.V82.of_tactic (generalize (List.map mkVar to_revert) ))) ((* observe_tac "thin" *) (thin to_revert)) g let id_of_decl = RelDecl.get_name %> Nameops.Name.get_id let var_of_decl = id_of_decl %> mkVar let revert idl = tclTHEN (Proofview.V82.of_tactic (generalize (List.map mkVar idl))) (thin idl) let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num = (* 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 = Global.lookup_constant (fst (destConst evd f)) in let eq_lhs = mkApp(f,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i))) in let (f_body, _) = Option.get (Global.body_of_constant_body f_def) in let f_body = EConstr.of_constr f_body in let params,f_body_with_params = decompose_lam_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 = 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 (* observe (str "eq_rhs " ++ pr_lconstr eq_rhs); *) let (type_ctxt,type_of_f),evd = let evd,t = Typing.type_of ~refresh:true (Global.env ()) evd f in decompose_prod_n_assum 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) (Proofview.V82.of_tactic intro); observe_tac "" (fun g -> let rec_id = pf_nth_hyp_id g 1 in tclTHENLIST [observe_tac "generalize_non_dep in generate_equation_lemma" (generalize_non_dep rec_id); observe_tac "h_case" (Proofview.V82.of_tactic (simplest_case (mkVar rec_id))); (Proofview.V82.of_tactic intros_reflexivity)] g ) ] in (* Pp.msgnl (str "lemma type (2) " ++ Printer.pr_lconstr_env (Global.env ()) evd lemma_type); *) Lemmas.start_proof (*i The next call to mk_equation_id is valid since we are constructing the lemma Ensures by: obvious i*) (mk_equation_id f_id) (Decl_kinds.Global, Flags.is_universe_polymorphism (), (Decl_kinds.Proof Decl_kinds.Theorem)) evd lemma_type (Lemmas.mk_hook (fun _ _ -> ())); ignore (Pfedit.by (Proofview.V82.tactic prove_replacement)); Lemmas.save_proof (Vernacexpr.(Proved(Transparent,None))); evd let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num all_funs g = let equation_lemma = try let finfos = find_Function_infos (fst (destConst !evd f)) (*FIXME*) 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 !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 = find_Function_infos (fst (destConst !evd f)) in update_Function {finfos with equation_lemma = Some (match Nametab.locate (qualid_of_ident equation_lemma_id) with ConstRef c -> c | _ -> CErrors.anomaly (Pp.str "Not a constant.") ) } | _ -> () in (* let res = Constrintern.construct_reference (pf_hyps g) equation_lemma_id in *) let evd',res = Evd.fresh_global (Global.env ()) !evd (Constrintern.locate_reference (qualid_of_ident equation_lemma_id)) in evd:=evd'; let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd res in res in let nb_intro_to_do = nb_prod (project g) (pf_concl g) in tclTHEN (tclDO nb_intro_to_do (Proofview.V82.of_tactic intro)) ( fun g' -> let just_introduced = nLastDecls nb_intro_to_do g' in let open Context.Named.Declaration in let just_introduced_id = List.map get_id just_introduced in tclTHEN (Proofview.V82.of_tactic (Equality.rewriteLR equation_lemma)) (revert just_introduced_id) g' ) g let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnames all_funs _nparams : tactic = fun g -> let princ_type = pf_concl 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 (project g) princ_type in let fresh_id = let avoid = ref (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 = match Global.body_of_constant const with | Some (body, _) -> Tacred.cbv_norm_flags (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA]) (Global.env ()) (Evd.empty) (EConstr.of_constr body) | None -> 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_lam (project g) 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 instanciated 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 instanciated with real params *) (List.map var_of_decl princ_info.params) f_body ) in observe (str "full_params := " ++ prlist_with_sep spc (RelDecl.get_name %> Nameops.Name.get_id %> Ppconstr.pr_id) full_params ); observe (str "princ_params := " ++ prlist_with_sep spc (RelDecl.get_name %> Nameops.Name.get_id %> Ppconstr.pr_id) princ_params ); observe (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 (project g) fbody_with_full_params with | Fix((idxs,i),(names,typess,bodies)) -> let bodies_with_all_params = Array.map (fun body -> Reductionops.nf_betaiota (pf_env g) (project g) (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 (project g) types (List.rev_map var_of_decl princ_params) in { idx = idxs.(i) - fix_offset; name = Nameops.Name.get_id (fresh_id names.(i)); types = types; offset = fix_offset; nb_realargs = List.length (fst (decompose_lam (project g) 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 (project g) 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 (pf_env g) (project g) ( applist(body,List.rev_map var_of_decl full_params)) in match EConstr.kind (project g) body_with_full_params with | Fix((_,num),(_,_,bs)) -> Reductionops.nf_betaiota (pf_env g) (project g) ( (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 = 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 : tactic = let pre_info,infos = list_chop fun_num infos in match pre_info,infos with | _,[] -> tclIDTAC | _, 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 if List.is_empty other_fix_infos then if this_fix_info.idx + 1 = 0 then tclIDTAC (* Someone tries to defined a principle on a fully parametric definition declared as a fixpoint (strange but ....) *) else observe_tac_stream (str "h_fix " ++ int (this_fix_info.idx +1) ) (Proofview.V82.of_tactic (fix (Some this_fix_info.name) (this_fix_info.idx +1))) else Proofview.V82.of_tactic (Tactics.mutual_fix this_fix_info.name (this_fix_info.idx + 1) other_fix_infos 0) in let first_tac : tactic = (* every operations until fix creations *) tclTHENLIST [ observe_tac "introducing params" (Proofview.V82.of_tactic (intros_using (List.rev_map id_of_decl princ_info.params))); observe_tac "introducing predictes" (Proofview.V82.of_tactic (intros_using (List.rev_map id_of_decl princ_info.predicates))); observe_tac "introducing branches" (Proofview.V82.of_tactic (intros_using (List.rev_map id_of_decl princ_info.branches))); observe_tac "building fixes" mk_fixes; ] in let intros_after_fixes : tactic = fun gl -> let ctxt,pte_app = (decompose_prod_assum (project gl) (pf_concl gl)) in let pte,pte_args = (decompose_app (project gl) pte_app) in try let pte = try destVar (project gl) 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 (Proofview.V82.of_tactic intro)); (fun g -> (* replacement of the function by its body *) let args = nLastDecls nb_args g in let fix_body = fix_info.body_with_param in (* observe (str "fix_body := "++ pr_lconstr_env (pf_env gl) fix_body); *) let open 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 (pf_env g) (project 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" *) (instanciate_hyps_with_args prove_tac (List.rev_map id_of_decl princ_info.branches) (List.rev args_id)) ] g ); ] gl with Not_found -> let nb_args = min (princ_info.nargs) (List.length ctxt) in tclTHENLIST [ tclDO nb_args (Proofview.V82.of_tactic intro); (fun g -> (* replacement of the function by its body *) let args = nLastDecls nb_args g in let open 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 (pf_env g) Evd.empty (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 (project g) (fst (decompose_app (project g) (List.hd (List.rev pte_args)))) in tclTHENLIST [Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, Names.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 instanciate_hyps_with_args prove_tac (List.rev_map id_of_decl princ_info.branches) (List.rev args_id) ] g ) ] gl in tclTHEN first_tac intros_after_fixes g (* 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 : tactic = match !tcc_lemma_constr with | Undefined -> anomaly (Pp.str "No tcc proof !!") | Value lemma -> fun gls -> (* 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 *) (* ) *) Proofview.V82.of_tactic (Eauto.gen_eauto (false,5) [] (Some [])) ] gls | Not_needed -> tclIDTAC let backtrack_eqs_until_hrec hrec eqs : tactic = fun gls -> let eqs = List.map mkVar eqs in let rewrite = tclFIRST (List.map (fun x -> Proofview.V82.of_tactic (Equality.rewriteRL x)) eqs ) in let _,hrec_concl = decompose_prod (project gls) (pf_unsafe_type_of gls (mkVar hrec)) in let f_app = Array.last (snd (destApp (project gls) hrec_concl)) in let f = (fst (destApp (project gls) f_app)) in let rec backtrack : tactic = fun g -> let f_app = Array.last (snd (destApp (project g) (pf_concl g))) in match EConstr.kind (project g) f_app with | App(f',_) when eq_constr (project g) f' f -> tclIDTAC g | _ -> tclTHEN rewrite backtrack g in backtrack gls let rec rewrite_eqs_in_eqs eqs = match eqs with | [] -> tclIDTAC | eq::eqs -> tclTHEN (tclMAP (fun id gl -> observe_tac (Format.sprintf "rewrite %s in %s " (Id.to_string eq) (Id.to_string id)) (tclTRY (Proofview.V82.of_tactic (Equality.general_rewrite_in true Locus.AllOccurrences true (* dep proofs also: *) true id (mkVar eq) false))) gl ) eqs ) (rewrite_eqs_in_eqs eqs) let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic = fun gls -> (tclTHENLIST [ backtrack_eqs_until_hrec hrec eqs; (* observe_tac ("new_prove_with_tcc ( applying "^(Id.to_string hrec)^" )" ) *) (tclTHENS (* We must have exactly ONE subgoal !*) (Proofview.V82.of_tactic (apply (mkVar hrec))) [ tclTHENLIST [ (Proofview.V82.of_tactic (keep (tcc_hyps@eqs))); (Proofview.V82.of_tactic (apply (Lazy.force acc_inv))); (fun g -> if is_mes then Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, evaluable_of_global_reference (delayed_force ltof_ref))]) g else tclIDTAC g ); observe_tac "rew_and_finish" (tclTHENLIST [tclTRY(list_rewrite false (List.map (fun v -> (mkVar v,true)) eqs)); observe_tac "rewrite_eqs_in_eqs" (rewrite_eqs_in_eqs eqs); (observe_tac "finishing using" ( tclCOMPLETE( Eauto.eauto_with_bases (true,5) [(fun _ sigma -> (sigma, Lazy.force refl_equal))] [Hints.Hint_db.empty empty_transparent_state false] ) ) ) ] ) ] ]) ]) gls 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 else false else false 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 gl = let princ_type = pf_concl gl in let princ_info = compute_elim_sig (project gl) princ_type in let fresh_id = let avoid = ref (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 then (fun b -> Recdef.tclUSER_if_not_mes tclIDTAC b None) else fun _ -> 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 = match List.rev post_rec_arg with | (LocalAssum (Name id,_) | LocalDef (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 let revert l = tclTHEN (Proofview.V82.of_tactic (Tactics.generalize (List.map mkVar l))) (Proofview.V82.of_tactic (clear l)) in let fix_id = Nameops.Name.get_id (fresh_id (Name hrec_id)) in let prove_rec_arg_acc g = ((* observe_tac "prove_rec_arg_acc" *) (tclCOMPLETE (tclTHEN (Proofview.V82.of_tactic (assert_by (Name wf_thm_id) (mkApp (delayed_force well_founded,[|input_type;relation|])) (Proofview.V82.tactic (fun g -> (* observe_tac "prove wf" *) (tclCOMPLETE (wf_tac is_mes)) g)))) ( (* observe_tac *) (* "apply wf_thm" *) Proofview.V82.of_tactic (Tactics.Simple.apply (mkApp(mkVar wf_thm_id,[|mkVar rec_arg_id|]))) ) ) ) ) g 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 (Universes.constr_of_global @@ Coqlib.build_coq_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 gls = let hyps = pf_ids_of_hyps gls in let hid = next_ident_away_in_goal (Id.of_string "prov") (Id.Set.of_list hyps) in tclTHENLIST [ Proofview.V82.of_tactic (generalize [lemma]); Proofview.V82.of_tactic (Simple.intro hid); Proofview.V82.of_tactic (Elim.h_decompose_and (mkVar hid)); (fun g -> let new_hyps = pf_ids_of_hyps g in tcc_list := List.rev (List.subtract Id.equal new_hyps (hid::hyps)); if List.is_empty !tcc_list then begin tcc_list := [hid]; tclIDTAC g end else thin [hid] g ) ] gls 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) ); (* observe_tac "" *) Proofview.V82.of_tactic (assert_by (Name acc_rec_arg_id) (mkApp (delayed_force acc_rel,[|input_type;relation;mkVar rec_arg_id|])) (Proofview.V82.tactic prove_rec_arg_acc) ); (* observe_tac "reverting" *) (revert (List.rev (acc_rec_arg_id::args_ids))); (* (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl () ++ *) (* str "fix arg num" ++ int (List.length args_ids + 1) ); tclIDTAC g); *) (* observe_tac "h_fix " *) (Proofview.V82.of_tactic (fix (Some fix_id) (List.length args_ids + 1))); (* (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl() ++ pr_lconstr_env (pf_env g ) (pf_unsafe_type_of g (mkVar fix_id) )); tclIDTAC g); *) h_intros (List.rev (acc_rec_arg_id::args_ids)); Proofview.V82.of_tactic (Equality.rewriteLR (mkConst eq_ref)); (* observe_tac "finish" *) (fun gl' -> let body = let _,args = destApp (project gl') (pf_concl gl') in Array.last args in let body_info rec_hyps = { nb_rec_hyps = List.length rec_hyps; rec_hyps = rec_hyps; eq_hyps = []; info = body } in let acc_inv = lazy ( mkApp ( delayed_force acc_inv_id, [|input_type;relation;mkVar rec_arg_id|] ) ) in let acc_inv = lazy (mkApp(Lazy.force acc_inv, [|mkVar acc_rec_arg_id|])) in let predicates_names = List.map (get_name %> Nameops.Name.get_id) princ_info.predicates in let pte_info = { proving_tac = (fun eqs -> (* msgnl (str "tcc_list := "++ prlist_with_sep spc Ppconstr.pr_id !tcc_list); *) (* msgnl (str "princ_info.args := "++ prlist_with_sep spc Ppconstr.pr_id (List.map (fun (na,_,_) -> (Nameops.Name.get_id na)) princ_info.args)); *) (* msgnl (str "princ_info.params := "++ prlist_with_sep spc Ppconstr.pr_id (List.map (fun (na,_,_) -> (Nameops.Name.get_id na)) princ_info.params)); *) (* msgnl (str "acc_rec_arg_id := "++ Ppconstr.pr_id acc_rec_arg_id); *) (* msgnl (str "eqs := "++ prlist_with_sep spc Ppconstr.pr_id eqs); *) (* observe_tac "new_prove_with_tcc" *) (new_prove_with_tcc is_mes acc_inv fix_id (!tcc_list@(List.map (get_name %> Nameops.Name.get_id) (princ_info.args@princ_info.params) )@ ([acc_rec_arg_id])) eqs ) ); is_valid = is_valid_hypothesis (project gl') predicates_names } in let ptes_info : pte_info Id.Map.t = List.fold_left (fun map pte_id -> Id.Map.add pte_id pte_info map ) Id.Map.empty predicates_names in let make_proof rec_hyps = build_proof false [f_ref] ptes_info (body_info rec_hyps) in (* observe_tac "instanciate_hyps_with_args" *) (instanciate_hyps_with_args make_proof (List.map (get_name %> Nameops.Name.get_id) princ_info.branches) (List.rev args_ids) ) gl' ) ] gl