aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Numbers
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Numbers')
-rw-r--r--theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v2
-rw-r--r--theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v3
-rw-r--r--theories/Numbers/Cyclic/Int31/Cyclic31.v43
-rw-r--r--theories/Numbers/NatInt/NZDomain.v38
-rw-r--r--theories/Numbers/Natural/BigN/Nbasic.v2
5 files changed, 46 insertions, 42 deletions
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v
index ed69a8f57..fe77bf5c7 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v
@@ -287,7 +287,7 @@ Section DoubleBase.
Lemma double_wB_wwB : forall n, double_wB n * double_wB n = double_wB (S n).
Proof.
intros n;unfold double_wB;simpl.
- unfold base. rewrite Pshiftl_nat_S, (Pos2Z.inj_xO (_ << _)).
+ unfold base. rewrite (Pos2Z.inj_xO (_ << _)).
replace (2 * Zpos (w_digits << n)) with
(Zpos (w_digits << n) + Zpos (w_digits << n)) by ring.
symmetry; apply Zpower_exp;intro;discriminate.
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v
index 5cb7405a6..23cbd1e8c 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v
@@ -160,7 +160,7 @@ Section GENDIVN1.
Lemma p_lt_double_digits : forall n, [|p|] <= Zpos (w_digits << n).
Proof.
induction n;simpl. trivial.
- case (spec_to_Z p); rewrite Pshiftl_nat_S, Pos2Z.inj_xO;auto with zarith.
+ case (spec_to_Z p); rewrite Pos2Z.inj_xO;auto with zarith.
Qed.
Lemma spec_double_divn1_p : forall n r h l,
@@ -305,7 +305,6 @@ Section GENDIVN1.
Lemma spec_double_digits:forall n, Zpos w_digits <= Zpos (w_digits << n).
Proof.
induction n;simpl;auto with zarith.
- rewrite Pshiftl_nat_S.
change (Zpos (xO (w_digits << n))) with
(2*Zpos (w_digits << n)).
assert (0 < Zpos w_digits) by reflexivity.
diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v
index 0284af7aa..5aa31d7bd 100644
--- a/theories/Numbers/Cyclic/Int31/Cyclic31.v
+++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v
@@ -86,14 +86,14 @@ Section Basics.
Lemma nshiftr_S_tail :
forall n x, nshiftr (S n) x = nshiftr n (shiftr x).
Proof.
- induction n; simpl; auto.
- intros; rewrite nshiftr_S, IHn, nshiftr_S; auto.
+ intros n; elim n; simpl; auto.
+ intros; now f_equal.
Qed.
Lemma nshiftr_n_0 : forall n, nshiftr n 0 = 0.
Proof.
induction n; simpl; auto.
- rewrite nshiftr_S, IHn; auto.
+ rewrite IHn; auto.
Qed.
Lemma nshiftr_size : forall x, nshiftr size x = 0.
@@ -108,7 +108,7 @@ Section Basics.
replace k with ((k-size)+size)%nat by omega.
induction (k-size)%nat; auto.
rewrite nshiftr_size; auto.
- simpl; rewrite nshiftr_S, IHn; auto.
+ simpl; rewrite IHn; auto.
Qed.
(** * Iterated shift to the left *)
@@ -124,14 +124,13 @@ Section Basics.
Lemma nshiftl_S_tail :
forall n x, nshiftl (S n) x = nshiftl n (shiftl x).
Proof.
- induction n; simpl; auto.
- intros; rewrite nshiftl_S, IHn, nshiftl_S; auto.
+ intros n; elim n; simpl; intros; now f_equal.
Qed.
Lemma nshiftl_n_0 : forall n, nshiftl n 0 = 0.
Proof.
induction n; simpl; auto.
- rewrite nshiftl_S, IHn; auto.
+ rewrite IHn; auto.
Qed.
Lemma nshiftl_size : forall x, nshiftl size x = 0.
@@ -146,7 +145,7 @@ Section Basics.
replace k with ((k-size)+size)%nat by omega.
induction (k-size)%nat; auto.
rewrite nshiftl_size; auto.
- simpl; rewrite nshiftl_S, IHn; auto.
+ simpl; rewrite IHn; auto.
Qed.
Lemma firstr_firstl :
@@ -176,7 +175,7 @@ Section Basics.
replace p with ((p-n)+n)%nat by omega.
induction (p-n)%nat.
simpl; auto.
- simpl; rewrite nshiftr_S; rewrite IHn0; auto.
+ simpl; rewrite IHn0; auto.
Qed.
Lemma nshiftr_0_firstl : forall n x, n < size ->
@@ -240,7 +239,7 @@ Section Basics.
recr_aux p A case0 caserec (nshiftr (size - n) x).
Proof.
induction n.
- simpl; intros.
+ simpl minus; intros.
rewrite nshiftr_size; destruct p; simpl; auto.
intros.
destruct p.
@@ -439,7 +438,7 @@ Section Basics.
(phibis_aux n (nshiftr (size-n) x) < 2 ^ (Z.of_nat n))%Z.
Proof.
induction n.
- simpl; unfold phibis_aux; simpl; auto with zarith.
+ simpl minus; unfold phibis_aux; simpl; auto with zarith.
intros.
unfold phibis_aux, recrbis_aux; fold recrbis_aux;
fold (phibis_aux n (shiftr (nshiftr (size - S n) x))).
@@ -529,7 +528,7 @@ Section Basics.
remember (k'-k)%nat as n.
clear Heqn H k'.
induction n; simpl; auto.
- rewrite 2 nshiftl_S; f_equal; auto.
+ f_equal; auto.
Qed.
Lemma EqShiftL_firstr : forall k x y, k < size ->
@@ -823,7 +822,7 @@ Section Basics.
nshiftr (size-n) x.
Proof.
induction n.
- intros; simpl.
+ intros; simpl minus.
rewrite nshiftr_size; auto.
intros.
unfold phibis_aux, recrbis_aux; fold recrbis_aux;
@@ -879,12 +878,12 @@ Section Basics.
Proof.
induction n.
simpl; intros; auto.
- simpl; intros.
- destruct p; simpl.
+ simpl p2ibis; intros.
+ destruct p; simpl snd.
specialize IHn with p.
- destruct (p2ibis n p); simpl in *.
- rewrite nshiftr_S_tail.
+ destruct (p2ibis n p). simpl snd in *.
+rewrite nshiftr_S_tail.
destruct (le_lt_dec size n).
rewrite nshiftr_above_size; auto.
assert (H:=nshiftr_0_firstl _ _ l IHn).
@@ -892,7 +891,7 @@ Section Basics.
destruct i; simpl in *; rewrite H; auto.
specialize IHn with p.
- destruct (p2ibis n p); simpl in *.
+ destruct (p2ibis n p); simpl snd in *.
rewrite nshiftr_S_tail.
destruct (le_lt_dec size n).
rewrite nshiftr_above_size; auto.
@@ -1525,14 +1524,14 @@ Section Int31_Specs.
unfold phibis_aux; simpl; rewrite H; fold (phibis_aux n (shiftr i));
generalize (phibis_aux_pos n (shiftr i)); intros;
set (z := phibis_aux n (shiftr i)) in *; clearbody z;
- rewrite <- iter_nat_plus.
+ rewrite <- nat_rect_plus.
f_equal.
rewrite Z.double_spec, <- Z.add_diag.
symmetry; apply Zabs2Nat.inj_add; auto with zarith.
- change (iter_nat (S (Z.abs_nat z + Z.abs_nat z)) A f a =
- iter_nat (Z.abs_nat (Z.succ_double z)) A f a); f_equal.
+ change (iter_nat (S (Z.abs_nat z) + (Z.abs_nat z))%nat A f a =
+ iter_nat (Z.abs_nat (Z.succ_double z)) A f a); f_equal.
rewrite Z.succ_double_spec, <- Z.add_diag.
rewrite Zabs2Nat.inj_add; auto with zarith.
rewrite Zabs2Nat.inj_add; auto with zarith.
@@ -1557,7 +1556,7 @@ Section Int31_Specs.
intros.
simpl addmuldiv31_alt.
replace (S n) with (n+1)%nat by (rewrite plus_comm; auto).
- rewrite iter_nat_plus; simpl; auto.
+ rewrite nat_rect_plus; simpl; auto.
Qed.
Lemma spec_add_mul_div : forall x y p, [|p|] <= Zpos 31 ->
diff --git a/theories/Numbers/NatInt/NZDomain.v b/theories/Numbers/NatInt/NZDomain.v
index 4b71d5390..cee2e3210 100644
--- a/theories/Numbers/NatInt/NZDomain.v
+++ b/theories/Numbers/NatInt/NZDomain.v
@@ -14,14 +14,12 @@ Require Import NZBase NZOrder NZAddOrder Plus Minus.
translation from Peano numbers [nat] into NZ.
*)
-(** First, some complements about [nat_iter] *)
+Local Notation "f ^ n" := (fun x => nat_rect _ x (fun _ => f) n).
-Local Notation "f ^ n" := (nat_iter n f).
-
-Instance nat_iter_wd n {A} (R:relation A) :
- Proper ((R==>R)==>R==>R) (nat_iter n).
+Instance nat_rect_wd n {A} (R:relation A) :
+ Proper (R==>(R==>R)==>R) (fun x f => nat_rect (fun _ => _) x (fun _ => f) n).
Proof.
-intros f f' Hf. induction n; simpl; red; auto.
+intros x y eq_xy f g eq_fg; induction n; [assumption | now apply eq_fg].
Qed.
Module NZDomainProp (Import NZ:NZDomainSig').
@@ -33,17 +31,24 @@ Include NZBaseProp NZ.
Lemma itersucc_or_itersucc n m : exists k, n == (S^k) m \/ m == (S^k) n.
Proof.
-nzinduct n m.
+revert n.
+apply central_induction with (z:=m).
+ { intros x y eq_xy; apply ex_iff_morphism.
+ intros n; apply or_iff_morphism.
+ + split; intros; etransitivity; try eassumption; now symmetry.
+ + split; intros; (etransitivity; [eassumption|]); [|symmetry];
+ (eapply nat_rect_wd; [eassumption|apply succ_wd]).
+ }
exists 0%nat. now left.
intros n. split; intros [k [L|R]].
exists (Datatypes.S k). left. now apply succ_wd.
destruct k as [|k].
simpl in R. exists 1%nat. left. now apply succ_wd.
-rewrite nat_iter_succ_r in R. exists k. now right.
+rewrite nat_rect_succ_r in R. exists k. now right.
destruct k as [|k]; simpl in L.
exists 1%nat. now right.
apply succ_inj in L. exists k. now left.
-exists (Datatypes.S k). right. now rewrite nat_iter_succ_r.
+exists (Datatypes.S k). right. now rewrite nat_rect_succ_r.
Qed.
(** Generalized version of [pred_succ] when iterating *)
@@ -53,7 +58,7 @@ Proof.
induction k.
simpl; auto with *.
simpl; intros. apply pred_wd in H. rewrite pred_succ in H. apply IHk in H; auto.
-rewrite <- nat_iter_succ_r in H; auto.
+rewrite <- nat_rect_succ_r in H; auto.
Qed.
(** From a given point, all others are iterated successors
@@ -319,7 +324,7 @@ Lemma ofnat_add : forall n m, [n+m] == [n]+[m].
Proof.
intros. rewrite ofnat_add_l.
induction n; simpl. reflexivity.
- rewrite ofnat_succ. now f_equiv.
+ now f_equiv.
Qed.
Lemma ofnat_mul : forall n m, [n*m] == [n]*[m].
@@ -327,15 +332,15 @@ Proof.
induction n; simpl; intros.
symmetry. apply mul_0_l.
rewrite plus_comm.
- rewrite ofnat_succ, ofnat_add, mul_succ_l.
+ rewrite ofnat_add, mul_succ_l.
now f_equiv.
Qed.
Lemma ofnat_sub_r : forall n m, n-[m] == (P^m) n.
Proof.
induction m; simpl; intros.
- rewrite ofnat_zero. apply sub_0_r.
- rewrite ofnat_succ, sub_succ_r. now f_equiv.
+ apply sub_0_r.
+ rewrite sub_succ_r. now f_equiv.
Qed.
Lemma ofnat_sub : forall n m, m<=n -> [n-m] == [n]-[m].
@@ -346,9 +351,10 @@ Proof.
intros.
destruct n.
inversion H.
- rewrite nat_iter_succ_r.
+ rewrite nat_rect_succ_r.
simpl.
- rewrite ofnat_succ, pred_succ; auto with arith.
+ etransitivity. apply IHm. auto with arith.
+ eapply nat_rect_wd; [symmetry;apply pred_succ|apply pred_wd].
Qed.
End NZOfNatOps.
diff --git a/theories/Numbers/Natural/BigN/Nbasic.v b/theories/Numbers/Natural/BigN/Nbasic.v
index 5bde10087..161f523ca 100644
--- a/theories/Numbers/Natural/BigN/Nbasic.v
+++ b/theories/Numbers/Natural/BigN/Nbasic.v
@@ -371,7 +371,7 @@ Section CompareRec.
intros n (H0, H); split; auto.
apply Z.lt_le_trans with (1:= H).
unfold double_wB, DoubleBase.double_wB; simpl.
- rewrite Pshiftl_nat_S, base_xO.
+ rewrite base_xO.
set (u := base (Pos.shiftl_nat wm_base n)).
assert (0 < u).
unfold u, base; auto with zarith.