diff options
author | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-28 21:54:47 +0000 |
---|---|---|
committer | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-28 21:54:47 +0000 |
commit | 6b649aba925b6f7462da07599fe67ebb12a3460e (patch) | |
tree | 43656bcaa51164548f3fa14e5b10de5ef1088574 /tactics/leminv.ml |
Imported Upstream version 8.0pl1upstream/8.0pl1
Diffstat (limited to 'tactics/leminv.ml')
-rw-r--r-- | tactics/leminv.ml | 318 |
1 files changed, 318 insertions, 0 deletions
diff --git a/tactics/leminv.ml b/tactics/leminv.ml new file mode 100644 index 00000000..1be465f5 --- /dev/null +++ b/tactics/leminv.ml @@ -0,0 +1,318 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id: leminv.ml,v 1.41.2.1 2004/07/16 19:30:54 herbelin Exp $ *) + +open Pp +open Util +open Names +open Nameops +open Term +open Termops +open Sign +open Evd +open Printer +open Reductionops +open Declarations +open Entries +open Inductiveops +open Environ +open Tacmach +open Proof_trees +open Proof_type +open Pfedit +open Evar_refiner +open Clenv +open Declare +open Tacticals +open Tactics +open Inv +open Vernacexpr +open Safe_typing +open Decl_kinds + +let not_work_message = "tactic fails to build the inversion lemma, may be because the predicate has arguments that depend on other arguments" + +let no_inductive_inconstr env constr = + (str "Cannot recognize an inductive predicate in " ++ + prterm_env env constr ++ + str "." ++ spc () ++ str "If there is one, may be the structure of the arity" ++ + spc () ++ str "or of the type of constructors" ++ spc () ++ + str "is hidden by constant definitions.") + +(* Inversion stored in lemmas *) + +(* ALGORITHM: + + An inversion stored in a lemma is computed from a term-pattern, in + a signature, as follows: + + Suppose we have an inductive relation, (I abar), in a signature Gamma: + + Gamma |- (I abar) + + Then we compute the free-variables of abar. Suppose that Gamma is + thinned out to only include these. + + [We need technically to require that all free-variables of the + types of the free variables of abar are themselves free-variables + of abar. This needs to be checked, but it should not pose a + problem - it is hard to imagine cases where it would not hold.] + + Now, we pose the goal: + + (P:(Gamma)Prop)(Gamma)(I abar)->(P vars[Gamma]). + + We execute the tactic: + + REPEAT Intro THEN (OnLastHyp (Inv NONE false o outSOME)) + + This leaves us with some subgoals. All the assumptions after "P" + in these subgoals are new assumptions. I.e. if we have a subgoal, + + P:(Gamma)Prop, Gamma, Hbar:Tbar |- (P ybar) + + then the assumption we needed to have was + + (Hbar:Tbar)(P ybar) + + So we construct all the assumptions we need, and rebuild the goal + with these assumptions. Then, we can re-apply the same tactic as + above, but instead of stopping after the inversion, we just apply + the respective assumption in each subgoal. + + *) + +let thin_ids env (hyps,vars) = + fst + (List.fold_left + (fun ((ids,globs) as sofar) (id,c,a) -> + if List.mem id globs then + match c with + | None -> (id::ids,(global_vars env a)@globs) + | Some body -> + (id::ids,(global_vars env body)@(global_vars env a)@globs) + else sofar) + ([],vars) hyps) + +(* returns the sub_signature of sign corresponding to those identifiers that + * are not global. *) +(* +let get_local_sign sign = + let lid = ids_of_sign sign in + let globsign = Global.named_context() in + let add_local id res_sign = + if not (mem_sign globsign id) then + add_sign (lookup_sign id sign) res_sign + else + res_sign + in + List.fold_right add_local lid nil_sign +*) +(* returs the identifier of lid that was the latest declared in sign. + * (i.e. is the identifier id of lid such that + * sign_length (sign_prefix id sign) > sign_length (sign_prefix id' sign) > + * for any id'<>id in lid). + * it returns both the pair (id,(sign_prefix id sign)) *) +(* +let max_prefix_sign lid sign = + let rec max_rec (resid,prefix) = function + | [] -> (resid,prefix) + | (id::l) -> + let pre = sign_prefix id sign in + if sign_length pre > sign_length prefix then + max_rec (id,pre) l + else + max_rec (resid,prefix) l + in + match lid with + | [] -> nil_sign + | id::l -> snd (max_rec (id, sign_prefix id sign) l) +*) +let rec add_prods_sign env sigma t = + match kind_of_term (whd_betadeltaiota env sigma t) with + | Prod (na,c1,b) -> + let id = id_of_name_using_hdchar env t na in + let b'= subst1 (mkVar id) b in + add_prods_sign (push_named (id,None,c1) env) sigma b' + | LetIn (na,c1,t1,b) -> + let id = id_of_name_using_hdchar env t na in + let b'= subst1 (mkVar id) b in + add_prods_sign (push_named (id,Some c1,t1) env) sigma b' + | _ -> (env,t) + +(* [dep_option] indicates wether the inversion lemma is dependent or not. + If it is dependent and I is of the form (x_bar:T_bar)(I t_bar) then + the stated goal will be (x_bar:T_bar)(H:(I t_bar))(P t_bar H) + where P:(x_bar:T_bar)(H:(I x_bar))[sort]. + The generalisation of such a goal at the moment of the dependent case should + be easy. + + If it is non dependent, then if [I]=(I t_bar) and (x_bar:T_bar) are the + variables occurring in [I], then the stated goal will be: + (x_bar:T_bar)(I t_bar)->(P x_bar) + where P: P:(x_bar:T_bar)[sort]. +*) + +let compute_first_inversion_scheme env sigma ind sort dep_option = + let indf,realargs = dest_ind_type ind in + let allvars = ids_of_context env in + let p = next_ident_away (id_of_string "P") allvars in + let pty,goal = + if dep_option then + let pty = make_arity env true indf sort in + let goal = + mkProd + (Anonymous, mkAppliedInd ind, applist(mkVar p,realargs@[mkRel 1])) + in + pty,goal + else + let i = mkAppliedInd ind in + let ivars = global_vars env i in + let revargs,ownsign = + fold_named_context + (fun env (id,_,_ as d) (revargs,hyps) -> + if List.mem id ivars then + ((mkVar id)::revargs,add_named_decl d hyps) + else + (revargs,hyps)) + env ~init:([],[]) + in + let pty = it_mkNamedProd_or_LetIn (mkSort sort) ownsign in + let goal = mkArrow i (applist(mkVar p, List.rev revargs)) in + (pty,goal) + in + let npty = nf_betadeltaiota env sigma pty in + let extenv = push_named (p,None,npty) env in + extenv, goal + +(* [inversion_scheme sign I] + + Given a local signature, [sign], and an instance of an inductive + relation, [I], inversion_scheme will prove the associated inversion + scheme on sort [sort]. Depending on the value of [dep_option] it will + build a dependent lemma or a non-dependent one *) + +let inversion_scheme env sigma t sort dep_option inv_op = + let (env,i) = add_prods_sign env sigma t in + let ind = + try find_rectype env sigma i + with Not_found -> + errorlabstrm "inversion_scheme" (no_inductive_inconstr env i) + in + let (invEnv,invGoal) = + compute_first_inversion_scheme env sigma ind sort dep_option + in + assert + (list_subset + (global_vars env invGoal) + (ids_of_named_context (named_context invEnv))); + (* + errorlabstrm "lemma_inversion" + (str"Computed inversion goal was not closed in initial signature"); + *) + let invSign = named_context invEnv in + let pfs = mk_pftreestate (mk_goal invSign invGoal) in + let pfs = solve_pftreestate (tclTHEN intro (onLastHyp inv_op)) pfs in + let (pfterm,meta_types) = extract_open_pftreestate pfs in + let global_named_context = Global.named_context () in + let ownSign = + fold_named_context + (fun env (id,_,_ as d) sign -> + if mem_named_context id global_named_context then sign + else add_named_decl d sign) + invEnv ~init:empty_named_context + in + let (_,ownSign,mvb) = + List.fold_left + (fun (avoid,sign,mvb) (mv,mvty) -> + let h = next_ident_away (id_of_string "H") avoid in + (h::avoid, add_named_decl (h,None,mvty) sign, (mv,mkVar h)::mvb)) + (ids_of_context invEnv, ownSign, []) + meta_types + in + let invProof = + it_mkNamedLambda_or_LetIn (local_strong (whd_meta mvb) pfterm) ownSign + in + invProof + +let add_inversion_lemma name env sigma t sort dep inv_op = + let invProof = inversion_scheme env sigma t sort dep inv_op in + let _ = + declare_constant name + (DefinitionEntry { const_entry_body = invProof; + const_entry_type = None; + const_entry_opaque = false }, + IsProof Lemma) + in () + +(* open Pfedit *) + +(* inv_op = Inv (derives de complete inv. lemma) + * inv_op = InvNoThining (derives de semi inversion lemma) *) + +let inversion_lemma_from_goal n na id sort dep_option inv_op = + let pts = get_pftreestate() in + let gl = nth_goal_of_pftreestate n pts in + let t = pf_get_hyp_typ gl id in + let env = pf_env gl and sigma = project gl in + let fv = global_vars env t in +(* Pourquoi ??? + let thin_ids = thin_ids (hyps,fv) in + if not(list_subset thin_ids fv) then + errorlabstrm "lemma_inversion" + (str"Cannot compute lemma inversion when there are" ++ spc () ++ + str"free variables in the types of an inductive" ++ spc () ++ + str"which are not free in its instance"); *) + add_inversion_lemma na env sigma t sort dep_option inv_op + +let add_inversion_lemma_exn na com comsort bool tac = + let env = Global.env () and sigma = Evd.empty in + let c = Constrintern.interp_type sigma env com in + let sort = Pretyping.interp_sort comsort in + try + add_inversion_lemma na env sigma c sort bool tac + with + | UserError ("Case analysis",s) -> (* référence à Indrec *) + errorlabstrm "Inv needs Nodep Prop Set" s + +(* ================================= *) +(* Applying a given inversion lemma *) +(* ================================= *) + +let lemInv id c gls = + try + let (wc,kONT) = startWalk gls in + let clause = mk_clenv_type_of wc c in + let clause = clenv_constrain_with_bindings [(-1,mkVar id)] clause in + elim_res_pf kONT clause true gls + with + | UserError (a,b) -> + errorlabstrm "LemInv" + (str "Cannot refine current goal with the lemma " ++ + prterm_env (Global.env()) c) + +let lemInv_gen id c = try_intros_until (fun id -> lemInv id c) id + +let lemInvIn id c ids gls = + let hyps = List.map (pf_get_hyp gls) ids in + let intros_replace_ids gls = + let nb_of_new_hyp = nb_prod (pf_concl gls) - List.length ids in + if nb_of_new_hyp < 1 then + intros_replacing ids gls + else + (tclTHEN (tclDO nb_of_new_hyp intro) (intros_replacing ids)) gls + in + ((tclTHEN (tclTHEN (bring_hyps hyps) (lemInv id c)) + (intros_replace_ids)) gls) + +let lemInvIn_gen id c l = try_intros_until (fun id -> lemInvIn id c l) id + +let lemInv_clause id c = function + | [] -> lemInv_gen id c + | l -> lemInvIn_gen id c l |