diff options
44 files changed, 284 insertions, 235 deletions
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/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/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/tactics.ml b/tactics/tactics.ml index 1dded80d92..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 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/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/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 |