aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--doc/changelog/10-standard-library/12479-fix-int-ltb-notations.rst9
-rw-r--r--test-suite/primitive/uint63/eqb.v16
-rw-r--r--test-suite/primitive/uint63/leb.v24
-rw-r--r--test-suite/primitive/uint63/ltb.v24
-rw-r--r--test-suite/primitive/uint63/mod.v16
-rw-r--r--test-suite/primitive/uint63/unsigned.v8
-rw-r--r--theories/Array/PArray.v22
-rw-r--r--theories/Numbers/Cyclic/Int63/Cyclic63.v2
-rw-r--r--theories/Numbers/Cyclic/Int63/Int63.v199
9 files changed, 178 insertions, 142 deletions
diff --git a/doc/changelog/10-standard-library/12479-fix-int-ltb-notations.rst b/doc/changelog/10-standard-library/12479-fix-int-ltb-notations.rst
new file mode 100644
index 0000000000..208855b4c8
--- /dev/null
+++ b/doc/changelog/10-standard-library/12479-fix-int-ltb-notations.rst
@@ -0,0 +1,9 @@
+- **Changed:**
+ Int63 notations now match up with the rest of the standard library: :g:`a \%
+ m`, :g:`m == n`, :g:`m < n`, :g:`m <= n`, and :g:`m ≤ n` have been replaced
+ with :g:`a mod m`, :g:`m =? n`, :g:`m <? n`, :g:`m <=? n`, and :g:`m ≤? n`.
+ The old notations are still available as deprecated notations. Additionally,
+ there is now a ``Coq.Numbers.Cyclic.Int63.Int63.Int63Notations`` module that
+ users can import to get the ``Int63`` notations without unqualifying the
+ various primitives (`#12479 <https://github.com/coq/coq/pull/12479>`_, fixes
+ `#12454 <https://github.com/coq/coq/issues/12454>`_, by Jason Gross).
diff --git a/test-suite/primitive/uint63/eqb.v b/test-suite/primitive/uint63/eqb.v
index dcc0b71f6d..43c98e2b6f 100644
--- a/test-suite/primitive/uint63/eqb.v
+++ b/test-suite/primitive/uint63/eqb.v
@@ -4,14 +4,14 @@ Set Implicit Arguments.
Open Scope int63_scope.
-Check (eq_refl : 1 == 1 = true).
-Check (eq_refl true <: 1 == 1 = true).
-Check (eq_refl true <<: 1 == 1 = true).
-Definition compute1 := Eval compute in 1 == 1.
+Check (eq_refl : 1 =? 1 = true).
+Check (eq_refl true <: 1 =? 1 = true).
+Check (eq_refl true <<: 1 =? 1 = true).
+Definition compute1 := Eval compute in 1 =? 1.
Check (eq_refl compute1 : true = true).
-Check (eq_refl : 9223372036854775807 == 0 = false).
-Check (eq_refl false <: 9223372036854775807 == 0 = false).
-Check (eq_refl false <<: 9223372036854775807 == 0 = false).
-Definition compute2 := Eval compute in 9223372036854775807 == 0.
+Check (eq_refl : 9223372036854775807 =? 0 = false).
+Check (eq_refl false <: 9223372036854775807 =? 0 = false).
+Check (eq_refl false <<: 9223372036854775807 =? 0 = false).
+Definition compute2 := Eval compute in 9223372036854775807 =? 0.
Check (eq_refl compute2 : false = false).
diff --git a/test-suite/primitive/uint63/leb.v b/test-suite/primitive/uint63/leb.v
index 5354919978..e5142282ae 100644
--- a/test-suite/primitive/uint63/leb.v
+++ b/test-suite/primitive/uint63/leb.v
@@ -4,20 +4,20 @@ Set Implicit Arguments.
Open Scope int63_scope.
-Check (eq_refl : 1 <= 1 = true).
-Check (eq_refl true <: 1 <= 1 = true).
-Check (eq_refl true <<: 1 <= 1 = true).
-Definition compute1 := Eval compute in 1 <= 1.
+Check (eq_refl : 1 <=? 1 = true).
+Check (eq_refl true <: 1 <=? 1 = true).
+Check (eq_refl true <<: 1 <=? 1 = true).
+Definition compute1 := Eval compute in 1 <=? 1.
Check (eq_refl compute1 : true = true).
-Check (eq_refl : 1 <= 2 = true).
-Check (eq_refl true <: 1 <= 2 = true).
-Check (eq_refl true <<: 1 <= 2 = true).
-Definition compute2 := Eval compute in 1 <= 2.
+Check (eq_refl : 1 <=? 2 = true).
+Check (eq_refl true <: 1 <=? 2 = true).
+Check (eq_refl true <<: 1 <=? 2 = true).
+Definition compute2 := Eval compute in 1 <=? 2.
Check (eq_refl compute2 : true = true).
-Check (eq_refl : 9223372036854775807 <= 0 = false).
-Check (eq_refl false <: 9223372036854775807 <= 0 = false).
-Check (eq_refl false <<: 9223372036854775807 <= 0 = false).
-Definition compute3 := Eval compute in 9223372036854775807 <= 0.
+Check (eq_refl : 9223372036854775807 <=? 0 = false).
+Check (eq_refl false <: 9223372036854775807 <=? 0 = false).
+Check (eq_refl false <<: 9223372036854775807 <=? 0 = false).
+Definition compute3 := Eval compute in 9223372036854775807 <=? 0.
Check (eq_refl compute3 : false = false).
diff --git a/test-suite/primitive/uint63/ltb.v b/test-suite/primitive/uint63/ltb.v
index 7ae5ac6493..50cef6be66 100644
--- a/test-suite/primitive/uint63/ltb.v
+++ b/test-suite/primitive/uint63/ltb.v
@@ -4,20 +4,20 @@ Set Implicit Arguments.
Open Scope int63_scope.
-Check (eq_refl : 1 < 1 = false).
-Check (eq_refl false <: 1 < 1 = false).
-Check (eq_refl false <<: 1 < 1 = false).
-Definition compute1 := Eval compute in 1 < 1.
+Check (eq_refl : 1 <? 1 = false).
+Check (eq_refl false <: 1 <? 1 = false).
+Check (eq_refl false <<: 1 <? 1 = false).
+Definition compute1 := Eval compute in 1 <? 1.
Check (eq_refl compute1 : false = false).
-Check (eq_refl : 1 < 2 = true).
-Check (eq_refl true <: 1 < 2 = true).
-Check (eq_refl true <<: 1 < 2 = true).
-Definition compute2 := Eval compute in 1 < 2.
+Check (eq_refl : 1 <? 2 = true).
+Check (eq_refl true <: 1 <? 2 = true).
+Check (eq_refl true <<: 1 <? 2 = true).
+Definition compute2 := Eval compute in 1 <? 2.
Check (eq_refl compute2 : true = true).
-Check (eq_refl : 9223372036854775807 < 0 = false).
-Check (eq_refl false <: 9223372036854775807 < 0 = false).
-Check (eq_refl false <<: 9223372036854775807 < 0 = false).
-Definition compute3 := Eval compute in 9223372036854775807 < 0.
+Check (eq_refl : 9223372036854775807 <? 0 = false).
+Check (eq_refl false <: 9223372036854775807 <? 0 = false).
+Check (eq_refl false <<: 9223372036854775807 <? 0 = false).
+Definition compute3 := Eval compute in 9223372036854775807 <? 0.
Check (eq_refl compute3 : false = false).
diff --git a/test-suite/primitive/uint63/mod.v b/test-suite/primitive/uint63/mod.v
index 5307eed493..3ad6312c2c 100644
--- a/test-suite/primitive/uint63/mod.v
+++ b/test-suite/primitive/uint63/mod.v
@@ -4,14 +4,14 @@ Set Implicit Arguments.
Open Scope int63_scope.
-Check (eq_refl : 6 \% 3 = 0).
-Check (eq_refl 0 <: 6 \% 3 = 0).
-Check (eq_refl 0 <<: 6 \% 3 = 0).
-Definition compute1 := Eval compute in 6 \% 3.
+Check (eq_refl : 6 mod 3 = 0).
+Check (eq_refl 0 <: 6 mod 3 = 0).
+Check (eq_refl 0 <<: 6 mod 3 = 0).
+Definition compute1 := Eval compute in 6 mod 3.
Check (eq_refl compute1 : 0 = 0).
-Check (eq_refl : 5 \% 3 = 2).
-Check (eq_refl 2 <: 5 \% 3 = 2).
-Check (eq_refl 2 <<: 5 \% 3 = 2).
-Definition compute2 := Eval compute in 5 \% 3.
+Check (eq_refl : 5 mod 3 = 2).
+Check (eq_refl 2 <: 5 mod 3 = 2).
+Check (eq_refl 2 <<: 5 mod 3 = 2).
+Definition compute2 := Eval compute in 5 mod 3.
Check (eq_refl compute2 : 2 = 2).
diff --git a/test-suite/primitive/uint63/unsigned.v b/test-suite/primitive/uint63/unsigned.v
index 82920bd201..6224e9d15b 100644
--- a/test-suite/primitive/uint63/unsigned.v
+++ b/test-suite/primitive/uint63/unsigned.v
@@ -11,8 +11,8 @@ Check (eq_refl 0 <<: 1/(0-1) = 0).
Definition compute1 := Eval compute in 1/(0-1).
Check (eq_refl compute1 : 0 = 0).
-Check (eq_refl : 3 \% (0-1) = 3).
-Check (eq_refl 3 <: 3 \% (0-1) = 3).
-Check (eq_refl 3 <<: 3 \% (0-1) = 3).
-Definition compute2 := Eval compute in 3 \% (0-1).
+Check (eq_refl : 3 mod (0-1) = 3).
+Check (eq_refl 3 <: 3 mod (0-1) = 3).
+Check (eq_refl 3 <<: 3 mod (0-1) = 3).
+Definition compute2 := Eval compute in 3 mod (0-1).
Check (eq_refl compute2 : 3 = 3).
diff --git a/theories/Array/PArray.v b/theories/Array/PArray.v
index 282f56267c..3511ba0918 100644
--- a/theories/Array/PArray.v
+++ b/theories/Array/PArray.v
@@ -45,19 +45,19 @@ Local Open Scope array_scope.
Primitive max_length := #array_max_length.
(** Axioms *)
-Axiom get_out_of_bounds : forall A (t:array A) i, (i < length t) = false -> t.[i] = default t.
+Axiom get_out_of_bounds : forall A (t:array A) i, (i <? length t) = false -> t.[i] = default t.
-Axiom get_set_same : forall A t i (a:A), (i < length t) = true -> t.[i<-a].[i] = a.
+Axiom get_set_same : forall A t i (a:A), (i <? length t) = true -> t.[i<-a].[i] = a.
Axiom get_set_other : forall A t i j (a:A), i <> j -> t.[i<-a].[j] = t.[j].
Axiom default_set : forall A t i (a:A), default t.[i<-a] = default t.
Axiom get_make : forall A (a:A) size i, (make size a).[i] = a.
-Axiom leb_length : forall A (t:array A), length t <= max_length = true.
+Axiom leb_length : forall A (t:array A), length t <=? max_length = true.
Axiom length_make : forall A size (a:A),
- length (make size a) = if size <= max_length then size else max_length.
+ length (make size a) = if size <=? max_length then size else max_length.
Axiom length_set : forall A t i (a:A),
length t.[i<-a] = length t.
@@ -69,7 +69,7 @@ Axiom length_reroot : forall A (t:array A), length (reroot t) = length t.
Axiom array_ext : forall A (t1 t2:array A),
length t1 = length t2 ->
- (forall i, i < length t1 = true -> t1.[i] = t2.[i]) ->
+ (forall i, i <? length t1 = true -> t1.[i] = t2.[i]) ->
default t1 = default t2 ->
t1 = t2.
@@ -77,7 +77,7 @@ Axiom array_ext : forall A (t1 t2:array A),
Lemma default_copy A (t:array A) : default (copy t) = default t.
Proof.
- assert (irr_lt : length t < length t = false).
+ assert (irr_lt : length t <? length t = false).
destruct (Int63.ltbP (length t) (length t)); try reflexivity.
exfalso; eapply BinInt.Z.lt_irrefl; eassumption.
assert (get_copy := get_copy A t (length t)).
@@ -87,7 +87,7 @@ Qed.
Lemma default_make A (a : A) size : default (make size a) = a.
Proof.
- assert (irr_lt : length (make size a) < length (make size a) = false).
+ assert (irr_lt : length (make size a) <? length (make size a) = false).
destruct (Int63.ltbP (length (make size a)) (length (make size a))); try reflexivity.
exfalso; eapply BinInt.Z.lt_irrefl; eassumption.
assert (get_make := get_make A a size (length (make size a))).
@@ -96,7 +96,7 @@ Qed.
Lemma default_reroot A (t:array A) : default (reroot t) = default t.
Proof.
- assert (irr_lt : length t < length t = false).
+ assert (irr_lt : length t <? length t = false).
destruct (Int63.ltbP (length t) (length t)); try reflexivity.
exfalso; eapply BinInt.Z.lt_irrefl; eassumption.
assert (get_reroot := get_reroot A t (length t)).
@@ -107,16 +107,16 @@ Qed.
Lemma get_set_same_default A (t : array A) (i : int) :
t.[i <- default t].[i] = default t.
Proof.
- case_eq (i < length t); intros.
+ case_eq (i <? length t); intros.
rewrite get_set_same; trivial.
rewrite get_out_of_bounds, default_set; trivial.
rewrite length_set; trivial.
Qed.
Lemma get_not_default_lt A (t:array A) x :
- t.[x] <> default t -> (x < length t) = true.
+ t.[x] <> default t -> (x <? length t) = true.
Proof.
intros Hd.
- case_eq (x < length t); intros Heq; [trivial | ].
+ case_eq (x <? length t); intros Heq; [trivial | ].
elim Hd; rewrite get_out_of_bounds; trivial.
Qed.
diff --git a/theories/Numbers/Cyclic/Int63/Cyclic63.v b/theories/Numbers/Cyclic/Int63/Cyclic63.v
index 5f903c41cb..2a26b6b12a 100644
--- a/theories/Numbers/Cyclic/Int63/Cyclic63.v
+++ b/theories/Numbers/Cyclic/Int63/Cyclic63.v
@@ -48,7 +48,7 @@ Definition mulc_WW x y :=
Notation "n '*c' m" := (mulc_WW n m) (at level 40, no associativity) : int63_scope.
Definition pos_mod p x :=
- if p <= digits then
+ if p <=? digits then
let p := digits - p in
(x << p) >> p
else x.
diff --git a/theories/Numbers/Cyclic/Int63/Int63.v b/theories/Numbers/Cyclic/Int63/Int63.v
index 2c112c3469..383c0aff3a 100644
--- a/theories/Numbers/Cyclic/Int63/Int63.v
+++ b/theories/Numbers/Cyclic/Int63/Int63.v
@@ -31,56 +31,61 @@ Declare Scope int63_scope.
Definition id_int : int -> int := fun x => x.
Declare ML Module "int63_syntax_plugin".
+Module Import Int63NotationsInternalA.
Delimit Scope int63_scope with int63.
Bind Scope int63_scope with int.
+End Int63NotationsInternalA.
(* Logical operations *)
Primitive lsl := #int63_lsl.
-Infix "<<" := lsl (at level 30, no associativity) : int63_scope.
Primitive lsr := #int63_lsr.
-Infix ">>" := lsr (at level 30, no associativity) : int63_scope.
Primitive land := #int63_land.
-Infix "land" := land (at level 40, left associativity) : int63_scope.
Primitive lor := #int63_lor.
-Infix "lor" := lor (at level 40, left associativity) : int63_scope.
Primitive lxor := #int63_lxor.
-Infix "lxor" := lxor (at level 40, left associativity) : int63_scope.
(* Arithmetic modulo operations *)
Primitive add := #int63_add.
-Notation "n + m" := (add n m) : int63_scope.
Primitive sub := #int63_sub.
-Notation "n - m" := (sub n m) : int63_scope.
Primitive mul := #int63_mul.
-Notation "n * m" := (mul n m) : int63_scope.
Primitive mulc := #int63_mulc.
Primitive div := #int63_div.
-Notation "n / m" := (div n m) : int63_scope.
Primitive mod := #int63_mod.
-Notation "n '\%' m" := (mod n m) (at level 40, left associativity) : int63_scope.
(* Comparisons *)
Primitive eqb := #int63_eq.
-Notation "m '==' n" := (eqb m n) (at level 70, no associativity) : int63_scope.
Primitive ltb := #int63_lt.
-Notation "m < n" := (ltb m n) : int63_scope.
Primitive leb := #int63_le.
-Notation "m <= n" := (leb m n) : int63_scope.
-Notation "m ≤ n" := (leb m n) (at level 70, no associativity) : int63_scope.
Local Open Scope int63_scope.
+Module Import Int63NotationsInternalB.
+Infix "<<" := lsl (at level 30, no associativity) : int63_scope.
+Infix ">>" := lsr (at level 30, no associativity) : int63_scope.
+Infix "land" := land (at level 40, left associativity) : int63_scope.
+Infix "lor" := lor (at level 40, left associativity) : int63_scope.
+Infix "lxor" := lxor (at level 40, left associativity) : int63_scope.
+Infix "+" := add : int63_scope.
+Infix "-" := sub : int63_scope.
+Infix "*" := mul : int63_scope.
+Infix "/" := div : int63_scope.
+Infix "mod" := mod (at level 40, no associativity) : int63_scope.
+Infix "=?" := eqb (at level 70, no associativity) : int63_scope.
+Infix "<?" := ltb (at level 70, no associativity) : int63_scope.
+Infix "<=?" := leb (at level 70, no associativity) : int63_scope.
+Infix "≤?" := leb (at level 70, no associativity) : int63_scope.
+End Int63NotationsInternalB.
+
(** The number of digits as a int *)
Definition digits := 63.
@@ -89,16 +94,16 @@ Definition max_int := Eval vm_compute in 0 - 1.
Register Inline max_int.
(** Access to the nth digits *)
-Definition get_digit x p := (0 < (x land (1 << p))).
+Definition get_digit x p := (0 <? (x land (1 << p))).
Definition set_digit x p (b:bool) :=
- if if 0 <= p then p < digits else false then
+ if if 0 <=? p then p <? digits else false then
if b then x lor (1 << p)
else x land (max_int lxor (1 << p))
else x.
(** Equality to 0 *)
-Definition is_zero (i:int) := i == 0.
+Definition is_zero (i:int) := i =? 0.
Register Inline is_zero.
(** Parity *)
@@ -113,7 +118,6 @@ Definition bit i n := negb (is_zero ((i >> n) << (digits - 1))).
(** Extra modulo operations *)
Definition opp (i:int) := 0 - i.
Register Inline opp.
-Notation "- x" := (opp x) : int63_scope.
Definition oppcarry i := max_int - i.
Register Inline oppcarry.
@@ -134,29 +138,27 @@ Register Inline subcarry.
Definition addc_def x y :=
let r := x + y in
- if r < x then C1 r else C0 r.
+ if r <? x then C1 r else C0 r.
(* the same but direct implementation for efficiency *)
Primitive addc := #int63_addc.
-Notation "n '+c' m" := (addc n m) (at level 50, no associativity) : int63_scope.
Definition addcarryc_def x y :=
let r := addcarry x y in
- if r <= x then C1 r else C0 r.
+ if r <=? x then C1 r else C0 r.
(* the same but direct implementation for efficiency *)
Primitive addcarryc := #int63_addcarryc.
Definition subc_def x y :=
- if y <= x then C0 (x - y) else C1 (x - y).
+ if y <=? x then C0 (x - y) else C1 (x - y).
(* the same but direct implementation for efficiency *)
Primitive subc := #int63_subc.
-Notation "n '-c' m" := (subc n m) (at level 50, no associativity) : int63_scope.
Definition subcarryc_def x y :=
- if y < x then C0 (x - y - 1) else C1 (x - y - 1).
+ if y <? x then C0 (x - y - 1) else C1 (x - y - 1).
(* the same but direct implementation for efficiency *)
Primitive subcarryc := #int63_subcarryc.
-Definition diveucl_def x y := (x/y, x\%y).
+Definition diveucl_def x y := (x/y, x mod y).
(* the same but direct implementation for efficiency *)
Primitive diveucl := #int63_diveucl.
@@ -166,6 +168,12 @@ Definition addmuldiv_def p x y :=
(x << p) lor (y >> (digits - p)).
Primitive addmuldiv := #int63_addmuldiv.
+Module Import Int63NotationsInternalC.
+Notation "- x" := (opp x) : int63_scope.
+Notation "n '+c' m" := (addc n m) (at level 50, no associativity) : int63_scope.
+Notation "n '-c' m" := (subc n m) (at level 50, no associativity) : int63_scope.
+End Int63NotationsInternalC.
+
Definition oppc (i:int) := 0 -c i.
Register Inline oppc.
@@ -177,11 +185,10 @@ Register Inline predc.
(** Comparison *)
Definition compare_def x y :=
- if x < y then Lt
- else if (x == y) then Eq else Gt.
+ if x <? y then Lt
+ else if (x =? y) then Eq else Gt.
Primitive compare := #int63_compare.
-Notation "n ?= m" := (compare n m) (at level 70, no associativity) : int63_scope.
Import Bool ZArith.
(** Translation to Z *)
@@ -194,8 +201,6 @@ Fixpoint to_Z_rec (n:nat) (i:int) :=
Definition to_Z := to_Z_rec size.
-Notation "'φ' x" := (to_Z x) (at level 0) : int63_scope.
-
Fixpoint of_pos_rec (n:nat) (p:positive) :=
match n, p with
| O, _ => 0
@@ -215,8 +220,12 @@ Definition of_Z z :=
Definition wB := (2 ^ (Z.of_nat size))%Z.
+Module Import Int63NotationsInternalD.
+Notation "n ?= m" := (compare n m) (at level 70, no associativity) : int63_scope.
+Notation "'φ' x" := (to_Z x) (at level 0) : int63_scope.
Notation "'Φ' x" :=
(zn2z_to_Z wB to_Z x) (at level 0) : int63_scope.
+End Int63NotationsInternalD.
Lemma to_Z_rec_bounded size : forall x, (0 <= to_Z_rec size x < 2 ^ Z.of_nat size)%Z.
Proof.
@@ -347,16 +356,16 @@ Axiom mulc_spec : forall x y, φ x * φ y = φ (fst (mulc x y)) * wB + φ (snd (
Axiom div_spec : forall x y, φ (x / y) = φ x / φ y.
-Axiom mod_spec : forall x y, φ (x \% y) = φ x mod φ y.
+Axiom mod_spec : forall x y, φ (x mod y) = φ x mod φ y.
(* Comparisons *)
-Axiom eqb_correct : forall i j, (i == j)%int63 = true -> i = j.
+Axiom eqb_correct : forall i j, (i =? j)%int63 = true -> i = j.
-Axiom eqb_refl : forall x, (x == x)%int63 = true.
+Axiom eqb_refl : forall x, (x =? x)%int63 = true.
-Axiom ltb_spec : forall x y, (x < y)%int63 = true <-> φ x < φ y.
+Axiom ltb_spec : forall x y, (x <? y)%int63 = true <-> φ x < φ y.
-Axiom leb_spec : forall x y, (x <= y)%int63 = true <-> φ x <= φ y.
+Axiom leb_spec : forall x y, (x <=? y)%int63 = true <-> φ x <= φ y.
(** Exotic operations *)
@@ -397,7 +406,7 @@ Local Open Scope int63_scope.
Definition sqrt_step (rec: int -> int -> int) (i j: int) :=
let quo := i / j in
- if quo < j then rec i ((j + quo) >> 1)
+ if quo <? j then rec i ((j + quo) >> 1)
else j.
Definition iter_sqrt :=
@@ -421,9 +430,9 @@ Definition high_bit := 1 << (digits - 1).
Definition sqrt2_step (rec: int -> int -> int -> int)
(ih il j: int) :=
- if ih < j then
+ if ih <? j then
let (quo,_) := diveucl_21 ih il j in
- if quo < j then
+ if quo <? j then
match j +c quo with
| C0 m1 => rec ih il (m1 >> 1)
| C1 m1 => rec ih il ((m1 >> 1) + high_bit)
@@ -448,48 +457,48 @@ Definition sqrt2 ih il :=
let (ih1, il1) := mulc s s in
match il -c il1 with
| C0 il2 =>
- if ih1 < ih then (s, C1 il2) else (s, C0 il2)
+ if ih1 <? ih then (s, C1 il2) else (s, C0 il2)
| C1 il2 =>
- if ih1 < (ih - 1) then (s, C1 il2) else (s, C0 il2)
+ if ih1 <? (ih - 1) then (s, C1 il2) else (s, C0 il2)
end.
(** Gcd **)
Fixpoint gcd_rec (guard:nat) (i j:int) {struct guard} :=
match guard with
| O => 1
- | S p => if j == 0 then i else gcd_rec p j (i \% j)
+ | S p => if j =? 0 then i else gcd_rec p j (i mod j)
end.
Definition gcd := gcd_rec (2*size).
(** equality *)
-Lemma eqb_complete : forall x y, x = y -> (x == y) = true.
+Lemma eqb_complete : forall x y, x = y -> (x =? y) = true.
Proof.
intros x y H; rewrite -> H, eqb_refl;trivial.
Qed.
-Lemma eqb_spec : forall x y, (x == y) = true <-> x = y.
+Lemma eqb_spec : forall x y, (x =? y) = true <-> x = y.
Proof.
split;auto using eqb_correct, eqb_complete.
Qed.
-Lemma eqb_false_spec : forall x y, (x == y) = false <-> x <> y.
+Lemma eqb_false_spec : forall x y, (x =? y) = false <-> x <> y.
Proof.
intros;rewrite <- not_true_iff_false, eqb_spec;split;trivial.
Qed.
-Lemma eqb_false_complete : forall x y, x <> y -> (x == y) = false.
+Lemma eqb_false_complete : forall x y, x <> y -> (x =? y) = false.
Proof.
intros x y;rewrite eqb_false_spec;trivial.
Qed.
-Lemma eqb_false_correct : forall x y, (x == y) = false -> x <> y.
+Lemma eqb_false_correct : forall x y, (x =? y) = false -> x <> y.
Proof.
intros x y;rewrite eqb_false_spec;trivial.
Qed.
Definition eqs (i j : int) : {i = j} + { i <> j } :=
- (if i == j as b return ((b = true -> i = j) -> (b = false -> i <> j) -> {i=j} + {i <> j} )
+ (if i =? j as b return ((b = true -> i = j) -> (b = false -> i <> j) -> {i=j} + {i <> j} )
then fun (Heq : true = true -> i = j) _ => left _ (Heq (eq_refl true))
else fun _ (Hdiff : false = false -> i <> j) => right _ (Hdiff (eq_refl false)))
(eqb_correct i j)
@@ -503,7 +512,7 @@ Qed.
(* Extra function on equality *)
Definition cast i j :=
- (if i == j as b return ((b = true -> i = j) -> option (forall P : int -> Type, P i -> P j))
+ (if i =? j as b return ((b = true -> i = j) -> option (forall P : int -> Type, P i -> P j))
then fun Heq : true = true -> i = j =>
Some
(fun (P : int -> Type) (Hi : P i) =>
@@ -520,14 +529,14 @@ Proof.
rewrite (Eqdep_dec.eq_proofs_unicity eq_dec (e (eq_refl true)) (eq_refl i));trivial.
Qed.
-Lemma cast_diff : forall i j, i == j = false -> cast i j = None.
+Lemma cast_diff : forall i j, i =? j = false -> cast i j = None.
Proof.
intros;unfold cast;intros; generalize (eqb_correct i j).
rewrite H;trivial.
Qed.
Definition eqo i j :=
- (if i == j as b return ((b = true -> i = j) -> option (i=j))
+ (if i =? j as b return ((b = true -> i = j) -> option (i=j))
then fun Heq : true = true -> i = j =>
Some (Heq (eq_refl true))
else fun _ : false = true -> i = j => None) (eqb_correct i j).
@@ -540,7 +549,7 @@ Proof.
rewrite (Eqdep_dec.eq_proofs_unicity eq_dec (e (eq_refl true)) (eq_refl i));trivial.
Qed.
-Lemma eqo_diff : forall i j, i == j = false -> eqo i j = None.
+Lemma eqo_diff : forall i j, i =? j = false -> eqo i j = None.
Proof.
unfold eqo;intros; generalize (eqb_correct i j).
rewrite H;trivial.
@@ -548,13 +557,13 @@ Qed.
(** Comparison *)
-Lemma eqbP x y : reflect (φ x = φ y ) (x == y).
+Lemma eqbP x y : reflect (φ x = φ y ) (x =? y).
Proof. apply iff_reflect; rewrite eqb_spec; split; [ apply to_Z_inj | apply f_equal ]. Qed.
-Lemma ltbP x y : reflect (φ x < φ y )%Z (x < y).
+Lemma ltbP x y : reflect (φ x < φ y )%Z (x <? y).
Proof. apply iff_reflect; symmetry; apply ltb_spec. Qed.
-Lemma lebP x y : reflect (φ x <= φ y )%Z (x ≤ y).
+Lemma lebP x y : reflect (φ x <= φ y )%Z (x ≤? y).
Proof. apply iff_reflect; symmetry; apply leb_spec. Qed.
Lemma compare_spec x y : compare x y = (φ x ?= φ y)%Z.
@@ -742,7 +751,7 @@ Proof.
Qed.
Lemma add_le_r m n:
- if (n <= m + n)%int63 then (φ m + φ n < wB)%Z else (wB <= φ m + φ n)%Z.
+ if (n <=? m + n)%int63 then (φ m + φ n < wB)%Z else (wB <= φ m + φ n)%Z.
Proof.
case (to_Z_bounded m); intros H1m H2m.
case (to_Z_bounded n); intros H1n H2n.
@@ -753,11 +762,11 @@ Proof.
rewrite -> Zplus_mod, Z_mod_same_full, Zplus_0_r, !Zmod_small; auto with zarith.
rewrite !Zmod_small; auto with zarith.
apply f_equal2 with (f := Zmod); auto with zarith.
- case_eq (n <= m + n)%int63; auto.
+ case_eq (n <=? m + n)%int63; auto.
rewrite leb_spec, H1; auto with zarith.
assert (H1: (φ (m + n) = φ m + φ n)%Z).
rewrite add_spec, Zmod_small; auto with zarith.
- replace (n <= m + n)%int63 with true; auto.
+ replace (n <=? m + n)%int63 with true; auto.
apply sym_equal; rewrite leb_spec, H1; auto with zarith.
Qed.
@@ -783,7 +792,7 @@ Proof. apply to_Z_inj; rewrite lsr_spec; reflexivity. Qed.
Lemma lsr_0_r i: i >> 0 = i.
Proof. apply to_Z_inj; rewrite lsr_spec, Zdiv_1_r; exact eq_refl. Qed.
-Lemma lsr_1 n : 1 >> n = (n == 0).
+Lemma lsr_1 n : 1 >> n = (n =? 0)%int63.
Proof.
case eqbP.
intros h; rewrite (to_Z_inj _ _ h), lsr_0_r; reflexivity.
@@ -798,12 +807,12 @@ Proof.
lia.
Qed.
-Lemma lsr_add i m n: ((i >> m) >> n = if n <= m + n then i >> (m + n) else 0)%int63.
+Lemma lsr_add i m n: ((i >> m) >> n = if n <=? m + n then i >> (m + n) else 0)%int63.
Proof.
case (to_Z_bounded m); intros H1m H2m.
case (to_Z_bounded n); intros H1n H2n.
case (to_Z_bounded i); intros H1i H2i.
- generalize (add_le_r m n); case (n <= m + n)%int63; intros H.
+ generalize (add_le_r m n); case (n <=? m + n)%int63; intros H.
apply to_Z_inj; rewrite -> !lsr_spec, Zdiv_Zdiv, <- Zpower_exp; auto with zarith.
rewrite add_spec, Zmod_small; auto with zarith.
apply to_Z_inj; rewrite -> !lsr_spec, Zdiv_Zdiv, <- Zpower_exp; auto with zarith.
@@ -833,7 +842,7 @@ Proof.
apply f_equal2 with (f := Zmod); auto with zarith.
Qed.
-Lemma lsr_M_r x i (H: (digits <= i = true)%int63) : x >> i = 0%int63.
+Lemma lsr_M_r x i (H: (digits <=? i = true)%int63) : x >> i = 0%int63.
Proof.
apply to_Z_inj.
rewrite lsr_spec, to_Z_0.
@@ -889,22 +898,22 @@ Proof.
Qed.
Lemma bit_lsr x i j :
- (bit (x >> i) j = if j <= i + j then bit x (i + j) else false)%int63.
+ (bit (x >> i) j = if j <=? i + j then bit x (i + j) else false)%int63.
Proof.
- unfold bit; rewrite lsr_add; case (_ ≤ _); auto.
+ unfold bit; rewrite lsr_add; case (_ ≤? _); auto.
Qed.
-Lemma bit_b2i (b: bool) i : bit b i = (i == 0) && b.
+Lemma bit_b2i (b: bool) i : bit b i = (i =? 0)%int63 && b.
Proof.
case b; unfold bit; simpl b2i.
- rewrite lsr_1; case (i == 0); auto.
+ rewrite lsr_1; case (i =? 0)%int63; auto.
rewrite lsr0, lsl0, andb_false_r; auto.
Qed.
-Lemma bit_1 n : bit 1 n = (n == 0).
+Lemma bit_1 n : bit 1 n = (n =? 0)%int63.
Proof.
unfold bit; rewrite lsr_1.
- case (_ == _); simpl; auto.
+ case (_ =? _)%int63; simpl; auto.
Qed.
Local Hint Resolve Z.lt_gt Z.div_pos : zarith.
@@ -929,14 +938,14 @@ Proof.
case bit; discriminate.
Qed.
-Lemma bit_M i n (H: (digits <= n = true)%int63): bit i n = false.
+Lemma bit_M i n (H: (digits <=? n = true)%int63): bit i n = false.
Proof. unfold bit; rewrite lsr_M_r; auto. Qed.
-Lemma bit_half i n (H: (n < digits = true)%int63) : bit (i>>1) n = bit i (n+1).
+Lemma bit_half i n (H: (n <? digits = true)%int63) : bit (i>>1) n = bit i (n+1).
Proof.
unfold bit.
rewrite lsr_add.
- case_eq (n <= (1 + n))%int63.
+ case_eq (n <=? (1 + n))%int63.
replace (1+n)%int63 with (n+1)%int63; [auto|idtac].
apply to_Z_inj; rewrite !add_spec, Zplus_comm; auto.
intros H1; assert (H2: n = max_int).
@@ -968,10 +977,10 @@ Proof.
Qed.
Lemma bit_lsl x i j : bit (x << i) j =
-(if (j < i) || (digits <= j) then false else bit x (j - i))%int63.
+(if (j <? i) || (digits <=? j) then false else bit x (j - i))%int63.
Proof.
assert (F1: 1 >= 0) by discriminate.
- case_eq (digits <= j)%int63; intros H.
+ case_eq (digits <=? j)%int63; intros H.
rewrite orb_true_r, bit_M; auto.
set (d := φ digits).
case (Zle_or_lt d (φ j)); intros H1.
@@ -1039,10 +1048,10 @@ Lemma lor_lsr i1 i2 i: (i1 lor i2) >> i = (i1 >> i) lor (i2 >> i).
Proof.
apply bit_ext; intros n.
rewrite -> lor_spec, !bit_lsr, lor_spec.
- case (_ <= _)%int63; auto.
+ case (_ <=? _)%int63; auto.
Qed.
-Lemma lor_le x y : (y <= x lor y)%int63 = true.
+Lemma lor_le x y : (y <=? x lor y)%int63 = true.
Proof.
generalize x y (to_Z_bounded x) (to_Z_bounded y); clear x y.
unfold wB; elim size.
@@ -1092,7 +1101,7 @@ Proof.
rewrite lsr_spec, Z.pow_1_r; split; auto with zarith.
apply Zdiv_lt_upper_bound; auto with zarith.
intros m H1 H2.
- case_eq (digits <= m)%int63; [idtac | rewrite <- not_true_iff_false];
+ case_eq (digits <=? m)%int63; [idtac | rewrite <- not_true_iff_false];
intros Heq.
rewrite bit_M in H1; auto; discriminate.
rewrite leb_spec in Heq.
@@ -1131,7 +1140,7 @@ Proof.
rewrite lsr_spec, to_Z_1, Z.pow_1_r; split; auto with zarith.
apply Zdiv_lt_upper_bound; auto with zarith.
intros _ HH m; case (to_Z_bounded m); intros H1m H2m.
- case_eq (digits <= m)%int63.
+ case_eq (digits <=? m)%int63.
intros Hlm; rewrite bit_M; auto; discriminate.
rewrite <- not_true_iff_false, leb_spec; intros Hlm.
case (Zle_lt_or_eq 0 φ m); auto; intros Hm.
@@ -1177,11 +1186,11 @@ Proof.
rewrite (fun x y => Zmod_small (x - y)); auto with zarith.
intros n; rewrite -> bit_lsl, bit_lsr.
generalize (add_le_r (digits - p) n).
- case (_ ≤ _); try discriminate.
+ case (_ ≤? _); try discriminate.
rewrite -> sub_spec, Zmod_small; auto with zarith; intros H1.
- case_eq (n < p)%int63; try discriminate.
+ case_eq (n <? p)%int63; try discriminate.
rewrite <- not_true_iff_false, ltb_spec; intros H2.
- case (_ ≤ _); try discriminate.
+ case (_ ≤? _); try discriminate.
intros _; rewrite bit_M; try discriminate.
rewrite -> leb_spec, add_spec, Zmod_small, sub_spec, Zmod_small; auto with zarith.
rewrite -> sub_spec, Zmod_small; auto with zarith.
@@ -1196,7 +1205,7 @@ Proof.
apply bit_ext; intros n.
rewrite bit_b2i, land_spec, bit_1.
generalize (eqb_spec n 0).
- case (n == 0); auto.
+ case (n =? 0)%int63; auto.
intros(H,_); rewrite andb_true_r, H; auto.
rewrite andb_false_r; auto.
Qed.
@@ -1373,9 +1382,9 @@ Qed.
(* sqrt2 *)
Lemma sqrt2_step_def rec ih il j:
sqrt2_step rec ih il j =
- if (ih < j)%int63 then
+ if (ih <? j)%int63 then
let quo := fst (diveucl_21 ih il j) in
- if (quo < j)%int63 then
+ if (quo <? j)%int63 then
let m :=
match j +c quo with
| C0 m1 => m1 >> 1
@@ -1453,7 +1462,7 @@ Proof.
apply Zmult_lt_0_compat; auto with zarith.
refine (Z.lt_le_trans _ _ _ _ Hih); auto with zarith. }
cbv zeta.
- case_eq (ih < j)%int63;intros Heq.
+ case_eq (ih <? j)%int63;intros Heq.
rewrite -> ltb_spec in Heq.
2: rewrite <-not_true_iff_false, ltb_spec in Heq.
2: split; auto.
@@ -1462,7 +1471,7 @@ Proof.
2: assert (0 <= φ il/φ j) by (apply Z_div_pos; auto with zarith).
2: rewrite Zmult_comm, Z_div_plus_full_l; unfold base; auto with zarith.
case (Zle_or_lt (2^(Z_of_nat size -1)) φ j); intros Hjj.
- case_eq (fst (diveucl_21 ih il j) < j)%int63;intros Heq0.
+ case_eq (fst (diveucl_21 ih il j) <? j)%int63;intros Heq0.
2: rewrite <-not_true_iff_false, ltb_spec, (div2_phi _ _ _ Hjj Heq) in Heq0.
2: split; auto; apply sqrt_test_true; auto with zarith.
rewrite -> ltb_spec, (div2_phi _ _ _ Hjj Heq) in Heq0.
@@ -1557,7 +1566,7 @@ Lemma sqrt2_spec : forall x y,
generalize (subc_spec il il1).
case subc; intros il2 Hil2.
simpl interp_carry in Hil2.
- case_eq (ih1 < ih)%int63; [idtac | rewrite <- not_true_iff_false];
+ case_eq (ih1 <? ih)%int63; [idtac | rewrite <- not_true_iff_false];
rewrite ltb_spec; intros Heq.
unfold interp_carry; rewrite Zmult_1_l.
rewrite -> Z.pow_2_r, Hihl1, Hil2.
@@ -1602,7 +1611,7 @@ Lemma sqrt2_spec : forall x y,
case (to_Z_bounded ih); intros H1 H2.
split; auto with zarith.
apply Z.le_trans with (wB/4 - 1); auto with zarith.
- case_eq (ih1 < ih - 1)%int63; [idtac | rewrite <- not_true_iff_false];
+ case_eq (ih1 <? ih - 1)%int63; [idtac | rewrite <- not_true_iff_false];
rewrite ltb_spec, Hsih; intros Heq.
rewrite Z.pow_2_r, Hihl1.
case (Zle_lt_or_eq (φ ih1 + 2) φ ih); auto with zarith.
@@ -1927,3 +1936,21 @@ Qed.
Lemma lxor0_r i : i lxor 0 = i.
Proof. rewrite lxorC; exact (lxor0 i). Qed.
+
+Module Export Int63Notations.
+ Local Open Scope int63_scope.
+ #[deprecated(since="8.13",note="use infix mod instead")]
+ Notation "a \% m" := (a mod m) (at level 40, left associativity) : int63_scope.
+ #[deprecated(since="8.13",note="use infix =? instead")]
+ Notation "m '==' n" := (m =? n) (at level 70, no associativity) : int63_scope.
+ #[deprecated(since="8.13",note="use infix <? instead")]
+ Notation "m < n" := (m <? n) : int63_scope.
+ #[deprecated(since="8.13",note="use infix <=? instead")]
+ Notation "m <= n" := (m <=? n) : int63_scope.
+ #[deprecated(since="8.13",note="use infix ≤? instead")]
+ Notation "m ≤ n" := (m <=? n) (at level 70, no associativity) : int63_scope.
+ Export Int63NotationsInternalA.
+ Export Int63NotationsInternalB.
+ Export Int63NotationsInternalC.
+ Export Int63NotationsInternalD.
+End Int63Notations.
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:04:13 +0000