diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
commit | 7cfc4e5146be5666419451bdd516f1f3f264d24a (patch) | |
tree | e4197645da03dc3c7cc84e434cc31d0a0cca7056 /theories/ZArith/Zcomplements.v | |
parent | 420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff) |
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'theories/ZArith/Zcomplements.v')
-rw-r--r-- | theories/ZArith/Zcomplements.v | 42 |
1 files changed, 22 insertions, 20 deletions
diff --git a/theories/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v index dceac4f2..9604a06e 100644 --- a/theories/ZArith/Zcomplements.v +++ b/theories/ZArith/Zcomplements.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -53,17 +53,18 @@ Theorem Z_lt_abs_rec : forall n:Z, P n. Proof. intros P HP p. - set (Q := fun z => 0 <= z -> P z * P (- z)) in *. - cut (Q (Z.abs p)); [ intros | apply (Z_lt_rec Q); auto with zarith ]. - elim (Zabs_dec p); intro eq; rewrite eq; elim H; auto with zarith. - unfold Q; clear Q; intros. + set (Q := fun z => 0 <= z -> P z * P (- z)). + enough (H:Q (Z.abs p)) by + (destruct (Zabs_dec p) as [-> | ->]; elim H; auto with zarith). + apply (Z_lt_rec Q); auto with zarith. + subst Q; intros x H. split; apply HP. - rewrite Z.abs_eq; auto; intros. - elim (H (Z.abs m)); intros; auto with zarith. - elim (Zabs_dec m); intro eq; rewrite eq; trivial. - rewrite Z.abs_neq, Z.opp_involutive; auto with zarith; intros. - elim (H (Z.abs m)); intros; auto with zarith. - elim (Zabs_dec m); intro eq; rewrite eq; trivial. + - rewrite Z.abs_eq; auto; intros. + destruct (H (Z.abs m)); auto with zarith. + destruct (Zabs_dec m) as [-> | ->]; trivial. + - rewrite Z.abs_neq, Z.opp_involutive; auto with zarith; intros. + destruct (H (Z.abs m)); auto with zarith. + destruct (Zabs_dec m) as [-> | ->]; trivial. Qed. Theorem Z_lt_abs_induction : @@ -73,16 +74,17 @@ Theorem Z_lt_abs_induction : Proof. intros P HP p. set (Q := fun z => 0 <= z -> P z /\ P (- z)) in *. - cut (Q (Z.abs p)); [ intros | apply (Z_lt_induction Q); auto with zarith ]. - elim (Zabs_dec p); intro eq; rewrite eq; elim H; auto with zarith. - unfold Q; clear Q; intros. + enough (Q (Z.abs p)) by + (destruct (Zabs_dec p) as [-> | ->]; elim H; auto with zarith). + apply (Z_lt_induction Q); auto with zarith. + subst Q; intros. split; apply HP. - rewrite Z.abs_eq; auto; intros. - elim (H (Z.abs m)); intros; auto with zarith. - elim (Zabs_dec m); intro eq; rewrite eq; trivial. - rewrite Z.abs_neq, Z.opp_involutive; auto with zarith; intros. - elim (H (Z.abs m)); intros; auto with zarith. - elim (Zabs_dec m); intro eq; rewrite eq; trivial. + - rewrite Z.abs_eq; auto; intros. + elim (H (Z.abs m)); intros; auto with zarith. + elim (Zabs_dec m); intro eq; rewrite eq; trivial. + - rewrite Z.abs_neq, Z.opp_involutive; auto with zarith; intros. + destruct (H (Z.abs m)); auto with zarith. + destruct (Zabs_dec m) as [-> | ->]; trivial. Qed. (** To do case analysis over the sign of [z] *) |