Commit c320a5f6 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Move the Coq printer to a precedence-based system.

This removes lots of superfluous parentheses in the outer terms.
parent 9e6f268f
......@@ -213,7 +213,7 @@ 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:Z), (n < 0%Z)%Z \/ (size <= n)%Z -> ((nth x n) = false).
intros.
unfold nth.
rewrite nth_aux_out_of_bound; auto with zarith.
......@@ -260,7 +260,7 @@ Defined.
(* Why3 goal *)
Lemma Nth_ones :
forall (n:Z), ((0%Z <= n)%Z /\ (n < size)%Z) -> ((nth ones n) = true).
forall (n:Z), (0%Z <= n)%Z /\ (n < size)%Z -> ((nth ones n) = true).
intros; apply nth_const; easy.
Qed.
......@@ -271,7 +271,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: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 +284,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: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 +297,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: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,7 +310,7 @@ Defined.
(* Why3 goal *)
Lemma Nth_bw_not :
forall (v:t) (n:Z), ((0%Z <= n)%Z /\ (n < size)%Z) ->
forall (v:t) (n: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.
......@@ -443,7 +443,7 @@ 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) ->
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)).
unfold nth, lsr.
intros.
......@@ -489,7 +489,7 @@ 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) ->
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)).
unfold nth, asr.
intros.
......@@ -526,7 +526,7 @@ 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:Z) (s: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,7 +556,7 @@ Qed.
(* Why3 goal *)
Lemma Lsl_nth_low :
forall (b:t) (n:Z) (s:Z), ((0%Z <= n)%Z /\ (n < s)%Z) ->
forall (b:t) (n:Z) (s:Z), (0%Z <= n)%Z /\ (n < s)%Z ->
((nth (lsl b s) n) = false).
intros.
apply Lsl_nth_low_aux.
......@@ -1097,7 +1097,7 @@ 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:Z) (i: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.
......@@ -1121,7 +1121,7 @@ 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:Z) (i: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.
......@@ -1185,8 +1185,8 @@ Defined.
(* Why3 goal *)
Lemma to_int_def :
forall (x:t),
((is_signed_positive x) -> ((to_int x) = (to_uint x))) /\
(~ (is_signed_positive x) ->
(is_signed_positive x -> ((to_int x) = (to_uint x))) /\
(~ is_signed_positive x ->
((to_int x) = (-(two_power_size - (to_uint x))%Z)%Z)).
intros. split.
- unfold to_int, to_uint,is_signed_positive, twos_complement, size_nat.
......@@ -1332,7 +1332,7 @@ Qed.
(* Why3 goal *)
Lemma to_uint_of_int :
forall (i:Z), ((0%Z <= i)%Z /\ (i < two_power_size)%Z) ->
forall (i: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.
......@@ -1438,7 +1438,7 @@ Qed.
(* Why3 goal *)
Lemma positive_is_ge_zeros :
forall (x:t), (is_signed_positive x) <-> (sge x zeros).
forall (x:t), is_signed_positive x <-> sge x zeros.
intros.
unfold is_signed_positive, sge, to_int, twos_complement, size_nat.
rewrite zeros_sign_false. destruct Bsign.
......@@ -1502,8 +1502,8 @@ Qed.
(* Why3 goal *)
Lemma to_uint_sub_bounded :
forall (v1:t) (v2:t),
((0%Z <= ((to_uint v1) - (to_uint v2))%Z)%Z /\
(((to_uint v1) - (to_uint v2))%Z < two_power_size)%Z) ->
(0%Z <= ((to_uint v1) - (to_uint v2))%Z)%Z /\
(((to_uint v1) - (to_uint v2))%Z < two_power_size)%Z ->
((to_uint (sub v1 v2)) = ((to_uint v1) - (to_uint v2))%Z).
intros v1 v2 (h1,h2).
rewrite <-(mod1_out (to_uint v1 - to_uint v2) two_power_size) by auto.
......@@ -1745,7 +1745,7 @@ 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: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.
......@@ -1764,14 +1764,14 @@ Defined.
Lemma eq_sub_bv_def :
forall (a:t) (b:t) (i:t) (n:t),
let mask := lsl_bv (sub (lsl_bv one n) one) i in
(eq_sub_bv a b i n) <-> ((bw_and b mask) = (bw_and a mask)).
eq_sub_bv a b i n <-> ((bw_and b mask) = (bw_and a mask)).
rewrite Of_int_one.
easy.
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)).
forall (j: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.
......@@ -2096,7 +2096,7 @@ Qed.
(* Why3 goal *)
Lemma eq_sub_equiv :
forall (a:t) (b:t) (i:t) (n:t),
(eq_sub a b (to_uint i) (to_uint n)) <-> (eq_sub_bv a b i n).
eq_sub a b (to_uint i) (to_uint n) <-> eq_sub_bv a b i n.
Proof.
intros a b i n.
unfold eq_sub, eq_sub_bv.
......@@ -2135,7 +2135,7 @@ Proof.
Qed.
(* Why3 goal *)
Lemma Extensionality : forall (x:t) (y:t), (eq_sub x y 0%Z size) -> (x = y).
Lemma Extensionality : forall (x:t) (y:t), eq_sub x y 0%Z size -> (x = y).
intros x y.
apply Extensionality_aux.
Qed.
......
......@@ -38,7 +38,7 @@ Qed.
(* Why3 goal *)
Lemma Power_sum :
forall (n:Z) (m:Z), ((0%Z <= n)%Z /\ (0%Z <= m)%Z) ->
forall (n:Z) (m: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].
......
......@@ -99,7 +99,7 @@ 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) ->
((-9007199254740992%Z)%Z <= i)%Z /\ (i <= 9007199254740992%Z)%Z ->
((round m (BuiltIn.IZR i)) = (BuiltIn.IZR i)).
Proof.
intros m i Hi.
......@@ -142,7 +142,7 @@ Defined.
(* Why3 goal *)
Lemma Round_logic_def :
forall (m:floating_point.Rounding.mode) (x:R), (no_overflow m x) ->
forall (m:floating_point.Rounding.mode) (x:R), no_overflow m x ->
((value (round_logic m x)) = (round m x)).
Proof.
exact (Round_logic_def 53 1024 (refl_equal true) (refl_equal true)).
......@@ -151,7 +151,7 @@ Qed.
(* Why3 assumption *)
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)).
((value res) = (round m x)) /\ ((exact res) = x) /\ ((model res) = x).
(* Why3 assumption *)
Definition add_post (m:floating_point.Rounding.mode)
......@@ -159,8 +159,8 @@ Definition add_post (m:floating_point.Rounding.mode)
(y:floating_point.DoubleFormat.double)
(res:floating_point.DoubleFormat.double) : Prop :=
((value res) = (round m ((value x) + (value y))%R)) /\
(((exact res) = ((exact x) + (exact y))%R) /\
((model res) = ((model x) + (model y))%R)).
((exact res) = ((exact x) + (exact y))%R) /\
((model res) = ((model x) + (model y))%R).
(* Why3 assumption *)
Definition sub_post (m:floating_point.Rounding.mode)
......@@ -168,8 +168,8 @@ Definition sub_post (m:floating_point.Rounding.mode)
(y:floating_point.DoubleFormat.double)
(res:floating_point.DoubleFormat.double) : Prop :=
((value res) = (round m ((value x) - (value y))%R)) /\
(((exact res) = ((exact x) - (exact y))%R) /\
((model res) = ((model x) - (model y))%R)).
((exact res) = ((exact x) - (exact y))%R) /\
((model res) = ((model x) - (model y))%R).
(* Why3 assumption *)
Definition mul_post (m:floating_point.Rounding.mode)
......@@ -177,8 +177,8 @@ Definition mul_post (m:floating_point.Rounding.mode)
(y:floating_point.DoubleFormat.double)
(res:floating_point.DoubleFormat.double) : Prop :=
((value res) = (round m ((value x) * (value y))%R)) /\
(((exact res) = ((exact x) * (exact y))%R) /\
((model res) = ((model x) * (model y))%R)).
((exact res) = ((exact x) * (exact y))%R) /\
((model res) = ((model x) * (model y))%R).
(* Why3 assumption *)
Definition div_post (m:floating_point.Rounding.mode)
......@@ -186,14 +186,14 @@ Definition div_post (m:floating_point.Rounding.mode)
(y:floating_point.DoubleFormat.double)
(res:floating_point.DoubleFormat.double) : Prop :=
((value res) = (round m ((value x) / (value y))%R)) /\
(((exact res) = ((exact x) / (exact y))%R) /\
((model res) = ((model x) / (model 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)
(res:floating_point.DoubleFormat.double) : Prop :=
((value res) = (-(value x))%R) /\
(((exact res) = (-(exact x))%R) /\ ((model res) = (-(model x))%R)).
((exact res) = (-(exact x))%R) /\ ((model res) = (-(model x))%R).
(* Why3 assumption *)
Definition lt (x:floating_point.DoubleFormat.double)
......
......@@ -120,7 +120,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) ->
((-16777216%Z)%Z <= i)%Z /\ (i <= 16777216%Z)%Z ->
((round m (BuiltIn.IZR i)) = (BuiltIn.IZR i)).
Proof.
intros m i Hi.
......@@ -168,7 +168,7 @@ Defined.
(* Why3 goal *)
Lemma Round_logic_def :
forall (m:floating_point.Rounding.mode) (x:R), (no_overflow m x) ->
forall (m:floating_point.Rounding.mode) (x:R), no_overflow m x ->
((value (round_logic m x)) = (round m x)).
Proof.
intros m x.
......@@ -180,7 +180,7 @@ Qed.
(* Why3 assumption *)
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)).
((value res) = (round m x)) /\ ((exact res) = x) /\ ((model res) = x).
(* Why3 assumption *)
Definition add_post (m:floating_point.Rounding.mode)
......@@ -188,8 +188,8 @@ Definition add_post (m:floating_point.Rounding.mode)
(y:floating_point.SingleFormat.single)
(res:floating_point.SingleFormat.single) : Prop :=
((value res) = (round m ((value x) + (value y))%R)) /\
(((exact res) = ((exact x) + (exact y))%R) /\
((model res) = ((model x) + (model y))%R)).
((exact res) = ((exact x) + (exact y))%R) /\
((model res) = ((model x) + (model y))%R).
(* Why3 assumption *)
Definition sub_post (m:floating_point.Rounding.mode)
......@@ -197,8 +197,8 @@ Definition sub_post (m:floating_point.Rounding.mode)
(y:floating_point.SingleFormat.single)
(res:floating_point.SingleFormat.single) : Prop :=
((value res) = (round m ((value x) - (value y))%R)) /\
(((exact res) = ((exact x) - (exact y))%R) /\
((model res) = ((model x) - (model y))%R)).
((exact res) = ((exact x) - (exact y))%R) /\
((model res) = ((model x) - (model y))%R).
(* Why3 assumption *)
Definition mul_post (m:floating_point.Rounding.mode)
......@@ -206,8 +206,8 @@ Definition mul_post (m:floating_point.Rounding.mode)
(y:floating_point.SingleFormat.single)
(res:floating_point.SingleFormat.single) : Prop :=
((value res) = (round m ((value x) * (value y))%R)) /\
(((exact res) = ((exact x) * (exact y))%R) /\
((model res) = ((model x) * (model y))%R)).
((exact res) = ((exact x) * (exact y))%R) /\
((model res) = ((model x) * (model y))%R).
(* Why3 assumption *)
Definition div_post (m:floating_point.Rounding.mode)
......@@ -215,14 +215,14 @@ Definition div_post (m:floating_point.Rounding.mode)
(y:floating_point.SingleFormat.single)
(res:floating_point.SingleFormat.single) : Prop :=
((value res) = (round m ((value x) / (value y))%R)) /\
(((exact res) = ((exact x) / (exact y))%R) /\
((model res) = ((model x) / (model 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)
(res:floating_point.SingleFormat.single) : Prop :=
((value res) = (-(value x))%R) /\
(((exact res) = (-(exact x))%R) /\ ((model res) = (-(model x))%R)).
((exact res) = (-(exact x))%R) /\ ((model res) = (-(model x))%R).
(* Why3 assumption *)
Definition lt (x:floating_point.SingleFormat.single)
......
......@@ -31,15 +31,16 @@ Qed.
(* Why3 goal *)
Lemma cdiv_cases : forall (n:Z) (d:Z), ((0%Z <= n)%Z -> ((0%Z < d)%Z ->
((ZArith.BinInt.Z.quot n d) = (int.EuclideanDivision.div n d)))) /\
(((n <= 0%Z)%Z -> ((0%Z < d)%Z ->
((ZArith.BinInt.Z.quot n d) = (-(int.EuclideanDivision.div (-n)%Z
d))%Z))) /\ (((0%Z <= n)%Z -> ((d < 0%Z)%Z ->
((ZArith.BinInt.Z.quot n d) = (-(int.EuclideanDivision.div n
(-d)%Z))%Z))) /\ ((n <= 0%Z)%Z -> ((d < 0%Z)%Z ->
((ZArith.BinInt.Z.quot n d) = (int.EuclideanDivision.div (-n)%Z
(-d)%Z)))))).
Lemma cdiv_cases :
forall (n:Z) (d:Z),
((0%Z <= n)%Z -> (0%Z < d)%Z ->
((ZArith.BinInt.Z.quot n d) = (int.EuclideanDivision.div n d))) /\
((n <= 0%Z)%Z -> (0%Z < d)%Z ->
((ZArith.BinInt.Z.quot n d) = (-(int.EuclideanDivision.div (-n)%Z d))%Z)) /\
((0%Z <= n)%Z -> (d < 0%Z)%Z ->
((ZArith.BinInt.Z.quot n d) = (-(int.EuclideanDivision.div n (-d)%Z))%Z)) /\
((n <= 0%Z)%Z -> (d < 0%Z)%Z ->
((ZArith.BinInt.Z.quot n d) = (int.EuclideanDivision.div (-n)%Z (-d)%Z))).
intros n d.
destruct d as [|d|d]; destruct n as [|n|n]; intuition (try contradiction; try discriminate; auto).
+ assert (NZ_d:((Zpos d) <> 0)%Z) by discriminate.
......@@ -64,15 +65,17 @@ Lemma cdiv_cases : forall (n:Z) (d:Z), ((0%Z <= n)%Z -> ((0%Z < d)%Z ->
Qed.
(* Why3 goal *)
Lemma cmod_cases : forall (n:Z) (d:Z), ((0%Z <= n)%Z -> ((0%Z < d)%Z ->
((ZArith.BinInt.Z.rem n d) = (int.EuclideanDivision.mod1 n d)))) /\
(((n <= 0%Z)%Z -> ((0%Z < d)%Z ->
((ZArith.BinInt.Z.rem n d) = (-(int.EuclideanDivision.mod1 (-n)%Z
d))%Z))) /\ (((0%Z <= n)%Z -> ((d < 0%Z)%Z ->
((ZArith.BinInt.Z.rem n d) = (int.EuclideanDivision.mod1 n (-d)%Z)))) /\
((n <= 0%Z)%Z -> ((d < 0%Z)%Z ->
((ZArith.BinInt.Z.rem n d) = (-(int.EuclideanDivision.mod1 (-n)%Z
(-d)%Z))%Z))))).
Lemma cmod_cases :
forall (n:Z) (d:Z),
((0%Z <= n)%Z -> (0%Z < d)%Z ->
((ZArith.BinInt.Z.rem n d) = (int.EuclideanDivision.mod1 n d))) /\
((n <= 0%Z)%Z -> (0%Z < d)%Z ->
((ZArith.BinInt.Z.rem n d) = (-(int.EuclideanDivision.mod1 (-n)%Z d))%Z)) /\
((0%Z <= n)%Z -> (d < 0%Z)%Z ->
((ZArith.BinInt.Z.rem n d) = (int.EuclideanDivision.mod1 n (-d)%Z))) /\
((n <= 0%Z)%Z -> (d < 0%Z)%Z ->
((ZArith.BinInt.Z.rem n d) =
(-(int.EuclideanDivision.mod1 (-n)%Z (-d)%Z))%Z)).
intros n d.
unfold int.EuclideanDivision.mod1.
assert (Z.rem n d = n - (d * (Z.quot n d)))%Z.
......
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
......@@ -36,7 +36,7 @@ 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).
((ZArith.BinInt.Z.abs x) <= y)%Z <-> ((-y)%Z <= x)%Z /\ (x <= y)%Z.
intros x y.
zify.
omega.
......
......@@ -34,7 +34,7 @@ Qed.
(* Why3 goal *)
Lemma Div_bound :
forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z < y)%Z) ->
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).
......@@ -68,7 +68,7 @@ Qed.
(* Why3 goal *)
Lemma Div_sign_pos :
forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z < y)%Z) ->
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.
......@@ -76,7 +76,7 @@ Qed.
(* Why3 goal *)
Lemma Div_sign_neg :
forall (x:Z) (y:Z), ((x <= 0%Z)%Z /\ (0%Z < y)%Z) ->
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).
......@@ -86,7 +86,7 @@ Qed.
(* Why3 goal *)
Lemma Mod_sign_pos :
forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ ~ (y = 0%Z)) ->
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.
......@@ -94,7 +94,7 @@ Qed.
(* Why3 goal *)
Lemma Mod_sign_neg :
forall (x:Z) (y:Z), ((x <= 0%Z)%Z /\ ~ (y = 0%Z)) ->
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.
......@@ -125,22 +125,21 @@ Qed.
(* Why3 goal *)
Lemma Div_inf :
forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (x < y)%Z) ->
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) ->
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)) ->
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).
......@@ -157,8 +156,7 @@ 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)) ->
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.
......
......@@ -58,7 +58,7 @@ Qed.
(* Why3 goal *)
Lemma Div_unique :
forall (x:Z) (y:Z) (q:Z), (0%Z < y)%Z ->
(((q * y)%Z <= x)%Z /\ (x < ((q * y)%Z + y)%Z)%Z) -> ((div x y) = q).
((q * y)%Z <= x)%Z /\ (x < ((q * y)%Z + y)%Z)%Z -> ((div x y) = q).
intros x y q h1 (h2,h3).
assert (h:(~(y=0))%Z) by omega.
generalize (Mod_bound x y h); intro h0.
......@@ -80,7 +80,7 @@ Qed.
(* Why3 goal *)
Lemma Div_bound :
forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z < y)%Z) ->
forall (x:Z) (y:Z), (0%Z <= x)%Z /\ (0%Z < y)%Z ->
(0%Z <= (div x y))%Z /\ ((div x y) <= x)%Z.
intros x y (Hx,Hy).
unfold div.
......@@ -116,7 +116,7 @@ Qed.
(* Why3 goal *)
Lemma Div_inf :
forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (x < y)%Z) -> ((div x y) = 0%Z).
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.
......@@ -127,7 +127,7 @@ Qed.
(* Why3 goal *)
Lemma Div_inf_neg :
forall (x:Z) (y:Z), ((0%Z < x)%Z /\ (x <= y)%Z) ->
forall (x:Z) (y:Z), (0%Z < x)%Z /\ (x <= y)%Z ->
((div (-x)%Z y) = (-1%Z)%Z).
intros x y Hxy.
assert (h: (x < y \/ x = y)%Z) by omega.
......
......@@ -33,7 +33,7 @@ Qed.
(* Why3 goal *)
Lemma infix_lseq_def :
forall (x:Z) (y:Z), (x <= y)%Z <-> ((x < y)%Z \/ (x = y)).
forall (x:Z) (y:Z), (x <= y)%Z <-> (x < y)%Z \/ (x = y).
exact Zle_lt_or_eq_iff.
Qed.
......
......@@ -85,7 +85,7 @@ Qed.
(* Why3 goal *)
Lemma Numof_append :
forall (p:Z -> bool) (a:Z) (b:Z) (c:Z), ((a <= b)%Z /\ (b <= c)%Z) ->
forall (p:Z -> bool) (a:Z) (b:Z) (c:Z), (a <= b)%Z /\ (b <= c)%Z ->
((numof p a c) = ((numof p a b) + (numof p b c))%Z).
Proof.
intros p a b c (h1,h2).
......@@ -152,7 +152,7 @@ Qed.
(* Why3 goal *)
Lemma Empty :
forall (p:Z -> bool) (a:Z) (b:Z),
(forall (n:Z), ((a <= n)%Z /\ (n < b)%Z) -> ~ ((p n) = true)) ->
(forall (n:Z), (a <= n)%Z /\ (n < b)%Z -> ~ ((p n) = true)) ->
((numof p a b) = 0%Z).
Proof.
intros p a b.
......@@ -174,7 +174,7 @@ Qed.
(* Why3 goal *)
Lemma Full :
forall (p:Z -> bool) (a:Z) (b:Z), (a <= b)%Z ->
(forall (n:Z), ((a <= n)%Z /\ (n < b)%Z) -> ((p n) = true)) ->
(forall (n:Z), (a <= n)%Z /\ (n < b)%Z -> ((p n) = true)) ->
((numof p a b) = (b - a)%Z).
Proof.
intros p a b h1.
......@@ -226,7 +226,7 @@ Qed.
(* Why3 goal *)
Lemma numof_increasing :
forall (p:Z -> bool) (i:Z) (j:Z) (k:Z), ((i <= j)%Z /\ (j <= k)%Z) ->
forall (p:Z -> bool) (i:Z) (j:Z) (k:Z), (i <= j)%Z /\ (j <= k)%Z ->
((numof p i j) <= (numof p i k))%Z.
Proof.
intros p i j k (h1,h2).
......@@ -238,7 +238,7 @@ Qed.
(* Why3 goal *)
Lemma numof_strictly_increasing :
forall (p:Z -> bool) (i:Z) (j:Z) (k:Z) (l:Z),
((i <= j)%Z /\ ((j <= k)%Z /\ (k < l)%Z)) -> ((p k) = true) ->
(i <= j)%Z /\ (j <= k)%Z /\ (k < l)%Z -> ((p k) = true) ->
((numof p i j) < (numof p i l))%Z.
Proof.
intros p i j k l (h1,(h2,h3)) h4.
......@@ -250,7 +250,7 @@ Qed.
(* Why3 goal *)
Lemma numof_change_any :
forall (p1:Z -> bool) (p2:Z -> bool) (a:Z) (b:Z),
(forall (j:Z), ((a <= j)%Z /\ (j < b)%Z) -> ((p1 j) = true) ->
(forall (j:Z), (a <= j)%Z /\ (j < b)%Z -> ((p1 j) = true) ->
((p2 j) = true)) ->
((numof p1 a b) <= (numof p2 a b))%Z.
Proof.
......@@ -274,8 +274,8 @@ Qed.