Update some additional Coq realizations.

lib/coq/floating_point/Rounding.v

@@ -2,9 +2,13 @@
 (* Beware! Only edit allowed sections below    *)
 Require Import ZArith.
 Require Import Rbase.
+
+(* Why3 assumption *)
 Inductive mode  :=
-  | NearestTiesToEven : mode
-  | ToZero : mode
-  | Up : mode
-  | Down : mode
+  | NearestTiesToEven : mode 
+  | ToZero : mode 
+  | Up : mode 
+  | Down : mode 
   | NearestTiesToAway : mode .
+
+

lib/coq/int/EuclideanDivision.v

@@ -2,47 +2,34 @@
 (* Beware! Only edit allowed sections below    *)
 Require Import ZArith.
 Require Import Rbase.
-(*Add Rec LoadPath "/home/guillaume/bin/why3/share/why3/theories".*)
-(*Add Rec LoadPath "/home/guillaume/bin/why3/share/why3/modules".*)
 Require int.Int.
 Require int.Abs.
 
-Definition div : Z -> Z -> Z.
-(* YOU MAY EDIT THE CONTEXT BELOW *)
+(* Why3 goal *)
+Definition div: Z -> Z -> Z.
 intros x y.
 case (Z_le_dec 0 (Zmod x y)) ; intros H.
 exact (Zdiv x y).
 exact (Zdiv x y + 1)%Z.
 Defined.
-(* DO NOT EDIT BELOW *)
 
-Definition mod1 : Z -> Z -> Z.
-(* YOU MAY EDIT THE CONTEXT BELOW *)
+(* Why3 goal *)
+Definition mod1: Z -> Z -> Z.
 intros x y.
 exact (x - y * div x y)%Z.
 Defined.
-(* DO NOT EDIT BELOW *)
-
-(* YOU MAY EDIT THE CONTEXT BELOW *)
-
-(* DO NOT EDIT BELOW *)
 
+(* Why3 goal *)
 Lemma Div_mod : forall (x:Z) (y:Z), (~ (y = 0%Z)) -> (x = ((y * (div x
   y))%Z + (mod1 x y))%Z).
-(* YOU MAY EDIT THE PROOF BELOW *)
 intros x y Zy.
 unfold mod1, div.
 case Z_le_dec ; intros H ; ring.
 Qed.
-(* DO NOT EDIT BELOW *)
-
-(* YOU MAY EDIT THE CONTEXT BELOW *)
-
-(* DO NOT EDIT BELOW *)
 
+(* 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).
-(* YOU MAY EDIT THE PROOF BELOW *)
 intros x y (Hx,Hy).
 unfold div.
 case Z_le_dec ; intros H.
@@ -59,15 +46,10 @@ elim H.
 apply Z_mod_lt.
 now apply Zlt_gt.
 Qed.
-(* DO NOT EDIT BELOW *)
-
-(* YOU MAY EDIT THE CONTEXT BELOW *)
-
-(* DO NOT EDIT BELOW *)
 
+(* Why3 goal *)
 Lemma Mod_bound : forall (x:Z) (y:Z), (~ (y = 0%Z)) -> ((0%Z <= (mod1 x
   y))%Z /\ ((mod1 x y) <  (Zabs y))%Z).
-(* YOU MAY EDIT THE PROOF BELOW *)
 intros x y Zy.
 zify.
 assert (H1 := Z_mod_neg x y).
@@ -80,31 +62,40 @@ replace (x - y * (x / y + 1))%Z with (x - x / y * y - y)%Z by ring.
 rewrite <- Zmod_eq_full with (1 := Zy).
 omega.
 Qed.
-(* DO NOT EDIT BELOW *)
-
-(* YOU MAY EDIT THE CONTEXT BELOW *)
-
-(* DO NOT EDIT BELOW *)
 
+(* Why3 goal *)
 Lemma Mod_1 : forall (x:Z), ((mod1 x 1%Z) = 0%Z).
-(* YOU MAY EDIT THE PROOF BELOW *)
 intros x.
 unfold mod1, div.
 rewrite Zmod_1_r, Zdiv_1_r, Zmult_1_l.
 apply Zminus_diag.
 Qed.
-(* DO NOT EDIT BELOW *)
-
-(* YOU MAY EDIT THE CONTEXT BELOW *)
-
-(* DO NOT EDIT BELOW *)
 
+(* Why3 goal *)
 Lemma Div_1 : forall (x:Z), ((div x 1%Z) = x).
-(* YOU MAY EDIT THE PROOF BELOW *)
 intros x.
 unfold div.
 now rewrite Zmod_1_r, Zdiv_1_r.
 Qed.
