diff options
| -rw-r--r-- | contrib/ring/quote.ml | 2 | ||||
| -rw-r--r-- | kernel/inductive.mli | 3 | ||||
| -rw-r--r-- | kernel/term.ml | 21 | ||||
| -rw-r--r-- | kernel/term.mli | 3 | ||||
| -rw-r--r-- | pretyping/termops.ml | 2 | ||||
| -rw-r--r-- | pretyping/termops.mli | 3 | ||||
| -rw-r--r-- | proofs/clenv.ml | 121 | ||||
| -rw-r--r-- | proofs/clenv.mli | 9 | ||||
| -rw-r--r-- | tactics/auto.ml | 4 | ||||
| -rw-r--r-- | tactics/equality.ml | 117 | ||||
| -rw-r--r-- | tactics/setoid_replace.ml | 2 | ||||
| -rw-r--r-- | tactics/tacticals.ml | 9 | ||||
| -rw-r--r-- | tactics/tacticals.mli | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 45 | ||||
| -rw-r--r-- | tactics/tactics.mli | 3 | ||||
| -rw-r--r-- | tactics/wcclausenv.ml | 7 | ||||
| -rwxr-xr-x | theories/Bool/Bool.v | 2 |
17 files changed, 179 insertions, 176 deletions
diff --git a/contrib/ring/quote.ml b/contrib/ring/quote.ml index 10c05ec0e..669fd21c5 100644 --- a/contrib/ring/quote.ml +++ b/contrib/ring/quote.ml @@ -268,7 +268,7 @@ let compute_ivs gl f cs = (* The Cases predicate is a lambda; we assume no dependency *) let p = match kind_of_term p with - | Lambda (_,_,p) -> pop p + | Lambda (_,_,p) -> Termops.pop p | _ -> p in diff --git a/kernel/inductive.mli b/kernel/inductive.mli index 719205331..79900a84e 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -43,9 +43,6 @@ val type_of_constructor : env -> constructor -> types (* Return constructor types in normal form *) val arities_of_constructors : env -> inductive -> types array - -exception Arity of (constr * constr * Type_errors.arity_error) option - (* [type_case_branches env (I,args) (p:A) c] computes useful types about the following Cases expression: <p>Cases (c :: (I args)) of b1..bn end diff --git a/kernel/term.ml b/kernel/term.ml index 16524ea46..62f21de5f 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -644,15 +644,14 @@ let map_rel_declaration = map_named_declaration (* Occurring *) (*********************) -exception FreeVar -exception Occur +exception LocalOccur (* (closedn n M) raises FreeVar if a variable of height greater than n occurs in M, returns () otherwise *) let closedn = let rec closed_rec n c = match kind_of_term c with - | Rel m -> if m>n then raise FreeVar + | Rel m -> if m>n then raise LocalOccur | _ -> iter_constr_with_binders succ closed_rec n c in closed_rec @@ -660,26 +659,26 @@ let closedn = (* [closed0 M] is true iff [M] is a (deBruijn) closed term *) let closed0 term = - try closedn 0 term; true with FreeVar -> false + try closedn 0 term; true with LocalOccur -> false (* (noccurn n M) returns true iff (Rel n) does NOT occur in term M *) let noccurn n term = let rec occur_rec n c = match kind_of_term c with - | Rel m -> if m = n then raise Occur + | Rel m -> if m = n then raise LocalOccur | _ -> iter_constr_with_binders succ occur_rec n c in - try occur_rec n term; true with Occur -> false + try occur_rec n term; true with LocalOccur -> false (* (noccur_between n m M) returns true iff (Rel p) does NOT occur in term M for n <= p < n+m *) let noccur_between n m term = let rec occur_rec n c = match kind_of_term c with - | Rel(p) -> if n<=p && p<n+m then raise Occur + | Rel(p) -> if n<=p && p<n+m then raise LocalOccur | _ -> iter_constr_with_binders succ occur_rec n c in - try occur_rec n term; true with Occur -> false + try occur_rec n term; true with LocalOccur -> false (* Checking function for terms containing existential variables. The function [noccur_with_meta] considers the fact that @@ -690,7 +689,7 @@ let noccur_between n m term = let noccur_with_meta n m term = let rec occur_rec n c = match kind_of_term c with - | Rel p -> if n<=p & p<n+m then raise Occur + | Rel p -> if n<=p & p<n+m then raise LocalOccur | App(f,cl) -> (match kind_of_term f with | Cast (c,_) when isMeta c -> () @@ -699,7 +698,7 @@ let noccur_with_meta n m term = | Evar (_, _) -> () | _ -> iter_constr_with_binders succ occur_rec n c in - try (occur_rec n term; true) with Occur -> false + try (occur_rec n term; true) with LocalOccur -> false (*********************) @@ -720,8 +719,6 @@ let liftn k n = let lift k = liftn k 1 -let pop t = lift (-1) t - (*********************) (* Substituting *) (*********************) diff --git a/kernel/term.mli b/kernel/term.mli index 00f835e0d..73f29ddbe 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -418,9 +418,6 @@ val liftn : int -> int -> constr -> constr (* [lift n c] lifts by [n] the positive indexes in [c] *) val lift : int -> constr -> constr -(* [pop c] lifts by -1 the positive indexes in [c] *) -val pop : constr -> constr - (* [substnl [a1;...;an] k c] substitutes in parallel [a1],...,[an] for respectively [Rel(k+1)],...,[Rel(k+n)] in [c]; it relocates accordingly indexes in [a1],...,[an] *) diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 867bbf50f..11afda96b 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -331,6 +331,8 @@ let dependent m t = in try deprec m t; false with Occur -> true +let pop t = lift (-1) t + (***************************) (* substitution functions *) (***************************) diff --git a/pretyping/termops.mli b/pretyping/termops.mli index 1bb74a303..c45b1b016 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -76,6 +76,9 @@ val subst_meta : (int * constr) list -> constr -> constr val whd_locals : env -> constr -> constr val nf_locals : env -> constr -> constr +(* [pop c] lifts by -1 the positive indexes in [c] *) +val pop : constr -> constr + (* substitution of an arbitrary large term. Uses equality modulo reduction of let *) val dependent : constr -> constr -> bool diff --git a/proofs/clenv.ml b/proofs/clenv.ml index ae45154cd..f7cfd7dab 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -25,6 +25,27 @@ open Reductionops open Tacmach open Evar_refiner +(* if lname_typ is [xn,An;..;x1,A1] and l is a list of terms, + gives [x1:A1]..[xn:An]c' such that c converts to ([x1:A1]..[xn:An]c' l) *) + +let abstract_scheme env c l lname_typ = + List.fold_left2 + (fun t (locc,a) (na,_,ta) -> + if occur_meta ta then error "cannot find a type for the generalisation" + else if occur_meta a then lambda_name env (na,ta,t) + else lambda_name env (na,ta,subst_term_occ env locc a t)) + c + (List.rev l) + lname_typ + +let abstract_list_all env sigma typ c l = + let ctxt,_ = decomp_n_prod env sigma (List.length l) typ in + let p = abstract_scheme env c (List.map (function a -> [],a) l) ctxt in + try + if is_conv_leq env sigma (Typing.type_of env sigma p) typ then p + else error "abstract_list_all" + with UserError _ -> + raise (RefinerError (CannotGeneralize typ)) (* Generator of metavariables *) let meta_ctr=ref 0;; @@ -638,13 +659,12 @@ let clenv_merge with_types = [clenv_typed_unify M N clenv] expects in addition that expected types of metavars are unifiable with the types of their instances *) -let clenv_unify_core with_types cv_pb m n clenv = +let clenv_unify_core_0 with_types cv_pb m n clenv = let (mc,ec) = unify_0 cv_pb [] clenv.hook m n in clenv_merge with_types mc ec clenv - -(* let clenv_unify = clenv_unify_core false *) -let clenv_unify = clenv_unify_core false -let clenv_typed_unify = clenv_unify_core true + +let clenv_unify_0 = clenv_unify_core_0 false +let clenv_typed_unify = clenv_unify_core_0 true (* takes a substitution s, an open term op and a closed term cl @@ -665,7 +685,7 @@ let constrain_clenv_to_subterm clause (op,cl) = let cl = strip_outer_cast cl in (try if closed0 cl - then clenv_unify CONV op cl clause,cl + then clenv_unify_0 CONV op cl clause,cl else error "Bound 1" with ex when catchable_exception ex -> (match kind_of_term cl with @@ -734,35 +754,13 @@ let constrain_clenv_using_subterm_list allow_K clause oplist t = oplist (clause,[]) -(* if lname_typ is [xn,An;..;x1,A1] and l is a list of terms, - gives [x1:A1]..[xn:An]c' such that c converts to ([x1:A1]..[xn:An]c' l) *) - -let abstract_scheme env c l lname_typ = - List.fold_left2 - (fun t (locc,a) (na,_,ta) -> - if occur_meta ta then error "cannot find a type for the generalisation" - else if occur_meta a then lambda_name env (na,ta,t) - else lambda_name env (na,ta,subst_term_occ env locc a t)) - c - (List.rev l) - lname_typ - -let abstract_list_all env sigma typ c l = - let ctxt,_ = decomp_n_prod env sigma (List.length l) typ in - let p = abstract_scheme env c (List.map (function a -> [],a) l) ctxt in - try - if is_conv_leq env sigma (Typing.type_of env sigma p) typ then p - else error "abstract_list_all" - with UserError _ -> - raise (RefinerError (CannotGeneralize typ)) - let secondOrderAbstraction allow_K typ (p, oplist) clause = let env = w_env clause.hook in let sigma = w_Underlying clause.hook in let (clause',cllist) = constrain_clenv_using_subterm_list allow_K clause oplist typ in let typp = clenv_instance_type clause' p in - clenv_unify CONV (mkMeta p) + clenv_unify_0 CONV (mkMeta p) (abstract_list_all env sigma typp typ cllist) clause' @@ -775,13 +773,13 @@ let clenv_unify2 allow_K cv_pb ty1 ty2 clause = let clause' = secondOrderAbstraction allow_K ty2 (p1,oplist1) clause in (* Resume first order unification *) - clenv_unify cv_pb (clenv_instance_term clause' ty1) ty2 clause' + clenv_unify_0 cv_pb (clenv_instance_term clause' ty1) ty2 clause' | _, Meta p2 -> (* Find the predicate *) let clause' = secondOrderAbstraction allow_K ty1 (p2, oplist2) clause in (* Resume first order unification *) - clenv_unify cv_pb ty1 (clenv_instance_term clause' ty2) clause' + clenv_unify_0 cv_pb ty1 (clenv_instance_term clause' ty2) clause' | _ -> error "clenv_unify2" @@ -805,13 +803,13 @@ let clenv_unify2 allow_K cv_pb ty1 ty2 clause = Before, second-order was used if the type of Meta(1) and [x:A]t was convertible and first-order otherwise. But if failed if e.g. the type of Meta(1) had meta-variables in it. *) -let clenv_unify_gen allow_K cv_pb ty1 ty2 clenv = +let clenv_unify allow_K cv_pb ty1 ty2 clenv = let hd1,l1 = whd_stack ty1 in let hd2,l2 = whd_stack ty2 in match kind_of_term hd1, l1<>[], kind_of_term hd2, l2<>[] with | (Meta _, true, Lambda _, _ | Lambda _, _, Meta _, true) -> (try - clenv_unify cv_pb ty1 ty2 clenv + clenv_unify_0 cv_pb ty1 ty2 clenv with ex when catchable_exception ex -> try clenv_unify2 allow_K cv_pb ty1 ty2 clenv @@ -827,7 +825,7 @@ let clenv_unify_gen allow_K cv_pb ty1 ty2 clenv = with ex when catchable_exception ex -> error "Cannot solve a second-order unification problem") - | _ -> clenv_unify CONV ty1 ty2 clenv + | _ -> clenv_unify_0 CONV ty1 ty2 clenv (* [clenv_bchain mv clenv' clenv] @@ -863,7 +861,7 @@ let clenv_bchain mv subclenv clenv = in (* unify the type of the template of [subclenv] with the type of [mv] *) let clenv'' = - clenv_unify_gen true CUMUL + clenv_unify true CUMUL (clenv_instance clenv' (clenv_template_type subclenv)) (clenv_instance_type clenv' mv) clenv' @@ -931,33 +929,33 @@ let dependent_metas clenv mvs conclmetas = Intset.union deps (clenv_metavars clenv mv)) mvs conclmetas -let clenv_dependent clenv (cval,ctyp) = - let mvs = collect_metas (clenv_instance clenv cval) in - let ctyp_mvs = metavars_of (clenv_instance clenv ctyp) in +let clenv_dependent clenv = + let mvs = collect_metas (clenv_instance_template clenv) in + let ctyp_mvs = metavars_of (clenv_instance_template_type clenv) in let deps = dependent_metas clenv mvs ctyp_mvs in List.filter (fun mv -> Intset.mem mv deps) mvs -(* [clenv_independent clenv (cval,ctyp)] +(* [clenv_independent clenv] * returns a list of metavariables which appear in the term cval, * and which are not dependent. That is, they do not appear in * the types of other metavars which are in cval, nor in the type * of cval, ctyp. *) -let clenv_independent clenv (cval,ctyp) = - let mvs = collect_metas (clenv_instance clenv cval) in - let ctyp_mvs = metavars_of (clenv_instance clenv ctyp) in +let clenv_independent clenv = + let mvs = collect_metas (clenv_instance_template clenv) in + let ctyp_mvs = metavars_of (clenv_instance_template_type clenv) in let deps = dependent_metas clenv mvs ctyp_mvs in List.filter (fun mv -> not (Intset.mem mv deps)) mvs -(* [clenv_missing clenv (cval,ctyp)] +(* [clenv_missing clenv] * returns a list of the metavariables which appear in the term cval, * and which are dependent, and do NOT appear in ctyp. *) -let clenv_missing clenv (cval,ctyp) = - let mvs = collect_metas (clenv_instance clenv cval) in - let ctyp_mvs = metavars_of (clenv_instance clenv ctyp) in +let clenv_missing clenv = + let mvs = collect_metas (clenv_instance_template clenv) in + let ctyp_mvs = metavars_of (clenv_instance_template_type clenv) in let deps = dependent_metas clenv mvs ctyp_mvs in List.filter (fun n -> Intset.mem n deps && not (Intset.mem n ctyp_mvs)) @@ -967,11 +965,10 @@ let clenv_constrain_missing_args mlist clause = if mlist = [] then clause else - let occlist = clenv_missing clause (clenv_template clause, - (clenv_template_type clause)) in + let occlist = clenv_missing clause in if List.length occlist = List.length mlist then List.fold_left2 - (fun clenv occ m -> clenv_unify_gen true CONV (mkMeta occ) m clenv) + (fun clenv occ m -> clenv_unify true CONV (mkMeta occ) m clenv) clause occlist mlist else error ("Not the right number of missing arguments (expected " @@ -981,11 +978,10 @@ let clenv_constrain_dep_args mlist clause = if mlist = [] then clause else - let occlist = clenv_dependent clause (clenv_template clause, - (clenv_template_type clause)) in + let occlist = clenv_dependent clause in if List.length occlist = List.length mlist then List.fold_left2 - (fun clenv occ m -> clenv_unify_gen true CONV (mkMeta occ) m clenv) + (fun clenv occ m -> clenv_unify true CONV (mkMeta occ) m clenv) clause occlist mlist else error ("Not the right number of missing arguments (expected " @@ -995,11 +991,10 @@ let clenv_constrain_dep_args_of mv mlist clause = if mlist = [] then clause else - let occlist = clenv_dependent clause (clenv_value clause mv, - clenv_type clause mv) in + let occlist = clenv_dependent clause in if List.length occlist = List.length mlist then List.fold_left2 - (fun clenv occ m -> clenv_unify_gen true CONV (mkMeta occ) m clenv) + (fun clenv occ m -> clenv_unify true CONV (mkMeta occ) m clenv) clause occlist mlist else error ("clenv_constrain_dep_args_of: Not the right number " ^ @@ -1016,10 +1011,7 @@ let clenv_lookup_name clenv id = anomaly "clenv_lookup_name: a name occurs more than once in clause" let clenv_match_args s clause = - let mvs = clenv_independent clause - (clenv_template clause, - clenv_template_type clause) - in + let mvs = clenv_independent clause in let rec matchrec clause = function | [] -> clause | (b,c)::t -> @@ -1038,14 +1030,14 @@ let clenv_match_args s clause = str " occurs more than once in binding"); (try List.nth mvs (n-1) - with Failure "nth" -> errorlabstrm "clenv_match_args" - (str "No such binder")) + with (Failure _|Invalid_argument _) -> + errorlabstrm "clenv_match_args" (str "No such binder")) | Com -> anomaly "No free term in clenv_match_args") in let k_typ = w_hnf_constr clause.hook (clenv_instance_type clause k) and c_typ = w_hnf_constr clause.hook (w_type_of clause.hook c) in matchrec - (clenv_assign k c (clenv_unify_gen true CUMUL c_typ k_typ clause)) t + (clenv_assign k c (clenv_unify true CUMUL c_typ k_typ clause)) t in matchrec clause s @@ -1057,8 +1049,7 @@ let clenv_match_args s clause = * metas. *) let clenv_pose_dependent_evars clenv = - let dep_mvs = clenv_dependent clenv (clenv_template clenv, - clenv_template_type clenv) in + let dep_mvs = clenv_dependent clenv in List.fold_left (fun clenv mv -> let evar = Evarutil.new_evar_in_sign (w_env clenv.hook) in @@ -1079,7 +1070,7 @@ let clenv_add_sign (id,sign) clenv = (***************************) let clenv_unique_resolver allow_K clause gl = - clenv_unify_gen allow_K CUMUL + clenv_unify allow_K CUMUL (clenv_instance_template_type clause) (pf_concl gl) clause let res_pf kONT clenv gls = diff --git a/proofs/clenv.mli b/proofs/clenv.mli index 5fd0e0c0e..78482c2db 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -81,16 +81,15 @@ val clenv_instance_type : wc clausenv -> int -> constr val clenv_instance_template : wc clausenv -> constr val clenv_instance_template_type : wc clausenv -> constr val clenv_unify : - Reductionops.conv_pb -> constr -> constr -> wc clausenv -> wc clausenv + bool -> Reductionops.conv_pb -> constr -> constr -> + wc clausenv -> wc clausenv val clenv_fchain : int -> 'a clausenv -> wc clausenv -> wc clausenv val clenv_refine : (wc -> tactic) -> wc clausenv -> tactic val res_pf : (wc -> tactic) -> wc clausenv -> tactic val res_pf_cast : (wc -> tactic) -> wc clausenv -> tactic val elim_res_pf : (wc -> tactic) -> wc clausenv -> tactic -val clenv_independent : - wc clausenv -> constr freelisted * constr freelisted -> int list -val clenv_missing : - 'a clausenv -> constr freelisted * constr freelisted -> int list +val clenv_independent : wc clausenv -> int list +val clenv_missing : 'a clausenv -> int list val clenv_constrain_missing_args : constr list -> wc clausenv -> wc clausenv val clenv_constrain_dep_args : constr list -> wc clausenv -> wc clausenv val clenv_lookup_name : 'a clausenv -> identifier -> int diff --git a/tactics/auto.ml b/tactics/auto.ml index 674b090c3..b9d09f717 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -217,9 +217,7 @@ let make_apply_entry env sigma (eapply,verbose) name (c,cty) = let pat = Pattern.pattern_of_constr c' in let hd = (try head_pattern_bound pat with BoundPattern -> failwith "make_apply_entry") in - let nmiss = - List.length - (clenv_missing ce (clenv_template ce,clenv_template_type ce)) + let nmiss = List.length (clenv_missing ce) in if eapply & (nmiss <> 0) then begin if verbose then diff --git a/tactics/equality.ml b/tactics/equality.ml index ca049a454..b6131936c 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -94,6 +94,47 @@ let dyn_rewriteRL = function | [Constr c; Cbindings binds] -> rewriteRL_bindings (c,binds) | _ -> assert false + +let v_rewriteLR = hide_tactic "RewriteLR" dyn_rewriteLR +let h_rewriteLR_bindings (c,bl) = v_rewriteLR [(Constr c);(Cbindings bl)] +let h_rewriteLR c = h_rewriteLR_bindings (c,[]) + +let v_rewriteRL = hide_tactic "RewriteRL" dyn_rewriteRL +let h_rewriteRL_bindings (c,bl) = v_rewriteRL [(Constr c);(Cbindings bl)] +let h_rewriteRL c = h_rewriteRL_bindings (c,[]) + +(*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 *) + 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 elim = + if lft2rgt then + pf_global gl (id_of_string (hdcncls^suffix)) + else + pf_global gl (id_of_string (hdcncls^suffix^"_r")) + in + general_elim_in id (c,l) (elim,[]) gl + + +let dyn_rewrite_in lft2rgt = function + | [Identifier id;(Command com);(Bindings binds)] -> + tactic_com_bind_list (general_rewrite_in lft2rgt id) (com,binds) + | [Identifier id;(Constr c);(Cbindings binds)] -> + general_rewrite_in lft2rgt id (c,binds) + | _ -> assert false + +let rewriteLR_in_tac = hide_tactic "RewriteLRin" (dyn_rewrite_in true) +let rewriteRL_in_tac = hide_tactic "RewriteRLin" (dyn_rewrite_in false) + (* Replacing tactics *) @@ -133,14 +174,6 @@ let dyn_replace args gl = | [(Constr c1);(Constr c2)] -> replace c1 c2 gl | _ -> assert false - -let v_rewriteLR = hide_tactic "RewriteLR" dyn_rewriteLR -let h_rewriteLR_bindings (c,bl) = v_rewriteLR [(Constr c);(Cbindings bl)] -let h_rewriteLR c = h_rewriteLR_bindings (c,[]) - -let v_rewriteRL = hide_tactic "RewriteRL" dyn_rewriteRL -let h_rewriteRL_bindings (c,bl) = v_rewriteRL [(Constr c);(Cbindings bl)] -let h_rewriteRL c = h_rewriteRL_bindings (c,[]) let v_replace = hide_tactic "Replace" dyn_replace let h_replace c1 c2 = v_replace [(Constr c1);(Constr c2)] @@ -373,12 +406,6 @@ let discriminable env sigma t1 t2 = the continuation then constructs the case-split. *) -let push_rel_type sigma (na,c,t) env = - push_rel (na,c,t) env - -let push_rels vars env = - List.fold_right (fun nvar env -> push_rel_type Evd.empty nvar env) vars env - let descend_then sigma env head dirn = let IndType (indf,_) as indt = try find_rectype env sigma (get_type_of env sigma head) @@ -387,7 +414,7 @@ let descend_then sigma env head dirn = let (mib,mip) = lookup_mind_specif env ind in let cstr = get_constructors env indf in let dirn_nlams = cstr.(dirn-1).cs_nargs in - let dirn_env = push_rels cstr.(dirn-1).cs_args env in + let dirn_env = push_rel_context cstr.(dirn-1).cs_args env in (dirn_nlams, dirn_env, (fun dirnval (dfltval,resty) -> @@ -1185,45 +1212,7 @@ let sub_term_with_unif cref ceq = None else Some ((plain_instance l ceq),nb) - -(*The Rewrite in tactic*) -let general_rewrite_in lft2rgt id (c,lb) gls = - let typ_id = pf_get_hyp_typ gls id in - let (wc,_) = startWalk gls - and (_,t) = pf_reduce_to_quantified_ind gls (pf_type_of gls c) in - let ctype = type_clenv_binding wc (c,t) lb in - match (match_with_equation ctype) with - | None -> error "The term provided does not end with an equation" - | Some (hdcncl,l) -> - let mbr_eq = - if lft2rgt then - List.hd (List.tl (List.rev l)) - else - List.hd (List.rev l) - in - (match sub_term_with_unif typ_id mbr_eq with - | None -> - errorlabstrm "general_rewrite_in" - (str "Nothing to rewrite in: " ++ pr_id id) - | Some (l2,nb_occ) -> - (tclTHENSI - (tclTHEN - (tclTHEN (generalize [(pf_global gls id)]) - (reduce (Pattern [(list_int nb_occ 1 [],l2, - pf_type_of gls l2)]) [])) - (general_rewrite_bindings lft2rgt (c,lb))) - [(tclTHEN (clear [id]) (introduction id))]) gls) - -let dyn_rewrite_in lft2rgt = function - | [Identifier id;(Command com);(Bindings binds)] -> - tactic_com_bind_list (general_rewrite_in lft2rgt id) (com,binds) - | [Identifier id;(Constr c);(Cbindings binds)] -> - general_rewrite_in lft2rgt id (c,binds) - | _ -> assert false - -let rewriteLR_in_tac = hide_tactic "RewriteLRin" (dyn_rewrite_in true) -let rewriteRL_in_tac = hide_tactic "RewriteRLin" (dyn_rewrite_in false) - + let conditional_rewrite_in lft2rgt id tac (c,bl) = tclTHEN_i (general_rewrite_in lft2rgt id (c,bl)) (fun i -> if i=1 then tclIDTAC else tclCOMPLETE tac) @@ -1243,26 +1232,6 @@ let v_conditional_rewriteLR_in = let v_conditional_rewriteRL_in = hide_tactic "CondRewriteRLin" (dyn_conditional_rewrite_in false) -(* Rewrite c in id. Rewrite -> c in id. Rewrite <- c in id. - Does not work when c is a conditional equation *) - -let rewrite_in lR com id gls = - (try - let _ = lookup_named id (pf_env gls) in () - with Not_found -> - errorlabstrm "rewrite_in" (str"No such hypothesis : " ++pr_id id)); - let c = pf_interp_constr gls com in - let eqn = pf_type_of gls c in - try - let _ = find_eq_data_decompose eqn in - (try - (tclTHENS - ((if lR then substInHyp else revSubstInHyp) eqn id) - ([tclIDTAC ; exact_no_check c])) gls - with UserError("SubstInHyp",_) -> tclIDTAC gls) - with UserError ("find_eq_data_decompose",_)-> - errorlabstrm "rewrite_in" (str"No equality here") - let subst eqn cls gls = match cls with | None -> substInConcl eqn gls diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml index 5c6391dc5..5ff8be0f4 100644 --- a/tactics/setoid_replace.ml +++ b/tactics/setoid_replace.ml @@ -162,6 +162,7 @@ let find_theory a = (* Add a Setoid to the database after a type verification. *) +(* Proof of (a,b,c,d:A)(eq a b)->(eq c d)->(eq a c)->(eq b d) *) let eq_lem_proof env a eq sym trans = lambda_create env (a, lambda_create env @@ -178,6 +179,7 @@ let eq_lem_proof env a eq sym trans = [|(mkRel 7);(mkRel 5);(mkRel 4);(mkRel 1);(mkRel 2)|]))|] ))))))))) +(* Proof of (a,b,c,d:A)(eq a b)->(eq c d)->((eq a c)<->(eq b d)) *) let eq_lem2_proof env a eq sym trans = lambda_create env (a, lambda_create env diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 69141302c..238dd4b95 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -289,6 +289,15 @@ let elimination_sort_of_goal gl = | Type _ -> InType) | _ -> anomaly "goal should be a type" +let elimination_sort_of_hyp id gl = + match kind_of_term (hnf_type_of gl (pf_get_hyp_typ gl id)) with + | Sort s -> + (match s with + | Prop Null -> InProp + | Prop Pos -> InSet + | Type _ -> InType) + | _ -> anomaly "goal should be a type" + (* Find the right elimination suffix corresponding to the sort of the goal *) (* c should be of type A1->.. An->B with B an inductive definition *) diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index af0ea2a66..7693e7f77 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -121,7 +121,7 @@ type branch_assumptions = { indargs : identifier list} (* the inductive arguments *) val elimination_sort_of_goal : goal sigma -> sorts_family -(*i val suff : goal sigma -> constr -> string i*) +val elimination_sort_of_hyp : identifier -> goal sigma -> sorts_family val general_elim_then_using : constr -> (inductive -> bool list array) -> diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 2fb555d88..a30025848 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1077,7 +1077,7 @@ let last_arg c = match kind_of_term c with | App (f,cl) -> array_last cl | _ -> anomaly "last_arg" -let elimination_clause_scheme kONT wc elimclause indclause gl = +let elimination_clause_scheme kONT elimclause indclause gl = let indmv = (match kind_of_term (last_arg (clenv_template elimclause).rebus) with | Meta mv -> mv @@ -1108,7 +1108,7 @@ let general_elim (c,lbindc) (elimc,lbindelimc) gl = let indclause = make_clenv_binding wc (c,t) lbindc in let elimt = w_type_of wc elimc in let elimclause = make_clenv_binding wc (elimc,elimt) lbindelimc in - elimination_clause_scheme kONT wc elimclause indclause gl + elimination_clause_scheme kONT elimclause indclause gl (* Elimination tactic with bindings but using the default elimination * constant associated with the type. *) @@ -1125,6 +1125,43 @@ let default_elim (c,lbindc) gl = let simplest_elim c = default_elim (c,[]) +(* Elimination in hypothesis *) + +let elimination_in_clause_scheme kONT id elimclause indclause = + let (hypmv,indmv) = + match clenv_independent elimclause with + [k1;k2] -> (k1,k2) + | _ -> errorlabstrm "elimination_clause" + (str "The type of elimination clause is not well-formed") in + let elimclause' = clenv_fchain indmv elimclause indclause in + let hyp = mkVar id in + let hyp_typ = clenv_type_of elimclause' hyp in + let hypclause = + mk_clenv_from_n elimclause'.hook 0 (hyp, hyp_typ) in + let elimclause'' = clenv_fchain hypmv elimclause' hypclause in + let new_hyp_prf = clenv_instance_template elimclause'' in + let new_hyp_typ = clenv_instance_template_type elimclause'' in + if eq_constr hyp_typ new_hyp_typ then + errorlabstrm "general_rewrite_in" + (str "Nothing to rewrite in " ++ pr_id id); + tclTHEN + (kONT elimclause''.hook) + (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 new_hyp_prf]) + +let general_elim_in id (c,lbindc) (elimc,lbindelimc) gl = + let (wc,kONT) = startWalk gl in + 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 wc (c,t) lbindc in + let elimt = w_type_of wc elimc in + let elimclause = make_clenv_binding wc (elimc,elimt) lbindelimc in + elimination_in_clause_scheme kONT id elimclause indclause gl + (* * A "natural" induction tactic * @@ -1440,7 +1477,7 @@ let induction_tac varname typ (elimc,elimt) gl = let (wc,kONT) = startWalk gl in let indclause = make_clenv_binding wc (c,typ) [] in let elimclause = make_clenv_binding wc (mkCast (elimc,elimt),elimt) [] in - elimination_clause_scheme kONT wc elimclause indclause gl + elimination_clause_scheme kONT elimclause indclause gl let is_indhyp p n t = let c,_ = decompose_app t in @@ -1648,7 +1685,7 @@ let elim_scheme_type elim t gl = | Meta mv -> let clause' = (* t is inductive, then CUMUL or CONV is irrelevant *) - clenv_unify CUMUL t (clenv_instance_type clause mv) clause in + clenv_unify true CUMUL t (clenv_instance_type clause mv) clause in elim_res_pf kONT clause' gl | _ -> anomaly "elim_scheme_type" diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 28a17ea51..19cd032b0 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -188,6 +188,9 @@ val default_elim : constr * constr substitution -> tactic val simplest_elim : constr -> tactic val dyn_elim : tactic_arg list -> tactic +val general_elim_in : identifier -> constr * constr substitution -> + constr * constr substitution -> tactic + val old_induct : identifier -> tactic val old_induct_nodep : int -> tactic val dyn_old_induct : tactic_arg list -> tactic diff --git a/tactics/wcclausenv.ml b/tactics/wcclausenv.ml index a233aef2d..007a3aa99 100644 --- a/tactics/wcclausenv.ml +++ b/tactics/wcclausenv.ml @@ -51,9 +51,7 @@ let clenv_constrain_with_bindings bl clause = clause else let all_mvs = collect_metas (clenv_template clause).rebus - and ind_mvs = clenv_independent clause - (clenv_template clause, - clenv_template_type clause) in + and ind_mvs = clenv_independent clause in let nb_indep = List.length ind_mvs in let rec matchrec clause = function | [] -> clause @@ -95,7 +93,8 @@ let clenv_constrain_with_bindings bl clause = let sigma = Evd.empty in let k_typ = nf_betaiota (clenv_instance_type clause k) in let c_typ = nf_betaiota (w_type_of clause.hook c) in - matchrec (clenv_assign k c (clenv_unify CUMUL c_typ k_typ clause)) t + matchrec + (clenv_assign k c (clenv_unify true CUMUL c_typ k_typ clause)) t in matchrec clause bl diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v index f8b50e6c2..1942ca6b3 100755 --- a/theories/Bool/Bool.v +++ b/theories/Bool/Bool.v @@ -449,7 +449,7 @@ Qed. Lemma xorb_move_l_r_2 : (b,b',b'':bool) (xorb b b')=b'' -> b=(xorb b'' b'). Proof. - Intros. Rewrite (xorb_comm b b') in H. Rewrite (xorb_move_l_r_1 b' b b'' H). Apply xorb_comm. + Intros. Rewrite xorb_comm in H. Rewrite (xorb_move_l_r_1 b' b b'' H). Apply xorb_comm. Qed. Lemma xorb_move_r_l_1 : (b,b',b'':bool) b=(xorb b' b'') -> (xorb b' b)=b''. |