diff options
32 files changed, 163 insertions, 108 deletions
@@ -30,6 +30,11 @@ Tactics - New tactics is_ind, is_const, is_proj, is_constructor for use in Ltac (DOC TODO). - New goal selectors. Sets of goals can be selected by select by listing integers ranges. Example: "1,4-7,24: tac" focuses "tac" on goals 1,4,5,6,7,24. +- For uniformity with "destruct"/"induction" and for a more natural + behavior, "injection" can now work in place by activating option + "Structural Injection". In this case, hypotheses are also put in the + context in the natural left-to-right order and the hypothesis on + which injection applies is cleared. Hints diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4 index 60ce59ed92..725f2a5342 100644 --- a/ltac/extratactics.ml4 +++ b/ltac/extratactics.ml4 @@ -144,6 +144,10 @@ TACTIC EXTEND einjection_as | [ "einjection" destruction_arg(c) "as" intropattern_list(ipat)] -> [ mytclWithHoles (injClause (Some ipat)) true c ] END +TACTIC EXTEND simple_injection +| [ "simple" "injection" ] -> [ simpleInjClause false None ] +| [ "simple" "injection" destruction_arg(c) ] -> [ mytclWithHoles simpleInjClause false c ] +END let injHyp id = Proofview.tclEVARMAP >>= fun sigma -> diff --git a/plugins/micromega/EnvRing.v b/plugins/micromega/EnvRing.v index fd4bb248bf..904ee4dac1 100644 --- a/plugins/micromega/EnvRing.v +++ b/plugins/micromega/EnvRing.v @@ -914,7 +914,7 @@ Qed. revert P1. induction LM1 as [|(M2,P2') LM2 IH]; simpl; intros. - discriminate. - assert (H':=PNSubst_ok n P3 M2 P2'). destruct PNSubst. - * injection H; intros <-. rewrite <- PSubstL1_ok; intuition. + * injection H as <-. rewrite <- PSubstL1_ok; intuition. * now apply IH. Qed. diff --git a/plugins/rtauto/Bintree.v b/plugins/rtauto/Bintree.v index 7394cebdef..3646018719 100644 --- a/plugins/rtauto/Bintree.v +++ b/plugins/rtauto/Bintree.v @@ -266,7 +266,7 @@ Qed. Lemma push_not_empty: forall a S, (push a S) <> empty. intros a [ind cont];unfold push,empty. -simpl;intro H;injection H; intros _ ; apply Pos.succ_not_1. +intros [= H%Pos.succ_not_1]. assumption. Qed. Fixpoint In (x:A) (S:Store) (F:Full S) {struct F}: Prop := diff --git a/plugins/setoid_ring/InitialRing.v b/plugins/setoid_ring/InitialRing.v index 8fcc077164..9c690e2b4a 100644 --- a/plugins/setoid_ring/InitialRing.v +++ b/plugins/setoid_ring/InitialRing.v @@ -96,7 +96,7 @@ Section ZMORPHISM. Proof. constructor. destruct c;intros;try discriminate. - injection H;clear H;intros H1;subst c'. + injection H as <-. simpl. unfold Zeq_bool. rewrite Z.compare_refl. trivial. Qed. diff --git a/plugins/setoid_ring/Ring_polynom.v b/plugins/setoid_ring/Ring_polynom.v index 760ad4da11..b69196679f 100644 --- a/plugins/setoid_ring/Ring_polynom.v +++ b/plugins/setoid_ring/Ring_polynom.v @@ -883,7 +883,7 @@ Section MakeRingPol. revert P1. induction LM1 as [|(M2,P2') LM2 IH]; simpl; intros. - discriminate. - assert (H':=PNSubst_ok n P3 M2 P2'). destruct PNSubst. - * injection H; intros <-. rewrite <- PSubstL1_ok; intuition. + * injection H as <-. rewrite <- PSubstL1_ok; intuition. * now apply IH. Qed. diff --git a/tactics/equality.ml b/tactics/equality.ml index db7d2e4a13..1d3239ef68 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -72,11 +72,26 @@ let _ = declare_bool_option { optsync = true; optdepr = false; - optname = "injection left-to-right pattern order"; + optname = "injection left-to-right pattern order and clear by default when with introduction pattern"; optkey = ["Injection";"L2R";"Pattern";"Order"]; optread = (fun () -> !injection_pattern_l2r_order) ; optwrite = (fun b -> injection_pattern_l2r_order := b) } +let injection_in_context = ref false + +let use_injection_in_context () = + !injection_in_context + && Flags.version_strictly_greater Flags.V8_5 + +let _ = + declare_bool_option + { optsync = true; + optdepr = false; + optname = "injection in context"; + optkey = ["Structural";"Injection"]; + optread = (fun () -> !injection_in_context) ; + optwrite = (fun b -> injection_in_context := b) } + (* Rewriting tactics *) let tclNOTSAMEGOAL tac = @@ -1381,27 +1396,41 @@ let injEqThen tac l2r (eq,_,(t,t1,t2) as u) eq_clause = inject_at_positions env sigma l2r u eq_clause posns (tac (clenv_value eq_clause)) -let use_clear_hyp_by_default () = false - -let postInjEqTac with_evars clear_flag ipats c n = - match ipats with - | Some ipats -> - let clear_tac = - let dft = - use_injection_pattern_l2r_order () || use_clear_hyp_by_default () in - tclTRY (apply_clear_request clear_flag dft c) in - let intro_tac = - if use_injection_pattern_l2r_order () - then intro_patterns_bound_to with_evars n MoveLast ipats - else intro_patterns_to with_evars MoveLast ipats in - tclTHEN clear_tac intro_tac - | None -> apply_clear_request clear_flag false c - -let injEq with_evars clear_flag ipats = - let l2r = - if use_injection_pattern_l2r_order () && not (Option.is_empty ipats) then true else false +let get_previous_hyp_position id gl = + let rec aux dest = function + | [] -> raise (RefinerError (NoSuchHyp id)) + | d :: right -> + let hyp = Context.Named.Declaration.get_id d in + if Id.equal hyp id then dest else aux (MoveAfter hyp) right in - injEqThen (fun c i -> postInjEqTac with_evars clear_flag ipats c i) l2r + aux MoveLast (Proofview.Goal.hyps (Proofview.Goal.assume gl)) + +let injEq ?(old=false) with_evars clear_flag ipats = + (* Decide which compatibility mode to use *) + let ipats_style, l2r, dft_clear_flag, bounded_intro = match ipats with + | None when not old && use_injection_in_context () -> + Some [], true, true, true + | None -> None, false, false, false + | _ -> let b = use_injection_pattern_l2r_order () in ipats, b, b, b in + (* Built the post tactic depending on compatibility mode *) + let post_tac c n = + match ipats_style with + | Some ipats -> + Proofview.Goal.enter { enter = begin fun gl -> + let destopt = match kind_of_term c with + | Var id -> get_previous_hyp_position id gl + | _ -> MoveLast in + let clear_tac = + tclTRY (apply_clear_request clear_flag dft_clear_flag c) in + (* Try should be removal if dependency were treated *) + let intro_tac = + if bounded_intro + then intro_patterns_bound_to with_evars n destopt ipats + else intro_patterns_to with_evars destopt ipats in + tclTHEN clear_tac intro_tac + end } + | None -> tclIDTAC in + injEqThen post_tac l2r let inj ipats with_evars clear_flag = onEquality with_evars (injEq with_evars clear_flag ipats) @@ -1409,6 +1438,10 @@ let injClause ipats with_evars = function | None -> onNegatedEquality with_evars (injEq with_evars None ipats) | Some c -> onInductionArg (inj ipats with_evars) c +let simpleInjClause with_evars = function + | None -> onNegatedEquality with_evars (injEq ~old:true with_evars None None) + | Some c -> onInductionArg (fun clear_flag -> onEquality with_evars (injEq ~old:true with_evars clear_flag None)) c + let injConcl = injClause None false None let injHyp clear_flag id = injClause None false (Some (clear_flag,ElimOnIdent (Loc.ghost,id))) diff --git a/tactics/equality.mli b/tactics/equality.mli index 1122615c3d..47cb6b82fd 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -79,6 +79,8 @@ val injClause : intro_patterns option -> evars_flag -> constr with_bindings destruction_arg option -> unit Proofview.tactic val injHyp : clear_flag -> Id.t -> unit Proofview.tactic val injConcl : unit Proofview.tactic +val simpleInjClause : evars_flag -> + constr with_bindings destruction_arg option -> unit Proofview.tactic val dEq : evars_flag -> constr with_bindings destruction_arg option -> unit Proofview.tactic val dEqThen : evars_flag -> (clear_flag -> constr -> int -> unit Proofview.tactic) -> constr with_bindings destruction_arg option -> unit Proofview.tactic diff --git a/test-suite/bugs/closed/2016.v b/test-suite/bugs/closed/2016.v index 13ec5bea9b..536e6fabd9 100644 --- a/test-suite/bugs/closed/2016.v +++ b/test-suite/bugs/closed/2016.v @@ -1,6 +1,8 @@ (* Coq 8.2beta4 *) Require Import Classical_Prop. +Unset Structural Injection. + Record coreSemantics : Type := CoreSemantics { core: Type; corestep: core -> core -> Prop; @@ -49,7 +51,7 @@ unfold oe_corestep; intros. assert (HH:= step_fun _ _ _ H H0); clear H H0. destruct q1; destruct q2; unfold oe2coreSem; simpl in *. generalize (inj_pairT1 _ _ _ _ _ _ HH); clear HH; intros. -injection H; clear H; intros. +injection H. revert in_q1 in_corestep1 in_corestep_fun1 H. pattern in_core1. @@ -59,4 +61,4 @@ apply sym_eq. (** good to here **) Show Universes. Print Universes. -Fail apply H0.
\ No newline at end of file +Fail apply H0. diff --git a/test-suite/bugs/closed/2021.v b/test-suite/bugs/closed/2021.v index e598e5aed7..5df92998e1 100644 --- a/test-suite/bugs/closed/2021.v +++ b/test-suite/bugs/closed/2021.v @@ -1,6 +1,8 @@ (* correct failure of injection/discriminate on types whose inductive status derives from the substitution of an argument *) +Unset Structural Injection. + Inductive t : nat -> Type := | M : forall n: nat, nat -> t n. diff --git a/test-suite/bugs/closed/HoTT_coq_047.v b/test-suite/bugs/closed/HoTT_coq_047.v index 29496be5ee..bef3c33ca1 100644 --- a/test-suite/bugs/closed/HoTT_coq_047.v +++ b/test-suite/bugs/closed/HoTT_coq_047.v @@ -1,3 +1,5 @@ +Unset Structural Injection. + Inductive nCk : nat -> nat -> Type := |zz : nCk 0 0 | incl { m n : nat } : nCk m n -> nCk (S m) (S n) diff --git a/test-suite/success/Injection.v b/test-suite/success/Injection.v index c072cc6417..8745cf2fbd 100644 --- a/test-suite/success/Injection.v +++ b/test-suite/success/Injection.v @@ -4,6 +4,7 @@ Require Eqdep_dec. (* Check that Injection tries Intro until *) +Unset Structural Injection. Lemma l1 : forall x : nat, S x = S (S x) -> False. injection 1. apply n_Sn. @@ -37,6 +38,7 @@ intros. injection H. exact (fun H => H). Qed. +Set Structural Injection. (* Test injection as *) @@ -65,7 +67,7 @@ Qed. Goal (forall x y : nat, x = y -> S x = S y) -> True. intros. einjection (H O). -instantiate (1:=O). +2:instantiate (1:=O). Abort. Goal (forall x y : nat, x = y -> S x = S y) -> True. @@ -85,12 +87,21 @@ Qed. (* Basic case, using sigT *) Scheme Equality for nat. +Unset Structural Injection. Goal forall n:nat, forall P:nat -> Type, forall H1 H2:P n, existT P n H1 = existT P n H2 -> H1 = H2. intros. injection H. intro H0. exact H0. Abort. +Set Structural Injection. + +Goal forall n:nat, forall P:nat -> Type, forall H1 H2:P n, + existT P n H1 = existT P n H2 -> H1 = H2. +intros. +injection H as H0. +exact H0. +Abort. (* Test injection using K, knowing that an equality is decidable *) (* Basic case, using sigT, with "as" clause *) diff --git a/test-suite/success/RecTutorial.v b/test-suite/success/RecTutorial.v index 11fbf24d4d..3f8a7f3eb6 100644 --- a/test-suite/success/RecTutorial.v +++ b/test-suite/success/RecTutorial.v @@ -831,7 +831,7 @@ Proof. intro n. apply nat_ind with (P:= fun n => n <> S n). discriminate. - red; intros n0 Hn0 eqn0Sn0;injection eqn0Sn0;trivial. + red; intros n0 Hn0 eqn0Sn0;injection eqn0Sn0;auto. Qed. Definition eq_nat_dec : forall n p:nat , {n=p}+{n <> p}. @@ -1076,7 +1076,7 @@ Proof. simpl. destruct i; discriminate 1. destruct i; simpl;auto. - injection 1; injection 2;intros; subst a; subst b; auto. + injection 1; injection 1; subst a; subst b; auto. Qed. Set Implicit Arguments. diff --git a/theories/Arith/Peano_dec.v b/theories/Arith/Peano_dec.v index 340a796891..f8020a50e0 100644 --- a/theories/Arith/Peano_dec.v +++ b/theories/Arith/Peano_dec.v @@ -38,8 +38,7 @@ intros m n. generalize (eq_refl (S n)). generalize n at -1. induction (S n) as [|n0 IHn0]; try discriminate. -clear n; intros n H; injection H; clear H; intro H. -rewrite <- H; intros le_mn1 le_mn2; clear n H. +clear n; intros n [= <-] le_mn1 le_mn2. pose (def_n2 := eq_refl n0); transitivity (eq_ind _ _ le_mn2 _ def_n2). 2: reflexivity. generalize def_n2; revert le_mn1 le_mn2. @@ -50,7 +49,7 @@ destruct le_mn1; intros le_mn2; destruct le_mn2. now destruct (Nat.nle_succ_diag_l _ le_mn0). + intros def_n0; generalize le_mn1; rewrite def_n0; intros le_mn0. now destruct (Nat.nle_succ_diag_l _ le_mn0). -+ intros def_n0; injection def_n0; intros ->. ++ intros def_n0. injection def_n0 as ->. rewrite (UIP_nat _ _ def_n0 eq_refl); simpl. assert (H : le_mn1 = le_mn2). now apply IHn0. diff --git a/theories/Compat/Coq85.v b/theories/Compat/Coq85.v index 3fc74943e1..d6d370cb51 100644 --- a/theories/Compat/Coq85.v +++ b/theories/Compat/Coq85.v @@ -14,3 +14,4 @@ Global Unset Bracketing Last Introduction Pattern. Global Unset Regular Subst Tactic. +Global Unset Structural Injection. diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v index eaeb2914b3..9a227ad130 100644 --- a/theories/FSets/FMapFacts.v +++ b/theories/FSets/FMapFacts.v @@ -1986,7 +1986,7 @@ Module OrdProperties (M:S). simpl; intros; try discriminate. intros. destruct a; destruct l; simpl in *. - injection H; clear H; intros; subst. + injection H as -> ->. inversion_clear H1. red in H; simpl in *; intuition. elim H0; eauto. @@ -2050,10 +2050,10 @@ Module OrdProperties (M:S). generalize (elements_3 m). destruct (elements m). try discriminate. - destruct p; injection H; intros; subst. - inversion_clear H1. + destruct p; injection H as -> ->; intros H4. + inversion_clear H1 as [? ? H2|? ? H2]. red in H2; destruct H2; simpl in *; ME.order. - inversion_clear H4. + inversion_clear H4. rename H1 into H3. rewrite (@InfA_alt _ eqke) in H3; eauto with *. apply (H3 (y,x0)); auto. Qed. diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v index 9e59f0c505..b1c0fdaa2f 100644 --- a/theories/FSets/FMapPositive.v +++ b/theories/FSets/FMapPositive.v @@ -274,8 +274,8 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. rewrite append_assoc_1; apply in_or_app; right; apply in_cons; apply IHm2; auto. rewrite append_assoc_0; apply in_or_app; left; apply IHm1; auto. - rewrite append_neutral_r; apply in_or_app; injection H; - intro EQ; rewrite EQ; right; apply in_eq. + rewrite append_neutral_r; apply in_or_app; injection H as ->; + right; apply in_eq. rewrite append_assoc_1; apply in_or_app; right; apply IHm2; auto. rewrite append_assoc_0; apply in_or_app; left; apply IHm1; auto. congruence. @@ -315,7 +315,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. apply in_or_app. left; apply IHm1; auto. right; destruct (in_inv H0). - injection H1; intros Eq1 Eq2; rewrite Eq1; rewrite Eq2; apply in_eq. + injection H1 as -> ->; apply in_eq. apply in_cons; apply IHm2; auto. left; apply IHm1; auto. right; apply IHm2; auto. @@ -346,7 +346,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. apply in_or_app. left; apply IHm1; auto. right; destruct (in_inv H0). - injection H1; intros Eq1 Eq2; rewrite Eq1; rewrite Eq2; apply in_eq. + injection H1 as -> ->; apply in_eq. apply in_cons; apply IHm2; auto. left; apply IHm1; auto. right; apply IHm2; auto. @@ -689,7 +689,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. destruct y2; destruct y0; compute in Hy2; destruct Hy2; subst. red; red; simpl. destruct H0. - injection H0; clear H0; intros _ H0; subst. + injection H0 as H0 _; subst. eapply xelements_bits_lt_1; eauto. apply E.bits_lt_trans with p. eapply xelements_bits_lt_1; eauto. diff --git a/theories/FSets/FSetPositive.v b/theories/FSets/FSetPositive.v index 7398c6d654..507f1cda69 100644 --- a/theories/FSets/FSetPositive.v +++ b/theories/FSets/FSetPositive.v @@ -1007,10 +1007,10 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. destruct o. intros x H. injection H; intros; subst. reflexivity. revert IHl. case choose. - intros p Hp x H. injection H; intros; subst; clear H. apply Hp. + intros p Hp x H. injection H as <-. apply Hp. reflexivity. intros _ x. revert IHr. case choose. - intros p Hp H. injection H; intros; subst; clear H. apply Hp. + intros p Hp H. injection H as <-. apply Hp. reflexivity. intros. discriminate. Qed. @@ -1066,11 +1066,11 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. induction s as [| l IHl o r IHr]; simpl. intros. discriminate. intros x. destruct (min_elt l); intros. - injection H. intros <-. apply IHl. reflexivity. + injection H as <-. apply IHl. reflexivity. destruct o; simpl. - injection H. intros <-. reflexivity. + injection H as <-. reflexivity. destruct (min_elt r); simpl in *. - injection H. intros <-. apply IHr. reflexivity. + injection H as <-. apply IHr. reflexivity. discriminate. Qed. @@ -1094,15 +1094,15 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. induction s as [|l IHl o r IHr]; intros x y H H'. discriminate. simpl in H. case_eq (min_elt l). - intros p Hp. rewrite Hp in H. injection H; intros <-. + intros p Hp. rewrite Hp in H. injection H as <-. destruct y as [z|z|]; simpl; intro; trivial. apply (IHl p z); trivial. intro Hp; rewrite Hp in H. apply min_elt_3 in Hp. destruct o. - injection H. intros <- Hl. clear H. + injection H as <-. intros Hl. destruct y as [z|z|]; simpl; trivial. elim (Hp _ H'). destruct (min_elt r). - injection H. intros <-. clear H. + injection H as <-. destruct y as [z|z|]. apply (IHr e z); trivial. elim (Hp _ H'). @@ -1119,11 +1119,11 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. induction s as [| l IHl o r IHr]; simpl. intros. discriminate. intros x. destruct (max_elt r); intros. - injection H. intros <-. apply IHr. reflexivity. + injection H as <-. apply IHr. reflexivity. destruct o; simpl. - injection H. intros <-. reflexivity. + injection H as <-. reflexivity. destruct (max_elt l); simpl in *. - injection H. intros <-. apply IHl. reflexivity. + injection H as <-. apply IHl. reflexivity. discriminate. Qed. @@ -1147,15 +1147,15 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. induction s as [|l IHl o r IHr]; intros x y H H'. discriminate. simpl in H. case_eq (max_elt r). - intros p Hp. rewrite Hp in H. injection H; intros <-. + intros p Hp. rewrite Hp in H. injection H as <-. destruct y as [z|z|]; simpl; intro; trivial. apply (IHr p z); trivial. intro Hp; rewrite Hp in H. apply max_elt_3 in Hp. destruct o. - injection H. intros <- Hl. clear H. + injection H as <-. intros Hl. destruct y as [z|z|]; simpl; trivial. elim (Hp _ H'). destruct (max_elt l). - injection H. intros <-. clear H. + injection H as <-. destruct y as [z|z|]. elim (Hp _ H'). apply (IHl e z); trivial. diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v index 59fdbb42f0..a3eb91ec65 100644 --- a/theories/Init/Tactics.v +++ b/theories/Init/Tactics.v @@ -79,7 +79,7 @@ Ltac case_eq x := generalize (eq_refl x); pattern x at -1; case x. (* use either discriminate or injection on a hypothesis *) -Ltac destr_eq H := discriminate H || (try (injection H; clear H; intro H)). +Ltac destr_eq H := discriminate H || (try (injection H as H)). (* Similar variants of destruct *) diff --git a/theories/Lists/List.v b/theories/Lists/List.v index b666992206..9886ae6a8e 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -248,8 +248,7 @@ Section Facts. generalize (app_nil_r l); intros E. rewrite -> E; auto. intros. - injection H. - intro. + injection H as H H0. assert ([] = l ++ a0 :: l0) by auto. apply app_cons_not_nil in H1 as []. Qed. @@ -335,7 +334,7 @@ Section Facts. absurd (length (x1 :: l1 ++ l) <= length l). simpl; rewrite app_length; auto with arith. rewrite H; auto with arith. - injection H; clear H; intros; f_equal; eauto. + injection H as H H0; f_equal; eauto. Qed. End Facts. @@ -518,7 +517,7 @@ Section Elts. Proof. revert l. induction n as [|n IH]; intros [|x l] H; simpl in *; try easy. - - exists nil; exists l. injection H; clear H; intros; now subst. + - exists nil; exists l. now injection H as ->. - destruct (IH _ H) as (l1 & l2 & H1 & H2). exists (x::l1); exists l2; simpl; split; now f_equal. Qed. @@ -1385,9 +1384,8 @@ End Fold_Right_Recursor. Lemma combine_split : forall (l:list A)(l':list B), length l = length l' -> split (combine l l') = (l,l'). Proof. - induction l; destruct l'; simpl; intros; auto; try discriminate. - injection H; clear H; intros. - rewrite IHl; auto. + induction l, l'; simpl; trivial; try discriminate. + now intros [= ->%IHl]. Qed. Lemma in_combine_l : forall (l:list A)(l':list B)(x:A)(y:B), @@ -1471,7 +1469,7 @@ End Fold_Right_Recursor. destruct (in_app_or _ _ _ H); clear H. destruct (in_map_iff (fun y : B => (a, y)) l' (x,y)) as (H1,_). destruct (H1 H0) as (z,(H2,H3)); clear H0 H1. - injection H2; clear H2; intros; subst; intuition. + injection H2 as -> ->; intuition. intuition. Qed. diff --git a/theories/MSets/MSetPositive.v b/theories/MSets/MSetPositive.v index 8dd240f46e..be95a03799 100644 --- a/theories/MSets/MSetPositive.v +++ b/theories/MSets/MSetPositive.v @@ -908,10 +908,10 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. destruct o. intros x H. injection H; intros; subst. reflexivity. revert IHl. case choose. - intros p Hp x H. injection H; intros; subst; clear H. apply Hp. + intros p Hp x H. injection H as <-. apply Hp. reflexivity. intros _ x. revert IHr. case choose. - intros p Hp H. injection H; intros; subst; clear H. apply Hp. + intros p Hp H. injection H as <-. apply Hp. reflexivity. intros. discriminate. Qed. @@ -968,11 +968,11 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. induction s as [| l IHl o r IHr]; simpl. intros. discriminate. intros x. destruct (min_elt l); intros. - injection H. intros <-. apply IHl. reflexivity. + injection H as <-. apply IHl. reflexivity. destruct o; simpl. - injection H. intros <-. reflexivity. + injection H as <-. reflexivity. destruct (min_elt r); simpl in *. - injection H. intros <-. apply IHr. reflexivity. + injection H as <-. apply IHr. reflexivity. discriminate. Qed. @@ -996,15 +996,15 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. induction s as [|l IHl o r IHr]; intros x y H H'. discriminate. simpl in H. case_eq (min_elt l). - intros p Hp. rewrite Hp in H. injection H; intros <-. + intros p Hp. rewrite Hp in H. injection H as <-. destruct y as [z|z|]; simpl; intro; trivial. apply (IHl p z); trivial. intro Hp; rewrite Hp in H. apply min_elt_spec3 in Hp. destruct o. - injection H. intros <- Hl. clear H. + injection H as <-. intros Hl. destruct y as [z|z|]; simpl; trivial. elim (Hp _ H'). destruct (min_elt r). - injection H. intros <-. clear H. + injection H as <-. destruct y as [z|z|]. apply (IHr e z); trivial. elim (Hp _ H'). @@ -1021,11 +1021,11 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. induction s as [| l IHl o r IHr]; simpl. intros. discriminate. intros x. destruct (max_elt r); intros. - injection H. intros <-. apply IHr. reflexivity. + injection H as <-. apply IHr. reflexivity. destruct o; simpl. - injection H. intros <-. reflexivity. + injection H as <-. reflexivity. destruct (max_elt l); simpl in *. - injection H. intros <-. apply IHl. reflexivity. + injection H as <-. apply IHl. reflexivity. discriminate. Qed. @@ -1049,15 +1049,15 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. induction s as [|l IHl o r IHr]; intros x y H H'. discriminate. simpl in H. case_eq (max_elt r). - intros p Hp. rewrite Hp in H. injection H; intros <-. + intros p Hp. rewrite Hp in H. injection H as <-. destruct y as [z|z|]; simpl; intro; trivial. apply (IHr p z); trivial. intro Hp; rewrite Hp in H. apply max_elt_spec3 in Hp. destruct o. - injection H. intros <- Hl. clear H. + injection H as <-. intros Hl. destruct y as [z|z|]; simpl; trivial. elim (Hp _ H'). destruct (max_elt l). - injection H. intros <-. clear H. + injection H as <-. destruct y as [z|z|]. elim (Hp _ H'). apply (IHl e z); trivial. diff --git a/theories/MSets/MSetRBT.v b/theories/MSets/MSetRBT.v index 751d4f35c6..83a2343dd4 100644 --- a/theories/MSets/MSetRBT.v +++ b/theories/MSets/MSetRBT.v @@ -911,7 +911,7 @@ Proof. { inversion_clear O. assert (InT x l) by now apply min_elt_spec1. auto. } simpl. case X.compare_spec; try order. - destruct lc; injection E; clear E; intros; subst l s0; auto. + destruct lc; injection E; subst l s0; auto. Qed. Lemma remove_min_spec1 s x s' `{Ok s}: @@ -1948,7 +1948,7 @@ Module Make (X: Orders.OrderedType) <: generalize (fun x s' => @Raw.remove_min_spec1 s x s' Hs). set (P := Raw.remove_min_ok s). clearbody P. destruct (Raw.remove_min s) as [(x0,s0)|]; try easy. - intros H U. injection U. clear U; intros; subst. simpl. + intros H U. injection U as -> <-. simpl. destruct (H x s0); auto. subst; intuition. Qed. diff --git a/theories/Numbers/Cyclic/ZModulo/ZModulo.v b/theories/Numbers/Cyclic/ZModulo/ZModulo.v index c115a831d9..04fc5a8dfa 100644 --- a/theories/Numbers/Cyclic/ZModulo/ZModulo.v +++ b/theories/Numbers/Cyclic/ZModulo/ZModulo.v @@ -369,7 +369,7 @@ Section ZModulo. assert (Z.div_eucl ([|x|]*[|y|]) wB = (([|x|]*[|y|])/wB,([|x|]*[|y|]) mod wB)). unfold Z.modulo, Z.div; destruct Z.div_eucl; auto. generalize (Z_div_mod ([|x|]*[|y|]) wB wB_pos); destruct Z.div_eucl as (h,l). - destruct 1; injection H; clear H; intros. + destruct 1; injection H as ? ?. rewrite H0. assert ([|l|] = l). apply Zmod_small; auto. @@ -411,7 +411,7 @@ Section ZModulo. unfold Z.modulo, Z.div; destruct Z.div_eucl; auto. generalize (Z_div_mod [|a|] [|b|] H0). destruct Z.div_eucl as (q,r); destruct 1; intros. - injection H1; clear H1; intros. + injection H1 as ? ?. assert ([|r|]=r). apply Zmod_small; generalize (Z_mod_lt b wB wB_pos); fold [|b|]; auto with zarith. @@ -522,7 +522,7 @@ Section ZModulo. unfold Z.modulo, Z.div; destruct Z.div_eucl; auto. generalize (Z_div_mod a [|b|] H3). destruct Z.div_eucl as (q,r); destruct 1; intros. - injection H4; clear H4; intros. + injection H4 as ? ?. assert ([|r|]=r). apply Zmod_small; generalize (Z_mod_lt b wB wB_pos); fold [|b|]; auto with zarith. diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v index 56cb9bbc2c..7c76011f21 100644 --- a/theories/Numbers/Integer/BigZ/BigZ.v +++ b/theories/Numbers/Integer/BigZ/BigZ.v @@ -138,7 +138,7 @@ intros NEQ. generalize (BigZ.spec_div_eucl a b). generalize (Z_div_mod_full [a] [b] NEQ). destruct BigZ.div_eucl as (q,r), Z.div_eucl as (q',r'). -intros (EQ,_). injection 1. intros EQr EQq. +intros (EQ,_). injection 1 as EQr EQq. BigZ.zify. rewrite EQr, EQq; auto. Qed. diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v index 8673b8a58f..63fb5800c1 100644 --- a/theories/Numbers/Integer/BigZ/ZMake.v +++ b/theories/Numbers/Integer/BigZ/ZMake.v @@ -427,13 +427,13 @@ Module Make (NN:NType) <: ZType. (* Pos Neg *) generalize (NN.spec_div_eucl x y); destruct (NN.div_eucl x y) as (q,r). break_nonneg x px EQx; break_nonneg y py EQy; - try (injection 1; intros Hr Hq; rewrite NN.spec_eqb, NN.spec_0, Hr; + try (injection 1 as Hq Hr; rewrite NN.spec_eqb, NN.spec_0, Hr; simpl; rewrite Hq, NN.spec_0; auto). change (- Zpos py) with (Zneg py). assert (GT : Zpos py > 0) by (compute; auto). generalize (Z_div_mod (Zpos px) (Zpos py) GT). unfold Z.div_eucl. destruct (Z.pos_div_eucl px (Zpos py)) as (q',r'). - intros (EQ,MOD). injection 1. intros Hr' Hq'. + intros (EQ,MOD). injection 1 as Hq' Hr'. rewrite NN.spec_eqb, NN.spec_0, Hr'. break_nonneg r pr EQr. subst; simpl. rewrite NN.spec_0; auto. @@ -442,13 +442,13 @@ Module Make (NN:NType) <: ZType. (* Neg Pos *) generalize (NN.spec_div_eucl x y); destruct (NN.div_eucl x y) as (q,r). break_nonneg x px EQx; break_nonneg y py EQy; - try (injection 1; intros Hr Hq; rewrite NN.spec_eqb, NN.spec_0, Hr; + try (injection 1 as Hq Hr; rewrite NN.spec_eqb, NN.spec_0, Hr; simpl; rewrite Hq, NN.spec_0; auto). change (- Zpos px) with (Zneg px). assert (GT : Zpos py > 0) by (compute; auto). generalize (Z_div_mod (Zpos px) (Zpos py) GT). unfold Z.div_eucl. destruct (Z.pos_div_eucl px (Zpos py)) as (q',r'). - intros (EQ,MOD). injection 1. intros Hr' Hq'. + intros (EQ,MOD). injection 1 as Hq' Hr'. rewrite NN.spec_eqb, NN.spec_0, Hr'. break_nonneg r pr EQr. subst; simpl. rewrite NN.spec_0; auto. @@ -457,7 +457,7 @@ Module Make (NN:NType) <: ZType. (* Neg Neg *) generalize (NN.spec_div_eucl x y); destruct (NN.div_eucl x y) as (q,r). break_nonneg x px EQx; break_nonneg y py EQy; - try (injection 1; intros Hr Hq; rewrite Hr, Hq; auto). + try (injection 1 as -> ->; auto). simpl. intros <-; auto. Qed. diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v index ec1017f505..e8ff516f35 100644 --- a/theories/Numbers/Natural/BigN/BigN.v +++ b/theories/Numbers/Natural/BigN/BigN.v @@ -110,7 +110,7 @@ intros NEQ. generalize (BigN.spec_div_eucl a b). generalize (Z_div_mod_full [a] [b] NEQ). destruct BigN.div_eucl as (q,r), Z.div_eucl as (q',r'). -intros (EQ,_). injection 1. intros EQr EQq. +intros (EQ,_). injection 1 as EQr EQq. BigN.zify. rewrite EQr, EQq; auto. Qed. diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v index 0ccfad7b28..7baf102aaa 100644 --- a/theories/PArith/BinPos.v +++ b/theories/PArith/BinPos.v @@ -201,7 +201,6 @@ Proof. Qed. (** ** No neutral elements for addition *) - Lemma add_no_neutral p q : q + p <> p. Proof. revert q. @@ -508,7 +507,7 @@ Qed. Lemma mul_xO_discr p q : p~0 * q <> q. Proof. induction q; try discriminate. - rewrite mul_xO_r; injection; assumption. + rewrite mul_xO_r; injection; auto. Qed. (** ** Simplification properties of multiplication *) diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v index 17f05c5113..a349eb9085 100644 --- a/theories/Program/Equality.v +++ b/theories/Program/Equality.v @@ -333,7 +333,7 @@ Ltac simplify_one_dep_elim_term c := (let hyp := fresh in intros hyp ; move hyp before y ; revert_until hyp ; generalize dependent y ; refine (solution_right _ _ _ _)(* ; intros until 0 *)) - | ?f ?x = ?g ?y -> _ => let H := fresh in progress (intros H ; injection H ; clear H) + | ?f ?x = ?g ?y -> _ => let H := fresh in progress (intros H ; simple injection H; clear H) | ?t = ?u -> _ => let hyp := fresh in intros hyp ; exfalso ; discriminate | ?x = ?y -> _ => let hyp := fresh in diff --git a/theories/QArith/Qcanon.v b/theories/QArith/Qcanon.v index 6bfa47bc55..9f9651d84a 100644 --- a/theories/QArith/Qcanon.v +++ b/theories/QArith/Qcanon.v @@ -84,7 +84,7 @@ Arguments Q2Qc q%Q. Lemma Q2Qc_eq_iff (q q' : Q) : Q2Qc q = Q2Qc q' <-> q == q'. Proof. split; intro H. - - injection H. apply Qred_eq_iff. + - now injection H as H%Qred_eq_iff. - apply Qc_is_canon. simpl. now rewrite H. Qed. @@ -266,7 +266,7 @@ Theorem Qcmult_integral : forall x y, x*y=0 -> x=0 \/ y=0. Proof. intros. destruct (Qmult_integral x y); try qc; auto. - injection H; clear H; intros. + injection H as H. rewrite <- (Qred_correct (x*y)). rewrite <- (Qred_correct 0). rewrite H; auto with qarith. diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v index 8470b79550..44f8ff6a71 100644 --- a/theories/Sorting/Permutation.v +++ b/theories/Sorting/Permutation.v @@ -318,7 +318,7 @@ Lemma Permutation_length_2_inv : Proof. intros a1 a2 l H; remember [a1;a2] as m in H. revert a1 a2 Heqm. - induction H; intros; try (injection Heqm; intros; subst; clear Heqm); + induction H; intros; try (injection Heqm as ? ?; subst); discriminate || (try tauto). apply Permutation_length_1_inv in H as ->; left; auto. apply IHPermutation1 in Heqm as [H1|H1]; apply IHPermutation2 in H1 as []; diff --git a/theories/Strings/String.v b/theories/Strings/String.v index 943bb48e92..451b65cbe9 100644 --- a/theories/Strings/String.v +++ b/theories/Strings/String.v @@ -83,7 +83,7 @@ intros H; generalize (H 0); simpl; intros H1; inversion H1. case (Rec s). intros H0; rewrite H0; auto. intros n; exact (H (S n)). -intros H; injection H; intros H1 H2 n; case n; auto. +intros H; injection H as H1 H2. rewrite H2; trivial. rewrite H1; auto. Qed. @@ -238,14 +238,14 @@ intros n m s1 s2; generalize n m s1; clear n m s1; elim s2; simpl; auto. intros n; case n; simpl; auto. intros m s1; case s1; simpl; auto. -intros H; injection H; intros H1; rewrite <- H1; auto. +intros H; injection H as <-; auto. intros; discriminate. intros; discriminate. intros b s2' Rec n m s1. case n; simpl; auto. generalize (prefix_correct s1 (String b s2')); case (prefix s1 (String b s2')). -intros H0 H; injection H; intros H1; rewrite <- H1; auto. +intros H0 H; injection H as <-; auto. case H0; simpl; auto. case m; simpl; auto. case (index 0 s1 s2'); intros; discriminate. @@ -271,7 +271,7 @@ intros n m s1 s2; generalize n m s1; clear n m s1; elim s2; simpl; auto. intros n; case n; simpl; auto. intros m s1; case s1; simpl; auto. -intros H; injection H; intros H1; rewrite <- H1. +intros H; injection H as <-. intros p H0 H2; inversion H2. intros; discriminate. intros; discriminate. @@ -279,7 +279,7 @@ intros b s2' Rec n m s1. case n; simpl; auto. generalize (prefix_correct s1 (String b s2')); case (prefix s1 (String b s2')). -intros H0 H; injection H; intros H1; rewrite <- H1; auto. +intros H0 H; injection H as <-; auto. intros p H2 H3; inversion H3. case m; simpl; auto. case (index 0 s1 s2'); intros; discriminate. diff --git a/theories/Wellfounded/Lexicographic_Product.v b/theories/Wellfounded/Lexicographic_Product.v index 4b8447f496..b2ada2f919 100644 --- a/theories/Wellfounded/Lexicographic_Product.v +++ b/theories/Wellfounded/Lexicographic_Product.v @@ -44,14 +44,11 @@ Section WfLexicographic_Product. apply H2. auto with sets. - injection H1. - destruct 2. - injection H3. - destruct 2; auto with sets. + injection H1 as <- _. + injection H3 as <- _; auto with sets. rewrite <- H1. - injection H3; intros _ Hx1. - subst x1. + injection H3 as -> H3. apply IHAcc0. elim inj_pair2 with A B x y' x0; assumption. Defined. |