1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(* $Id: leminv.ml 11897 2009-02-09 19:28:02Z barras $ *)
39
let not_work_message = "tactic fails to build the inversion lemma, may be because the predicate has arguments that depend on other arguments"
41
let no_inductive_inconstr env constr =
42
(str "Cannot recognize an inductive predicate in " ++
43
pr_lconstr_env env constr ++
44
str "." ++ spc () ++ str "If there is one, may be the structure of the arity" ++
45
spc () ++ str "or of the type of constructors" ++ spc () ++
46
str "is hidden by constant definitions.")
48
(* Inversion stored in lemmas *)
52
An inversion stored in a lemma is computed from a term-pattern, in
53
a signature, as follows:
55
Suppose we have an inductive relation, (I abar), in a signature Gamma:
59
Then we compute the free-variables of abar. Suppose that Gamma is
60
thinned out to only include these.
62
[We need technically to require that all free-variables of the
63
types of the free variables of abar are themselves free-variables
64
of abar. This needs to be checked, but it should not pose a
65
problem - it is hard to imagine cases where it would not hold.]
67
Now, we pose the goal:
69
(P:(Gamma)Prop)(Gamma)(I abar)->(P vars[Gamma]).
71
We execute the tactic:
73
REPEAT Intro THEN (OnLastHyp (Inv NONE false o outSOME))
75
This leaves us with some subgoals. All the assumptions after "P"
76
in these subgoals are new assumptions. I.e. if we have a subgoal,
78
P:(Gamma)Prop, Gamma, Hbar:Tbar |- (P ybar)
80
then the assumption we needed to have was
84
So we construct all the assumptions we need, and rebuild the goal
85
with these assumptions. Then, we can re-apply the same tactic as
86
above, but instead of stopping after the inversion, we just apply
87
the respective assumption in each subgoal.
91
let thin_ids env (hyps,vars) =
94
(fun ((ids,globs) as sofar) (id,c,a) ->
95
if List.mem id globs then
97
| None -> (id::ids,(global_vars env a)@globs)
99
(id::ids,(global_vars env body)@(global_vars env a)@globs)
103
(* returns the sub_signature of sign corresponding to those identifiers that
106
let get_local_sign sign =
107
let lid = ids_of_sign sign in
108
let globsign = Global.named_context() in
109
let add_local id res_sign =
110
if not (mem_sign globsign id) then
111
add_sign (lookup_sign id sign) res_sign
115
List.fold_right add_local lid nil_sign
117
(* returs the identifier of lid that was the latest declared in sign.
118
* (i.e. is the identifier id of lid such that
119
* sign_length (sign_prefix id sign) > sign_length (sign_prefix id' sign) >
120
* for any id'<>id in lid).
121
* it returns both the pair (id,(sign_prefix id sign)) *)
123
let max_prefix_sign lid sign =
124
let rec max_rec (resid,prefix) = function
125
| [] -> (resid,prefix)
127
let pre = sign_prefix id sign in
128
if sign_length pre > sign_length prefix then
131
max_rec (resid,prefix) l
135
| id::l -> snd (max_rec (id, sign_prefix id sign) l)
137
let rec add_prods_sign env sigma t =
138
match kind_of_term (whd_betadeltaiota env sigma t) with
140
let id = id_of_name_using_hdchar env t na in
141
let b'= subst1 (mkVar id) b in
142
add_prods_sign (push_named (id,None,c1) env) sigma b'
143
| LetIn (na,c1,t1,b) ->
144
let id = id_of_name_using_hdchar env t na in
145
let b'= subst1 (mkVar id) b in
146
add_prods_sign (push_named (id,Some c1,t1) env) sigma b'
149
(* [dep_option] indicates wether the inversion lemma is dependent or not.
150
If it is dependent and I is of the form (x_bar:T_bar)(I t_bar) then
151
the stated goal will be (x_bar:T_bar)(H:(I t_bar))(P t_bar H)
152
where P:(x_bar:T_bar)(H:(I x_bar))[sort].
153
The generalisation of such a goal at the moment of the dependent case should
156
If it is non dependent, then if [I]=(I t_bar) and (x_bar:T_bar) are the
157
variables occurring in [I], then the stated goal will be:
158
(x_bar:T_bar)(I t_bar)->(P x_bar)
159
where P: P:(x_bar:T_bar)[sort].
162
let compute_first_inversion_scheme env sigma ind sort dep_option =
163
let indf,realargs = dest_ind_type ind in
164
let allvars = ids_of_context env in
165
let p = next_ident_away (id_of_string "P") allvars in
168
let pty = make_arity env true indf sort in
171
(Anonymous, mkAppliedInd ind, applist(mkVar p,realargs@[mkRel 1]))
175
let i = mkAppliedInd ind in
176
let ivars = global_vars env i in
177
let revargs,ownsign =
179
(fun env (id,_,_ as d) (revargs,hyps) ->
180
if List.mem id ivars then
181
((mkVar id)::revargs,add_named_decl d hyps)
186
let pty = it_mkNamedProd_or_LetIn (mkSort sort) ownsign in
187
let goal = mkArrow i (applist(mkVar p, List.rev revargs)) in
190
let npty = nf_betadeltaiota env sigma pty in
191
let extenv = push_named (p,None,npty) env in
194
(* [inversion_scheme sign I]
196
Given a local signature, [sign], and an instance of an inductive
197
relation, [I], inversion_scheme will prove the associated inversion
198
scheme on sort [sort]. Depending on the value of [dep_option] it will
199
build a dependent lemma or a non-dependent one *)
201
let inversion_scheme env sigma t sort dep_option inv_op =
202
let (env,i) = add_prods_sign env sigma t in
204
try find_rectype env sigma i
206
errorlabstrm "inversion_scheme" (no_inductive_inconstr env i)
208
let (invEnv,invGoal) =
209
compute_first_inversion_scheme env sigma ind sort dep_option
213
(global_vars env invGoal)
214
(ids_of_named_context (named_context invEnv)));
216
errorlabstrm "lemma_inversion"
217
(str"Computed inversion goal was not closed in initial signature.");
219
let invSign = named_context_val invEnv in
220
let pfs = mk_pftreestate (mk_goal invSign invGoal None) in
221
let pfs = solve_pftreestate (tclTHEN intro (onLastHyp inv_op)) pfs in
222
let (pfterm,meta_types) = extract_open_pftreestate pfs in
223
let global_named_context = Global.named_context () in
226
(fun env (id,_,_ as d) sign ->
227
if mem_named_context id global_named_context then sign
228
else add_named_decl d sign)
229
invEnv ~init:empty_named_context
231
let (_,ownSign,mvb) =
233
(fun (avoid,sign,mvb) (mv,mvty) ->
234
let h = next_ident_away (id_of_string "H") avoid in
235
(h::avoid, add_named_decl (h,None,mvty) sign, (mv,mkVar h)::mvb))
236
(ids_of_context invEnv, ownSign, [])
240
it_mkNamedLambda_or_LetIn
241
(local_strong (fun _ -> whd_meta mvb) Evd.empty pfterm) ownSign
245
let add_inversion_lemma name env sigma t sort dep inv_op =
246
let invProof = inversion_scheme env sigma t sort dep inv_op in
248
declare_constant name
250
{ const_entry_body = invProof;
251
const_entry_type = None;
252
const_entry_opaque = false;
253
const_entry_boxed = true && (Flags.boxed_definitions())},
259
(* inv_op = Inv (derives de complete inv. lemma)
260
* inv_op = InvNoThining (derives de semi inversion lemma) *)
262
let inversion_lemma_from_goal n na (loc,id) sort dep_option inv_op =
263
let pts = get_pftreestate() in
264
let gl = nth_goal_of_pftreestate n pts in
266
try pf_get_hyp_typ gl id
267
with Not_found -> Pretype_errors.error_var_not_found_loc loc id in
268
let env = pf_env gl and sigma = project gl in
270
let fv = global_vars env t in
271
let thin_ids = thin_ids (hyps,fv) in
272
if not(list_subset thin_ids fv) then
273
errorlabstrm "lemma_inversion"
274
(str"Cannot compute lemma inversion when there are" ++ spc () ++
275
str"free variables in the types of an inductive" ++ spc () ++
276
str"which are not free in its instance."); *)
277
add_inversion_lemma na env sigma t sort dep_option inv_op
279
let add_inversion_lemma_exn na com comsort bool tac =
280
let env = Global.env () and sigma = Evd.empty in
281
let c = Constrintern.interp_type sigma env com in
282
let sort = Pretyping.interp_sort comsort in
284
add_inversion_lemma na env sigma c sort bool tac
286
| UserError ("Case analysis",s) -> (* r�f�rence � Indrec *)
287
errorlabstrm "Inv needs Nodep Prop Set" s
289
(* ================================= *)
290
(* Applying a given inversion lemma *)
291
(* ================================= *)
293
let lemInv id c gls =
295
let clause = mk_clenv_type_of gls c in
296
let clause = clenv_constrain_last_binding (mkVar id) clause in
297
Clenvtac.res_pf clause ~allow_K:true gls
300
errorlabstrm "LemInv"
301
(str "Cannot refine current goal with the lemma " ++
302
pr_lconstr_env (Global.env()) c)
304
let lemInv_gen id c = try_intros_until (fun id -> lemInv id c) id
306
let lemInvIn id c ids gls =
307
let hyps = List.map (pf_get_hyp gls) ids in
308
let intros_replace_ids gls =
309
let nb_of_new_hyp = nb_prod (pf_concl gls) - List.length ids in
310
if nb_of_new_hyp < 1 then
311
intros_replacing ids gls
313
(tclTHEN (tclDO nb_of_new_hyp intro) (intros_replacing ids)) gls
315
((tclTHEN (tclTHEN (bring_hyps hyps) (lemInv id c))
316
(intros_replace_ids)) gls)
318
let lemInvIn_gen id c l = try_intros_until (fun id -> lemInvIn id c l) id
320
let lemInv_clause id c = function
321
| [] -> lemInv_gen id c
322
| l -> lemInvIn_gen id c l
added
removed
tactics/leminv.ml
