diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-10-27 17:44:27 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-10-27 17:44:27 +0000 |
commit | d11d40bef81202f3bfea6174aece2709f069dc04 (patch) | |
tree | a1d42c3be3090f950b183193d9cbe7502915ec0e /tactics | |
parent | 95a66e52524b899cdfe3765c4b85296b82aa5416 (diff) |
Restructuration fonctions de réécriture depuis égalité dépendante; factorisation cut_replacing
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6261 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
-rw-r--r-- | tactics/equality.ml | 200 | ||||
-rw-r--r-- | tactics/equality.mli | 38 | ||||
-rw-r--r-- | tactics/tactics.ml | 85 | ||||
-rw-r--r-- | tactics/tactics.mli | 11 |
4 files changed, 159 insertions, 175 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index eb90fa213..fed587e4e 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -39,6 +39,7 @@ open Coqlib open Vernacexpr open Setoid_replace open Declarations +open Indrec (* Rewriting tactics *) @@ -47,10 +48,28 @@ open Declarations with type (A:<sort>)(x:A)(P:A->Prop)(P x)->(y:A)(eqname A y x)->(P y). If another equality myeq is introduced, then corresponding theorems myeq_ind_r, myeq_rec_r and myeq_rect_r have to be proven. See below. - -- Eduardo (19/8/97 + -- Eduardo (19/8/97) *) -let general_rewrite_bindings lft2rgt (c,l) gl = +let general_s_rewrite_clause = function + | None -> general_s_rewrite + | Some id -> general_s_rewrite_in id + +(* Ad hoc asymmetric general_elim_clause *) +let general_elim_clause cls c elim = match cls with + | None -> + (* was tclWEAK_PROGRESS which only fails for tactics generating one + subgoal and did not fail for useless conditional rewritings generating + an extra condition *) + tclNOTSAMEGOAL (general_elim c elim ~allow_K:false) + | Some id -> + general_elim_in id c elim + +let elimination_sort_of_clause = function + | None -> elimination_sort_of_goal + | Some id -> elimination_sort_of_hyp id + +let general_rewrite_bindings_clause cls lft2rgt (c,l) gl = let ctype = pf_type_of gl c in let env = pf_env gl in let sigma = project gl in @@ -58,21 +77,27 @@ let general_rewrite_bindings lft2rgt (c,l) gl = match match_with_equation t with | None -> if l = NoBindings - then general_s_rewrite lft2rgt c [] gl + then general_s_rewrite_clause cls lft2rgt c [] gl else error "The term provided does not end with an equation" | Some (hdcncl,_) -> let hdcncls = string_of_inductive hdcncl in - let suffix = Indrec.elimination_suffix (elimination_sort_of_goal gl)in + let suffix = elimination_suffix (elimination_sort_of_clause cls gl) in + let dir = if cls=None then lft2rgt else not lft2rgt in + let rwr_thm = if dir then hdcncls^suffix^"_r" else hdcncls^suffix in let elim = - if lft2rgt then - pf_global gl (id_of_string (hdcncls^suffix^"_r")) - else - pf_global gl (id_of_string (hdcncls^suffix)) + try pf_global gl (id_of_string rwr_thm) + with Not_found -> + error ("Cannot find rewrite principle "^rwr_thm) in - tclNOTSAMEGOAL (general_elim (c,l) (elim,NoBindings) ~allow_K:false) gl - (* was tclWEAK_PROGRESS which only fails for tactics generating one subgoal - and did not fail for useless conditional rewritings generating an - extra condition *) + general_elim_clause cls (c,l) (elim,NoBindings) gl + +let general_rewrite_bindings = general_rewrite_bindings_clause None +let general_rewrite l2r c = general_rewrite_bindings l2r (c,NoBindings) + +let general_rewrite_bindings_in l2r id = + general_rewrite_bindings_clause (Some id) l2r +let general_rewrite_in l2r id c = + general_rewrite_bindings_clause (Some id) l2r (c,NoBindings) (* Conditional rewriting, the success of a rewriting is related to the resolution of the conditions by a given tactic *) @@ -81,47 +106,22 @@ let conditional_rewrite lft2rgt tac (c,bl) = tclTHENSFIRSTn (general_rewrite_bindings lft2rgt (c,bl)) [|tclIDTAC|] (tclCOMPLETE tac) -let general_rewrite lft2rgt c = general_rewrite_bindings lft2rgt (c,NoBindings) - let rewriteLR_bindings = general_rewrite_bindings true let rewriteRL_bindings = general_rewrite_bindings false let rewriteLR = general_rewrite true let rewriteRL = general_rewrite false -(* The Rewrite in tactic *) -let general_rewrite_in lft2rgt id (c,l) gl = - let ctype = pf_type_of gl c in - let env = pf_env gl in - let sigma = project gl in - let _,t = splay_prod env sigma ctype in - match match_with_equation t with - | None -> (* Do not deal with setoids yet *) - if l = NoBindings - then general_s_rewrite_in id lft2rgt c [] gl - else error "The term provided does not end with an equation" - | Some (hdcncl,_) -> - let hdcncls = string_of_inductive hdcncl in - let suffix = - Indrec.elimination_suffix (elimination_sort_of_hyp id gl) in - let rwr_thm = - if lft2rgt then hdcncls^suffix else hdcncls^suffix^"_r" in - let elim = - try pf_global gl (id_of_string rwr_thm) - with Not_found -> - error ("Cannot find rewrite principle "^rwr_thm) in - general_elim_in id (c,l) (elim,NoBindings) gl - -let rewriteLRin = general_rewrite_in true -let rewriteRLin = general_rewrite_in false +let rewriteLRin_bindings = general_rewrite_bindings_in true +let rewriteRLin_bindings = general_rewrite_bindings_in false let conditional_rewrite_in lft2rgt id tac (c,bl) = - tclTHENSFIRSTn (general_rewrite_in lft2rgt id (c,bl)) + tclTHENSFIRSTn (general_rewrite_bindings_in lft2rgt id (c,bl)) [|tclIDTAC|] (tclCOMPLETE tac) let rewriteRL_clause = function | None -> rewriteRL_bindings - | Some id -> rewriteRLin id + | Some id -> rewriteRLin_bindings id (* Replacing tactics *) @@ -827,9 +827,8 @@ let swapEquandsInConcl gls = refine (applist(sym_equal,[t;e2;e1;Evarutil.mk_new_meta()])) gls let swapEquandsInHyp id gls = - ((tclTHENS (cut_replacing id (swap_equands gls (pf_get_hyp_typ gls id))) - ([tclIDTAC; - (tclTHEN (swapEquandsInConcl) (exact_no_check (mkVar id)))]))) gls + cut_replacing id (swap_equands gls (pf_get_hyp_typ gls id)) + (tclTHEN swapEquandsInConcl) gls (* find_elim determines which elimination principle is necessary to eliminate lbeq on sort_of_gl. It yields the boolean true wether @@ -940,9 +939,10 @@ let subst_tuple_term env sigma dep_pair b = |- (P e1) |- (eq T e1 e2) *) + (* Redondant avec Replace ! *) -let substInConcl_RL eqn gls = +let cutSubstInConcl_RL eqn gls = let (lbeq,(t,e1,e2)) = find_eq_data_decompose eqn in let body = subst_tuple_term (pf_env gls) (project gls) e2 (pf_concl gls) in assert (dependent (mkRel 1) body); @@ -953,28 +953,26 @@ let substInConcl_RL eqn gls = |- (P e2) |- (eq T e1 e2) *) -let substInConcl_LR eqn gls = - (tclTHENS (substInConcl_RL (swap_equands gls eqn)) +let cutSubstInConcl_LR eqn gls = + (tclTHENS (cutSubstInConcl_RL (swap_equands gls eqn)) ([tclIDTAC; swapEquandsInConcl])) gls -let substInConcl l2r = if l2r then substInConcl_LR else substInConcl_RL +let cutSubstInConcl l2r =if l2r then cutSubstInConcl_LR else cutSubstInConcl_RL -let substInHyp_LR eqn id gls = +let cutSubstInHyp_LR eqn id gls = let (lbeq,(t,e1,e2)) = find_eq_data_decompose eqn in let body = subst_term e1 (pf_get_hyp_typ gls id) in if not (dependent (mkRel 1) body) then errorlabstrm "SubstInHyp" (mt ()); - (tclTHENS (cut_replacing id (subst1 e2 body)) - ([tclIDTAC; - (tclTHENS (bareRevSubstInConcl lbeq body (t,e1,e2)) - ([exact_no_check (mkVar id);tclIDTAC]))])) gls + cut_replacing id (subst1 e2 body) + (tclTHENFIRST (bareRevSubstInConcl lbeq body (t,e1,e2))) gls -let substInHyp_RL eqn id gls = - (tclTHENS (substInHyp_LR (swap_equands gls eqn) id) +let cutSubstInHyp_RL eqn id gls = + (tclTHENS (cutSubstInHyp_LR (swap_equands gls eqn) id) ([tclIDTAC; swapEquandsInConcl])) gls -let substInHyp l2r = if l2r then substInHyp_LR else substInHyp_RL +let cutSubstInHyp l2r = if l2r then cutSubstInHyp_LR else cutSubstInHyp_RL let try_rewrite tac gls = try @@ -987,77 +985,51 @@ let try_rewrite tac gls = (str "Cannot find a well-typed generalization of the goal that" ++ str " makes the proof progress") -let subst l2r eqn cls gls = +let cutSubstClause l2r eqn cls gls = match cls with - | None -> substInConcl l2r eqn gls - | Some id -> substInHyp l2r eqn id gls + | None -> cutSubstInConcl l2r eqn gls + | Some id -> cutSubstInHyp l2r eqn id gls -(* |- (P a) - * SubstConcl_LR a=b - * |- (P b) - * |- a=b - *) +let cutRewriteClause l2r eqn cls = try_rewrite (cutSubstClause l2r eqn cls) +let cutRewriteInHyp l2r eqn id = cutRewriteClause l2r eqn (Some id) +let cutRewriteInConcl l2r eqn = cutRewriteClause l2r eqn None -let substConcl l2r eqn gls = try_rewrite (subst l2r eqn None) gls -let substConcl_LR = substConcl true +let substClause l2r c cls gls = + let eq = pf_type_of gls c in + tclTHENS (cutSubstClause l2r eq cls) [tclIDTAC; exact_no_check c] gls -(* id:(P a) |- G - * SubstHyp a=b id - * id:(P b) |- G - * id:(P a) |-a=b -*) +let rewriteClause l2r c cls = try_rewrite (substClause l2r c cls) +let rewriteInHyp l2r c id = rewriteClause l2r c (Some id) +let rewriteInConcl l2r c = rewriteClause l2r c None -let hypSubst l2r id cls gls = - onClauses (function - | None -> - (tclTHENS (substInConcl l2r (pf_get_hyp_typ gls id)) - ([tclIDTAC; exact_no_check (mkVar id)])) - | Some (hypid,_,_) -> - (tclTHENS (substInHyp l2r (pf_get_hyp_typ gls id) hypid) - ([tclIDTAC;exact_no_check (mkVar id)]))) - cls gls +(* Renaming scheme correspondence new name (old name) -let hypSubst_LR = hypSubst true + give equality give proof of equality -(* id:a=b |- (P a) - * HypSubst id. - * id:a=b |- (P b) - *) -let substHypInConcl l2r id gls = try_rewrite (hypSubst l2r id onConcl) gls -let substHypInConcl_LR = substHypInConcl true + / cutSubstClause (subst) substClause (HypSubst on hyp) +raw | cutSubstInHyp (substInHyp) substInHyp (none) + \ cutSubstInConcl (substInConcl) substInConcl (none) -(* id:a=b H:(P a) |- G - SubstHypInHyp id H. - id:a=b H:(P b) |- G -*) -(* |- (P b) - SubstConcl_RL a=b - |- (P a) - |- a=b -*) -let substConcl_RL = substConcl false + / cutRewriteClause (none) rewriteClause (none) +user| cutRewriteInHyp (substHyp) rewriteInHyp (none) + \ cutRewriteInConcl (substConcl) rewriteInConcl (substHypInConcl on hyp) -(* id:(P b) |-G - SubstHyp_RL a=b id - id:(P a) |- G - |- a=b +raw = raise typing error or PatternMatchingFailure +user = raise user error specific to rewrite *) -let substHyp l2r eqn id gls = try_rewrite (subst l2r eqn (Some id)) gls -let substHyp_RL = substHyp false +(* Summary of obsolete forms +let substInConcl = cutSubstInConcl +let substInHyp = cutSubstInHyp +let hypSubst l2r id = substClause l2r (mkVar id) +let hypSubst_LR = hypSubst true let hypSubst_RL = hypSubst false - -(* id:a=b |- (P b) - * HypSubst id. - * id:a=b |- (P a) - *) -let substHypInConcl_RL = substHypInConcl false - -(* id:a=b H:(P b) |- G - SubstHypInHyp id H. - id:a=b H:(P a) |- G +let substHypInConcl l2r id = rewriteInConcl l2r (mkVar id) +let substConcl = cutRewriteInConcl +let substHyp = cutRewriteInHyp *) +(**********************************************************************) (* Substitutions tactics (JCF) *) let unfold_body x gl = @@ -1172,7 +1144,7 @@ let rewrite_assumption_cond_in faildir hyp gl = | [] -> error "No such assumption" | (id,_,t)::rest -> (try let dir = faildir t gl in - general_rewrite_in dir hyp ((mkVar id),NoBindings) gl + general_rewrite_in dir hyp (mkVar id) gl with Failure _ | UserError _ -> arec rest) in arec (pf_hyps gl) diff --git a/tactics/equality.mli b/tactics/equality.mli index 672c4014a..f511fe675 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -28,14 +28,24 @@ val find_eq_pattern : sorts -> sorts -> constr val general_rewrite_bindings : bool -> constr with_bindings -> tactic val general_rewrite : bool -> constr -> tactic + +(* Obsolete, use [general_rewrite_bindings l2r] val rewriteLR_bindings : constr with_bindings -> tactic val rewriteRL_bindings : constr with_bindings -> tactic +*) +(* Equivalent to [general_rewrite l2r] *) val rewriteLR : constr -> tactic val rewriteRL : constr -> tactic +(* Warning: old [general_rewrite_in] is now [general_rewrite_bindings_in] *) + +val general_rewrite_bindings_in : + bool -> identifier -> constr with_bindings -> tactic +val general_rewrite_in : + bool -> identifier -> constr -> tactic + val conditional_rewrite : bool -> tactic -> constr with_bindings -> tactic -val general_rewrite_in : bool -> identifier -> constr with_bindings -> tactic val conditional_rewrite_in : bool -> identifier -> tactic -> constr with_bindings -> tactic @@ -57,12 +67,36 @@ val dEqThen : (int -> tactic) -> quantified_hypothesis option -> tactic val make_iterated_tuple : env -> evar_map -> constr -> (constr * types) -> constr * constr * constr +(* The family cutRewriteIn expect an equality statement *) +val cutRewriteInHyp : bool -> types -> identifier -> tactic +val cutRewriteInConcl : bool -> constr -> tactic + +(* The family rewriteIn expect the proof of an equality *) +val rewriteInHyp : bool -> constr -> identifier -> tactic +val rewriteInConcl : bool -> constr -> tactic + +(* Expect the proof of an equality; fails with raw internal errors *) +val substClause : bool -> constr -> identifier option -> tactic + +(* +(* [substHypInConcl l2r id] is obsolete: use [rewriteInConcl l2r (mkVar id)] *) val substHypInConcl : bool -> identifier -> tactic + +(* [substConcl] is an obsolete synonym for [cutRewriteInConcl] *) val substConcl : bool -> constr -> tactic -val substHyp : bool -> constr -> identifier -> tactic +(* [substHyp] is an obsolete synonym of [cutRewriteInHyp] *) +val substHyp : bool -> types -> identifier -> tactic +*) + +(* Obsolete, use [rewriteInConcl lr (mkVar id)] in concl + or [rewriteInHyp lr (mkVar id) (Some hyp)] in hyp + (which, if they fail, raise only UserError, not PatternMatchingFailure) + or [substClause lr (mkVar id) None] + or [substClause lr (mkVar id) (Some hyp)] val hypSubst_LR : identifier -> clause -> tactic val hypSubst_RL : identifier -> clause -> tactic +*) val discriminable : env -> evar_map -> constr -> constr -> bool diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 11f2e38fe..dc2865be4 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -41,6 +41,7 @@ open Genarg open Tacexpr open Decl_kinds open Evarutil +open Indrec exception Bound @@ -309,7 +310,7 @@ let rec intros_using = function let intros = tclREPEAT (intro_force false) -let intro_erasing id = tclTHEN (thin [id]) (intro_using id) +let intro_erasing id = tclTHEN (thin [id]) (introduction id) let intros_replacing ids gls = let rec introrec = function @@ -530,14 +531,13 @@ let cut c gl = | _ -> error "Not a proposition or a type" let cut_intro t = tclTHENFIRST (cut t) intro - -let cut_replacing id t = - tclTHENFIRST - (cut t) - (tclORELSE + +let cut_replacing id t tac = + tclTHENS (cut t) + [tclORELSE (intro_replacing id) - (tclORELSE (intro_erasing id) - (intro_using id))) + (tclORELSE (intro_erasing id) (intro_using id)); + tac (refine_no_check (mkVar id)) ] let cut_in_parallel l = let rec prec = function @@ -895,7 +895,7 @@ let last_arg c = match kind_of_term c with | App (f,cl) -> array_last cl | _ -> anomaly "last_arg" -let elimination_clause_scheme elimclause indclause allow_K gl = +let elimination_clause_scheme allow_K elimclause indclause gl = let indmv = (match kind_of_term (last_arg elimclause.templval.rebus) with | Meta mv -> mv @@ -919,40 +919,30 @@ let type_clenv_binding wc (c,t) lbind = * matching I, lbindc are the expected terms for c arguments *) -let general_elim (c,lbindc) (elimc,lbindelimc) ?(allow_K=true) gl = +let general_elim_clause elimtac (c,lbindc) (elimc,lbindelimc) gl = let ct = pf_type_of gl c in let t = try snd (pf_reduce_to_quantified_ind gl ct) with UserError _ -> ct in let indclause = make_clenv_binding gl (c,t) lbindc in let elimt = pf_type_of gl elimc in let elimclause = make_clenv_binding gl (elimc,elimt) lbindelimc in - elimination_clause_scheme elimclause indclause allow_K gl + elimtac elimclause indclause gl + +let general_elim c e ?(allow_K=true) = + general_elim_clause (elimination_clause_scheme allow_K) c e (* Elimination tactic with bindings but using the default elimination * constant associated with the type. *) let find_eliminator c gl = - let env = pf_env gl in - let (ind,t) = reduce_to_quantified_ind env (project gl) (pf_type_of gl c) in - let s = elimination_sort_of_goal gl in - Indrec.lookup_eliminator ind s -(* with Not_found -> - let dir, base = repr_path (path_of_inductive env ind) in - let id = Indrec.make_elimination_ident base s in - errorlabstrm "default_elim" - (str "Cannot find the elimination combinator :" ++ - pr_id id ++ spc () ++ - str "The elimination of the inductive definition :" ++ - pr_id base ++ spc () ++ str "on sort " ++ - spc () ++ print_sort (new_sort_in_family s) ++ - str " is probably not allowed") -(* lookup_eliminator prints the message *) *) -let default_elim (c,lbindc) gl = - general_elim (c,lbindc) (find_eliminator c gl,NoBindings) gl - -let elim_in_context (c,_ as cx) elim gl = - match elim with - | Some (elimc,lbindelimc) -> general_elim cx (elimc,lbindelimc) gl - | None -> general_elim cx (find_eliminator c gl,NoBindings) gl + let (ind,t) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in + Indrec.lookup_eliminator ind (elimination_sort_of_goal gl) + +let default_elim (c,_ as cx) gl = + general_elim cx (find_eliminator c gl,NoBindings) gl + +let elim_in_context c = function + | Some elim -> general_elim c elim ~allow_K:true + | None -> default_elim c let elim (c,lbindc as cx) elim = match kind_of_term c with @@ -985,31 +975,20 @@ let elimination_in_clause_scheme id elimclause indclause gl = (str "Nothing to rewrite in " ++ pr_id id); tclTHEN (tclEVARS (evars_of elimclause''.env)) - (tclTHENS - (cut new_hyp_typ) - [ (* Try to insert the new hyp at the same place *) - tclORELSE (intro_replacing id) - (tclTHEN (clear [id]) (introduction id)); - refine_no_check new_hyp_prf]) gl - -let general_elim_in id (c,lbindc) (elimc,lbindelimc) gl = - let ct = pf_type_of gl c in - let t = try snd (pf_reduce_to_quantified_ind gl ct) with UserError _ -> ct in - let indclause = make_clenv_binding gl (c,t) lbindc in - let elimt = pf_type_of gl elimc in - let elimclause = make_clenv_binding gl (elimc,elimt) lbindelimc in - elimination_in_clause_scheme id elimclause indclause gl + (cut_replacing id new_hyp_typ + (fun x gls -> refine_no_check new_hyp_prf gls)) gl + +let general_elim_in id = + general_elim_clause (elimination_in_clause_scheme id) (* Case analysis tactics *) let general_case_analysis_in_context (c,lbindc) gl = - let env = pf_env gl in let (mind,_) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in - let sigma = project gl in let sort = elimination_sort_of_goal gl in - let case = if occur_term c (pf_concl gl) then Indrec.make_case_dep - else Indrec.make_case_gen in - let elim = case env sigma mind sort in + let case = + if occur_term c (pf_concl gl) then make_case_dep else make_case_gen in + let elim = pf_apply case gl mind sort in general_elim (c,lbindc) (elim,NoBindings) gl let general_case_analysis (c,lbindc as cx) = @@ -1372,7 +1351,7 @@ let induction_tac varname typ ((elimc,lbindelimc),elimt) gl = let indclause = make_clenv_binding gl (c,typ) NoBindings in let elimclause = make_clenv_binding gl (mkCast (elimc,elimt),elimt) lbindelimc in - elimination_clause_scheme elimclause indclause true gl + elimination_clause_scheme true elimclause indclause gl let make_up_names7 n ind (old_style,cname) = if old_style (* = V6.3 version of Induction on hypotheses *) diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 6d0f9024b..a6b906b34 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -166,15 +166,13 @@ val cut_and_apply : constr -> tactic val general_elim : constr with_bindings -> constr with_bindings -> ?allow_K:bool -> tactic +val general_elim_in : + identifier -> constr with_bindings -> constr with_bindings -> tactic + val default_elim : constr with_bindings -> tactic val simplest_elim : constr -> tactic val elim : constr with_bindings -> constr with_bindings option -> tactic -val general_elim_in : identifier -> constr * constr bindings -> - constr * constr bindings -> tactic - val simple_induct : quantified_hypothesis * (bool ref * intro_pattern_expr list ref list) list ref -> tactic -val general_elim_in : identifier -> constr * constr bindings -> - constr * constr bindings -> tactic val new_induct : constr induction_arg -> constr with_bindings option -> intro_pattern_expr option * (bool ref * intro_pattern_expr list ref list) list ref @@ -236,7 +234,8 @@ val intros_transitivity : constr -> tactic val cut : constr -> tactic val cut_intro : constr -> tactic -val cut_replacing : identifier -> constr -> tactic +val cut_replacing : + identifier -> constr -> (tactic -> tactic) -> tactic val cut_in_parallel : constr list -> tactic val assert_tac : bool -> name -> constr -> tactic |