1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322
|
(************************************************************************)
(* 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 11897 2009-02-09 19:28:02Z barras $ *)
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 " ++
pr_lconstr_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_val invEnv in
let pfs = mk_pftreestate (mk_goal invSign invGoal None) 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 (fun _ -> whd_meta mvb) Evd.empty 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;
const_entry_boxed = true && (Flags.boxed_definitions())},
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 (loc,id) sort dep_option inv_op =
let pts = get_pftreestate() in
let gl = nth_goal_of_pftreestate n pts in
let t =
try pf_get_hyp_typ gl id
with Not_found -> Pretype_errors.error_var_not_found_loc loc id in
let env = pf_env gl and sigma = project gl in
(* Pourquoi ???
let fv = global_vars env t in
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) -> (* rfrence Indrec *)
errorlabstrm "Inv needs Nodep Prop Set" s
(* ================================= *)
(* Applying a given inversion lemma *)
(* ================================= *)
let lemInv id c gls =
try
let clause = mk_clenv_type_of gls c in
let clause = clenv_constrain_last_binding (mkVar id) clause in
Clenvtac.res_pf clause ~allow_K:true gls
with
| UserError (a,b) ->
errorlabstrm "LemInv"
(str "Cannot refine current goal with the lemma " ++
pr_lconstr_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
|