aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--contrib/romega/ReflOmegaCore.v28
-rw-r--r--theories/Arith/Compare_dec.v4
-rw-r--r--theories/FSets/FMapAVL.v30
-rw-r--r--theories/FSets/FMapFacts.v2
-rw-r--r--theories/FSets/FMapIntMap.v2
-rw-r--r--theories/FSets/FMapWeakFacts.v6
-rw-r--r--theories/FSets/FMapWeakList.v34
-rw-r--r--theories/FSets/FSetProperties.v2
-rw-r--r--theories/FSets/FSetToFiniteSet.v4
-rw-r--r--theories/FSets/FSetWeakList.v14
-rw-r--r--theories/Init/Tactics.v20
-rw-r--r--theories/Lists/List.v10
-rw-r--r--theories/Lists/SetoidList.v12
-rw-r--r--theories/QArith/QArith_base.v4
-rw-r--r--theories/QArith/Qcanon.v2
-rw-r--r--theories/Sorting/PermutSetoid.v2
-rw-r--r--theories/ZArith/Zdiv.v8
-rw-r--r--theories/ZArith/Znumtheory.v16
-rw-r--r--theories/ZArith/Zpow_facts.v4
-rw-r--r--theories/ZArith/Zsqrt.v6
20 files changed, 106 insertions, 104 deletions
diff --git a/contrib/romega/ReflOmegaCore.v b/contrib/romega/ReflOmegaCore.v
index f3a82c05e..ee44d6d21 100644
--- a/contrib/romega/ReflOmegaCore.v
+++ b/contrib/romega/ReflOmegaCore.v
@@ -277,9 +277,9 @@ Module IntProperties (I:Int).
Lemma ne_left_2 : forall x y : int, x<>y -> 0<>(x + - y).
Proof.
- intros; swap H.
+ intros; contradict H.
apply (plus_reg_l (-y)).
- now rewrite plus_opp_l, plus_comm, H0.
+ now rewrite plus_opp_l, plus_comm, H.
Qed.
(* Special lemmas for factorisation. *)
@@ -483,7 +483,7 @@ Module IntProperties (I:Int).
destruct (eq_dec n m) as [H'|H'].
right; intuition.
left; rewrite lt_le_iff.
- swap H'.
+ contradict H'.
apply le_antisym; auto.
Qed.
@@ -536,9 +536,9 @@ Module IntProperties (I:Int).
apply plus_le_compat; auto.
apply lt_le_weak; auto.
rewrite lt_le_iff in H0.
- swap H0.
+ contradict H0.
apply plus_le_reg_r with m.
- rewrite (plus_comm q m), <-H1, (plus_comm p m).
+ rewrite (plus_comm q m), <-H0, (plus_comm p m).
apply plus_le_compat; auto.
apply le_refl; auto.
Qed.
@@ -552,7 +552,7 @@ Module IntProperties (I:Int).
Lemma opp_lt_compat : forall n m, n<m -> -m < -n.
Proof.
- intros n m; do 2 rewrite lt_le_iff; intros H; swap H.
+ intros n m; do 2 rewrite lt_le_iff; intros H; contradict H.
rewrite <-(opp_involutive m), <-(opp_involutive n).
apply opp_le_compat; auto.
Qed.
@@ -648,8 +648,8 @@ Module IntProperties (I:Int).
Proof.
intros.
subst b; rewrite mult_0_l, plus_0_r.
- swap H.
- symmetry in H1; destruct (mult_integral _ _ H1); congruence.
+ contradict H.
+ symmetry in H; destruct (mult_integral _ _ H); congruence.
Qed.
Lemma one_neq_zero : 1 <> 0.
@@ -788,8 +788,8 @@ Module IntProperties (I:Int).
intros n m p.
do 2 rewrite gt_lt_iff.
do 2 rewrite le_lt_iff; intros.
- swap H1.
- rewrite lt_0_neg' in H2.
+ contradict H1.
+ rewrite lt_0_neg' in H1.
rewrite lt_0_neg'.
rewrite opp_plus_distr.
rewrite mult_comm, opp_mult_distr_r.
@@ -800,13 +800,13 @@ Module IntProperties (I:Int).
rewrite le_lt_int in H0.
apply le_trans with (n+-(1)); auto.
apply plus_le_compat; [ | apply le_refl ].
- rewrite le_lt_int in H2.
- generalize (mult_le_compat _ _ _ _ (lt_le_weak _ _ H) H2 (le_refl 0) (le_refl 0)).
+ rewrite le_lt_int in H1.
+ generalize (mult_le_compat _ _ _ _ (lt_le_weak _ _ H) H1 (le_refl 0) (le_refl 0)).
rewrite mult_0_l.
rewrite mult_plus_distr_l.
rewrite <- opp_eq_mult_neg_1.
intros.
- generalize (plus_le_compat _ _ _ _ (le_refl n) H1).
+ generalize (plus_le_compat _ _ _ _ (le_refl n) H2).
now rewrite plus_permute, opp_def, plus_0_r, plus_0_r.
Qed.
@@ -2372,7 +2372,7 @@ Proof.
Simplify; simpl; auto; subst;
rewrite <- scalar_norm_stable; simpl; intros;
[ destruct (mult_integral _ _ (sym_eq H0)); intuition
- | swap H0; rewrite <- H1, mult_0_l; auto
+ | contradict H0; rewrite <- H0, mult_0_l; auto
].
Qed.
diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v
index 8b7e2c61d..ac44586c1 100644
--- a/theories/Arith/Compare_dec.v
+++ b/theories/Arith/Compare_dec.v
@@ -170,7 +170,7 @@ Proof.
exact (lt_irrefl n).
intros.
apply not_gt.
- swap H.
+ contradict H.
destruct (nat_compare_gt n m); auto.
Qed.
@@ -184,7 +184,7 @@ Proof.
exact (lt_irrefl m).
intros.
apply not_lt.
- swap H.
+ contradict H.
destruct (nat_compare_lt n m); auto.
Qed.
diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v
index b7947cddd..0e9bd6e5e 100644
--- a/theories/FSets/FMapAVL.v
+++ b/theories/FSets/FMapAVL.v
@@ -1335,20 +1335,21 @@ Definition equal_aux :
{ ~ L.Equal cmp (flatten_e e1) (flatten_e e2) }.
Proof.
intros cmp e1 e2; pattern e1, e2 in |- *; apply compare_rec2.
- simple destruct x; simple destruct x'; intuition.
+ simple destruct x; simple destruct x'; intros.
(* x = x' = End *)
- left; unfold L.Equal in |- *; intuition.
+ left; unfold L.Equal in |- *; split; intros.
+ intuition.
inversion H2.
(* x = End x' = More *)
right; simpl in |- *; auto.
- destruct 1.
+ red; destruct 1.
destruct (H2 k).
destruct H5; auto.
exists e; auto.
inversion H5.
(* x = More x' = End *)
right; simpl in |- *; auto.
- destruct 1.
+ red; destruct 1.
destruct (H2 k).
destruct H4; auto.
exists e; auto.
@@ -1357,7 +1358,7 @@ Proof.
case (X.compare k k0); intro.
(* k < k0 *)
right.
- destruct 1.
+ red; destruct 1.
clear H3 H.
assert (L.PX.In k (flatten_e (More k0 e3 t0 e4))).
destruct (H2 k).
@@ -1371,7 +1372,7 @@ Proof.
intros EQ.
destruct (@cons t e0) as [c1 (H2,(H3,H4))]; try inversion_clear H0; auto.
destruct (@cons t0 e4) as [c2 (H5,(H6,H7))]; try inversion_clear H1; auto.
- destruct (H c1 c2); clear H; intuition.
+ destruct (H c1 c2); clear H; intros; auto.
Measure_e; omega.
left.
rewrite H4 in e6; rewrite H7 in e6.
@@ -1382,14 +1383,14 @@ Proof.
simpl; rewrite <- L.equal_cons; auto.
apply (sorted_flatten_e H0).
apply (sorted_flatten_e H1).
- swap f.
+ contradict n.
rewrite H4; rewrite H7; auto.
right.
- destruct 1.
+ red; destruct 1.
rewrite (H4 k) in H2; try discriminate; simpl; auto.
(* k > k0 *)
right.
- destruct 1.
+ red; destruct 1.
clear H3 H.
assert (L.PX.In k0 (flatten_e (More k e t e0))).
destruct (H2 k0).
@@ -1422,13 +1423,14 @@ Proof.
inversion_clear 2.
simpl in a; rewrite <- app_nil_end in a.
simpl in a0; rewrite <- app_nil_end in a0.
- destruct (@equal_aux cmp x x0); intuition.
+ decompose [and] a; decompose [and] a0.
+ destruct (@equal_aux cmp x x0); auto.
left.
- rewrite H4 in e; rewrite H5 in e.
+ rewrite H2 in e; rewrite H5 in e.
rewrite Equal_elements; auto.
right.
- swap n.
- rewrite H4; rewrite H5.
+ contradict n.
+ rewrite H2; rewrite H5.
rewrite <- Equal_elements; auto.
Qed.
@@ -1586,7 +1588,7 @@ inversion H1; auto.
intros.
inversion_clear H1.
assert (~X.eq x k).
- swap H5.
+ contradict H5.
destruct H3.
apply InA_eqA with (x,x0); eauto.
apply (H2 x).
diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index 0906099de..720bdd4af 100644
--- a/theories/FSets/FMapFacts.v
+++ b/theories/FSets/FMapFacts.v
@@ -680,7 +680,7 @@ Module Properties (M: S).
destruct y; unfold O.ltk in *; simpl in *.
rewrite <- elements_mapsto_iff in H1.
assert (~E.eq x t0).
- swap H.
+ contradict H.
exists e0; apply MapsTo_1 with t0; auto.
ME.order.
intros.
diff --git a/theories/FSets/FMapIntMap.v b/theories/FSets/FMapIntMap.v
index b5fe6722b..761c8d8e6 100644
--- a/theories/FSets/FMapIntMap.v
+++ b/theories/FSets/FMapIntMap.v
@@ -465,7 +465,7 @@ Module MapIntMap <: S with Module E:=NUsualOrderedType.
intros.
inversion_clear H.
assert (~E.eq x k).
- swap H3.
+ contradict H3.
destruct H1.
apply InA_eqA with (x,x0); eauto.
unfold eq_key, E.eq; eauto.
diff --git a/theories/FSets/FMapWeakFacts.v b/theories/FSets/FMapWeakFacts.v
index 5d401126a..11608698f 100644
--- a/theories/FSets/FMapWeakFacts.v
+++ b/theories/FSets/FMapWeakFacts.v
@@ -603,9 +603,9 @@ Module Properties
Proof.
induction 1; auto.
constructor; auto.
- swap H.
+ contradict H.
destruct x as (x,y).
- rewrite InA_alt in *; destruct H1 as ((a,b),((H1,H2),H3)); simpl in *.
+ rewrite InA_alt in *; destruct H as ((a,b),((H1,H2),H3)); simpl in *.
exists (a,b); auto.
Qed.
@@ -656,7 +656,7 @@ Module Properties
apply NoDupA_rev; auto; apply NoDupA_eqk_eqke; apply elements_3w.
apply NoDupA_rev; auto; apply NoDupA_eqk_eqke; apply elements_3w.
rewrite InA_rev.
- swap H1.
+ contradict H1.
exists e.
rewrite elements_mapsto_iff; auto.
intros a.
diff --git a/theories/FSets/FMapWeakList.v b/theories/FSets/FMapWeakList.v
index 0afdf5d00..dca6e5498 100644
--- a/theories/FSets/FMapWeakList.v
+++ b/theories/FSets/FMapWeakList.v
@@ -221,10 +221,10 @@ Proof.
destruct a as (x',e').
simpl; case (X.eq_dec x x'); inversion_clear Hm; auto.
constructor; auto.
- swap H.
+ contradict H.
apply InA_eqk with (x,e); auto.
constructor; auto.
- swap H; apply add_3' with x e; auto.
+ contradict H; apply add_3' with x e; auto.
Qed.
(* Not part of the exported specifications, used later for [combine]. *)
@@ -272,8 +272,8 @@ Proof.
inversion_clear Hm.
subst.
- swap H0.
- destruct H2 as (e,H2); unfold PX.MapsTo in H2.
+ contradict H0.
+ destruct H0 as (e,H2); unfold PX.MapsTo in H2.
apply InA_eqk with (y,e); auto.
compute; apply X.eq_trans with x; auto.
@@ -323,7 +323,7 @@ Proof.
destruct a as (x',e').
simpl; case (X.eq_dec x x'); auto.
constructor; auto.
- swap H; apply remove_3' with x; auto.
+ contradict H; apply remove_3' with x; auto.
Qed.
(** * [elements] *)
@@ -533,12 +533,12 @@ Proof.
destruct a as (x',e').
inversion_clear Hm.
constructor; auto.
- swap H.
+ contradict H.
(* il faut un map_1 avec eqk au lieu de eqke *)
clear IHm H0.
induction m; simpl in *; auto.
- inversion H1.
- destruct a; inversion H1; auto.
+ inversion H.
+ destruct a; inversion H; auto.
Qed.
(** Specification of [mapi] *)
@@ -593,11 +593,11 @@ Proof.
destruct a as (x',e').
inversion_clear Hm; auto.
constructor; auto.
- swap H.
+ contradict H.
clear IHm H0.
induction m; simpl in *; auto.
- inversion_clear H1.
- destruct a; inversion_clear H1; auto.
+ inversion_clear H.
+ destruct a; inversion_clear H; auto.
Qed.
End Elt2.
@@ -765,13 +765,13 @@ Proof.
inversion_clear H1.
destruct a; destruct o; simpl; auto.
constructor; auto.
- swap H.
+ contradict H.
clear IHl1.
induction l1.
- inversion H1.
+ inversion H.
inversion_clear H0.
destruct a; destruct o; simpl in *; auto.
- inversion_clear H1; auto.
+ inversion_clear H; auto.
Qed.
Definition at_least_one_then_f (o:option elt)(o':option elt') :=
@@ -807,7 +807,7 @@ Proof.
rewrite H2.
unfold f'; simpl.
destruct (f oo oo'); simpl.
- destruct (X.eq_dec x k); try absurd_hyp n; auto.
+ destruct (X.eq_dec x k); try contradict n; auto.
destruct (IHm0 H1) as (_,H4); apply H4; auto.
case_eq (find x m0); intros; auto.
elim H0.
@@ -817,7 +817,7 @@ Proof.
(* k < x *)
unfold f'; simpl.
destruct (f oo oo'); simpl.
- destruct (X.eq_dec x k); [ absurd_hyp n; auto | auto].
+ destruct (X.eq_dec x k); [ contradict n; auto | auto].
destruct (IHm0 H1) as (H3,_); apply H3; auto.
destruct (IHm0 H1) as (H3,_); apply H3; auto.
@@ -831,7 +831,7 @@ Proof.
(* k < x *)
unfold f'; simpl.
destruct (f oo oo'); simpl.
- destruct (X.eq_dec x k); [ absurd_hyp n; auto | auto].
+ destruct (X.eq_dec x k); [ contradict n; auto | auto].
destruct (IHm0 H1) as (_,H4); apply H4; auto.
destruct (IHm0 H1) as (_,H4); apply H4; auto.
Qed.
diff --git a/theories/FSets/FSetProperties.v b/theories/FSets/FSetProperties.v
index 2315dc532..f6eebdc17 100644
--- a/theories/FSets/FSetProperties.v
+++ b/theories/FSets/FSetProperties.v
@@ -546,7 +546,7 @@ Module Properties (M: S).
rewrite leb_1 in H2.
rewrite <- elements_iff in H1.
assert (~E.eq x y).
- swap H; rewrite H3; auto.
+ contradict H; rewrite H; auto.
ME.order.
intros.
rewrite filter_InA in H1; auto; destruct H1.
diff --git a/theories/FSets/FSetToFiniteSet.v b/theories/FSets/FSetToFiniteSet.v
index 747fd3796..de483f158 100644
--- a/theories/FSets/FSetToFiniteSet.v
+++ b/theories/FSets/FSetToFiniteSet.v
@@ -107,8 +107,8 @@ Module S_to_Finite_set (U:UsualOrderedType)(M:S with Module E := U).
unfold Same_set, Included, mkEns, In.
split; intro; set_iff; inversion 1; unfold E.eq in *; auto with sets.
split; auto.
- swap H1.
- inversion H2; auto.
+ contradict H1.
+ inversion H1; auto.
Qed.
Lemma mkEns_Finite : forall s, Finite _ (!!s).
diff --git a/theories/FSets/FSetWeakList.v b/theories/FSets/FSetWeakList.v
index e45c2c343..b207f1f1e 100644
--- a/theories/FSets/FSetWeakList.v
+++ b/theories/FSets/FSetWeakList.v
@@ -777,22 +777,22 @@ Module Raw (X: DecidableType).
apply remove_2; auto.
(* In a s' /\ ~ s [=] remove a s' *)
generalize (mem_2 H); clear H; intro H.
- swap H'.
+ contradict H'.
unfold Equal in *; intros b.
split; intros.
apply remove_2; auto.
inversion_clear Hs.
- swap H2; apply In_eq with b; auto.
- rewrite <- H0; rewrite InA_cons; auto.
+ contradict H1; apply In_eq with b; auto.
+ rewrite <- H'; rewrite InA_cons; auto.
assert (In b s') by (apply remove_3 with a; auto).
- rewrite <- H0, InA_cons in H2; destruct H2; auto.
- elim (remove_1 Hs' (X.eq_sym H2) H1).
+ rewrite <- H', InA_cons in H1; destruct H1; auto.
+ elim (remove_1 Hs' (X.eq_sym H1) H0).
(* ~ In a s' *)
assert (~In a s').
red; intro H'; rewrite (mem_1 H') in H; discriminate.
- swap H0.
+ contradict H0.
unfold Equal in *.
- rewrite <- H1.
+ rewrite <- H0.
rewrite InA_cons; auto.
Qed.
diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
index 29ec5f888..de38e88c1 100644
--- a/theories/Init/Tactics.v
+++ b/theories/Init/Tactics.v
@@ -49,23 +49,23 @@ Ltac contradict name :=
end
end).
-(* to contradict an hypothesis without copying its type. *)
+(* Transforming a negative goal [ H:~A |- ~B ] into a positive one [ B |- A ]*)
+
+Ltac swap H :=
+ idtac "swap is OBSOLETE: use contradict instead.";
+ intro; apply H; clear H.
+(* to contradict an hypothesis without copying its type. *)
Ltac absurd_hyp h :=
- (* idtac "absurd_hyp is OBSOLETE: use contradict instead."; *)
+ idtac "contradict is OBSOLETE: use contradict instead.";
let T := type of h in
absurd T.
-(* A useful complement to absurd_hyp. Here t : ~ A where H : A. *)
-Ltac false_hyp H t :=
-absurd_hyp H; [apply t | assumption].
-
-(* Transforming a negative goal [ H:~A |- ~B ] into a positive one [ B |- A ]*)
+(* A useful complement to contradict. Here t : ~ A where H : A. *)
-Ltac swap H :=
- (* idtac "swap is OBSOLETE: use contradict instead."; *)
- intro; apply H; clear H.
+Ltac false_hyp h t :=
+ let T := type of h in absurd T; [ apply t | assumption ].
(* A case with no loss of information. *)
diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index c618257b9..d0bf5bee9 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -919,7 +919,7 @@ Section ListOps.
apply perm_trans with (l1'++a::l2); auto using Permutation_cons_app.
apply perm_skip.
apply (IH a l1' l2 l3' l4); auto.
- (* swap *)
+ (* contradict *)
intros x y l l' Hp IH; intros.
break_list l1 b l1' H; break_list l3 c l3' H0.
auto.
@@ -1692,8 +1692,8 @@ Section ReDun.
inversion_clear 1; auto.
inversion_clear 1.
constructor.
- swap H0.
- apply in_or_app; destruct (in_app_or _ _ _ H); simpl; tauto.
+ contradict H0.
+ apply in_or_app; destruct (in_app_or _ _ _ H0); simpl; tauto.
apply IHl with a0; auto.
Qed.
@@ -1702,8 +1702,8 @@ Section ReDun.
induction l; simpl.
inversion_clear 1; auto.
inversion_clear 1.
- swap H0.
- destruct H.
+ contradict H0.
+ destruct H0.
subst a0.
apply in_or_app; right; red; auto.
destruct (IHl _ _ H1); auto.
diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v
index 301a09f25..6c4e76d82 100644
--- a/theories/Lists/SetoidList.v
+++ b/theories/Lists/SetoidList.v
@@ -293,7 +293,7 @@ Lemma NoDupA_split : forall l l' x, NoDupA (l++x::l') -> NoDupA (l++l').
Proof.
induction l; simpl in *; inversion_clear 1; auto.
constructor; eauto.
- swap H0.
+ contradict H0.
rewrite InA_app_iff in *; rewrite InA_cons; intuition.
Qed.
@@ -309,7 +309,7 @@ Proof.
rewrite InA_app_iff in *; rewrite InA_cons; auto.
apply H; auto.
constructor.
- swap H0.
+ contradict H0.
rewrite InA_app_iff in *; rewrite InA_cons; intuition.
eapply NoDupA_split; eauto.
Qed.
@@ -482,9 +482,9 @@ Proof.
rewrite InA_app_iff in H0.
split; intros.
assert (~eqA a x).
- swap H3; apply InA_eqA with a; auto.
+ contradict H3; apply InA_eqA with a; auto.
assert (~eqA a y).
- swap H8; eauto.
+ contradict H8; eauto.
intuition.
assert (eqA a x \/ InA a l) by intuition.
destruct H8; auto.
@@ -569,7 +569,7 @@ destruct H0; apply eqA_trans with a; auto.
split.
inversion_clear 1.
split; auto.
-swap n.
+contradict n.
apply eqA_trans with y; auto.
rewrite (IHl x y) in H0; destruct H0; auto.
destruct 1; inversion_clear H; auto.
@@ -595,7 +595,7 @@ unfold equivlistA; intros.
rewrite removeA_InA.
split; intros.
rewrite <- H0; split; auto.
-swap H.
+contradict H.
apply InA_eqA with x0; auto.
rewrite <- (H0 x0) in H1.
destruct H1.
diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v
index 75bd9c5e6..5199333ed 100644
--- a/theories/QArith/QArith_base.v
+++ b/theories/QArith/QArith_base.v
@@ -79,9 +79,9 @@ Qed.
Lemma Qge_alt : forall p q, (p>=q) <-> (p?=q <> Lt).
Proof.
unfold Qle, Qcompare, Zle.
-split; intros; swap H.
+split; intros; contradict H.
rewrite Zcompare_Gt_Lt_antisym; auto.
-rewrite Zcompare_Gt_Lt_antisym in H0; auto.
+rewrite Zcompare_Gt_Lt_antisym in H; auto.
Qed.
Hint Unfold Qeq Qlt Qle: qarith.
diff --git a/theories/QArith/Qcanon.v b/theories/QArith/Qcanon.v
index cfe0187a3..06d653e30 100644
--- a/theories/QArith/Qcanon.v
+++ b/theories/QArith/Qcanon.v
@@ -139,7 +139,7 @@ Theorem Qc_eq_dec : forall x y:Qc, {x=y} + {x<>y}.
Proof.
intros.
destruct (Qeq_dec x y) as [H|H]; auto.
- right; swap H; subst; auto with qarith.
+ right; contradict H; subst; auto with qarith.
Defined.
(** The addition, multiplication and opposite are defined
diff --git a/theories/Sorting/PermutSetoid.v b/theories/Sorting/PermutSetoid.v
index f262f5e40..84eac9905 100644
--- a/theories/Sorting/PermutSetoid.v
+++ b/theories/Sorting/PermutSetoid.v
@@ -81,7 +81,7 @@ Proof.
rewrite IHl in H1.
intros; destruct (eqA_dec a a0) as [H2|H2]; simpl; auto.
rewrite multiplicity_InA_O; auto.
- swap H0.
+ contradict H0.
apply InA_eqA with a0; auto.
intros; constructor.
rewrite multiplicity_InA.
diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v
index 258ae1d13..187e182ea 100644
--- a/theories/ZArith/Zdiv.v
+++ b/theories/ZArith/Zdiv.v
@@ -666,7 +666,7 @@ Lemma Z_mod_nz_opp_full : forall a b:Z, a mod b <> 0 ->
(-a) mod b = b - (a mod b).
Proof.
intros.
- assert (b<>0) by (swap H; subst; rewrite Zmod_0_r; auto).
+ assert (b<>0) by (contradict H; subst; rewrite Zmod_0_r; auto).
symmetry; apply Zmod_unique_full with (-1-a/b); auto.
generalize (Z_mod_remainder a b H0); destruct 1; [left|right]; omega.
rewrite Zmult_minus_distr_l.
@@ -704,7 +704,7 @@ Lemma Z_div_nz_opp_full : forall a b:Z, a mod b <> 0 ->
(-a)/b = -(a/b)-1.
Proof.
intros.
- assert (b<>0) by (swap H; subst; rewrite Zmod_0_r; auto).
+ assert (b<>0) by (contradict H; subst; rewrite Zmod_0_r; auto).
symmetry; apply Zdiv_unique_full with (b-a mod b); auto.
generalize (Z_mod_remainder a b H0); destruct 1; [left|right]; omega.
pattern a at 1; rewrite (Z_div_mod_eq_full a b H0); ring.
@@ -1122,8 +1122,8 @@ Lemma Odiv_Omod_eq : forall a b, b<>0 ->
Proof.
intros.
assert (Zabs b <> 0).
- swap H.
- destruct b; simpl in *; auto with zarith; inversion H0.
+ contradict H.
+ destruct b; simpl in *; auto with zarith; inversion H.
pattern a at 1; rewrite <- (Zabs_Zsgn a).
rewrite (Z_div_mod_eq_full (Zabs a) (Zabs b) H0).
unfold Odiv, Omod.
diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v
index 710c8aca0..cbe65989e 100644
--- a/theories/ZArith/Znumtheory.v
+++ b/theories/ZArith/Znumtheory.v
@@ -663,7 +663,7 @@ Qed.
Theorem not_rel_prime_0: forall n, 1 < n -> ~ rel_prime 0 n.
Proof.
intros n H H1; absurd (n = 1 \/ n = -1).
- intros [H2 | H2]; subst; absurd_hyp H; auto with zarith.
+ intros [H2 | H2]; subst; contradict H; auto with zarith.
case (Zis_gcd_unique 0 n n 1); auto.
apply Zis_gcd_intro; auto.
exists 0; auto with zarith.
@@ -791,7 +791,7 @@ Proof.
apply prime_intro; auto with zarith.
intros n [H1 H2]; case Zle_lt_or_eq with ( 1 := H1 ); auto with zarith;
clear H1; intros H1.
- absurd_hyp H2; auto with zarith.
+ contradict H2; auto with zarith.
subst n; red; auto with zarith.
apply Zis_gcd_intro; auto with zarith.
Qed.
@@ -802,7 +802,7 @@ Proof.
intros n [H1 H2]; case Zle_lt_or_eq with ( 1 := H1 ); auto with zarith;
clear H1; intros H1.
case (Zle_lt_or_eq 2 n); auto with zarith; clear H1; intros H1.
- absurd_hyp H2; auto with zarith.
+ contradict H2; auto with zarith.
subst n; red; auto with zarith.
apply Zis_gcd_intro; auto with zarith.
intros x [q1 Hq1] [q2 Hq2].
@@ -871,10 +871,10 @@ Proof.
assert (Hp: 0 < p); try apply Zlt_le_trans with 2; try apply prime_ge_2; auto with zarith.
assert (Hq: 0 < q); try apply Zlt_le_trans with 2; try apply prime_ge_2; auto with zarith.
case prime_divisors with (2 := H2); auto.
- intros H4; absurd_hyp Hp; subst; auto with zarith.
+ intros H4; contradict Hp; subst; auto with zarith.
intros [H4| [H4 | H4]]; subst; auto.
- absurd_hyp H; auto; apply not_prime_1.
- absurd_hyp Hp; auto with zarith.
+ contradict H; auto; apply not_prime_1.
+ contradict Hp; auto with zarith.
Qed.
@@ -1147,7 +1147,7 @@ Definition rel_prime_dec: forall a b,
Proof.
intros a b; case (Z_eq_dec (Zgcd a b) 1); intros H1.
left; apply -> Zgcd_1_rel_prime; auto.
- right; swap H1; apply <- Zgcd_1_rel_prime; auto.
+ right; contradict H1; apply <- Zgcd_1_rel_prime; auto.
Defined.
Definition prime_dec_aux:
@@ -1167,7 +1167,7 @@ Proof.
intros HH3; subst x; auto.
case (Z_lt_dec 1 x); intros HH1.
right; exists x; split; auto with zarith.
- left; intros n [HHH1 HHH2]; absurd_hyp HHH1; auto with zarith.
+ left; intros n [HHH1 HHH2]; contradict HHH1; auto with zarith.
right; destruct E as (n,((H0,H2),H3)); exists n; auto with zarith.
Defined.
diff --git a/theories/ZArith/Zpow_facts.v b/theories/ZArith/Zpow_facts.v
index 448fa8602..fd8da834d 100644
--- a/theories/ZArith/Zpow_facts.v
+++ b/theories/ZArith/Zpow_facts.v
@@ -344,7 +344,7 @@ Theorem rel_prime_Zpower_r: forall i p q, 0 < i ->
rel_prime p q -> rel_prime p (q^i).
Proof.
intros i p q Hi Hpq; generalize Hi; pattern i; apply natlike_ind; auto with zarith; clear i Hi.
- intros H; absurd_hyp H; auto with zarith.
+ intros H; contradict H; auto with zarith.
intros i Hi Rec _; rewrite Zpower_Zsucc; auto.
apply rel_prime_mult; auto.
case Zle_lt_or_eq with (1 := Hi); intros Hi1; subst; auto.
@@ -403,7 +403,7 @@ Proof.
split; auto with zarith.
pattern q1 at 1; replace q1 with (q1 * 1); auto with zarith.
apply Zmult_lt_compat_l; auto with zarith.
- intros H5; subst; absurd_hyp Hx; auto with zarith.
+ intros H5; subst; contradict Hx; auto with zarith.
apply Zmult_le_0_reg_r with p1; auto with zarith.
apply Zdivide_trans with (2 := H); exists p1; auto with zarith.
intros r2 Hr2; exists (r2 + r1); subst.
diff --git a/theories/ZArith/Zsqrt.v b/theories/ZArith/Zsqrt.v
index 00da766d8..a97750d77 100644
--- a/theories/ZArith/Zsqrt.v
+++ b/theories/ZArith/Zsqrt.v
@@ -169,7 +169,7 @@ Theorem Zsqrt_plain_is_pos: forall n, 0 <= n -> 0 <= Zsqrt_plain n.
Proof.
intros n m; case (Zsqrt_interval n); auto with zarith.
intros H1 H2; case (Zle_or_lt 0 (Zsqrt_plain n)); auto.
- intros H3; absurd_hyp H2; auto; apply Zle_not_lt.
+ intros H3; contradict H2; auto; apply Zle_not_lt.
apply Zle_trans with ( 2 := H1 ).
replace ((Zsqrt_plain n + 1) * (Zsqrt_plain n + 1))
with (Zsqrt_plain n * Zsqrt_plain n + (2 * Zsqrt_plain n + 1));
@@ -187,10 +187,10 @@ Proof.
intros H1 H2.
case (Zle_or_lt a (Zsqrt_plain (a * a))); intros H3; auto.
case Zle_lt_or_eq with (1:=H3); auto; clear H3; intros H3.
- absurd_hyp H1; auto; apply Zlt_not_le; auto with zarith.
+ contradict H1; auto; apply Zlt_not_le; auto with zarith.
apply Zle_lt_trans with (a * Zsqrt_plain (a * a)); auto with zarith.
apply Zmult_lt_compat_r; auto with zarith.
- absurd_hyp H2; auto; apply Zle_not_lt; auto with zarith.
+ contradict H2; auto; apply Zle_not_lt; auto with zarith.
apply Zmult_le_compat; auto with zarith.
Qed.
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 10:54:52 +0000