aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--tactics/Inv.v94
-rw-r--r--tactics/inv.ml562
-rw-r--r--tactics/inv.mli17
-rw-r--r--tactics/leminv.ml419
4 files changed, 1092 insertions, 0 deletions
diff --git a/tactics/Inv.v b/tactics/Inv.v
new file mode 100644
index 000000000..2126ced3d
--- /dev/null
+++ b/tactics/Inv.v
@@ -0,0 +1,94 @@
+
+(* $Id: *)
+
+Require Export Equality.
+
+Declare ML Module "Inv" "Leminv".
+
+Syntax tactic level 0:
+ inversion [(Inv $ic $id)] -> [ (INVCOM $ic) [1 1] $id]
+| inversion_in [(InvIn $ic $id ($LIST $l))]
+ -> [ (INVCOM $ic) [1 1] $id (CLAUSE ($LIST $l))]
+
+| dep_inv [(DInv $ic $id)] -> ["Dependent " (INVCOM $ic) [1 1] $id]
+| dep_inv_with [(DInvWith $ic $id $c)]
+ -> ["Dependent " (INVCOM $ic) [1 1] $id [1 1] "with " $c]
+
+(* Use rules *)
+
+| inv_using
+ [(UseInversionLemma $id $c)] -> ["Inversion " $id [1 1] "using " $c]
+| inv_using_in [(UseInversionLemmaIn $id $c ($LIST $l))]
+ -> ["Inversion " $id [1 1] "using " $c (CLAUSE ($LIST $l))]
+
+| simple_inv [(INVCOM HalfInversion)] -> [ "Simple Inversion" ]
+| inversion_com [(INVCOM Inversion)] -> [ "Inversion" ]
+| inversion_clear [(INVCOM InversionClear)] -> [ "Inversion_clear" ].
+
+
+Grammar tactic simple_tactic :=
+ inversion [ inversion_com($ic) identarg($id) ] -> [(Inv $ic $id)]
+| inversion_in [ inversion_com($ic) identarg($id) "in" ne_identarg_list($l) ]
+ -> [(InvIn $ic $id ($LIST $l))]
+| dep_inv [ "Dependent" inversion_com($ic) identarg($id) ]
+ -> [(DInv $ic $id)]
+| dep_inv_with
+ [ "Dependent" inversion_com($ic) identarg($id) "with" constrarg($c) ]
+ -> [(DInvWith $ic $id $c) ]
+
+| inv_using [ inversion_com($ic) identarg($id) "using" constrarg($c) ]
+ -> case [$ic] of
+ Inversion -> [(UseInversionLemma $id $c)]
+ esac
+
+| inv_using_in
+ [ inversion_com($ic) identarg($id) "using" constrarg($c)
+ "in" ne_identarg_list($l) ]
+ -> case [$ic] of
+ Inversion -> [(UseInversionLemmaIn $id $c ($LIST $l))]
+ esac
+
+with inversion_com :=
+ simple_inv [ "Simple" "Inversion" ] -> [ HalfInversion ]
+| inversion_com [ "Inversion" ] -> [ Inversion ]
+| inv_clear [ "Inversion_clear" ] -> [ InversionClear ].
+
+
+Grammar vernac vernac :=
+ der_inv_clr [ "Derive" "Inversion_clear" identarg($na) identarg($id) "." ]
+ -> [(MakeInversionLemmaFromHyp 1 $na $id)]
+
+| der_inv_clr_num [ "Derive" "Inversion_clear"
+ numarg($n) identarg($na) identarg($id) "." ]
+ -> [(MakeInversionLemmaFromHyp $n $na $id)]
+
+| der_inv_clr_with_srt [ "Derive" "Inversion_clear" identarg($na)
+ "with" constrarg($com) "Sort" sortarg($s) "." ]
+ -> [(MakeInversionLemma $na $com (COMMAND $s))]
+
+| der_inv_clr_with [ "Derive" "Inversion_clear" identarg($na)
+ "with" constrarg($com) "." ]
+ -> [(MakeInversionLemma $na $com (COMMAND (PROP{Null})))]
+
+| der_inv_with_srt [ "Derive" "Inversion" identarg($na)
+ "with" constrarg($com) "Sort" sortarg($s) "." ]
+ -> [(MakeSemiInversionLemma $na $com (COMMAND $s))]
+
+| der_inv_with [ "Derive" "Inversion" identarg($na) "with" constrarg($com) "." ]
+ -> [(MakeSemiInversionLemma $na $com (COMMAND (PROP{Null})))]
+
+| der_inv [ "Derive" "Inversion" identarg($na) identarg($id) "." ]
+ -> [(MakeSemiInversionLemmaFromHyp 1 $na $id)]
+
+| der_inv_num [ "Derive" "Inversion"
+ numarg($n) identarg($na) identarg($id) "." ]
+ -> [(MakeSemiInversionLemmaFromHyp $n $na $id)]
+
+| der_dep_inv_with_srt [ "Derive" "Dependent" "Inversion" identarg($na)
+ "with" constrarg($com) "Sort" sortarg($s) "." ]
+ -> [(MakeDependentSemiInversionLemma $na $com (COMMAND $s))]
+
+| der_dep_inv_clr_with_srt
+ [ "Derive" "Dependent" "Inversion_clear" identarg($na)
+ "with" constrarg($com) "Sort" sortarg($s)"." ]
+ -> [(MakeDependentInversionLemma $na $com (COMMAND $s))].
diff --git a/tactics/inv.ml b/tactics/inv.ml
new file mode 100644
index 000000000..a8b6787ed
--- /dev/null
+++ b/tactics/inv.ml
@@ -0,0 +1,562 @@
+
+(* $Id$ *)
+
+open Pp
+open Util
+open Names
+open Generic
+open Term
+open Global
+open Sign
+open Environ
+open Printer
+open Reduction
+open Tacmach
+open Proof_trees
+open Clenv
+open Tactics
+open Wcclausenv
+open Tacticals
+open Tactics
+open Elim
+open Equality
+open Typing
+
+(* [make_inv_predicate (ity,args) C]
+
+ is given the inductive type, its arguments, both the global
+ parameters and its local arguments, and is expected to produce a
+ predicate P such that if largs is the "local" part of the
+ arguments, then (P largs) will be convertible with a conclusion of
+ the form:
+
+ <A1>a1=a1-><A2>a2=a2 ... -> C
+
+ Algorithm: suppose length(largs)=n
+
+ (1) Push the entire arity, [xbar:Abar], carrying along largs and
+ the conclusion
+
+ (2) Pair up each ai with its respective Rel version: a1==(Rel n),
+ a2==(Rel n-1), etc.
+
+ (3) For each pair, ai,Rel j, if the Ai is dependent - that is, the
+ type of [Rel j] is an open term, then we construct the iterated
+ tuple, [make_iterated_tuple] does it, and use that for our equation
+
+ Otherwise, we just use <Ai>ai=Rel j
+
+ *)
+
+let named_push_and_liftl env n hyps t l =
+ let rec pushrec = function
+ | (0, t, (hyps,l)) -> (hyps,t,l)
+ | (n, (DOP2(Prod,t,DLAM(na,b))), (hyps,l)) ->
+ pushrec (n-1, b, (push_and_lift (Environ.named_hd env t na,t) hyps l))
+ | (n, (DOP2(Cast,t,_)), (hyps,l)) -> pushrec (n,t,(hyps,l))
+ | _ -> error "push_and_liftl"
+ in
+ pushrec (n,t,(hyps,l))
+
+let named_push_lambda_and_liftl env n hyps t l =
+ let rec pushrec = function
+ | (0, t, (hyps,l)) -> (hyps,t,l)
+ | (n, (DOP2(Lambda,t,DLAM(na,b))), (hyps,l)) ->
+ pushrec (n-1, b, (push_and_lift (Environ.named_hd env t na,t) hyps l))
+ | (n, (DOP2(Cast,t,_)), (hyps,l)) -> pushrec (n,t,(hyps,l))
+ | _ -> error "push_and_liftl"
+ in
+ pushrec (n,t,(hyps,l))
+
+let dest_match_eq gls eqn =
+ try
+ dest_match gls eqn eq_pattern
+ with _ ->
+ (try
+ dest_match gls eqn eqT_pattern
+ with _ ->
+ (try
+ dest_match gls eqn idT_pattern
+ with _ -> errorlabstrm "dest_match_eq"
+ [< 'sTR "no primitive equality here" >]))
+
+let type_of_predicate_argument gls ity globargs =
+ let env = pf_env gls in
+ let sigma = project gls in
+ let sort = sort_of_goal gls in
+ let elim = Indrec.make_case_gen env sigma ity sort in
+ let type_elim = type_of env sigma elim in
+ let nparams = mind_nparams ity in
+ let (hyps,predicate,_) = named_push_and_liftl env nparams [] type_elim [] in
+ let (_,predicate,_) = lam_and_popl nparams hyps predicate [] in
+ let prod = whd_beta env Evd.empty (applist (predicate,globargs)) in
+ let (_,ty,_) = destProd prod in
+ ty
+
+let implicit = Sort implicit_sort
+
+let change_sign env (vars,rels) =
+ let env' = change_hyps (fun _ -> vars) env in
+ List.fold_left
+ (fun env (n,t) ->
+ let tt = execute_type env Evd.empty t in push_rel (n,tt) env)
+ env' rels
+
+let make_inv_predicate (ity,args) c dflt_concl dep_option gls =
+ let env = pf_env gls in
+ let sigma = project gls in
+ let sign = pf_hyps gls in
+ let concl = (pf_concl gls) in
+ let id = destVar c in
+ let nparams = mind_nparams ity in
+ let (globargs,largs_init) = list_chop nparams args in
+ let arity = hnf_prod_applist env sigma "make_inv_predicate"
+ (nf_betadeltaiota env sigma (mind_arity ity)) globargs in
+ let len = List.length largs_init in
+ let hyps = [] in
+ let largs = (List.map insert_lifted largs_init) in
+ let (hyps,larg_var_list,concl,dephyp) =
+ if not dep_option (* (dependent (VAR id) concl) *) then
+ (* We push de arity and leave concl unchanged *)
+ let hyps_ar,_,largs_ar = named_push_and_liftl env len hyps arity largs in
+ let larg_var_list =
+ list_map_i
+ (fun i ai ->
+ insert_lifted
+ (DOP2(implicit,extract_lifted ai,Rel(len-i+1)))) 1 largs
+ in
+ (hyps_ar,larg_var_list,concl,0)
+ else
+ if not (dependent (VAR id) concl) then errorlabstrm "make_inv_predicate"
+ [< 'sTR "Current goal does not depend on "; print_id id >]
+ else
+ (* We abstract the conclusion of goal with respect to args and c to be
+ * concl in order to rewrite and have c also rewritten when the case
+ * will be done *)
+ let p=type_of_predicate_argument gls ity globargs in
+ let c2 =
+ (match dflt_concl with
+ | None -> abstract_list_all gls p concl (largs_init@[c])
+ | (Some concl) -> concl)
+ in
+ let hyps,_,largs =
+ named_push_lambda_and_liftl env (nb_lam c2) hyps c2 largs in
+ let c3 = whd_beta env Evd.empty
+ (applist (c2,Array.to_list
+ (rel_vect (List.length largs)
+ (nb_prod arity +1))))
+ in
+ let larg_var_list =
+ list_map_i
+ (fun i ai->
+ insert_lifted
+ (DOP2(implicit,extract_lifted ai,Rel(len-i+2)))) 1 largs
+ in
+ (hyps,larg_var_list,c3,1)
+ in
+ (* Now the arity is pushed, and we need to construct the pairs
+ * ai,Rel(n-i+1) *)
+ (* Now, we can recurse down this list, for each ai,(Rel k) whether to
+ push <Ai>(Rel k)=ai (when Ai is closed).
+ In any case, we carry along the rest of larg_var_list *)
+ let rec build_concl (hyps,l) =
+ match l with
+ | [] ->
+ let neqns = ((List.length hyps-dephyp)-len) in
+ let hyps,concl,_ = prod_and_popl neqns hyps concl [] in
+ let _,concl,_ = lam_and_popl (List.length hyps) hyps concl [] in
+ (concl,neqns)
+ | t::restlist ->
+ let (ai,k) =
+ match extract_lifted t with
+ | DOP2(_,ai,Rel k) -> (ai,k)
+ | _ -> assert false
+ in
+ let tk = (Typeops.relative (change_sign env (sign,hyps)) k).uj_val in
+ let (lhs,eqnty,rhs) =
+ if closed0 tk then
+ (Rel k,tk,ai)
+ else
+ make_iterated_tuple Evd.empty
+ (change_sign env (sign,hyps))
+ (ai,type_of env Evd.empty ai)
+ (Rel k,tk)
+ in
+ let type_type_rhs = type_of env sigma (type_of env sigma rhs) in
+ let sort = pf_type_of gls (pf_concl gls) in
+ let eq_term = find_eq_pattern type_type_rhs sort in
+ let eqn = applist (eq_term ,[eqnty;lhs;rhs]) in
+ build_concl (push_and_lift (Anonymous,eqn) hyps restlist)
+ in
+ let (predicate,neqns) = build_concl (hyps,larg_var_list) in
+ (* OK - this predicate should now be usable by res_elimination_then to
+ do elimination on the conclusion. *)
+ (predicate,neqns)
+
+(* The result of the elimination is a bunch of goals like:
+
+ |- (cibar:Cibar)Equands->C
+
+ where the cibar are either dependent or not. We are fed a
+ signature, with "true" for every recursive argument, and false for
+ every non-recursive one. So we need to do the
+ sign_branch_len(sign) intros, thinning out all recursive
+ assumptions. This leaves us with exactly length(sign) assumptions.
+
+ We save their names, and then do introductions for all the equands
+ (there are some number of them, which is the other argument of the
+ tactic)
+
+ This gives us the #neqns equations, whose names we get also, and
+ the #length(sign) arguments.
+
+ Suppose that #nodep of these arguments are non-dependent.
+ Generalize and thin them.
+
+ This gives us #dep = #length(sign)-#nodep arguments which are
+ dependent.
+
+ Now, we want to take each of the equations, and do all possible
+ injections to get the left-hand-side to be a variable. At the same
+ time, if we find a lhs/rhs pair which are different, we can
+ discriminate them to prove false and finish the branch.
+
+ Then, we thin away the equations, and do the introductions for the
+ #nodep arguments which we generalized before.
+ *)
+
+(* Called after the case-assumptions have been killed off, and all the
+ intros have been done. Given that the clause in question is an
+ equality (if it isn't we fail), we are responsible for projecting
+ the equality, using Injection and Discriminate, and applying it to
+ the concusion *)
+
+let introsReplacing ids gls =
+ let rec introrec = function
+ | [] -> tclIDTAC
+ | id::tl ->
+ (tclTHEN (tclORELSE (intro_replacing id)
+ (tclORELSE (intro_erasing id)
+ (intro_using id)))
+ (introrec tl))
+ in
+ introrec ids gls
+
+(* Computes the subset of hypothesis in the local context whose
+ type depends on t (should be of the form (VAR id)), then
+ it generalizes them, applies tac to rewrite all occurrencies of t,
+ and introduces generalized hypotheis.
+ Precondition: t=(VAR id) *)
+
+let rec dependent_hyps id idlist sign =
+ let rec dep_rec =function
+ | [] -> []
+ | (id1::l) ->
+ let id1ty = snd (lookup_var id1 sign) in
+ if occur_var id id1ty.body then id1::dep_rec l else dep_rec l
+ in
+ dep_rec idlist
+
+let generalizeRewriteIntros tac depids id gls =
+ let dids = dependent_hyps id depids (pf_env gls) in
+ (tclTHEN (bring_hyps (List.map in_some dids))
+ (tclTHEN tac
+ (introsReplacing dids)))
+ gls
+
+let var_occurs_in_pf gl id =
+ occur_var id (pf_concl gl) or
+ exists_sign (fun _ t -> occur_var id t) (pf_untyped_hyps gl)
+
+let split_dep_and_nodep idl gl =
+ (List.filter (var_occurs_in_pf gl) idl,
+ List.filter (fun x -> not(var_occurs_in_pf gl x)) idl)
+
+(* invariant: ProjectAndApply is responsible for erasing the clause
+ which it is given as input
+ It simplifies the clause (an equality) to use it as a rewrite rule and then
+ erases the result of the simplification. *)
+
+let dest_eq gls t =
+ match dest_match_eq gls t with
+ | [x;y;z] -> (x,y,z)
+ | _ -> error "dest_eq: should be an equality"
+
+(* invariant: ProjectAndApplyNoThining simplifies the clause (an equality) .
+ If it can discriminate then the goal is proved, if not tries to use it as
+ a rewrite rule. It erases the clause which is given as input *)
+
+let projectAndApply thin cls depids gls =
+ let subst_hyp_LR cls = tclTRY(hypSubst (out_some cls) None) in
+ let subst_hyp_RL cls = tclTRY(revHypSubst (out_some cls) None) in
+ let subst_hyp gls =
+ let orient_rule cls =
+ let (t,t1,t2) = dest_eq gls (clause_type cls gls) in
+ match (strip_outer_cast t1, strip_outer_cast t2) with
+ | (VAR id1, _) -> generalizeRewriteIntros (subst_hyp_LR cls) depids id1
+ | (_, VAR id2) -> generalizeRewriteIntros (subst_hyp_RL cls) depids id2
+ | _ -> subst_hyp_RL cls
+ in
+ onLastHyp orient_rule gls
+ in
+ let (t,t1,t2) = dest_eq gls (clause_type cls gls) in
+ match (thin, strip_outer_cast t1, strip_outer_cast t2) with
+ | (true, VAR id1, _) -> generalizeRewriteIntros
+ (tclTHEN (subst_hyp_LR cls) (clear_clause cls)) depids id1 gls
+ | (false, VAR id1, _) ->
+ generalizeRewriteIntros (subst_hyp_LR cls) depids id1 gls
+ | (true, _ , VAR id2) -> generalizeRewriteIntros
+ (tclTHEN (subst_hyp_RL cls) (clear_clause cls)) depids id2 gls
+ | (false, _ , VAR id2) ->
+ generalizeRewriteIntros (subst_hyp_RL cls) depids id2 gls
+ | (true, _, _) ->
+ let deq_trailer neqns =
+ tclDO neqns
+ (tclTHEN intro (tclTHEN subst_hyp (onLastHyp clear_clause)))
+ in
+ (tclTHEN (tclTRY (dEqThen deq_trailer cls)) (clear_clause cls)) gls
+ | (false, _, _) ->
+ let deq_trailer neqns = tclDO neqns (tclTHEN intro subst_hyp) in
+ (tclTHEN (dEqThen deq_trailer cls) (clear_clause cls)) gls
+
+(* Inversion qui n'introduit pas les hypotheses, afin de pouvoir les nommer
+ soi-meme (proposition de Valerie). *)
+let case_trailer_gene othin neqns ba gl =
+ let (depids,nodepids) = split_dep_and_nodep ba.assums gl in
+ let rewrite_eqns =
+ match othin with
+ | Some thin ->
+ onLastHyp
+ (fun last ->
+ (tclTHEN
+ (tclDO neqns
+ (tclTHEN intro
+ (onLastHyp
+ (fun cls ->
+ tclTRY (projectAndApply thin cls depids)))))
+ (tclTHEN
+ (onCL (compose List.rev (afterHyp (out_some last)))
+ bring_hyps)
+ (onCL (afterHyp (out_some last)) clear_clauses))))
+ | None -> tclIDTAC
+ in
+ (tclTHEN (tclDO neqns intro)
+ (tclTHEN (bring_hyps (List.map in_some nodepids))
+ (tclTHEN (clear_clauses (List.map in_some nodepids))
+ (tclTHEN (onCL (compose List.rev (nLastHyps neqns)) bring_hyps)
+ (tclTHEN (onCL (nLastHyps neqns) clear_clauses)
+ (tclTHEN rewrite_eqns
+ (tclMAP (fun id ->
+ (tclORELSE (clear_clause (Some id))
+ (tclTHEN (bring_hyps [Some id])
+ (clear_clause (Some id)))))
+ depids)))))))
+ gl
+
+(* Introduction of the equations on arguments
+ othin: discriminates Simple Inversion, Inversion and Inversion_clear
+ None: the equations are introduced, but not rewritten
+ Some thin: the equations are rewritten, and cleared if thin is true *)
+
+let case_trailer othin neqns ba gl =
+ let (depids,nodepids) = split_dep_and_nodep ba.assums gl in
+ let rewrite_eqns =
+ match othin with
+ | Some thin ->
+ (tclTHEN (onCL (compose List.rev (nLastHyps neqns)) bring_hyps)
+ (tclTHEN (onCL (nLastHyps neqns) clear_clauses)
+ (tclTHEN
+ (tclDO neqns
+ (tclTHEN intro
+ (onLastHyp
+ (fun cls ->
+ tclTRY (projectAndApply thin cls depids)))))
+ (tclTHEN (tclDO (List.length nodepids) intro)
+ (tclMAP (fun id ->
+ tclTRY (clear_clause (Some id))) depids)))))
+ | None -> tclIDTAC
+ in
+ (tclTHEN (tclDO neqns intro)
+ (tclTHEN (bring_hyps (List.map in_some nodepids))
+ (tclTHEN (clear_clauses (List.map in_some nodepids))
+ rewrite_eqns)))
+ gl
+
+let res_case_then gene thin indbinding c dflt_concl dep_option gl =
+ let (wc,kONT) = startWalk gl in
+ let t =
+ strong_prodspine (fun _ _ -> pf_whd_betadeltaiota gl)
+ (pf_env gl) (project gl) (pf_type_of gl c) in
+ let indclause = mk_clenv_from wc (c,t) in
+ let indclause' = clenv_constrain_with_bindings indbinding indclause in
+ let newc = clenv_instance_template indclause' in
+ let (ity,args) = decomp_app (clenv_instance_template_type indclause') in
+ let ity = destMutInd ity in
+ let (elim_predicate,neqns) =
+ make_inv_predicate (ity,args) c dflt_concl dep_option gl in
+ let nparams = mind_nparams ity in
+ let largs = snd (list_chop nparams args) in
+ let (cut_concl,case_tac) =
+ if dep_option & (dependent c (pf_concl gl)) then
+ applist(elim_predicate,largs@[c]),case_then_using
+ else
+ applist(elim_predicate,largs),case_nodep_then_using
+ in
+ let case_trailer_tac =
+ if gene then case_trailer_gene thin neqns else case_trailer thin neqns
+ in
+ (tclTHENS
+ (cut_intro cut_concl)
+ [onLastHyp
+ (fun cls->
+ (tclTHEN (applyUsing
+ (applist(VAR (out_some cls),
+ list_tabulate
+ (fun _ -> mkMeta(new_meta())) neqns)))
+ Auto.default_auto));
+ case_tac (introCaseAssumsThen case_trailer_tac)
+ (Some elim_predicate) ([],[]) newc])
+ gl
+
+(* Error messages of the inversion tactics *)
+let not_found_message ids =
+ if List.length ids = 1 then
+ [<'sTR "the variable"; 'sPC ; 'sTR (string_of_id (List.hd ids)) ; 'sPC;
+ 'sTR" was not found in the current environment" >]
+ else
+ [<'sTR "the variables [";
+ 'sPC ; prlist (fun id -> [<'sTR (string_of_id id) ; 'sPC >]) ids;
+ 'sTR" ] were not found in the current environment" >]
+
+let no_generalisation() =
+ errorlabstrm "Inv"
+ [< 'sTR "Cannot find a well typed generalisation of the goal">]
+
+let dep_prop_prop_message id =
+ errorlabstrm "Inv"
+ [< 'sTR "Inversion on "; print_id id ;
+ 'sTR " would needs dependent elimination Prop-Prop" >]
+
+let not_inductive_here id =
+ errorlabstrm "mind_specif_of_mind"
+ [< 'sTR "Cannot recognize an inductive predicate in "; print_id id ;
+ 'sTR ". If there is one, may be the structure of the arity or of the type of constructors is hidden by constant definitions." >]
+
+let wrap_inv_error id = function
+ | UserError ("abstract_list_all",_) -> no_generalisation ()
+ | UserError ("Case analysis",s) -> errorlabstrm "Inv needs Nodep Prop Set" s
+ | UserError("mind_specif_of_mind",_) -> not_inductive_here id
+ | UserError (a,b) -> errorlabstrm "Inv" b
+ | Invalid_argument "it_list2" -> dep_prop_prop_message id
+ | Invalid_argument("mind_specif_of_mind") -> not_inductive_here id
+ | Not_found -> errorlabstrm "Inv" (not_found_message [id])
+ | e -> raise e
+
+let inv gene com dflt_concl dep_option id =
+ let inv_tac = res_case_then gene com [] (VAR id) dflt_concl dep_option in
+ let tac =
+ if com = Some true (* if Inversion_clear, clear the hypothesis *) then
+ tclTHEN inv_tac (tclTRY (clear_clause (Some id)))
+ else
+ inv_tac
+ in
+ fun gls -> try tac gls with e -> wrap_inv_error id e
+
+let hinv_kind = Identifier (id_of_string "HalfInversion")
+let inv_kind = Identifier (id_of_string "Inversion")
+let invclr_kind = Identifier (id_of_string "InversionClear")
+
+let com_of_id id =
+ if id = hinv_kind then None
+ else if id = inv_kind then Some false
+ else Some true
+
+(* Inv generates nodependent inversion *)
+let (half_inv_tac, inv_tac, inv_clear_tac) =
+ let gentac =
+ hide_tactic "Inv"
+ (function
+ | [ic; Identifier id] -> inv false (com_of_id ic) None false id
+ | _ -> anomaly "Inv called with bad args")
+ in
+ ((fun id -> gentac [hinv_kind; Identifier id]),
+ (fun id -> gentac [inv_kind; Identifier id]),
+ (fun id -> gentac [invclr_kind; Identifier id]))
+
+(* Inversion without intros. No vernac entry yet! *)
+let named_inv =
+ let gentac =
+ hide_tactic "NamedInv"
+ (function
+ | [ic; Identifier id] -> inv true (com_of_id ic) None false id
+ | _ -> anomaly "NamedInv called with bad args")
+ in
+ (fun ic id -> gentac [ic; Identifier id])
+
+(* Generates a dependent inversion with a certain generalisation of the goal *)
+let (half_dinv_tac, dinv_tac, dinv_clear_tac) =
+ let gentac =
+ hide_tactic "DInv"
+ (function
+ | [ic; Identifier id] -> inv false (com_of_id ic) None true id
+ | _ -> anomaly "DInv called with bad args")
+ in
+ ((fun id -> gentac [hinv_kind; Identifier id]),
+ (fun id -> gentac [inv_kind; Identifier id]),
+ (fun id -> gentac [invclr_kind; Identifier id]))
+
+(* generates a dependent inversion using a given generalisation of the goal *)
+let (half_dinv_with, dinv_with, dinv_clear_with) =
+ let gentac =
+ hide_tactic "DInvWith"
+ (function
+ | [ic; Identifier id; Command com] ->
+ fun gls ->
+ inv false (com_of_id ic)
+ (Some (pf_constr_of_com gls com)) true id gls
+ | _ -> anomaly "DInvWith called with bad args")
+ in
+ ((fun id com -> gentac [hinv_kind; Identifier id; Command com]),
+ (fun id com -> gentac [inv_kind; Identifier id; Command com]),
+ (fun id com -> gentac [invclr_kind; Identifier id; Command com]))
+
+(* InvIn will bring the specified clauses into the conclusion, and then
+ * perform inversion on the named hypothesis. After, it will intro them
+ * back to their places in the hyp-list. *)
+
+let invIn com id ids gls =
+ let nb_prod_init = nb_prod (pf_concl gls) in
+ let intros_replace_ids gls =
+ let nb_of_new_hyp =
+ nb_prod (pf_concl gls) - (List.length ids + nb_prod_init)
+ in
+ if nb_of_new_hyp < 1 then
+ introsReplacing ids gls
+ else
+ (tclTHEN (tclDO nb_of_new_hyp intro) (introsReplacing ids)) gls
+ in
+ try
+ (tclTHEN (bring_hyps (List.map in_some ids))
+ (tclTHEN (inv false com None false id)
+ (intros_replace_ids)))
+ gls
+ with e -> wrap_inv_error id e
+
+let invIn_tac =
+ let gentac =
+ hide_tactic "InvIn"
+ (function
+ | (com::(Identifier id)::hl) ->
+ let hl' =
+ List.map (function
+ | Identifier id -> id
+ | _ -> anomaly "InvIn called with bas args") hl
+ in
+ invIn (com_of_id com) id hl'
+ | _ -> anomaly "InvIn called with bad args")
+ in
+ fun com id hl ->
+ gentac
+ ((Identifier (id_of_string com))
+ ::(Identifier id)
+ ::(List.map (fun id -> (Identifier id)) hl))
diff --git a/tactics/inv.mli b/tactics/inv.mli
new file mode 100644
index 000000000..52804f134
--- /dev/null
+++ b/tactics/inv.mli
@@ -0,0 +1,17 @@
+
+(* $Id$ *)
+
+(*i*)
+open Names
+open Tacmach
+(*i*)
+
+val inv_tac : identifier -> tactic
+val inv_clear_tac : identifier -> tactic
+val half_dinv_tac : identifier -> tactic
+val dinv_tac : identifier -> tactic
+val dinv_clear_tac : identifier -> tactic
+val half_dinv_with : identifier -> Coqast.t -> tactic
+val dinv_with : identifier -> Coqast.t -> tactic
+val dinv_clear_with : identifier -> Coqast.t -> tactic
+val invIn_tac : string -> identifier -> identifier list -> tactic
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
new file mode 100644
index 000000000..240a8e172
--- /dev/null
+++ b/tactics/leminv.ml
@@ -0,0 +1,419 @@
+
+(* $Id$ *)
+
+open Pp
+open Util
+open Names
+open Generic
+open Term
+open Sign
+open Evd
+open Printer
+open Reduction
+open Tacmach
+open Proof_trees
+open Clenv
+open Declare
+open Wcclausenv
+open Pattern
+open Tacticals
+open Tactics
+open Equality
+open Inv
+
+(* Fonctions temporaires pour relier la forme castée et la forme jugement *)
+let tsign_of_csign (idl,tl) = (idl,List.map outcast_type tl)
+
+let csign_of_tsign (idl,tl) = (idl,List.map incast_type tl)
+(* FIN TMP *)
+
+let not_work_message = "tactic fails to build the inversion lemma, may be because the predicate has arguments that depend on other arguments"
+
+(* 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_hyps_to_term (hyps,t) =
+ let vars = (global_vars t) in
+ rev_sign(fst(it_sign (fun ((hyps,globs) as sofar) id a ->
+ if List.mem id globs then
+ (add_sign (id,a) hyps,(global_vars a)@globs)
+ else sofar) (nil_sign,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 = initial_sign() 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
+ let (id::l) = lid in
+ max_rec (id, sign_prefix id sign) l
+
+let rel_of_env env =
+ let rec rel_rec = function
+ | ([], _) -> []
+ | ((_::env), n) -> (Rel n)::(rel_rec (env, n+1))
+ in
+ rel_rec (env, 1)
+
+let build_app op env = applist (op, List.rev (rel_of_env env))
+
+(* similar to prod_and_pop, but gives [na:T]B intead of (na:T)B *)
+
+let prod_and_pop_named = function
+ | ([], body, l, acc_ids) -> error "lam_and_pop"
+ | (((na,t)::tlenv), body, l, acc_ids) ->
+ let (Name id)=
+ if na=Anonymous then
+ Name(next_ident_away (id_of_string "a") acc_ids)
+ else
+ na
+ in
+ (tlenv,DOP2(Prod,t,DLAM((Name id),body)),
+ List.map (function
+ | (0,x) -> (0,lift (-1) x)
+ | (n,x) -> (n-1,x)) l,
+ (id::acc_ids))
+
+(* similar to prod_and_popl but gives [nan:Tan]...[na1:Ta1]B instead of
+ * (nan:Tan)...(na1:Ta1)B it generates new names with respect to l
+ whenever nai=Anonymous *)
+
+let prod_and_popl_named n env t l =
+ let rec poprec = function
+ | (0, (env,b,l,_)) -> (env,b,l)
+ | (n, ([],_,_,_)) -> error "lam_and_popl"
+ | (n, q) -> poprec (n-1, prod_and_pop_named q)
+ in
+ poprec (n,(env,t,l,[]))
+
+(* [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 t_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 thte
+ 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)(H:(I t_bar)->[sort]
+*)
+
+let compute_first_inversion_scheme sign i sort dep_option =
+ let (ity,largs) = find_mrectype empty_evd i in
+ let ar = mind_arity ity in
+ (* let ar = nf_betadeltaiota empty_evd (mind_arity ity) in *)
+ let fv = global_vars i in
+ let thin_sign = thin_hyps_to_term (sign,i) in
+ if not(same_members fv (ids_of_sign thin_sign)) 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" >];
+ let p = next_ident_away (id_of_string "P") (ids_of_sign sign) in
+ if dep_option then
+ let (pty,goal) =
+ let (env,_,_) = push_and_liftl (nb_prod ar) [] ar [] in
+ let h = next_ident_away (id_of_string "P") (ids_of_sign sign) in
+ let (env1,_)= push_and_lift (Name h, (build_app ity env)) env [] in
+ let (_,pty,_) = prod_and_popl_named (List.length env1) env1 sort [] in
+ let pHead= applist(VAR p, largs@[Rel 1])
+ in (pty, Environ.prod_name(Name h,i,pHead))
+ in
+ (prepend_sign thin_sign
+ (add_sign (p,nf_betadeltaiota empty_evd pty) nil_sign),
+ goal)
+ else
+ let local_sign = get_local_sign thin_sign in
+ let pHead=
+ applist(VAR p,
+ List.rev(List.map (fun id -> VAR id) (ids_of_sign local_sign)))in
+ let (pty,goal) =
+ (it_sign (fun b id ty -> mkNamedProd id ty b)
+ sort local_sign, mkArrow i pHead)
+ in
+ let npty = nf_betadeltaiota empty_evd pty in
+ let lid = global_vars npty in
+ let maxprefix =
+ if lid=[] then nil_sign else snd (max_prefix_sign lid thin_sign)
+ in
+ (prepend_sign local_sign (add_sign (p,npty) maxprefix), 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 sign i sort dep_option inv_op =
+ let (i,sign) = add_prods_sign empty_evd (i,sign) in
+ let sign = csign_of_tsign sign in
+ let (invSign,invGoal) =
+ compute_first_inversion_scheme sign i sort dep_option in
+ let invSign = castify_sign empty_evd invSign in
+ if (not((subset (global_vars invGoal) (ids_of_sign invSign)))) then
+ errorlabstrm "lemma_inversion"
+ [< 'sTR"Computed inversion goal was not closed in initial signature" >];
+ let invGoalj = fexecute empty_evd invSign invGoal in
+ let pfs =
+ mk_pftreestate
+ (mkGOAL (mt_ctxt Spset.empty) invSign (j_val_cast invGoalj)) in
+ let pfs =
+ solve_pftreestate (tclTHEN intro
+ (onLastHyp (comp inv_op outSOME))) pfs in
+ let pf = proof_of_pftreestate pfs in
+ let (pfterm,meta_types) = Refiner.extract_open_proof pf.goal.hyps pf in
+ let invSign =
+ sign_it
+ (fun id ty sign ->
+ if mem_sign (initial_sign()) id then sign
+ else add_sign (id,ty) sign)
+ invSign
+ nil_sign
+ in
+ let (invSign,mvb) =
+ List.fold_left
+ (fun (sign,mvb) (mv,mvty) ->
+ let h = next_ident_away (id_of_string "H") (ids_of_sign sign) in
+ (add_sign (h,mvty) sign,
+ (mv,((VAR h):constr))::mvb))
+ (csign_of_tsign invSign,[])
+ meta_types
+ in
+ let invProof =
+ it_sign (fun b id ty -> mkNamedLambda id ty b)
+ (strong (whd_meta mvb) pfterm) invSign
+ in
+ invProof
+
+open Discharge
+open Constrtypes
+
+let add_inversion_lemma name sign i sort dep_option inv_op =
+ let invProof = inversion_scheme sign i sort dep_option inv_op in
+ machine_constant_verbose (initial_assumptions())
+ ((name,false,NeverDischarge),invProof)
+
+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 pf = proof_of_pftreestate pts in
+ let gll,_ = frontier pf in
+ let gl = List.nth gll (n-1) in
+ add_inversion_lemma na gl.hyps (snd(lookup_sign id gl.hyps)).body
+ sort dep_option inv_op
+
+let inversion_clear = inv false (Some true) None
+
+open Vernacinterp
+
+let _ =
+ vinterp_add
+ ("MakeInversionLemmaFromHyp",
+ fun [VARG_NUMBER n;
+ VARG_IDENTIFIER na;
+ VARG_IDENTIFIER id] ->
+ fun () ->
+ inversion_lemma_from_goal n na id mkProp
+ false (inversion_clear false))
+
+let no_inductive_inconstr ass constr =
+ [< 'sTR "Cannot recognize an inductive predicate in "; term0 ass 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." >]
+
+let add_inversion_lemma_exn na constr sort bool tac =
+ try
+ (add_inversion_lemma na (initial_sign()) constr sort bool tac)
+ with
+ | Induc ->
+ errorlabstrm "add_inversion_lemma" (no_inductive_inconstr
+ (gLOB (initial_sign())) constr)
+ | UserError ("abstract_list_all",_) ->
+ no_generalisation()
+ | UserError ("Case analysis",s) ->
+ errorlabstrm "Inv needs Nodep Prop Set" s
+ | UserError ("mind_specif_of_mind",_) ->
+ errorlabstrm "mind_specif_of_mind"
+ (no_inductive_inconstr (gLOB (initial_sign())) constr)
+
+let _ =
+ vinterp_add
+ ("MakeInversionLemma",
+ fun [VARG_IDENTIFIER na;
+ VARG_COMMAND com;
+ VARG_COMMAND sort] ->
+ fun () ->
+ add_inversion_lemma_exn na
+ (constr_of_com empty_evd (initial_sign()) com)
+ (constr_of_com empty_evd (initial_sign()) sort)
+ false (inversion_clear false))
+
+let _ =
+ vinterp_add
+ ("MakeSemiInversionLemmaFromHyp",
+ fun [VARG_NUMBER n;
+ VARG_IDENTIFIER na;
+ VARG_IDENTIFIER id] ->
+ fun () ->
+ inversion_lemma_from_goal n na id mkProp false
+ (inversion_clear false))
+
+let _ =
+ vinterp_add
+ ("MakeSemiInversionLemma",
+ fun [VARG_IDENTIFIER na;
+ VARG_COMMAND com;
+ VARG_COMMAND sort] ->
+ fun () ->
+ add_inversion_lemma_exn na
+ (constr_of_com empty_evd (initial_sign()) com)
+ (constr_of_com empty_evd (initial_sign()) sort)
+ false (inv false (Some false) None false))
+
+let _ =
+ vinterp_add
+ ("MakeDependentInversionLemma",
+ fun [VARG_IDENTIFIER na;
+ VARG_COMMAND com;
+ VARG_COMMAND sort] ->
+ fun () ->
+ add_inversion_lemma_exn na
+ (constr_of_com empty_evd (initial_sign()) com)
+ (constr_of_com empty_evd (initial_sign()) sort)
+ true (inversion_clear true))
+
+let _ =
+ vinterp_add
+ ("MakeDependentSemiInversionLemma",
+ fun [VARG_IDENTIFIER na;
+ VARG_COMMAND com;
+ VARG_COMMAND sort] ->
+ fun () ->
+ add_inversion_lemma_exn na
+ (constr_of_com empty_evd (initial_sign()) com)
+ (constr_of_com empty_evd (initial_sign()) sort)
+ true (inversion_clear true))
+
+(* ================================= *)
+(* 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 [(ABS (-1),VAR id)] clause in
+ res_pf kONT clause gls
+ with
+ | Not_found ->
+ errorlabstrm "LemInv" (not_found_message [id])
+ | UserError (a,b) ->
+ errorlabstrm "LemInv"
+ [< 'sTR "Cannot refine current goal with the lemma ";
+ term0 (gLOB (initial_sign())) c >]
+
+let useInversionLemma =
+ let gentac =
+ hide_tactic "UseInversionLemma"
+ (fun [IDENTIFIER id;COMMAND com] gls ->
+ lemInv id (pf_constr_of_com gls com) gls)
+ (*fun sigma gl (_,[IDENTIFIER id;COMMAND com]) ->
+ [< 'sTR"UseInv" ; 'sPC ; print_id id ; 'sPC ; pr_com sigma gl com >]*)
+ in
+ fun id com -> gentac [IDENTIFIER id;COMMAND com]
+
+let lemInvIn id c ids gls =
+ 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
+ introsReplacing ids gls
+ else
+ (tclTHEN (tclDO nb_of_new_hyp intro) (introsReplacing ids)) gls
+ in
+ try
+ ((tclTHEN (tclTHEN (bring_hyps (List.map inSOME ids))
+ (lemInv id c))
+ (intros_replace_ids)) gls)
+ with Not_found -> errorlabstrm "LemInvIn" (not_found_message ids)
+ | UserError(a,b) -> errorlabstrm "LemInvIn" b
+
+let useInversionLemmaIn =
+ let gentac = hide_tactic "UseInversionLemmaIn"
+ (fun ((IDENTIFIER id)::(COMMAND com)::hl) gls ->
+ lemInvIn id (pf_constr_of_com gls com)
+ (List.map (fun (IDENTIFIER id) -> id) hl) gls)
+ in
+ fun id com hl ->
+ gentac ((IDENTIFIER id)::(COMMAND com)
+ ::(List.map (fun id -> (IDENTIFIER id)) hl))
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 18:18:01 +0000