diff options
59 files changed, 497 insertions, 355 deletions
diff --git a/doc/changelog/02-specification-language/07825-rechable-from-evars.rst b/doc/changelog/02-specification-language/07825-rechable-from-evars.rst new file mode 100644 index 0000000000..e57d5a7bc5 --- /dev/null +++ b/doc/changelog/02-specification-language/07825-rechable-from-evars.rst @@ -0,0 +1,9 @@ +- **Changed:** + In :tacn:`refine`, new existential variables unified with existing ones are no + longer considered as fresh. The behavior of :tacn:`simple refine` no longer depends on + the orientation of evar-evar unification problems, and new existential variables + are always turned into (unshelved) goals. This can break compatibility in + some cases (`#7825 <https://github.com/coq/coq/pull/7825>`_, by Matthieu + Sozeau, with help from Maxime Dénès, review by Pierre-Marie Pédrot and + Enrico Tassi, fixes `#4095 <https://github.com/coq/coq/issues/4095>`_ and + `#4413 <https://github.com/coq/coq/issues/4413>`_). diff --git a/doc/changelog/04-tactics/12993-remove-cutrewrite.rst b/doc/changelog/04-tactics/12993-remove-cutrewrite.rst new file mode 100644 index 0000000000..b719c5618e --- /dev/null +++ b/doc/changelog/04-tactics/12993-remove-cutrewrite.rst @@ -0,0 +1,4 @@ +- **Removed:** + Deprecated ``cutrewrite`` tactic. Use :tacn:`replace` instead + (`#12993 <https://github.com/coq/coq/pull/12993>`_, + by Théo Zimmermann). diff --git a/doc/sphinx/language/extensions/match.rst b/doc/sphinx/language/extensions/match.rst index 34752a4c4d..182f599a29 100644 --- a/doc/sphinx/language/extensions/match.rst +++ b/doc/sphinx/language/extensions/match.rst @@ -880,10 +880,10 @@ Here is a summary of the error messages corresponding to each situation: .. exn:: The constructor @ident expects @num arguments. + The variable ident is bound several times in pattern term + Found a constructor of inductive type term while a constructor of term is expected - The variable ident is bound several times in pattern termFound a constructor - of inductive type term while a constructor of term is expectedPatterns are - incorrect (because constructors are not applied to the correct number of the + Patterns are incorrect (because constructors are not applied to the correct number of arguments, because they are not linear or they are wrongly typed). .. exn:: Non exhaustive pattern matching. diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index e7ba82fb31..d8b2af092f 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -375,8 +375,14 @@ behavior.) | ! | par - Applies :token:`ltac_expr` to the selected goals. It can only be used at the top - level of a tactic expression; it cannot be used within a tactic expression. + Reorders the goals and applies :token:`ltac_expr` to the selected goals. It can + only be used at the top level of a tactic expression; it cannot be used within a + tactic expression. The selected goals are reordered so they appear after the + lowest-numbered selected goal, ordered by goal number. :ref:`Example + <reordering_goals_ex>`. If the selector applies + to a single goal or to all goals, the reordering will not be apparent. The order of + the goals in the :token:`selector` is irrelevant. (This may not be what you expect; + see `#8481 <https://github.com/coq/coq/issues/8481>`_.) .. todo why shouldn't "all" and "!" be accepted anywhere a @selector is accepted? It would be simpler to explain. @@ -430,6 +436,19 @@ Selectors can also be used nested within a tactic expression with the :name: No such goal. (Goal selector) :undocumented: +.. _reordering_goals_ex: + +.. example:: Selector reordering goals + + .. coqtop:: reset in + + Goal 1=0 /\ 2=0 /\ 3=0. + + .. coqtop:: all + + repeat split. + 1,3: idtac. + .. TODO change error message index entry diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 4480b10319..55e4f26fe8 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -156,6 +156,10 @@ list of assertion commands is given in :ref:`Assertions`. The command ``T``, then the commands ``Proof using a`` and ``Proof using T a`` are equivalent. + The set of declared variables always includes the variables used by + the statement. In other words ``Proof using e`` is equivalent to + ``Proof using Type + e`` for any declaration expression ``e``. + .. cmdv:: Proof using {+ @ident } with @tactic Combines in a single line :cmd:`Proof with` and :cmd:`Proof using`. diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 7f270e8076..5a11b4f474 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -3110,7 +3110,7 @@ An :token:`r_item` can be: + A list of terms ``(t1 ,…,tn)``, each ``ti`` having a type above. The tactic: ``rewrite r_prefix (t1 ,…,tn ).`` is equivalent to: ``do [rewrite r_prefix t1 | … | rewrite r_prefix tn ].`` - + An anonymous rewrite lemma ``(_ : term)``, where term has a type as above. tactic: ``rewrite (_ : term)`` is in fact synonym of: ``cutrewrite (term).``. + + An anonymous rewrite lemma ``(_ : term)``, where term has a type as above. .. example:: diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index f3dc9a6cb1..2211a58e6e 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -54,7 +54,7 @@ Invocation of tactics ~~~~~~~~~~~~~~~~~~~~~ A tactic is applied as an ordinary command. It may be preceded by a -goal selector (see Section :ref:`ltac-semantics`). If no selector is +goal selector (see Section :ref:`goal-selectors`). If no selector is specified, the default selector is used. .. _tactic_invocation_grammar: @@ -2819,13 +2819,6 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. only in the conclusion of the goal. The clause argument must not contain any ``type of`` nor ``value of``. - .. tacv:: cutrewrite {? {| <- | -> } } (@term__1 = @term__2) {? in @ident } - :name: cutrewrite - - .. deprecated:: 8.5 - - Use :tacn:`replace` instead. - .. tacn:: subst @ident :name: subst @@ -4751,9 +4744,13 @@ Non-logical tactics .. tacn:: cycle @num :name: cycle - This tactic puts the :n:`@num` first goals at the end of the list of goals. - If :n:`@num` is negative, it will put the last :math:`|num|` goals at the + Reorders the selected goals so that the first :n:`@num` goals appear after the + other selected goals. + If :n:`@num` is negative, it puts the last :n:`@num` goals at the beginning of the list. + The tactic is only useful with a goal selector, most commonly `all:`. + Note that other selectors reorder goals; `1,3: cycle 1` is not equivalent + to `all: cycle 1`. See :tacn:`… : … (goal selector)`. .. example:: @@ -4771,10 +4768,12 @@ Non-logical tactics .. tacn:: swap @num @num :name: swap - This tactic switches the position of the goals of indices :n:`@num` and - :n:`@num`. Negative values for:n:`@num` indicate counting goals - backward from the end of the focused goal list. Goals are indexed from 1, - there is no goal with position 0. + Exchanges the position of the specified goals. + Negative values for :n:`@num` indicate counting goals + backward from the end of the list of selected goals. Goals are indexed from 1. + The tactic is only useful with a goal selector, most commonly `all:`. + Note that other selectors reorder goals; `1,3: swap 1 3` is not equivalent + to `all: swap 1 3`. See :tacn:`… : … (goal selector)`. .. example:: @@ -4788,7 +4787,9 @@ Non-logical tactics .. tacn:: revgoals :name: revgoals - This tactics reverses the list of the focused goals. + Reverses the order of the selected goals. The tactic is only useful with a goal + selector, most commonly `all :`. Note that other selectors reorder goals; + `1,3: revgoals` is not equivalent to `all: revgoals`. See :tacn:`… : … (goal selector)`. .. example:: diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index 6625e07d05..9971a03894 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -1033,9 +1033,6 @@ simple_tactic: [ | DELETE "unify" constr constr | REPLACE "unify" constr constr "with" preident | WITH "unify" constr constr OPT ( "with" preident ) -| DELETE "cutrewrite" orient constr -| REPLACE "cutrewrite" orient constr "in" hyp -| WITH "cutrewrite" orient constr OPT ( "in" hyp ) | DELETE "destauto" | REPLACE "destauto" "in" hyp | WITH "destauto" OPT ( "in" hyp ) diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index 7f4e92fc37..f628c86cf1 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -1535,8 +1535,6 @@ simple_tactic: [ | "simple" "injection" destruction_arg | "dependent" "rewrite" orient constr | "dependent" "rewrite" orient constr "in" hyp -| "cutrewrite" orient constr -| "cutrewrite" orient constr "in" hyp | "decompose" "sum" constr | "decompose" "record" constr | "absurd" constr diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index 84efc1e36c..3cd5a85654 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -1445,7 +1445,6 @@ simple_tactic: [ | "einjection" OPT destruction_arg OPT ( "as" LIST0 simple_intropattern ) | "simple" "injection" OPT destruction_arg | "dependent" "rewrite" OPT [ "->" | "<-" ] one_term OPT ( "in" ident ) -| "cutrewrite" OPT [ "->" | "<-" ] one_term OPT ( "in" ident ) | "decompose" "sum" one_term | "decompose" "record" one_term | "absurd" one_term diff --git a/engine/evarutil.ml b/engine/evarutil.ml index d719731464..771571fd3f 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -516,12 +516,7 @@ let restrict_evar evd evk filter ?src candidates = let candidates = Option.map (filter_effective_candidates evd evar_info filter) candidates in match candidates with | Some [] -> raise (ClearDependencyError (*FIXME*)(Id.of_string "blah", (NoCandidatesLeft evk), None)) - | _ -> - let evd, evk' = Evd.restrict evk filter ?candidates ?src evd in - (* Mark new evar as future goal, removing previous one, - circumventing Proofview.advance but making Proof.run_tactic catch these. *) - let evd = Evd.remove_future_goal evd evk in - (Evd.declare_future_goal evk' evd, evk') + | _ -> Evd.restrict evk filter ?candidates ?src evd let rec check_and_clear_in_constr env evdref err ids global c = (* returns a new constr where all the evars have been 'cleaned' @@ -703,10 +698,22 @@ let rec advance sigma evk = match evi.evar_body with | Evar_empty -> Some evk | Evar_defined v -> - match is_restricted_evar sigma evk with + match is_aliased_evar sigma evk with | Some evk -> advance sigma evk | None -> None +let reachable_from_evars sigma evars = + let aliased = Evd.get_aliased_evars sigma in + let rec search evk visited = + if Evar.Set.mem evk visited then visited + else + let visited = Evar.Set.add evk visited in + match Evar.Map.find evk aliased with + | evk' -> search evk' visited + | exception Not_found -> visited + in + Evar.Set.fold (fun evk visited -> search evk visited) evars Evar.Set.empty + (** The following functions return the set of undefined evars contained in the object, the defined evars being traversed. This is roughly a combination of the previous functions and diff --git a/engine/evarutil.mli b/engine/evarutil.mli index 9d2c29547e..6e1f67021f 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -112,6 +112,10 @@ val gather_dependent_evars : evar_map -> Evar.t list -> (Evar.Set.t option) Evar solved. *) val advance : evar_map -> Evar.t -> Evar.t option +(** [reachable_from_evars sigma seeds] computes the descendents of + evars in [seeds] by restriction or evar-evar unifications in [sigma]. *) +val reachable_from_evars : evar_map -> Evar.Set.t -> Evar.Set.t + (** The following functions return the set of undefined evars contained in the object, the defined evars being traversed. This is roughly a combination of the previous functions and @@ -234,8 +238,8 @@ exception ClearDependencyError of Id.t * clear_dependency_error * GlobRef.t opti (** Restrict an undefined evar according to a (sub)filter and candidates. The evar will be defined if there is only one candidate left, -@raise ClearDependencyError NoCandidatesLeft if the filter turns the candidates - into an empty list. *) + @raise ClearDependencyError NoCandidatesLeft if the filter turns the candidates + into an empty list. *) val restrict_evar : evar_map -> Evar.t -> Filter.t -> ?src:Evar_kinds.t Loc.located -> constr list option -> evar_map * Evar.t diff --git a/engine/evd.ml b/engine/evd.ml index 65df2643f2..4ae1d034d7 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -453,7 +453,7 @@ end type evar_flags = { obligation_evars : Evar.Set.t; - restricted_evars : Evar.t Evar.Map.t; + aliased_evars : Evar.t Evar.Map.t; typeclass_evars : Evar.Set.t } type side_effect_role = @@ -631,7 +631,7 @@ let add_with_name ?name ?(typeclass_candidate = true) d e i = match i.evar_body associated to an evar, so we prevent registering its typeclass status. *) let add d e i = add_with_name ~typeclass_candidate:false d e i -(*** Evar flags: typeclasses, restricted or obligation flag *) +(*** Evar flags: typeclasses, aliased or obligation flag *) let get_typeclass_evars evd = evd.evar_flags.typeclass_evars @@ -659,29 +659,28 @@ let is_obligation_evar evd evk = let inherit_evar_flags evar_flags evk evk' = let evk_typeclass = Evar.Set.mem evk evar_flags.typeclass_evars in let evk_obligation = Evar.Set.mem evk evar_flags.obligation_evars in - if not (evk_obligation || evk_typeclass) then evar_flags - else - let typeclass_evars = - if evk_typeclass then - let typeclass_evars = Evar.Set.remove evk evar_flags.typeclass_evars in - Evar.Set.add evk' typeclass_evars - else evar_flags.typeclass_evars - in - let obligation_evars = - if evk_obligation then - let obligation_evars = Evar.Set.remove evk evar_flags.obligation_evars in - Evar.Set.add evk' obligation_evars - else evar_flags.obligation_evars - in - { evar_flags with obligation_evars; typeclass_evars } + let aliased_evars = Evar.Map.add evk evk' evar_flags.aliased_evars in + let typeclass_evars = + if evk_typeclass then + let typeclass_evars = Evar.Set.remove evk evar_flags.typeclass_evars in + Evar.Set.add evk' typeclass_evars + else evar_flags.typeclass_evars + in + let obligation_evars = + if evk_obligation then + let obligation_evars = Evar.Set.remove evk evar_flags.obligation_evars in + Evar.Set.add evk' obligation_evars + else evar_flags.obligation_evars + in + { obligation_evars; aliased_evars; typeclass_evars } (** Removal: in all other cases of definition *) let remove_evar_flags evk evar_flags = { typeclass_evars = Evar.Set.remove evk evar_flags.typeclass_evars; obligation_evars = Evar.Set.remove evk evar_flags.obligation_evars; - (* Restriction information is kept. *) - restricted_evars = evar_flags.restricted_evars } + (* Aliasing information is kept. *) + aliased_evars = evar_flags.aliased_evars } (** New evars *) @@ -809,7 +808,7 @@ let create_evar_defs sigma = { sigma with let empty_evar_flags = { obligation_evars = Evar.Set.empty; - restricted_evars = Evar.Map.empty; + aliased_evars = Evar.Map.empty; typeclass_evars = Evar.Set.empty } let empty_side_effects = { @@ -872,71 +871,12 @@ let evar_source evk d = (find d evk).evar_source let evar_ident evk evd = EvNames.ident evk evd.evar_names let evar_key id evd = EvNames.key id evd.evar_names -let define_aux def undef evk body = - let oldinfo = - try EvMap.find evk undef - with Not_found -> - if EvMap.mem evk def then - anomaly ~label:"Evd.define" (Pp.str "cannot define an evar twice.") - else - anomaly ~label:"Evd.define" (Pp.str "cannot define undeclared evar.") - in - let () = assert (oldinfo.evar_body == Evar_empty) in - let newinfo = { oldinfo with evar_body = Evar_defined body } in - EvMap.add evk newinfo def, EvMap.remove evk undef - -(* define the existential of section path sp as the constr body *) -let define_gen evk body evd evar_flags = - let (defn_evars, undf_evars) = define_aux evd.defn_evars evd.undf_evars evk body in - let last_mods = match evd.conv_pbs with - | [] -> evd.last_mods - | _ -> Evar.Set.add evk evd.last_mods - in - let evar_names = EvNames.remove_name_defined evk evd.evar_names in - { evd with defn_evars; undf_evars; last_mods; evar_names; evar_flags } +let get_aliased_evars evd = evd.evar_flags.aliased_evars -(** By default, the obligation and evar tag of the evar is removed *) -let define evk body evd = - let evar_flags = remove_evar_flags evk evd.evar_flags in - define_gen evk body evd evar_flags - -(** In case of an evar-evar solution, the flags are inherited *) -let define_with_evar evk body evd = - let evk' = fst (destEvar body) in - let evar_flags = inherit_evar_flags evd.evar_flags evk evk' in - define_gen evk body evd evar_flags - -let is_restricted_evar evd evk = - try Some (Evar.Map.find evk evd.evar_flags.restricted_evars) +let is_aliased_evar evd evk = + try Some (Evar.Map.find evk evd.evar_flags.aliased_evars) with Not_found -> None -let declare_restricted_evar evar_flags evk evk' = - { evar_flags with restricted_evars = Evar.Map.add evk evk' evar_flags.restricted_evars } - -(* In case of restriction, we declare the restriction and inherit the obligation - and typeclass flags. *) - -let restrict evk filter ?candidates ?src evd = - let evk' = new_untyped_evar () in - let evar_info = EvMap.find evk evd.undf_evars in - let id_inst = Filter.filter_list filter evar_info.evar_hyps.env_named_var in - let evar_info' = - { evar_info with evar_filter = filter; - evar_candidates = candidates; - evar_source = (match src with None -> evar_info.evar_source | Some src -> src); - evar_identity = Identity.make id_inst; - } in - let last_mods = match evd.conv_pbs with - | [] -> evd.last_mods - | _ -> Evar.Set.add evk evd.last_mods in - let evar_names = EvNames.reassign_name_defined evk evk' evd.evar_names in - let body = mkEvar(evk',id_inst) in - let (defn_evars, undf_evars) = define_aux evd.defn_evars evd.undf_evars evk body in - let evar_flags = declare_restricted_evar evd.evar_flags evk evk' in - let evar_flags = inherit_evar_flags evar_flags evk evk' in - { evd with undf_evars = EvMap.add evk' evar_info' undf_evars; - defn_evars; last_mods; evar_names; evar_flags }, evk' - let downcast evk ccl evd = let evar_info = EvMap.find evk evd.undf_evars in let evar_info' = { evar_info with evar_concl = ccl } in @@ -1224,6 +1164,73 @@ let pr_shelf evd = if List.is_empty evd.shelf then str"(empty stack)" else prlist_with_sep (fun () -> str"||") (prlist_with_sep spc Evar.print) evd.shelf +let define_aux def undef evk body = + let oldinfo = + try EvMap.find evk undef + with Not_found -> + if EvMap.mem evk def then + anomaly ~label:"Evd.define" (Pp.str "cannot define an evar twice.") + else + anomaly ~label:"Evd.define" (Pp.str "cannot define undeclared evar.") + in + let () = assert (oldinfo.evar_body == Evar_empty) in + let newinfo = { oldinfo with evar_body = Evar_defined body } in + EvMap.add evk newinfo def, EvMap.remove evk undef + +(* define the existential of section path sp as the constr body *) +let define_gen evk body evd evar_flags = + let (defn_evars, undf_evars) = define_aux evd.defn_evars evd.undf_evars evk body in + let last_mods = match evd.conv_pbs with + | [] -> evd.last_mods + | _ -> Evar.Set.add evk evd.last_mods + in + let evar_names = EvNames.remove_name_defined evk evd.evar_names in + { evd with defn_evars; undf_evars; last_mods; evar_names; evar_flags } + +(** By default, the obligation and evar tag of the evar is removed *) +let define evk body evd = + let evar_flags = remove_evar_flags evk evd.evar_flags in + define_gen evk body evd evar_flags + +(** In case of an evar-evar solution, the flags are inherited *) +let define_with_evar evk body evd = + let evk' = fst (destEvar body) in + let evar_flags = inherit_evar_flags evd.evar_flags evk evk' in + let evd = unshelve evd [evk] in + let future_goals = FutureGoals.remove evk evd.future_goals in + let evd = { evd with future_goals } in + define_gen evk body evd evar_flags + +(* In case of restriction, we declare the aliasing and inherit the obligation + and typeclass flags. *) + +let restrict evk filter ?candidates ?src evd = + let evk' = new_untyped_evar () in + let evar_info = EvMap.find evk evd.undf_evars in + let id_inst = Filter.filter_list filter evar_info.evar_hyps.env_named_var in + let evar_info' = + { evar_info with evar_filter = filter; + evar_candidates = candidates; + evar_source = (match src with None -> evar_info.evar_source | Some src -> src); + evar_identity = Identity.make id_inst; + } in + let last_mods = match evd.conv_pbs with + | [] -> evd.last_mods + | _ -> Evar.Set.add evk evd.last_mods in + let evar_names = EvNames.reassign_name_defined evk evk' evd.evar_names in + let body = mkEvar(evk',id_inst) in + let (defn_evars, undf_evars) = define_aux evd.defn_evars evd.undf_evars evk body in + let evar_flags = inherit_evar_flags evd.evar_flags evk evk' in + let evd = { evd with undf_evars = EvMap.add evk' evar_info' undf_evars; + defn_evars; last_mods; evar_names; evar_flags } + in + (* Mark new evar as future goal, removing previous one, + circumventing Proofview.advance but making Proof.run_tactic catch these. *) + let evd = unshelve evd [evk] in + let evd = remove_future_goal evd evk in + let evd = declare_future_goal evk' evd in + (evd, evk') + (**********************************************************) (* Accessing metas *) diff --git a/engine/evd.mli b/engine/evd.mli index 9394f9a9dd..fafaad9a04 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -284,8 +284,11 @@ val restrict : Evar.t-> Filter.t -> ?candidates:econstr list -> possibly limiting the instances to a set of candidates (candidates are filtered according to the filter) *) -val is_restricted_evar : evar_map -> Evar.t -> Evar.t option -(** Tell if an evar comes from restriction of another evar, and if yes, which *) +val get_aliased_evars : evar_map -> Evar.t Evar.Map.t +(** The map of aliased evars *) + +val is_aliased_evar : evar_map -> Evar.t -> Evar.t option +(** Tell if an evar has been aliased to another evar, and if yes, which *) val set_typeclass_evars : evar_map -> Evar.Set.t -> evar_map (** Mark the given set of evars as available for resolution. @@ -388,7 +391,6 @@ val pop_future_goals : evar_map -> FutureGoals.t * evar_map val fold_future_goals : (evar_map -> Evar.t -> evar_map) -> evar_map -> evar_map - val remove_future_goal : evar_map -> Evar.t -> evar_map val pr_future_goals_stack : evar_map -> Pp.t diff --git a/engine/proofview_monad.ml b/engine/proofview_monad.ml index df9fc5dab3..80263694f5 100644 --- a/engine/proofview_monad.ml +++ b/engine/proofview_monad.ml @@ -202,6 +202,11 @@ module type State = sig val modify : (t->t) -> unit Logical.t end +module type Reader = sig + type t + val get : t Logical.t +end + module type Writer = sig type t val put : t -> unit Logical.t diff --git a/engine/proofview_monad.mli b/engine/proofview_monad.mli index 6cca3f5a5e..00d322858d 100644 --- a/engine/proofview_monad.mli +++ b/engine/proofview_monad.mli @@ -79,7 +79,7 @@ val with_empty_state : goal -> goal_with_state val map_goal_with_state : (goal -> goal) -> goal_with_state -> goal_with_state (** Type of proof views: current [evar_map] together with the list of - focused goals. *) + focused goals, locally shelved goals and globally shelved goals. *) type proofview = { solution : Evd.evar_map; comb : goal_with_state list; @@ -115,6 +115,10 @@ module type State = sig val set : t -> unit Logical.t val modify : (t->t) -> unit Logical.t end +module type Reader = sig + type t + val get : t Logical.t +end module type Writer = sig type t diff --git a/engine/termops.ml b/engine/termops.ml index ac6870a39e..0923ab6f4b 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -310,15 +310,15 @@ let pr_evar_map_gen with_univs pr_evars env sigma = let pr_evar_list env sigma l = let open Evd in - let pr_restrict ev = - match is_restricted_evar sigma ev with + let pr_alias ev = + match is_aliased_evar sigma ev with | None -> mt () - | Some ev' -> str " (restricted to " ++ Evar.print ev' ++ str ")" + | Some ev' -> str " (aliased to " ++ Evar.print ev' ++ str ")" in let pr (ev, evi) = h 0 (Evar.print ev ++ str "==" ++ pr_evar_info env sigma evi ++ - pr_restrict ev ++ + pr_alias ev ++ (if evi.evar_body == Evar_empty then str " {" ++ pr_existential_key sigma ev ++ str "}" else mt ())) diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg index 66c72a30a2..4f20e5a800 100644 --- a/plugins/ltac/extratactics.mlg +++ b/plugins/ltac/extratactics.mlg @@ -43,7 +43,7 @@ DECLARE PLUGIN "ltac_plugin" (**********************************************************************) (* replace, discriminate, injection, simplify_eq *) -(* cutrewrite, dependent rewrite *) +(* dependent rewrite *) let with_delayed_uconstr ist c tac = let flags = { @@ -203,12 +203,6 @@ TACTIC EXTEND dependent_rewrite -> { rewriteInHyp b c id } END -TACTIC EXTEND cut_rewrite -| [ "cutrewrite" orient(b) constr(eqn) ] -> { cutRewriteInConcl b eqn } -| [ "cutrewrite" orient(b) constr(eqn) "in" hyp(id) ] - -> { cutRewriteInHyp b eqn id } -END - (**********************************************************************) (* Decompose *) diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 6233807016..f69fe064a7 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -831,7 +831,7 @@ let pr_goal_selector ~toplevel s = ++ pr_non_empty_arg (pr_clauses (Some true) pr.pr_name) h ) | TacChange (check,op,c,h) -> - let name = if check then "change_no_check" else "change" in + let name = if check then "change" else "change_no_check" in hov 1 ( primitive name ++ brk (1,1) ++ ( diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 4893758ab3..31bc698830 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -713,12 +713,6 @@ let make_clenv_binding_gen hyps_only n env sigma (c,t) = function | NoBindings -> mk_clenv_from_env env sigma n (c,t) -let make_clenv_binding_env_apply env sigma n = - make_clenv_binding_gen true n env sigma - -let make_clenv_binding_env env sigma = - make_clenv_binding_gen false None env sigma - let make_clenv_binding_apply env sigma n = make_clenv_binding_gen true n env sigma let make_clenv_binding env sigma = make_clenv_binding_gen false None env sigma diff --git a/proofs/clenv.mli b/proofs/clenv.mli index d4905de434..a72c8c5e1f 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -75,17 +75,10 @@ val clenv_unify_meta_types : ?flags:unify_flags -> clausenv -> clausenv (** the arity of the lemma is fixed the optional int tells how many prods of the lemma have to be used use all of them if None *) -val make_clenv_binding_env_apply : - env -> evar_map -> int option -> EConstr.constr * EConstr.constr -> constr bindings -> - clausenv - val make_clenv_binding_apply : env -> evar_map -> int option -> EConstr.constr * EConstr.constr -> constr bindings -> clausenv -val make_clenv_binding_env : - env -> evar_map -> EConstr.constr * EConstr.constr -> constr bindings -> clausenv - val make_clenv_binding : env -> evar_map -> EConstr.constr * EConstr.constr -> constr bindings -> clausenv diff --git a/proofs/refine.ml b/proofs/refine.ml index dcff5e2b6c..ac410a958f 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -75,6 +75,8 @@ let generic_refine ~typecheck f gl = let future_goals, sigma = Evd.pop_future_goals sigma in (* Select the goals *) let future_goals = Evd.FutureGoals.map_filter (Proofview.Unsafe.advance sigma) future_goals in + let shelf = Evd.shelf sigma in + let future_goals = Evd.FutureGoals.filter (fun ev -> not @@ List.mem ev shelf) future_goals in (* Proceed to the refinement *) let sigma = match Proofview.Unsafe.advance sigma self with | None -> diff --git a/tactics/equality.ml b/tactics/equality.ml index 26ae35a79d..8478c1957a 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1651,17 +1651,6 @@ let cutSubstClause l2r eqn cls = | None -> cutSubstInConcl l2r eqn | Some id -> cutSubstInHyp l2r eqn id -let warn_deprecated_cutrewrite = - CWarnings.create ~name:"deprecated-cutrewrite" ~category:"deprecated" - (fun () -> strbrk"\"cutrewrite\" is deprecated. Use \"replace\" instead.") - -let cutRewriteClause l2r eqn cls = - warn_deprecated_cutrewrite (); - 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 substClause l2r c cls = Proofview.Goal.enter begin fun gl -> let eq = pf_apply get_type_of gl c in diff --git a/tactics/equality.mli b/tactics/equality.mli index fdcbbc0e3c..5a4fe47cab 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -107,10 +107,6 @@ val dEqThen : keep_proofs:(bool option) -> evars_flag -> (clear_flag -> constr - val make_iterated_tuple : env -> evar_map -> constr -> (constr * types) -> evar_map * (constr * constr * constr) -(* The family cutRewriteIn expect an equality statement *) -val cutRewriteInHyp : bool -> types -> Id.t -> unit Proofview.tactic -val cutRewriteInConcl : bool -> constr -> unit Proofview.tactic - (* The family rewriteIn expect the proof of an equality *) val rewriteInHyp : bool -> constr -> Id.t -> unit Proofview.tactic val rewriteInConcl : bool -> constr -> unit Proofview.tactic diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index fc099f643d..c0fad0026f 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -695,6 +695,8 @@ module New = struct (* Check that holes in arguments have been resolved *) let check_evars env sigma extsigma origsigma = + let reachable = lazy (Evarutil.reachable_from_evars sigma + (Evar.Map.domain (Evd.undefined_map origsigma))) in let rec is_undefined_up_to_restriction sigma evk = if Evd.mem origsigma evk then None else let evi = Evd.find sigma evk in @@ -710,7 +712,12 @@ module New = struct let rest = Evd.fold_undefined (fun evk evi acc -> match is_undefined_up_to_restriction sigma evk with - | Some (evk',evi) -> (evk',evi)::acc + | Some (evk',evi) -> + (* If [evk'] descends from [evk] which descends itself from + an originally undefined evar in [origsigma], it is a not + a fresh undefined hole from [sigma]. *) + if Evar.Set.mem evk (Lazy.force reachable) then acc + else (evk',evi)::acc | _ -> acc) extsigma [] in diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 5f7e35d205..686779b1d2 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -3248,13 +3248,10 @@ let rec consume_pattern avoid na isdep gl = let open CAst in function | {loc;v=IntroForthcoming true}::names when not isdep -> consume_pattern avoid na isdep gl names | {loc;v=IntroForthcoming _}::names as fullpat -> - let avoid = Id.Set.union avoid (explicit_intro_names names) in (CAst.make ?loc @@ intropattern_of_name gl avoid na, fullpat) | {loc;v=IntroNaming IntroAnonymous}::names -> - let avoid = Id.Set.union avoid (explicit_intro_names names) in (CAst.make ?loc @@ intropattern_of_name gl avoid na, names) | {loc;v=IntroNaming (IntroFresh id')}::names -> - let avoid = Id.Set.union avoid (explicit_intro_names names) in (CAst.make ?loc @@ IntroNaming (IntroIdentifier (new_fresh_id avoid id' gl)), names) | pat::names -> (pat,names) @@ -3312,7 +3309,7 @@ let get_recarg_dest (recargdests,tophyp) = *) let induct_discharge with_evars dests avoid' tac (avoid,ra) names = - let avoid = Id.Set.union avoid avoid' in + let avoid = Id.Set.union avoid' (Id.Set.union avoid (explicit_intro_names names)) in let rec peel_tac ra dests names thin = match ra with | (RecArg,_,deprec,recvarname) :: @@ -3320,7 +3317,7 @@ let induct_discharge with_evars dests avoid' tac (avoid,ra) names = Proofview.Goal.enter begin fun gl -> let (recpat,names) = match names with | [{CAst.loc;v=IntroNaming (IntroIdentifier id)} as pat] -> - let id' = next_ident_away (add_prefix "IH" id) avoid in + let id' = new_fresh_id avoid (add_prefix "IH" id) gl in (pat, [CAst.make @@ IntroNaming (IntroIdentifier id')]) | _ -> consume_pattern avoid (Name recvarname) deprec gl names in let dest = get_recarg_dest dests in @@ -5184,14 +5181,14 @@ end (** Tacticals defined directly in term of Proofview *) module New = struct - open Genredexpr - open Locus - let reduce_after_refine = - reduce - (Lazy {rBeta=true;rMatch=true;rFix=true;rCofix=true; - rZeta=false;rDelta=false;rConst=[]}) - {onhyps = Some []; concl_occs = AllOccurrences } + (* For backward compatibility reasons, we do not contract let-ins, but we unfold them. *) + let redfun env t = + let open CClosure in + let flags = RedFlags.red_add_transparent allnolet TransparentState.empty in + clos_norm_flags flags env t + in + reduct_in_concl ~check:false (redfun,DEFAULTcast) let refine ~typecheck c = Refine.refine ~typecheck c <*> diff --git a/test-suite/bugs/closed/bug_12930.v b/test-suite/bugs/closed/bug_12930.v new file mode 100644 index 0000000000..e2a524301a --- /dev/null +++ b/test-suite/bugs/closed/bug_12930.v @@ -0,0 +1,10 @@ +Section S. + Variable v : Prop. + Variable vv : v. + Collection easy := Type*. + + Lemma ybar : v. + Proof using easy. + exact vv. + Qed. +End S. diff --git a/test-suite/bugs/closed/bug_12944.v b/test-suite/bugs/closed/bug_12944.v new file mode 100644 index 0000000000..d6720d9906 --- /dev/null +++ b/test-suite/bugs/closed/bug_12944.v @@ -0,0 +1,12 @@ + +Inductive vector A : nat -> Type := + |nil : vector A 0 + |cons : forall (h:A) (n:nat), vector A n -> vector A (S n). + +Global Set Mangle Names. + +Lemma vlookup_middle {A n} (v : vector A n) : True. +Proof. + induction v as [|?? IHv]. + all:exact I. +Qed. diff --git a/test-suite/bugs/closed/bug_4413.v b/test-suite/bugs/closed/bug_4413.v new file mode 100644 index 0000000000..cb30aa5d1f --- /dev/null +++ b/test-suite/bugs/closed/bug_4413.v @@ -0,0 +1,8 @@ + +(* Regression wrt v8.4 related to the change of order of resolution of evar-evar unification problems. *) +Goal exists x, x=1 -> True. +eexists. intro H. +pose proof (f_equal (fun k => k) H). +Undo. +pose (@f_equal _ _ S _ _ H). +Abort. diff --git a/test-suite/bugs/closed/bug_7825.v b/test-suite/bugs/closed/bug_7825.v new file mode 100644 index 0000000000..3f8708059a --- /dev/null +++ b/test-suite/bugs/closed/bug_7825.v @@ -0,0 +1,50 @@ +Record T (x : nat) := { t : x = x }. + +Goal exists x, T x. + refine (ex_intro _ _ _). + Show Existentials. + simple refine {| t := _ |}. + reflexivity. + Unshelve. exact 0. +Qed. + +(** Fine if the new evar is defined as the originally shelved evar: we do nothing. + In the other direction we promote the non-shelved new goal to a shelved one: + shelved status has priority over goal status. *) + +Goal forall a : nat, exists x, T x. + evar (x : nat). subst x. Show Existentials. + intros a. simple refine (ex_intro ?[x0] _ _). shelve. simpl. + (** Here ?x := ?x0 which is shelved, so ?x becomes shelved even if it would + not be by default (refine ?x and _ produce non-shelved evars by default)*) + simple refine (Build_T ?x _). + reflexivity. + Unshelve. exact 0. +Qed. + +Goal { A : _ & { P : _ & @sigT A P } }. + epose _ as A; + epose _ as P; + exists A, P. + (* Regardless of which evars are in the goals vs the hypotheses, + [simple refine (existT _ _ _)] should leave over two goals. This + should be true even when chained with epose. *) + assert_succeeds (simple refine (existT _ _ _); let n := numgoals in guard n = 2); + subst P; + assert_succeeds (simple refine (existT _ _ _); let n := numgoals in guard n = 2); + subst A; + assert_succeeds (simple refine (existT _ _ _); let n := numgoals in guard n = 2). + (* fails *) +Abort. + +Goal { A : _ & { P : _ & @sigT A P } }. + epose _ as A; + epose _ as P; + exists A, P; (* In this example we chain everything *) + assert_succeeds (simple refine (existT _ _ _); let n := numgoals in guard n = 2); + subst P; + assert_succeeds (simple refine (existT _ _ _); let n := numgoals in guard n = 2); + subst A; + assert_succeeds (simple refine (existT _ _ _); let n := numgoals in guard n = 2). + (* fails *) +Abort. diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v index 73fe53c757..a39b17e1f1 100644 --- a/test-suite/success/induct.v +++ b/test-suite/success/induct.v @@ -196,3 +196,13 @@ Goal forall m n:nat, n=m. double induction m n. Abort. +(* Mentioned as part of bug #12944 *) + +Inductive test : Set := cons : forall (IHv : nat) (v : test), test. + +Goal test -> test. +induction 1 as [? IHv]. +Undo. +destruct 1 as [? IHv]. +exact IHv. (* Check that the name is granted *) +Qed. diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v index 9e10786fcd..0f62db42cf 100644 --- a/theories/Bool/Bool.v +++ b/theories/Bool/Bool.v @@ -258,7 +258,7 @@ Qed. Lemma orb_true_elim : forall b1 b2:bool, b1 || b2 = true -> {b1 = true} + {b2 = true}. Proof. - destruct b1; simpl; auto. + intro b1; destruct b1; simpl; auto. Defined. Lemma orb_prop : forall a b:bool, a || b = true -> a = true \/ b = true. @@ -424,7 +424,7 @@ Notation andb_true_b := andb_true_l (only parsing). Lemma andb_false_elim : forall b1 b2:bool, b1 && b2 = false -> {b1 = false} + {b2 = false}. Proof. - destruct b1; simpl; auto. + intro b1; destruct b1; simpl; auto. Defined. Hint Resolve andb_false_elim: bool. @@ -681,17 +681,17 @@ Qed. Lemma negb_xorb_l : forall b b', negb (xorb b b') = xorb (negb b) b'. Proof. - destruct b,b'; trivial. + intros b b'; destruct b,b'; trivial. Qed. Lemma negb_xorb_r : forall b b', negb (xorb b b') = xorb b (negb b'). Proof. - destruct b,b'; trivial. + intros b b'; destruct b,b'; trivial. Qed. Lemma xorb_negb_negb : forall b b', xorb (negb b) (negb b') = xorb b b'. Proof. - destruct b,b'; trivial. + intros b b'; destruct b,b'; trivial. Qed. (** Lemmas about the [b = true] embedding of [bool] to [Prop] *) diff --git a/theories/Classes/CMorphisms.v b/theories/Classes/CMorphisms.v index 598bd8b9c5..9a3a1d3709 100644 --- a/theories/Classes/CMorphisms.v +++ b/theories/Classes/CMorphisms.v @@ -20,7 +20,7 @@ Require Import Coq.Program.Tactics. Require Export Coq.Classes.CRelationClasses. Generalizable Variables A eqA B C D R RA RB RC m f x y. -Local Obligation Tactic := simpl_crelation. +Local Obligation Tactic := try solve [ simpl_crelation ]. Set Universe Polymorphism. @@ -268,6 +268,7 @@ Section GenericInstances. Next Obligation. Proof with auto. + intros A R H B R' H0 x y z X X0 x0 y0 X1. assert(R x0 x0). - transitivity y0... symmetry... - transitivity (y x0)... @@ -284,6 +285,7 @@ Section GenericInstances. Next Obligation. Proof. + intros A B C RA RB RC f mor x y X x0 y0 X0. apply mor ; auto. Qed. @@ -297,6 +299,7 @@ Section GenericInstances. Next Obligation. Proof with auto. + intros A R H x y X x0 y0 X0 X1. transitivity x... transitivity x0... Qed. @@ -309,6 +312,7 @@ Section GenericInstances. Next Obligation. Proof with auto. + intros A R H x x0 y X X0. transitivity y... Qed. @@ -318,6 +322,7 @@ Section GenericInstances. Next Obligation. Proof with auto. + intros A R H x x0 y X X0. transitivity x0... Qed. @@ -327,6 +332,7 @@ Section GenericInstances. Next Obligation. Proof with auto. + intros A R H x x0 y X X0. transitivity y... symmetry... Qed. @@ -335,6 +341,7 @@ Section GenericInstances. Next Obligation. Proof with auto. + intros A R H x x0 y X X0. transitivity x0... symmetry... Qed. @@ -343,6 +350,7 @@ Section GenericInstances. Next Obligation. Proof with auto. + intros A R H x x0 y X. split. - intros ; transitivity x0... - intros. @@ -358,6 +366,7 @@ Section GenericInstances. Next Obligation. Proof with auto. + intros A R H x y X y0 y1 e X0; destruct e. transitivity y... Qed. @@ -368,6 +377,7 @@ Section GenericInstances. Next Obligation. Proof with auto. + intros A R H x y X x0 y0 X0. split ; intros. - transitivity x0... transitivity x... symmetry... diff --git a/theories/Classes/CRelationClasses.v b/theories/Classes/CRelationClasses.v index a27919dd43..72a196ca7a 100644 --- a/theories/Classes/CRelationClasses.v +++ b/theories/Classes/CRelationClasses.v @@ -319,7 +319,7 @@ Section Binary. split; red; unfold relation_equivalence, iffT. - firstorder. - firstorder. - - intros. specialize (X x0 y0). specialize (X0 x0 y0). firstorder. + - intros x y z X X0 x0 y0. specialize (X x0 y0). specialize (X0 x0 y0). firstorder. Qed. Global Instance relation_implication_preorder : PreOrder (@subrelation A). @@ -346,7 +346,7 @@ Section Binary. Lemma PartialOrder_inverse `(PartialOrder eqA R) : PartialOrder eqA (flip R). Proof. unfold flip; constructor; unfold flip. - - intros. apply H. apply symmetry. apply X. + - intros X. apply H. apply symmetry. apply X. - unfold relation_conjunction. intros [H1 H2]. apply H. constructor; assumption. Qed. End Binary. diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v index 43adb0b69f..c70e3fe478 100644 --- a/theories/Classes/Morphisms.v +++ b/theories/Classes/Morphisms.v @@ -21,7 +21,7 @@ Require Import Coq.Relations.Relation_Definitions. Require Export Coq.Classes.RelationClasses. Generalizable Variables A eqA B C D R RA RB RC m f x y. -Local Obligation Tactic := simpl_relation. +Local Obligation Tactic := try solve [ simpl_relation ]. (** * Morphisms. @@ -201,12 +201,12 @@ Section Relations. Global Instance pointwise_subrelation `(sub : subrelation B R R') : subrelation (pointwise_relation R) (pointwise_relation R') | 4. - Proof. reduce. unfold pointwise_relation in *. apply sub. apply H. Qed. + Proof. intros x y H a. unfold pointwise_relation in *. apply sub. apply H. Qed. (** For dependent function types. *) Lemma forall_subrelation (R S : forall x : A, relation (P x)) : (forall a, subrelation (R a) (S a)) -> subrelation (forall_relation R) (forall_relation S). - Proof. reduce. apply H. apply H0. Qed. + Proof. intros H x y H0 a. apply H. apply H0. Qed. End Relations. Typeclasses Opaque respectful pointwise_relation forall_relation. @@ -259,6 +259,7 @@ Section GenericInstances. Next Obligation. Proof with auto. + intros R H R' H0 x y z H1 H2 x0 y0 H3. assert(R x0 x0). - transitivity y0... symmetry... - transitivity (y x0)... @@ -272,6 +273,7 @@ Section GenericInstances. Next Obligation. Proof. + intros RA R mR x y H x0 y0 H0. unfold complement. pose (mR x y H x0 y0 H0). intuition. @@ -285,7 +287,7 @@ Section GenericInstances. Next Obligation. Proof. - apply mor ; auto. + intros RA RB RC f mor x y H x0 y0 H0; apply mor ; auto. Qed. @@ -298,6 +300,7 @@ Section GenericInstances. Next Obligation. Proof with auto. + intros R H x y H0 x0 y0 H1 H2. transitivity x... transitivity x0... Qed. @@ -310,6 +313,7 @@ Section GenericInstances. Next Obligation. Proof with auto. + intros R H x x0 y H0 H1. transitivity y... Qed. @@ -319,6 +323,7 @@ Section GenericInstances. Next Obligation. Proof with auto. + intros R H x x0 y H0 H1. transitivity x0... Qed. @@ -328,6 +333,7 @@ Section GenericInstances. Next Obligation. Proof with auto. + intros R H x x0 y H0 H1. transitivity y... symmetry... Qed. @@ -336,6 +342,7 @@ Section GenericInstances. Next Obligation. Proof with auto. + intros R H x x0 y H0 H1. transitivity x0... symmetry... Qed. @@ -344,6 +351,7 @@ Section GenericInstances. Next Obligation. Proof with auto. + intros R H x x0 y H0. split. - intros ; transitivity x0... - intros. @@ -359,6 +367,7 @@ Section GenericInstances. Next Obligation. Proof with auto. + intros R H x y H0 y0 y1 e H2; destruct e. transitivity y... Qed. @@ -369,6 +378,7 @@ Section GenericInstances. Next Obligation. Proof with auto. + intros R H x y H0 x0 y0 H1. split ; intros. - transitivity x0... transitivity x... symmetry... @@ -383,7 +393,7 @@ Section GenericInstances. Next Obligation. Proof. - simpl_relation. + intros RA RB RC x y H x0 y0 H0 x1 y1 H1. unfold compose. apply H. apply H0. apply H1. Qed. @@ -400,9 +410,9 @@ Section GenericInstances. Proper (relation_equivalence ++> relation_equivalence ++> relation_equivalence) (@respectful A B). Proof. - reduce. + intros x y H x0 y0 H0 x1 x2. unfold respectful, relation_equivalence, predicate_equivalence in * ; simpl in *. - split ; intros. + split ; intros H1 x3 y1 H2. - rewrite <- H0. apply H1. @@ -512,9 +522,9 @@ Ltac partial_application_tactic := Instance proper_proper : Proper (relation_equivalence ==> eq ==> iff) (@Proper A). Proof. - simpl_relation. + intros A x y H y0 y1 e; destruct e. reduce in H. - split ; red ; intros. + split ; red ; intros H0. - setoid_rewrite <- H. apply H0. - setoid_rewrite H. @@ -555,8 +565,7 @@ Section Normalize. Lemma proper_normalizes_proper `(Normalizes R0 R1, Proper A R1 m) : Proper R0 m. Proof. - red in H, H0. - rewrite H. + rewrite normalizes. assumption. Qed. @@ -571,10 +580,11 @@ Lemma flip_arrow {A : Type} {B : Type} `(NA : Normalizes A R (flip R'''), NB : Normalizes B R' (flip R'')) : Normalizes (A -> B) (R ==> R') (flip (R''' ==> R'')%signature). Proof. - unfold Normalizes in *. intros. + unfold Normalizes in *. unfold relation_equivalence in *. unfold predicate_equivalence in *. simpl in *. - unfold respectful. unfold flip in *. firstorder. + unfold respectful. unfold flip in *. + intros x x0; split; intros H x1 y H0. - apply NB. apply H. apply NA. apply H0. - apply NB. apply H. apply NA. apply H0. Qed. diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index 9b92ade096..5381e91997 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -107,7 +107,7 @@ Section Defs. (** Any symmetric relation is equal to its inverse. *) Lemma subrelation_symmetric R `(Symmetric R) : subrelation (flip R) R. - Proof. hnf. intros. red in H0. apply symmetry. assumption. Qed. + Proof. hnf. intros x y H0. red in H0. apply symmetry. assumption. Qed. Section flip. @@ -212,7 +212,7 @@ Hint Extern 3 (PreOrder (flip _)) => class_apply flip_PreOrder : typeclass_insta Hint Extern 4 (subrelation (flip _) _) => class_apply @subrelation_symmetric : typeclass_instances. -Arguments irreflexivity {A R Irreflexive} [x] _. +Arguments irreflexivity {A R Irreflexive} [x] _ : rename. Arguments symmetry {A} {R} {_} [x] [y] _. Arguments asymmetry {A} {R} {_} [x] [y] _ _. Arguments transitivity {A} {R} {_} [x] [y] [z] _ _. @@ -260,7 +260,7 @@ Ltac simpl_relation := unfold flip, impl, arrow ; try reduce ; program_simpl ; try ( solve [ dintuition ]). -Local Obligation Tactic := simpl_relation. +Local Obligation Tactic := try solve [ simpl_relation ]. (** Logical implication. *) @@ -399,29 +399,30 @@ Program Instance predicate_equivalence_equivalence : Equivalence (@predicate_equivalence l). Next Obligation. - induction l ; firstorder. + intro l; induction l ; firstorder. Qed. Next Obligation. - induction l ; firstorder. + intro l; induction l ; firstorder. Qed. Next Obligation. + intro l. fold pointwise_lifting. - induction l. + induction l as [|T l IHl]. - firstorder. - - intros. simpl in *. pose (IHl (x x0) (y x0) (z x0)). + - intros x y z H H0 x0. pose (IHl (x x0) (y x0) (z x0)). firstorder. Qed. Program Instance predicate_implication_preorder : PreOrder (@predicate_implication l). Next Obligation. - induction l ; firstorder. + intro l; induction l ; firstorder. Qed. Next Obligation. - induction l. + intro l. + induction l as [|T l IHl]. - firstorder. - - unfold predicate_implication in *. simpl in *. - intro. pose (IHl (x x0) (y x0) (z x0)). firstorder. + - intros x y z H H0 x0. pose (IHl (x x0) (y x0) (z x0)). firstorder. Qed. (** We define the various operations which define the algebra on binary relations, diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v index 02903643d4..98fd52f351 100644 --- a/theories/Init/Peano.v +++ b/theories/Init/Peano.v @@ -77,7 +77,7 @@ Hint Resolve O_S: core. Theorem n_Sn : forall n:nat, n <> S n. Proof. - induction n; auto. + intro n; induction n; auto. Qed. Hint Resolve n_Sn: core. @@ -92,7 +92,7 @@ Hint Resolve f_equal2_nat: core. Lemma plus_n_O : forall n:nat, n = n + 0. Proof. - induction n; simpl; auto. + intro n; induction n; simpl; auto. Qed. Remove Hints eq_refl : core. @@ -129,13 +129,13 @@ Hint Resolve f_equal2_mult: core. Lemma mult_n_O : forall n:nat, 0 = n * 0. Proof. - induction n; simpl; auto. + intro n; induction n; simpl; auto. Qed. Hint Resolve mult_n_O: core. Lemma mult_n_Sm : forall n m:nat, n * m + n = n * S m. Proof. - intros; induction n as [| p H]; simpl; auto. + intros n m; induction n as [| p H]; simpl; auto. destruct H; rewrite <- plus_n_Sm; apply eq_S. pattern m at 1 3; elim m; simpl; auto. Qed. @@ -192,7 +192,7 @@ Register gt as num.nat.gt. Theorem le_pred : forall n m, n <= m -> pred n <= pred m. Proof. -induction 1; auto. destruct m; simpl; auto. +induction 1 as [|m _]; auto. destruct m; simpl; auto. Qed. Theorem le_S_n : forall n m, S n <= S m -> n <= m. @@ -202,7 +202,7 @@ Qed. Theorem le_0_n : forall n, 0 <= n. Proof. - induction n; constructor; trivial. + intro n; induction n; constructor; trivial. Qed. Theorem le_n_S : forall n m, n <= m -> S n <= S m. @@ -215,7 +215,7 @@ Qed. Theorem nat_case : forall (n:nat) (P:nat -> Prop), P 0 -> (forall m:nat, P (S m)) -> P n. Proof. - induction n; auto. + intros n P IH0 IHS; case n; auto. Qed. (** Principle of double induction *) @@ -226,8 +226,9 @@ Theorem nat_double_ind : (forall n:nat, R (S n) 0) -> (forall n m:nat, R n m -> R (S n) (S m)) -> forall n m:nat, R n m. Proof. + intros R ? ? ? n. induction n; auto. - destruct m; auto. + intro m; destruct m; auto. Qed. (** Maximum and minimum : definitions and specifications *) @@ -237,28 +238,28 @@ Notation min := Nat.min (only parsing). Lemma max_l n m : m <= n -> Nat.max n m = n. Proof. - revert m; induction n; destruct m; simpl; trivial. + revert m; induction n as [|n IHn]; intro m; destruct m; simpl; trivial. - inversion 1. - intros. apply f_equal, IHn, le_S_n; trivial. Qed. Lemma max_r n m : n <= m -> Nat.max n m = m. Proof. - revert m; induction n; destruct m; simpl; trivial. + revert m; induction n as [|n IHn]; intro m; destruct m; simpl; trivial. - inversion 1. - intros. apply f_equal, IHn, le_S_n; trivial. Qed. Lemma min_l n m : n <= m -> Nat.min n m = n. Proof. - revert m; induction n; destruct m; simpl; trivial. + revert m; induction n as [|n IHn]; intro m; destruct m; simpl; trivial. - inversion 1. - intros. apply f_equal, IHn, le_S_n; trivial. Qed. Lemma min_r n m : m <= n -> Nat.min n m = m. Proof. - revert m; induction n; destruct m; simpl; trivial. + revert m; induction n as [|n IHn]; intro m; destruct m; simpl; trivial. - inversion 1. - intros. apply f_equal, IHn, le_S_n; trivial. Qed. @@ -267,7 +268,7 @@ Qed. Lemma nat_rect_succ_r {A} (f: A -> A) (x:A) n : nat_rect (fun _ => A) x (fun _ => f) (S n) = nat_rect (fun _ => A) (f x) (fun _ => f) n. Proof. - induction n; intros; simpl; rewrite <- ?IHn; trivial. + induction n as [|n IHn]; intros; simpl; rewrite <- ?IHn; trivial. Qed. Theorem nat_rect_plus : @@ -275,5 +276,5 @@ Theorem nat_rect_plus : nat_rect (fun _ => A) x (fun _ => f) (n + m) = nat_rect (fun _ => A) (nat_rect (fun _ => A) x (fun _ => f) m) (fun _ => f) n. Proof. - induction n; intros; simpl; rewrite ?IHn; trivial. + intro n; induction n as [|n IHn]; intros; simpl; rewrite ?IHn; trivial. Qed. diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v index b13206db94..e1db68aea9 100644 --- a/theories/Init/Tactics.v +++ b/theories/Init/Tactics.v @@ -135,8 +135,8 @@ lazymatch T with rename H2 into H; find_equiv H | clear H] | forall x : ?t, _ => - let a := fresh "a" with - H1 := fresh "H" in + let a := fresh "a" in + let H1 := fresh "H" in evar (a : t); pose proof (H a) as H1; unfold a in H1; clear a; clear H; rename H1 into H; find_equiv H | ?A <-> ?B => idtac @@ -203,7 +203,7 @@ Set Implicit Arguments. Lemma decide_left : forall (C:Prop) (decide:{C}+{~C}), C -> forall P:{C}+{~C}->Prop, (forall H:C, P (left _ H)) -> P decide. Proof. - intros; destruct decide. + intros C decide H P H0; destruct decide. - apply H0. - contradiction. Qed. @@ -211,7 +211,7 @@ Qed. Lemma decide_right : forall (C:Prop) (decide:{C}+{~C}), ~C -> forall P:{C}+{~C}->Prop, (forall H:~C, P (right _ H)) -> P decide. Proof. - intros; destruct decide. + intros C decide H P H0; destruct decide. - contradiction. - apply H0. Qed. diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v index a305626eb3..60200ae0f6 100644 --- a/theories/Init/Wf.v +++ b/theories/Init/Wf.v @@ -85,8 +85,7 @@ Section Well_founded. Scheme Acc_inv_dep := Induction for Acc Sort Prop. - Lemma Fix_F_eq : - forall (x:A) (r:Acc x), + Lemma Fix_F_eq (x:A) (r:Acc x) : F (fun (y:A) (p:R y x) => Fix_F (x:=y) (Acc_inv r p)) = Fix_F (x:=x) r. Proof. destruct r using Acc_inv_dep; auto. @@ -104,7 +103,7 @@ Section Well_founded. Lemma Fix_F_inv : forall (x:A) (r s:Acc x), Fix_F r = Fix_F s. Proof. - intro x; induction (Rwf x); intros. + intro x; induction (Rwf x); intros r s. rewrite <- (Fix_F_eq r); rewrite <- (Fix_F_eq s); intros. apply F_ext; auto. Qed. diff --git a/theories/Numbers/NatInt/NZAdd.v b/theories/Numbers/NatInt/NZAdd.v index 7982411bdd..66cbba9e08 100644 --- a/theories/Numbers/NatInt/NZAdd.v +++ b/theories/Numbers/NatInt/NZAdd.v @@ -22,7 +22,7 @@ Ltac nzsimpl' := autorewrite with nz nz'. Theorem add_0_r : forall n, n + 0 == n. Proof. - nzinduct n. + intro n; nzinduct n. - now nzsimpl. - intro. nzsimpl. now rewrite succ_inj_wd. Qed. diff --git a/theories/Numbers/NatInt/NZBase.v b/theories/Numbers/NatInt/NZBase.v index 8bc393bbad..d4f70adbc5 100644 --- a/theories/Numbers/NatInt/NZBase.v +++ b/theories/Numbers/NatInt/NZBase.v @@ -74,7 +74,7 @@ Proof. intros z Base Step; revert Base; pattern z; apply bi_induction. - solve_proper. - intro; now apply bi_induction. -- intro; pose proof (Step n); tauto. +- intro n; pose proof (Step n); tauto. Qed. End CentralInduction. @@ -83,7 +83,7 @@ Tactic Notation "nzinduct" ident(n) := induction_maker n ltac:(apply bi_induction). Tactic Notation "nzinduct" ident(n) constr(u) := - induction_maker n ltac:(apply central_induction with (z := u)). + induction_maker n ltac:(apply (fun A A_wd => central_induction A A_wd u)). End NZBaseProp. diff --git a/theories/Numbers/NatInt/NZDiv.v b/theories/Numbers/NatInt/NZDiv.v index 1c45aa440f..e6249be8df 100644 --- a/theories/Numbers/NatInt/NZDiv.v +++ b/theories/Numbers/NatInt/NZDiv.v @@ -116,7 +116,7 @@ Qed. Theorem div_small: forall a b, 0<=a<b -> a/b == 0. Proof. -intros. symmetry. +intros a b ?. symmetry. apply div_unique with a; intuition; try order. now nzsimpl. Qed. @@ -149,7 +149,7 @@ Qed. Lemma mod_1_r: forall a, 0<=a -> a mod 1 == 0. Proof. -intros. symmetry. +intros a ?. symmetry. apply mod_unique with a; try split; try order; try apply lt_0_1. now nzsimpl. Qed. @@ -173,7 +173,7 @@ Qed. Lemma mod_mul : forall a b, 0<=a -> 0<b -> (a*b) mod b == 0. Proof. -intros; symmetry. +intros a b ? ?; symmetry. apply mod_unique with a; try split; try order. - apply mul_nonneg_nonneg; order. - nzsimpl; apply mul_comm. @@ -186,7 +186,7 @@ Qed. Theorem mod_le: forall a b, 0<=a -> 0<b -> a mod b <= a. Proof. -intros. destruct (le_gt_cases b a). +intros a b ? ?. destruct (le_gt_cases b a). - apply le_trans with b; auto. apply lt_le_incl. destruct (mod_bound_pos a b); auto. - rewrite lt_eq_cases; right. @@ -198,7 +198,7 @@ Qed. Lemma div_pos: forall a b, 0<=a -> 0<b -> 0 <= a/b. Proof. -intros. +intros a b ? ?. rewrite (mul_le_mono_pos_l _ _ b); auto; nzsimpl. rewrite (add_le_mono_r _ _ (a mod b)). rewrite <- div_mod by order. @@ -247,7 +247,7 @@ Qed. Lemma div_lt : forall a b, 0<a -> 1<b -> a/b < a. Proof. -intros. +intros a b ? ?. assert (0 < b) by (apply lt_trans with 1; auto using lt_0_1). destruct (lt_ge_cases a b). - rewrite div_small; try split; order. @@ -284,7 +284,7 @@ Qed. Lemma mul_div_le : forall a b, 0<=a -> 0<b -> b*(a/b) <= a. Proof. -intros. +intros a b ? ?. rewrite (add_le_mono_r _ _ (a mod b)), <- div_mod by order. rewrite <- (add_0_r a) at 1. rewrite <- add_le_mono_l. destruct (mod_bound_pos a b); order. @@ -292,7 +292,7 @@ Qed. Lemma mul_succ_div_gt : forall a b, 0<=a -> 0<b -> a < b*(S (a/b)). Proof. -intros. +intros a b ? ?. rewrite (div_mod a b) at 1 by order. rewrite (mul_succ_r). rewrite <- add_lt_mono_l. @@ -304,7 +304,7 @@ Qed. Lemma div_exact : forall a b, 0<=a -> 0<b -> (a == b*(a/b) <-> a mod b == 0). Proof. -intros. rewrite (div_mod a b) at 1 by order. +intros a b ? ?. rewrite (div_mod a b) at 1 by order. rewrite <- (add_0_r (b*(a/b))) at 2. apply add_cancel_l. Qed. @@ -314,7 +314,7 @@ Qed. Theorem div_lt_upper_bound: forall a b q, 0<=a -> 0<b -> a < b*q -> a/b < q. Proof. -intros. +intros a b q ? ? ?. rewrite (mul_lt_mono_pos_l b) by order. apply le_lt_trans with a; auto. apply mul_div_le; auto. @@ -323,7 +323,7 @@ Qed. Theorem div_le_upper_bound: forall a b q, 0<=a -> 0<b -> a <= b*q -> a/b <= q. Proof. -intros. +intros a b q ? ? ?. rewrite (mul_le_mono_pos_l _ _ b) by order. apply le_trans with a; auto. apply mul_div_le; auto. @@ -362,7 +362,7 @@ Qed. Lemma mod_add : forall a b c, 0<=a -> 0<=a+b*c -> 0<c -> (a + b * c) mod c == a mod c. Proof. - intros. + intros a b c ? ? ?. symmetry. apply mod_unique with (a/c+b); auto. - apply mod_bound_pos; auto. @@ -373,7 +373,7 @@ Qed. Lemma div_add : forall a b c, 0<=a -> 0<=a+b*c -> 0<c -> (a + b * c) / c == a / c + b. Proof. - intros. + intros a b c ? ? ?. apply (mul_cancel_l _ _ c); try order. apply (add_cancel_r _ _ ((a+b*c) mod c)). rewrite <- div_mod, mod_add by order. @@ -393,7 +393,7 @@ Qed. Lemma div_mul_cancel_r : forall a b c, 0<=a -> 0<b -> 0<c -> (a*c)/(b*c) == a/b. Proof. - intros. + intros a b c ? ? ?. symmetry. apply div_unique with ((a mod b)*c). - apply mul_nonneg_nonneg; order. @@ -409,13 +409,13 @@ Qed. Lemma div_mul_cancel_l : forall a b c, 0<=a -> 0<b -> 0<c -> (c*a)/(c*b) == a/b. Proof. - intros. rewrite !(mul_comm c); apply div_mul_cancel_r; auto. + intros a b c ? ? ?. rewrite !(mul_comm c); apply div_mul_cancel_r; auto. Qed. Lemma mul_mod_distr_l: forall a b c, 0<=a -> 0<b -> 0<c -> (c*a) mod (c*b) == c * (a mod b). Proof. - intros. + intros a b c ? ? ?. rewrite <- (add_cancel_l _ _ ((c*b)* ((c*a)/(c*b)))). rewrite <- div_mod. - rewrite div_mul_cancel_l; auto. @@ -427,7 +427,7 @@ Qed. Lemma mul_mod_distr_r: forall a b c, 0<=a -> 0<b -> 0<c -> (a*c) mod (b*c) == (a mod b) * c. Proof. - intros. rewrite !(mul_comm _ c); now rewrite mul_mod_distr_l. + intros a b c ? ? ?. rewrite !(mul_comm _ c); now rewrite mul_mod_distr_l. Qed. (** Operations modulo. *) @@ -435,7 +435,7 @@ Qed. Theorem mod_mod: forall a n, 0<=a -> 0<n -> (a mod n) mod n == a mod n. Proof. - intros. destruct (mod_bound_pos a n); auto. now rewrite mod_small_iff. + intros a n ? ?. destruct (mod_bound_pos a n); auto. now rewrite mod_small_iff. Qed. Lemma mul_mod_idemp_l : forall a b n, 0<=a -> 0<=b -> 0<n -> @@ -454,13 +454,14 @@ Qed. Lemma mul_mod_idemp_r : forall a b n, 0<=a -> 0<=b -> 0<n -> (a*(b mod n)) mod n == (a*b) mod n. Proof. - intros. rewrite !(mul_comm a). apply mul_mod_idemp_l; auto. + intros a b n ? ? ?. rewrite !(mul_comm a). apply mul_mod_idemp_l; auto. Qed. Theorem mul_mod: forall a b n, 0<=a -> 0<=b -> 0<n -> (a * b) mod n == ((a mod n) * (b mod n)) mod n. Proof. - intros. rewrite mul_mod_idemp_l, mul_mod_idemp_r; trivial. - reflexivity. + intros a b n ? ? ?. rewrite mul_mod_idemp_l, mul_mod_idemp_r; trivial. + - reflexivity. - now destruct (mod_bound_pos b n). Qed. @@ -478,13 +479,14 @@ Qed. Lemma add_mod_idemp_r : forall a b n, 0<=a -> 0<=b -> 0<n -> (a+(b mod n)) mod n == (a+b) mod n. Proof. - intros. rewrite !(add_comm a). apply add_mod_idemp_l; auto. + intros a b n ? ? ?. rewrite !(add_comm a). apply add_mod_idemp_l; auto. Qed. Theorem add_mod: forall a b n, 0<=a -> 0<=b -> 0<n -> (a+b) mod n == (a mod n + b mod n) mod n. Proof. - intros. rewrite add_mod_idemp_l, add_mod_idemp_r; trivial. - reflexivity. + intros a b n ? ? ?. rewrite add_mod_idemp_l, add_mod_idemp_r; trivial. + - reflexivity. - now destruct (mod_bound_pos b n). Qed. @@ -525,7 +527,7 @@ Qed. Theorem div_mul_le: forall a b c, 0<=a -> 0<b -> 0<=c -> c*(a/b) <= (c*a)/b. Proof. - intros. + intros a b c ? ? ?. apply div_le_lower_bound; auto. - apply mul_nonneg_nonneg; auto. - rewrite mul_assoc, (mul_comm b c), <- mul_assoc. @@ -538,7 +540,7 @@ Qed. Lemma mod_divides : forall a b, 0<=a -> 0<b -> (a mod b == 0 <-> exists c, a == b*c). Proof. - split. + intros a b ? ?; split. - intros. exists (a/b). rewrite div_exact; auto. - intros (c,Hc). rewrite Hc, mul_comm. apply mod_mul; auto. rewrite (mul_le_mono_pos_l _ _ b); auto. nzsimpl. order. diff --git a/theories/Numbers/NatInt/NZGcd.v b/theories/Numbers/NatInt/NZGcd.v index 63cc725aec..c542c3fc2c 100644 --- a/theories/Numbers/NatInt/NZGcd.v +++ b/theories/Numbers/NatInt/NZGcd.v @@ -147,7 +147,7 @@ Qed. Lemma mul_divide_cancel_r : forall n m p, p ~= 0 -> ((n * p | m * p) <-> (n | m)). Proof. - intros. rewrite 2 (mul_comm _ p). now apply mul_divide_cancel_l. + intros n m p ?. rewrite 2 (mul_comm _ p). now apply mul_divide_cancel_l. Qed. Lemma divide_add_r : forall n m p, (n | m) -> (n | p) -> (n | m + p). @@ -215,7 +215,7 @@ Qed. Lemma gcd_divide_iff : forall n m p, (p | gcd n m) <-> (p | n) /\ (p | m). Proof. - intros. split. - split. + intros n m p. split. - split. + transitivity (gcd n m); trivial using gcd_divide_l. + transitivity (gcd n m); trivial using gcd_divide_r. - intros (H,H'). now apply gcd_greatest. @@ -273,18 +273,18 @@ Qed. Lemma gcd_eq_0_l : forall n m, gcd n m == 0 -> n == 0. Proof. - intros. + intros n m H. generalize (gcd_divide_l n m). rewrite H. apply divide_0_l. Qed. Lemma gcd_eq_0_r : forall n m, gcd n m == 0 -> m == 0. Proof. - intros. apply gcd_eq_0_l with n. now rewrite gcd_comm. + intros n m ?. apply gcd_eq_0_l with n. now rewrite gcd_comm. Qed. Lemma gcd_eq_0 : forall n m, gcd n m == 0 <-> n == 0 /\ m == 0. Proof. - intros. split. + intros n m. split. - split. + now apply gcd_eq_0_l with m. + now apply gcd_eq_0_r with n. diff --git a/theories/Numbers/NatInt/NZLog.v b/theories/Numbers/NatInt/NZLog.v index 5491d7ab04..526af2f9df 100644 --- a/theories/Numbers/NatInt/NZLog.v +++ b/theories/Numbers/NatInt/NZLog.v @@ -335,7 +335,7 @@ Qed. Lemma log2_succ_or : forall a, log2 (S a) == S (log2 a) \/ log2 (S a) == log2 a. Proof. - intros. + intros a. destruct (le_gt_cases (log2 (S a)) (log2 a)) as [H|H]. - right. generalize (log2_le_mono _ _ (le_succ_diag_r a)); order. - left. apply le_succ_l in H. generalize (log2_succ_le a); order. @@ -601,7 +601,7 @@ Lemma log2_log2_up_exact : Proof. intros a Ha. split. - - intros. exists (log2 a). + - intros H. exists (log2 a). generalize (log2_log2_up_spec a Ha). rewrite <-H. destruct 1; order. - intros (b,Hb). rewrite Hb. @@ -806,8 +806,8 @@ Qed. Lemma log2_up_succ_or : forall a, log2_up (S a) == S (log2_up a) \/ log2_up (S a) == log2_up a. Proof. - intros. - destruct (le_gt_cases (log2_up (S a)) (log2_up a)). + intros a. + destruct (le_gt_cases (log2_up (S a)) (log2_up a)) as [H|H]. - right. generalize (log2_up_le_mono _ _ (le_succ_diag_r a)); order. - left. apply le_succ_l in H. generalize (log2_up_succ_le a); order. Qed. diff --git a/theories/Numbers/NatInt/NZMul.v b/theories/Numbers/NatInt/NZMul.v index 9ddf7cb0eb..3d6465191d 100644 --- a/theories/Numbers/NatInt/NZMul.v +++ b/theories/Numbers/NatInt/NZMul.v @@ -17,7 +17,7 @@ Include NZAddProp NZ NZBase. Theorem mul_0_r : forall n, n * 0 == 0. Proof. -nzinduct n; intros; now nzsimpl. +intro n; nzinduct n; intros; now nzsimpl. Qed. Theorem mul_succ_r : forall n m, n * (S m) == n * m + n. diff --git a/theories/Numbers/NatInt/NZMulOrder.v b/theories/Numbers/NatInt/NZMulOrder.v index 46749504a9..c67bbe38d8 100644 --- a/theories/Numbers/NatInt/NZMulOrder.v +++ b/theories/Numbers/NatInt/NZMulOrder.v @@ -46,7 +46,7 @@ Qed. Theorem mul_lt_mono_neg_l : forall p n m, p < 0 -> (n < m <-> p * m < p * n). Proof. -nzord_induct p. +intro p; nzord_induct p. - order. - intros p Hp _ n m Hp'. apply lt_succ_l in Hp'. order. - intros p Hp IH n m _. apply le_succ_l in Hp. @@ -196,7 +196,7 @@ Qed. Theorem mul_nonneg_nonneg : forall n m, 0 <= n -> 0 <= m -> 0 <= n*m. Proof. -intros. rewrite <- (mul_0_l m). apply mul_le_mono_nonneg; order. +intros n m Hn Hm. rewrite <- (mul_0_l m). apply mul_le_mono_nonneg; order. Qed. Theorem mul_pos_cancel_l : forall n m, 0 < n -> (0 < n*m <-> 0 < m). @@ -343,7 +343,7 @@ Qed. Lemma square_nonneg : forall a, 0 <= a * a. Proof. - intros. rewrite <- (mul_0_r a). destruct (le_gt_cases a 0). + intro a. rewrite <- (mul_0_r a). destruct (le_gt_cases a 0). - now apply mul_le_mono_nonpos_l. - apply mul_le_mono_nonneg_l; order. Qed. @@ -391,7 +391,7 @@ Qed. Lemma quadmul_le_squareadd : forall a b, 0<=a -> 0<=b -> 2*2*a*b <= (a+b)*(a+b). Proof. - intros. + intros a b Ha Hb. nzsimpl'. rewrite !mul_add_distr_l, !mul_add_distr_r. rewrite (add_comm _ (b*b)), add_assoc. diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v index d576902c5c..68bb974c5d 100644 --- a/theories/Numbers/NatInt/NZOrder.v +++ b/theories/Numbers/NatInt/NZOrder.v @@ -65,7 +65,7 @@ Qed. Theorem le_succ_l : forall n m, S n <= m <-> n < m. Proof. -intro n; nzinduct m n. +intros n m; nzinduct m n. - split; intro H. + false_hyp H nle_succ_diag_l. + false_hyp H lt_irrefl. - intro m. rewrite (lt_eq_cases (S n) (S m)), !lt_succ_r, (lt_eq_cases n m), succ_inj_wd. @@ -362,7 +362,7 @@ induction does not go through, so we need to use strong Lemma lt_exists_pred_strong : forall z n m, z < m -> m <= n -> exists k, m == S k /\ z <= k. Proof. -intro z; nzinduct n z. +intros z n; nzinduct n z. - order. - intro n; split; intros IH m H1 H2. + apply le_succ_r in H2. destruct H2 as [H2 | H2]. @@ -373,7 +373,7 @@ Qed. Theorem lt_exists_pred : forall z n, z < n -> exists k, n == S k /\ z <= k. Proof. -intros z n H; apply lt_exists_pred_strong with (z := z) (n := n). +intros z n H; apply (lt_exists_pred_strong z n). - assumption. - apply le_refl. Qed. @@ -428,12 +428,12 @@ Qed. Lemma A'A_right : (forall n, A' n) -> forall n, z <= n -> A n. Proof. -intros H1 n H2. apply H1 with (n := S n); [assumption | apply lt_succ_diag_r]. +intros H1 n H2. apply (H1 (S n)); [assumption | apply lt_succ_diag_r]. Qed. Theorem strong_right_induction: right_step' -> forall n, z <= n -> A n. Proof. -intro RS'; apply A'A_right; unfold A'; nzinduct n z; +intro RS'; apply A'A_right; unfold A'; intro n; nzinduct n z; [apply rbase | apply rs'_rs''; apply RS']. Qed. @@ -504,7 +504,7 @@ Qed. Theorem strong_left_induction: left_step' -> forall n, n <= z -> A n. Proof. -intro LS'; apply A'A_left; unfold A'; nzinduct n (S z); +intro LS'; apply A'A_left; unfold A'; intro n; nzinduct n (S z); [apply lbase | apply ls'_ls''; apply LS']. Qed. @@ -629,8 +629,7 @@ Qed. Theorem lt_wf : well_founded Rlt. Proof. unfold well_founded. -apply strong_right_induction' with (z := z). -- auto with typeclass_instances. +apply (strong_right_induction' _ _ z). - intros n H; constructor; intros y [H1 H2]. apply nle_gt in H2. elim H2. now apply le_trans with z. - intros n H1 H2; constructor; intros m [H3 H4]. now apply H2. @@ -639,8 +638,7 @@ Qed. Theorem gt_wf : well_founded Rgt. Proof. unfold well_founded. -apply strong_left_induction' with (z := z). -- auto with typeclass_instances. +apply (strong_left_induction' _ _ z). - intros n H; constructor; intros y [H1 H2]. apply nle_gt in H2. + elim H2. diff --git a/theories/Numbers/NatInt/NZParity.v b/theories/Numbers/NatInt/NZParity.v index ee6f4014f0..07a33e3f67 100644 --- a/theories/Numbers/NatInt/NZParity.v +++ b/theories/Numbers/NatInt/NZParity.v @@ -47,7 +47,7 @@ Qed. Lemma Even_or_Odd : forall x, Even x \/ Odd x. Proof. - nzinduct x. + intro x; nzinduct x. - left. exists 0. now nzsimpl. - intros x. split; intros [(y,H)|(y,H)]. @@ -86,7 +86,7 @@ Qed. Lemma orb_even_odd : forall n, orb (even n) (odd n) = true. Proof. - intros. + intros n. destruct (Even_or_Odd n) as [H|H]. - rewrite <- even_spec in H. now rewrite H. - rewrite <- odd_spec in H. now rewrite H, orb_true_r. @@ -94,7 +94,7 @@ Qed. Lemma negb_odd : forall n, negb (odd n) = even n. Proof. - intros. + intros n. generalize (Even_or_Odd n) (Even_Odd_False n). rewrite <- even_spec, <- odd_spec. destruct (odd n), (even n) ; simpl; intuition. @@ -188,7 +188,7 @@ Qed. Lemma even_add : forall n m, even (n+m) = Bool.eqb (even n) (even m). Proof. - intros. + intros n m. case_eq (even n); case_eq (even m); rewrite <- ?negb_true_iff, ?negb_even, ?odd_spec, ?even_spec; intros (m',Hm) (n',Hn). @@ -200,7 +200,7 @@ Qed. Lemma odd_add : forall n m, odd (n+m) = xorb (odd n) (odd m). Proof. - intros. rewrite <- !negb_even. rewrite even_add. + intros n m. rewrite <- !negb_even. rewrite even_add. now destruct (even n), (even m). Qed. @@ -208,7 +208,7 @@ Qed. Lemma even_mul : forall n m, even (mul n m) = even n || even m. Proof. - intros. + intros n m. case_eq (even n); simpl; rewrite ?even_spec. - intros (n',Hn). exists (n'*m). now rewrite Hn, mul_assoc. - case_eq (even m); simpl; rewrite ?even_spec. @@ -222,7 +222,7 @@ Qed. Lemma odd_mul : forall n m, odd (mul n m) = odd n && odd m. Proof. - intros. rewrite <- !negb_even. rewrite even_mul. + intros n m. rewrite <- !negb_even. rewrite even_mul. now destruct (even n), (even m). Qed. diff --git a/theories/Numbers/NatInt/NZPow.v b/theories/Numbers/NatInt/NZPow.v index 01a15686e0..3b2a496229 100644 --- a/theories/Numbers/NatInt/NZPow.v +++ b/theories/Numbers/NatInt/NZPow.v @@ -238,7 +238,7 @@ Qed. Lemma pow_le_mono : forall a b c d, 0<a<=c -> b<=d -> a^b <= c^d. Proof. - intros. transitivity (a^d). + intros a b c d ? ?. transitivity (a^d). - apply pow_le_mono_r; intuition order. - apply pow_le_mono_l; intuition order. Qed. diff --git a/theories/Numbers/NatInt/NZSqrt.v b/theories/Numbers/NatInt/NZSqrt.v index 446ed07b53..4122632603 100644 --- a/theories/Numbers/NatInt/NZSqrt.v +++ b/theories/Numbers/NatInt/NZSqrt.v @@ -58,7 +58,7 @@ Qed. Lemma sqrt_nonneg : forall a, 0<=√a. Proof. - intros. destruct (lt_ge_cases a 0) as [Ha|Ha]. + intros a. destruct (lt_ge_cases a 0) as [Ha|Ha]. - now rewrite (sqrt_neg _ Ha). - apply sqrt_spec_nonneg. destruct (sqrt_spec a Ha). order. Qed. @@ -429,7 +429,7 @@ Qed. Lemma sqrt_up_nonneg : forall a, 0<=√°a. Proof. - intros. destruct (le_gt_cases a 0) as [Ha|Ha]. + intros a. destruct (le_gt_cases a 0) as [Ha|Ha]. - now rewrite sqrt_up_eqn0. - rewrite sqrt_up_eqn; trivial. apply le_le_succ_r, sqrt_nonneg. Qed. @@ -527,7 +527,7 @@ Lemma sqrt_sqrt_up_exact : forall a, 0<=a -> (√a == √°a <-> exists b, 0<=b /\ a == b²). Proof. intros a Ha. - split. - intros. exists √a. + split. - intros H. exists √a. split. + apply sqrt_nonneg. + generalize (sqrt_sqrt_up_spec a Ha). rewrite <-H. destruct 1; order. - intros (b & Hb & Hb'). rewrite Hb'. diff --git a/theories/Relations/Operators_Properties.v b/theories/Relations/Operators_Properties.v index 72183f76e6..51be2bd956 100644 --- a/theories/Relations/Operators_Properties.v +++ b/theories/Relations/Operators_Properties.v @@ -54,8 +54,7 @@ Section Properties. Lemma clos_rt_idempotent : inclusion (R*)* R*. Proof. red. - induction 1; auto with sets. - intros. + induction 1 as [x y H|x|x y z H IH H0 IH0]; auto with sets. apply rt_trans with y; auto with sets. Qed. @@ -70,7 +69,7 @@ Section Properties. inclusion (clos_refl_trans R) (clos_refl_sym_trans R). Proof. red. - induction 1; auto with sets. + induction 1 as [x y H|x|x y z H IH H0 IH0]; auto with sets. apply rst_trans with y; auto with sets. Qed. @@ -90,7 +89,7 @@ Section Properties. clos_trans R x z. Proof. induction 1 as [b d H1|b|a b d H1 H2 IH1 IH2]; auto. - intro H. apply t_trans with (y:=d); auto. + intro H. apply (t_trans _ _ _ d); auto. constructor. auto. Qed. @@ -111,7 +110,7 @@ Section Properties. (clos_refl_sym_trans R). Proof. red. - induction 1; auto with sets. + induction 1 as [x y H|x|x y H IH|x y z H IH H0 IH0]; auto with sets. apply rst_trans with y; auto with sets. Qed. @@ -128,7 +127,7 @@ Section Properties. Lemma clos_t1n_trans : forall x y, clos_trans_1n R x y -> clos_trans R x y. Proof. - induction 1. + induction 1 as [x y H|x y z H H0 IH0]. - left; assumption. - right with y; auto. left; auto. @@ -136,9 +135,10 @@ Section Properties. Lemma clos_trans_t1n : forall x y, clos_trans R x y -> clos_trans_1n R x y. Proof. - induction 1. + induction 1 as [x y H|x y z H IHclos_trans1 H0 IHclos_trans2]. - left; assumption. - - generalize IHclos_trans2; clear IHclos_trans2; induction IHclos_trans1. + - generalize IHclos_trans2; clear IHclos_trans2. + induction IHclos_trans1 as [x y H1|x y z0 H1 ? IHIHclos_trans1]. + right with y; auto. + right with y; auto. eapply IHIHclos_trans1; auto. @@ -157,7 +157,7 @@ Section Properties. Lemma clos_tn1_trans : forall x y, clos_trans_n1 R x y -> clos_trans R x y. Proof. - induction 1. + induction 1 as [y H|y z H H0 ?]. - left; assumption. - right with y; auto. left; assumption. @@ -165,13 +165,13 @@ Section Properties. Lemma clos_trans_tn1 : forall x y, clos_trans R x y -> clos_trans_n1 R x y. Proof. - induction 1. + induction 1 as [x y H|x y z H IHclos_trans1 H0 IHclos_trans2]. - left; assumption. - elim IHclos_trans2. + intro y0; right with y. * auto. * auto. - + intros. + + intro y0; intros. right with y0; auto. Qed. @@ -201,7 +201,7 @@ Section Properties. Lemma clos_rt1n_rt : forall x y, clos_refl_trans_1n R x y -> clos_refl_trans R x y. Proof. - induction 1. + induction 1 as [|x y z]. - constructor 2. - constructor 3 with y; auto. constructor 1; auto. @@ -210,14 +210,14 @@ Section Properties. Lemma clos_rt_rt1n : forall x y, clos_refl_trans R x y -> clos_refl_trans_1n R x y. Proof. - induction 1. + induction 1 as [| |x y z H IHclos_refl_trans1 H0 IHclos_refl_trans2]. - apply clos_rt1n_step; assumption. - left. - generalize IHclos_refl_trans2; clear IHclos_refl_trans2; - induction IHclos_refl_trans1; auto. + induction IHclos_refl_trans1 as [|x y z0 H1 ? IH]; auto. right with y; auto. - eapply IHIHclos_refl_trans1; auto. + eapply IH; auto. apply clos_rt1n_rt; auto. Qed. @@ -235,7 +235,7 @@ Section Properties. Lemma clos_rtn1_rt : forall x y, clos_refl_trans_n1 R x y -> clos_refl_trans R x y. Proof. - induction 1. + induction 1 as [|y z]. - constructor 2. - constructor 3 with y; auto. constructor 1; assumption. @@ -244,11 +244,11 @@ Section Properties. Lemma clos_rt_rtn1 : forall x y, clos_refl_trans R x y -> clos_refl_trans_n1 R x y. Proof. - induction 1. + induction 1 as [| |x y z H1 IH1 H2 IH2]. - apply clos_rtn1_step; auto. - left. - - elim IHclos_refl_trans2; auto. - intros. + - elim IH2; auto. + intro y0; intros. right with y0; auto. Qed. @@ -267,16 +267,16 @@ Section Properties. (forall y z:A, clos_refl_trans R x y -> P y -> R y z -> P z) -> forall z:A, clos_refl_trans R x z -> P z. Proof. - intros. + intros x P H H0 z H1. revert H H0. - induction H1; intros; auto with sets. - - apply H1 with x; auto with sets. + induction H1 as [x| |x y z H1 IH1 H2 IH2]; intros HP HIS; auto with sets. + - apply HIS with x; auto with sets. - - apply IHclos_refl_trans2. - + apply IHclos_refl_trans1; auto with sets. + - apply IH2. + + apply IH1; auto with sets. - + intros. - apply H0 with y0; auto with sets. + + intro y0; intros; + apply HIS with y0; auto with sets. apply rt_trans with y; auto with sets. Qed. @@ -286,7 +286,7 @@ Section Properties. P z -> (forall x y, R x y -> clos_refl_trans_1n R y z -> P y -> P x) -> forall x, clos_refl_trans_1n R x z -> P x. - induction 3; auto. + intros P z H H0 x; induction 1 as [|x y z]; auto. apply H0 with y; auto. Qed. @@ -309,7 +309,7 @@ Section Properties. Lemma clos_rst1n_rst : forall x y, clos_refl_sym_trans_1n R x y -> clos_refl_sym_trans R x y. Proof. - induction 1. + induction 1 as [|x y z H]. - constructor 2. - constructor 4 with y; auto. case H;[constructor 1|constructor 3; constructor 1]; auto. @@ -317,7 +317,7 @@ Section Properties. Lemma clos_rst1n_trans : forall x y z, clos_refl_sym_trans_1n R x y -> clos_refl_sym_trans_1n R y z -> clos_refl_sym_trans_1n R x z. - induction 1. + induction 1 as [|x y z0]. - auto. - intros; right with y; eauto. Qed. @@ -335,7 +335,7 @@ Section Properties. Lemma clos_rst_rst1n : forall x y, clos_refl_sym_trans R x y -> clos_refl_sym_trans_1n R x y. - induction 1. + induction 1 as [x y| | |]. - constructor 2 with y; auto. constructor 1. - constructor 1. @@ -357,7 +357,7 @@ Section Properties. Lemma clos_rstn1_rst : forall x y, clos_refl_sym_trans_n1 R x y -> clos_refl_sym_trans R x y. Proof. - induction 1. + induction 1 as [|y z H]. - constructor 2. - constructor 4 with y; auto. case H;[constructor 1|constructor 3; constructor 1]; auto. @@ -367,10 +367,9 @@ Section Properties. clos_refl_sym_trans_n1 R y z -> clos_refl_sym_trans_n1 R x z. Proof. intros x y z H1 H2. - induction H2. + induction H2 as [|y0 z]. - auto. - - intros. - right with y0; eauto. + - right with y0; eauto. Qed. Lemma clos_rstn1_sym : forall x y, clos_refl_sym_trans_n1 R x y -> @@ -387,7 +386,7 @@ Section Properties. Lemma clos_rst_rstn1 : forall x y, clos_refl_sym_trans R x y -> clos_refl_sym_trans_n1 R x y. Proof. - induction 1. + induction 1 as [x| | |]. - constructor 2 with x; auto. constructor 1. - constructor 1. diff --git a/theories/Relations/Relations.v b/theories/Relations/Relations.v index 0a5128f093..dea76694f3 100644 --- a/theories/Relations/Relations.v +++ b/theories/Relations/Relations.v @@ -16,16 +16,16 @@ Lemma inverse_image_of_equivalence : forall (A B:Type) (f:A -> B) (r:relation B), equivalence B r -> equivalence A (fun x y:A => r (f x) (f y)). Proof. - intros; split; elim H; red; auto. + intros A B f r H; split; elim H; red; auto. intros _ equiv_trans _ x y z H0 H1; apply equiv_trans with (f y); assumption. Qed. Lemma inverse_image_of_eq : forall (A B:Type) (f:A -> B), equivalence A (fun x y:A => f x = f y). Proof. - split; red; + intros A B f; split; red; [ (* reflexivity *) reflexivity - | (* transitivity *) intros; transitivity (f y); assumption + | (* transitivity *) intros x y z; transitivity (f y); assumption | (* symmetry *) intros; symmetry ; assumption ]. Qed. diff --git a/theories/Setoids/Setoid.v b/theories/Setoids/Setoid.v index b10c4f3768..cec1033fdf 100644 --- a/theories/Setoids/Setoid.v +++ b/theories/Setoids/Setoid.v @@ -33,7 +33,7 @@ Defined. Definition Seq_trans A Aeq (s : Setoid_Theory A Aeq) : forall x y z:A, Aeq x y -> Aeq y z -> Aeq x z. Proof. - unfold Setoid_Theory in s. intros ; transitivity y ; assumption. + unfold Setoid_Theory in s. intros x y z H0 H1 ; transitivity y ; assumption. Defined. (** Some tactics for manipulating Setoid Theory not officially diff --git a/theories/Structures/GenericMinMax.v b/theories/Structures/GenericMinMax.v index 8d20ce77f9..1af6aebec6 100644 --- a/theories/Structures/GenericMinMax.v +++ b/theories/Structures/GenericMinMax.v @@ -629,9 +629,9 @@ Module TOMaxEqDec_to_Compare if eq_dec x y then Eq else if eq_dec (M.max x y) y then Lt else Gt. - Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y). + Lemma compare_spec x y : CompSpec eq lt x y (compare x y). Proof. - intros; unfold compare; repeat destruct eq_dec; auto; constructor. + unfold compare; repeat destruct eq_dec; auto; constructor. - destruct (lt_total x y); auto. absurd (x==y); auto. transitivity (max x y); auto. symmetry. apply max_l. rewrite le_lteq; intuition. diff --git a/theories/Structures/Orders.v b/theories/Structures/Orders.v index 94938c1d4d..b3e3b6e853 100644 --- a/theories/Structures/Orders.v +++ b/theories/Structures/Orders.v @@ -165,7 +165,7 @@ End OT_to_Full. Module OTF_LtIsTotal (Import O:OrderedTypeFull') <: LtIsTotal O. Lemma lt_total : forall x y, x<y \/ x==y \/ y<x. - Proof. intros; destruct (compare_spec x y); auto. Qed. + Proof. intros x y; destruct (compare_spec x y); auto. Qed. End OTF_LtIsTotal. Module OTF_to_TotalOrder (O:OrderedTypeFull) <: TotalOrder @@ -250,7 +250,7 @@ Module OTF_to_TTLB (Import O : OrderedTypeFull') <: TotalTransitiveLeBool. Lemma leb_le : forall x y, leb x y <-> x <= y. Proof. - intros. unfold leb. rewrite le_lteq. + intros x y. unfold leb. rewrite le_lteq. destruct (compare_spec x y) as [EQ|LT|GT]; split; auto. - discriminate. - intros LE. elim (StrictOrder_Irreflexive x). @@ -261,7 +261,7 @@ Module OTF_to_TTLB (Import O : OrderedTypeFull') <: TotalTransitiveLeBool. Lemma leb_total : forall x y, leb x y \/ leb y x. Proof. - intros. rewrite 2 leb_le. rewrite 2 le_lteq. + intros x y. rewrite 2 leb_le. rewrite 2 le_lteq. destruct (compare_spec x y); intuition. Qed. @@ -302,7 +302,7 @@ Module TTLB_to_OTF (Import O : TotalTransitiveLeBool') <: OrderedTypeFull. Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y). Proof. - intros. unfold compare. + intros x y. unfold compare. case_eq (x <=? y). - case_eq (y <=? x). + constructor. split; auto. @@ -352,7 +352,7 @@ Module TTLB_to_OTF (Import O : TotalTransitiveLeBool') <: OrderedTypeFull. Definition le_lteq : forall x y, le x y <-> lt x y \/ eq x y. Proof. - intros. + intros x y. unfold lt, eq, le. split; [ | intuition ]. intros LE. diff --git a/theories/Structures/OrdersFacts.v b/theories/Structures/OrdersFacts.v index d5a76ee69f..4ac54d280a 100644 --- a/theories/Structures/OrdersFacts.v +++ b/theories/Structures/OrdersFacts.v @@ -102,10 +102,10 @@ Module OrderedTypeFullFacts (Import O:OrderedTypeFull'). Proof. iorder. Qed. Lemma le_or_gt : forall x y, x<=y \/ y<x. - Proof. intros. rewrite le_lteq; destruct (O.compare_spec x y); auto. Qed. + Proof. intros x y. rewrite le_lteq; destruct (O.compare_spec x y); auto. Qed. Lemma lt_or_ge : forall x y, x<y \/ y<=x. - Proof. intros. rewrite le_lteq; destruct (O.compare_spec x y); iorder. Qed. + Proof. intros x y. rewrite le_lteq; destruct (O.compare_spec x y); iorder. Qed. Lemma eq_is_le_ge : forall x y, x==y <-> x<=y /\ y<=x. Proof. iorder. Qed. @@ -175,11 +175,11 @@ Module OrderedTypeFacts (Import O: OrderedType'). Definition eqb x y : bool := if eq_dec x y then true else false. - Lemma if_eq_dec : forall x y (B:Type)(b b':B), + Lemma if_eq_dec x y (B:Type)(b b':B) : (if eq_dec x y then b else b') = (match compare x y with Eq => b | _ => b' end). Proof. - intros; destruct eq_dec; elim_compare x y; auto; order. + destruct eq_dec; elim_compare x y; auto; order. Qed. Lemma eqb_alt : @@ -257,7 +257,7 @@ Definition compare := flip O.compare. Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y). Proof. -intros; unfold compare, eq, lt, flip. +intros x y; unfold compare, eq, lt, flip. destruct (O.compare_spec y x); auto with relations. Qed. diff --git a/theories/Structures/OrdersTac.v b/theories/Structures/OrdersTac.v index 408348139d..1c8073972d 100644 --- a/theories/Structures/OrdersTac.v +++ b/theories/Structures/OrdersTac.v @@ -100,9 +100,9 @@ Definition interp_ord o := match o with OEQ => O.eq | OLT => O.lt | OLE => O.le end. Local Notation "#" := interp_ord. -Lemma trans : forall o o' x y z, #o x y -> #o' y z -> #(o+o') x z. +Lemma trans o o' x y z : #o x y -> #o' y z -> #(o+o') x z. Proof. -destruct o, o'; simpl; intros x y z; +destruct o, o'; simpl; rewrite ?P.le_lteq; intuition auto; subst_eqns; eauto using (StrictOrder_Transitive x y z) with *. Qed. diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index 0f34adf1c7..564d24c1ea 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -247,6 +247,7 @@ let interp_fixpoint ?(check_recursivity=true) ~cofix l : (EConstr.rel_context * Impargs.manual_implicits * int option) list) = let (env,_,pl,evd),fix,info = interp_recursive ~program_mode:false ~cofix l in if check_recursivity then check_recursive true env evd fix; + let evd = Pretyping.(solve_remaining_evars all_no_fail_flags env evd) in let uctx,fix = ground_fixpoint env evd fix in (fix,pl,uctx,info) diff --git a/vernac/proof_using.ml b/vernac/proof_using.ml index 2130a398e9..95680c2a4e 100644 --- a/vernac/proof_using.ml +++ b/vernac/proof_using.ml @@ -41,28 +41,27 @@ let set_of_type env ty = let full_set env = List.fold_right Id.Set.add (List.map NamedDecl.get_id (named_context env)) Id.Set.empty -let rec process_expr env e ty = +let process_expr env e v_ty = let rec aux = function | SsEmpty -> Id.Set.empty - | SsType -> set_of_type env ty - | SsSingl { CAst.v = id } -> set_of_id env id + | SsType -> v_ty + | SsSingl { CAst.v = id } -> set_of_id id | SsUnion(e1,e2) -> Id.Set.union (aux e1) (aux e2) | SsSubstr(e1,e2) -> Id.Set.diff (aux e1) (aux e2) | SsCompl e -> Id.Set.diff (full_set env) (aux e) | SsFwdClose e -> close_fwd env (aux e) + and set_of_id id = + if Id.to_string id = "All" then + full_set env + else if CList.mem_assoc_f Id.equal id !known_names then + aux (CList.assoc_f Id.equal id !known_names) + else Id.Set.singleton id in - aux e - -and set_of_id env id = - if Id.to_string id = "All" then - List.fold_right Id.Set.add (List.map NamedDecl.get_id (named_context env)) Id.Set.empty - else if CList.mem_assoc_f Id.equal id !known_names then - process_expr env (CList.assoc_f Id.equal id !known_names) [] - else Id.Set.singleton id + aux e let process_expr env e ty = let v_ty = set_of_type env ty in - let s = Id.Set.union v_ty (process_expr env e ty) in + let s = Id.Set.union v_ty (process_expr env e v_ty) in Id.Set.elements s let name_set id expr = known_names := (id,expr) :: !known_names |