Commit 74f9e12f authored by Guillaume Melquiond's avatar Guillaume Melquiond

Update Coq realizations.

parent efa0940b
......@@ -5,7 +5,7 @@ Require BuiltIn.
(* Why3 goal *)
Lemma andb_def : forall (x:bool) (y:bool),
((andb x y) = match x with
((Init.Datatypes.andb x y) = match x with
| true => y
| false => false
end).
......@@ -16,7 +16,7 @@ Qed.
(* Why3 goal *)
Lemma orb_def : forall (x:bool) (y:bool),
((orb x y) = match x with
((Init.Datatypes.orb x y) = match x with
| false => y
| true => true
end).
......@@ -26,7 +26,8 @@ apply refl_equal.
Qed.
(* Why3 goal *)
Lemma xorb_def : forall (x:bool) (y:bool), ((xorb x y) = match (x,
Lemma xorb_def : forall (x:bool) (y:bool),
((Init.Datatypes.xorb x y) = match (x,
y) with
| (true, false) => true
| (false, true) => true
......@@ -39,7 +40,7 @@ Qed.
(* Why3 goal *)
Lemma notb_def : forall (x:bool),
((negb x) = match x with
((Init.Datatypes.negb x) = match x with
| false => true
| true => false
end).
......@@ -49,7 +50,8 @@ apply refl_equal.
Qed.
(* Why3 goal *)
Lemma implb_def : forall (x:bool) (y:bool), ((implb x y) = match (x,
Lemma implb_def : forall (x:bool) (y:bool),
((Init.Datatypes.implb x y) = match (x,
y) with
| (true, false) => false
| (_, _) => true
......
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require Import Rbasic_fun.
Require Reals.Rbasic_fun.
Require BuiltIn.
Require int.Int.
Require real.Real.
......@@ -34,21 +34,21 @@ Defined.
(* Why3 assumption *)
Definition round_error (x:floating_point.DoubleFormat.double): R :=
(Rabs ((value x) - (exact x))%R).
(Reals.Rbasic_fun.Rabs ((value x) - (exact x))%R).
(* Why3 assumption *)
Definition total_error (x:floating_point.DoubleFormat.double): R :=
(Rabs ((value x) - (model x))%R).
(Reals.Rbasic_fun.Rabs ((value x) - (model x))%R).
(* Why3 assumption *)
Definition no_overflow (m:floating_point.Rounding.mode) (x:R): Prop :=
((Rabs (round m
((Reals.Rbasic_fun.Rabs (round m
x)) <= (9007199254740991 * 19958403095347198116563727130368385660674512604354575415025472424372118918689640657849579654926357010893424468441924952439724379883935936607391717982848314203200056729510856765175377214443629871826533567445439239933308104551208703888888552684480441575071209068757560416423584952303440099278848)%R)%R.
(* Why3 goal *)
Lemma Bounded_real_no_overflow : forall (m:floating_point.Rounding.mode)
(x:R),
((Rabs x) <= (9007199254740991 * 19958403095347198116563727130368385660674512604354575415025472424372118918689640657849579654926357010893424468441924952439724379883935936607391717982848314203200056729510856765175377214443629871826533567445439239933308104551208703888888552684480441575071209068757560416423584952303440099278848)%R)%R ->
((Reals.Rbasic_fun.Rabs x) <= (9007199254740991 * 19958403095347198116563727130368385660674512604354575415025472424372118918689640657849579654926357010893424468441924952439724379883935936607391717982848314203200056729510856765175377214443629871826533567445439239933308104551208703888888552684480441575071209068757560416423584952303440099278848)%R)%R ->
(no_overflow m x).
exact (Bounded_real_no_overflow 53 1024 (refl_equal true) (refl_equal true)).
Qed.
......@@ -74,14 +74,14 @@ Qed.
(* Why3 goal *)
Lemma Bounded_value : forall (x:floating_point.DoubleFormat.double),
((Rabs (value x)) <= (9007199254740991 * 19958403095347198116563727130368385660674512604354575415025472424372118918689640657849579654926357010893424468441924952439724379883935936607391717982848314203200056729510856765175377214443629871826533567445439239933308104551208703888888552684480441575071209068757560416423584952303440099278848)%R)%R.
((Reals.Rbasic_fun.Rabs (value x)) <= (9007199254740991 * 19958403095347198116563727130368385660674512604354575415025472424372118918689640657849579654926357010893424468441924952439724379883935936607391717982848314203200056729510856765175377214443629871826533567445439239933308104551208703888888552684480441575071209068757560416423584952303440099278848)%R)%R.
now apply Bounded_value.
Qed.
(* Why3 goal *)
Lemma Exact_rounding_for_integers : forall (m:floating_point.Rounding.mode)
(i:Z), (((-9007199254740992%Z)%Z <= i)%Z /\ (i <= 9007199254740992%Z)%Z) ->
((round m (IZR i)) = (IZR i)).
((round m (Reals.Raxioms.IZR i)) = (Reals.Raxioms.IZR i)).
intros m i Hi.
now apply Exact_rounding_for_integers.
Qed.
......@@ -160,9 +160,9 @@ Definition div_post (m:floating_point.Rounding.mode)
(x:floating_point.DoubleFormat.double)
(y:floating_point.DoubleFormat.double)
(res:floating_point.DoubleFormat.double): Prop := ((value res) = (round m
(Rdiv (value x) (value y))%R)) /\
(((exact res) = (Rdiv (exact x) (exact y))%R) /\
((model res) = (Rdiv (model x) (model y))%R)).
((value x) / (value y))%R)) /\
(((exact res) = ((exact x) / (exact y))%R) /\
((model res) = ((model x) / (model y))%R)).
(* Why3 assumption *)
Definition neg_post (x:floating_point.DoubleFormat.double)
......
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require Import Rbasic_fun.
Require Reals.Rbasic_fun.
Require BuiltIn.
Require int.Int.
Require real.Real.
......@@ -34,15 +34,16 @@ Defined.
(* Why3 assumption *)
Definition round_error (x:floating_point.SingleFormat.single): R :=
(Rabs ((value x) - (exact x))%R).
(Reals.Rbasic_fun.Rabs ((value x) - (exact x))%R).
(* Why3 assumption *)
Definition total_error (x:floating_point.SingleFormat.single): R :=
(Rabs ((value x) - (model x))%R).
(Reals.Rbasic_fun.Rabs ((value x) - (model x))%R).
(* Why3 assumption *)
Definition no_overflow (m:floating_point.Rounding.mode) (x:R): Prop :=
((Rabs (round m x)) <= (33554430 * 10141204801825835211973625643008)%R)%R.
((Reals.Rbasic_fun.Rabs (round m
x)) <= (33554430 * 10141204801825835211973625643008)%R)%R.
Lemma max_single_eq: (33554430 * 10141204801825835211973625643008 = max 24 128)%R.
unfold max, Fcore_defs.F2R; simpl.
......@@ -51,7 +52,8 @@ Qed.
(* Why3 goal *)
Lemma Bounded_real_no_overflow : forall (m:floating_point.Rounding.mode)
(x:R), ((Rabs x) <= (33554430 * 10141204801825835211973625643008)%R)%R ->
(x:R),
((Reals.Rbasic_fun.Rabs x) <= (33554430 * 10141204801825835211973625643008)%R)%R ->
(no_overflow m x).
intros m x Hx.
unfold no_overflow.
......@@ -81,7 +83,7 @@ Qed.
(* Why3 goal *)
Lemma Bounded_value : forall (x:floating_point.SingleFormat.single),
((Rabs (value x)) <= (33554430 * 10141204801825835211973625643008)%R)%R.
((Reals.Rbasic_fun.Rabs (value x)) <= (33554430 * 10141204801825835211973625643008)%R)%R.
rewrite max_single_eq.
now apply Bounded_value.
Qed.
......@@ -89,7 +91,7 @@ Qed.
(* Why3 goal *)
Lemma Exact_rounding_for_integers : forall (m:floating_point.Rounding.mode)
(i:Z), (((-16777216%Z)%Z <= i)%Z /\ (i <= 16777216%Z)%Z) -> ((round m
(IZR i)) = (IZR i)).
(Reals.Raxioms.IZR i)) = (Reals.Raxioms.IZR i)).
intros m i Hi.
now apply Exact_rounding_for_integers.
Qed.
......@@ -171,9 +173,9 @@ Definition div_post (m:floating_point.Rounding.mode)
(x:floating_point.SingleFormat.single)
(y:floating_point.SingleFormat.single)
(res:floating_point.SingleFormat.single): Prop := ((value res) = (round m
(Rdiv (value x) (value y))%R)) /\
(((exact res) = (Rdiv (exact x) (exact y))%R) /\
((model res) = (Rdiv (model x) (model y))%R)).
((value x) / (value y))%R)) /\
(((exact res) = ((exact x) / (exact y))%R) /\
((model res) = ((model x) / (model y))%R)).
(* Why3 assumption *)
Definition neg_post (x:floating_point.SingleFormat.single)
......
......@@ -5,11 +5,12 @@ Require BuiltIn.
Require int.Int.
(* Why3 comment *)
(* abs is replaced with (Zabs x) by the coq driver *)
(* 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 -> ((Zabs x) = x)) /\
((~ (0%Z <= x)%Z) -> ((Zabs 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.
......@@ -21,15 +22,15 @@ now apply Zgt_lt.
Qed.
(* Why3 goal *)
Lemma Abs_le : forall (x:Z) (y:Z), ((Zabs 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.
Qed.
(* Why3 goal *)
Lemma Abs_pos : forall (x:Z), (0%Z <= (Zabs x))%Z.
Lemma Abs_pos : forall (x:Z), (0%Z <= (ZArith.BinInt.Z.abs x))%Z.
exact Zabs_pos.
Qed.
......@@ -49,7 +49,7 @@ Qed.
(* 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).
y))%Z /\ ((mod1 x y) < (ZArith.BinInt.Z.abs y))%Z).
intros x y Zy.
zify.
assert (H1 := Z_mod_neg x y).
......
......@@ -5,21 +5,22 @@ Require BuiltIn.
Require int.Int.
(* Why3 comment *)
(* min is replaced with (Zmin x x1) by the coq driver *)
(* min is replaced with (ZArith.BinInt.Z.min x x1) by the coq driver *)
(* Why3 comment *)
(* max is replaced with (Zmax x x1) by the coq driver *)
(* max is replaced with (ZArith.BinInt.Z.max x x1) by the coq driver *)
(* Why3 goal *)
Lemma Max_is_ge : forall (x:Z) (y:Z), (x <= (Zmax x y))%Z /\
(y <= (Zmax x y))%Z.
Lemma Max_is_ge : forall (x:Z) (y:Z), (x <= (ZArith.BinInt.Z.max x y))%Z /\
(y <= (ZArith.BinInt.Z.max x y))%Z.
split.
apply Zle_max_l.
apply Zle_max_r.
Qed.
(* Why3 goal *)
Lemma Max_is_some : forall (x:Z) (y:Z), ((Zmax x y) = x) \/ ((Zmax x y) = y).
Lemma Max_is_some : forall (x:Z) (y:Z), ((ZArith.BinInt.Z.max x y) = x) \/
((ZArith.BinInt.Z.max x y) = y).
intros x y.
unfold Zmax.
case Zcompare.
......@@ -29,15 +30,16 @@ now left.
Qed.
(* Why3 goal *)
Lemma Min_is_le : forall (x:Z) (y:Z), ((Zmin x y) <= x)%Z /\
((Zmin x y) <= y)%Z.
Lemma Min_is_le : forall (x:Z) (y:Z), ((ZArith.BinInt.Z.min x y) <= x)%Z /\
((ZArith.BinInt.Z.min x y) <= y)%Z.
split.
apply Zle_min_l.
apply Zle_min_r.
Qed.
(* Why3 goal *)
Lemma Min_is_some : forall (x:Z) (y:Z), ((Zmin x y) = x) \/ ((Zmin x y) = y).
Lemma Min_is_some : forall (x:Z) (y:Z), ((ZArith.BinInt.Z.min x y) = x) \/
((ZArith.BinInt.Z.min x y) = y).
intros x y.
unfold Zmin.
case Zcompare.
......@@ -47,33 +49,39 @@ now right.
Qed.
(* Why3 goal *)
Lemma Max_x : forall (x:Z) (y:Z), (y <= x)%Z -> ((Zmax x y) = x).
Lemma Max_x : forall (x:Z) (y:Z), (y <= x)%Z ->
((ZArith.BinInt.Z.max x y) = x).
exact Zmax_l.
Qed.
(* Why3 goal *)
Lemma Max_y : forall (x:Z) (y:Z), (x <= y)%Z -> ((Zmax x y) = y).
Lemma Max_y : forall (x:Z) (y:Z), (x <= y)%Z ->
((ZArith.BinInt.Z.max x y) = y).
exact Zmax_r.
Qed.
(* Why3 goal *)
Lemma Min_x : forall (x:Z) (y:Z), (x <= y)%Z -> ((Zmin x y) = x).
Lemma Min_x : forall (x:Z) (y:Z), (x <= y)%Z ->
((ZArith.BinInt.Z.min x y) = x).
exact Zmin_l.
Qed.
(* Why3 goal *)
Lemma Min_y : forall (x:Z) (y:Z), (y <= x)%Z -> ((Zmin x y) = y).
Lemma Min_y : forall (x:Z) (y:Z), (y <= x)%Z ->
((ZArith.BinInt.Z.min x y) = y).
exact Zmin_r.
Qed.
(* Why3 goal *)
Lemma Max_sym : forall (x:Z) (y:Z), (y <= x)%Z -> ((Zmax x y) = (Zmax y x)).
Lemma Max_sym : forall (x:Z) (y:Z), (y <= x)%Z ->
((ZArith.BinInt.Z.max x y) = (ZArith.BinInt.Z.max y x)).
intros x y _.
apply Zmax_comm.
Qed.
(* Why3 goal *)
Lemma Min_sym : forall (x:Z) (y:Z), (y <= x)%Z -> ((Zmin x y) = (Zmin y x)).
Lemma Min_sym : forall (x:Z) (y:Z), (y <= x)%Z ->
((ZArith.BinInt.Z.min x y) = (ZArith.BinInt.Z.min y x)).
intros x y _.
apply Zmin_comm.
Qed.
......
......@@ -11,8 +11,8 @@ Require list.Mem.
Lemma infix_plpl_def {a:Type} {a_WT:WhyType a}: forall (l1:(list a))
(l2:(list a)),
((List.app l1 l2) = match l1 with
| nil => l2
| (cons x1 r1) => (cons x1 (List.app r1 l2))
| Init.Datatypes.nil => l2
| (Init.Datatypes.cons x1 r1) => (Init.Datatypes.cons x1 (List.app r1 l2))
end).
Proof.
now intros [|h1 q1] l2.
......@@ -31,7 +31,7 @@ Qed.
(* Why3 goal *)
Lemma Append_l_nil : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)),
((List.app l nil) = l).
((List.app l Init.Datatypes.nil) = l).
Proof.
intros a a_WT l.
apply app_nil_r.
......@@ -75,7 +75,7 @@ Qed.
(* Why3 goal *)
Lemma mem_decomp : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(l:(list a)), (list.Mem.mem x l) -> exists l1:(list a), exists l2:(list a),
(l = (List.app l1 (cons x l2))).
(l = (List.app l1 (Init.Datatypes.cons x l2))).
Proof.
intros a a_WT x l h1.
apply in_split.
......
......@@ -8,14 +8,14 @@ Require option.Option.
(* Why3 assumption *)
Definition hd {a:Type} {a_WT:WhyType a} (l:(list a)): (option a) :=
match l with
| nil => None
| (cons h _) => (Some h)
| Init.Datatypes.nil => Init.Datatypes.None
| (Init.Datatypes.cons h _) => (Init.Datatypes.Some h)
end.
(* Why3 assumption *)
Definition tl {a:Type} {a_WT:WhyType a} (l:(list a)): (option (list a)) :=
match l with
| nil => None
| (cons _ t) => (Some t)
| Init.Datatypes.nil => Init.Datatypes.None
| (Init.Datatypes.cons _ t) => (Init.Datatypes.Some t)
end.
......@@ -8,8 +8,8 @@ Require list.List.
(* Why3 assumption *)
Fixpoint length {a:Type} {a_WT:WhyType a} (l:(list a)) {struct l}: Z :=
match l with
| nil => 0%Z
| (cons _ r) => (1%Z + (length r))%Z
| Init.Datatypes.nil => 0%Z
| (Init.Datatypes.cons _ r) => (1%Z + (length r))%Z
end.
Lemma length_std :
......@@ -34,7 +34,7 @@ Qed.
(* Why3 goal *)
Lemma Length_nil : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)),
((length l) = 0%Z) <-> (l = nil).
((length l) = 0%Z) <-> (l = Init.Datatypes.nil).
Proof.
intros a a_WT [|h t] ; split ; try easy.
unfold length. fold length.
......
......@@ -7,8 +7,8 @@ Require list.List.
(* Why3 assumption *)
Fixpoint mem {a:Type} {a_WT:WhyType a} (x:a) (l:(list a)) {struct l}: Prop :=
match l with
| nil => False
| (cons y r) => (x = y) \/ (mem x r)
| Init.Datatypes.nil => False
| (Init.Datatypes.cons y r) => (x = y) \/ (mem x r)
end.
Lemma mem_std :
......
......@@ -16,9 +16,10 @@ Defined.
(* Why3 goal *)
Lemma nth_def : forall {a:Type} {a_WT:WhyType a}, forall (n:Z) (l:(list a)),
match l with
| nil => ((nth n l) = None)
| (cons x r) => ((n = 0%Z) -> ((nth n l) = (Some x))) /\ ((~ (n = 0%Z)) ->
((nth n l) = (nth (n - 1%Z)%Z r)))
| Init.Datatypes.nil => ((nth n l) = Init.Datatypes.None)
| (Init.Datatypes.cons x r) => ((n = 0%Z) -> ((nth n
l) = (Init.Datatypes.Some x))) /\ ((~ (n = 0%Z)) -> ((nth n
l) = (nth (n - 1%Z)%Z r)))
end.
Proof.
intros a a_WT n l.
......
......@@ -10,9 +10,9 @@ Require list.HdTl.
(* Why3 goal *)
Lemma Nth_tl : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
(l2:(list a)), ((list.HdTl.tl l1) = (Some l2)) -> forall (i:Z),
(~ (i = (-1%Z)%Z)) -> ((list.Nth.nth i l2) = (list.Nth.nth (i + 1%Z)%Z
l1)).
(l2:(list a)), ((list.HdTl.tl l1) = (Init.Datatypes.Some l2)) ->
forall (i:Z), (~ (i = (-1%Z)%Z)) -> ((list.Nth.nth i
l2) = (list.Nth.nth (i + 1%Z)%Z l1)).
Proof.
intros a a_WT [|x1 l1] l2 h1 i h2.
easy.
......
......@@ -10,7 +10,7 @@ Require option.Option.
(* Why3 goal *)
Lemma nth_none_1 : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a))
(i:Z), (i < 0%Z)%Z -> ((list.Nth.nth i l) = None).
(i:Z), (i < 0%Z)%Z -> ((list.Nth.nth i l) = Init.Datatypes.None).
Proof.
intros a a_WT l.
induction l as [|h q].
......@@ -28,7 +28,8 @@ Qed.
(* Why3 goal *)
Lemma nth_none_2 : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a))
(i:Z), ((list.Length.length l) <= i)%Z -> ((list.Nth.nth i l) = None).
(i:Z), ((list.Length.length l) <= i)%Z -> ((list.Nth.nth i
l) = Init.Datatypes.None).
Proof.
intros a a_WT l.
induction l as [|h q].
......@@ -51,7 +52,7 @@ Qed.
(* Why3 goal *)
Lemma nth_none_3 : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a))
(i:Z), ((list.Nth.nth i l) = None) -> ((i < 0%Z)%Z \/
(i:Z), ((list.Nth.nth i l) = Init.Datatypes.None) -> ((i < 0%Z)%Z \/
((list.Length.length l) <= i)%Z).
Proof.
intros a a_WT l.
......
......@@ -11,8 +11,9 @@ Require list.Append.
(* Why3 goal *)
Lemma reverse_def {a:Type} {a_WT:WhyType a}: forall (l:(list a)),
((List.rev l) = match l with
| nil => nil
| (cons x r) => (List.app (List.rev r) (cons x nil))
| Init.Datatypes.nil => Init.Datatypes.nil
| (Init.Datatypes.cons x r) =>
(List.app (List.rev r) (Init.Datatypes.cons x Init.Datatypes.nil))
end).
Proof.
now intros [|x l].
......@@ -21,7 +22,7 @@ Qed.
(* Why3 goal *)
Lemma reverse_append : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
(l2:(list a)) (x:a),
((List.app (List.rev (cons x l1)) l2) = (List.app (List.rev l1) (cons x l2))).
((List.app (List.rev (Init.Datatypes.cons x l1)) l2) = (List.app (List.rev l1) (Init.Datatypes.cons x l2))).
Proof.
intros a a_WT l1 l2 x.
simpl.
......
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require Import ZOdiv.
Require BuiltIn.
Require int.Int.
Require int.Abs.
......
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require Import ZOdiv.
Require BuiltIn.
Require int.Int.
Require int.Abs.
......@@ -141,7 +140,7 @@ Qed.
(* Why3 goal *)
Lemma divides_bounds : forall (a:Z) (b:Z), (divides a b) -> ((~ (b = 0%Z)) ->
((Zabs a) <= (Zabs b))%Z).
((ZArith.BinInt.Z.abs a) <= (ZArith.BinInt.Z.abs b))%Z).
Proof.
exact Zdivide_bounds.
Qed.
......@@ -176,7 +175,7 @@ Qed.
(* Why3 goal *)
Lemma mod_divides_computer : forall (a:Z) (b:Z), (~ (b = 0%Z)) ->
(((ZOmod a b) = 0%Z) -> (divides b a)).
(((ZArith.BinInt.Z.rem a b) = 0%Z) -> (divides b a)).
Proof.
intros a b Zb H.
exists (Z.quot a b).
......@@ -186,7 +185,7 @@ Qed.
(* Why3 goal *)
Lemma divides_mod_computer : forall (a:Z) (b:Z), (~ (b = 0%Z)) -> ((divides b
a) -> ((ZOmod a b) = 0%Z)).
a) -> ((ZArith.BinInt.Z.rem a b) = 0%Z)).
Proof.
intros a b Zb (q,H).
rewrite H.
......
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require Import ZOdiv.
Require BuiltIn.
Require int.Int.
Require int.Abs.
......@@ -115,7 +114,7 @@ Qed.
(* Why3 goal *)
Lemma Gcd_computer_mod : forall (a:Z) (b:Z), (~ (b = 0%Z)) -> ((gcd b
(ZOmod a b)) = (gcd a b)).
(ZArith.BinInt.Z.rem a b)) = (gcd a b)).
Proof.
intros a b _.
rewrite (Zgcd_comm a b).
......
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require Import ZOdiv.
Require BuiltIn.
Require int.Int.
Require int.Abs.
......
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require Import Rbasic_fun.
Require Reals.Rbasic_fun.
Require BuiltIn.
Require real.Real.
Import Rbasic_fun.
(* Why3 comment *)
(* abs is replaced with (Rabs x) by the coq driver *)
(* 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 -> ((Rabs x) = x)) /\
((~ (0%R <= x)%R) -> ((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.
......@@ -21,8 +22,8 @@ now apply Rnot_le_lt.
Qed.
(* Why3 goal *)
Lemma Abs_le : forall (x:R) (y:R), ((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)]).
......@@ -47,25 +48,25 @@ exact H1.
Qed.
(* Why3 goal *)
Lemma Abs_pos : forall (x:R), (0%R <= (Rabs x))%R.
Lemma Abs_pos : forall (x:R), (0%R <= (Reals.Rbasic_fun.Rabs x))%R.
exact Rabs_pos.
Qed.
(* Why3 goal *)
Lemma Abs_sum : forall (x:R) (y:R),
((Rabs (x + y)%R) <= ((Rabs x) + (Rabs y))%R)%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),
((Rabs (x * y)%R) = ((Rabs x) * (Rabs 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),
((Rabs (x - z)%R) <= ((Rabs (x - y)%R) + (Rabs (y - z)%R))%R)%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.
......
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require Import Rtrigo_def.
Require Import Rpower.
Require Reals.Rtrigo_def.
Require Reals.Rpower.
Require BuiltIn.
Require real.Real.
......@@ -10,10 +10,10 @@ Import Rtrigo_def.
Import Rpower.
(* Why3 comment *)
(* exp is replaced with (exp x) by the coq driver *)
(* exp is replaced with (Reals.Rtrigo_def.exp x) by the coq driver *)
(* Why3 goal *)
Lemma Exp_zero : ((exp 0%R) = 1%R).
Lemma Exp_zero : ((Reals.Rtrigo_def.exp 0%R) = 1%R).
exact exp_0.
Qed.
......@@ -21,38 +21,41 @@ Require Import Exp_prop.
(* Why3 goal *)
Lemma Exp_sum : forall (x:R) (y:R),
((exp (x + y)%R) = ((exp x) * (exp y))%R).
((Reals.Rtrigo_def.exp (x + y)%R) = ((Reals.Rtrigo_def.exp x) * (Reals.Rtrigo_def.exp y))%R).
exact exp_plus.
Qed.
(* Why3 comment *)
(* log is replaced with (ln x) by the coq driver *)
(* log is replaced with (Reals.Rpower.ln x) by the coq driver *)
(* Why3 goal *)
Lemma Log_one : ((ln 1%R) = 0%R).
Lemma Log_one : ((Reals.Rpower.ln 1%R) = 0%R).
exact ln_1.
Qed.
(* Why3 goal *)
Lemma Log_mul : forall (x:R) (y:R), ((0%R < x)%R /\ (0%R < y)%R) ->
((ln (x * y)%R) = ((ln x) + (ln 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), ((ln (exp x)) = x).
Lemma Log_exp : forall (x:R),