aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Changelog4
-rw-r--r--MenhirLib/Alphabet.v2
-rw-r--r--aarch64/Asmexpand.ml5
-rw-r--r--arm/Asmexpand.ml4
-rw-r--r--flocq/Core/Raux.v4
-rw-r--r--flocq/Core/Zaux.v46
-rw-r--r--flocq/IEEE754/Binary.v4
-rw-r--r--flocq/IEEE754/Bits.v4
-rw-r--r--powerpc/Asmexpand.ml4
-rw-r--r--riscV/Asmexpand.ml4
10 files changed, 34 insertions, 47 deletions
diff --git a/Changelog b/Changelog
index aa57a554..d3a4cc4b 100644
--- a/Changelog
+++ b/Changelog
@@ -1,3 +1,7 @@
+Coq development:
+- Updated the Flocq library to version 3.4.2.
+
+
Release 3.9, 2021-05-10
=======================
diff --git a/MenhirLib/Alphabet.v b/MenhirLib/Alphabet.v
index 530e3b4a..cd849761 100644
--- a/MenhirLib/Alphabet.v
+++ b/MenhirLib/Alphabet.v
@@ -11,7 +11,7 @@
(* *)
(****************************************************************************)
-From Coq Require Import Omega List Relations RelationClasses.
+From Coq Require Import ZArith List Relations RelationClasses.
Import ListNotations.
Local Obligation Tactic := intros.
diff --git a/aarch64/Asmexpand.ml b/aarch64/Asmexpand.ml
index d24a9ef6..573e8b92 100644
--- a/aarch64/Asmexpand.ml
+++ b/aarch64/Asmexpand.ml
@@ -185,14 +185,15 @@ let memcpy_small_arg sz arg tmp =
| BA_addrstack ofs ->
if offset_in_range ofs
&& offset_in_range (Ptrofs.add ofs (Ptrofs.repr (Z.of_uint sz)))
+ && Int64.rem (Z.to_int64 ofs) 8L = 0L
then (XSP, ofs)
else begin expand_addimm64 (RR1 tmp) XSP ofs; (RR1 tmp, _0) end
| _ ->
assert false
let expand_builtin_memcpy_small sz al src dst =
- let (tsrc, tdst) =
- if dst <> BA (IR X17) then (X17, X29) else (X29, X17) in
+ let tsrc = if dst <> BA (IR X17) then X17 else X29 in
+ let tdst = if src <> BA (IR X29) then X29 else X17 in
let (rsrc, osrc) = memcpy_small_arg sz src tsrc in
let (rdst, odst) = memcpy_small_arg sz dst tdst in
let rec copy osrc odst sz =
diff --git a/arm/Asmexpand.ml b/arm/Asmexpand.ml
index 01b18c37..223cf7fc 100644
--- a/arm/Asmexpand.ml
+++ b/arm/Asmexpand.ml
@@ -111,8 +111,8 @@ let memcpy_small_arg sz arg tmp =
assert false
let expand_builtin_memcpy_small sz al src dst =
- let (tsrc, tdst) =
- if dst <> BA (IR IR2) then (IR2, IR3) else (IR3, IR2) in
+ let tsrc = if dst <> BA (IR IR2) then IR2 else IR3 in
+ let tdst = if src <> BA (IR IR3) then IR3 else IR2 in
let (rsrc, osrc) = memcpy_small_arg sz src tsrc in
let (rdst, odst) = memcpy_small_arg sz dst tdst in
let rec copy osrc odst sz =
diff --git a/flocq/Core/Raux.v b/flocq/Core/Raux.v
index 455190dc..221d84d6 100644
--- a/flocq/Core/Raux.v
+++ b/flocq/Core/Raux.v
@@ -18,7 +18,7 @@ COPYING file for more details.
*)
(** * Missing definitions/lemmas *)
-Require Export Psatz.
+Require Import Psatz.
Require Export Reals ZArith.
Require Export Zaux.
@@ -1277,7 +1277,7 @@ Theorem Zfloor_div :
Zfloor (IZR x / IZR y) = (x / y)%Z.
Proof.
intros x y Zy.
-generalize (Z_div_mod_eq_full x y Zy).
+generalize (Z.div_mod x y Zy).
intros Hx.
rewrite Hx at 1.
assert (Zy': IZR y <> 0%R).
diff --git a/flocq/Core/Zaux.v b/flocq/Core/Zaux.v
index b40b0c4f..5ca3971f 100644
--- a/flocq/Core/Zaux.v
+++ b/flocq/Core/Zaux.v
@@ -327,18 +327,10 @@ Theorem Zmod_mod_mult :
forall n a b, (0 < a)%Z -> (0 <= b)%Z ->
Zmod (Zmod n (a * b)) b = Zmod n b.
Proof.
-intros n a [|b|b] Ha Hb.
-now rewrite 2!Zmod_0_r.
-rewrite (Zmod_eq n (a * Zpos b)).
-rewrite Zmult_assoc.
-unfold Zminus.
-rewrite Zopp_mult_distr_l.
-apply Z_mod_plus.
-easy.
-apply Zmult_gt_0_compat.
-now apply Z.lt_gt.
-easy.
-now elim Hb.
+ intros n a b Ha Hb. destruct (Zle_lt_or_eq _ _ Hb) as [H'b|H'b].
+ - rewrite (Z.mul_comm a b), Z.rem_mul_r, Z.add_mod, Z.mul_mod, Z.mod_same,
+ Z.mul_0_l, Z.mod_0_l, Z.add_0_r, !Z.mod_mod; lia.
+ - subst. now rewrite Z.mul_0_r, !Zmod_0_r.
Qed.
Theorem ZOmod_eq :
@@ -370,24 +362,14 @@ Theorem Zdiv_mod_mult :
(Z.div (Zmod n (a * b)) a) = Zmod (Z.div n a) b.
Proof.
intros n a b Ha Hb.
-destruct (Zle_lt_or_eq _ _ Ha) as [Ha'|Ha'].
-destruct (Zle_lt_or_eq _ _ Hb) as [Hb'|Hb'].
-rewrite (Zmod_eq n (a * b)).
-rewrite (Zmult_comm a b) at 2.
-rewrite Zmult_assoc.
-unfold Zminus.
-rewrite Zopp_mult_distr_l.
-rewrite Z_div_plus by now apply Z.lt_gt.
-rewrite <- Zdiv_Zdiv by easy.
-apply sym_eq.
-apply Zmod_eq.
-now apply Z.lt_gt.
-now apply Zmult_gt_0_compat ; apply Z.lt_gt.
-rewrite <- Hb'.
-rewrite Zmult_0_r, 2!Zmod_0_r.
-apply Zdiv_0_l.
-rewrite <- Ha'.
-now rewrite 2!Zdiv_0_r, Zmod_0_l.
+destruct (Zle_lt_or_eq _ _ Ha) as [Ha'|<-].
+- destruct (Zle_lt_or_eq _ _ Hb) as [Hb'|<-].
+ + rewrite Z.rem_mul_r, Z.add_comm, Z.mul_comm, Z.div_add_l by lia.
+ rewrite (Zdiv_small (Zmod n a)).
+ apply Z.add_0_r.
+ now apply Z.mod_pos_bound.
+ + now rewrite Z.mul_0_r, !Zmod_0_r, ?Zdiv_0_l.
+- now rewrite Z.mul_0_l, !Zdiv_0_r, Zmod_0_l.
Qed.
Theorem ZOdiv_mod_mult :
@@ -856,7 +838,7 @@ Definition Zfast_div_eucl (a b : Z) :=
| Z0 => (0, 0)%Z
| Zpos a' =>
match b with
- | Z0 => (0, 0)%Z
+ | Z0 => (0, (match (1 mod 0) with | 0 => 0 | _ => a end))%Z
| Zpos b' => Zpos_div_eucl_aux a' b'
| Zneg b' =>
let (q, r) := Zpos_div_eucl_aux a' b' in
@@ -868,7 +850,7 @@ Definition Zfast_div_eucl (a b : Z) :=
end
| Zneg a' =>
match b with
- | Z0 => (0, 0)%Z
+ | Z0 => (0, (match (1 mod 0) with | 0 => 0 | _ => a end))%Z
| Zpos b' =>
let (q, r) := Zpos_div_eucl_aux a' b' in
match r with
diff --git a/flocq/IEEE754/Binary.v b/flocq/IEEE754/Binary.v
index 35d15cb3..4516f0a0 100644
--- a/flocq/IEEE754/Binary.v
+++ b/flocq/IEEE754/Binary.v
@@ -2472,9 +2472,9 @@ case f.
now revert Hover; unfold B2R, F2R; simpl; rewrite Rmult_assoc, bpow_plus.
Qed.
-(** This hypothesis is needed to implement Bfrexp
+(** This hypothesis is needed to implement [Bfrexp]
(otherwise, we have emin > - prec
- and Bfrexp cannot fit the mantissa in interval [0.5, 1)) *)
+ and [Bfrexp] cannot fit the mantissa in interval #[0.5, 1)#) *)
Hypothesis Hemax : (3 <= emax)%Z.
Definition Ffrexp_core_binary s m e :=
diff --git a/flocq/IEEE754/Bits.v b/flocq/IEEE754/Bits.v
index 68bc541a..3c19e31b 100644
--- a/flocq/IEEE754/Bits.v
+++ b/flocq/IEEE754/Bits.v
@@ -163,11 +163,11 @@ Proof.
intros x Hx.
unfold split_bits, join_bits.
rewrite Z.shiftl_mul_pow2 by now apply Zlt_le_weak.
-pattern x at 4 ; rewrite Z_div_mod_eq_full with x (2^mw)%Z.
+pattern x at 4 ; rewrite Z.div_mod with x (2^mw)%Z.
apply (f_equal (fun v => (v + _)%Z)).
rewrite Zmult_comm.
apply f_equal.
-pattern (x / (2^mw))%Z at 2 ; rewrite Z_div_mod_eq_full with (x / (2^mw))%Z (2^ew)%Z.
+pattern (x / (2^mw))%Z at 2 ; rewrite Z.div_mod with (x / (2^mw))%Z (2^ew)%Z.
apply (f_equal (fun v => (v + _)%Z)).
replace (x / 2 ^ mw / 2 ^ ew)%Z with (if Zle_bool (2 ^ mw * 2 ^ ew) x then 1 else 0)%Z.
case Zle_bool.
diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index 7efa80a6..45b3f708 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -118,8 +118,8 @@ let memcpy_small_arg sz arg tmp =
assert false
let expand_builtin_memcpy_small sz al src dst =
- let (tsrc, tdst) =
- if dst <> BA (IR GPR11) then (GPR11, GPR12) else (GPR12, GPR11) in
+ let tsrc = if dst <> BA (IR GPR11) then GPR11 else GPR12 in
+ let tdst = if dst <> BA (IR GPR12) then GPR12 else GPR11 in
let (rsrc, osrc) = memcpy_small_arg sz src tsrc in
let (rdst, odst) = memcpy_small_arg sz dst tdst in
let rec copy osrc odst sz =
diff --git a/riscV/Asmexpand.ml b/riscV/Asmexpand.ml
index dc0ec184..ab0e6fee 100644
--- a/riscV/Asmexpand.ml
+++ b/riscV/Asmexpand.ml
@@ -170,8 +170,8 @@ let memcpy_small_arg sz arg tmp =
assert false
let expand_builtin_memcpy_small sz al src dst =
- let (tsrc, tdst) =
- if dst <> BA (IR X5) then (X5, X6) else (X6, X5) in
+ let tsrc = if dst <> BA (IR X5) then X5 else X6 in
+ let tdst = if src <> BA (IR X6) then X6 else X5 in
let (rsrc, osrc) = memcpy_small_arg sz src tsrc in
let (rdst, odst) = memcpy_small_arg sz dst tdst in
let rec copy osrc odst sz =
generated by cgit (git 2.34.1) at 2024-07-04 11:34:05 +0000