aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-05-05 15:13:04 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-05-05 15:13:04 +0000
commit959543f6f899f0384394f9770abbf17649f69b81 (patch)
tree46dc4791f1799a3b2095bec6d887d9aa54f42ad3 /theories
parentd2bd5d87d23d443f6e41496bdfe5f8e82d675634 (diff)
BinInt: Z.add become the alternative Z.add'
It relies on Z.pos_sub instead of a Pos.compare followed by Pos.sub. Proofs seem to be quite easy to adapt, via some rewrite Z.pos_sub_spec. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14107 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories')
-rw-r--r--theories/QArith/Qpower.v4
-rw-r--r--theories/Reals/RIneq.v3
-rw-r--r--theories/Reals/Rfunctions.v10
-rw-r--r--theories/ZArith/BinInt.v207
-rw-r--r--theories/ZArith/BinIntDef.v73
-rw-r--r--theories/ZArith/Zeven.v2
-rw-r--r--theories/ZArith/Zmax.v2
-rw-r--r--theories/ZArith/Znat.v2
8 files changed, 132 insertions, 171 deletions
diff --git a/theories/QArith/Qpower.v b/theories/QArith/Qpower.v
index 188a74fdd..b05ee6495 100644
--- a/theories/QArith/Qpower.v
+++ b/theories/QArith/Qpower.v
@@ -136,9 +136,9 @@ Proof.
intros a [|n|n] [|m|m] H; simpl; try ring;
try rewrite Qpower_plus_positive;
try apply Qinv_mult_distr; try reflexivity;
-case_eq ((n ?= m)%positive); intros H0; simpl;
+rewrite ?Z.pos_sub_spec;
+case Pos.compare_spec; intros H0; simpl; subst;
try rewrite Qpower_minus_positive;
- try rewrite (Pcompare_Eq_eq _ _ H0);
try (field; try split; apply Qpower_not_0_positive);
try assumption;
apply ZC2;
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v
index de41fd3f6..70f4ff0d9 100644
--- a/theories/Reals/RIneq.v
+++ b/theories/Reals/RIneq.v
@@ -1717,7 +1717,8 @@ Qed.
Lemma plus_IZR_NEG_POS :
forall p q:positive, IZR (Zpos p + Zneg q) = IZR (Zpos p) + IZR (Zneg q).
Proof.
- intros p q; simpl. case Pcompare_spec; intros H; simpl.
+ intros p q; simpl. rewrite Z.pos_sub_spec.
+ case Pcompare_spec; intros H; simpl.
subst. ring.
rewrite Pminus_minus by trivial.
rewrite minus_INR by (now apply lt_le_weak, Plt_lt).
diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v
index 1eee8d852..c0cd78649 100644
--- a/theories/Reals/Rfunctions.v
+++ b/theories/Reals/Rfunctions.v
@@ -557,6 +557,7 @@ Proof.
(* POS/POS *)
rewrite Pplus_plus; auto with real.
(* POS/NEG *)
+ rewrite Z.pos_sub_spec.
case Pcompare_spec; intros; simpl.
subst; auto with real.
rewrite Pminus_minus by trivial.
@@ -568,16 +569,17 @@ Proof.
rewrite plus_comm, le_plus_minus_r by (now apply lt_le_weak, Plt_lt).
reflexivity.
(* NEG/POS *)
+ rewrite Z.pos_sub_spec.
case Pcompare_spec; intros; simpl.
subst; auto with real.
rewrite Pminus_minus by trivial.
- rewrite (pow_RN_plus x _ (nat_of_P n1)) by auto with real.
- rewrite plus_comm, le_plus_minus_r by (now apply lt_le_weak, Plt_lt).
- auto with real.
- rewrite Pminus_minus by trivial.
rewrite (pow_RN_plus x _ (nat_of_P m1)) by auto with real.
rewrite plus_comm, le_plus_minus_r by (now apply lt_le_weak, Plt_lt).
rewrite Rinv_mult_distr, Rinv_involutive; auto with real.
+ rewrite Pminus_minus by trivial.
+ rewrite (pow_RN_plus x _ (nat_of_P n1)) by auto with real.
+ rewrite plus_comm, le_plus_minus_r by (now apply lt_le_weak, Plt_lt).
+ auto with real.
(* NEG/NEG *)
rewrite Pplus_plus; auto with real.
intros H'; rewrite pow_add; auto with real.
diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v
index b9ae45110..62f5a0f78 100644
--- a/theories/ZArith/BinInt.v
+++ b/theories/ZArith/BinInt.v
@@ -69,11 +69,18 @@ Proof.
decide equality; apply Pos.eq_dec.
Defined.
-(** * Equivalence with alternative [add'] [succ'] [pred'] *)
+(** * Properties of [pos_sub] *)
-(** ** Caracterisation of [pos_sub] *)
+(** [pos_sub] can be written in term of positive comparison
+ and subtraction (cf. earlier definition of addition of Z) *)
-Lemma pos_sub_spec p q : pos_sub p q = Zpos p + Zneg q.
+Lemma pos_sub_spec p q :
+ pos_sub p q =
+ match (p ?= q)%positive with
+ | Eq => 0
+ | Lt => Zneg (q - p)
+ | Gt => Zpos (p - q)
+ end.
Proof.
revert q. induction p; destruct q; simpl; trivial;
rewrite ?Pos.compare_xI_xI, ?Pos.compare_xO_xI,
@@ -84,24 +91,29 @@ Proof.
subst; unfold Pos.sub; simpl; now rewrite Pos.sub_mask_diag.
Qed.
-Lemma add_add' n m : n + m = add' n m.
+(** Particular cases of the previous result *)
+
+Lemma pos_sub_diag p : pos_sub p p = 0.
Proof.
- symmetry.
- destruct n as [|n|n], m as [|m|m]; simpl add'; rewrite ?pos_sub_spec;
- trivial.
- simpl. rewrite Pos.compare_antisym. now case Pos.compare.
+ now rewrite pos_sub_spec, Pos.compare_refl.
Qed.
-Lemma succ_succ' n : succ n = succ' n.
+Lemma pos_sub_lt p q : (p < q)%positive -> pos_sub p q = Zneg (q - p).
Proof.
- unfold succ. rewrite add_add'. destruct n; trivial.
- simpl. f_equal. apply Pos.add_1_r.
+ intros H. now rewrite pos_sub_spec, H.
Qed.
-Lemma pred_pred' n : pred n = pred' n.
+Lemma pos_sub_gt p q : (q < p)%positive -> pos_sub p q = Zpos (p - q).
Proof.
- unfold pred. rewrite add_add'. destruct n; trivial.
- simpl. f_equal. apply Pos.add_1_r.
+ intros H. now rewrite pos_sub_spec, Pos.compare_antisym, H.
+Qed.
+
+(** The opposite of [pos_sub] is [pos_sub] with reversed arguments *)
+
+Lemma pos_sub_opp p q : - pos_sub p q = pos_sub q p.
+Proof.
+ revert q; induction p; destruct q; simpl; trivial;
+ rewrite <- IHp; now destruct pos_sub.
Qed.
(** * Results concerning [Zpos] and [Zneg] and the operators *)
@@ -131,9 +143,19 @@ Proof.
reflexivity.
Qed.
+Lemma add_Zpos_Zneg p q : Zpos p + Zneg q = pos_sub p q.
+Proof.
+ reflexivity.
+Qed.
+
+Lemma add_Zneg_Zpos p q : Zneg p + Zpos q = pos_sub q p.
+Proof.
+ reflexivity.
+Qed.
+
Lemma sub_Zpos n m : (n < m)%positive -> Zpos m - Zpos n = Zpos (m-n).
Proof.
- intros H. simpl. now rewrite Pos.compare_antisym, H.
+ intros H. simpl. now apply pos_sub_gt.
Qed.
Lemma mul_Zpos (p q : positive) : Zpos p * Zpos q = Zpos (p*q).
@@ -196,7 +218,6 @@ Qed.
Lemma add_comm n m : n + m = m + n.
Proof.
- rewrite !add_add'.
destruct n, m; simpl; trivial; now rewrite Pos.add_comm.
Qed.
@@ -204,57 +225,57 @@ Qed.
Lemma opp_add_distr n m : - (n + m) = - n + - m.
Proof.
- destruct n, m; simpl; trivial; now case Pos.compare_spec.
+ destruct n, m; simpl; trivial using pos_sub_opp.
+Qed.
+
+(** ** Opposite is injective *)
+
+Lemma opp_inj n m : -n = -m -> n = m.
+Proof.
+ destruct n, m; simpl; intros H; destr_eq H; now f_equal.
Qed.
(** ** Addition is associative *)
-Lemma add_assoc_pos (p q:positive)(n:Z) :
- Zpos p + (Zpos q + n) = Zpos p + Zpos q + n.
+Lemma pos_sub_add p q r :
+ pos_sub (p + q) r = Zpos p + pos_sub q r.
Proof.
- destruct n as [|n|n]; simpl; trivial.
- now rewrite Pos.add_assoc.
- case Pos.compare_spec; intros E0.
- (* y = z *)
+ simpl. rewrite !pos_sub_spec.
+ case (Pos.compare_spec q r); intros E0.
+ (* q = r *)
subst.
- assert (H := Pos.lt_add_r n p).
+ assert (H := Pos.lt_add_r r p).
rewrite Pos.add_comm in H. apply Pos.lt_gt in H.
now rewrite H, Pos.add_sub.
- (* y < z *)
- assert (Hz : (n = (n-q)+q)%positive) by (now rewrite Pos.sub_add).
- rewrite Hz at 4. rewrite Pos.add_compare_mono_r.
+ (* q < r *)
+ rewrite pos_sub_spec.
+ assert (Hr : (r = (r-q)+q)%positive) by (now rewrite Pos.sub_add).
+ rewrite Hr at 1. rewrite Pos.add_compare_mono_r.
case Pos.compare_spec; intros E1; trivial; f_equal.
- symmetry. rewrite Pos.add_comm. apply Pos.sub_add_distr.
- rewrite Hz, Pos.add_comm. now apply Pos.add_lt_mono_r.
- apply Pos.sub_sub_distr; trivial.
- (* z < y *)
- assert (LT : (n < p + q)%positive).
+ rewrite Pos.add_comm. apply Pos.sub_add_distr.
+ rewrite Hr, Pos.add_comm. now apply Pos.add_lt_mono_r.
+ symmetry. apply Pos.sub_sub_distr; trivial.
+ (* r < q *)
+ assert (LT : (r < p + q)%positive).
apply Pos.lt_trans with q; trivial. rewrite Pos.add_comm. apply Pos.lt_add_r.
apply Pos.lt_gt in LT. rewrite LT. f_equal.
- now apply Pos.add_sub_assoc.
+ symmetry. now apply Pos.add_sub_assoc.
Qed.
Lemma add_assoc n m p : n + (m + p) = n + m + p.
Proof.
- destruct n as [|x|x], m as [|y|y], p as [|z|z]; trivial.
- apply add_assoc_pos.
- apply add_assoc_pos.
- now rewrite !add_0_r.
- rewrite 2 (add_comm _ (Zpos z)), 2 add_assoc_pos.
- f_equal; apply add_comm.
- rewrite <- !opp_Zpos, <- (opp_Zneg x), <- !opp_add_distr. f_equal.
- rewrite 2 (add_comm (Zneg x)), 2 (add_comm _ (Zpos z)).
- now rewrite add_assoc_pos.
- now rewrite !add_0_r.
- rewrite 2 (add_comm (Zneg x)), 2 (add_comm _ (Zpos z)).
- now rewrite add_assoc_pos.
- rewrite <- !opp_Zpos, <- (opp_Zneg y), <- !opp_add_distr. f_equal.
- rewrite 2 (add_comm _ (Zpos z)), 2 add_assoc_pos.
- f_equal; apply add_comm.
- rewrite <- !opp_Zpos, <- (opp_Zneg z), <- !opp_add_distr. f_equal.
- apply add_assoc_pos.
- rewrite <- !opp_Zpos, <- !opp_add_distr. f_equal.
- apply add_assoc_pos.
+ assert (AUX : forall x y z, Zpos x + (y + z) = Zpos x + y + z).
+ intros x [|y|y] [|z|z]; rewrite ?add_0_r; trivial.
+ simpl. now rewrite Pos.add_assoc.
+ simpl (_ + Zneg _). symmetry. apply pos_sub_add.
+ simpl (Zneg _ + _); simpl (_ + Zneg _).
+ now rewrite (add_comm _ (Zpos _)), <- 2 pos_sub_add, Pos.add_comm.
+ apply opp_inj. rewrite !opp_add_distr, opp_Zpos, !opp_Zneg.
+ simpl (Zneg _ + _); simpl (_ + Zneg _).
+ rewrite add_comm, Pos.add_comm. apply pos_sub_add.
+ (* main *)
+ destruct n as [|n|n]. trivial. apply AUX.
+ apply opp_inj. rewrite !opp_add_distr, opp_Zneg. apply AUX.
Qed.
(** ** Subtraction and successor *)
@@ -268,7 +289,7 @@ Qed.
Lemma add_opp_diag_r n : n + - n = 0.
Proof.
- destruct n; simpl; trivial; now rewrite Pos.compare_refl.
+ destruct n; simpl; trivial; now rewrite pos_sub_diag.
Qed.
Lemma add_opp_diag_l n : - n + n = 0.
@@ -330,8 +351,8 @@ Lemma mul_add_distr_pos (p:positive) n m :
Zpos p * (n + m) = Zpos p * n + Zpos p * m.
Proof.
destruct n as [|n|n], m as [|m|m]; simpl; trivial;
- rewrite ?Pos.mul_compare_mono_l; try case Pos.compare_spec; intros;
- now rewrite ?Pos.mul_add_distr_l, ?Pos.mul_sub_distr_l.
+ rewrite ?pos_sub_spec, ?Pos.mul_compare_mono_l; try case Pos.compare_spec;
+ intros; now rewrite ?Pos.mul_add_distr_l, ?Pos.mul_sub_distr_l.
Qed.
Lemma mul_add_distr_l n m p : n * (m + p) = n * m + n * p.
@@ -384,7 +405,7 @@ Qed.
Lemma opp_succ n : -(succ n) = pred (-n).
Proof.
- unfold succ, pred. destruct n; simpl; trivial. now case Pos.compare_spec.
+ unfold succ, pred. apply opp_add_distr.
Qed.
(** ** Specification of successor and predecessor *)
@@ -451,8 +472,8 @@ Qed.
Lemma compare_sub n m : (n ?= m) = (n - m ?= 0).
Proof.
- destruct n as [|n|n], m as [|m|m]; simpl; trivial.
- case Pos.compare_spec; trivial.
+ destruct n as [|n|n], m as [|m|m]; simpl; trivial;
+ rewrite <- ? Pos.compare_antisym, ?pos_sub_spec;
case Pos.compare_spec; trivial.
Qed.
@@ -675,7 +696,7 @@ Lemma odd_spec n : odd n = true <-> Odd n.
Proof.
split.
exists (div2 n). destruct n as [|[ | | ]|[ | | ]]; simpl; try easy.
- now rewrite Pos.double_succ, Pos.sub_1_r, Pos.pred_succ.
+ now rewrite Pos.pred_double_succ.
intros (m,->). now destruct m as [|[ | | ]|[ | | ]].
Qed.
@@ -797,7 +818,7 @@ Proof.
now split.
split. unfold le.
now rewrite <- compare_antisym, <- compare_sub, compare_antisym, Hr'.
- unfold lt in *; simpl in *. rewrite Pos.compare_antisym, Hr'.
+ unfold lt in *; simpl in *. rewrite pos_sub_gt by trivial.
simpl. now apply Pos.sub_decr.
Qed.
@@ -813,8 +834,8 @@ Proof.
destruct r as [|r|r]; (now destruct Hr) || clear Hr.
now split.
split.
- unfold lt in *; simpl in *. rewrite Pos.compare_antisym, Hr'.
- simpl. rewrite <- Pos.compare_antisym. now apply Pos.sub_decr.
+ unfold lt in *; simpl in *. rewrite pos_sub_lt by trivial.
+ rewrite <- Pos.compare_antisym. now apply Pos.sub_decr.
change (Zneg b - Zneg r <= 0). unfold le, lt in *.
rewrite <- compare_sub. simpl in *.
now rewrite <- Pos.compare_antisym, Hr'.
@@ -1093,7 +1114,7 @@ Proof.
red. now rewrite <- compare_antisym, <- compare_sub, compare_antisym.
assert (EQ : to_N (Zpos m - Zpos n) = (Npos m - Npos n)%N).
red in H. simpl in H. simpl to_N.
- rewrite Pos.compare_antisym.
+ rewrite pos_sub_spec, Pos.compare_antisym.
destruct (Pos.compare_spec n m) as [H'|H'|H']; try (now destruct H).
subst. now rewrite N.sub_diag.
simpl. destruct (Pos.sub_mask_pos' m n H') as (p & -> & <-).
@@ -1207,49 +1228,23 @@ Proof.
destruct n. trivial. simpl. now rewrite Pos.add_1_r.
Qed.
-(** ** Properties of [succ'] and [pred'] *)
-
-Lemma succ'_pred' n : succ' (pred' n) = n.
-Proof.
- rewrite <- succ_succ', <- pred_pred'. apply succ_pred.
-Qed.
-
-Lemma pred'_succ' n : pred' (succ' n) = n.
-Proof.
- rewrite <- succ_succ', <- pred_pred'. apply pred_succ.
-Qed.
-
-Lemma succ'_inj n m : succ' n = succ' m -> n = m.
-Proof.
- intros H. now rewrite <- (pred'_succ' n), <- (pred'_succ' m), H.
-Qed.
-
-Lemma pred'_inj n m : pred' n = pred' m -> n = m.
-Proof.
- intros H. now rewrite <- (succ'_pred' n), <- (succ'_pred' m), H.
-Qed.
-
-Lemma neq_succ'_diag_r n : n <> succ' n.
-Proof.
- rewrite <- succ_succ'. rewrite <- compare_eq_iff.
- rewrite compare_sub, sub_succ_r. unfold sub. now rewrite add_opp_diag_r.
-Qed.
-
(** ** Induction principles based on successor / predecessor *)
Lemma peano_ind (P : Z -> Prop) :
P 0 ->
- (forall x, P x -> P (succ' x)) ->
- (forall x, P x -> P (pred' x)) ->
+ (forall x, P x -> P (succ x)) ->
+ (forall x, P x -> P (pred x)) ->
forall z, P z.
Proof.
intros H0 Hs Hp z; destruct z.
assumption.
induction p using Pos.peano_ind.
now apply (Hs 0).
+ rewrite <- Pos.add_1_r.
now apply (Hs (Zpos p)).
induction p using Pos.peano_ind.
now apply (Hp 0).
+ rewrite <- Pos.add_1_r.
now apply (Hp (Zneg p)).
Qed.
@@ -1261,8 +1256,8 @@ Lemma bi_induction (P : Z -> Prop) :
Proof.
intros _ H0 Hs. induction z using peano_ind.
assumption.
- rewrite <- succ_succ'. now apply -> Hs.
- rewrite <- pred_pred'. apply Hs. now rewrite succ_pred.
+ now apply -> Hs.
+ apply Hs. now rewrite succ_pred.
Qed.
@@ -1403,7 +1398,10 @@ Notation Zdouble_plus_one := Z.succ_double (only parsing).
Notation Zdouble_minus_one := Z.pred_double (only parsing).
Notation Zdouble := Z.double (only parsing).
Notation ZPminus := Z.pos_sub (only parsing).
-Notation Zplus := Z.add (only parsing).
+Notation Zsucc' := Z.succ (only parsing).
+Notation Zpred' := Z.pred (only parsing).
+Notation Zplus' := Z.add (only parsing).
+Notation Zplus := Z.add (only parsing). (* Slightly incompatible *)
Notation Zopp := Z.opp (only parsing).
Notation Zsucc := Z.succ (only parsing).
Notation Zpred := Z.pred (only parsing).
@@ -1411,9 +1409,6 @@ Notation Zminus := Z.sub (only parsing).
Notation Zmult := Z.mul (only parsing).
Notation Zcompare := Z.compare (only parsing).
Notation Zsgn := Z.sgn (only parsing).
-Notation Zsucc' := Z.succ' (only parsing).
-Notation Zpred' := Z.pred' (only parsing).
-Notation Zplus' := Z.add' (only parsing).
Notation Zle := Z.le (only parsing).
Notation Zge := Z.ge (only parsing).
Notation Zlt := Z.lt (only parsing).
@@ -1445,13 +1440,11 @@ Notation Zplus_succ_l := Z.add_succ_l (only parsing).
Notation Zplus_succ_comm := Z.add_succ_comm (only parsing).
Notation Zsucc_discr := Z.neq_succ_diag_r (only parsing).
Notation Zsucc_inj := Z.succ_inj (only parsing).
-Notation Zsucc_succ' := Z.succ_succ' (only parsing).
-Notation Zpred_pred' := Z.pred_pred' (only parsing).
-Notation Zsucc'_inj := Z.succ'_inj (only parsing).
-Notation Zsucc'_pred' := Z.succ'_pred' (only parsing).
-Notation Zpred'_succ' := Z.pred'_succ' (only parsing).
-Notation Zpred'_inj := Z.pred'_inj (only parsing).
-Notation Zsucc'_discr := Z.neq_succ'_diag_r (only parsing).
+Notation Zsucc'_inj := Z.succ_inj (only parsing).
+Notation Zsucc'_pred' := Z.succ_pred (only parsing).
+Notation Zpred'_succ' := Z.pred_succ (only parsing).
+Notation Zpred'_inj := Z.pred_inj (only parsing).
+Notation Zsucc'_discr := Z.neq_succ_diag_r (only parsing).
Notation Zminus_0_r := Z.sub_0_r (only parsing).
Notation Zminus_diag := Z.sub_diag (only parsing).
Notation Zminus_plus_distr := Z.sub_add_distr (only parsing).
@@ -1576,6 +1569,8 @@ Zplus_0_simpl_l
Zplus_0_simpl_l_reverse
Zplus_opp_expand
Zsucc_inj_contrapositive
+Zsucc_succ'
+Zpred_pred'
*)
(* No compat notation for :
diff --git a/theories/ZArith/BinIntDef.v b/theories/ZArith/BinIntDef.v
index b0fef2a9d..4c2a19f69 100644
--- a/theories/ZArith/BinIntDef.v
+++ b/theories/ZArith/BinIntDef.v
@@ -51,26 +51,30 @@ Definition pred_double x :=
| Zpos p => Zpos (Pos.pred_double p)
end.
+(** ** Subtraction of positive into Z *)
+
+Fixpoint pos_sub (x y:positive) {struct y} : Z :=
+ match x, y with
+ | p~1, q~1 => double (pos_sub p q)
+ | p~1, q~0 => succ_double (pos_sub p q)
+ | p~1, 1 => Zpos p~0
+ | p~0, q~1 => pred_double (pos_sub p q)
+ | p~0, q~0 => double (pos_sub p q)
+ | p~0, 1 => Zpos (Pos.pred_double p)
+ | 1, q~1 => Zneg q~0
+ | 1, q~0 => Zneg (Pos.pred_double q)
+ | 1, 1 => Z0
+ end%positive.
+
(** ** Addition *)
Definition add x y :=
match x, y with
| 0, y => y
- | Zpos x', 0 => Zpos x'
- | Zneg x', 0 => Zneg x'
+ | x, 0 => x
| Zpos x', Zpos y' => Zpos (x' + y')
- | Zpos x', Zneg y' =>
- match (x' ?= y')%positive with
- | Eq => 0
- | Lt => Zneg (y' - x')
- | Gt => Zpos (x' - y')
- end
- | Zneg x', Zpos y' =>
- match (x' ?= y')%positive with
- | Eq => 0
- | Lt => Zpos (y' - x')
- | Gt => Zneg (x' - y')
- end
+ | Zpos x', Zneg y' => pos_sub x' y'
+ | Zneg x', Zpos y' => pos_sub y' x'
| Zneg x', Zneg y' => Zneg (x' + y')
end.
@@ -115,47 +119,6 @@ Definition mul x y :=
Infix "*" := mul : Z_scope.
-(** ** Subtraction of positive into Z *)
-
-Fixpoint pos_sub (x y:positive) {struct y} : Z :=
- match x, y with
- | p~1, q~1 => double (pos_sub p q)
- | p~1, q~0 => succ_double (pos_sub p q)
- | p~1, 1 => Zpos p~0
- | p~0, q~1 => pred_double (pos_sub p q)
- | p~0, q~0 => double (pos_sub p q)
- | p~0, 1 => Zpos (Pos.pred_double p)
- | 1, q~1 => Zneg q~0
- | 1, q~0 => Zneg (Pos.pred_double q)
- | 1, 1 => Z0
- end%positive.
-
-(** ** Direct, easier to handle variants of successor and addition *)
-
-Definition succ' x :=
- match x with
- | 0 => 1
- | Zpos x' => Zpos (Pos.succ x')
- | Zneg x' => pos_sub 1 x'
- end.
-
-Definition pred' x :=
- match x with
- | 0 => -1
- | Zpos x' => pos_sub x' 1
- | Zneg x' => Zneg (Pos.succ x')
- end.
-
-Definition add' x y :=
- match x, y with
- | 0, y => y
- | x, 0 => x
- | Zpos x', Zpos y' => Zpos (x' + y')
- | Zpos x', Zneg y' => pos_sub x' y'
- | Zneg x', Zpos y' => pos_sub y' x'
- | Zneg x', Zneg y' => Zneg (x' + y')
- end.
-
(** ** Power function *)
Definition pow_pos (z:Z) (n:positive) := Pos.iter n (mul z) 1.
diff --git a/theories/ZArith/Zeven.v b/theories/ZArith/Zeven.v
index ef91f2d77..d37a6a9c3 100644
--- a/theories/ZArith/Zeven.v
+++ b/theories/ZArith/Zeven.v
@@ -169,7 +169,7 @@ Lemma Zdiv2_odd_eqn : forall n,
n = 2*(Zdiv2 n) + if Zodd_bool n then 1 else 0.
Proof.
intros [ |[p|p| ]|[p|p| ]]; simpl; trivial.
- f_equal. now rewrite xO_succ_permute, <-Ppred_minus, Ppred_succ.
+ f_equal. symmetry. apply Pos.pred_double_succ.
Qed.
Lemma Zeven_div2 : forall n:Z, Zeven n -> n = 2 * Zdiv2 n.
diff --git a/theories/ZArith/Zmax.v b/theories/ZArith/Zmax.v
index a4b5390e3..87a14a136 100644
--- a/theories/ZArith/Zmax.v
+++ b/theories/ZArith/Zmax.v
@@ -97,7 +97,7 @@ Qed.
Lemma Zpos_minus : forall p q, Zpos (Pminus p q) = Zmax 1 (Zpos p - Zpos q).
Proof.
- intros; simpl. case Pos.compare_spec; intros H.
+ intros; simpl. rewrite Z.pos_sub_spec. case Pos.compare_spec; intros H.
now rewrite H, Pos.sub_diag.
rewrite Pminus_Lt; auto.
symmetry. apply Zpos_max_1.
diff --git a/theories/ZArith/Znat.v b/theories/ZArith/Znat.v
index 454f62aa9..353ab602e 100644
--- a/theories/ZArith/Znat.v
+++ b/theories/ZArith/Znat.v
@@ -318,7 +318,7 @@ Qed.
Lemma Z_of_N_minus : forall n m, Z_of_N (n-m) = Zmax 0 (Z_of_N n - Z_of_N m).
Proof.
- intros [|n] [|m]; simpl; trivial.
+ intros [|n] [|m]; simpl; trivial. rewrite Z.pos_sub_spec.
case Pcompare_spec; intros H.
subst. now rewrite Pminus_mask_diag.
rewrite Pminus_mask_Lt; trivial.