diff options
Diffstat (limited to 'plugins/funind/invfun.ml')
| -rw-r--r-- | plugins/funind/invfun.ml | 670 |
1 files changed, 335 insertions, 335 deletions
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 5f8587408..116a3c991 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -22,7 +22,7 @@ open Hiddentac (* Some pretty printing function for debugging purpose *) -let pr_binding prc = +let pr_binding prc = function | loc, Rawterm.NamedHyp id, (_,c) -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ Pp.cut () ++ prc c) | loc, Rawterm.AnonHyp n, (_,c) -> hov 1 (int n ++ str " := " ++ Pp.cut () ++ prc c) @@ -32,7 +32,7 @@ let pr_bindings prc prlc = function brk (1,1) ++ str "with" ++ brk (1,1) ++ Util.prlist_with_sep spc (fun (_,c) -> prc c) l | Rawterm.ExplicitBindings l -> - brk (1,1) ++ str "with" ++ brk (1,1) ++ + brk (1,1) ++ str "with" ++ brk (1,1) ++ Util.prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l | Rawterm.NoBindings -> mt () @@ -42,7 +42,7 @@ let pr_with_bindings prc prlc (c,bl) = -let pr_constr_with_binding prc (c,bl) : Pp.std_ppcmds = +let pr_constr_with_binding prc (c,bl) : Pp.std_ppcmds = pr_with_bindings prc prc (c,bl) (* The local debuging mechanism *) @@ -61,11 +61,11 @@ let observennl strm = let do_observe_tac s tac g = let goal = begin try (Printer.pr_goal (sig_it g)) with _ -> assert false end in - try + try let v = tac g in msgnl (goal ++ fnl () ++ s ++(str " ")++(str "finished")); v with e -> - msgnl (str "observation "++ s++str " raised exception " ++ - Cerrors.explain_exn e ++ str " on goal " ++ goal ); + msgnl (str "observation "++ s++str " raised exception " ++ + Cerrors.explain_exn e ++ str " on goal " ++ goal ); raise e;; @@ -75,117 +75,117 @@ let observe_tac s tac g = else tac g (* [nf_zeta] $\zeta$-normalization of a term *) -let nf_zeta = +let nf_zeta = Reductionops.clos_norm_flags (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA]) Environ.empty_env Evd.empty (* [id_to_constr id] finds the term associated to [id] in the global environment *) -let id_to_constr id = +let id_to_constr id = try Tacinterp.constr_of_id (Global.env ()) id - with Not_found -> + with Not_found -> raise (UserError ("",str "Cannot find " ++ Ppconstr.pr_id id)) -(* [generate_type g_to_f f graph i] build the completeness (resp. correctness) lemma type if [g_to_f = true] - (resp. g_to_f = false) where [graph] is the graph of [f] and is the [i]th function in the block. +(* [generate_type g_to_f f graph i] build the completeness (resp. correctness) lemma type if [g_to_f = true] + (resp. g_to_f = false) where [graph] is the graph of [f] and is the [i]th function in the block. - [generate_type true f i] returns - \[\forall (x_1:t_1)\ldots(x_n:t_n), let fv := f x_1\ldots x_n in, forall res, - graph\ x_1\ldots x_n\ res \rightarrow res = fv \] decomposed as the context and the conclusion + [generate_type true f i] returns + \[\forall (x_1:t_1)\ldots(x_n:t_n), let fv := f x_1\ldots x_n in, forall res, + graph\ x_1\ldots x_n\ res \rightarrow res = fv \] decomposed as the context and the conclusion - [generate_type false f i] returns - \[\forall (x_1:t_1)\ldots(x_n:t_n), let fv := f x_1\ldots x_n in, forall res, - res = fv \rightarrow graph\ x_1\ldots x_n\ res\] decomposed as the context and the conclusion + [generate_type false f i] returns + \[\forall (x_1:t_1)\ldots(x_n:t_n), let fv := f x_1\ldots x_n in, forall res, + res = fv \rightarrow graph\ x_1\ldots x_n\ res\] decomposed as the context and the conclusion *) -let generate_type g_to_f f graph i = +let generate_type g_to_f f graph i = (*i we deduce the number of arguments of the function and its returned type from the graph i*) - let graph_arity = Inductive.type_of_inductive (Global.env()) (Global.lookup_inductive (destInd graph)) in - let ctxt,_ = decompose_prod_assum graph_arity in - let fun_ctxt,res_type = - match ctxt with + let graph_arity = Inductive.type_of_inductive (Global.env()) (Global.lookup_inductive (destInd graph)) in + let ctxt,_ = decompose_prod_assum graph_arity in + let fun_ctxt,res_type = + match ctxt with | [] | [_] -> anomaly "Not a valid context" | (_,_,res_type)::fun_ctxt -> fun_ctxt,res_type in let nb_args = List.length fun_ctxt in - let args_from_decl i decl = - match decl with + let args_from_decl i decl = + match decl with | (_,Some _,_) -> incr i; failwith "args_from_decl" - | _ -> let j = !i in incr i;mkRel (nb_args - j + 1) + | _ -> let j = !i in incr i;mkRel (nb_args - j + 1) in (*i We need to name the vars [res] and [fv] i*) - let res_id = - Termops.next_global_ident_away + let res_id = + Termops.next_global_ident_away true (id_of_string "res") (map_succeed (function (Name id,_,_) -> id | (Anonymous,_,_) -> failwith "") fun_ctxt) in - let fv_id = - Termops.next_global_ident_away + let fv_id = + Termops.next_global_ident_away true (id_of_string "fv") (res_id::(map_succeed (function (Name id,_,_) -> id | (Anonymous,_,_) -> failwith "Anonymous!") fun_ctxt)) in (*i we can then type the argument to be applied to the function [f] i*) - let args_as_rels = + let args_as_rels = let i = ref 0 in - Array.of_list ((map_succeed (args_from_decl i) (List.rev fun_ctxt))) + Array.of_list ((map_succeed (args_from_decl i) (List.rev fun_ctxt))) in let args_as_rels = Array.map Termops.pop args_as_rels in (*i - the hypothesis [res = fv] can then be computed - We will need to lift it by one in order to use it as a conclusion + the hypothesis [res = fv] can then be computed + We will need to lift it by one in order to use it as a conclusion i*) let res_eq_f_of_args = mkApp(Coqlib.build_coq_eq (),[|lift 2 res_type;mkRel 1;mkRel 2|]) - in - (*i - The hypothesis [graph\ x_1\ldots x_n\ res] can then be computed - We will need to lift it by one in order to use it as a conclusion - i*) - let graph_applied = - let args_and_res_as_rels = + in + (*i + The hypothesis [graph\ x_1\ldots x_n\ res] can then be computed + We will need to lift it by one in order to use it as a conclusion + i*) + let graph_applied = + let args_and_res_as_rels = let i = ref 0 in Array.of_list ((map_succeed (args_from_decl i) (List.rev ((Name res_id,None,res_type)::fun_ctxt))) ) in - let args_and_res_as_rels = + let args_and_res_as_rels = Array.mapi (fun i c -> if i <> Array.length args_and_res_as_rels - 1 then lift 1 c else c) args_and_res_as_rels in - mkApp(graph,args_and_res_as_rels) - in - (*i The [pre_context] is the defined to be the context corresponding to + mkApp(graph,args_and_res_as_rels) + in + (*i The [pre_context] is the defined to be the context corresponding to \[\forall (x_1:t_1)\ldots(x_n:t_n), let fv := f x_1\ldots x_n in, forall res, \] i*) - let pre_ctxt = - (Name res_id,None,lift 1 res_type)::(Name fv_id,Some (mkApp(mkConst f,args_as_rels)),res_type)::fun_ctxt - in + let pre_ctxt = + (Name res_id,None,lift 1 res_type)::(Name fv_id,Some (mkApp(mkConst f,args_as_rels)),res_type)::fun_ctxt + in (*i and we can return the solution depending on which lemma type we are defining i*) - if g_to_f + if g_to_f then (Anonymous,None,graph_applied)::pre_ctxt,(lift 1 res_eq_f_of_args) else (Anonymous,None,res_eq_f_of_args)::pre_ctxt,(lift 1 graph_applied) -(* +(* [find_induction_principle f] searches and returns the [body] and the [type] of [f_rect] - + WARNING: while convertible, [type_of body] and [type] can be non equal *) -let find_induction_principle f = - let f_as_constant = match kind_of_term f with +let find_induction_principle f = + let f_as_constant = match kind_of_term f with | Const c' -> c' | _ -> error "Must be used with a function" in - let infos = find_Function_infos f_as_constant in - match infos.rect_lemma with - | None -> raise Not_found - | Some rect_lemma -> - let rect_lemma = mkConst rect_lemma in - let typ = Typing.type_of (Global.env ()) Evd.empty rect_lemma in + let infos = find_Function_infos f_as_constant in + match infos.rect_lemma with + | None -> raise Not_found + | Some rect_lemma -> + let rect_lemma = mkConst rect_lemma in + let typ = Typing.type_of (Global.env ()) Evd.empty rect_lemma in rect_lemma,typ - - + + (* let fname = *) (* match kind_of_term f with *) @@ -205,41 +205,41 @@ let find_induction_principle f = (* c,Typing.type_of (Global.env ()) Evd.empty c *) -let rec generate_fresh_id x avoid i = - if i == 0 - then [] +let rec generate_fresh_id x avoid i = + if i == 0 + then [] else - let id = Termops.next_global_ident_away true x avoid in + let id = Termops.next_global_ident_away true x avoid in id::(generate_fresh_id x (id::avoid) (pred i)) -(* [prove_fun_correct functional_induction funs_constr graphs_constr schemes lemmas_types_infos i ] - is the tactic used to prove correctness lemma. - +(* [prove_fun_correct functional_induction funs_constr graphs_constr schemes lemmas_types_infos i ] + is the tactic used to prove correctness lemma. + [functional_induction] is the tactic defined in [indfun] (dependency problem) [funs_constr], [graphs_constr] [schemes] [lemmas_types_infos] are the mutually recursive functions - (resp. graphs of the functions and principles and correctness lemma types) to prove correct. - + (resp. graphs of the functions and principles and correctness lemma types) to prove correct. + [i] is the indice of the function to prove correct - The lemma to prove if suppose to have been generated by [generate_type] (in $\zeta$ normal form that is + The lemma to prove if suppose to have been generated by [generate_type] (in $\zeta$ normal form that is it looks like~: - [\forall (x_1:t_1)\ldots(x_n:t_n), forall res, + [\forall (x_1:t_1)\ldots(x_n:t_n), forall res, res = f x_1\ldots x_n in, \rightarrow graph\ x_1\ldots x_n\ res] - The sketch of the proof is the following one~: + The sketch of the proof is the following one~: \begin{enumerate} \item intros until $x_n$ \item $functional\ induction\ (f.(i)\ x_1\ldots x_n)$ using schemes.(i) - \item for each generated branch intro [res] and [hres :res = f x_1\ldots x_n], rewrite [hres] and the + \item for each generated branch intro [res] and [hres :res = f x_1\ldots x_n], rewrite [hres] and the apply the corresponding constructor of the corresponding graph inductive. \end{enumerate} - + *) let prove_fun_correct functional_induction funs_constr graphs_constr schemes lemmas_types_infos i : tactic = fun g -> - (* first of all we recreate the lemmas types to be used as predicates of the induction principle + (* first of all we recreate the lemmas types to be used as predicates of the induction principle that is~: \[fun (x_1:t_1)\ldots(x_n:t_n)=> fun fv => fun res => res = fv \rightarrow graph\ x_1\ldots x_n\ res\] *) @@ -257,8 +257,8 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem in (* we the get the definition of the graphs block *) let graph_ind = destInd graphs_constr.(i) in - let kn = fst graph_ind in - let mib,_ = Global.lookup_inductive graph_ind in + let kn = fst graph_ind in + let mib,_ = Global.lookup_inductive graph_ind in (* and the principle to use in this lemma in $\zeta$ normal form *) let f_principle,princ_type = schemes.(i) in let princ_type = nf_zeta princ_type in @@ -267,9 +267,9 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem let nb_fun_args = nb_prod (pf_concl g) - 2 in let args_names = generate_fresh_id (id_of_string "x") [] nb_fun_args in let ids = args_names@(pf_ids_of_hyps g) in - (* Since we cannot ensure that the funcitonnal principle is defined in the + (* Since we cannot ensure that the funcitonnal principle is defined in the environement and due to the bug #1174, we will need to pose the principle - using a name + using a name *) let principle_id = Termops.next_global_ident_away true (id_of_string "princ") ids in let ids = principle_id :: ids in @@ -290,8 +290,8 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem let eq_ind = Coqlib.build_coq_eq () in let eq_construct = mkConstruct((destInd eq_ind),1) in (* The next to referencies will be used to find out which constructor to apply in each branch *) - let ind_number = ref 0 - and min_constr_number = ref 0 in + let ind_number = ref 0 + and min_constr_number = ref 0 in (* The tactic to prove the ith branch of the principle *) let prove_branche i g = (* We get the identifiers of this branch *) @@ -317,18 +317,18 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem (pre_args, tclTHEN (h_reduce (Rawterm.Unfold([Rawterm.all_occurrences_expr,EvalVarRef id])) allHyps) pre_tac ) - + else (pre_args,pre_tac) ) (pf_hyps g) ([],tclIDTAC) in - (* - We can then recompute the arguments of the constructor. - For each [hid] introduced by this branch, if [hid] has type + (* + We can then recompute the arguments of the constructor. + For each [hid] introduced by this branch, if [hid] has type $forall res, res=fv -> graph.(j)\ x_1\ x_n res$ the corresponding arguments of the constructor are - [ fv (hid fv (refl_equal fv)) ]. - + [ fv (hid fv (refl_equal fv)) ]. + If [hid] has another type the corresponding argument of the constructor is [hid] *) let constructor_args = @@ -360,21 +360,21 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem let params_id = fst (list_chop princ_infos.nparams args_names) in (List.map mkVar params_id)@(List.rev constructor_args) in - (* We then get the constructor corresponding to this branch and - modifies the references has needed i.e. - if the constructor is the last one of the current inductive then - add one the number of the inductive to take and add the number of constructor of the previous - graph to the minimal constructor number + (* We then get the constructor corresponding to this branch and + modifies the references has needed i.e. + if the constructor is the last one of the current inductive then + add one the number of the inductive to take and add the number of constructor of the previous + graph to the minimal constructor number *) - let constructor = - let constructor_num = i - !min_constr_number in - let length = Array.length (mib.Declarations.mind_packets.(!ind_number).Declarations.mind_consnames) in + let constructor = + let constructor_num = i - !min_constr_number in + let length = Array.length (mib.Declarations.mind_packets.(!ind_number).Declarations.mind_consnames) in if constructor_num <= length - then - begin + then + begin (kn,!ind_number),constructor_num end - else + else begin incr ind_number; min_constr_number := !min_constr_number + length ; @@ -418,8 +418,8 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem let param_names = fst (list_chop princ_infos.nparams args_names) in let params = List.map mkVar param_names in let lemmas = Array.to_list (Array.map (fun c -> applist(c,params)) lemmas) in - (* The bindings of the principle - that is the params of the principle and the different lemma types + (* The bindings of the principle + that is the params of the principle and the different lemma types *) let bindings = let params_bindings,avoid = @@ -435,7 +435,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem let lemmas_bindings = List.rev (fst (List.fold_left2 (fun (bindings,avoid) (x,_,_) p -> - let id = Nameops.next_ident_away (Nameops.out_name x) avoid in + let id = Nameops.next_ident_away (Nameops.out_name x) avoid in (dummy_loc,Rawterm.NamedHyp id,inj_open (nf_zeta p))::bindings,id::avoid) ([],avoid) princ_infos.predicates @@ -451,7 +451,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem (h_exact f_principle)); tclTHEN_i (observe_tac "functional_induction" ( - fun g -> + fun g -> observe (pr_constr_with_binding (Printer.pr_lconstr_env (pf_env g)) (mkVar principle_id,bindings)); functional_induction false (applist(funs_constr.(i),List.map mkVar args_names)) @@ -462,13 +462,13 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem ] g -(* [generalize_dependent_of x hyp g] - generalize every hypothesis which depends of [x] but [hyp] +(* [generalize_dependent_of x hyp g] + generalize every hypothesis which depends of [x] but [hyp] *) -let generalize_dependent_of x hyp g = - tclMAP - (function - | (id,None,t) when not (id = hyp) && +let generalize_dependent_of x hyp g = + tclMAP + (function + | (id,None,t) when not (id = hyp) && (Termops.occur_var (pf_env g) x t) -> tclTHEN (h_generalize [mkVar id]) (thin [id]) | _ -> tclIDTAC ) @@ -479,86 +479,86 @@ let generalize_dependent_of x hyp g = - (* [intros_with_rewrite] do the intros in each branch and treat each new hypothesis + (* [intros_with_rewrite] do the intros in each branch and treat each new hypothesis (unfolding, substituting, destructing cases \ldots) *) -let rec intros_with_rewrite g = +let rec intros_with_rewrite g = observe_tac "intros_with_rewrite" intros_with_rewrite_aux g -and intros_with_rewrite_aux : tactic = - fun g -> - let eq_ind = Coqlib.build_coq_eq () in - match kind_of_term (pf_concl g) with - | Prod(_,t,t') -> - begin - match kind_of_term t with - | App(eq,args) when (eq_constr eq eq_ind) -> +and intros_with_rewrite_aux : tactic = + fun g -> + let eq_ind = Coqlib.build_coq_eq () in + match kind_of_term (pf_concl g) with + | Prod(_,t,t') -> + begin + match kind_of_term t with + | App(eq,args) when (eq_constr eq eq_ind) -> if Reductionops.is_conv (pf_env g) (project g) args.(1) args.(2) then let id = pf_get_new_id (id_of_string "y") g in tclTHENSEQ [ h_intro id; thin [id]; intros_with_rewrite ] g else if isVar args.(1) - then - let id = pf_get_new_id (id_of_string "y") g in + then + let id = pf_get_new_id (id_of_string "y") g in tclTHENSEQ [ h_intro id; - generalize_dependent_of (destVar args.(1)) id; + generalize_dependent_of (destVar args.(1)) id; tclTRY (Equality.rewriteLR (mkVar id)); intros_with_rewrite - ] + ] g else - begin - let id = pf_get_new_id (id_of_string "y") g in + begin + let id = pf_get_new_id (id_of_string "y") g in tclTHENSEQ[ h_intro id; tclTRY (Equality.rewriteLR (mkVar id)); intros_with_rewrite ] g end - | Ind _ when eq_constr t (Coqlib.build_coq_False ()) -> + | Ind _ when eq_constr t (Coqlib.build_coq_False ()) -> Tauto.tauto g - | Case(_,_,v,_) -> + | Case(_,_,v,_) -> tclTHENSEQ[ h_case false (v,Rawterm.NoBindings); intros_with_rewrite ] g - | LetIn _ -> + | LetIn _ -> tclTHENSEQ[ - h_reduce + h_reduce (Rawterm.Cbv - {Rawterm.all_flags - with Rawterm.rDelta = false; - }) + {Rawterm.all_flags + with Rawterm.rDelta = false; + }) onConcl ; intros_with_rewrite ] g - | _ -> - let id = pf_get_new_id (id_of_string "y") g in + | _ -> + let id = pf_get_new_id (id_of_string "y") g in tclTHENSEQ [ h_intro id;intros_with_rewrite] g end - | LetIn _ -> + | LetIn _ -> tclTHENSEQ[ - h_reduce + h_reduce (Rawterm.Cbv - {Rawterm.all_flags - with Rawterm.rDelta = false; - }) + {Rawterm.all_flags + with Rawterm.rDelta = false; + }) onConcl ; intros_with_rewrite ] g - | _ -> tclIDTAC g - -let rec reflexivity_with_destruct_cases g = - let destruct_case () = - try - match kind_of_term (snd (destApp (pf_concl g))).(2) with - | Case(_,_,v,_) -> + | _ -> tclIDTAC g + +let rec reflexivity_with_destruct_cases g = + let destruct_case () = + try + match kind_of_term (snd (destApp (pf_concl g))).(2) with + | Case(_,_,v,_) -> tclTHENSEQ[ h_case false (v,Rawterm.NoBindings); intros; - observe_tac "reflexivity_with_destruct_cases" reflexivity_with_destruct_cases + observe_tac "reflexivity_with_destruct_cases" reflexivity_with_destruct_cases ] | _ -> reflexivity with _ -> reflexivity @@ -566,13 +566,13 @@ let rec reflexivity_with_destruct_cases g = let eq_ind = Coqlib.build_coq_eq () in let discr_inject = Tacticals.onAllHypsAndConcl ( - fun sc g -> - match sc with + fun sc g -> + match sc with None -> tclIDTAC g - | Some id -> - match kind_of_term (pf_type_of g (mkVar id)) with - | App(eq,[|_;t1;t2|]) when eq_constr eq eq_ind -> - if Equality.discriminable (pf_env g) (project g) t1 t2 + | Some id -> + match kind_of_term (pf_type_of g (mkVar id)) with + | App(eq,[|_;t1;t2|]) when eq_constr eq eq_ind -> + if Equality.discriminable (pf_env g) (project g) t1 t2 then Equality.discrHyp id g else if Equality.injectable (pf_env g) (project g) t1 t2 then tclTHENSEQ [Equality.injHyp id;thin [id];intros_with_rewrite] g @@ -583,10 +583,10 @@ let rec reflexivity_with_destruct_cases g = (tclFIRST [ reflexivity; tclTHEN (tclPROGRESS discr_inject) (destruct_case ()); - (* We reach this point ONLY if - the same value is matched (at least) two times + (* We reach this point ONLY if + the same value is matched (at least) two times along binding path. - In this case, either we have a discriminable hypothesis and we are done, + In this case, either we have a discriminable hypothesis and we are done, either at least an injectable one and we do the injection before continuing *) tclTHEN (tclPROGRESS discr_inject ) reflexivity_with_destruct_cases @@ -594,95 +594,95 @@ let rec reflexivity_with_destruct_cases g = g -(* [prove_fun_complete funs graphs schemes lemmas_types_infos i] - is the tactic used to prove completness lemma. - +(* [prove_fun_complete funs graphs schemes lemmas_types_infos i] + is the tactic used to prove completness lemma. + [funcs], [graphs] [schemes] [lemmas_types_infos] are the mutually recursive functions - (resp. definitions of the graphs of the functions, principles and correctness lemma types) to prove correct. - + (resp. definitions of the graphs of the functions, principles and correctness lemma types) to prove correct. + [i] is the indice of the function to prove complete - The lemma to prove if suppose to have been generated by [generate_type] (in $\zeta$ normal form that is + The lemma to prove if suppose to have been generated by [generate_type] (in $\zeta$ normal form that is it looks like~: - [\forall (x_1:t_1)\ldots(x_n:t_n), forall res, + [\forall (x_1:t_1)\ldots(x_n:t_n), forall res, graph\ x_1\ldots x_n\ res, \rightarrow res = f x_1\ldots x_n in] - The sketch of the proof is the following one~: + The sketch of the proof is the following one~: \begin{enumerate} \item intros until $H:graph\ x_1\ldots x_n\ res$ \item $elim\ H$ using schemes.(i) - \item for each generated branch, intro the news hyptohesis, for each such hyptohesis [h], if [h] has - type [x=?] with [x] a variable, then subst [x], - if [h] has type [t=?] with [t] not a variable then rewrite [t] in the subterms, else - if [h] is a match then destruct it, else do just introduce it, + \item for each generated branch, intro the news hyptohesis, for each such hyptohesis [h], if [h] has + type [x=?] with [x] a variable, then subst [x], + if [h] has type [t=?] with [t] not a variable then rewrite [t] in the subterms, else + if [h] is a match then destruct it, else do just introduce it, after all intros, the conclusion should be a reflexive equality. \end{enumerate} - + *) -let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = - fun g -> - (* We compute the types of the different mutually recursive lemmas +let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = + fun g -> + (* We compute the types of the different mutually recursive lemmas in $\zeta$ normal form *) - let lemmas = - Array.map - (fun (_,(ctxt,concl)) -> nf_zeta (Termops.it_mkLambda_or_LetIn ~init:concl ctxt)) + let lemmas = + Array.map + (fun (_,(ctxt,concl)) -> nf_zeta (Termops.it_mkLambda_or_LetIn ~init:concl ctxt)) lemmas_types_infos in (* We get the constant and the principle corresponding to this lemma *) let f = funcs.(i) in - let graph_principle = nf_zeta schemes.(i) in - let princ_type = pf_type_of g graph_principle in - let princ_infos = Tactics.compute_elim_sig princ_type in - (* Then we get the number of argument of the function + let graph_principle = nf_zeta schemes.(i) in + let princ_type = pf_type_of g graph_principle in + let princ_infos = Tactics.compute_elim_sig princ_type in + (* Then we get the number of argument of the function and compute a fresh name for each of them *) - let nb_fun_args = nb_prod (pf_concl g) - 2 in + let nb_fun_args = nb_prod (pf_concl g) - 2 in let args_names = generate_fresh_id (id_of_string "x") [] nb_fun_args in let ids = args_names@(pf_ids_of_hyps g) in (* and fresh names for res H and the principle (cf bug bug #1174) *) - let res,hres,graph_principle_id = - match generate_fresh_id (id_of_string "z") ids 3 with + let res,hres,graph_principle_id = + match generate_fresh_id (id_of_string "z") ids 3 with | [res;hres;graph_principle_id] -> res,hres,graph_principle_id - | _ -> assert false + | _ -> assert false in - let ids = res::hres::graph_principle_id::ids in + let ids = res::hres::graph_principle_id::ids in (* we also compute fresh names for each hyptohesis of each branche of the principle *) - let branches = List.rev princ_infos.branches in - let intro_pats = - List.map - (fun (_,_,br_type) -> - List.map - (fun id -> id) + let branches = List.rev princ_infos.branches in + let intro_pats = + List.map + (fun (_,_,br_type) -> + List.map + (fun id -> id) (generate_fresh_id (id_of_string "y") ids (nb_prod br_type)) ) branches in - (* We will need to change the function by its body - using [f_equation] if it is recursive (that is the graph is infinite - or unfold if the graph is finite + (* We will need to change the function by its body + using [f_equation] if it is recursive (that is the graph is infinite + or unfold if the graph is finite *) - let rewrite_tac j ids : tactic = - let graph_def = graphs.(j) in - let infos = try find_Function_infos (destConst funcs.(j)) with Not_found -> error "No graph found" in + let rewrite_tac j ids : tactic = + let graph_def = graphs.(j) in + let infos = try find_Function_infos (destConst funcs.(j)) with Not_found -> error "No graph found" in if infos.is_general || Rtree.is_infinite graph_def.mind_recargs - then - let eq_lemma = + then + let eq_lemma = try Option.get (infos).equation_lemma with Option.IsNone -> anomaly "Cannot find equation lemma" - in + in tclTHENSEQ[ tclMAP h_intro ids; Equality.rewriteLR (mkConst eq_lemma); (* Don't forget to $\zeta$ normlize the term since the principles have been $\zeta$-normalized *) - h_reduce + h_reduce (Rawterm.Cbv - {Rawterm.all_flags - with Rawterm.rDelta = false; - }) + {Rawterm.all_flags + with Rawterm.rDelta = false; + }) onConcl ; h_generalize (List.map mkVar ids); @@ -691,16 +691,16 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = else unfold_in_concl [(all_occurrences,Names.EvalConstRef (destConst f))] in (* The proof of each branche itself *) - let ind_number = ref 0 in + let ind_number = ref 0 in let min_constr_number = ref 0 in - let prove_branche i g = + let prove_branche i g = (* we fist compute the inductive corresponding to the branch *) - let this_ind_number = - let constructor_num = i - !min_constr_number in - let length = Array.length (graphs.(!ind_number).Declarations.mind_consnames) in + let this_ind_number = + let constructor_num = i - !min_constr_number in + let length = Array.length (graphs.(!ind_number).Declarations.mind_consnames) in if constructor_num <= length then !ind_number - else + else begin incr ind_number; min_constr_number := !min_constr_number + length; @@ -719,13 +719,13 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = g in let params_names = fst (list_chop princ_infos.nparams args_names) in - let params = List.map mkVar params_names in - tclTHENSEQ + let params = List.map mkVar params_names in + tclTHENSEQ [ tclMAP h_intro (args_names@[res;hres]); - observe_tac "h_generalize" + observe_tac "h_generalize" (h_generalize [mkApp(applist(graph_principle,params),Array.map (fun c -> applist(c,params)) lemmas)]); h_intro graph_principle_id; - observe_tac "" (tclTHEN_i + observe_tac "" (tclTHEN_i (observe_tac "elim" ((elim false (mkVar hres,Rawterm.NoBindings) (Some (mkVar graph_principle_id,Rawterm.NoBindings))))) (fun i g -> observe_tac "prove_branche" (prove_branche i) g )) ] @@ -737,94 +737,94 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = let do_save () = Command.save_named false -(* [derive_correctness make_scheme functional_induction funs graphs] create correctness and completeness +(* [derive_correctness make_scheme functional_induction funs graphs] create correctness and completeness lemmas for each function in [funs] w.r.t. [graphs] - - [make_scheme] is Functional_principle_types.make_scheme (dependency pb) and - [functional_induction] is Indfun.functional_induction (same pb) + + [make_scheme] is Functional_principle_types.make_scheme (dependency pb) and + [functional_induction] is Indfun.functional_induction (same pb) *) - -let derive_correctness make_scheme functional_induction (funs: constant list) (graphs:inductive list) = + +let derive_correctness make_scheme functional_induction (funs: constant list) (graphs:inductive list) = let funs = Array.of_list funs and graphs = Array.of_list graphs in let funs_constr = Array.map mkConst funs in - try - let graphs_constr = Array.map mkInd graphs in - let lemmas_types_infos = - Util.array_map2_i - (fun i f_constr graph -> - let const_of_f = destConst f_constr in - let (type_of_lemma_ctxt,type_of_lemma_concl) as type_info = + try + let graphs_constr = Array.map mkInd graphs in + let lemmas_types_infos = + Util.array_map2_i + (fun i f_constr graph -> + let const_of_f = destConst f_constr in + let (type_of_lemma_ctxt,type_of_lemma_concl) as type_info = generate_type false const_of_f graph i - in - let type_of_lemma = Termops.it_mkProd_or_LetIn ~init:type_of_lemma_concl type_of_lemma_ctxt in + in + let type_of_lemma = Termops.it_mkProd_or_LetIn ~init:type_of_lemma_concl type_of_lemma_ctxt in let type_of_lemma = nf_zeta type_of_lemma in observe (str "type_of_lemma := " ++ Printer.pr_lconstr type_of_lemma); type_of_lemma,type_info ) funs_constr - graphs_constr + graphs_constr in - let schemes = - (* The functional induction schemes are computed and not saved if there is more that one function + let schemes = + (* The functional induction schemes are computed and not saved if there is more that one function if the block contains only one function we can safely reuse [f_rect] *) try if Array.length funs_constr <> 1 then raise Not_found; [| find_induction_principle funs_constr.(0) |] - with Not_found -> - Array.of_list - (List.map - (fun entry -> + with Not_found -> + Array.of_list + (List.map + (fun entry -> (entry.Entries.const_entry_body, Option.get entry.Entries.const_entry_type ) ) (make_scheme (array_map_to_list (fun const -> const,Rawterm.RType None) funs)) ) in - let proving_tac = + let proving_tac = prove_fun_correct functional_induction funs_constr graphs_constr schemes lemmas_types_infos in - Array.iteri - (fun i f_as_constant -> + Array.iteri + (fun i f_as_constant -> let f_id = id_of_label (con_label f_as_constant) in - Command.start_proof + Command.start_proof (*i The next call to mk_correct_id is valid since we are constructing the lemma Ensures by: obvious - i*) + i*) (mk_correct_id f_id) (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem)) (fst lemmas_types_infos.(i)) (fun _ _ -> ()); Pfedit.by (observe_tac ("prove correctness ("^(string_of_id f_id)^")") (proving_tac i)); do_save (); - let finfo = find_Function_infos f_as_constant in + let finfo = find_Function_infos f_as_constant in update_Function - {finfo with + {finfo with correctness_lemma = Some (destConst (Tacinterp.constr_of_id (Global.env ())(mk_correct_id f_id))) } ) funs; - let lemmas_types_infos = - Util.array_map2_i - (fun i f_constr graph -> - let const_of_f = destConst f_constr in - let (type_of_lemma_ctxt,type_of_lemma_concl) as type_info = + let lemmas_types_infos = + Util.array_map2_i + (fun i f_constr graph -> + let const_of_f = destConst f_constr in + let (type_of_lemma_ctxt,type_of_lemma_concl) as type_info = generate_type true const_of_f graph i - in - let type_of_lemma = Termops.it_mkProd_or_LetIn ~init:type_of_lemma_concl type_of_lemma_ctxt in + in + let type_of_lemma = Termops.it_mkProd_or_LetIn ~init:type_of_lemma_concl type_of_lemma_ctxt in let type_of_lemma = nf_zeta type_of_lemma in observe (str "type_of_lemma := " ++ Printer.pr_lconstr type_of_lemma); type_of_lemma,type_info ) funs_constr - graphs_constr + graphs_constr in - let kn,_ as graph_ind = destInd graphs_constr.(0) in + let kn,_ as graph_ind = destInd graphs_constr.(0) in let mib,mip = Global.lookup_inductive graph_ind in - let schemes = - Array.of_list + let schemes = + Array.of_list (Indrec.build_mutual_indrec (Global.env ()) Evd.empty - (Array.to_list + (Array.to_list (Array.mapi (fun i mip -> (kn,i),mib,mip,true,InType) mib.Declarations.mind_packets @@ -832,25 +832,25 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g ) ) in - let proving_tac = + let proving_tac = prove_fun_complete funs_constr mib.Declarations.mind_packets schemes lemmas_types_infos in - Array.iteri - (fun i f_as_constant -> + Array.iteri + (fun i f_as_constant -> let f_id = id_of_label (con_label f_as_constant) in - Command.start_proof + Command.start_proof (*i The next call to mk_complete_id is valid since we are constructing the lemma Ensures by: obvious - i*) + i*) (mk_complete_id f_id) (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem)) (fst lemmas_types_infos.(i)) (fun _ _ -> ()); Pfedit.by (observe_tac ("prove completeness ("^(string_of_id f_id)^")") (proving_tac i)); do_save (); - let finfo = find_Function_infos f_as_constant in + let finfo = find_Function_infos f_as_constant in update_Function - {finfo with + {finfo with completeness_lemma = Some (destConst (Tacinterp.constr_of_id (Global.env ())(mk_complete_id f_id))) } ) @@ -859,16 +859,16 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g (* In case of problem, we reset all the lemmas *) (*i The next call to mk_correct_id is valid since we are erasing the lemmas Ensures by: obvious - i*) - let first_lemma_id = - let f_id = id_of_label (con_label funs.(0)) in - - mk_correct_id f_id + i*) + let first_lemma_id = + let f_id = id_of_label (con_label funs.(0)) in + + mk_correct_id f_id in ignore(try Vernacentries.vernac_reset_name (Util.dummy_loc,first_lemma_id) with _ -> ()); raise e - - + + @@ -876,73 +876,73 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g (* [revert_graph kn post_tac hid] transforme an hypothesis [hid] having type Ind(kn,num) t1 ... tn res when [kn] denotes a graph block into - f_num t1... tn = res (by applying [f_complete] to the first type) before apply post_tac on the result - + f_num t1... tn = res (by applying [f_complete] to the first type) before apply post_tac on the result + if the type of hypothesis has not this form or if we cannot find the completeness lemma then we do nothing *) let revert_graph kn post_tac hid g = - let typ = pf_type_of g (mkVar hid) in - match kind_of_term typ with - | App(i,args) when isInd i -> - let ((kn',num) as ind') = destInd i in - if kn = kn' + let typ = pf_type_of g (mkVar hid) in + match kind_of_term typ with + | App(i,args) when isInd i -> + let ((kn',num) as ind') = destInd i in + if kn = kn' then (* We have generated a graph hypothesis so that we must change it if we can *) - let info = + let info = try find_Function_of_graph ind' with Not_found -> (* The graphs are mutually recursive but we cannot find one of them !*) anomaly "Cannot retrieve infos about a mutual block" - in - (* if we can find a completeness lemma for this function - then we can come back to the functional form. If not, we do nothing + in + (* if we can find a completeness lemma for this function + then we can come back to the functional form. If not, we do nothing *) - match info.completeness_lemma with + match info.completeness_lemma with | None -> tclIDTAC g - | Some f_complete -> + | Some f_complete -> let f_args,res = array_chop (Array.length args - 1) args in tclTHENSEQ [ h_generalize [applist(mkConst f_complete,(Array.to_list f_args)@[res.(0);mkVar hid])]; thin [hid]; - h_intro hid; + h_intro hid; post_tac hid ] g - + else tclIDTAC g | _ -> tclIDTAC g -(* +(* [functional_inversion hid fconst f_correct ] is the functional version of [inversion] - + [hid] is the hypothesis to invert, [fconst] is the function to invert and [f_correct] is the correctness lemma for [fconst]. - The sketch is the follwing~: - \begin{enumerate} - \item Transforms the hypothesis [hid] such that its type is now $res\ =\ f\ t_1 \ldots t_n$ + The sketch is the follwing~: + \begin{enumerate} + \item Transforms the hypothesis [hid] such that its type is now $res\ =\ f\ t_1 \ldots t_n$ (fails if it is not possible) \item replace [hid] with $R\_f t_1 \ldots t_n res$ using [f_correct] \item apply [inversion] on [hid] - \item finally in each branch, replace each hypothesis [R\_f ..] by [f ...] using [f_complete] (whenever + \item finally in each branch, replace each hypothesis [R\_f ..] by [f ...] using [f_complete] (whenever such a lemma exists) \end{enumerate} *) - -let functional_inversion kn hid fconst f_correct : tactic = - fun g -> - let old_ids = List.fold_right Idset.add (pf_ids_of_hyps g) Idset.empty in - let type_of_h = pf_type_of g (mkVar hid) in - match kind_of_term type_of_h with - | App(eq,args) when eq_constr eq (Coqlib.build_coq_eq ()) -> - let pre_tac,f_args,res = - match kind_of_term args.(1),kind_of_term args.(2) with - | App(f,f_args),_ when eq_constr f fconst -> + +let functional_inversion kn hid fconst f_correct : tactic = + fun g -> + let old_ids = List.fold_right Idset.add (pf_ids_of_hyps g) Idset.empty in + let type_of_h = pf_type_of g (mkVar hid) in + match kind_of_term type_of_h with + | App(eq,args) when eq_constr eq (Coqlib.build_coq_eq ()) -> + let pre_tac,f_args,res = + match kind_of_term args.(1),kind_of_term args.(2) with + | App(f,f_args),_ when eq_constr f fconst -> ((fun hid -> h_symmetry (onHyp hid)),f_args,args.(2)) - |_,App(f,f_args) when eq_constr f fconst -> - ((fun hid -> tclIDTAC),f_args,args.(1)) + |_,App(f,f_args) when eq_constr f fconst -> + ((fun hid -> tclIDTAC),f_args,args.(1)) | _ -> (fun hid -> tclFAIL 1 (mt ())),[||],args.(2) - in + in tclTHENSEQ[ pre_tac hid; h_generalize [applist(f_correct,(Array.to_list f_args)@[res;mkVar hid])]; @@ -950,7 +950,7 @@ let functional_inversion kn hid fconst f_correct : tactic = h_intro hid; Inv.inv FullInversion None (Rawterm.NamedHyp hid); (fun g -> - let new_ids = List.filter (fun id -> not (Idset.mem id old_ids)) (pf_ids_of_hyps g) in + let new_ids = List.filter (fun id -> not (Idset.mem id old_ids)) (pf_ids_of_hyps g) in tclMAP (revert_graph kn pre_tac) (hid::new_ids) g ); ] g @@ -958,62 +958,62 @@ let functional_inversion kn hid fconst f_correct : tactic = -let invfun qhyp f = - let f = - match f with - | ConstRef f -> f +let invfun qhyp f = + let f = + match f with + | ConstRef f -> f | _ -> raise (Util.UserError("",str "Not a function")) in - try - let finfos = find_Function_infos f in - let f_correct = mkConst(Option.get finfos.correctness_lemma) + try + let finfos = find_Function_infos f in + let f_correct = mkConst(Option.get finfos.correctness_lemma) and kn = fst finfos.graph_ind in - Tactics.try_intros_until (fun hid -> functional_inversion kn hid (mkConst f) f_correct) qhyp - with - | Not_found -> error "No graph found" + Tactics.try_intros_until (fun hid -> functional_inversion kn hid (mkConst f) f_correct) qhyp + with + | Not_found -> error "No graph found" | Option.IsNone -> error "Cannot use equivalence with graph!" -let invfun qhyp f g = - match f with +let invfun qhyp f g = + match f with | Some f -> invfun qhyp f g - | None -> - Tactics.try_intros_until - (fun hid g -> - let hyp_typ = pf_type_of g (mkVar hid) in - match kind_of_term hyp_typ with - | App(eq,args) when eq_constr eq (Coqlib.build_coq_eq ()) -> + | None -> + Tactics.try_intros_until + (fun hid g -> + let hyp_typ = pf_type_of g (mkVar hid) in + match kind_of_term hyp_typ with + | App(eq,args) when eq_constr eq (Coqlib.build_coq_eq ()) -> begin - let f1,_ = decompose_app args.(1) in - try + let f1,_ = decompose_app args.(1) in + try if not (isConst f1) then failwith ""; - let finfos = find_Function_infos (destConst f1) in - let f_correct = mkConst(Option.get finfos.correctness_lemma) + let finfos = find_Function_infos (destConst f1) in + let f_correct = mkConst(Option.get finfos.correctness_lemma) and kn = fst finfos.graph_ind in functional_inversion kn hid f1 f_correct g - with | Failure "" | Option.IsNone | Not_found -> - try - let f2,_ = decompose_app args.(2) in + with | Failure "" | Option.IsNone | Not_found -> + try + let f2,_ = decompose_app args.(2) in if not (isConst f2) then failwith ""; - let finfos = find_Function_infos (destConst f2) in - let f_correct = mkConst(Option.get finfos.correctness_lemma) + let finfos = find_Function_infos (destConst f2) in + let f_correct = mkConst(Option.get finfos.correctness_lemma) and kn = fst finfos.graph_ind in functional_inversion kn hid f2 f_correct g with - | Failure "" -> + | Failure "" -> errorlabstrm "" (str "Hypothesis" ++ Ppconstr.pr_id hid ++ str " must contain at leat one Function") - | Option.IsNone -> - if do_observe () + | Option.IsNone -> + if do_observe () then error "Cannot use equivalence with graph for any side of the equality" else errorlabstrm "" (str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid) - | Not_found -> - if do_observe () + | Not_found -> + if do_observe () then - error "No graph found for any side of equality" + error "No graph found for any side of equality" else errorlabstrm "" (str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid) end | _ -> errorlabstrm "" (Ppconstr.pr_id hid ++ str " must be an equality ") |