diff --git a/src/plugins/wp/share/Makefile.resources b/src/plugins/wp/share/Makefile.resources
index ea63e1e894360f056b5fc4133a0d97cf40ab1b01..fdd317b4ee803a3fbe387668efd5106193f34333 100644
--- a/src/plugins/wp/share/Makefile.resources
+++ b/src/plugins/wp/share/Makefile.resources
@@ -64,11 +64,14 @@ COQ_LIBS_CEA:= \
## Used in share/coqwp only
COQ_LIBS_INRIA:=\
BuiltIn.v \
+ HighOrd.v \
bool/Bool.v \
int/Abs.v \
int/ComputerDivision.v \
+ int/Exponentiation.v \
int/Int.v \
int/MinMax.v \
+ int/Power.v \
map/Map.v \
map/Const.v \
real/Abs.v \
diff --git a/src/plugins/wp/share/coqwp/Bits.v b/src/plugins/wp/share/coqwp/Bits.v
index 0381e15181d8c41bcc35734f624d9fe24be8dfa4..624a253f499923ab9206ce27fe7bd78ca4313ce8 100644
--- a/src/plugins/wp/share/coqwp/Bits.v
+++ b/src/plugins/wp/share/coqwp/Bits.v
@@ -587,7 +587,7 @@ Qed.
(** {@integer:} *)
(** * Bits of Integers *)
-Open Local Scope Z_scope.
+Local Open Scope Z_scope.
(** The bits representation of an integer consists of a bit function,
packed with its trailing property.
diff --git a/src/plugins/wp/share/coqwp/Cbits.v b/src/plugins/wp/share/coqwp/Cbits.v
index aff75e9b1e9667a2d0cf74393c4fae83a97721f2..c32a1cf32a5ab401e78c78dae72c60082d138dfd 100644
--- a/src/plugins/wp/share/coqwp/Cbits.v
+++ b/src/plugins/wp/share/coqwp/Cbits.v
@@ -167,7 +167,7 @@ Proof.
Qed.
Require Import Qedlib.
-Open Local Scope Z_scope.
+Local Open Scope Z_scope.
(** * Bit extraction *)
(** Tacticals *)
diff --git a/src/plugins/wp/share/coqwp/Cint.v b/src/plugins/wp/share/coqwp/Cint.v
index 3a7c0ab7042f7c00f5b022ea1231af44ac2904d5..1f80f9e6d3254d795bbfa37f0ff06dfb57d97db2 100644
--- a/src/plugins/wp/share/coqwp/Cint.v
+++ b/src/plugins/wp/share/coqwp/Cint.v
@@ -117,7 +117,7 @@ Proof.
intros x. unfold to_bool. induction (Z.eqb_spec x 0%Z) ; intuition.
Qed.
-Open Local Scope Z_scope.
+Local Open Scope Z_scope.
Definition to_range a b z := a + (z-a) mod (b-a).
@@ -328,7 +328,6 @@ Proof. to_range.
Qed.
(** * C-Integer Conversions are identity when in-range *)
-Open Local Scope Z_scope.
Remark mod_kn_mod_n: forall (k:Z) (n:Z) (x:Z), k>0 -> n>0 -> (x mod (k*n)) mod n = x mod n.
Proof.
diff --git a/src/plugins/wp/share/coqwp/HighOrd.v b/src/plugins/wp/share/coqwp/HighOrd.v
new file mode 100644
index 0000000000000000000000000000000000000000..da42135acf8f61280beecc37296a761f70134ca4
--- /dev/null
+++ b/src/plugins/wp/share/coqwp/HighOrd.v
@@ -0,0 +1,25 @@
+(********************************************************************)
+(* *)
+(* 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. *)
+(* *)
+(********************************************************************)
+
+Require Import BuiltIn.
+
+Definition func : forall (a:Type) (b:Type), Type.
+intros a b.
+exact (a -> b).
+Defined.
+
+Definition infix_at: forall {a:Type} {a_WT:WhyType a}
+ {b:Type} {b_WT:WhyType b}, (a -> b) -> a -> b.
+intros a aWT b bWT f x.
+exact (f x).
+Defined.
+
+Definition pred (a: Type) := func a bool.
diff --git a/src/plugins/wp/share/coqwp/Memory.v b/src/plugins/wp/share/coqwp/Memory.v
index a8aa1ff53a88bac2c385d7bc61603d29ac53173f..a586724d831b0224f3aedf8d52b4c80f9f1549ed 100644
--- a/src/plugins/wp/share/coqwp/Memory.v
+++ b/src/plugins/wp/share/coqwp/Memory.v
@@ -143,7 +143,7 @@ Definition separated (p:addr) (a:Z) (q:addr) (b:Z): Prop := (a <= 0%Z)%Z \/
(* Why3 assumption *)
Definition eqmem {a:Type} {a_WT:WhyType a} (m1:(map.Map.map addr a))
(m2:(map.Map.map addr a)) (p:addr) (a1:Z): Prop := forall (q:addr),
- (included q 1%Z p a1) -> ((map.Map.get m1 q) = (map.Map.get m2 q)).
+ (included q 1%Z p a1) -> ((m1 q) = (m2 q)).
(* Why3 goal *)
Definition havoc: forall {a:Type} {a_WT:WhyType a}, (map.Map.map addr a) ->
@@ -160,16 +160,16 @@ Definition fhavoc {A : Type}
(* Why3 assumption *)
Definition valid_rw (m:(map.Map.map Z Z)) (p:addr) (n:Z): Prop :=
(0%Z < n)%Z -> ((0%Z < (base p))%Z /\ ((0%Z <= (offset p))%Z /\
- (((offset p) + n)%Z <= (map.Map.get m (base p)))%Z)).
+ (((offset p) + n)%Z <= (m (base p)))%Z)).
(* Why3 assumption *)
Definition valid_rd (m:(map.Map.map Z Z)) (p:addr) (n:Z): Prop :=
(0%Z < n)%Z -> ((~ (0%Z = (base p))) /\ ((0%Z <= (offset p))%Z /\
- (((offset p) + n)%Z <= (map.Map.get m (base p)))%Z)).
+ (((offset p) + n)%Z <= (m (base p)))%Z)).
(* Why3 assumption *)
Definition invalid (m:(map.Map.map Z Z)) (p:addr) (n:Z): Prop :=
- (0%Z < n)%Z -> (((map.Map.get m (base p)) <= (offset p))%Z \/
+ (0%Z < n)%Z -> (((m (base p)) <= (offset p))%Z \/
(((offset p) + n)%Z <= 0%Z)%Z).
(* Why3 goal *)
@@ -184,7 +184,7 @@ Qed.
(* Why3 goal *)
Lemma valid_string : forall (m:(map.Map.map Z Z)), forall (p:addr),
((base p) < 0%Z)%Z -> (((0%Z <= (offset p))%Z /\
- ((offset p) < (map.Map.get m (base p)))%Z) -> ((valid_rd m p 1%Z) /\
+ ((offset p) < (m (base p)))%Z) -> ((valid_rd m p 1%Z) /\
~ (valid_rw m p 1%Z))).
Proof.
intros m p.
@@ -251,7 +251,7 @@ Admitted.
(* Why3 assumption *)
Definition framed (m:(map.Map.map addr addr)): Prop := forall (p:addr),
- ((region (base (map.Map.get m p))) <= 0%Z)%Z.
+ ((region (base (m p))) <= 0%Z)%Z.
(* Why3 goal *)
Lemma separated_included : forall (p:addr) (q:addr), forall (a:Z) (b:Z),
@@ -318,9 +318,9 @@ Admitted.
(* Why3 goal *)
Lemma havoc_access : forall {a:Type} {a_WT:WhyType a},
forall (m0:(map.Map.map addr a)) (m1:(map.Map.map addr a)), forall (q:addr)
- (p:addr), forall (a1:Z), ((separated q 1%Z p a1) -> ((map.Map.get (havoc m0
- m1 p a1) q) = (map.Map.get m1 q))) /\ ((~ (separated q 1%Z p a1)) ->
- ((map.Map.get (havoc m0 m1 p a1) q) = (map.Map.get m0 q))).
+ (p:addr), forall (a1:Z), ((separated q 1%Z p a1) -> (((havoc m0
+ m1 p a1) q) = (m1 q))) /\ ((~ (separated q 1%Z p a1)) ->
+ (((havoc m0 m1 p a1) q) = (m0 q))).
Proof.
intros a a_WT m0 m1 q p a1.
Admitted.
diff --git a/src/plugins/wp/share/coqwp/Qedlib.v b/src/plugins/wp/share/coqwp/Qedlib.v
index 4156a9e32907453de88b7494189f01dd8ce715ea..68c2a998c3dd04aefa90a44182940d74a305771c 100644
--- a/src/plugins/wp/share/coqwp/Qedlib.v
+++ b/src/plugins/wp/share/coqwp/Qedlib.v
@@ -211,8 +211,9 @@ Definition array (A : Type) := farray Z A.
Hypothesis extensionality: forall (A B : Type) (f g : A -> B),
(forall x, f x = g x) -> f = g.
+
Definition select {A B : Type}
- (m : farray A B) (k : A) : B := @Map.get A (whytype1 m) B (whytype2 m) m k.
+ (m : farray A B) (k : A) : B := (access m k).
Lemma farray_eq : forall A B (m1 m2 : farray A B),
whytype1 m1 = whytype1 m2 -> whytype2 m1 = whytype2 m2 ->
@@ -221,15 +222,14 @@ Proof.
intros A B m1 m2.
destruct m1. destruct m2. simpl.
intros H1 H2; rewrite H1; rewrite H2 ; clear H1 H2.
- destruct access0. destruct access1. compute.
intro K.
- rewrite (extensionality b b0 K).
+ rewrite (extensionality access0 access1 K).
reflexivity.
Qed.
Definition update {A B : Type}
(m : farray A B) (k : A) (v : B) : (farray A B) :=
- {| whytype1 := whytype1 m; whytype2 := whytype2 m; access := @Map.set A (whytype1 m) B (whytype2 m) m k v|}.
+ {| whytype1 := whytype1 m; whytype2 := whytype2 m; access := @Map.set A (whytype1 m) B (whytype2 m) (access m) k v|}.
Notation " a .[ k ] " := (select a k) (at level 60).
Notation " a .[ k <- v ] " := (update a k v) (at level 60).
@@ -239,7 +239,7 @@ Lemma access_update :
m.[k <- v].[k] = v.
Proof.
intros.
- apply Map.Select_eq.
+ apply Map.set_def.
reflexivity.
Qed.
@@ -248,8 +248,8 @@ Lemma access_update_neq :
i <> j -> m.[ i <- v ].[j] = m.[j].
Proof.
intros.
- apply Map.Select_neq.
- assumption.
+ apply Map.set_def.
+ auto.
Qed.
(** ** Division on Z *)
diff --git a/src/plugins/wp/share/coqwp/Vlist.v b/src/plugins/wp/share/coqwp/Vlist.v
index 182898718639ae466b39a16277bcd32445f8be76..dfcb15ea7fdc389ba1e81e3e9e448e06fb84d7fc 100644
--- a/src/plugins/wp/share/coqwp/Vlist.v
+++ b/src/plugins/wp/share/coqwp/Vlist.v
@@ -64,7 +64,7 @@ Defined.
Definition concat: forall {a:Type} {a_WT:WhyType a}, (list a) -> (list a) ->
(list a).
intros a a_WT.
- Open Local Scope list_scope.
+ Local Open Scope list_scope.
exact(fun u v => u ++ v).
Defined.
diff --git a/src/plugins/wp/share/coqwp/Zbits.v b/src/plugins/wp/share/coqwp/Zbits.v
index e168e835e820688d375580f4521ecd7911399972..0c02116df5e35bf4555528819a49b1a7a504b4fa 100644
--- a/src/plugins/wp/share/coqwp/Zbits.v
+++ b/src/plugins/wp/share/coqwp/Zbits.v
@@ -46,7 +46,7 @@ Require Import Qedlib.
Require Import Bits.
Require Import Psatz.
-Open Local Scope Z_scope.
+Local Open Scope Z_scope.
Local Ltac omegaContradiction := cut False; [contradiction|omega].
diff --git a/src/plugins/wp/share/coqwp/bool/Bool.v b/src/plugins/wp/share/coqwp/bool/Bool.v
index 64b159874c5c3aab7209d8c1d7486376ecf44f6f..9038682132e398aa54c4168348f364db9f7e1ac0 100644
--- a/src/plugins/wp/share/coqwp/bool/Bool.v
+++ b/src/plugins/wp/share/coqwp/bool/Bool.v
@@ -1,12 +1,13 @@
-(**************************************************************************)
-(* *)
-(* The Why3 Verification Platform / The Why3 Development Team *)
-(* Copyright 2010-2013 -- 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-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. *)
+(* *)
+(********************************************************************)
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
@@ -14,55 +15,61 @@ Require Import BuiltIn.
Require BuiltIn.
(* Why3 goal *)
-Lemma andb_def : forall (x:bool) (y:bool),
+Lemma andb_def :
+ forall (x:bool) (y:bool),
((Init.Datatypes.andb x y) = match x with
- | true => y
- | false => false
- end).
+ | true => y
+ | false => false
+ end).
Proof.
intros x y.
apply refl_equal.
Qed.
(* Why3 goal *)
-Lemma orb_def : forall (x:bool) (y:bool),
+Lemma orb_def :
+ forall (x:bool) (y:bool),
((Init.Datatypes.orb x y) = match x with
- | false => y
- | true => true
- end).
+ | false => y
+ | true => true
+ end).
Proof.
intros x y.
apply refl_equal.
Qed.
(* Why3 goal *)
-Lemma notb_def : forall (x:bool),
+Lemma notb_def :
+ forall (x:bool),
((Init.Datatypes.negb x) = match x with
- | false => true
- | true => false
- end).
+ | false => true
+ | true => false
+ end).
Proof.
intros x.
apply refl_equal.
Qed.
(* Why3 goal *)
-Lemma xorb_def : forall (x:bool) (y:bool),
- ((Init.Datatypes.xorb x y) = match x with
- | false => y
- | true => (Init.Datatypes.negb y)
- end).
+Lemma xorb_def :
+ forall (x:bool) (y:bool),
+ ((Init.Datatypes.xorb x y) =
+ match x with
+ | false => y
+ | true => (Init.Datatypes.negb y)
+ end).
Proof.
intros x y.
destruct x; destruct y; auto.
Qed.
(* Why3 goal *)
-Lemma implb_def : forall (x:bool) (y:bool),
+Lemma implb_def :
+ forall (x:bool) (y:bool),
((Init.Datatypes.implb x y) = match x with
- | false => true
- | true => y
- end).
+ | false => true
+ | true => y
+ end).
Proof.
now intros [|] [|].
Qed.
diff --git a/src/plugins/wp/share/coqwp/int/Abs.v b/src/plugins/wp/share/coqwp/int/Abs.v
index d5164fde98392e2999b827829832d659ef329f83..5637e82b7dacbce17a776dae26afeca3dc0c4333 100644
--- a/src/plugins/wp/share/coqwp/int/Abs.v
+++ b/src/plugins/wp/share/coqwp/int/Abs.v
@@ -1,12 +1,13 @@
-(**************************************************************************)
-(* *)
-(* The Why3 Verification Platform / The Why3 Development Team *)
-(* Copyright 2010-2013 -- 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-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. *)
+(* *)
+(********************************************************************)
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
@@ -18,9 +19,10 @@ Require int.Int.
(* abs is replaced with (ZArith.BinInt.Z.abs x) by the coq driver *)
(* Why3 goal *)
-Lemma abs_def : forall (x:Z), ((0%Z <= x)%Z ->
- ((ZArith.BinInt.Z.abs x) = x)) /\ ((~ (0%Z <= x)%Z) ->
- ((ZArith.BinInt.Z.abs x) = (-x)%Z)).
+Lemma abs_def :
+ forall (x:Z),
+ ((0%Z <= x)%Z -> ((ZArith.BinInt.Z.abs x) = x)) /\
+ (~ (0%Z <= x)%Z -> ((ZArith.BinInt.Z.abs x) = (-x)%Z)).
intros x.
split ; intros H.
now apply Zabs_eq.
@@ -32,8 +34,9 @@ now apply Zgt_lt.
Qed.
(* Why3 goal *)
-Lemma Abs_le : forall (x:Z) (y:Z), ((ZArith.BinInt.Z.abs x) <= y)%Z <->
- (((-y)%Z <= x)%Z /\ (x <= y)%Z).
+Lemma Abs_le :
+ forall (x:Z) (y:Z),
+ ((ZArith.BinInt.Z.abs x) <= y)%Z <-> (((-y)%Z <= x)%Z /\ (x <= y)%Z).
intros x y.
zify.
omega.
diff --git a/src/plugins/wp/share/coqwp/int/ComputerDivision.v b/src/plugins/wp/share/coqwp/int/ComputerDivision.v
index 043a92f2c905ab5ca6082c86234a8a21764af637..c34926e4c2fcdd44c6a8e2fb11e18be5241f24dd 100644
--- a/src/plugins/wp/share/coqwp/int/ComputerDivision.v
+++ b/src/plugins/wp/share/coqwp/int/ComputerDivision.v
@@ -1,12 +1,13 @@
-(**************************************************************************)
-(* *)
-(* The Why3 Verification Platform / The Why3 Development Team *)
-(* Copyright 2010-2013 -- 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-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. *)
+(* *)
+(********************************************************************)
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
@@ -24,16 +25,18 @@ Require Import Zquot.
(* mod1 is replaced with (ZArith.BinInt.Z.rem x x1) by the coq driver *)
(* Why3 goal *)
-Lemma Div_mod : forall (x:Z) (y:Z), (~ (y = 0%Z)) ->
+Lemma Div_mod :
+ forall (x:Z) (y:Z), ~ (y = 0%Z) ->
(x = ((y * (ZArith.BinInt.Z.quot x y))%Z + (ZArith.BinInt.Z.rem x y))%Z).
intros x y _.
apply Z.quot_rem'.
Qed.
(* Why3 goal *)
-Lemma Div_bound : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z < y)%Z) ->
- ((0%Z <= (ZArith.BinInt.Z.quot x y))%Z /\
- ((ZArith.BinInt.Z.quot x y) <= x)%Z).
+Lemma Div_bound :
+ forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z < y)%Z) ->
+ (0%Z <= (ZArith.BinInt.Z.quot x y))%Z /\
+ ((ZArith.BinInt.Z.quot x y) <= x)%Z.
intros x y (Hx,Hy).
split.
now apply Z.quot_pos.
@@ -48,9 +51,10 @@ now rewrite <- H', Zquot_0_l.
Qed.
(* Why3 goal *)
-Lemma Mod_bound : forall (x:Z) (y:Z), (~ (y = 0%Z)) ->
- (((-(ZArith.BinInt.Z.abs y))%Z < (ZArith.BinInt.Z.rem x y))%Z /\
- ((ZArith.BinInt.Z.rem x y) < (ZArith.BinInt.Z.abs y))%Z).
+Lemma Mod_bound :
+ forall (x:Z) (y:Z), ~ (y = 0%Z) ->
+ ((-(ZArith.BinInt.Z.abs y))%Z < (ZArith.BinInt.Z.rem x y))%Z /\
+ ((ZArith.BinInt.Z.rem x y) < (ZArith.BinInt.Z.abs y))%Z.
intros x y Zy.
destruct (Zle_or_lt 0 x) as [Hx|Hx].
refine ((fun H => conj (Zlt_le_trans _ 0 _ _ (proj1 H)) (proj2 H)) _).
@@ -63,14 +67,16 @@ now apply Zlt_le_weak.
Qed.
(* Why3 goal *)
-Lemma Div_sign_pos : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z < y)%Z) ->
+Lemma Div_sign_pos :
+ forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z < y)%Z) ->
(0%Z <= (ZArith.BinInt.Z.quot x y))%Z.
intros x y (Hx, Hy).
now apply Z.quot_pos.
Qed.
(* Why3 goal *)
-Lemma Div_sign_neg : forall (x:Z) (y:Z), ((x <= 0%Z)%Z /\ (0%Z < y)%Z) ->
+Lemma Div_sign_neg :
+ forall (x:Z) (y:Z), ((x <= 0%Z)%Z /\ (0%Z < y)%Z) ->
((ZArith.BinInt.Z.quot x y) <= 0%Z)%Z.
intros x y (Hx, Hy).
generalize (Z.quot_pos (-x) y).
@@ -79,22 +85,26 @@ omega.
Qed.
(* Why3 goal *)
-Lemma Mod_sign_pos : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ ~ (y = 0%Z)) ->
+Lemma Mod_sign_pos :
+ forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ ~ (y = 0%Z)) ->
(0%Z <= (ZArith.BinInt.Z.rem x y))%Z.
intros x y (Hx, Zy).
now apply Zrem_lt_pos.
Qed.
(* Why3 goal *)
-Lemma Mod_sign_neg : forall (x:Z) (y:Z), ((x <= 0%Z)%Z /\ ~ (y = 0%Z)) ->
+Lemma Mod_sign_neg :
+ forall (x:Z) (y:Z), ((x <= 0%Z)%Z /\ ~ (y = 0%Z)) ->
((ZArith.BinInt.Z.rem x y) <= 0%Z)%Z.
intros x y (Hx, Zy).
now apply Zrem_lt_neg.
Qed.
(* Why3 goal *)
-Lemma Rounds_toward_zero : forall (x:Z) (y:Z), (~ (y = 0%Z)) ->
- ((ZArith.BinInt.Z.abs ((ZArith.BinInt.Z.quot x y) * y)%Z) <= (ZArith.BinInt.Z.abs x))%Z.
+Lemma Rounds_toward_zero :
+ forall (x:Z) (y:Z), ~ (y = 0%Z) ->
+ ((ZArith.BinInt.Z.abs ((ZArith.BinInt.Z.quot x y) * y)%Z) <=
+ (ZArith.BinInt.Z.abs x))%Z.
intros x y Zy.
rewrite Zmult_comm.
zify.
@@ -114,21 +124,25 @@ exact Z.rem_1_r.
Qed.
(* Why3 goal *)
-Lemma Div_inf : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (x < y)%Z) ->
+Lemma Div_inf :
+ forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (x < y)%Z) ->
((ZArith.BinInt.Z.quot x y) = 0%Z).
exact Z.quot_small.
Qed.
(* Why3 goal *)
-Lemma Mod_inf : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (x < y)%Z) ->
+Lemma Mod_inf :
+ forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (x < y)%Z) ->
((ZArith.BinInt.Z.rem x y) = x).
exact Z.rem_small.
Qed.
(* Why3 goal *)
-Lemma Div_mult : forall (x:Z) (y:Z) (z:Z), ((0%Z < x)%Z /\ ((0%Z <= y)%Z /\
- (0%Z <= z)%Z)) ->
- ((ZArith.BinInt.Z.quot ((x * y)%Z + z)%Z x) = (y + (ZArith.BinInt.Z.quot z x))%Z).
+Lemma Div_mult :
+ forall (x:Z) (y:Z) (z:Z),
+ ((0%Z < x)%Z /\ ((0%Z <= y)%Z /\ (0%Z <= z)%Z)) ->
+ ((ZArith.BinInt.Z.quot ((x * y)%Z + z)%Z x) =
+ (y + (ZArith.BinInt.Z.quot z x))%Z).
intros x y z (Hx&Hy&Hz).
rewrite (Zplus_comm y).
rewrite <- Z_quot_plus.
@@ -142,8 +156,9 @@ now rewrite H in Hx.
Qed.
(* Why3 goal *)
-Lemma Mod_mult : forall (x:Z) (y:Z) (z:Z), ((0%Z < x)%Z /\ ((0%Z <= y)%Z /\
- (0%Z <= z)%Z)) ->
+Lemma Mod_mult :
+ forall (x:Z) (y:Z) (z:Z),
+ ((0%Z < x)%Z /\ ((0%Z <= y)%Z /\ (0%Z <= z)%Z)) ->
((ZArith.BinInt.Z.rem ((x * y)%Z + z)%Z x) = (ZArith.BinInt.Z.rem z x)).
intros x y z (Hx&Hy&Hz).
rewrite Zplus_comm, Zmult_comm.
diff --git a/src/plugins/wp/share/coqwp/int/Exponentiation.v b/src/plugins/wp/share/coqwp/int/Exponentiation.v
new file mode 100644
index 0000000000000000000000000000000000000000..f911f4cd6bda205689f287c4c3a9398140ba9c9e
--- /dev/null
+++ b/src/plugins/wp/share/coqwp/int/Exponentiation.v
@@ -0,0 +1,151 @@
+(********************************************************************)
+(* *)
+(* 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. *)
+(* *)
+(********************************************************************)
+
+(* This file is generated by Why3's Coq-realize driver *)
+(* Beware! Only edit allowed sections below *)
+Require Import BuiltIn.
+Require BuiltIn.
+Require int.Int.
+
+Section Exponentiation.
+
+(* Why3 goal *)
+Variable t : Type.
+Hypothesis t_WhyType : WhyType t.
+Existing Instance t_WhyType.
+
+(* Why3 goal *)
+Variable one: t.
+
+(* Why3 goal *)
+Variable infix_as: t -> t -> t.
+
+(* Why3 goal *)
+Hypothesis Assoc :
+ forall (x:t) (y:t) (z:t),
+ ((infix_as (infix_as x y) z) = (infix_as x (infix_as y z))).
+
+(* Why3 goal *)
+Hypothesis Unit_def_l : forall (x:t), ((infix_as one x) = x).
+
+(* Why3 goal *)
+Hypothesis Unit_def_r : forall (x:t), ((infix_as x one) = x).
+
+(* Why3 goal *)
+Definition power : t -> Z -> t.
+intros x n.
+exact (iter_nat (Zabs_nat n) t (fun acc => infix_as x acc) one).
+Defined.
+
+(* Why3 goal *)
+Lemma Power_0 : forall (x:t), ((power x 0%Z) = one).
+Proof.
+easy.
+Qed.
+
+(* Why3 goal *)
+Lemma Power_s :
+ forall (x:t) (n:Z), (0%Z <= n)%Z ->
+ ((power x (n + 1%Z)%Z) = (infix_as x (power x n))).
+Proof.
+intros x n h1.
+unfold power.
+fold (Zsucc n).
+now rewrite Zabs_nat_Zsucc.
+Qed.
+
+(* Why3 goal *)
+Lemma Power_s_alt :
+ forall (x:t) (n:Z), (0%Z < n)%Z ->
+ ((power x n) = (infix_as x (power x (n - 1%Z)%Z))).
+Proof.
+intros x n h1.
+rewrite <- Power_s; auto with zarith.
+f_equal; omega.
+Qed.
+
+(* Why3 goal *)
+Lemma Power_1 : forall (x:t), ((power x 1%Z) = x).
+Proof.
+exact Unit_def_r.
+Qed.
+
+(* Why3 goal *)
+Lemma Power_sum :
+ forall (x:t) (n:Z) (m:Z), (0%Z <= n)%Z -> (0%Z <= m)%Z ->
+ ((power x (n + m)%Z) = (infix_as (power x n) (power x m))).
+Proof.
+intros x n m Hn Hm.
+revert n Hn.
+apply natlike_ind.
+apply sym_eq, Unit_def_l.
+intros n Hn IHn.
+replace (Zsucc n + m)%Z with ((n + m) + 1)%Z by ring.
+rewrite Power_s by auto with zarith.
+rewrite IHn.
+now rewrite <- Assoc, <- Power_s.
+Qed.
+
+(* Why3 goal *)
+Lemma Power_mult :
+ forall (x:t) (n:Z) (m:Z), (0%Z <= n)%Z -> (0%Z <= m)%Z ->
+ ((power x (n * m)%Z) = (power (power x n) m)).
+Proof.
+intros x n m Hn Hm.
+revert m Hm.
+apply natlike_ind.
+now rewrite Zmult_0_r, 2!Power_0.
+intros m Hm IHm.
+replace (n * Zsucc m)%Z with (n + n * m)%Z by ring.
+rewrite Power_sum by auto with zarith.
+rewrite IHm.
+now rewrite <- Power_s.
+Qed.
+
+(* Why3 goal *)
+Lemma Power_comm1 :
+ forall (x:t) (y:t), ((infix_as x y) = (infix_as y x)) -> forall (n:Z),
+ (0%Z <= n)%Z -> ((infix_as (power x n) y) = (infix_as y (power x n))).
+Proof.
+intros x y comm.
+apply natlike_ind.
+now rewrite Power_0, Unit_def_r, Unit_def_l.
+intros n Hn IHn.
+unfold Zsucc.
+rewrite (Power_s _ _ Hn).
+rewrite Assoc.
+rewrite IHn.
+rewrite <- Assoc.
+rewrite <- Assoc.
+now rewrite comm.
+Qed.
+
+(* Why3 goal *)
+Lemma Power_comm2 :
+ forall (x:t) (y:t), ((infix_as x y) = (infix_as y x)) -> forall (n:Z),
+ (0%Z <= n)%Z ->
+ ((power (infix_as x y) n) = (infix_as (power x n) (power y n))).
+Proof.
+intros x y comm.
+apply natlike_ind.
+rewrite 3!Power_0.
+now rewrite Unit_def_r.
+intros n Hn IHn.
+unfold Zsucc.
+rewrite 3!(Power_s _ _ Hn).
+rewrite IHn.
+rewrite <- Assoc.
+rewrite (Assoc x).
+rewrite <- (Power_comm1 _ _ comm _ Hn).
+now rewrite <- 2!Assoc.
+Qed.
+
+End Exponentiation.
diff --git a/src/plugins/wp/share/coqwp/int/Int.v b/src/plugins/wp/share/coqwp/int/Int.v
index f262ae6374551b3f689ea90a8bd891990f0a286c..a5106073930d4a7cafe8d7f84883d0756b28c832 100644
--- a/src/plugins/wp/share/coqwp/int/Int.v
+++ b/src/plugins/wp/share/coqwp/int/Int.v
@@ -1,12 +1,13 @@
-(**************************************************************************)
-(* *)
-(* The Why3 Verification Platform / The Why3 Development Team *)
-(* Copyright 2010-2013 -- 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-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. *)
+(* *)
+(********************************************************************)
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
@@ -14,26 +15,31 @@ Require Import BuiltIn.
Require BuiltIn.
(* Why3 comment *)
-(* infix_ls is replaced with (x < x1)%Z by the coq driver *)
-
-(* Why3 goal *)
-Lemma infix_lseq_def : forall (x:Z) (y:Z), (x <= y)%Z <-> ((x < y)%Z \/
- (x = y)).
-exact Zle_lt_or_eq_iff.
-Qed.
+(* prefix_mn is replaced with (-x)%Z by the coq driver *)
(* Why3 comment *)
(* infix_pl is replaced with (x + x1)%Z by the coq driver *)
(* Why3 comment *)
-(* prefix_mn is replaced with (-x)%Z by the coq driver *)
+(* infix_as is replaced with (x * x1)%Z by the coq driver *)
(* Why3 comment *)
-(* infix_as is replaced with (x * x1)%Z by the coq driver *)
+(* infix_ls is replaced with (x < x1)%Z by the coq driver *)
+
+(* Why3 goal *)
+Lemma infix_mn_def : forall (x:Z) (y:Z), ((x - y)%Z = (x + (-y)%Z)%Z).
+reflexivity.
+Qed.
+
+(* Why3 goal *)
+Lemma infix_lseq_def :
+ forall (x:Z) (y:Z), (x <= y)%Z <-> ((x < y)%Z \/ (x = y)).
+exact Zle_lt_or_eq_iff.
+Qed.
(* Why3 goal *)
-Lemma Assoc : forall (x:Z) (y:Z) (z:Z),
- (((x + y)%Z + z)%Z = (x + (y + z)%Z)%Z).
+Lemma Assoc :
+ forall (x:Z) (y:Z) (z:Z), (((x + y)%Z + z)%Z = (x + (y + z)%Z)%Z).
Proof.
intros x y z.
apply sym_eq.
@@ -71,8 +77,8 @@ exact Zplus_comm.
Qed.
(* Why3 goal *)
-Lemma Assoc1 : forall (x:Z) (y:Z) (z:Z),
- (((x * y)%Z * z)%Z = (x * (y * z)%Z)%Z).
+Lemma Assoc1 :
+ forall (x:Z) (y:Z) (z:Z), (((x * y)%Z * z)%Z = (x * (y * z)%Z)%Z).
Proof.
intros x y z.
apply sym_eq.
@@ -80,26 +86,21 @@ apply Zmult_assoc.
Qed.
(* Why3 goal *)
-Lemma Mul_distr_l : forall (x:Z) (y:Z) (z:Z),
- ((x * (y + z)%Z)%Z = ((x * y)%Z + (x * z)%Z)%Z).
+Lemma Mul_distr_l :
+ forall (x:Z) (y:Z) (z:Z), ((x * (y + z)%Z)%Z = ((x * y)%Z + (x * z)%Z)%Z).
Proof.
intros x y z.
apply Zmult_plus_distr_r.
Qed.
(* Why3 goal *)
-Lemma Mul_distr_r : forall (x:Z) (y:Z) (z:Z),
- (((y + z)%Z * x)%Z = ((y * x)%Z + (z * x)%Z)%Z).
+Lemma Mul_distr_r :
+ forall (x:Z) (y:Z) (z:Z), (((y + z)%Z * x)%Z = ((y * x)%Z + (z * x)%Z)%Z).
Proof.
intros x y z.
apply Zmult_plus_distr_l.
Qed.
-(* Why3 goal *)
-Lemma infix_mn_def : forall (x:Z) (y:Z), ((x - y)%Z = (x + (-y)%Z)%Z).
-reflexivity.
-Qed.
-
(* Why3 goal *)
Lemma Comm1 : forall (x:Z) (y:Z), ((x * y)%Z = (y * x)%Z).
Proof.
@@ -126,14 +127,14 @@ apply Zle_refl.
Qed.
(* Why3 goal *)
-Lemma Trans : forall (x:Z) (y:Z) (z:Z), (x <= y)%Z -> ((y <= z)%Z ->
- (x <= z)%Z).
+Lemma Trans :
+ forall (x:Z) (y:Z) (z:Z), (x <= y)%Z -> (y <= z)%Z -> (x <= z)%Z.
Proof.
exact Zle_trans.
Qed.
(* Why3 goal *)
-Lemma Antisymm : forall (x:Z) (y:Z), (x <= y)%Z -> ((y <= x)%Z -> (x = y)).
+Lemma Antisymm : forall (x:Z) (y:Z), (x <= y)%Z -> (y <= x)%Z -> (x = y).
Proof.
exact Zle_antisym.
Qed.
@@ -157,15 +158,16 @@ now left.
Qed.
(* Why3 goal *)
-Lemma CompatOrderAdd : forall (x:Z) (y:Z) (z:Z), (x <= y)%Z ->
- ((x + z)%Z <= (y + z)%Z)%Z.
+Lemma CompatOrderAdd :
+ forall (x:Z) (y:Z) (z:Z), (x <= y)%Z -> ((x + z)%Z <= (y + z)%Z)%Z.
Proof.
exact Zplus_le_compat_r.
Qed.
(* Why3 goal *)
-Lemma CompatOrderMult : forall (x:Z) (y:Z) (z:Z), (x <= y)%Z ->
- ((0%Z <= z)%Z -> ((x * z)%Z <= (y * z)%Z)%Z).
+Lemma CompatOrderMult :
+ forall (x:Z) (y:Z) (z:Z), (x <= y)%Z -> (0%Z <= z)%Z ->
+ ((x * z)%Z <= (y * z)%Z)%Z.
Proof.
exact Zmult_le_compat_r.
Qed.
diff --git a/src/plugins/wp/share/coqwp/int/MinMax.v b/src/plugins/wp/share/coqwp/int/MinMax.v
index 793c7139aef46781d70ebdcdd12ff4f42a180ce4..d969091e7810e422f58e80b10c076bc2d5f09704 100644
--- a/src/plugins/wp/share/coqwp/int/MinMax.v
+++ b/src/plugins/wp/share/coqwp/int/MinMax.v
@@ -1,12 +1,13 @@
-(**************************************************************************)
-(* *)
-(* The Why3 Verification Platform / The Why3 Development Team *)
-(* Copyright 2010-2013 -- 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-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. *)
+(* *)
+(********************************************************************)
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
@@ -18,9 +19,10 @@ Require int.Int.
(* min is replaced with (ZArith.BinInt.Z.min x x1) by the coq driver *)
(* Why3 goal *)
-Lemma min_def : forall (x:Z) (y:Z), ((x <= y)%Z ->
- ((ZArith.BinInt.Z.min x y) = x)) /\ ((~ (x <= y)%Z) ->
- ((ZArith.BinInt.Z.min x y) = y)).
+Lemma min_def :
+ forall (x:Z) (y:Z),
+ ((x <= y)%Z -> ((ZArith.BinInt.Z.min x y) = x)) /\
+ (~ (x <= y)%Z -> ((ZArith.BinInt.Z.min x y) = y)).
Proof.
intros x y.
split ; intros H.
@@ -33,9 +35,10 @@ Qed.
(* max is replaced with (ZArith.BinInt.Z.max x x1) by the coq driver *)
(* Why3 goal *)
-Lemma max_def : forall (x:Z) (y:Z), ((x <= y)%Z ->
- ((ZArith.BinInt.Z.max x y) = y)) /\ ((~ (x <= y)%Z) ->
- ((ZArith.BinInt.Z.max x y) = x)).
+Lemma max_def :
+ forall (x:Z) (y:Z),
+ ((x <= y)%Z -> ((ZArith.BinInt.Z.max x y) = y)) /\
+ (~ (x <= y)%Z -> ((ZArith.BinInt.Z.max x y) = x)).
Proof.
intros x y.
split ; intros H.
@@ -45,40 +48,44 @@ omega.
Qed.
(* Why3 goal *)
-Lemma Min_r : forall (x:Z) (y:Z), (y <= x)%Z ->
- ((ZArith.BinInt.Z.min x y) = y).
+Lemma Min_r :
+ forall (x:Z) (y:Z), (y <= x)%Z -> ((ZArith.BinInt.Z.min x y) = y).
exact Zmin_r.
Qed.
(* Why3 goal *)
-Lemma Max_l : forall (x:Z) (y:Z), (y <= x)%Z ->
- ((ZArith.BinInt.Z.max x y) = x).
+Lemma Max_l :
+ forall (x:Z) (y:Z), (y <= x)%Z -> ((ZArith.BinInt.Z.max x y) = x).
exact Zmax_l.
Qed.
(* Why3 goal *)
-Lemma Min_comm : forall (x:Z) (y:Z),
- ((ZArith.BinInt.Z.min x y) = (ZArith.BinInt.Z.min y x)).
+Lemma Min_comm :
+ forall (x:Z) (y:Z), ((ZArith.BinInt.Z.min x y) = (ZArith.BinInt.Z.min y x)).
exact Zmin_comm.
Qed.
(* Why3 goal *)
-Lemma Max_comm : forall (x:Z) (y:Z),
- ((ZArith.BinInt.Z.max x y) = (ZArith.BinInt.Z.max y x)).
+Lemma Max_comm :
+ forall (x:Z) (y:Z), ((ZArith.BinInt.Z.max x y) = (ZArith.BinInt.Z.max y x)).
exact Zmax_comm.
Qed.
(* Why3 goal *)
-Lemma Min_assoc : forall (x:Z) (y:Z) (z:Z),
- ((ZArith.BinInt.Z.min (ZArith.BinInt.Z.min x y) z) = (ZArith.BinInt.Z.min x (ZArith.BinInt.Z.min y z))).
+Lemma Min_assoc :
+ forall (x:Z) (y:Z) (z:Z),
+ ((ZArith.BinInt.Z.min (ZArith.BinInt.Z.min x y) z) =
+ (ZArith.BinInt.Z.min x (ZArith.BinInt.Z.min y z))).
Proof.
intros x y z.
apply eq_sym, Zmin_assoc.
Qed.
(* Why3 goal *)
-Lemma Max_assoc : forall (x:Z) (y:Z) (z:Z),
- ((ZArith.BinInt.Z.max (ZArith.BinInt.Z.max x y) z) = (ZArith.BinInt.Z.max x (ZArith.BinInt.Z.max y z))).
+Lemma Max_assoc :
+ forall (x:Z) (y:Z) (z:Z),
+ ((ZArith.BinInt.Z.max (ZArith.BinInt.Z.max x y) z) =
+ (ZArith.BinInt.Z.max x (ZArith.BinInt.Z.max y z))).
Proof.
intros x y z.
apply eq_sym, Zmax_assoc.
diff --git a/src/plugins/wp/share/coqwp/int/Power.v b/src/plugins/wp/share/coqwp/int/Power.v
new file mode 100644
index 0000000000000000000000000000000000000000..e2bed67ea5dd8ad31ec00b8246b77e12cffe93e1
--- /dev/null
+++ b/src/plugins/wp/share/coqwp/int/Power.v
@@ -0,0 +1,132 @@
+(********************************************************************)
+(* *)
+(* 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. *)
+(* *)
+(********************************************************************)
+
+(* This file is generated by Why3's Coq-realize driver *)
+(* Beware! Only edit allowed sections below *)
+Require Import BuiltIn.
+Require BuiltIn.
+Require int.Int.
+
+Require Import Exponentiation.
+
+(* Why3 goal *)
+Notation power := Zpower.
+
+Lemma power_is_exponentiation :
+ forall x n, (0 <= n)%Z -> power x n = Exponentiation.power _ 1%Z Zmult x n.
+Proof.
+intros x [|n|n] H.
+easy.
+2: now elim H.
+unfold Exponentiation.power, power, Zpower_pos.
+now rewrite iter_nat_of_P.
+Qed.
+
+(* Why3 goal *)
+Lemma Power_0 : forall (x:Z), ((power x 0%Z) = 1%Z).
+Proof.
+intros x.
+apply refl_equal.
+Qed.
+
+(* Why3 goal *)
+Lemma Power_s :
+ forall (x:Z) (n:Z), (0%Z <= n)%Z ->
+ ((power x (n + 1%Z)%Z) = (x * (power x n))%Z).
+Proof.
+intros x n h1.
+rewrite Zpower_exp.
+change (power x 1) with (x * 1)%Z.
+ring.
+now apply Zle_ge.
+easy.
+Qed.
+
+(* Why3 goal *)
+Lemma Power_s_alt :
+ forall (x:Z) (n:Z), (0%Z < n)%Z ->
+ ((power x n) = (x * (power x (n - 1%Z)%Z))%Z).
+intros x n h1.
+rewrite <- Power_s.
+f_equal; auto with zarith.
+omega.
+Qed.
+
+(* Why3 goal *)
+Lemma Power_1 : forall (x:Z), ((power x 1%Z) = x).
+Proof.
+exact Zmult_1_r.
+Qed.
+
+(* Why3 goal *)
+Lemma Power_sum :
+ forall (x:Z) (n:Z) (m:Z), (0%Z <= n)%Z -> (0%Z <= m)%Z ->
+ ((power x (n + m)%Z) = ((power x n) * (power x m))%Z).
+Proof.
+intros x n m Hn Hm.
+now apply Zpower_exp; apply Zle_ge.
+Qed.
+
+(* Why3 goal *)
+Lemma Power_mult :
+ forall (x:Z) (n:Z) (m:Z), (0%Z <= n)%Z -> (0%Z <= m)%Z ->
+ ((power x (n * m)%Z) = (power (power x n) m)).
+Proof.
+intros x n m Hn Hm.
+rewrite 3!power_is_exponentiation ; auto with zarith.
+apply Power_mult ; auto with zarith.
+Qed.
+
+(* Why3 goal *)
+Lemma Power_comm1 :
+ forall (x:Z) (y:Z), ((x * y)%Z = (y * x)%Z) -> forall (n:Z),
+ (0%Z <= n)%Z -> (((power x n) * y)%Z = (y * (power x n))%Z).
+Proof.
+intros x y h1 n h2.
+auto with zarith.
+Qed.
+
+(* Why3 goal *)
+Lemma Power_comm2 :
+ forall (x:Z) (y:Z), ((x * y)%Z = (y * x)%Z) -> forall (n:Z),
+ (0%Z <= n)%Z -> ((power (x * y)%Z n) = ((power x n) * (power y n))%Z).
+Proof.
+intros x y h1 n h2.
+rewrite 3!power_is_exponentiation ; auto with zarith.
+apply Power_comm2 ; auto with zarith.
+Qed.
+
+(* Why3 goal *)
+Lemma Power_non_neg :
+ forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z <= y)%Z) ->
+ (0%Z <= (power x y))%Z.
+intros x y (h1,h2).
+now apply Z.pow_nonneg.
+Qed.
+
+(* Why3 goal *)
+Lemma Power_pos :
+ forall (x:Z) (y:Z), ((0%Z < x)%Z /\ (0%Z <= y)%Z) -> (0%Z < (power x y))%Z.
+Proof.
+intros x y (h1,h2).
+eapply Z.pow_pos_nonneg; eauto.
+Qed.
+
+Open Scope Z_scope.
+
+(* Why3 goal *)
+Lemma Power_monotonic :
+ forall (x:Z) (n:Z) (m:Z), ((0%Z < x)%Z /\ ((0%Z <= n)%Z /\ (n <= m)%Z)) ->
+ ((power x n) <= (power x m))%Z.
+intros.
+apply Z.pow_le_mono_r; auto with zarith.
+Qed.
+
diff --git a/src/plugins/wp/share/coqwp/map/Const.v b/src/plugins/wp/share/coqwp/map/Const.v
index fbe804309c1a135ed67bffd990ed82be791b77d6..c2ebf2444c87bc8a7a8f6c5d337b1b734b94bfd5 100644
--- a/src/plugins/wp/share/coqwp/map/Const.v
+++ b/src/plugins/wp/share/coqwp/map/Const.v
@@ -1,33 +1,23 @@
-(**************************************************************************)
-(* *)
-(* The Why3 Verification Platform / The Why3 Development Team *)
-(* Copyright 2010-2013 -- 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-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. *)
+(* *)
+(********************************************************************)
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
+Require HighOrd.
Require map.Map.
-(* Why3 goal *)
-Definition const: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
- b -> (map.Map.map a b).
-intros a a_WT b b_WT v.
-constructor; intros i.
-exact v.
-Defined.
-
-(* Why3 goal *)
-Lemma Const : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
- forall (b1:b) (a1:a), ((map.Map.get (const b1: (map.Map.map a b))
- a1) = b1).
-intros a a_WT b b_WT b1 a1.
-unfold const.
-auto.
-Qed.
+(* Why3 assumption *)
+Definition const {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}
+ (v:b) : a -> b :=
+ fun (us:a) => v.
diff --git a/src/plugins/wp/share/coqwp/map/Map.v b/src/plugins/wp/share/coqwp/map/Map.v
index 8275368d51c7bbb89907a9639d2396349202ed94..1cb87d0a041491c37ebdebdbfe6eb8f18cd6fc80 100644
--- a/src/plugins/wp/share/coqwp/map/Map.v
+++ b/src/plugins/wp/share/coqwp/map/Map.v
@@ -1,28 +1,24 @@
-(**************************************************************************)
-(* *)
-(* The Why3 Verification Platform / The Why3 Development Team *)
-(* Copyright 2010-2013 -- 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-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. *)
+(* *)
+(********************************************************************)
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
+Require HighOrd.
Require Import ClassicalEpsilon.
-Inductive _map (a b:Type) :=
- | _map_constr : (a -> b) -> _map a b.
-
-(* Why3 goal *)
-Definition map : forall (a:Type) (b:Type), Type.
-intros.
-exact (_map a b).
-Defined.
+(* Why3 assumption *)
+Definition map (a:Type) (b:Type) := a -> b.
Global Instance map_WhyType : forall (a:Type) {a_WT:WhyType a} (b:Type) {b_WT:WhyType b}, WhyType (map a b).
Proof.
@@ -34,17 +30,10 @@ apply excluded_middle_informative.
Qed.
(* Why3 goal *)
-Definition get: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
- (map a b) -> a -> b.
-intros a a_WT b b_WT (m) x.
-exact (m x).
-Defined.
-
-(* Why3 goal *)
-Definition set: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
- (map a b) -> a -> b -> (map a b).
-intros a a_WT b b_WT (m) x y.
-split.
+Definition set {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b} :
+ (a -> b) -> a -> b -> a -> b.
+Proof.
+intros m x y.
intros x'.
destruct (why_decidable_eq x x') as [H|H].
exact y.
@@ -52,32 +41,19 @@ exact (m x').
Defined.
(* Why3 goal *)
-Lemma Select_eq : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
- forall (m:(map a b)), forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) ->
- ((get (set m a1 b1) a2) = b1).
-Proof.
-intros a a_WT b b_WT (m) a1 a2 b1 h1.
-unfold get, set.
-now case why_decidable_eq.
-Qed.
-
-(* Why3 goal *)
-Lemma Select_neq : forall {a:Type} {a_WT:WhyType a}
- {b:Type} {b_WT:WhyType b}, forall (m:(map a b)), forall (a1:a) (a2:a),
- forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1) a2) = (get m a2)).
-Proof.
-intros a a_WT b b_WT (m) a1 a2 b1 h1.
-unfold get, set.
-now case why_decidable_eq.
-Qed.
-
-(* Unused content named const
-intros a a_WT b b_WT y.
-exact (_map_constr _ _ (fun _ => y)).
-Defined.
- *)
-(* Unused content named Const
+Lemma set_def {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b} :
+ forall (f:a -> b) (x:a) (v:b) (y:a),
+ ((y = x) -> (((set f x v) y) = v)) /\
+ (~ (y = x) -> (((set f x v) y) = (f y))).
Proof.
+intros f x v y.
+unfold set.
+case why_decidable_eq.
+intros <-.
+split ; try easy ; intros H ; now elim H. (* TODO: replace by easy after 8.4 *)
+intros H.
+split ; intros H'.
+now elim H.
easy.
Qed.
- *)
+
diff --git a/src/plugins/wp/share/coqwp/real/Abs.v b/src/plugins/wp/share/coqwp/real/Abs.v
index 8ac538e8bff23bd11e707a81e28bfcf1f6665f40..5c1bcd5b23db2c13c4d14a1543ed94a10052c27c 100644
--- a/src/plugins/wp/share/coqwp/real/Abs.v
+++ b/src/plugins/wp/share/coqwp/real/Abs.v
@@ -1,12 +1,13 @@
-(**************************************************************************)
-(* *)
-(* The Why3 Verification Platform / The Why3 Development Team *)
-(* Copyright 2010-2013 -- 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-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. *)
+(* *)
+(********************************************************************)
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
@@ -21,9 +22,10 @@ Import Rbasic_fun.
(* abs is replaced with (Reals.Rbasic_fun.Rabs x) by the coq driver *)
(* Why3 goal *)
-Lemma abs_def : forall (x:R), ((0%R <= x)%R ->
- ((Reals.Rbasic_fun.Rabs x) = x)) /\ ((~ (0%R <= x)%R) ->
- ((Reals.Rbasic_fun.Rabs x) = (-x)%R)).
+Lemma abs_def :
+ forall (x:R),
+ ((0%R <= x)%R -> ((Reals.Rbasic_fun.Rabs x) = x)) /\
+ (~ (0%R <= x)%R -> ((Reals.Rbasic_fun.Rabs x) = (-x)%R)).
split ; intros H.
apply Rabs_right.
now apply Rle_ge.
@@ -32,8 +34,9 @@ now apply Rnot_le_lt.
Qed.
(* Why3 goal *)
-Lemma Abs_le : forall (x:R) (y:R), ((Reals.Rbasic_fun.Rabs x) <= y)%R <->
- (((-y)%R <= x)%R /\ (x <= y)%R).
+Lemma Abs_le :
+ forall (x:R) (y:R),
+ ((Reals.Rbasic_fun.Rabs x) <= y)%R <-> (((-y)%R <= x)%R /\ (x <= y)%R).
intros x y.
unfold Rabs.
case Rcase_abs ; intros H ; (split ; [intros H0;split | intros (H0,H1)]).
@@ -63,20 +66,26 @@ exact Rabs_pos.
Qed.
(* Why3 goal *)
-Lemma Abs_sum : forall (x:R) (y:R),
- ((Reals.Rbasic_fun.Rabs (x + y)%R) <= ((Reals.Rbasic_fun.Rabs x) + (Reals.Rbasic_fun.Rabs y))%R)%R.
+Lemma Abs_sum :
+ forall (x:R) (y:R),
+ ((Reals.Rbasic_fun.Rabs (x + y)%R) <=
+ ((Reals.Rbasic_fun.Rabs x) + (Reals.Rbasic_fun.Rabs y))%R)%R.
exact Rabs_triang.
Qed.
(* Why3 goal *)
-Lemma Abs_prod : forall (x:R) (y:R),
- ((Reals.Rbasic_fun.Rabs (x * y)%R) = ((Reals.Rbasic_fun.Rabs x) * (Reals.Rbasic_fun.Rabs y))%R).
+Lemma Abs_prod :
+ forall (x:R) (y:R),
+ ((Reals.Rbasic_fun.Rabs (x * y)%R) =
+ ((Reals.Rbasic_fun.Rabs x) * (Reals.Rbasic_fun.Rabs y))%R).
exact Rabs_mult.
Qed.
(* Why3 goal *)
-Lemma triangular_inequality : forall (x:R) (y:R) (z:R),
- ((Reals.Rbasic_fun.Rabs (x - z)%R) <= ((Reals.Rbasic_fun.Rabs (x - y)%R) + (Reals.Rbasic_fun.Rabs (y - z)%R))%R)%R.
+Lemma triangular_inequality :
+ forall (x:R) (y:R) (z:R),
+ ((Reals.Rbasic_fun.Rabs (x - z)%R) <=
+ ((Reals.Rbasic_fun.Rabs (x - y)%R) + (Reals.Rbasic_fun.Rabs (y - z)%R))%R)%R.
intros x y z.
replace (x - z)%R with ((x - y) + (y - z))%R by ring.
apply Rabs_triang.
diff --git a/src/plugins/wp/share/coqwp/real/ExpLog.v b/src/plugins/wp/share/coqwp/real/ExpLog.v
index 9211ebc212c065ced6c02d3af603408c94095d86..b0f17454da3d2b1f126611525f6944dcafff82bb 100644
--- a/src/plugins/wp/share/coqwp/real/ExpLog.v
+++ b/src/plugins/wp/share/coqwp/real/ExpLog.v
@@ -1,12 +1,13 @@
-(**************************************************************************)
-(* *)
-(* The Why3 Verification Platform / The Why3 Development Team *)
-(* Copyright 2010-2013 -- 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-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. *)
+(* *)
+(********************************************************************)
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
@@ -30,8 +31,10 @@ Qed.
Require Import Exp_prop.
(* Why3 goal *)
-Lemma Exp_sum : forall (x:R) (y:R),
- ((Reals.Rtrigo_def.exp (x + y)%R) = ((Reals.Rtrigo_def.exp x) * (Reals.Rtrigo_def.exp y))%R).
+Lemma Exp_sum :
+ forall (x:R) (y:R),
+ ((Reals.Rtrigo_def.exp (x + y)%R) =
+ ((Reals.Rtrigo_def.exp x) * (Reals.Rtrigo_def.exp y))%R).
exact exp_plus.
Qed.
@@ -44,28 +47,31 @@ exact ln_1.
Qed.
(* Why3 goal *)
-Lemma Log_mul : forall (x:R) (y:R), ((0%R < x)%R /\ (0%R < y)%R) ->
- ((Reals.Rpower.ln (x * y)%R) = ((Reals.Rpower.ln x) + (Reals.Rpower.ln y))%R).
+Lemma Log_mul :
+ forall (x:R) (y:R), ((0%R < x)%R /\ (0%R < y)%R) ->
+ ((Reals.Rpower.ln (x * y)%R) =
+ ((Reals.Rpower.ln x) + (Reals.Rpower.ln y))%R).
intros x y (Hx,Hy).
now apply ln_mult.
Qed.
(* Why3 goal *)
-Lemma Log_exp : forall (x:R),
- ((Reals.Rpower.ln (Reals.Rtrigo_def.exp x)) = x).
+Lemma Log_exp :
+ forall (x:R), ((Reals.Rpower.ln (Reals.Rtrigo_def.exp x)) = x).
exact ln_exp.
Qed.
(* Why3 goal *)
-Lemma Exp_log : forall (x:R), (0%R < x)%R ->
+Lemma Exp_log :
+ forall (x:R), (0%R < x)%R ->
((Reals.Rtrigo_def.exp (Reals.Rpower.ln x)) = x).
exact exp_ln.
Qed.
(* Why3 assumption *)
-Definition log2 (x:R): R := ((Reals.Rpower.ln x) / (Reals.Rpower.ln 2%R))%R.
+Definition log2 (x:R) : R := ((Reals.Rpower.ln x) / (Reals.Rpower.ln 2%R))%R.
(* Why3 assumption *)
-Definition log10 (x:R): R :=
+Definition log10 (x:R) : R :=
((Reals.Rpower.ln x) / (Reals.Rpower.ln 10%R))%R.
diff --git a/src/plugins/wp/share/coqwp/real/FromInt.v b/src/plugins/wp/share/coqwp/real/FromInt.v
index c10466940d61635bc09710fb3bf3ad11f1e3e5f0..fa6f14fc3853322f7b041c4000e060f29c0ffb92 100644
--- a/src/plugins/wp/share/coqwp/real/FromInt.v
+++ b/src/plugins/wp/share/coqwp/real/FromInt.v
@@ -1,12 +1,13 @@
-(**************************************************************************)
-(* *)
-(* The Why3 Verification Platform / The Why3 Development Team *)
-(* Copyright 2010-2013 -- 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-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. *)
+(* *)
+(********************************************************************)
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
@@ -31,21 +32,24 @@ split.
Qed.
(* Why3 goal *)
-Lemma Add : forall (x:Z) (y:Z),
+Lemma Add :
+ forall (x:Z) (y:Z),
((BuiltIn.IZR (x + y)%Z) = ((BuiltIn.IZR x) + (BuiltIn.IZR y))%R).
Proof.
exact plus_IZR.
Qed.
(* Why3 goal *)
-Lemma Sub : forall (x:Z) (y:Z),
+Lemma Sub :
+ forall (x:Z) (y:Z),
((BuiltIn.IZR (x - y)%Z) = ((BuiltIn.IZR x) - (BuiltIn.IZR y))%R).
Proof.
exact minus_IZR.
Qed.
(* Why3 goal *)
-Lemma Mul : forall (x:Z) (y:Z),
+Lemma Mul :
+ forall (x:Z) (y:Z),
((BuiltIn.IZR (x * y)%Z) = ((BuiltIn.IZR x) * (BuiltIn.IZR y))%R).
Proof.
exact mult_IZR.
@@ -58,8 +62,15 @@ exact opp_IZR.
Qed.
(* Why3 goal *)
-Lemma Monotonic : forall (x:Z) (y:Z), (x <= y)%Z ->
- ((BuiltIn.IZR x) <= (BuiltIn.IZR y))%R.
+Lemma Injective :
+ forall (x:Z) (y:Z), ((BuiltIn.IZR x) = (BuiltIn.IZR y)) -> (x = y).
+Proof.
+exact eq_IZR.
+Qed.
+
+(* Why3 goal *)
+Lemma Monotonic :
+ forall (x:Z) (y:Z), (x <= y)%Z -> ((BuiltIn.IZR x) <= (BuiltIn.IZR y))%R.
Proof.
exact (IZR_le).
Qed.
diff --git a/src/plugins/wp/share/coqwp/real/MinMax.v b/src/plugins/wp/share/coqwp/real/MinMax.v
index 4eee104e72b9966a4d26c4929d59fbea12ae3586..3f6ade0b9ac3f6e71d3ac798c720e26860ecd962 100644
--- a/src/plugins/wp/share/coqwp/real/MinMax.v
+++ b/src/plugins/wp/share/coqwp/real/MinMax.v
@@ -1,12 +1,13 @@
-(**************************************************************************)
-(* *)
-(* The Why3 Verification Platform / The Why3 Development Team *)
-(* Copyright 2010-2013 -- 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-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. *)
+(* *)
+(********************************************************************)
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
@@ -20,9 +21,10 @@ Require Import Rbasic_fun.
(* min is replaced with (Reals.Rbasic_fun.Rmin x x1) by the coq driver *)
(* Why3 goal *)
-Lemma min_def : forall (x:R) (y:R), ((x <= y)%R ->
- ((Reals.Rbasic_fun.Rmin x y) = x)) /\ ((~ (x <= y)%R) ->
- ((Reals.Rbasic_fun.Rmin x y) = y)).
+Lemma min_def :
+ forall (x:R) (y:R),
+ ((x <= y)%R -> ((Reals.Rbasic_fun.Rmin x y) = x)) /\
+ (~ (x <= y)%R -> ((Reals.Rbasic_fun.Rmin x y) = y)).
Proof.
intros x y.
split ; intros H.
@@ -35,9 +37,10 @@ Qed.
(* max is replaced with (Reals.Rbasic_fun.Rmax x x1) by the coq driver *)
(* Why3 goal *)
-Lemma max_def : forall (x:R) (y:R), ((x <= y)%R ->
- ((Reals.Rbasic_fun.Rmax x y) = y)) /\ ((~ (x <= y)%R) ->
- ((Reals.Rbasic_fun.Rmax x y) = x)).
+Lemma max_def :
+ forall (x:R) (y:R),
+ ((x <= y)%R -> ((Reals.Rbasic_fun.Rmax x y) = y)) /\
+ (~ (x <= y)%R -> ((Reals.Rbasic_fun.Rmax x y) = x)).
Proof.
intros x y.
split ; intros H.
@@ -47,32 +50,36 @@ now apply Rlt_le, Rnot_le_lt.
Qed.
(* Why3 goal *)
-Lemma Min_r : forall (x:R) (y:R), (y <= x)%R ->
- ((Reals.Rbasic_fun.Rmin x y) = y).
+Lemma Min_r :
+ forall (x:R) (y:R), (y <= x)%R -> ((Reals.Rbasic_fun.Rmin x y) = y).
exact Rmin_right.
Qed.
(* Why3 goal *)
-Lemma Max_l : forall (x:R) (y:R), (y <= x)%R ->
- ((Reals.Rbasic_fun.Rmax x y) = x).
+Lemma Max_l :
+ forall (x:R) (y:R), (y <= x)%R -> ((Reals.Rbasic_fun.Rmax x y) = x).
exact Rmax_left.
Qed.
(* Why3 goal *)
-Lemma Min_comm : forall (x:R) (y:R),
+Lemma Min_comm :
+ forall (x:R) (y:R),
((Reals.Rbasic_fun.Rmin x y) = (Reals.Rbasic_fun.Rmin y x)).
exact Rmin_comm.
Qed.
(* Why3 goal *)
-Lemma Max_comm : forall (x:R) (y:R),
+Lemma Max_comm :
+ forall (x:R) (y:R),
((Reals.Rbasic_fun.Rmax x y) = (Reals.Rbasic_fun.Rmax y x)).
exact Rmax_comm.
Qed.
(* Why3 goal *)
-Lemma Min_assoc : forall (x:R) (y:R) (z:R),
- ((Reals.Rbasic_fun.Rmin (Reals.Rbasic_fun.Rmin x y) z) = (Reals.Rbasic_fun.Rmin x (Reals.Rbasic_fun.Rmin y z))).
+Lemma Min_assoc :
+ forall (x:R) (y:R) (z:R),
+ ((Reals.Rbasic_fun.Rmin (Reals.Rbasic_fun.Rmin x y) z) =
+ (Reals.Rbasic_fun.Rmin x (Reals.Rbasic_fun.Rmin y z))).
Proof.
intros x y z.
destruct (Rle_or_lt x y) as [Hxy|Hxy].
@@ -93,8 +100,10 @@ apply Rmin_l.
Qed.
(* Why3 goal *)
-Lemma Max_assoc : forall (x:R) (y:R) (z:R),
- ((Reals.Rbasic_fun.Rmax (Reals.Rbasic_fun.Rmax x y) z) = (Reals.Rbasic_fun.Rmax x (Reals.Rbasic_fun.Rmax y z))).
+Lemma Max_assoc :
+ forall (x:R) (y:R) (z:R),
+ ((Reals.Rbasic_fun.Rmax (Reals.Rbasic_fun.Rmax x y) z) =
+ (Reals.Rbasic_fun.Rmax x (Reals.Rbasic_fun.Rmax y z))).
Proof.
intros x y z.
destruct (Rle_or_lt x y) as [Hxy|Hxy].
diff --git a/src/plugins/wp/share/coqwp/real/PowerReal.v b/src/plugins/wp/share/coqwp/real/PowerReal.v
index 1a03e615e87c85b13d3f3b3d242233624bf4b70f..1532b405d1b6e16e368ad34b05abdba7b3a57f9b 100644
--- a/src/plugins/wp/share/coqwp/real/PowerReal.v
+++ b/src/plugins/wp/share/coqwp/real/PowerReal.v
@@ -1,12 +1,13 @@
-(**************************************************************************)
-(* *)
-(* The Why3 Verification Platform / The Why3 Development Team *)
-(* Copyright 2010-2013 -- 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-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. *)
+(* *)
+(********************************************************************)
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
@@ -15,7 +16,10 @@ Require Reals.Rtrigo_def.
Require Reals.Rpower.
Require Reals.R_sqrt.
Require BuiltIn.
+Require int.Int.
+Require int.Power.
Require real.Real.
+Require real.FromInt.
Require real.Square.
Require real.ExpLog.
@@ -25,47 +29,53 @@ Import Rpower.
(* pow is replaced with (Reals.Rpower.Rpower x x1) by the coq driver *)
(* Why3 goal *)
-Lemma Pow_def : forall (x:R) (y:R), (0%R < x)%R ->
- ((Reals.Rpower.Rpower x y) = (Reals.Rtrigo_def.exp (y * (Reals.Rpower.ln x))%R)).
+Lemma Pow_def :
+ forall (x:R) (y:R), (0%R < x)%R ->
+ ((Reals.Rpower.Rpower x y) =
+ (Reals.Rtrigo_def.exp (y * (Reals.Rpower.ln x))%R)).
Proof.
easy.
Qed.
(* Why3 goal *)
-Lemma Pow_pos : forall (x:R) (y:R), (0%R < x)%R ->
- (0%R < (Reals.Rpower.Rpower x y))%R.
+Lemma Pow_pos :
+ forall (x:R) (y:R), (0%R < x)%R -> (0%R < (Reals.Rpower.Rpower x y))%R.
Proof.
intros x y h1.
apply Exp_prop.exp_pos.
Qed.
(* Why3 goal *)
-Lemma Pow_plus : forall (x:R) (y:R) (z:R), (0%R < z)%R ->
- ((Reals.Rpower.Rpower z (x + y)%R) = ((Reals.Rpower.Rpower z x) * (Reals.Rpower.Rpower z y))%R).
+Lemma Pow_plus :
+ forall (x:R) (y:R) (z:R), (0%R < z)%R ->
+ ((Reals.Rpower.Rpower z (x + y)%R) =
+ ((Reals.Rpower.Rpower z x) * (Reals.Rpower.Rpower z y))%R).
Proof.
intros x y z h1.
now apply Rpower_plus.
Qed.
(* Why3 goal *)
-Lemma Pow_mult : forall (x:R) (y:R) (z:R), (0%R < x)%R ->
- ((Reals.Rpower.Rpower (Reals.Rpower.Rpower x y) z) = (Reals.Rpower.Rpower x (y * z)%R)).
+Lemma Pow_mult :
+ forall (x:R) (y:R) (z:R), (0%R < x)%R ->
+ ((Reals.Rpower.Rpower (Reals.Rpower.Rpower x y) z) =
+ (Reals.Rpower.Rpower x (y * z)%R)).
Proof.
intros x y z h1.
now apply Rpower_mult.
Qed.
(* Why3 goal *)
-Lemma Pow_x_zero : forall (x:R), (0%R < x)%R ->
- ((Reals.Rpower.Rpower x 0%R) = 1%R).
+Lemma Pow_x_zero :
+ forall (x:R), (0%R < x)%R -> ((Reals.Rpower.Rpower x 0%R) = 1%R).
Proof.
intros x h1.
now apply Rpower_O.
Qed.
(* Why3 goal *)
-Lemma Pow_x_one : forall (x:R), (0%R < x)%R ->
- ((Reals.Rpower.Rpower x 1%R) = x).
+Lemma Pow_x_one :
+ forall (x:R), (0%R < x)%R -> ((Reals.Rpower.Rpower x 1%R) = x).
Proof.
intros x h1.
now apply Rpower_1.
@@ -82,7 +92,8 @@ now apply Rtrigo_def.exp_0.
Qed.
(* Why3 goal *)
-Lemma Pow_x_two : forall (x:R), (0%R < x)%R ->
+Lemma Pow_x_two :
+ forall (x:R), (0%R < x)%R ->
((Reals.Rpower.Rpower x 2%R) = (Reals.RIneq.Rsqr x)).
Proof.
intros x h1.
@@ -92,7 +103,8 @@ now rewrite Rmult_1_r.
Qed.
(* Why3 goal *)
-Lemma Pow_half : forall (x:R), (0%R < x)%R ->
+Lemma Pow_half :
+ forall (x:R), (0%R < x)%R ->
((Reals.Rpower.Rpower x (05 / 10)%R) = (Reals.R_sqrt.sqrt x)).
Proof.
intros x h1.
@@ -100,3 +112,17 @@ replace (5 / 10)%R with (/ 2)%R by field.
now apply Rpower_sqrt.
Qed.
+(* Why3 goal *)
+Lemma pow_from_int :
+ forall (x:Z) (y:Z), (0%Z < x)%Z -> (0%Z <= y)%Z ->
+ ((Reals.Rpower.Rpower (BuiltIn.IZR x) (BuiltIn.IZR y)) =
+ (BuiltIn.IZR (int.Power.power x y))).
+Proof.
+intros x y h1 h2.
+rewrite <- Z2Nat.id with (1 := h2).
+rewrite <- pow_IZR.
+rewrite <- INR_IZR_INZ.
+apply Rpower_pow.
+now apply (IZR_lt 0).
+Qed.
+
diff --git a/src/plugins/wp/share/coqwp/real/Real.v b/src/plugins/wp/share/coqwp/real/Real.v
index 1d80601d2f3f16324d09f8d2dfbb95fdfaede25f..8fc9927ec9bfdc1a5356e288542103a6a648ab17 100644
--- a/src/plugins/wp/share/coqwp/real/Real.v
+++ b/src/plugins/wp/share/coqwp/real/Real.v
@@ -1,12 +1,13 @@
-(**************************************************************************)
-(* *)
-(* The Why3 Verification Platform / The Why3 Development Team *)
-(* Copyright 2010-2013 -- 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-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. *)
+(* *)
+(********************************************************************)
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
@@ -14,26 +15,27 @@ Require Import BuiltIn.
Require BuiltIn.
(* Why3 comment *)
-(* infix_ls is replaced with (x < x1)%R by the coq driver *)
-
-(* Why3 goal *)
-Lemma infix_lseq_def : forall (x:R) (y:R), (x <= y)%R <-> ((x < y)%R \/
- (x = y)).
-reflexivity.
-Qed.
+(* prefix_mn is replaced with (-x)%R by the coq driver *)
(* Why3 comment *)
(* infix_pl is replaced with (x + x1)%R by the coq driver *)
(* Why3 comment *)
-(* prefix_mn is replaced with (-x)%R by the coq driver *)
+(* infix_as is replaced with (x * x1)%R by the coq driver *)
(* Why3 comment *)
-(* infix_as is replaced with (x * x1)%R by the coq driver *)
+(* infix_ls is replaced with (x < x1)%R by the coq driver *)
+
+(* Why3 goal *)
+Lemma infix_lseq_def :
+ forall (x:R) (y:R), (x <= y)%R <-> ((x < y)%R \/ (x = y)).
+Proof.
+reflexivity.
+Qed.
(* Why3 goal *)
-Lemma Assoc : forall (x:R) (y:R) (z:R),
- (((x + y)%R + z)%R = (x + (y + z)%R)%R).
+Lemma Assoc :
+ forall (x:R) (y:R) (z:R), (((x + y)%R + z)%R = (x + (y + z)%R)%R).
Proof.
exact Rplus_assoc.
Qed.
@@ -69,33 +71,28 @@ exact Rplus_comm.
Qed.
(* Why3 goal *)
-Lemma Assoc1 : forall (x:R) (y:R) (z:R),
- (((x * y)%R * z)%R = (x * (y * z)%R)%R).
+Lemma Assoc1 :
+ forall (x:R) (y:R) (z:R), (((x * y)%R * z)%R = (x * (y * z)%R)%R).
Proof.
exact Rmult_assoc.
Qed.
(* Why3 goal *)
-Lemma Mul_distr_l : forall (x:R) (y:R) (z:R),
- ((x * (y + z)%R)%R = ((x * y)%R + (x * z)%R)%R).
+Lemma Mul_distr_l :
+ forall (x:R) (y:R) (z:R), ((x * (y + z)%R)%R = ((x * y)%R + (x * z)%R)%R).
Proof.
intros x y z.
apply Rmult_plus_distr_l.
Qed.
(* Why3 goal *)
-Lemma Mul_distr_r : forall (x:R) (y:R) (z:R),
- (((y + z)%R * x)%R = ((y * x)%R + (z * x)%R)%R).
+Lemma Mul_distr_r :
+ forall (x:R) (y:R) (z:R), (((y + z)%R * x)%R = ((y * x)%R + (z * x)%R)%R).
Proof.
intros x y z.
apply Rmult_plus_distr_r.
Qed.
-(* Why3 goal *)
-Lemma infix_mn_def : forall (x:R) (y:R), ((x - y)%R = (x + (-y)%R)%R).
-reflexivity.
-Qed.
-
(* Why3 goal *)
Lemma Comm1 : forall (x:R) (y:R), ((x * y)%R = (y * x)%R).
Proof.
@@ -119,19 +116,28 @@ Qed.
(* inv is replaced with (Reals.Rdefinitions.Rinv x) by the coq driver *)
(* Why3 goal *)
-Lemma Inverse : forall (x:R), (~ (x = 0%R)) ->
- ((x * (Reals.Rdefinitions.Rinv x))%R = 1%R).
+Lemma Inverse :
+ forall (x:R), ~ (x = 0%R) -> ((x * (Reals.Rdefinitions.Rinv x))%R = 1%R).
+Proof.
exact Rinv_r.
Qed.
(* Why3 goal *)
-Lemma infix_sl_def : forall (x:R) (y:R),
- ((x / y)%R = (x * (Reals.Rdefinitions.Rinv y))%R).
+Lemma infix_mn_def : forall (x:R) (y:R), ((x - y)%R = (x + (-y)%R)%R).
+Proof.
+reflexivity.
+Qed.
+
+(* Why3 goal *)
+Lemma infix_sl_def :
+ forall (x:R) (y:R), ((x / y)%R = (x * (Reals.Rdefinitions.Rinv y))%R).
+Proof.
reflexivity.
Qed.
(* Why3 goal *)
-Lemma add_div : forall (x:R) (y:R) (z:R), (~ (z = 0%R)) ->
+Lemma add_div :
+ forall (x:R) (y:R) (z:R), ~ (z = 0%R) ->
(((x + y)%R / z)%R = ((x / z)%R + (y / z)%R)%R).
Proof.
intros.
@@ -140,7 +146,8 @@ assumption.
Qed.
(* Why3 goal *)
-Lemma sub_div : forall (x:R) (y:R) (z:R), (~ (z = 0%R)) ->
+Lemma sub_div :
+ forall (x:R) (y:R) (z:R), ~ (z = 0%R) ->
(((x - y)%R / z)%R = ((x / z)%R - (y / z)%R)%R).
Proof.
intros.
@@ -149,8 +156,8 @@ assumption.
Qed.
(* Why3 goal *)
-Lemma neg_div : forall (x:R) (y:R), (~ (y = 0%R)) ->
- (((-x)%R / y)%R = (-(x / y)%R)%R).
+Lemma neg_div :
+ forall (x:R) (y:R), ~ (y = 0%R) -> (((-x)%R / y)%R = (-(x / y)%R)%R).
Proof.
intros.
field.
@@ -158,7 +165,8 @@ assumption.
Qed.
(* Why3 goal *)
-Lemma assoc_mul_div : forall (x:R) (y:R) (z:R), (~ (z = 0%R)) ->
+Lemma assoc_mul_div :
+ forall (x:R) (y:R) (z:R), ~ (z = 0%R) ->
(((x * y)%R / z)%R = (x * (y / z)%R)%R).
Proof.
intros x y z _.
@@ -166,8 +174,9 @@ apply Rmult_assoc.
Qed.
(* Why3 goal *)
-Lemma assoc_div_mul : forall (x:R) (y:R) (z:R), ((~ (y = 0%R)) /\
- ~ (z = 0%R)) -> (((x / y)%R / z)%R = (x / (y * z)%R)%R).
+Lemma assoc_div_mul :
+ forall (x:R) (y:R) (z:R), (~ (y = 0%R) /\ ~ (z = 0%R)) ->
+ (((x / y)%R / z)%R = (x / (y * z)%R)%R).
Proof.
intros x y z (Zy, Zz).
unfold Rdiv.
@@ -176,8 +185,9 @@ now rewrite Rinv_mult_distr.
Qed.
(* Why3 goal *)
-Lemma assoc_div_div : forall (x:R) (y:R) (z:R), ((~ (y = 0%R)) /\
- ~ (z = 0%R)) -> ((x / (y / z)%R)%R = ((x * z)%R / y)%R).
+Lemma assoc_div_div :
+ forall (x:R) (y:R) (z:R), (~ (y = 0%R) /\ ~ (z = 0%R)) ->
+ ((x / (y / z)%R)%R = ((x * z)%R / y)%R).
Proof.
intros x y z (Zy, Zz).
field.
@@ -191,14 +201,14 @@ exact Rle_refl.
Qed.
(* Why3 goal *)
-Lemma Trans : forall (x:R) (y:R) (z:R), (x <= y)%R -> ((y <= z)%R ->
- (x <= z)%R).
+Lemma Trans :
+ forall (x:R) (y:R) (z:R), (x <= y)%R -> (y <= z)%R -> (x <= z)%R.
Proof.
exact Rle_trans.
Qed.
(* Why3 goal *)
-Lemma Antisymm : forall (x:R) (y:R), (x <= y)%R -> ((y <= x)%R -> (x = y)).
+Lemma Antisymm : forall (x:R) (y:R), (x <= y)%R -> (y <= x)%R -> (x = y).
Proof.
exact Rle_antisym.
Qed.
@@ -220,16 +230,17 @@ exact Rle_0_1.
Qed.
(* Why3 goal *)
-Lemma CompatOrderAdd : forall (x:R) (y:R) (z:R), (x <= y)%R ->
- ((x + z)%R <= (y + z)%R)%R.
+Lemma CompatOrderAdd :
+ forall (x:R) (y:R) (z:R), (x <= y)%R -> ((x + z)%R <= (y + z)%R)%R.
Proof.
intros x y z.
exact (Rplus_le_compat_r z x y).
Qed.
(* Why3 goal *)
-Lemma CompatOrderMult : forall (x:R) (y:R) (z:R), (x <= y)%R ->
- ((0%R <= z)%R -> ((x * z)%R <= (y * z)%R)%R).
+Lemma CompatOrderMult :
+ forall (x:R) (y:R) (z:R), (x <= y)%R -> (0%R <= z)%R ->
+ ((x * z)%R <= (y * z)%R)%R.
Proof.
intros x y z H Zz.
now apply Rmult_le_compat_r.
diff --git a/src/plugins/wp/share/coqwp/real/RealInfix.v b/src/plugins/wp/share/coqwp/real/RealInfix.v
index 5275e1ad9792d7b12b25b60207418b84076685cd..fe99b70efc6e17dae668c46566b6fbeaef60cab2 100644
--- a/src/plugins/wp/share/coqwp/real/RealInfix.v
+++ b/src/plugins/wp/share/coqwp/real/RealInfix.v
@@ -1,12 +1,13 @@
-(**************************************************************************)
-(* *)
-(* The Why3 Verification Platform / The Why3 Development Team *)
-(* Copyright 2010-2013 -- 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-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. *)
+(* *)
+(********************************************************************)
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
@@ -14,3 +15,10 @@ Require Import BuiltIn.
Require BuiltIn.
Require real.Real.
+(* Why3 goal *)
+Lemma infix_mndt_def : forall (x:R) (y:R), ((x - y)%R = (x + (-y)%R)%R).
+Proof.
+intros x y.
+reflexivity.
+Qed.
+
diff --git a/src/plugins/wp/share/coqwp/real/Square.v b/src/plugins/wp/share/coqwp/real/Square.v
index 49db3fd0aea30470459ab2b992eb1faa246c831c..11e34192e345ec8fc325f139ef8b8b8b5b417115 100644
--- a/src/plugins/wp/share/coqwp/real/Square.v
+++ b/src/plugins/wp/share/coqwp/real/Square.v
@@ -1,12 +1,13 @@
-(**************************************************************************)
-(* *)
-(* The Why3 Verification Platform / The Why3 Development Team *)
-(* Copyright 2010-2013 -- 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-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. *)
+(* *)
+(********************************************************************)
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
@@ -26,32 +27,36 @@ Qed.
(* sqrt is replaced with (Reals.R_sqrt.sqrt x) by the coq driver *)
(* Why3 goal *)
-Lemma Sqrt_positive : forall (x:R), (0%R <= x)%R ->
- (0%R <= (Reals.R_sqrt.sqrt x))%R.
+Lemma Sqrt_positive :
+ forall (x:R), (0%R <= x)%R -> (0%R <= (Reals.R_sqrt.sqrt x))%R.
intros x _.
apply sqrt_pos.
Qed.
(* Why3 goal *)
-Lemma Sqrt_square : forall (x:R), (0%R <= x)%R ->
+Lemma Sqrt_square :
+ forall (x:R), (0%R <= x)%R ->
((Reals.RIneq.Rsqr (Reals.R_sqrt.sqrt x)) = x).
exact sqrt_sqrt.
Qed.
(* Why3 goal *)
-Lemma Square_sqrt : forall (x:R), (0%R <= x)%R ->
- ((Reals.R_sqrt.sqrt (x * x)%R) = x).
+Lemma Square_sqrt :
+ forall (x:R), (0%R <= x)%R -> ((Reals.R_sqrt.sqrt (x * x)%R) = x).
exact sqrt_square.
Qed.
(* Why3 goal *)
-Lemma Sqrt_mul : forall (x:R) (y:R), ((0%R <= x)%R /\ (0%R <= y)%R) ->
- ((Reals.R_sqrt.sqrt (x * y)%R) = ((Reals.R_sqrt.sqrt x) * (Reals.R_sqrt.sqrt y))%R).
+Lemma Sqrt_mul :
+ forall (x:R) (y:R), ((0%R <= x)%R /\ (0%R <= y)%R) ->
+ ((Reals.R_sqrt.sqrt (x * y)%R) =
+ ((Reals.R_sqrt.sqrt x) * (Reals.R_sqrt.sqrt y))%R).
intros x y (hx & hy); now apply sqrt_mult.
Qed.
(* Why3 goal *)
-Lemma Sqrt_le : forall (x:R) (y:R), ((0%R <= x)%R /\ (x <= y)%R) ->
+Lemma Sqrt_le :
+ forall (x:R) (y:R), ((0%R <= x)%R /\ (x <= y)%R) ->
((Reals.R_sqrt.sqrt x) <= (Reals.R_sqrt.sqrt y))%R.
intros x y (h1 & h2); apply sqrt_le_1; auto.
apply Rle_trans with x; auto.
diff --git a/src/plugins/wp/share/coqwp/real/Trigonometry.v b/src/plugins/wp/share/coqwp/real/Trigonometry.v
index 3edae63d6aa1e62ed42e66749da9687bf88ded10..04707511fb389e17dcf319e6334d970374f631e4 100644
--- a/src/plugins/wp/share/coqwp/real/Trigonometry.v
+++ b/src/plugins/wp/share/coqwp/real/Trigonometry.v
@@ -1,12 +1,13 @@
-(**************************************************************************)
-(* *)
-(* The Why3 Verification Platform / The Why3 Development Team *)
-(* Copyright 2010-2013 -- 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-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. *)
+(* *)
+(********************************************************************)
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
@@ -30,8 +31,11 @@ Require Import Reals.
(* sin is replaced with (Reals.Rtrigo_def.sin x) by the coq driver *)
(* Why3 goal *)
-Lemma Pythagorean_identity : forall (x:R),
- (((Reals.RIneq.Rsqr (Reals.Rtrigo_def.cos x)) + (Reals.RIneq.Rsqr (Reals.Rtrigo_def.sin x)))%R = 1%R).
+Lemma Pythagorean_identity :
+ forall (x:R),
+ (((Reals.RIneq.Rsqr (Reals.Rtrigo_def.cos x)) +
+ (Reals.RIneq.Rsqr (Reals.Rtrigo_def.sin x)))%R
+ = 1%R).
Proof.
intros x.
rewrite Rplus_comm.
@@ -39,8 +43,8 @@ apply sin2_cos2.
Qed.
(* Why3 goal *)
-Lemma Cos_le_one : forall (x:R),
- ((Reals.Rbasic_fun.Rabs (Reals.Rtrigo_def.cos x)) <= 1%R)%R.
+Lemma Cos_le_one :
+ forall (x:R), ((Reals.Rbasic_fun.Rabs (Reals.Rtrigo_def.cos x)) <= 1%R)%R.
Proof.
intros x.
apply Abs.Abs_le.
@@ -48,8 +52,8 @@ apply COS_bound.
Qed.
(* Why3 goal *)
-Lemma Sin_le_one : forall (x:R),
- ((Reals.Rbasic_fun.Rabs (Reals.Rtrigo_def.sin x)) <= 1%R)%R.
+Lemma Sin_le_one :
+ forall (x:R), ((Reals.Rbasic_fun.Rabs (Reals.Rtrigo_def.sin x)) <= 1%R)%R.
Proof.
intros x.
apply Abs.Abs_le.
@@ -72,7 +76,8 @@ Qed.
(* pi is replaced with Reals.Rtrigo1.PI by the coq driver *)
(* Why3 goal *)
-Lemma Pi_double_precision_bounds : ((7074237752028440 / 2251799813685248)%R < Reals.Rtrigo1.PI)%R /\
+Lemma Pi_double_precision_bounds :
+ ((7074237752028440 / 2251799813685248)%R < Reals.Rtrigo1.PI)%R /\
(Reals.Rtrigo1.PI < (7074237752028441 / 2251799813685248)%R)%R.
Proof.
replace PI with (4 * (PI / 4))%R by field.
@@ -97,38 +102,46 @@ apply sin_PI.
Qed.
(* Why3 goal *)
-Lemma Cos_pi2 : ((Reals.Rtrigo_def.cos ((05 / 10)%R * Reals.Rtrigo1.PI)%R) = 0%R).
+Lemma Cos_pi2 :
+ ((Reals.Rtrigo_def.cos ((05 / 10)%R * Reals.Rtrigo1.PI)%R) = 0%R).
Proof.
replace (5 / 10 * PI)%R with (PI / 2)%R by field.
apply cos_PI2.
Qed.
(* Why3 goal *)
-Lemma Sin_pi2 : ((Reals.Rtrigo_def.sin ((05 / 10)%R * Reals.Rtrigo1.PI)%R) = 1%R).
+Lemma Sin_pi2 :
+ ((Reals.Rtrigo_def.sin ((05 / 10)%R * Reals.Rtrigo1.PI)%R) = 1%R).
Proof.
replace (5 / 10 * PI)%R with (PI / 2)%R by field.
apply sin_PI2.
Qed.
(* Why3 goal *)
-Lemma Cos_plus_pi : forall (x:R),
- ((Reals.Rtrigo_def.cos (x + Reals.Rtrigo1.PI)%R) = (-(Reals.Rtrigo_def.cos x))%R).
+Lemma Cos_plus_pi :
+ forall (x:R),
+ ((Reals.Rtrigo_def.cos (x + Reals.Rtrigo1.PI)%R) =
+ (-(Reals.Rtrigo_def.cos x))%R).
Proof.
intros x.
apply neg_cos.
Qed.
(* Why3 goal *)
-Lemma Sin_plus_pi : forall (x:R),
- ((Reals.Rtrigo_def.sin (x + Reals.Rtrigo1.PI)%R) = (-(Reals.Rtrigo_def.sin x))%R).
+Lemma Sin_plus_pi :
+ forall (x:R),
+ ((Reals.Rtrigo_def.sin (x + Reals.Rtrigo1.PI)%R) =
+ (-(Reals.Rtrigo_def.sin x))%R).
Proof.
intros x.
apply neg_sin.
Qed.
(* Why3 goal *)
-Lemma Cos_plus_pi2 : forall (x:R),
- ((Reals.Rtrigo_def.cos (x + ((05 / 10)%R * Reals.Rtrigo1.PI)%R)%R) = (-(Reals.Rtrigo_def.sin x))%R).
+Lemma Cos_plus_pi2 :
+ forall (x:R),
+ ((Reals.Rtrigo_def.cos (x + ((05 / 10)%R * Reals.Rtrigo1.PI)%R)%R) =
+ (-(Reals.Rtrigo_def.sin x))%R).
Proof.
intros x.
rewrite cos_sin.
@@ -137,8 +150,10 @@ apply neg_sin.
Qed.
(* Why3 goal *)
-Lemma Sin_plus_pi2 : forall (x:R),
- ((Reals.Rtrigo_def.sin (x + ((05 / 10)%R * Reals.Rtrigo1.PI)%R)%R) = (Reals.Rtrigo_def.cos x)).
+Lemma Sin_plus_pi2 :
+ forall (x:R),
+ ((Reals.Rtrigo_def.sin (x + ((05 / 10)%R * Reals.Rtrigo1.PI)%R)%R) =
+ (Reals.Rtrigo_def.cos x)).
Proof.
intros x.
rewrite cos_sin.
@@ -147,15 +162,16 @@ field.
Qed.
(* Why3 goal *)
-Lemma Cos_neg : forall (x:R),
- ((Reals.Rtrigo_def.cos (-x)%R) = (Reals.Rtrigo_def.cos x)).
+Lemma Cos_neg :
+ forall (x:R), ((Reals.Rtrigo_def.cos (-x)%R) = (Reals.Rtrigo_def.cos x)).
Proof.
intros x.
apply cos_neg.
Qed.
(* Why3 goal *)
-Lemma Sin_neg : forall (x:R),
+Lemma Sin_neg :
+ forall (x:R),
((Reals.Rtrigo_def.sin (-x)%R) = (-(Reals.Rtrigo_def.sin x))%R).
Proof.
intros x.
@@ -163,24 +179,32 @@ apply sin_neg.
Qed.
(* Why3 goal *)
-Lemma Cos_sum : forall (x:R) (y:R),
- ((Reals.Rtrigo_def.cos (x + y)%R) = (((Reals.Rtrigo_def.cos x) * (Reals.Rtrigo_def.cos y))%R - ((Reals.Rtrigo_def.sin x) * (Reals.Rtrigo_def.sin y))%R)%R).
+Lemma Cos_sum :
+ forall (x:R) (y:R),
+ ((Reals.Rtrigo_def.cos (x + y)%R) =
+ (((Reals.Rtrigo_def.cos x) * (Reals.Rtrigo_def.cos y))%R -
+ ((Reals.Rtrigo_def.sin x) * (Reals.Rtrigo_def.sin y))%R)%R).
Proof.
intros x y.
apply cos_plus.
Qed.
(* Why3 goal *)
-Lemma Sin_sum : forall (x:R) (y:R),
- ((Reals.Rtrigo_def.sin (x + y)%R) = (((Reals.Rtrigo_def.sin x) * (Reals.Rtrigo_def.cos y))%R + ((Reals.Rtrigo_def.cos x) * (Reals.Rtrigo_def.sin y))%R)%R).
+Lemma Sin_sum :
+ forall (x:R) (y:R),
+ ((Reals.Rtrigo_def.sin (x + y)%R) =
+ (((Reals.Rtrigo_def.sin x) * (Reals.Rtrigo_def.cos y))%R +
+ ((Reals.Rtrigo_def.cos x) * (Reals.Rtrigo_def.sin y))%R)%R).
Proof.
intros x y.
apply sin_plus.
Qed.
(* Why3 goal *)
-Lemma tan_def : forall (x:R),
- ((Reals.Rtrigo1.tan x) = ((Reals.Rtrigo_def.sin x) / (Reals.Rtrigo_def.cos x))%R).
+Lemma tan_def :
+ forall (x:R),
+ ((Reals.Rtrigo1.tan x) =
+ ((Reals.Rtrigo_def.sin x) / (Reals.Rtrigo_def.cos x))%R).
Proof.
intros x.
apply eq_refl.
@@ -190,8 +214,8 @@ Qed.
(* atan is replaced with (Reals.Ratan.atan x) by the coq driver *)
(* Why3 goal *)
-Lemma Tan_atan : forall (x:R),
- ((Reals.Rtrigo1.tan (Reals.Ratan.atan x)) = x).
+Lemma Tan_atan :
+ forall (x:R), ((Reals.Rtrigo1.tan (Reals.Ratan.atan x)) = x).
Proof.
intros x.
apply atan_right_inv.