-(* DO NOT EDIT BELOW *)
+
+(* Why3 goal *)
+Lemma Div_inf : forall (x:Z) (y: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.
+now apply Zdiv_small.
+elim H.
+now rewrite Zmod_small.
+Qed.
+
+(* Why3 goal *)
+Lemma Mod_0 : forall (y:Z), (~ (y = 0%Z)) -> ((mod1 0%Z y) = 0%Z).
+intros y Hy.
+unfold mod1, div.
+rewrite Zmod_0_l.
+simpl.
+now rewrite Zdiv_0_l, Zmult_0_r.
+Qed.
 
 

lib/coq/real/MinMax.v

@@ -2,46 +2,30 @@
 (* Beware! Only edit allowed sections below    *)
 Require Import ZArith.
 Require Import Rbase.
-(*Add Rec LoadPath "/home/guillaume/bin/why3/share/why3/theories".*)
-(*Add Rec LoadPath "/home/guillaume/bin/why3/share/why3/modules".*)
 Require real.Real.
 
-(* no editable section? *)
 Require Import Rbasic_fun.
 
+(* Why3 goal *)
 Definition min: R -> R -> R.
-(* YOU MAY EDIT THE PROOF BELOW *)
 exact Rmin.
 Defined.
-(* DO NOT EDIT BELOW *)
-
 
+(* Why3 goal *)
 Definition max: R -> R -> R.
-(* YOU MAY EDIT THE PROOF BELOW *)
 exact Rmax.
 Defined.
-(* DO NOT EDIT BELOW *)
-
-
-(* YOU MAY EDIT THE CONTEXT BELOW *)
-
-(* DO NOT EDIT BELOW *)
 
+(* Why3 goal *)
 Lemma Max_is_ge : forall (x:R) (y:R), (x <= (max x y))%R /\ (y <= (max x
   y))%R.
-(* YOU MAY EDIT THE PROOF BELOW *)
 split.
 apply Rmax_l.
 apply Rmax_r.
 Qed.
-(* DO NOT EDIT BELOW *)
-
-(* YOU MAY EDIT THE CONTEXT BELOW *)
-
-(* DO NOT EDIT BELOW *)
 
+(* Why3 goal *)
 Lemma Max_is_some : forall (x:R) (y:R), ((max x y) = x) \/ ((max x y) = y).
-(* YOU MAY EDIT THE PROOF BELOW *)
 intros x y.
 destruct (Rle_or_lt x y) as [H|H].
 right.
@@ -50,27 +34,17 @@ left.
 apply Rmax_left.
 now apply Rlt_le.
 Qed.
-(* DO NOT EDIT BELOW *)
-
-(* YOU MAY EDIT THE CONTEXT BELOW *)
-
-(* DO NOT EDIT BELOW *)
 
+(* Why3 goal *)
 Lemma Min_is_le : forall (x:R) (y:R), ((min x y) <= x)%R /\ ((min x
   y) <= y)%R.
-(* YOU MAY EDIT THE PROOF BELOW *)
 split.
 apply Rmin_l.
 apply Rmin_r.
 Qed.
-(* DO NOT EDIT BELOW *)
-
-(* YOU MAY EDIT THE CONTEXT BELOW *)
-
-(* DO NOT EDIT BELOW *)
 
+(* Why3 goal *)
 Lemma Min_is_some : forall (x:R) (y:R), ((min x y) = x) \/ ((min x y) = y).
-(* YOU MAY EDIT THE PROOF BELOW *)
 intros x y.
 destruct (Rle_or_lt x y) as [H|H].
 left.
@@ -79,6 +53,5 @@ right.
 apply Rmin_right.
 now apply Rlt_le.
 Qed.
-(* DO NOT EDIT BELOW *)
 
 

lib/coq/real/Square.v

@@ -3,47 +3,30 @@
 Require Import ZArith.
 Require Import Rbase.
 Require Import R_sqrt.
-(*Add Rec LoadPath "/home/guillaume/bin/why3/share/why3/theories".*)
-(*Add Rec LoadPath "/home/guillaume/bin/why3/share/why3/modules".*)
 Require real.Real.
+
+(* Why3 assumption *)
 Definition sqr(x:R): R := (x * x)%R.
 
+(* Why3 goal *)
 Definition sqrt: R -> R.
-(* YOU MAY EDIT THE PROOF BELOW *)
 exact sqrt.
 Defined.
-(* DO NOT EDIT BELOW *)
-
-
-(* YOU MAY EDIT THE CONTEXT BELOW *)
-
-(* DO NOT EDIT BELOW *)
 
+(* Why3 goal *)
 Lemma Sqrt_positive : forall (x:R), (0%R <= x)%R -> (0%R <= (sqrt x))%R.
-(* YOU MAY EDIT THE PROOF BELOW *)
 intros x _.
 apply sqrt_pos.
 Qed.
-(* DO NOT EDIT BELOW *)
-
-(* YOU MAY EDIT THE CONTEXT BELOW *)
-
-(* DO NOT EDIT BELOW *)
 
+(* Why3 goal *)
 Lemma Sqrt_square : forall (x:R), (0%R <= x)%R -> ((sqr (sqrt x)) = x).
-(* YOU MAY EDIT THE PROOF BELOW *)
 exact sqrt_sqrt.
 Qed.
-(* DO NOT EDIT BELOW *)
-
-(* YOU MAY EDIT THE CONTEXT BELOW *)
-
-(* DO NOT EDIT BELOW *)
 
+(* Why3 goal *)
 Lemma Square_sqrt : forall (x:R), (0%R <= x)%R -> ((sqrt (x * x)%R) = x).
-(* YOU MAY EDIT THE PROOF BELOW *)
 exact sqrt_square.
 Qed.
-(* DO NOT EDIT BELOW *)