diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-14 15:17:04 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-17 12:41:14 +0200 |
commit | a53b44aa042cfded28c34205074f194de7e2e4ee (patch) | |
tree | 1f155c4f0e76897fae441bc4c55e9f71cb791712 /theories | |
parent | 63d0047f903020735dd6a814c35278ff53d0625f (diff) |
Essai où assert_style n'est utilisé que si pas visuellement une équation;
Diffstat (limited to 'theories')
-rw-r--r-- | theories/QArith/Qreduction.v | 6 | ||||
-rw-r--r-- | theories/ZArith/Zcomplements.v | 14 |
2 files changed, 10 insertions, 10 deletions
diff --git a/theories/QArith/Qreduction.v b/theories/QArith/Qreduction.v index 2aac617eb..7d8ed5275 100644 --- a/theories/QArith/Qreduction.v +++ b/theories/QArith/Qreduction.v @@ -46,12 +46,12 @@ Proof. generalize (Z.ggcd_gcd a ('b)) (Zgcd_is_gcd a ('b)) (Z.gcd_nonneg a ('b)) (Z.ggcd_correct_divisors a ('b)). destruct (Z.ggcd a (Zpos b)) as (g,(aa,bb)). - simpl. intros <- Hg1 Hg2 (Hg3,Hg4). - assert (Hg0 : g <> 0) by (intro; now subst g). + simpl. intros <- Hg1 Hg2 (Hg3,Hg4). clear H0. + assert (Hg0 : g <> 0). (intro; now subst g). Show Proof. generalize (Z.ggcd_gcd c ('d)) (Zgcd_is_gcd c ('d)) (Z.gcd_nonneg c ('d)) (Z.ggcd_correct_divisors c ('d)). destruct (Z.ggcd c (Zpos d)) as (g',(cc,dd)). - simpl. intros <- Hg'1 Hg'2 (Hg'3,Hg'4). + simpl. intros <- Hg'1 Hg'2 (Hg'3,Hg'4). clear H0. assert (Hg'0 : g' <> 0) by (intro; now subst g'). elim (rel_prime_cross_prod aa bb cc dd). diff --git a/theories/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v index 99b631905..be975e882 100644 --- a/theories/ZArith/Zcomplements.v +++ b/theories/ZArith/Zcomplements.v @@ -54,17 +54,17 @@ Theorem Z_lt_abs_rec : Proof. intros P HP p. 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). + enough (H:Q (Z.abs p)) by admit. +(* (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. destruct (H (Z.abs m)); auto with zarith. - destruct (Zabs_dec m) as [-> | ->]; trivial. + (* destruct (Zabs_dec m) as [-> | ->]; trivial. *) admit. - 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. + destruct (Zabs_dec m) as [-> | ->]; trivial; admit. Qed. Theorem Z_lt_abs_induction : @@ -74,8 +74,8 @@ Theorem Z_lt_abs_induction : Proof. intros P HP p. set (Q := fun z => 0 <= z -> P z /\ P (- z)) in *. - enough (Q (Z.abs p)) by - (destruct (Zabs_dec p) as [-> | ->]; elim H; auto with zarith). + enough (Q (Z.abs p)) by admit. +(* (destruct (Zabs_dec p) as [-> | ->]; elim H; auto with zarith).*) apply (Z_lt_induction Q); auto with zarith. subst Q; intros. split; apply HP. @@ -84,7 +84,7 @@ Proof. 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. + destruct (Zabs_dec m) as [-> | ->]; trivial; admit. Qed. (** To do case analysis over the sign of [z] *) |