Commit 31c70762 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Use plain identifiers whenever possible in the Coq printer.

This patch also fully qualifies some realized types and constructors to
avoid inadvertent shadowing.
parent 80fbe713
......@@ -19,31 +19,31 @@ theory BuiltIn
prelude "Require Import BuiltIn."
syntax type int "Z"
syntax type real "R"
syntax type int "Numbers.BinNums.Z"
syntax type real "Reals.Rdefinitions.R"
syntax predicate (=) "(%1 = %2)"
end
theory Unit
syntax type unit "unit"
syntax type unit "Init.Datatypes.unit"
end
theory Bool
syntax type bool "bool"
syntax type bool "Init.Datatypes.bool"
syntax function True "true"
syntax function False "false"
syntax function True "Init.Datatypes.true"
syntax function False "Init.Datatypes.false"
end
theory bool.Bool
syntax function andb "(Init.Datatypes.andb %1 %2)"
syntax function orb "(Init.Datatypes.orb %1 %2)"
syntax function xorb "(Init.Datatypes.xorb %1 %2)"
syntax function notb "(Init.Datatypes.negb %1)"
syntax function implb "(Init.Datatypes.implb %1 %2)"
syntax function andb "Init.Datatypes.andb"
syntax function orb "Init.Datatypes.orb"
syntax function xorb "Init.Datatypes.xorb"
syntax function notb "Init.Datatypes.negb"
syntax function implb "Init.Datatypes.implb"
end
......@@ -87,7 +87,7 @@ end
theory int.Abs
syntax function abs "(ZArith.BinInt.Z.abs %1)"
syntax function abs "ZArith.BinInt.Z.abs"
remove prop Abs_pos
......@@ -95,8 +95,8 @@ end
theory int.MinMax
syntax function min "(ZArith.BinInt.Z.min %1 %2)"
syntax function max "(ZArith.BinInt.Z.max %1 %2)"
syntax function min "ZArith.BinInt.Z.min"
syntax function max "ZArith.BinInt.Z.max"
end
......@@ -106,8 +106,8 @@ end
theory int.EuclideanDivision
syntax function div "(ZArith.BinInt.Z.div %1 %2)"
syntax function mod "(ZArith.BinInt.Z.modulo %1 %2)"
syntax function div "ZArith.BinInt.Z.div"
syntax function mod "ZArith.BinInt.Z.modulo"
remove prop Div_mod
remove prop Div_bound
......@@ -124,8 +124,8 @@ theory int.ComputerDivision
with the same convention as mainstream programming language
such C, Java, OCaml *)
syntax function div "(ZArith.BinInt.Z.quot %1 %2)"
syntax function mod "(ZArith.BinInt.Z.rem %1 %2)"
syntax function div "ZArith.BinInt.Z.quot"
syntax function mod "ZArith.BinInt.Z.rem"
remove prop Div_mod
remove prop Div_bound
......@@ -155,7 +155,7 @@ theory real.Real
syntax function (-_) "(-%1)%R"
syntax function (*) "(%1 * %2)%R"
syntax function (/) "(%1 / %2)%R"
syntax function inv "(Reals.Rdefinitions.Rinv %1)"
syntax function inv "(/ %1)%R"
syntax predicate (<=) "(%1 <= %2)%R"
syntax predicate (<) "(%1 < %2)%R"
......@@ -207,7 +207,7 @@ theory real.Abs
prelude "Require Reals.Rbasic_fun."
syntax function abs "(Reals.Rbasic_fun.Rabs %1)"
syntax function abs "Reals.Rbasic_fun.Rabs"
remove prop Abs_le
remove prop Abs_pos
......@@ -216,14 +216,14 @@ end
theory real.MinMax
syntax function min "(Reals.Rbasic_fun.Rmin %1 %2)"
syntax function max "(Reals.Rbasic_fun.Rmax %1 %2)"
syntax function min "Reals.Rbasic_fun.Rmin"
syntax function max "Reals.Rbasic_fun.Rmax"
end
theory real.FromInt
syntax function from_int "(BuiltIn.IZR %1)"
syntax function from_int "BuiltIn.IZR"
remove prop Zero
remove prop One
......@@ -238,8 +238,8 @@ theory real.Square
prelude "Require Reals.R_sqrt."
syntax function sqr "(Reals.RIneq.Rsqr %1)"
syntax function sqrt "(Reals.R_sqrt.sqrt %1)" (* and not Rsqrt *)
syntax function sqr "Reals.RIneq.Rsqr"
syntax function sqrt "Reals.R_sqrt.sqrt" (* and not Rsqrt *)
remove prop Sqrt_positive
remove prop Sqrt_square
......@@ -252,8 +252,8 @@ theory real.ExpLog
prelude "Require Reals.Rtrigo_def."
prelude "Require Reals.Rpower."
syntax function exp "(Reals.Rtrigo_def.exp %1)"
syntax function log "(Reals.Rpower.ln %1)"
syntax function exp "Reals.Rtrigo_def.exp"
syntax function log "Reals.Rpower.ln"
remove prop Exp_zero
remove prop Exp_sum
......@@ -268,7 +268,7 @@ theory real.PowerInt
prelude "Require Reals.Rfunctions."
syntax function power "(Reals.Rfunctions.powerRZ %1 %2)"
syntax function power "Reals.Rfunctions.powerRZ"
remove prop Power_0 (* already as powerRZ_O *)
(* remove prop Power_s *)
......@@ -280,7 +280,7 @@ end
theory real.PowerReal
syntax function pow "(Reals.Rpower.Rpower %1 %2)"
syntax function pow "Reals.Rpower.Rpower"
end
......@@ -290,14 +290,14 @@ theory real.Trigonometry
prelude "Require Reals.Rtrigo1."
prelude "Require Reals.Ratan."
syntax function cos "(Reals.Rtrigo_def.cos %1)"
syntax function sin "(Reals.Rtrigo_def.sin %1)"
syntax function cos "Reals.Rtrigo_def.cos"
syntax function sin "Reals.Rtrigo_def.sin"
syntax function pi "Reals.Rtrigo1.PI"
syntax function tan "(Reals.Rtrigo1.tan %1)"
syntax function tan "Reals.Rtrigo1.tan"
syntax function atan "(Reals.Ratan.atan %1)"
syntax function atan "Reals.Ratan.atan"
remove prop Pythagorean_identity
remove prop Cos_le_one
......@@ -313,41 +313,41 @@ end
theory list.List
syntax type list "(list %1)"
syntax type list "Init.Datatypes.list"
syntax function Nil "Init.Datatypes.nil"
syntax function Cons "(Init.Datatypes.cons %1 %2)"
syntax function Cons "Init.Datatypes.cons"
end
theory list.Append
syntax function (++) "(Init.Datatypes.app %1 %2)"
syntax function (++) "Init.Datatypes.app"
end
theory list.Reverse
syntax function reverse "(Lists.List.rev %1)"
syntax function reverse "Lists.List.rev"
end
theory list.RevAppend
syntax function rev_append "(Lists.List.rev_append %1 %2)"
syntax function rev_append "Lists.List.rev_append"
end
theory list.Combine
syntax function combine "(Lists.List.combine %1 %2)"
syntax function combine "Lists.List.combine"
end
theory option.Option
syntax type option "(option %1)"
syntax type option "Init.Datatypes.option"
syntax function None "Init.Datatypes.None"
syntax function Some "(Init.Datatypes.Some %1)"
syntax function Some "Init.Datatypes.Some"
end
......
......@@ -16,11 +16,12 @@ Require BuiltIn.
(* Why3 goal *)
Lemma andb_def :
forall (x:bool) (y:bool),
((Init.Datatypes.andb x y) = match x with
| true => y
| false => false
end).
forall (x:Init.Datatypes.bool) (y:Init.Datatypes.bool),
((Init.Datatypes.andb x y) =
match x with
| Init.Datatypes.true => y
| Init.Datatypes.false => Init.Datatypes.false
end).
Proof.
intros x y.
apply refl_equal.
......@@ -28,11 +29,12 @@ Qed.
(* Why3 goal *)
Lemma orb_def :
forall (x:bool) (y:bool),
((Init.Datatypes.orb x y) = match x with
| false => y
| true => true
end).
forall (x:Init.Datatypes.bool) (y:Init.Datatypes.bool),
((Init.Datatypes.orb x y) =
match x with
| Init.Datatypes.false => y
| Init.Datatypes.true => Init.Datatypes.true
end).
Proof.
intros x y.
apply refl_equal.
......@@ -40,11 +42,12 @@ Qed.
(* Why3 goal *)
Lemma notb_def :
forall (x:bool),
((Init.Datatypes.negb x) = match x with
| false => true
| true => false
end).
forall (x:Init.Datatypes.bool),
((Init.Datatypes.negb x) =
match x with
| Init.Datatypes.false => Init.Datatypes.true
| Init.Datatypes.true => Init.Datatypes.false
end).
Proof.
intros x.
apply refl_equal.
......@@ -52,11 +55,11 @@ Qed.
(* Why3 goal *)
Lemma xorb_def :
forall (x:bool) (y:bool),
forall (x:Init.Datatypes.bool) (y:Init.Datatypes.bool),
((Init.Datatypes.xorb x y) =
match x with
| false => y
| true => (Init.Datatypes.negb y)
| Init.Datatypes.false => y
| Init.Datatypes.true => Init.Datatypes.negb y
end).
Proof.
intros x y.
......@@ -65,11 +68,12 @@ Qed.
(* Why3 goal *)
Lemma implb_def :
forall (x:bool) (y:bool),
((Init.Datatypes.implb x y) = match x with
| false => true
| true => y
end).
forall (x:Init.Datatypes.bool) (y:Init.Datatypes.bool),
((Init.Datatypes.implb x y) =
match x with
| Init.Datatypes.false => Init.Datatypes.true
| Init.Datatypes.true => y
end).
Proof.
now intros [|] [|].
Qed.
......
......@@ -27,7 +27,7 @@ Local Parameter last_bit : nat.
Definition size_nat: nat := S last_bit.
(* Why3 goal *)
Definition size : Z.
Definition size : Numbers.BinNums.Z.
exact (Z.of_nat size_nat).
Defined.
......@@ -189,7 +189,7 @@ Qed.
(* end of nth helpers *)
(* Why3 goal *)
Definition nth : t -> Z -> bool.
Definition nth : t -> Numbers.BinNums.Z -> Init.Datatypes.bool.
exact nth_aux.
Defined.
......@@ -213,7 +213,8 @@ Qed.
(* Why3 goal *)
Lemma nth_out_of_bound :
forall (x:t) (n:Z), (n < 0%Z)%Z \/ (size <= n)%Z -> ((nth x n) = false).
forall (x:t) (n:Numbers.BinNums.Z), (n < 0%Z)%Z \/ (size <= n)%Z ->
((nth x n) = Init.Datatypes.false).
intros.
unfold nth.
rewrite nth_aux_out_of_bound; auto with zarith.
......@@ -236,7 +237,8 @@ Lemma Nth_zeros_aux : forall {l} (n:Z), ((@nth_aux l zeros_aux n) = false).
Qed.
(* Why3 goal *)
Lemma Nth_zeros : forall (n:Z), ((nth zeros n) = false).
Lemma Nth_zeros :
forall (n:Numbers.BinNums.Z), ((nth zeros n) = Init.Datatypes.false).
intros n; apply Nth_zeros_aux.
Qed.
......@@ -260,7 +262,8 @@ Defined.
(* Why3 goal *)
Lemma Nth_ones :
forall (n:Z), (0%Z <= n)%Z /\ (n < size)%Z -> ((nth ones n) = true).
forall (n:Numbers.BinNums.Z), (0%Z <= n)%Z /\ (n < size)%Z ->
((nth ones n) = Init.Datatypes.true).
intros; apply nth_const; easy.
Qed.
......@@ -271,7 +274,7 @@ Defined.
(* Why3 goal *)
Lemma Nth_bw_and :
forall (v1:t) (v2:t) (n:Z), (0%Z <= n)%Z /\ (n < size)%Z ->
forall (v1:t) (v2:t) (n:Numbers.BinNums.Z), (0%Z <= n)%Z /\ (n < size)%Z ->
((nth (bw_and v1 v2) n) = (Init.Datatypes.andb (nth v1 n) (nth v2 n))).
symmetry.
apply nth_aux_map2 with (f := fun x y => x && y); easy.
......@@ -284,7 +287,7 @@ Defined.
(* Why3 goal *)
Lemma Nth_bw_or :
forall (v1:t) (v2:t) (n:Z), (0%Z <= n)%Z /\ (n < size)%Z ->
forall (v1:t) (v2:t) (n:Numbers.BinNums.Z), (0%Z <= n)%Z /\ (n < size)%Z ->
((nth (bw_or v1 v2) n) = (Init.Datatypes.orb (nth v1 n) (nth v2 n))).
symmetry.
apply nth_aux_map2; easy.
......@@ -297,7 +300,7 @@ Defined.
(* Why3 goal *)
Lemma Nth_bw_xor :
forall (v1:t) (v2:t) (n:Z), (0%Z <= n)%Z /\ (n < size)%Z ->
forall (v1:t) (v2:t) (n:Numbers.BinNums.Z), (0%Z <= n)%Z /\ (n < size)%Z ->
((nth (bw_xor v1 v2) n) = (Init.Datatypes.xorb (nth v1 n) (nth v2 n))).
symmetry.
apply nth_aux_map2; easy.
......@@ -310,14 +313,14 @@ Defined.
(* Why3 goal *)
Lemma Nth_bw_not :
forall (v:t) (n:Z), (0%Z <= n)%Z /\ (n < size)%Z ->
forall (v:t) (n:Numbers.BinNums.Z), (0%Z <= n)%Z /\ (n < size)%Z ->
((nth (bw_not v) n) = (Init.Datatypes.negb (nth v n))).
symmetry.
apply nth_aux_map; easy.
Qed.
(* Why3 goal *)
Definition lsr : t -> Z -> t.
Definition lsr : t -> Numbers.BinNums.Z -> t.
exact (fun v m => BshiftRl_iter last_bit v (Z.to_nat m)).
Defined.
......@@ -339,8 +342,9 @@ Qed.
(* Why3 goal *)
Lemma Lsr_nth_low :
forall (b:t) (n:Z) (s:Z), (0%Z <= s)%Z -> (0%Z <= n)%Z ->
((n + s)%Z < size)%Z -> ((nth (lsr b s) n) = (nth b (n + s)%Z)).
forall (b:t) (n:Numbers.BinNums.Z) (s:Numbers.BinNums.Z), (0%Z <= s)%Z ->
(0%Z <= n)%Z -> ((n + s)%Z < size)%Z ->
((nth (lsr b s) n) = (nth b (n + s)%Z)).
intros b n s h1 h2 h3.
rewrite <-Z2Nat.id with (n := s) at 2; auto.
apply bshiftRl_iter_nth; omega.
......@@ -348,8 +352,9 @@ Qed.
(* Why3 goal *)
Lemma Lsr_nth_high :
forall (b:t) (n:Z) (s:Z), (0%Z <= s)%Z -> (0%Z <= n)%Z ->
(size <= (n + s)%Z)%Z -> ((nth (lsr b s) n) = false).
forall (b:t) (n:Numbers.BinNums.Z) (s:Numbers.BinNums.Z), (0%Z <= s)%Z ->
(0%Z <= n)%Z -> (size <= (n + s)%Z)%Z ->
((nth (lsr b s) n) = Init.Datatypes.false).
intros b n s h1 h2 h3.
unfold nth,lsr.
cut (nth_aux b (n + Z.of_nat (Z.to_nat s)) = false).
......@@ -366,7 +371,7 @@ auto.
Qed.
(* Why3 goal *)
Definition asr : t -> Z -> t.
Definition asr : t -> Numbers.BinNums.Z -> t.
exact (fun v m => BshiftRa_iter last_bit v (Z.to_nat m)).
Defined.
......@@ -443,8 +448,9 @@ Qed.
(* Why3 goal *)
Lemma Asr_nth_low :
forall (b:t) (n:Z) (s:Z), (0%Z <= s)%Z -> (0%Z <= n)%Z /\ (n < size)%Z ->
((n + s)%Z < size)%Z -> ((nth (asr b s) n) = (nth b (n + s)%Z)).
forall (b:t) (n:Numbers.BinNums.Z) (s:Numbers.BinNums.Z), (0%Z <= s)%Z ->
(0%Z <= n)%Z /\ (n < size)%Z -> ((n + s)%Z < size)%Z ->
((nth (asr b s) n) = (nth b (n + s)%Z)).
unfold nth, lsr.
intros.
assert ((n + s)%Z = (n + Z.of_nat (Z.to_nat s))%Z).
......@@ -489,8 +495,9 @@ Qed.
(* Why3 goal *)
Lemma Asr_nth_high :
forall (b:t) (n:Z) (s:Z), (0%Z <= s)%Z -> (0%Z <= n)%Z /\ (n < size)%Z ->
(size <= (n + s)%Z)%Z -> ((nth (asr b s) n) = (nth b (size - 1%Z)%Z)).
forall (b:t) (n:Numbers.BinNums.Z) (s:Numbers.BinNums.Z), (0%Z <= s)%Z ->
(0%Z <= n)%Z /\ (n < size)%Z -> (size <= (n + s)%Z)%Z ->
((nth (asr b s) n) = (nth b (size - 1%Z)%Z)).
unfold nth, asr.
intros.
apply BhiftRa_iter_nth_high.
......@@ -504,7 +511,7 @@ auto.
Qed.
(* Why3 goal *)
Definition lsl : t -> Z -> t.
Definition lsl : t -> Numbers.BinNums.Z -> t.
exact (fun v m => BshiftL_iter last_bit v (Z.to_nat m)).
Defined.
......@@ -526,7 +533,8 @@ Qed.
(* Why3 goal *)
Lemma Lsl_nth_high :
forall (b:t) (n:Z) (s:Z), (0%Z <= s)%Z /\ (s <= n)%Z /\ (n < size)%Z ->
forall (b:t) (n:Numbers.BinNums.Z) (s:Numbers.BinNums.Z),
(0%Z <= s)%Z /\ (s <= n)%Z /\ (n < size)%Z ->
((nth (lsl b s) n) = (nth b (n - s)%Z)).
intros.
unfold lsl, nth.
......@@ -556,8 +564,8 @@ Qed.
(* Why3 goal *)
Lemma Lsl_nth_low :
forall (b:t) (n:Z) (s:Z), (0%Z <= n)%Z /\ (n < s)%Z ->
((nth (lsl b s) n) = false).
forall (b:t) (n:Numbers.BinNums.Z) (s:Numbers.BinNums.Z),
(0%Z <= n)%Z /\ (n < s)%Z -> ((nth (lsl b s) n) = Init.Datatypes.false).
intros.
apply Lsl_nth_low_aux.
rewrite Z2Nat.id; omega.
......@@ -1091,13 +1099,14 @@ Lemma bvec_to_nat_shiftout_mod1 : forall {l} v, Z.of_nat (bvec_to_nat l (Vector.
Qed.
(* Why3 goal *)
Definition rotate_right : t -> Z -> t.
Definition rotate_right : t -> Numbers.BinNums.Z -> t.
exact (fun b p => rotate_right_aux b (Z.to_nat p)).
Defined.
(* Why3 goal *)
Lemma Nth_rotate_right :
forall (v:t) (n:Z) (i:Z), (0%Z <= i)%Z /\ (i < size)%Z -> (0%Z <= n)%Z ->
forall (v:t) (n:Numbers.BinNums.Z) (i:Numbers.BinNums.Z),
(0%Z <= i)%Z /\ (i < size)%Z -> (0%Z <= n)%Z ->
((nth (rotate_right v n) i) =
(nth v (int.EuclideanDivision.mod1 (i + n)%Z size))).
intros v n i h1 h2.
......@@ -1115,13 +1124,14 @@ Lemma Nth_rotate_right :
Qed.
(* Why3 goal *)
Definition rotate_left : t -> Z -> t.
Definition rotate_left : t -> Numbers.BinNums.Z -> t.
exact (fun b p => rotate_left_aux b (Z.to_nat p)).
Defined.
(* Why3 goal *)
Lemma Nth_rotate_left :
forall (v:t) (n:Z) (i:Z), (0%Z <= i)%Z /\ (i < size)%Z -> (0%Z <= n)%Z ->
forall (v:t) (n:Numbers.BinNums.Z) (i:Numbers.BinNums.Z),
(0%Z <= i)%Z /\ (i < size)%Z -> (0%Z <= n)%Z ->
((nth (rotate_left v n) i) =
(nth v (int.EuclideanDivision.mod1 (i - n)%Z size))).
intros v n i h1 h2.
......@@ -1139,12 +1149,12 @@ Lemma Nth_rotate_left :
Qed.
(* Why3 goal *)
Definition two_power_size : Z.
Definition two_power_size : Numbers.BinNums.Z.
exact (Pow2int.pow2 size)%Z.
Defined.
(* Why3 goal *)
Definition max_int : Z.
Definition max_int : Numbers.BinNums.Z.
exact (Pow2int.pow2 size - 1)%Z.
Defined.
......@@ -1164,7 +1174,7 @@ Definition is_signed_positive : t -> Prop.
Defined.
(* Why3 goal *)
Definition to_uint : t -> Z.
Definition to_uint : t -> Numbers.BinNums.Z.
exact (fun x => Z.of_nat (bvec_to_nat size_nat x)).
Defined.
......@@ -1173,12 +1183,12 @@ Lemma max_int_S : (two_power_size = max_int + 1)%Z.
Qed.
(* Why3 goal *)
Definition of_int : Z -> t.
Definition of_int : Numbers.BinNums.Z -> t.
exact (fun x => nat_to_bvec size_nat (Z.to_nat x)).
Defined.
(* Why3 goal *)
Definition to_int : t -> Z.
Definition to_int : t -> Numbers.BinNums.Z.
exact (twos_complement size_nat).
Defined.
......@@ -1223,7 +1233,8 @@ Lemma to_int_extensionality :
Qed.
(* Why3 assumption *)
Definition uint_in_range (i:Z) : Prop := (0%Z <= i)%Z /\ (i <= max_int)%Z.
Definition uint_in_range (i:Numbers.BinNums.Z) : Prop :=
(0%Z <= i)%Z /\ (i <= max_int)%Z.
(* Why3 goal *)
Lemma to_uint_bounds :
......@@ -1332,7 +1343,7 @@ Qed.
(* Why3 goal *)
Lemma to_uint_of_int :
forall (i:Z), (0%Z <= i)%Z /\ (i < two_power_size)%Z ->
forall (i:Numbers.BinNums.Z), (0%Z <= i)%Z /\ (i < two_power_size)%Z ->
((to_uint (of_int i)) = i).
intros i h1; destruct h1.
unfold to_uint, of_int.
......@@ -1674,7 +1685,7 @@ trivial.
Qed.
(* Why3 goal *)
Definition nth_bv : t -> t -> bool.
Definition nth_bv : t -> t -> Init.Datatypes.bool.
exact (fun v w => nth v (to_uint w)).
Defined.
......@@ -1706,7 +1717,8 @@ Qed.
(* Why3 goal *)
Lemma nth_bv_def :
forall (x:t) (i:t),
((nth_bv x i) = true) <-> ~ ((bw_and (lsr_bv x i) one) = zeros).
((nth_bv x i) = Init.Datatypes.true) <->
~ ((bw_and (lsr_bv x i) one) = zeros).
intros; unfold nth_bv.
case (Z_lt_ge_dec (to_uint i) size); intro.
rewrite <-(Zplus_0_l (to_uint i)).
......@@ -1745,7 +1757,8 @@ Qed.
(* Why3 goal *)
Lemma Nth_bv_is_nth2 :
forall (x:t) (i:Z), (0%Z <= i)%Z /\ (i < two_power_size)%Z ->
forall (x:t) (i:Numbers.BinNums.Z),
(0%Z <= i)%Z /\ (i < two_power_size)%Z ->
((nth_bv x (of_int i)) = (nth x i)).
intros x i h1.
rewrite <-Nth_bv_is_nth.
......@@ -1770,8 +1783,10 @@ Lemma eq_sub_bv_def :
Qed.
(* Why3 assumption *)
Definition eq_sub (a:t) (b:t) (i:Z) (n:Z) : Prop :=
forall (j:Z), (i <= j)%Z /\ (j < (i + n)%Z)%Z -> ((nth a j) = (nth b j)).
Definition eq_sub (a:t) (b:t) (i:Numbers.BinNums.Z) (n:Numbers.BinNums.Z) :
Prop :=
forall (j:Numbers.BinNums.Z), (i <= j)%Z /\ (j < (i + n)%Z)%Z ->
((nth a j) = (nth b j)).
Lemma in_range_1 : uint_in_range 1.
split; auto with zarith.
......
......@@ -16,7 +16,7 @@ Require BuiltIn.
Require int.Int.
(* Why3 goal *)
Definition pow2 : Z -> Z.
Definition pow2 : Numbers.BinNums.Z -> Numbers.BinNums.Z.
exact (two_p).
Defined.
......@@ -27,7 +27,8 @@ Qed.
(* Why3 goal *)
Lemma Power_s :
forall (n:Z), (0%Z <= n)%Z -> ((pow2 (n + 1%Z)%Z) = (2%Z * (pow2 n))%Z).
forall (n:Numbers.BinNums.Z), (0%Z <= n)%Z ->
((pow2 (n + 1%Z)%Z) = (2%Z * (pow2 n))%Z).
apply two_p_S.
Qed.
......@@ -38,7 +39,8 @@ Qed.
(* Why3 goal *)
Lemma Power_sum :
forall (n:Z) (m:Z), (0%Z <= n)%Z /\ (0%Z <= m)%Z ->
forall (n:Numbers.BinNums.Z) (m:Numbers.BinNums.Z),
(0%Z <= n)%Z /\ (0%Z <= m)%Z ->
((pow2 (n + m)%Z) = ((pow2 n) * (pow2 m))%Z).
unfold pow2.
intros n m [H1 H2].
......@@ -46,7 +48,8 @@ Lemma Power_sum :
Qed.
(* Why3 goal *)
Lemma pow2pos : forall (i:Z), (0%Z <= i)%Z -> (0%Z < (pow2 i))%Z.
Lemma pow2pos :
forall (i:Numbers.BinNums.Z), (0%Z <= i)%Z -> (0%Z < (pow2 i))%Z.
intros i h1.
Require Import Zorder.
apply Zgt_lt.
......
......@@ -24,41 +24,49 @@ Require floating_point.DoubleFormat.
Require Import floating_point.GenFloat.
(* Why3 goal *)
Definition round : floating_point.Rounding.mode -> R -> R.
Definition round :
floating_point.Rounding.mode -> Reals.Rdefinitions.R ->
Reals.Rdefinitions.R.
exact (round 53 1024).
Defined.
(* Why3 goal *)
Definition value : floating_point.DoubleFormat.double -> R.
Definition value :
floating_point.DoubleFormat.double -> Reals.Rdefinitions.R.
exact (value 53 1024).
Defined.
(* Why3 goal *)
Definition exact : floating_point.DoubleFormat.double -> R.
Definition exact :
floating_point.DoubleFormat.double -> Reals.Rdefinitions.R.
exact (exact 53 1024).
Defined.
(* Why3 goal *)
Definition model : floating_point.DoubleFormat.double -> R.
Definition model :
floating_point.DoubleFormat.double -> Reals.Rdefinitions.R.
exact (model 53 1024).
Defined.
(* Why3 assumption *)
Definition round_error (x:floating_point.DoubleFormat.double) : R :=
(Reals.Rbasic_fun.Rabs ((value x) - (exact x))%R).
Definition round_error (x:floating_point.DoubleFormat.double) :
Reals.Rdefinitions.R :=
Reals.Rbasic_fun.Rabs ((value x) - (exact x))%R.
(* Why3 assumption *)
Definition total_error (x:floating_point.DoubleFormat.double) : R :=
(Reals.Rbasic_fun.Rabs ((value x) - (model x))%R).
Definition total_error (x:floating_point.DoubleFormat.double) :
Reals.Rdefinitions.R :=
Reals.Rbasic_fun.Rabs ((value x) - (model x))%R.