diff options
| -rw-r--r-- | tactics/class_tactics.ml4 | 34 | ||||
| -rw-r--r-- | tactics/extratactics.ml4 | 7 | ||||
| -rw-r--r-- | tactics/tactics.ml | 207 | ||||
| -rw-r--r-- | tactics/tactics.mli | 4 | ||||
| -rw-r--r-- | theories/Program/Equality.v | 2 | ||||
| -rw-r--r-- | theories/Structures/OrderedType2Facts.v | 7 |
6 files changed, 149 insertions, 112 deletions
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index 40eaec65c6..4a2964a6fc 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -275,6 +275,15 @@ let intro_tac : atac = (g', { info with hints = ldb; auto_last_tac = str"intro" })) gls in {it = gls'; sigma = s}) +let normevars_tac : atac = + lift_tactic tclNORMEVAR + (fun {it = gls; sigma = s} info -> + let gls' = + List.map (fun g' -> + (g', { info with auto_last_tac = str"NORMEVAR" })) gls + in {it = gls'; sigma = s}) + + let id_tac : atac = { skft = fun sk fk {it = gl; sigma = s} -> sk ({it = [gl]; sigma = s}, fun _ pfs -> List.hd pfs) fk } @@ -299,14 +308,13 @@ let hints_tac hints = let possible_resolve ((lgls,v) as res, pri, b, pp) = (pri, pp, b, res) in - let ({it = normalized; sigma = s}, valid) = tclNORMEVAR {it = gl; sigma = s} in - let gl = List.hd normalized in let tacs = - let concl = Evarutil.nf_evar s gl.evar_concl in + let concl = gl.evar_concl in let poss = e_possible_resolve hints info.hints concl in let l = + let tacgl = {it = gl; sigma = s} in Util.list_map_append (fun (tac, pri, b, pptac) -> - try [(tclTHEN tclNORMEVAR tac) {it = gl; sigma = s}, pri, b, pptac] with e when catchable e -> []) + try [tac tacgl, pri, b, pptac] with e when catchable e -> []) poss in if l = [] && !typeclasses_debug then @@ -333,8 +341,7 @@ let hints_tac hints = ~st:(Hint_db.transparent_state info.hints) {it = g; sigma = s} else info.hints } in g, info) 1 gls in - let glsvalid _ pfs = valid [v pfs] in - let glsv = {it = gls'; sigma = s}, glsvalid in + let glsv = {it = gls'; sigma = s}, (fun _ -> v) in sk glsv fk | [] -> fk () in aux 1 tacs } @@ -403,7 +410,8 @@ let run_on_evars ?(only_classes=true) ?(st=full_transparent_state) p evm tac = | None -> raise Not_found | Some (evm', fk) -> Some (Evd.evars_reset_evd evm' evm, fk) -let eauto_tac hints = fix (or_tac intro_tac (hints_tac hints)) +let eauto_tac hints = + fix (or_tac intro_tac (then_tac normevars_tac (hints_tac hints))) let eauto ?(only_classes=true) ?st hints g = let gl = { it = make_autogoal ~only_classes ?st g; sigma = project g } in @@ -616,16 +624,16 @@ VERNAC COMMAND EXTEND Typeclasses_Settings ] END -let typeclasses_eauto ?(st=full_transparent_state) dbs gl = +let typeclasses_eauto ?(only_classes=false) ?(st=full_transparent_state) dbs gl = try let dbs = list_map_filter (fun db -> try Some (Auto.searchtable_map db) with _ -> None) dbs in - let st = match dbs with [x] -> Hint_db.transparent_state x | _ -> st in - eauto ~only_classes:false ~st dbs gl - with Not_found -> tclFAIL 0 (str" typeclasses eauto failed") gl - + let st = match dbs with x :: _ -> Hint_db.transparent_state x | _ -> st in + eauto ~only_classes ~st dbs gl + with Not_found -> tclFAIL 0 (str" typeclasses eauto failed") gl + TACTIC EXTEND typeclasses_eauto | [ "typeclasses" "eauto" "with" ne_preident_list(l) ] -> [ typeclasses_eauto l ] -| [ "typeclasses" "eauto" ] -> [ typeclasses_eauto [typeclasses_db] ] +| [ "typeclasses" "eauto" ] -> [ typeclasses_eauto ~only_classes:true [typeclasses_db] ] END let _ = Classes.refine_ref := Refine.refine diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index de54453100..b951734e36 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -499,7 +499,12 @@ TACTIC EXTEND specialize_hyp END TACTIC EXTEND dependent_pattern -| ["dependent_pattern" constr(c) ] -> [ dependent_pattern c ] +| ["dependent" "pattern" constr(c) ] -> [ dependent_pattern c ] +END + +TACTIC EXTEND dependent_pattern_from +| ["dependent" "pattern" "from" constr(c) ] -> + [ dependent_pattern ~pattern_term:false c ] END TACTIC EXTEND resolve_classes diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 70e8557db9..d54e568e07 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1468,7 +1468,7 @@ let generalize_goal gl i ((occs,c,b),na) cl = let na = generalized_name c t (pf_ids_of_hyps gl) cl' na in mkProd_or_LetIn (na,b,t) cl' -let generalize_dep c gl = +let generalize_dep ?(with_let=false) c gl = let env = pf_env gl in let sign = pf_hyps gl in let init_ids = ids_of_named_context (Global.named_context()) in @@ -1489,10 +1489,17 @@ let generalize_dep c gl = | _ -> tothin in let cl' = it_mkNamedProd_or_LetIn (pf_concl gl) to_quantify in - let cl'' = generalize_goal gl 0 ((all_occurrences,c,None),Anonymous) cl' in + let body = + if with_let then + match kind_of_term c with + | Var id -> pi2 (pf_get_hyp gl id) + | _ -> None + else None + in + let cl'' = generalize_goal gl 0 ((all_occurrences,c,body),Anonymous) cl' in let args = Array.to_list (instance_from_named_context to_quantify_rev) in tclTHEN - (apply_type cl'' (c::args)) + (apply_type cl'' (if body = None then c::args else args)) (thin (List.rev tothin')) gl @@ -2225,10 +2232,10 @@ let mk_term_eq env sigma ty t ty' t' = else mkHEq ty t ty' t', mkHRefl ty' t' -let make_abstract_generalize gl id concl dep ctx c eqs args refls = +let make_abstract_generalize gl id concl dep ctx body c eqs args refls = let meta = Evarutil.new_meta() in - let term, typ = mkVar id, pf_get_hyp_typ gl id (* de Bruijn closed! *) in let eqslen = List.length eqs in + let term, typ = mkVar id, pf_get_hyp_typ gl id in (* Abstract by the "generalized" hypothesis equality proof if necessary. *) let abshypeq, abshypt = if dep then @@ -2240,7 +2247,7 @@ let make_abstract_generalize gl id concl dep ctx c eqs args refls = let eqs = lift_togethern 1 eqs in (* lift together and past genarg *) let abseqs = it_mkProd_or_LetIn ~init:(lift eqslen abshypeq) (List.map (fun x -> (Anonymous, None, x)) eqs) in (* Abstract by the "generalized" hypothesis. *) - let genarg = mkProd (Name id, c, abseqs) in + let genarg = mkProd_or_LetIn (Name id, body, c) abseqs in (* Abstract by the extension of the context *) let genctyp = it_mkProd_or_LetIn ~init:genarg ctx in (* The goal will become this product. *) @@ -2248,7 +2255,7 @@ let make_abstract_generalize gl id concl dep ctx c eqs args refls = (* Apply the old arguments giving the proper instantiation of the hyp *) let instc = mkApp (genc, Array.of_list args) in (* Then apply to the original instanciated hyp. *) - let instc = mkApp (instc, [| mkVar id |]) in + let instc = Option.cata (fun _ -> instc) (mkApp (instc, [| mkVar id |])) body in (* Apply the reflexivity proofs on the indices. *) let appeqs = mkApp (instc, Array.of_list refls) in (* Finaly, apply the reflexivity proof for the original hyp, to get a term of type gl again. *) @@ -2299,8 +2306,7 @@ let linear vars args = true with Seen -> false -let abstract_args gl generalize_vars dep id = - let c = pf_get_hyp_typ gl id in +let abstract_args gl generalize_vars dep id defined f args = let sigma = project gl in let env = pf_env gl in let concl = pf_concl gl in @@ -2310,90 +2316,101 @@ let abstract_args gl generalize_vars dep id = let id = fresh_id !avoid (match name with Name n -> n | Anonymous -> id_of_string "gen_x") gl in avoid := id :: !avoid; id in - match kind_of_term c with - | App (f, args) -> - (* Build application generalized w.r.t. the argument plus the necessary eqs. - From env |- c : forall G, T and args : G we build - (T[G'], G' : ctx, env ; G' |- args' : G, eqs := G'_i = G_i, refls : G' = G, vars to generalize) - - eqs are not lifted w.r.t. each other yet. (* will be needed when going to dependent indexes *) - *) - let aux (prod, ctx, ctxenv, c, args, eqs, refls, vars, env) arg = - let (name, _, ty), arity = - let rel, c = Reductionops.splay_prod_n env sigma 1 prod in - List.hd rel, c + (* Build application generalized w.r.t. the argument plus the necessary eqs. + From env |- c : forall G, T and args : G we build + (T[G'], G' : ctx, env ; G' |- args' : G, eqs := G'_i = G_i, refls : G' = G, vars to generalize) + + eqs are not lifted w.r.t. each other yet. (* will be needed when going to dependent indexes *) + *) + let aux (prod, ctx, ctxenv, c, args, eqs, refls, vars, env) arg = + let (name, _, ty), arity = + let rel, c = Reductionops.splay_prod_n env sigma 1 prod in + List.hd rel, c + in + let argty = pf_type_of gl arg in + let argty = if isSort argty then new_Type () else argty in + let liftargty = lift (List.length ctx) argty in + let convertible = Reductionops.is_conv_leq ctxenv sigma liftargty ty in + match kind_of_term arg with + (* | Var id -> *) + (* let deps = deps_of_var id env in *) + (* (subst1 arg arity, ctx, ctxenv, mkApp (c, [|arg|]), args, eqs, refls, Idset.union deps vars, env) *) + | _ -> + let name = get_id name in + let decl = (Name name, None, ty) in + let ctx = decl :: ctx in + let c' = mkApp (lift 1 c, [|mkRel 1|]) in + let args = arg :: args in + let liftarg = lift (List.length ctx) arg in + let eq, refl = + if convertible then + mkEq (lift 1 ty) (mkRel 1) liftarg, mkRefl argty arg + else + mkHEq (lift 1 ty) (mkRel 1) liftargty liftarg, mkHRefl argty arg in - let argty = pf_type_of gl arg in - let argty = if isSort argty then new_Type () else argty in - let liftargty = lift (List.length ctx) argty in - let convertible = Reductionops.is_conv_leq ctxenv sigma liftargty ty in - match kind_of_term arg with -(* | Var id -> *) -(* let deps = deps_of_var id env in *) -(* (subst1 arg arity, ctx, ctxenv, mkApp (c, [|arg|]), args, eqs, refls, Idset.union deps vars, env) *) - | _ -> - let name = get_id name in - let decl = (Name name, None, ty) in - let ctx = decl :: ctx in - let c' = mkApp (lift 1 c, [|mkRel 1|]) in - let args = arg :: args in - let liftarg = lift (List.length ctx) arg in - let eq, refl = - if convertible then - mkEq (lift 1 ty) (mkRel 1) liftarg, mkRefl argty arg - else - mkHEq (lift 1 ty) (mkRel 1) liftargty liftarg, mkHRefl argty arg - in - let eqs = eq :: lift_list eqs in - let refls = refl :: refls in - let argvars = ids_of_constr vars arg in - (arity, ctx, push_rel decl ctxenv, c', args, eqs, refls, Idset.union argvars vars, env) - in - let f', args' = decompose_indapp f args in - let dogen, f', args' = - let parvars = ids_of_constr ~all:true Idset.empty f' in - if not (linear parvars args') then true, f, args - else - match array_find_i (fun i x -> not (isVar x)) args' with - | None -> false, f', args' - | Some nonvar -> - let before, after = array_chop nonvar args' in - true, mkApp (f', before), after - in - if dogen then - let arity, ctx, ctxenv, c', args, eqs, refls, vars, env = - Array.fold_left aux (pf_type_of gl f',[],env,f',[],[],[],Idset.empty,env) args' - in - let args, refls = List.rev args, List.rev refls in - let vars = - if generalize_vars then - let nogen = Idset.add id Idset.empty in - hyps_of_vars (pf_env gl) (pf_hyps gl) nogen vars - else [] - in - Some (make_abstract_generalize gl id concl dep ctx c' eqs args refls, - dep, succ (List.length ctx), vars) - else None - | _ -> None - + let eqs = eq :: lift_list eqs in + let refls = refl :: refls in + let argvars = ids_of_constr vars arg in + (arity, ctx, push_rel decl ctxenv, c', args, eqs, refls, Idset.union argvars vars, env) + in + let f', args' = decompose_indapp f args in + let dogen, f', args' = + let parvars = ids_of_constr ~all:true Idset.empty f' in + if not (linear parvars args') then true, f, args + else + match array_find_i (fun i x -> not (isVar x)) args' with + | None -> false, f', args' + | Some nonvar -> + let before, after = array_chop nonvar args' in + true, mkApp (f', before), after + in + if dogen then + let arity, ctx, ctxenv, c', args, eqs, refls, vars, env = + Array.fold_left aux (pf_type_of gl f',[],env,f',[],[],[],Idset.empty,env) args' + in + let args, refls = List.rev args, List.rev refls in + let vars = + if generalize_vars then + let nogen = Idset.singleton id in + hyps_of_vars (pf_env gl) (pf_hyps gl) nogen vars + else [] + in + let body, c' = if defined then Some c', Retyping.get_type_of ctxenv Evd.empty c' else None, c' in + Some (make_abstract_generalize gl id concl dep ctx body c' eqs args refls, + dep, succ (List.length ctx), vars) + else None + let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id gl = Coqlib.check_required_library ["Coq";"Logic";"JMeq"]; - let oldid = pf_get_new_id id gl in - let newc = abstract_args gl generalize_vars force_dep id in - match newc with - | None -> tclIDTAC gl - | Some (newc, dep, n, vars) -> - let tac = - if dep then - tclTHENLIST [refine newc; rename_hyp [(id, oldid)]; tclDO n intro; - generalize_dep (mkVar oldid)] - else - tclTHENLIST [refine newc; clear [id]; tclDO n intro] - in - if vars = [] then tac gl - else tclTHEN tac - (fun gl -> tclFIRST [revert vars ; - tclMAP (fun id -> tclTRY (generalize_dep (mkVar id))) vars] gl) gl + let f, args, def, id, oldid = + let oldid = pf_get_new_id id gl in + let (_, b, t) = pf_get_hyp gl id in + match b with + | None -> let f, args = decompose_app t in + f, args, false, id, oldid + | Some t -> + let f, args = decompose_app t in + f, args, true, id, oldid + in + if args = [] then tclIDTAC gl + else + let args = Array.of_list args in + let newc = abstract_args gl generalize_vars force_dep id def f args in + match newc with + | None -> tclIDTAC gl + | Some (newc, dep, n, vars) -> + let tac = + if dep then + tclTHENLIST [refine newc; rename_hyp [(id, oldid)]; tclDO n intro; + generalize_dep ~with_let:true (mkVar oldid)] + else + tclTHENLIST [refine newc; clear [id]; tclDO n intro] + in + if vars = [] then tac gl + else tclTHEN tac + (fun gl -> tclFIRST [revert vars ; + tclMAP (fun id -> + tclTRY (generalize_dep ~with_let:true (mkVar id))) vars] gl) gl let specialize_hypothesis id gl = let env = pf_env gl in @@ -2444,11 +2461,11 @@ let specialize_hypothesis id gl = let specialize_hypothesis id gl = - if occur_var (pf_env gl) id (pf_concl gl) then + if try ignore(clear [id] gl); false with _ -> true then tclFAIL 0 (str "Specialization not allowed on dependent hypotheses") gl else specialize_hypothesis id gl -let dependent_pattern c gl = +let dependent_pattern ?(pattern_term=true) c gl = let cty = pf_type_of gl c in let deps = match kind_of_term cty with @@ -2465,7 +2482,11 @@ let dependent_pattern c gl = let conclvar = subst_term_occ all_occurrences c ty in mkNamedLambda id cty conclvar in - let subst = (c, varname c, cty) :: List.rev_map (fun c -> (c, varname c, pf_type_of gl c)) deps in + let subst = + let deps = List.rev_map (fun c -> (c, varname c, pf_type_of gl c)) deps in + if pattern_term then (c, varname c, cty) :: deps + else deps + in let concllda = List.fold_left mklambda (pf_concl gl) subst in let conclapp = applistc concllda (List.rev_map pi1 subst) in convert_concl_no_check conclapp DEFAULTcast gl diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 19c0ba3332..2202fa8c88 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -373,7 +373,7 @@ val pose_proof : name -> constr -> tactic val generalize : constr list -> tactic val generalize_gen : ((occurrences * constr) * name) list -> tactic -val generalize_dep : constr -> tactic +val generalize_dep : ?with_let:bool (* Don't lose let bindings *) -> constr -> tactic val unify : ?state:Names.transparent_state -> constr -> constr -> tactic val resolve_classes : tactic @@ -385,7 +385,7 @@ val admit_as_an_axiom : tactic val abstract_generalize : ?generalize_vars:bool -> ?force_dep:bool -> identifier -> tactic val specialize_hypothesis : identifier -> tactic -val dependent_pattern : constr -> tactic +val dependent_pattern : ?pattern_term:bool -> constr -> tactic val register_general_multi_rewrite : (bool -> evars_flag -> open_constr with_bindings -> clause -> tactic) -> unit diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v index 76dc09b26e..c9ec29d2b0 100644 --- a/theories/Program/Equality.v +++ b/theories/Program/Equality.v @@ -22,7 +22,7 @@ Ltac is_ground_goal := (** Try to find a contradiction. *) -Hint Extern 10 => is_ground_goal ; progress (elimtype False). +Hint Extern 10 => is_ground_goal ; progress exfalso : exfalso. (** We will use the [block] definition to separate the goal from the equalities generated by the tactic. *) diff --git a/theories/Structures/OrderedType2Facts.v b/theories/Structures/OrderedType2Facts.v index a7bb661ea7..e35c7c651c 100644 --- a/theories/Structures/OrderedType2Facts.v +++ b/theories/Structures/OrderedType2Facts.v @@ -23,7 +23,10 @@ Module OTF_to_OrderSig (O : OrderedTypeFull) : OrderSig with Definition t := O.t with Definition eq := O.eq with Definition lt := O.lt - with Definition le := O.le. + with Definition le := O.le + with Definition eq_equiv := O.eq_equiv + with Definition lt_strorder := O.lt_strorder + with Definition lt_compat := O.lt_compat. Include O. Lemma lt_total : forall x y, O.lt x y \/ O.eq x y \/ O.lt y x. Proof. intros; destruct (O.compare_spec x y); auto. Qed. @@ -156,7 +159,7 @@ Module OrderedTypeFacts (Import O: OrderedType). Lemma compare_antisym : forall x y, (y ?= x) = CompOpp (x ?= y). Proof. - intros; elim_compare x y; autorewrite with order; order. + intros; elim_compare x y; simpl; autorewrite with order; order. Qed. (** For compatibility reasons *) |