From b4abefba4ec266b66a57f307ad1c6c3d3064b585 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 21 Sep 2020 15:42:20 +0200
Subject: [PATCH] [wp] upgrade coq resources
---
src/plugins/wp/share/coqwp/Vlist.v | 7 +-
.../coqwp/int/ComputerOfEuclideanDivision.v | 64 ++++++++--------
.../wp/share/coqwp/int/EuclideanDivision.v | 74 ++++++++++---------
3 files changed, 76 insertions(+), 69 deletions(-)
diff --git a/src/plugins/wp/share/coqwp/Vlist.v b/src/plugins/wp/share/coqwp/Vlist.v
index 62ef751f993..f91fabec5d1 100644
--- a/src/plugins/wp/share/coqwp/Vlist.v
+++ b/src/plugins/wp/share/coqwp/Vlist.v
@@ -40,6 +40,7 @@ Hint Rewrite List.app_assoc List.app_nil_l List.app_nil_r : list.
(* --- Classical Lists for Alt-Ergo --- *)
(* -------------------------------------------------------------------- *)
Require Import Qedlib.
+Require Import Lia.
(* Why3 goal *)
Definition list : forall (a:Type), Type.
@@ -399,11 +400,7 @@ intros p q w h1 h2. unfold vlist_eq ; simpl ; split ; auto with zarith.
rewrite length_repeat ; auto with zarith.
replace (i - p * length A) with (i + (-p) * length A).
rewrite Z.rem_add ; auto with zarith.
- apply Z.mul_nonneg_nonneg ; auto with zarith.
- replace (i + -p * length A) with (i - p * length A) ; auto with zarith.
- rewrite Z.mul_opp_l. rewrite Z.add_opp_r. auto.
- rewrite Z.mul_opp_l. rewrite Z.add_opp_r. auto.
- rewrite length_repeat ; auto with zarith.
+ lia. rewrite length_repeat. lia. auto.
Qed.
(* Why3 goal *)
diff --git a/src/plugins/wp/share/coqwp/int/ComputerOfEuclideanDivision.v b/src/plugins/wp/share/coqwp/int/ComputerOfEuclideanDivision.v
index f9fb43d9194..1ee49b12af3 100644
--- a/src/plugins/wp/share/coqwp/int/ComputerOfEuclideanDivision.v
+++ b/src/plugins/wp/share/coqwp/int/ComputerOfEuclideanDivision.v
@@ -1,13 +1,13 @@
-(**************************************************************************)
-(* *)
-(* The Why3 Verification Platform / The Why3 Development Team *)
-(* Copyright 2010-2019 -- Inria - CNRS - Paris-Sud University *)
-(* *)
-(* This software is distributed under the terms of the GNU Lesser *)
-(* General Public License version 2.1, with the special exception *)
-(* on linking described in file LICENSE. *)
-(* *)
-(**************************************************************************)
+(********************************************************************)
+(* *)
+(* The Why3 Verification Platform / The Why3 Development Team *)
+(* Copyright 2010-2020 -- Inria - CNRS - Paris-Sud University *)
+(* *)
+(* This software is distributed under the terms of the GNU Lesser *)
+(* General Public License version 2.1, with the special exception *)
+(* on linking described in file LICENSE. *)
+(* *)
+(********************************************************************)
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
@@ -29,19 +29,19 @@ case (Z_le_dec 0 (n mod (Zpos d))); intros H2.
* destruct (H2 H0).
Qed.
-
(* Why3 goal *)
-Lemma cdiv_cases : forall (n:Z) (d:Z), ((0%Z <= n)%Z -> ((0%Z < d)%Z ->
- ((ZArith.BinInt.Z.quot n d) = (int.EuclideanDivision.div n d)))) /\
- (((n <= 0%Z)%Z -> ((0%Z < d)%Z ->
- ((ZArith.BinInt.Z.quot n d) = (-(int.EuclideanDivision.div (-n)%Z
- d))%Z))) /\ (((0%Z <= n)%Z -> ((d < 0%Z)%Z ->
- ((ZArith.BinInt.Z.quot n d) = (-(int.EuclideanDivision.div n
- (-d)%Z))%Z))) /\ ((n <= 0%Z)%Z -> ((d < 0%Z)%Z ->
- ((ZArith.BinInt.Z.quot n d) = (int.EuclideanDivision.div (-n)%Z
- (-d)%Z)))))).
+Lemma cdiv_cases :
+ forall (n:Numbers.BinNums.Z) (d:Numbers.BinNums.Z),
+ ((0%Z <= n)%Z -> (0%Z < d)%Z ->
+ ((ZArith.BinInt.Z.quot n d) = (int.EuclideanDivision.div n d))) /\
+ ((n <= 0%Z)%Z -> (0%Z < d)%Z ->
+ ((ZArith.BinInt.Z.quot n d) = (-(int.EuclideanDivision.div (-n)%Z d))%Z)) /\
+ ((0%Z <= n)%Z -> (d < 0%Z)%Z ->
+ ((ZArith.BinInt.Z.quot n d) = (-(int.EuclideanDivision.div n (-d)%Z))%Z)) /\
+ ((n <= 0%Z)%Z -> (d < 0%Z)%Z ->
+ ((ZArith.BinInt.Z.quot n d) = (int.EuclideanDivision.div (-n)%Z (-d)%Z))).
intros n d.
- destruct d as [|d|d]; destruct n as [|n|n]; intuition (try contradiction; try discriminate; auto).
+ destruct d as [|d|d]; destruct n as [|n|n]; intuition (try discriminate; try contradiction).
+ assert (NZ_d:((Zpos d) <> 0)%Z) by discriminate.
rewrite (Z.quot_div (Z.pos n) (Z.pos d) NZ_d).
rewrite on_pos_euclidean_is_div.
@@ -64,15 +64,17 @@ Lemma cdiv_cases : forall (n:Z) (d:Z), ((0%Z <= n)%Z -> ((0%Z < d)%Z ->
Qed.
(* Why3 goal *)
-Lemma cmod_cases : forall (n:Z) (d:Z), ((0%Z <= n)%Z -> ((0%Z < d)%Z ->
- ((ZArith.BinInt.Z.rem n d) = (int.EuclideanDivision.mod1 n d)))) /\
- (((n <= 0%Z)%Z -> ((0%Z < d)%Z ->
- ((ZArith.BinInt.Z.rem n d) = (-(int.EuclideanDivision.mod1 (-n)%Z
- d))%Z))) /\ (((0%Z <= n)%Z -> ((d < 0%Z)%Z ->
- ((ZArith.BinInt.Z.rem n d) = (int.EuclideanDivision.mod1 n (-d)%Z)))) /\
- ((n <= 0%Z)%Z -> ((d < 0%Z)%Z ->
- ((ZArith.BinInt.Z.rem n d) = (-(int.EuclideanDivision.mod1 (-n)%Z
- (-d)%Z))%Z))))).
+Lemma cmod_cases :
+ forall (n:Numbers.BinNums.Z) (d:Numbers.BinNums.Z),
+ ((0%Z <= n)%Z -> (0%Z < d)%Z ->
+ ((ZArith.BinInt.Z.rem n d) = (int.EuclideanDivision.mod1 n d))) /\
+ ((n <= 0%Z)%Z -> (0%Z < d)%Z ->
+ ((ZArith.BinInt.Z.rem n d) = (-(int.EuclideanDivision.mod1 (-n)%Z d))%Z)) /\
+ ((0%Z <= n)%Z -> (d < 0%Z)%Z ->
+ ((ZArith.BinInt.Z.rem n d) = (int.EuclideanDivision.mod1 n (-d)%Z))) /\
+ ((n <= 0%Z)%Z -> (d < 0%Z)%Z ->
+ ((ZArith.BinInt.Z.rem n d) =
+ (-(int.EuclideanDivision.mod1 (-n)%Z (-d)%Z))%Z)).
intros n d.
unfold int.EuclideanDivision.mod1.
assert (Z.rem n d = n - (d * (Z.quot n d)))%Z.
@@ -80,7 +82,7 @@ Lemma cmod_cases : forall (n:Z) (d:Z), ((0%Z <= n)%Z -> ((0%Z < d)%Z ->
omega.
rewrite H.
assert (H2:=cdiv_cases n d).
- intuition.
+ intuition idtac.
+ rewrite H1.
reflexivity.
+ rewrite H4.
diff --git a/src/plugins/wp/share/coqwp/int/EuclideanDivision.v b/src/plugins/wp/share/coqwp/int/EuclideanDivision.v
index 45c05b8a8ab..816b3451613 100644
--- a/src/plugins/wp/share/coqwp/int/EuclideanDivision.v
+++ b/src/plugins/wp/share/coqwp/int/EuclideanDivision.v
@@ -1,13 +1,13 @@
-(**************************************************************************)
-(* *)
-(* The Why3 Verification Platform / The Why3 Development Team *)
-(* Copyright 2010-2019 -- Inria - CNRS - Paris-Sud University *)
-(* *)
-(* This software is distributed under the terms of the GNU Lesser *)
-(* General Public License version 2.1, with the special exception *)
-(* on linking described in file LICENSE. *)
-(* *)
-(**************************************************************************)
+(********************************************************************)
+(* *)
+(* The Why3 Verification Platform / The Why3 Development Team *)
+(* Copyright 2010-2020 -- Inria - CNRS - Paris-Sud University *)
+(* *)
+(* This software is distributed under the terms of the GNU Lesser *)
+(* General Public License version 2.1, with the special exception *)
+(* on linking described in file LICENSE. *)
+(* *)
+(********************************************************************)
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
@@ -17,7 +17,7 @@ Require int.Int.
Require int.Abs.
(* Why3 goal *)
-Definition div : Z -> Z -> Z.
+Definition div : Numbers.BinNums.Z -> Numbers.BinNums.Z -> Numbers.BinNums.Z.
intros x y.
case (Z_le_dec 0 (Zmod x y)) ; intros H.
exact (Z.div x y).
@@ -25,14 +25,16 @@ exact (Z.div x y + 1)%Z.
Defined.
(* Why3 goal *)
-Definition mod1 : Z -> Z -> Z.
+Definition mod1 :
+ Numbers.BinNums.Z -> Numbers.BinNums.Z -> Numbers.BinNums.Z.
intros x y.
exact (x - y * div x y)%Z.
Defined.
(* Why3 goal *)
Lemma Div_mod :
- forall (x:Z) (y:Z), ~ (y = 0%Z) -> (x = ((y * (div x y))%Z + (mod1 x y))%Z).
+ forall (x:Numbers.BinNums.Z) (y:Numbers.BinNums.Z), ~ (y = 0%Z) ->
+ (x = ((y * (div x y))%Z + (mod1 x y))%Z).
intros x y Zy.
unfold mod1, div.
case Z_le_dec ; intros H ; ring.
@@ -40,10 +42,10 @@ Qed.
(* Why3 goal *)
Lemma Mod_bound :
- forall (x:Z) (y:Z), ~ (y = 0%Z) ->
+ forall (x:Numbers.BinNums.Z) (y:Numbers.BinNums.Z), ~ (y = 0%Z) ->
(0%Z <= (mod1 x y))%Z /\ ((mod1 x y) < (ZArith.BinInt.Z.abs y))%Z.
intros x y Zy.
-zify.
+assert (H := Zabs_spec y).
assert (H1 := Z_mod_neg x y).
assert (H2 := Z_mod_lt x y).
unfold mod1, div.
@@ -57,8 +59,9 @@ Qed.
(* Why3 goal *)
Lemma Div_unique :
- forall (x:Z) (y:Z) (q:Z), (0%Z < y)%Z ->
- (((q * y)%Z <= x)%Z /\ (x < ((q * y)%Z + y)%Z)%Z) -> ((div x y) = q).
+ forall (x:Numbers.BinNums.Z) (y:Numbers.BinNums.Z) (q:Numbers.BinNums.Z),
+ (0%Z < y)%Z -> ((q * y)%Z <= x)%Z /\ (x < ((q * y)%Z + y)%Z)%Z ->
+ ((div x y) = q).
intros x y q h1 (h2,h3).
assert (h:(~(y=0))%Z) by omega.
generalize (Mod_bound x y h); intro h0.
@@ -80,8 +83,8 @@ Qed.
(* Why3 goal *)
Lemma Div_bound :
- forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z < y)%Z) ->
- (0%Z <= (div x y))%Z /\ ((div x y) <= x)%Z.
+ forall (x:Numbers.BinNums.Z) (y:Numbers.BinNums.Z),
+ (0%Z <= x)%Z /\ (0%Z < y)%Z -> (0%Z <= (div x y))%Z /\ ((div x y) <= x)%Z.
intros x y (Hx,Hy).
unfold div.
case Z_le_dec ; intros H.
@@ -100,7 +103,7 @@ now apply Z.lt_gt.
Qed.
(* Why3 goal *)
-Lemma Mod_1 : forall (x:Z), ((mod1 x 1%Z) = 0%Z).
+Lemma Mod_1 : forall (x:Numbers.BinNums.Z), ((mod1 x 1%Z) = 0%Z).
intros x.
unfold mod1, div.
rewrite Zmod_1_r, Zdiv_1_r, Zmult_1_l.
@@ -108,7 +111,7 @@ apply Zminus_diag.
Qed.
(* Why3 goal *)
-Lemma Div_1 : forall (x:Z), ((div x 1%Z) = x).
+Lemma Div_1 : forall (x:Numbers.BinNums.Z), ((div x 1%Z) = x).
intros x.
unfold div.
now rewrite Zmod_1_r, Zdiv_1_r.
@@ -116,7 +119,8 @@ Qed.
(* Why3 goal *)
Lemma Div_inf :
- forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (x < y)%Z) -> ((div x y) = 0%Z).
+ forall (x:Numbers.BinNums.Z) (y:Numbers.BinNums.Z),
+ (0%Z <= x)%Z /\ (x < y)%Z -> ((div x y) = 0%Z).
intros x y Hxy.
unfold div.
case Z_le_dec ; intros H.
@@ -127,8 +131,8 @@ Qed.
(* Why3 goal *)
Lemma Div_inf_neg :
- forall (x:Z) (y:Z), ((0%Z < x)%Z /\ (x <= y)%Z) ->
- ((div (-x)%Z y) = (-1%Z)%Z).
+ forall (x:Numbers.BinNums.Z) (y:Numbers.BinNums.Z),
+ (0%Z < x)%Z /\ (x <= y)%Z -> ((div (-x)%Z y) = (-1%Z)%Z).
intros x y Hxy.
assert (h: (x < y \/ x = y)%Z) by omega.
destruct h.
@@ -159,7 +163,8 @@ rewrite Z_div_same_full; auto with zarith.
Qed.
(* Why3 goal *)
-Lemma Mod_0 : forall (y:Z), ~ (y = 0%Z) -> ((mod1 0%Z y) = 0%Z).
+Lemma Mod_0 :
+ forall (y:Numbers.BinNums.Z), ~ (y = 0%Z) -> ((mod1 0%Z y) = 0%Z).
intros y Hy.
unfold mod1, div.
rewrite Zmod_0_l.
@@ -168,14 +173,15 @@ now rewrite Zdiv_0_l, Zmult_0_r.
Qed.
(* Why3 goal *)
-Lemma Div_1_left : forall (y:Z), (1%Z < y)%Z -> ((div 1%Z y) = 0%Z).
+Lemma Div_1_left :
+ forall (y:Numbers.BinNums.Z), (1%Z < y)%Z -> ((div 1%Z y) = 0%Z).
intros y Hy.
rewrite Div_inf; auto with zarith.
Qed.
(* Why3 goal *)
Lemma Div_minus1_left :
- forall (y:Z), (1%Z < y)%Z -> ((div (-1%Z)%Z y) = (-1%Z)%Z).
+ forall (y:Numbers.BinNums.Z), (1%Z < y)%Z -> ((div (-1%Z)%Z y) = (-1%Z)%Z).
intros y Hy.
unfold div.
assert (h1: (1 mod y = 1)%Z).
@@ -189,7 +195,8 @@ rewrite Zdiv_small; auto with zarith.
Qed.
(* Why3 goal *)
-Lemma Mod_1_left : forall (y:Z), (1%Z < y)%Z -> ((mod1 1%Z y) = 1%Z).
+Lemma Mod_1_left :
+ forall (y:Numbers.BinNums.Z), (1%Z < y)%Z -> ((mod1 1%Z y) = 1%Z).
intros y Hy.
unfold mod1.
rewrite Div_1_left; auto with zarith.
@@ -197,7 +204,8 @@ Qed.
(* Why3 goal *)
Lemma Mod_minus1_left :
- forall (y:Z), (1%Z < y)%Z -> ((mod1 (-1%Z)%Z y) = (y - 1%Z)%Z).
+ forall (y:Numbers.BinNums.Z), (1%Z < y)%Z ->
+ ((mod1 (-1%Z)%Z y) = (y - 1%Z)%Z).
intros y Hy.
unfold mod1.
rewrite Div_minus1_left; auto with zarith.
@@ -207,8 +215,8 @@ Open Scope Z_scope.
(* Why3 goal *)
Lemma Div_mult :
- forall (x:Z) (y:Z) (z:Z), (0%Z < x)%Z ->
- ((div ((x * y)%Z + z)%Z x) = (y + (div z x))%Z).
+ forall (x:Numbers.BinNums.Z) (y:Numbers.BinNums.Z) (z:Numbers.BinNums.Z),
+ (0%Z < x)%Z -> ((div ((x * y)%Z + z)%Z x) = (y + (div z x))%Z).
intros x y z h.
unfold div.
destruct (Z_le_dec 0 (z mod x)).
@@ -221,8 +229,8 @@ Qed.
(* Why3 goal *)
Lemma Mod_mult :
- forall (x:Z) (y:Z) (z:Z), (0%Z < x)%Z ->
- ((mod1 ((x * y)%Z + z)%Z x) = (mod1 z x)).
+ forall (x:Numbers.BinNums.Z) (y:Numbers.BinNums.Z) (z:Numbers.BinNums.Z),
+ (0%Z < x)%Z -> ((mod1 ((x * y)%Z + z)%Z x) = (mod1 z x)).
intros x y z h.
unfold mod1.
rewrite Div_mult.
--
GitLab