From 4302a75d82b9ac983cd89dd01c742c36777d921b Mon Sep 17 00:00:00 2001 From: Ana Date: Tue, 1 Dec 2020 08:52:12 +0000 Subject: Signed primitive integers Signed primitive integers defined on top of the existing unsigned ones with two's complement. The module Sint63 includes the theory of signed primitive integers that differs from the unsigned case. Additions to the kernel: les (signed <=), lts (signed <), compares (signed compare), divs (signed division), rems (signed remainder), asr (arithmetic shift right) (The s suffix is not used when importing the Sint63 module.) The printing and parsing of primitive ints was updated and the int63_syntax_plugin was removed (we use Number Notation instead). A primitive int is parsed / printed as unsigned or signed depending on the scope. In the default (Set Printing All) case, it is printed in hexadecimal. --- theories/Numbers/Cyclic/Int63/Int63.v | 17 ++ theories/Numbers/Cyclic/Int63/PrimInt63.v | 33 ++- theories/Numbers/Cyclic/Int63/Sint63.v | 407 ++++++++++++++++++++++++++++++ theories/dune | 1 - theories/extraction/ExtrOCamlInt63.v | 9 +- 5 files changed, 462 insertions(+), 5 deletions(-) create mode 100644 theories/Numbers/Cyclic/Int63/Sint63.v (limited to 'theories') diff --git a/theories/Numbers/Cyclic/Int63/Int63.v b/theories/Numbers/Cyclic/Int63/Int63.v index 7bb725538b..a3ebe67325 100644 --- a/theories/Numbers/Cyclic/Int63/Int63.v +++ b/theories/Numbers/Cyclic/Int63/Int63.v @@ -205,6 +205,7 @@ Qed. Corollary to_Z_bounded : forall x, (0 <= φ x < wB)%Z. Proof. apply to_Z_rec_bounded. Qed. + (* =================================================== *) Local Open Scope Z_scope. (* General arithmetic results *) @@ -1904,6 +1905,22 @@ Qed. Lemma lxor0_r i : i lxor 0 = i. Proof. rewrite lxorC; exact (lxor0 i). Qed. +Lemma opp_to_Z_opp (x : int) : + φ x mod wB <> 0 -> + (- φ (- x)) mod wB = (φ x) mod wB. +Proof. + intros neqx0. + rewrite opp_spec. + rewrite (Z_mod_nz_opp_full (φ x%int63)) by assumption. + rewrite (Z.mod_small (φ x%int63)) by apply to_Z_bounded. + rewrite <- Z.add_opp_l. + rewrite Z.opp_add_distr, Z.opp_involutive. + replace (- wB) with (-1 * wB) by easy. + rewrite Z_mod_plus by easy. + now rewrite Z.mod_small by apply to_Z_bounded. +Qed. + + Module Export Int63Notations. Local Open Scope int63_scope. #[deprecated(since="8.13",note="use infix mod instead")] diff --git a/theories/Numbers/Cyclic/Int63/PrimInt63.v b/theories/Numbers/Cyclic/Int63/PrimInt63.v index 64c1b862c7..98127ef0ac 100644 --- a/theories/Numbers/Cyclic/Int63/PrimInt63.v +++ b/theories/Numbers/Cyclic/Int63/PrimInt63.v @@ -17,11 +17,21 @@ Register comparison as kernel.ind_cmp. Primitive int := #int63_type. Register int as num.int63.type. +Variant pos_neg_int63 := Pos (d:int) | Neg (d:int). +Register pos_neg_int63 as num.int63.pos_neg_int63. Declare Scope int63_scope. Definition id_int : int -> int := fun x => x. -Declare ML Module "int63_syntax_plugin". - -Module Export Int63NotationsInternalA. +Record int_wrapper := wrap_int {int_wrap : int}. +Register wrap_int as num.int63.wrap_int. +Definition printer (x : int_wrapper) : pos_neg_int63 := Pos (int_wrap x). +Definition parser (x : pos_neg_int63) : option int := + match x with + | Pos p => Some p + | Neg _ => None + end. +Number Notation int parser printer : int63_scope. + +Module Import Int63NotationsInternalA. Delimit Scope int63_scope with int63. Bind Scope int63_scope with int. End Int63NotationsInternalA. @@ -37,6 +47,9 @@ Primitive lor := #int63_lor. Primitive lxor := #int63_lxor. + +Primitive asr := #int63_asr. + (* Arithmetic modulo operations *) Primitive add := #int63_add. @@ -50,6 +63,10 @@ Primitive div := #int63_div. Primitive mod := #int63_mod. +Primitive divs := #int63_divs. + +Primitive mods := #int63_mods. + (* Comparisons *) Primitive eqb := #int63_eq. @@ -57,6 +74,10 @@ Primitive ltb := #int63_lt. Primitive leb := #int63_le. +Primitive ltsb := #int63_lts. + +Primitive lesb := #int63_les. + (** Exact arithmetic operations *) Primitive addc := #int63_addc. @@ -76,7 +97,13 @@ Primitive addmuldiv := #int63_addmuldiv. (** Comparison *) Primitive compare := #int63_compare. +Primitive compares := #int63_compares. + (** Exotic operations *) Primitive head0 := #int63_head0. Primitive tail0 := #int63_tail0. + +Module Export PrimInt63Notations. + Export Int63NotationsInternalA. +End PrimInt63Notations. diff --git a/theories/Numbers/Cyclic/Int63/Sint63.v b/theories/Numbers/Cyclic/Int63/Sint63.v new file mode 100644 index 0000000000..c0239ae3db --- /dev/null +++ b/theories/Numbers/Cyclic/Int63/Sint63.v @@ -0,0 +1,407 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* if (p if (n <=? 4611686018427387904)%int63 + then Some ((n - 1) lxor max_int)%int63 else None + end. +Number Notation int parser printer : sint63_scope. + + +Module Import Sint63NotationsInternalA. +Delimit Scope sint63_scope with sint63. +Bind Scope sint63_scope with int. +End Sint63NotationsInternalA. + + +Module Import Sint63NotationsInternalB. +Infix "<<" := Int63.lsl (at level 30, no associativity) : sint63_scope. +(* TODO do we want >> to be asr or lsr? And is there a notation for the other one? *) +Infix ">>" := asr (at level 30, no associativity) : sint63_scope. +Infix "land" := Int63.land (at level 40, left associativity) : sint63_scope. +Infix "lor" := Int63.lor (at level 40, left associativity) : sint63_scope. +Infix "lxor" := Int63.lxor (at level 40, left associativity) : sint63_scope. +Infix "+" := Int63.add : sint63_scope. +Infix "-" := Int63.sub : sint63_scope. +Infix "*" := Int63.mul : sint63_scope. +Infix "/" := divs : sint63_scope. +Infix "mod" := mods (at level 40, no associativity) : sint63_scope. +Infix "=?" := Int63.eqb (at level 70, no associativity) : sint63_scope. +Infix " lia | intros _]. + case (ltbP max_int); [> intros _ | now intros H; exfalso; apply H]. + rewrite opp_spec. + rewrite Z_mod_nz_opp_full by easy. + rewrite Z.mod_small by apply Int63.to_Z_bounded. + case ltbP. + - intros ltxmin; split. + + now transitivity 0%Z; [>| now apply Int63.to_Z_bounded]. + + replace (φ min_int%int63) with (φ max_int%int63 + 1)%Z in ltxmin. + * lia. + * now compute. + - rewrite Z.nlt_ge; intros leminx. + rewrite opp_spec. + rewrite Z_mod_nz_opp_full. + + rewrite Z.mod_small by apply Int63.to_Z_bounded. + split. + * rewrite <- Z.opp_le_mono. + now rewrite <- Z.sub_le_mono_l. + * transitivity 0%Z; [>| now apply Int63.to_Z_bounded]. + rewrite Z.opp_nonpos_nonneg. + apply Zle_minus_le_0. + apply Z.lt_le_incl. + now apply Int63.to_Z_bounded. + + rewrite Z.mod_small by apply Int63.to_Z_bounded. + now intros eqx0; rewrite eqx0 in leminx. +Qed. + +Lemma of_to_Z : forall x, of_Z (to_Z x) = x. +Proof. + unfold to_Z, of_Z. + intros x. + generalize (Int63.to_Z_bounded x). + case ltbP. + - intros ltxmin [leq0x _]. + generalize (Int63.of_to_Z x). + destruct (φ x%int63). + + now intros <-. + + now intros <-; unfold Int63.of_Z. + + now intros _. + - intros nltxmin leq0xltwB. + rewrite (opp_spec x). + rewrite Z_mod_nz_opp_full. + + rewrite Zmod_small by easy. + destruct (wB - φ x%int63) eqn: iswbmx. + * lia. + * simpl. + apply to_Z_inj. + rewrite opp_spec. + generalize (of_Z_spec (Z.pos p)). + simpl Int63.of_Z; intros ->. + rewrite <- iswbmx. + rewrite <- Z.sub_0_l. + rewrite <- (Zmod_0_l wB). + rewrite <- Zminus_mod. + replace (0 - _) with (φ x%int63 - wB) by ring. + rewrite <- Zminus_mod_idemp_r. + rewrite Z_mod_same_full. + rewrite Z.sub_0_r. + now rewrite Z.mod_small. + * lia. + + rewrite Z.mod_small by easy. + intros eqx0; revert nltxmin; rewrite eqx0. + now compute. +Qed. + +Lemma to_Z_inj (x y : int) : to_Z x = to_Z y -> x = y. +Proof. exact (fun e => can_inj of_to_Z e). Qed. + +Lemma to_Z_mod_Int63to_Z (x : int) : to_Z x mod wB = φ x%int63. +Proof. + unfold to_Z. + case ltbP; [> now rewrite Z.mod_small by now apply Int63.to_Z_bounded |]. + rewrite Z.nlt_ge; intros gexmin. + rewrite opp_to_Z_opp; rewrite Z.mod_small by now apply Int63.to_Z_bounded. + - easy. + - now intros neqx0; rewrite neqx0 in gexmin. +Qed. + + +(** Centered modulo *) +Definition cmod (x d : Z) : Z := + (x + d / 2) mod d - (d / 2). + +Lemma cmod_mod (x d : Z) : + cmod (x mod d) d = cmod x d. +Proof. + now unfold cmod; rewrite Zplus_mod_idemp_l. +Qed. + +Lemma cmod_small (x d : Z) : + - (d / 2) <= x < d / 2 -> cmod x d = x. +Proof. + intros bound. + unfold cmod. + rewrite Zmod_small; [> lia |]. + split; [> lia |]. + rewrite Z.lt_add_lt_sub_r. + apply (Z.lt_le_trans _ (d / 2)); [> easy |]. + now rewrite <- Z.le_add_le_sub_r, Z.add_diag, Z.mul_div_le. +Qed. + +Lemma to_Z_cmodwB (x : int) : + to_Z x = cmod (φ x%int63) wB. +Proof. + unfold to_Z, cmod. + case ltbP; change φ (min_int)%int63 with (wB / 2). + - intros ltxmin. + rewrite Z.mod_small; [> lia |]. + split. + + now apply Z.add_nonneg_nonneg; try apply Int63.to_Z_bounded. + + change wB with (wB / 2 + wB / 2) at 2; lia. + - rewrite Z.nlt_ge; intros gexmin. + rewrite Int63.opp_spec. + rewrite Z_mod_nz_opp_full. + + rewrite Z.mod_small by apply Int63.to_Z_bounded. + rewrite <- (Z_mod_plus_full _ (-1)). + change (-1 * wB) with (- (wB / 2) - wB / 2). + rewrite <- Z.add_assoc, Zplus_minus. + rewrite Z.mod_small. + * change wB with (wB / 2 + wB / 2) at 1; lia. + * split; [> lia |]. + apply Z.lt_sub_lt_add_r. + transitivity wB; [>| easy]. + now apply Int63.to_Z_bounded. + + rewrite Z.mod_small by now apply Int63.to_Z_bounded. + now intros not0; rewrite not0 in gexmin. +Qed. + +Lemma of_Z_spec (z : Z) : to_Z (of_Z z) = cmod z wB. +Proof. now rewrite to_Z_cmodwB, Int63.of_Z_spec, cmod_mod. Qed. + +Lemma of_Z_cmod (z : Z) : of_Z (cmod z wB) = of_Z z. +Proof. now rewrite <- of_Z_spec, of_to_Z. Qed. + +Lemma is_int (z : Z) : + to_Z min_int <= z <= to_Z max_int -> + z = to_Z (of_Z z). +Proof. + rewrite to_Z_min, to_Z_max. + intros bound; rewrite of_Z_spec, cmod_small; lia. +Qed. + +(** Specification of operations that differ on signed and unsigned ints *) + +Axiom asr_spec : forall x p, to_Z (x >> p) = (to_Z x) / 2 ^ (to_Z p). + +Axiom div_spec : forall x y, + to_Z x <> to_Z min_int \/ to_Z y <> (-1)%Z -> + to_Z (x / y) = Z.quot (to_Z x) (to_Z y). + +Axiom mod_spec : forall x y, to_Z (x mod y) = Z.rem (to_Z x) (to_Z y). + +Axiom ltb_spec : forall x y, (x to_Z x < to_Z y. + +Axiom leb_spec : forall x y, (x <=? y)%sint63 = true <-> to_Z x <= to_Z y. + +Axiom compare_spec : forall x y, (x ?= y)%sint63 = (to_Z x ?= to_Z y). + +(** Specification of operations that coincide on signed and unsigned ints *) + +Lemma add_spec (x y : int) : + to_Z (x + y)%sint63 = cmod (to_Z x + to_Z y) wB. +Proof. + rewrite to_Z_cmodwB, Int63.add_spec. + rewrite <- 2!to_Z_mod_Int63to_Z, <- Z.add_mod by easy. + now rewrite cmod_mod. +Qed. + +Lemma sub_spec (x y : int) : + to_Z (x - y)%sint63 = cmod (to_Z x - to_Z y) wB. +Proof. + rewrite to_Z_cmodwB, Int63.sub_spec. + rewrite <- 2!to_Z_mod_Int63to_Z, <- Zminus_mod by easy. + now rewrite cmod_mod. +Qed. + +Lemma mul_spec (x y : int) : + to_Z (x * y)%sint63 = cmod (to_Z x * to_Z y) wB. +Proof. + rewrite to_Z_cmodwB, Int63.mul_spec. + rewrite <- 2!to_Z_mod_Int63to_Z, <- Zmult_mod by easy. + now rewrite cmod_mod. +Qed. + +Lemma succ_spec (x : int) : + to_Z (succ x)%sint63 = cmod (to_Z x + 1) wB. +Proof. now unfold succ; rewrite add_spec. Qed. + +Lemma pred_spec (x : int) : + to_Z (pred x)%sint63 = cmod (to_Z x - 1) wB. +Proof. now unfold pred; rewrite sub_spec. Qed. + +Lemma opp_spec (x : int) : + to_Z (- x)%sint63 = cmod (- to_Z x) wB. +Proof. + rewrite to_Z_cmodwB, Int63.opp_spec. + rewrite <- Z.sub_0_l, <- to_Z_mod_Int63to_Z, Zminus_mod_idemp_r. + now rewrite cmod_mod. +Qed. + +(** Behaviour when there is no under or overflow *) + +Lemma add_bounded (x y : int) : + to_Z min_int <= to_Z x + to_Z y <= to_Z max_int -> + to_Z (x + y) = to_Z x + to_Z y. +Proof. + rewrite to_Z_min, to_Z_max; intros bound. + now rewrite add_spec, cmod_small; [>| lia]. +Qed. + +Lemma sub_bounded (x y : int) : + to_Z min_int <= to_Z x - to_Z y <= to_Z max_int -> + to_Z (x - y) = to_Z x - to_Z y. +Proof. + rewrite to_Z_min, to_Z_max; intros bound. + now rewrite sub_spec, cmod_small; [>| lia]. +Qed. + +Lemma mul_bounded (x y : int) : + to_Z min_int <= to_Z x * to_Z y <= to_Z max_int -> + to_Z (x * y) = to_Z x * to_Z y. +Proof. + rewrite to_Z_min, to_Z_max; intros bound. + now rewrite mul_spec, cmod_small; [>| lia]. +Qed. + +Lemma succ_bounded (x : int) : + to_Z min_int <= to_Z x + 1 <= to_Z max_int -> + to_Z (succ x) = to_Z x + 1. +Proof. + rewrite to_Z_min, to_Z_max; intros bound. + now rewrite succ_spec, cmod_small; [>| lia]. +Qed. + +Lemma pred_bounded (x : int) : + to_Z min_int <= to_Z x - 1 <= to_Z max_int -> + to_Z (pred x) = to_Z x - 1. +Proof. + rewrite to_Z_min, to_Z_max; intros bound. + now rewrite pred_spec, cmod_small; [>| lia]. +Qed. + +Lemma opp_bounded (x : int) : + to_Z min_int <= - to_Z x <= to_Z max_int -> + to_Z (- x) = - to_Z x. +Proof. + rewrite to_Z_min, to_Z_max; intros bound. + now rewrite opp_spec, cmod_small; [>| lia]. +Qed. + +(** Relationship with of_Z *) + +Lemma add_of_Z (x y : int) : + (x + y)%sint63 = of_Z (to_Z x + to_Z y). +Proof. now rewrite <- of_Z_cmod, <- add_spec, of_to_Z. Qed. + +Lemma sub_of_Z (x y : int) : + (x - y)%sint63 = of_Z (to_Z x - to_Z y). +Proof. now rewrite <- of_Z_cmod, <- sub_spec, of_to_Z. Qed. + +Lemma mul_of_Z (x y : int) : + (x * y)%sint63 = of_Z (to_Z x * to_Z y). +Proof. now rewrite <- of_Z_cmod, <- mul_spec, of_to_Z. Qed. + +Lemma succ_of_Z (x : int) : + (succ x)%sint63 = of_Z (to_Z x + 1). +Proof. now rewrite <- of_Z_cmod, <- succ_spec, of_to_Z. Qed. + +Lemma pred_of_Z (x : int) : + (pred x)%sint63 = of_Z (to_Z x - 1). +Proof. now rewrite <- of_Z_cmod, <- pred_spec, of_to_Z. Qed. + +Lemma opp_of_Z (x : int) : + (- x)%sint63 = of_Z (- to_Z x). +Proof. now rewrite <- of_Z_cmod, <- opp_spec, of_to_Z. Qed. + +(** Comparison *) +Import Bool. + +Lemma eqbP x y : reflect (to_Z x = to_Z y) (x =? y)%sint63. +Proof. + apply iff_reflect; rewrite Int63.eqb_spec. + now split; [> apply to_Z_inj | apply f_equal]. +Qed. + +Lemma ltbP x y : reflect (to_Z x < to_Z y) (x > i)%sint63 = 0%sint63. +Proof. now apply to_Z_inj; rewrite asr_spec. Qed. + +Lemma asr_0_r (i : int) : (i >> 0)%sint63 = i. +Proof. now apply to_Z_inj; rewrite asr_spec, Zdiv_1_r. Qed. + +Lemma asr_neg_r (i n : int) : to_Z n < 0 -> (i >> n)%sint63 = 0%sint63. +Proof. + intros ltn0. + apply to_Z_inj. + rewrite asr_spec, Z.pow_neg_r by assumption. + now rewrite Zdiv_0_r. +Qed. + +Lemma asr_1 (n : int) : (1 >> n)%sint63 = (n =? 0)%sint63. +Proof. + apply to_Z_inj; rewrite asr_spec. + case eqbP; [> now intros -> | intros neqn0]. + case (lebP 0 n). + - intros le0n. + apply Z.div_1_l; apply Z.pow_gt_1; [> easy |]. + rewrite to_Z_0 in *; lia. + - rewrite Z.nle_gt; intros ltn0. + now rewrite Z.pow_neg_r. +Qed. + +Notation asr := asr (only parsing). +Notation div := divs (only parsing). +Notation rem := mods (only parsing). +Notation ltb := ltsb (only parsing). +Notation leb := lesb (only parsing). +Notation compare := compares (only parsing). + +Module Export Sint63Notations. + Export Sint63NotationsInternalA. + Export Sint63NotationsInternalB. +End Sint63Notations. diff --git a/theories/dune b/theories/dune index 18e000cfe1..90e9522b7b 100644 --- a/theories/dune +++ b/theories/dune @@ -15,7 +15,6 @@ coq.plugins.firstorder coq.plugins.number_string_notation - coq.plugins.int63_syntax coq.plugins.float_syntax coq.plugins.btauto diff --git a/theories/extraction/ExtrOCamlInt63.v b/theories/extraction/ExtrOCamlInt63.v index 7f7b4af98d..1949a1a9d8 100644 --- a/theories/extraction/ExtrOCamlInt63.v +++ b/theories/extraction/ExtrOCamlInt63.v @@ -10,7 +10,7 @@ (** Extraction to OCaml of native 63-bit machine integers. *) -From Coq Require Int63 Extraction. +From Coq Require Int63 Sint63 Extraction. (** Basic data types used by some primitive operators. *) @@ -26,6 +26,7 @@ Extraction Inline Int63.int. Extract Constant Int63.lsl => "Uint63.l_sl". Extract Constant Int63.lsr => "Uint63.l_sr". +Extract Constant Sint63.asr => "Uint63.a_sr". Extract Constant Int63.land => "Uint63.l_and". Extract Constant Int63.lor => "Uint63.l_or". Extract Constant Int63.lxor => "Uint63.l_xor". @@ -36,10 +37,15 @@ Extract Constant Int63.mul => "Uint63.mul". Extract Constant Int63.mulc => "Uint63.mulc". Extract Constant Int63.div => "Uint63.div". Extract Constant Int63.mod => "Uint63.rem". +Extract Constant Sint63.div => "Uint63.divs". +Extract Constant Sint63.rem => "Uint63.rems". + Extract Constant Int63.eqb => "Uint63.equal". Extract Constant Int63.ltb => "Uint63.lt". Extract Constant Int63.leb => "Uint63.le". +Extract Constant Sint63.ltb => "Uint63.lts". +Extract Constant Sint63.leb => "Uint63.les". Extract Constant Int63.addc => "Uint63.addc". Extract Constant Int63.addcarryc => "Uint63.addcarryc". @@ -51,6 +57,7 @@ Extract Constant Int63.diveucl_21 => "Uint63.div21". Extract Constant Int63.addmuldiv => "Uint63.addmuldiv". Extract Constant Int63.compare => "Uint63.compare". +Extract Constant Sint63.compare => "Uint63.compares". Extract Constant Int63.head0 => "Uint63.head0". Extract Constant Int63.tail0 => "Uint63.tail0". -- cgit v1.2.3