aboutsummaryrefslogtreecommitdiff
path: root/theories/Numbers/Integer
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Numbers/Integer')
-rw-r--r--theories/Numbers/Integer/Abstract/ZAddOrder.v5
-rw-r--r--theories/Numbers/Integer/Abstract/ZLt.v2
-rw-r--r--theories/Numbers/Integer/Abstract/ZMulOrder.v24
-rw-r--r--theories/Numbers/Integer/Abstract/ZParity.v12
-rw-r--r--theories/Numbers/Integer/Abstract/ZPow.v12
-rw-r--r--theories/Numbers/Integer/BigZ/BigZ.v4
-rw-r--r--theories/Numbers/Integer/BigZ/ZMake.v5
-rw-r--r--theories/Numbers/Integer/Binary/ZBinary.v12
-rw-r--r--theories/Numbers/Integer/NatPairs/ZNatPairs.v38
-rw-r--r--theories/Numbers/Integer/SpecViaZ/ZSig.v4
-rw-r--r--theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v19
11 files changed, 90 insertions, 47 deletions
diff --git a/theories/Numbers/Integer/Abstract/ZAddOrder.v b/theories/Numbers/Integer/Abstract/ZAddOrder.v
index eb27e63782..b5ca908b40 100644
--- a/theories/Numbers/Integer/Abstract/ZAddOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZAddOrder.v
@@ -102,6 +102,11 @@ Proof.
intro n. rewrite (opp_le_mono 0 n). now rewrite opp_0.
Qed.
+Theorem lt_m1_0 : -(1) < 0.
+Proof.
+apply opp_neg_pos, lt_0_1.
+Qed.
+
Theorem sub_lt_mono_l : forall n m p, n < m <-> p - m < p - n.
Proof.
intros n m p. do 2 rewrite <- add_opp_r. rewrite <- add_lt_mono_l.
diff --git a/theories/Numbers/Integer/Abstract/ZLt.v b/theories/Numbers/Integer/Abstract/ZLt.v
index 540e17cb40..23eac0e699 100644
--- a/theories/Numbers/Integer/Abstract/ZLt.v
+++ b/theories/Numbers/Integer/Abstract/ZLt.v
@@ -125,7 +125,7 @@ Theorem lt_n1_r : forall n m, n < m -> m < 0 -> n < -(1).
Proof.
intros n m H1 H2. apply -> lt_le_pred in H2.
setoid_replace (P 0) with (-(1)) in H2. now apply lt_le_trans with m.
-apply <- eq_opp_r. now rewrite opp_pred, opp_0.
+apply <- eq_opp_r. now rewrite one_succ, opp_pred, opp_0.
Qed.
End ZOrderProp.
diff --git a/theories/Numbers/Integer/Abstract/ZMulOrder.v b/theories/Numbers/Integer/Abstract/ZMulOrder.v
index 76428584d7..25989b2d40 100644
--- a/theories/Numbers/Integer/Abstract/ZMulOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZMulOrder.v
@@ -177,22 +177,16 @@ Qed.
Theorem eq_mul_1 : forall n m, n * m == 1 -> n == 1 \/ n == -1.
Proof.
-assert (F : ~ 1 < -1).
-intro H.
-assert (H1 : -1 < 0). apply <- opp_neg_pos. apply lt_succ_diag_r.
-assert (H2 : 1 < 0) by now apply lt_trans with (-1).
-false_hyp H2 nlt_succ_diag_l.
+assert (F := lt_m1_0).
zero_pos_neg n.
-intros m H; rewrite mul_0_l in H; false_hyp H neq_succ_diag_r.
-intros n H; split; apply <- le_succ_l in H; le_elim H.
-intros m H1; apply (lt_1_mul_l n m) in H.
-rewrite H1 in H; destruct H as [H | [H | H]].
-false_hyp H F. false_hyp H neq_succ_diag_l. false_hyp H lt_irrefl.
-intros; now left.
-intros m H1; apply (lt_1_mul_l n m) in H. rewrite mul_opp_l in H1;
-apply -> eq_opp_l in H1. rewrite H1 in H; destruct H as [H | [H | H]].
-false_hyp H lt_irrefl. apply -> eq_opp_l in H. rewrite opp_0 in H.
-false_hyp H neq_succ_diag_l. false_hyp H F.
+(* n = 0 *)
+intros m. nzsimpl. now left.
+(* 0 < n, proving P n /\ P (-n) *)
+intros n Hn. rewrite <- le_succ_l, <- one_succ in Hn.
+le_elim Hn; split; intros m H.
+destruct (lt_1_mul_l n m) as [|[|]]; order'.
+rewrite mul_opp_l, eq_opp_l in H. destruct (lt_1_mul_l n m) as [|[|]]; order'.
+now left.
intros; right; symmetry; now apply opp_wd.
Qed.
diff --git a/theories/Numbers/Integer/Abstract/ZParity.v b/theories/Numbers/Integer/Abstract/ZParity.v
index 1ababfe5c8..4c752043c7 100644
--- a/theories/Numbers/Integer/Abstract/ZParity.v
+++ b/theories/Numbers/Integer/Abstract/ZParity.v
@@ -41,20 +41,20 @@ Proof.
intros x.
split; intros [(y,H)|(y,H)].
right. exists y. rewrite H. now nzsimpl.
- left. exists (S y). rewrite H. now nzsimpl.
+ left. exists (S y). rewrite H. now nzsimpl'.
right. exists (P y). rewrite <- succ_inj_wd. rewrite H.
- nzsimpl. now rewrite <- add_succ_l, <- add_succ_r, succ_pred.
+ nzsimpl'. now rewrite <- add_succ_l, <- add_succ_r, succ_pred.
left. exists y. rewrite <- succ_inj_wd. rewrite H. now nzsimpl.
Qed.
Lemma double_below : forall n m, n<=m -> 2*n < 2*m+1.
Proof.
- intros. nzsimpl. apply lt_succ_r. now apply add_le_mono.
+ intros. nzsimpl'. apply lt_succ_r. now apply add_le_mono.
Qed.
Lemma double_above : forall n m, n<m -> 2*n+1 < 2*m.
Proof.
- intros. nzsimpl.
+ intros. nzsimpl'.
rewrite <- le_succ_l, <- add_succ_l, <- add_succ_r.
apply add_le_mono; now apply le_succ_l.
Qed.
@@ -95,7 +95,7 @@ Qed.
Lemma odd_1 : odd 1 = true.
Proof.
- rewrite odd_spec. exists 0. now nzsimpl.
+ rewrite odd_spec. exists 0. now nzsimpl'.
Qed.
Lemma Odd_succ_Even : forall n, Odd (S n) <-> Even n.
@@ -140,7 +140,7 @@ Proof.
exists (n'+m'). now rewrite mul_add_distr_l, Hn, Hm.
exists (n'+m'). now rewrite mul_add_distr_l, Hn, Hm, add_assoc.
exists (n'+m'). now rewrite mul_add_distr_l, Hn, Hm, add_shuffle0.
- exists (n'+m'+1). rewrite Hm,Hn. nzsimpl. now rewrite add_shuffle1.
+ exists (n'+m'+1). rewrite Hm,Hn. nzsimpl'. now rewrite add_shuffle1.
Qed.
Lemma odd_add : forall n m, odd (n+m) = xorb (odd n) (odd m).
diff --git a/theories/Numbers/Integer/Abstract/ZPow.v b/theories/Numbers/Integer/Abstract/ZPow.v
index 9de681375d..782a110240 100644
--- a/theories/Numbers/Integer/Abstract/ZPow.v
+++ b/theories/Numbers/Integer/Abstract/ZPow.v
@@ -78,12 +78,10 @@ Lemma pow_opp_even : forall a b, Even b -> (-a)^b == a^b.
Proof.
intros a b (c,H). rewrite H.
destruct (le_gt_cases 0 c).
- assert (0 <= 2) by (apply le_le_succ_r, le_0_1).
- rewrite 2 pow_mul_r; trivial.
+ rewrite 2 pow_mul_r by order'.
rewrite 2 pow_2_r.
now rewrite mul_opp_opp.
- assert (2*c < 0).
- apply mul_pos_neg; trivial. rewrite lt_succ_r. apply le_0_1.
+ assert (2*c < 0) by (apply mul_pos_neg; order').
now rewrite !pow_neg.
Qed.
@@ -91,10 +89,8 @@ Lemma pow_opp_odd : forall a b, Odd b -> (-a)^b == -(a^b).
Proof.
intros a b (c,H). rewrite H.
destruct (le_gt_cases 0 c) as [LE|GT].
- assert (0 <= 2*c).
- apply mul_nonneg_nonneg; trivial.
- apply le_le_succ_r, le_0_1.
- rewrite add_succ_r, add_0_r, !pow_succ_r; trivial.
+ assert (0 <= 2*c) by (apply mul_nonneg_nonneg; order').
+ rewrite add_1_r, !pow_succ_r; trivial.
rewrite pow_opp_even by (now exists c).
apply mul_opp_l.
apply double_above in GT. rewrite mul_0_r in GT.
diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v
index 6c9dc77c10..92be49bdaf 100644
--- a/theories/Numbers/Integer/BigZ/BigZ.v
+++ b/theories/Numbers/Integer/BigZ/BigZ.v
@@ -70,6 +70,7 @@ Arguments Scope BigZ.gcd [bigZ_scope bigZ_scope].
Local Notation "0" := BigZ.zero : bigZ_scope.
Local Notation "1" := BigZ.one : bigZ_scope.
+Local Notation "2" := BigZ.two : bigZ_scope.
Infix "+" := BigZ.add : bigZ_scope.
Infix "-" := BigZ.sub : bigZ_scope.
Notation "- x" := (BigZ.opp x) : bigZ_scope.
@@ -171,6 +172,7 @@ Ltac isBigZcst t :=
| BigZ.Neg ?t => isBigNcst t
| BigZ.zero => constr:true
| BigZ.one => constr:true
+ | BigZ.two => constr:true
| BigZ.minus_one => constr:true
| _ => constr:false
end.
@@ -186,6 +188,7 @@ Ltac BigZ_to_N t :=
| BigZ.Pos ?t => BigN_to_N t
| BigZ.zero => constr:0%N
| BigZ.one => constr:1%N
+ | BigZ.two => constr:2%N
| _ => constr:NotConstant
end.
@@ -198,7 +201,6 @@ Add Ring BigZr : BigZring
div BigZdiv).
Section TestRing.
-Local Notation "2" := (BigZ.Pos (BigN.N0 2%int31)) : bigZ_scope.
Let test : forall x y, 1 + x*y + x^2 + 1 == 1*1 + 1 + (y + 1*x)*x.
Proof.
intros. ring_simplify. reflexivity.
diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v
index fb760bdf57..f9490cc9c7 100644
--- a/theories/Numbers/Integer/BigZ/ZMake.v
+++ b/theories/Numbers/Integer/BigZ/ZMake.v
@@ -31,6 +31,7 @@ Module Make (N:NType) <: ZType.
Definition zero := Pos N.zero.
Definition one := Pos N.one.
+ Definition two := Pos N.two.
Definition minus_one := Neg N.one.
Definition of_Z x :=
@@ -64,6 +65,10 @@ Module Make (N:NType) <: ZType.
exact N.spec_1.
Qed.
+ Theorem spec_2: to_Z two = 2.
+ exact N.spec_2.
+ Qed.
+
Theorem spec_m1: to_Z minus_one = -1.
simpl; rewrite N.spec_1; auto.
Qed.
diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v
index 28a37abf85..5f87283940 100644
--- a/theories/Numbers/Integer/Binary/ZBinary.v
+++ b/theories/Numbers/Integer/Binary/ZBinary.v
@@ -63,6 +63,8 @@ Module Z
Definition t := Z.
Definition eqb := Zeq_bool.
Definition zero := 0.
+Definition one := 1.
+Definition two := 2.
Definition succ := Zsucc.
Definition pred := Zpred.
Definition add := Zplus.
@@ -99,6 +101,16 @@ Definition sub_succ_r := Zminus_succ_r.
Definition mul_0_l := Zmult_0_l.
Definition mul_succ_l := Zmult_succ_l.
+Lemma one_succ : 1 = Zsucc 0.
+Proof.
+reflexivity.
+Qed.
+
+Lemma two_succ : 2 = Zsucc 1.
+Proof.
+reflexivity.
+Qed.
+
(** Boolean Equality *)
Definition eqb_eq x y := iff_sym (Zeq_is_eq_bool x y).
diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
index 7df1871e11..ab555ca321 100644
--- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v
+++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
@@ -25,7 +25,8 @@ Bind Scope NScope with N.t.
Infix "==" := N.eq (at level 70) : NScope.
Notation "x ~= y" := (~ N.eq x y) (at level 70) : NScope.
Notation "0" := N.zero : NScope.
-Notation "1" := (N.succ N.zero) : NScope.
+Notation "1" := N.one : NScope.
+Notation "2" := N.two : NScope.
Infix "+" := N.add : NScope.
Infix "-" := N.sub : NScope.
Infix "*" := N.mul : NScope.
@@ -43,6 +44,8 @@ Module Z.
Definition t := (N.t * N.t)%type.
Definition zero : t := (0, 0).
+Definition one : t := (1,0).
+Definition two : t := (2,0).
Definition eq (p q : t) := (p#1 + q#2 == q#1 + p#2).
Definition succ (n : t) : t := (N.succ n#1, n#2).
Definition pred (n : t) : t := (n#1, N.succ n#2).
@@ -73,7 +76,8 @@ Bind Scope ZScope with Z.t.
Infix "==" := Z.eq (at level 70) : ZScope.
Notation "x ~= y" := (~ Z.eq x y) (at level 70) : ZScope.
Notation "0" := Z.zero : ZScope.
-Notation "1" := (Z.succ Z.zero) : ZScope.
+Notation "1" := Z.one : ZScope.
+Notation "2" := Z.two : ZScope.
Infix "+" := Z.add : ZScope.
Infix "-" := Z.sub : ZScope.
Infix "*" := Z.mul : ZScope.
@@ -159,20 +163,22 @@ Hypothesis A_wd : Proper (Z.eq==>iff) A.
Theorem bi_induction :
A 0 -> (forall n, A n <-> A (Z.succ n)) -> forall n, A n.
Proof.
+Open Scope NScope.
intros A0 AS n; unfold Z.zero, Z.succ, Z.eq in *.
destruct n as [n m].
-cut (forall p, A (p, 0%N)); [intro H1 |].
-cut (forall p, A (0%N, p)); [intro H2 |].
+cut (forall p, A (p, 0)); [intro H1 |].
+cut (forall p, A (0, p)); [intro H2 |].
destruct (add_dichotomy n m) as [[p H] | [p H]].
-rewrite (A_wd (n, m) (0%N, p)) by (rewrite add_0_l; now rewrite add_comm).
+rewrite (A_wd (n, m) (0, p)) by (rewrite add_0_l; now rewrite add_comm).
apply H2.
-rewrite (A_wd (n, m) (p, 0%N)) by now rewrite add_0_r. apply H1.
+rewrite (A_wd (n, m) (p, 0)) by now rewrite add_0_r. apply H1.
induct p. assumption. intros p IH.
-apply -> (A_wd (0%N, p) (1%N, N.succ p)) in IH; [| now rewrite add_0_l, add_1_l].
-now apply <- AS.
+apply -> (A_wd (0, p) (1, N.succ p)) in IH; [| now rewrite add_0_l, add_1_l].
+rewrite one_succ in IH. now apply <- AS.
induct p. assumption. intros p IH.
-replace 0%N with (snd (p, 0%N)); [| reflexivity].
-replace (N.succ p) with (N.succ (fst (p, 0%N))); [| reflexivity]. now apply -> AS.
+replace 0 with (snd (p, 0)); [| reflexivity].
+replace (N.succ p) with (N.succ (fst (p, 0))); [| reflexivity]. now apply -> AS.
+Close Scope NScope.
Qed.
End Induction.
@@ -189,6 +195,16 @@ Proof.
intro n; unfold Z.succ, Z.pred, Z.eq; simpl; now nzsimpl.
Qed.
+Theorem one_succ : 1 == Z.succ 0.
+Proof.
+unfold Z.eq; simpl. now nzsimpl'.
+Qed.
+
+Theorem two_succ : 2 == Z.succ 1.
+Proof.
+unfold Z.eq; simpl. now nzsimpl'.
+Qed.
+
Theorem opp_0 : - 0 == 0.
Proof.
unfold Z.opp, Z.eq; simpl. now nzsimpl.
@@ -297,6 +313,8 @@ Qed.
Definition t := Z.t.
Definition eq := Z.eq.
Definition zero := Z.zero.
+Definition one := Z.one.
+Definition two := Z.two.
Definition succ := Z.succ.
Definition pred := Z.pred.
Definition add := Z.add.
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSig.v b/theories/Numbers/Integer/SpecViaZ/ZSig.v
index b33ed5f8ef..be201f2d66 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSig.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSig.v
@@ -38,6 +38,7 @@ Module Type ZType.
Parameter max : t -> t -> t.
Parameter zero : t.
Parameter one : t.
+ Parameter two : t.
Parameter minus_one : t.
Parameter succ : t -> t.
Parameter add : t -> t -> t.
@@ -65,6 +66,7 @@ Module Type ZType.
Parameter spec_max : forall x y, [max x y] = Zmax [x] [y].
Parameter spec_0: [zero] = 0.
Parameter spec_1: [one] = 1.
+ Parameter spec_2: [two] = 2.
Parameter spec_m1: [minus_one] = -1.
Parameter spec_succ: forall n, [succ n] = [n] + 1.
Parameter spec_add: forall x y, [add x y] = [x] + [y].
@@ -94,6 +96,8 @@ Module Type ZType_Notation (Import Z:ZType).
Notation "[ x ]" := (to_Z x).
Infix "==" := eq (at level 70).
Notation "0" := zero.
+ Notation "1" := one.
+ Notation "2" := two.
Infix "+" := add.
Infix "-" := sub.
Infix "*" := mul.
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
index 90bda6343e..3e63755434 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
@@ -17,7 +17,7 @@ Require Import ZArith Nnat ZAxioms ZDivFloor ZSig.
Module ZTypeIsZAxioms (Import Z : ZType').
Hint Rewrite
- spec_0 spec_1 spec_add spec_sub spec_pred spec_succ
+ spec_0 spec_1 spec_2 spec_add spec_sub spec_pred spec_succ
spec_mul spec_opp spec_of_Z spec_div spec_modulo
spec_compare spec_eq_bool spec_max spec_min spec_abs spec_sgn
spec_pow spec_even spec_odd
@@ -43,6 +43,16 @@ Proof.
intros. zify. auto with zarith.
Qed.
+Theorem one_succ : 1 == succ 0.
+Proof.
+now zify.
+Qed.
+
+Theorem two_succ : 2 == succ 1.
+Proof.
+now zify.
+Qed.
+
Section Induction.
Variable A : Z.t -> Prop.
@@ -225,12 +235,12 @@ Proof.
intros n. zify. omega with *.
Qed.
-Theorem sgn_pos : forall n, 0<n -> sgn n == succ 0.
+Theorem sgn_pos : forall n, 0<n -> sgn n == 1.
Proof.
intros n. zify. omega with *.
Qed.
-Theorem sgn_neg : forall n, n<0 -> sgn n == opp (succ 0).
+Theorem sgn_neg : forall n, n<0 -> sgn n == opp 1.
Proof.
intros n. zify. omega with *.
Qed.
@@ -239,9 +249,6 @@ Qed.
Program Instance pow_wd : Proper (eq==>eq==>eq) pow.
-Local Notation "1" := (succ 0).
-Local Notation "2" := (succ 1).
-
Lemma pow_0_r : forall a, a^0 == 1.
Proof.
intros. now zify.
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-31 19:44:08 +0000