Skip to content
GitLab
Commit 404a9dd8 authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Update Coq realizations.

parent 648ecbd5
Hide whitespace changes
Inline Side-by-side
lib/coq/floating_point/Double.v
View file @ 404a9dd8
......@@ -39,15 +39,15 @@ exact (model 53 1024).
Defined.
(* Why3 assumption *)
Definition round_error(x:floating_point.DoubleFormat.double): R :=
Definition round_error (x:floating_point.DoubleFormat.double): R :=
(Rabs ((value x) - (exact x))%R).
(* Why3 assumption *)
Definition total_error(x:floating_point.DoubleFormat.double): R :=
Definition total_error (x:floating_point.DoubleFormat.double): R :=
(Rabs ((value x) - (model x))%R).
(* Why3 assumption *)
Definition no_overflow(m:floating_point.Rounding.mode) (x:R): Prop :=
Definition no_overflow (m:floating_point.Rounding.mode) (x:R): Prop :=
((Rabs (round m
x)) <= (9007199254740991 * 19958403095347198116563727130368385660674512604354575415025472424372118918689640657849579654926357010893424468441924952439724379883935936607391717982848314203200056729510856765175377214443629871826533567445439239933308104551208703888888552684480441575071209068757560416423584952303440099278848)%R)%R.
......@@ -118,12 +118,12 @@ now apply Round_up_neg.
Qed.
(* Why3 assumption *)
Definition of_real_post(m:floating_point.Rounding.mode) (x:R)
Definition of_real_post (m:floating_point.Rounding.mode) (x:R)
(res:floating_point.DoubleFormat.double): Prop := ((value res) = (round m
x)) /\ (((exact res) = x) /\ ((model res) = x)).
(* Why3 assumption *)
Definition add_post(m:floating_point.Rounding.mode)
Definition add_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
......@@ -132,7 +132,7 @@ Definition add_post(m:floating_point.Rounding.mode)
((model res) = ((model x) + (model y))%R)).
(* Why3 assumption *)
Definition sub_post(m:floating_point.Rounding.mode)
Definition sub_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
......@@ -141,7 +141,7 @@ Definition sub_post(m:floating_point.Rounding.mode)
((model res) = ((model x) - (model y))%R)).
(* Why3 assumption *)
Definition mul_post(m:floating_point.Rounding.mode)
Definition mul_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
......@@ -150,7 +150,7 @@ Definition mul_post(m:floating_point.Rounding.mode)
((model res) = ((model x) * (model y))%R)).
(* Why3 assumption *)
Definition div_post(m:floating_point.Rounding.mode)
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
......@@ -159,17 +159,17 @@ Definition div_post(m:floating_point.Rounding.mode)
((model res) = (Rdiv (model x) (model y))%R)).
(* Why3 assumption *)
Definition neg_post(x:floating_point.DoubleFormat.double)
Definition neg_post (x:floating_point.DoubleFormat.double)
(res:floating_point.DoubleFormat.double): Prop :=
((value res) = (-(value x))%R) /\ (((exact res) = (-(exact x))%R) /\
((model res) = (-(model x))%R)).
(* Why3 assumption *)
Definition lt(x:floating_point.DoubleFormat.double)
Definition lt (x:floating_point.DoubleFormat.double)
(y:floating_point.DoubleFormat.double): Prop := ((value x) < (value y))%R.
(* Why3 assumption *)
Definition gt(x:floating_point.DoubleFormat.double)
Definition gt (x:floating_point.DoubleFormat.double)
(y:floating_point.DoubleFormat.double): Prop := ((value y) < (value x))%R.
lib/coq/floating_point/Rounding.v
View file @ 404a9dd8
......@@ -4,12 +4,12 @@ Require Import BuiltIn.
Require BuiltIn.
(* Why3 assumption *)
Inductive mode :=
| NearestTiesToEven : mode
| ToZero : mode
| Up : mode
| Down : mode
| NearestTiesToAway : mode .
Inductive mode :=
| NearestTiesToEven : mode
| ToZero : mode
| Up : mode
| Down : mode
| NearestTiesToAway : mode.
Axiom mode_WhyType : WhyType mode.
Existing Instance mode_WhyType.
......
lib/coq/floating_point/Single.v
View file @ 404a9dd8
......@@ -39,15 +39,15 @@ exact (model 24 128).
Defined.
(* Why3 assumption *)
Definition round_error(x:floating_point.SingleFormat.single): R :=
Definition round_error (x:floating_point.SingleFormat.single): R :=
(Rabs ((value x) - (exact x))%R).
(* Why3 assumption *)
Definition total_error(x:floating_point.SingleFormat.single): R :=
Definition total_error (x:floating_point.SingleFormat.single): R :=
(Rabs ((value x) - (model x))%R).
(* Why3 assumption *)
Definition no_overflow(m:floating_point.Rounding.mode) (x:R): Prop :=
Definition no_overflow (m:floating_point.Rounding.mode) (x:R): Prop :=
((Rabs (round m x)) <= (33554430 * 10141204801825835211973625643008)%R)%R.
Lemma max_single_eq: (33554430 * 10141204801825835211973625643008 = max 24 128)%R.
......@@ -126,12 +126,12 @@ now apply Round_up_neg.
Qed.
(* Why3 assumption *)
Definition of_real_post(m:floating_point.Rounding.mode) (x:R)
Definition of_real_post (m:floating_point.Rounding.mode) (x:R)
(res:floating_point.SingleFormat.single): Prop := ((value res) = (round m
x)) /\ (((exact res) = x) /\ ((model res) = x)).
(* Why3 assumption *)
Definition add_post(m:floating_point.Rounding.mode)
Definition add_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
......@@ -140,7 +140,7 @@ Definition add_post(m:floating_point.Rounding.mode)
((model res) = ((model x) + (model y))%R)).
(* Why3 assumption *)
Definition sub_post(m:floating_point.Rounding.mode)
Definition sub_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
......@@ -149,7 +149,7 @@ Definition sub_post(m:floating_point.Rounding.mode)
((model res) = ((model x) - (model y))%R)).
(* Why3 assumption *)
Definition mul_post(m:floating_point.Rounding.mode)
Definition mul_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
......@@ -158,7 +158,7 @@ Definition mul_post(m:floating_point.Rounding.mode)
((model res) = ((model x) * (model y))%R)).
(* Why3 assumption *)
Definition div_post(m:floating_point.Rounding.mode)
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
......@@ -167,17 +167,17 @@ Definition div_post(m:floating_point.Rounding.mode)
((model res) = (Rdiv (model x) (model y))%R)).
(* Why3 assumption *)
Definition neg_post(x:floating_point.SingleFormat.single)
Definition neg_post (x:floating_point.SingleFormat.single)
(res:floating_point.SingleFormat.single): Prop :=
((value res) = (-(value x))%R) /\ (((exact res) = (-(exact x))%R) /\
((model res) = (-(model x))%R)).
(* Why3 assumption *)
Definition lt(x:floating_point.SingleFormat.single)
Definition lt (x:floating_point.SingleFormat.single)
(y:floating_point.SingleFormat.single): Prop := ((value x) < (value y))%R.
(* Why3 assumption *)
Definition gt(x:floating_point.SingleFormat.single)
Definition gt (x:floating_point.SingleFormat.single)
(y:floating_point.SingleFormat.single): Prop := ((value y) < (value x))%R.
lib/coq/map/MapPermut.v
View file @ 404a9dd8
......@@ -6,7 +6,7 @@ Require int.Int.
Require map.Map.
(* Why3 assumption *)
Definition exchange {a:Type} {a_WT:WhyType a}(a1:(map.Map.map Z a))
Definition exchange {a:Type} {a_WT:WhyType a} (a1:(map.Map.map Z a))
(a2:(map.Map.map Z a)) (i:Z) (j:Z): Prop := ((map.Map.get a1
i) = (map.Map.get a2 j)) /\ (((map.Map.get a2 i) = (map.Map.get a1 j)) /\
forall (k:Z), ((~ (k = i)) /\ ~ (k = j)) -> ((map.Map.get a1
......
lib/coq/number/Divisibility.v
View file @ 404a9dd8
......@@ -12,7 +12,7 @@ Require number.Parity.
(* Hack so that Why3 does not override the notation below.
(* Why3 assumption *)
Definition divides(d:Z) (n:Z): Prop := exists q:Z, (n = (q * d)%Z).
Definition divides (d:Z) (n:Z): Prop := exists q:Z, (n = (q * d)%Z).
*)
......@@ -38,15 +38,15 @@ exact Zdivide_0.
Qed.
(* Why3 goal *)
Lemma divides_left : forall (a:Z) (b:Z) (c:Z), (divides a b) ->
(divides (c * a)%Z (c * b)%Z).
Lemma divides_left : forall (a:Z) (b:Z) (c:Z), (divides a b) -> (divides
(c * a)%Z (c * b)%Z).
Proof.
exact Zmult_divide_compat_l.
Qed.
(* Why3 goal *)
Lemma divides_right : forall (a:Z) (b:Z) (c:Z), (divides a b) ->
(divides (a * c)%Z (b * c)%Z).
Lemma divides_right : forall (a:Z) (b:Z) (c:Z), (divides a b) -> (divides
(a * c)%Z (b * c)%Z).
Proof.
exact Zmult_divide_compat_r.
Qed.
......@@ -160,8 +160,8 @@ ring.
Qed.
(* Why3 goal *)
Lemma divides_mod_euclidean : forall (a:Z) (b:Z), (~ (b = 0%Z)) ->
((divides b a) -> ((int.EuclideanDivision.mod1 a b) = 0%Z)).
Lemma divides_mod_euclidean : forall (a:Z) (b:Z), (~ (b = 0%Z)) -> ((divides
b a) -> ((int.EuclideanDivision.mod1 a b) = 0%Z)).
Proof.
intros a b Zb H.
assert (Zmod a b = Z0).
......
lib/coq/number/Parity.v
View file @ 404a9dd8
......@@ -5,10 +5,10 @@ Require BuiltIn.
Require int.Int.
(* Why3 assumption *)
Definition even(n:Z): Prop := exists k:Z, (n = (2%Z * k)%Z).
Definition even (n:Z): Prop := exists k:Z, (n = (2%Z * k)%Z).
(* Why3 assumption *)
Definition odd(n:Z): Prop := exists k:Z, (n = ((2%Z * k)%Z + 1%Z)%Z).
Definition odd (n:Z): Prop := exists k:Z, (n = ((2%Z * k)%Z + 1%Z)%Z).
Lemma even_is_Zeven :
forall n, even n <-> Zeven n.
......
lib/coq/number/Prime.v
View file @ 404a9dd8
......@@ -13,7 +13,7 @@ Require number.Divisibility.
Import Znumtheory.
(* Why3 assumption *)
Definition prime(p:Z): Prop := (2%Z <= p)%Z /\ forall (n:Z), ((1%Z < n)%Z /\
Definition prime (p:Z): Prop := (2%Z <= p)%Z /\ forall (n:Z), ((1%Z < n)%Z /\
(n < p)%Z) -> ~ (number.Divisibility.divides n p).
Lemma prime_is_Zprime :
......@@ -58,8 +58,8 @@ Qed.
(* Why3 goal *)
Lemma small_divisors : forall (p:Z), (2%Z <= p)%Z -> ((forall (d:Z),
(2%Z <= d)%Z -> ((prime d) -> (((1%Z < (d * d)%Z)%Z /\
((d * d)%Z <= p)%Z) -> ~ (number.Divisibility.divides d p)))) ->
(prime p)).
((d * d)%Z <= p)%Z) -> ~ (number.Divisibility.divides d p)))) -> (prime
p)).
Proof.
intros p Hp H.
apply <- prime_is_Zprime.
......
lib/coq/real/ExpLog.v
View file @ 404a9dd8
......@@ -48,9 +48,9 @@ exact exp_ln.
Qed.
(* Why3 assumption *)
Definition log2(x:R): R := (Rdiv (ln x) (ln 2%R))%R.
Definition log2 (x:R): R := (Rdiv (ln x) (ln 2%R))%R.
(* Why3 assumption *)
Definition log10(x:R): R := (Rdiv (ln x) (ln 10%R))%R.
Definition log10 (x:R): R := (Rdiv (ln x) (ln 10%R))%R.
lib/coq/set/Set.v
View file @ 404a9dd8
......@@ -35,7 +35,7 @@ Defined.
Hint Unfold mem.
(* Why3 assumption *)
Definition infix_eqeq {a:Type} {a_WT:WhyType a}(s1:(set a)) (s2:(set
Definition infix_eqeq {a:Type} {a_WT:WhyType a} (s1:(set a)) (s2:(set
a)): Prop := forall (x:a), (mem x s1) <-> (mem x s2).
Notation "x == y" := (infix_eqeq x y) (at level 70, no associativity).
......@@ -50,8 +50,8 @@ apply h1.
Qed.
(* Why3 assumption *)
Definition subset {a:Type} {a_WT:WhyType a}(s1:(set a)) (s2:(set a)): Prop :=
forall (x:a), (mem x s1) -> (mem x s2).
Definition subset {a:Type} {a_WT:WhyType a} (s1:(set a)) (s2:(set
a)): Prop := forall (x:a), (mem x s1) -> (mem x s2).
(* Why3 goal *)
Lemma subset_refl : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a)),
......@@ -75,7 +75,7 @@ exact (fun _ => False).
Defined.
(* Why3 assumption *)
Definition is_empty {a:Type} {a_WT:WhyType a}(s:(set a)): Prop :=
Definition is_empty {a:Type} {a_WT:WhyType a} (s:(set a)): Prop :=
forall (x:a), ~ (mem x s).
(* Why3 goal *)
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment