Attention une mise à jour du serveur va être effectuée le vendredi 16 avril entre 12h et 12h30. Cette mise à jour va générer une interruption du service de quelques minutes.

Commit e1551d67 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Revert Coq realizations to the versions before b6e25241.

parent dcc04803
......@@ -15,60 +15,55 @@ Require Import BuiltIn.
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).
Lemma andb_def : forall (x:bool) (y:bool),
((Init.Datatypes.andb x y) = match x with
| true => y
| false => false
end).
Proof.
intros x y.
apply refl_equal.
Qed.
(* Why3 goal *)
Lemma orb_def :
forall (x:bool) (y:bool),
((Init.Datatypes.orb x y) = match x with
| false => y
| true => true
end).
Lemma orb_def : forall (x:bool) (y:bool),
((Init.Datatypes.orb x y) = match x with
| false => y
| true => true
end).
Proof.
intros x y.
apply refl_equal.
Qed.
(* Why3 goal *)
Lemma notb_def :
forall (x:bool),
((Init.Datatypes.negb x) = match x with
| false => true
| true => false
end).
Lemma notb_def : forall (x:bool),
((Init.Datatypes.negb x) = match x with
| false => true
| true => false
end).
Proof.
intros x.
apply refl_equal.
Qed.
(* Why3 goal *)
Lemma xorb_def :
forall (x:bool) (y:bool),
((Init.Datatypes.xorb x y) = match x with
| false => y
| true => (Init.Datatypes.negb y)
end).
Lemma xorb_def : forall (x:bool) (y:bool),
((Init.Datatypes.xorb x y) = match x with
| false => y
| true => (Init.Datatypes.negb y)
end).
Proof.
intros x y.
destruct x; destruct y; auto.
Qed.
(* Why3 goal *)
Lemma implb_def :
forall (x:bool) (y:bool),
((Init.Datatypes.implb x y) = match x with
| false => true
| true => y
end).
Lemma implb_def : forall (x:bool) (y:bool),
((Init.Datatypes.implb x y) = match x with
| false => true
| true => y
end).
Proof.
now intros [|] [|].
Qed.
......
......@@ -37,8 +37,7 @@ Lemma size_int_S : size = Z.succ (Z.of_nat last_bit).
Qed.
(* Why3 goal *)
Lemma size_pos :
(0%Z < size)%Z.
Lemma size_pos : (0%Z < size)%Z.
rewrite size_int_S; omega.
Qed.
......@@ -213,8 +212,8 @@ omega.
Qed.
(* Why3 goal *)
Lemma nth_out_of_bound :
forall (x:t) (n:Z), ((n < 0%Z)%Z \/ (size <= n)%Z) -> ((nth x n) = false).
Lemma nth_out_of_bound : 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.
......@@ -237,8 +236,7 @@ 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:Z), ((nth zeros n) = false).
intros n; apply Nth_zeros_aux.
Qed.
......@@ -261,8 +259,8 @@ Definition ones: t.
Defined.
(* Why3 goal *)
Lemma Nth_ones :
forall (n:Z), ((0%Z <= n)%Z /\ (n < size)%Z) -> ((nth ones n) = true).
Lemma Nth_ones : forall (n:Z), ((0%Z <= n)%Z /\ (n < size)%Z) -> ((nth ones
n) = true).
intros; apply nth_const; easy.
Qed.
......@@ -272,10 +270,9 @@ Definition bw_and: t -> t -> t.
Defined.
(* Why3 goal *)
Lemma Nth_bw_and :
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))).
Lemma Nth_bw_and : 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.
Qed.
......@@ -286,10 +283,9 @@ Definition bw_or: t -> t -> t.
Defined.
(* Why3 goal *)
Lemma Nth_bw_or :
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))).
Lemma Nth_bw_or : 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.
Qed.
......@@ -300,10 +296,9 @@ Definition bw_xor: t -> t -> t.
Defined.
(* Why3 goal *)
Lemma Nth_bw_xor :
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))).
Lemma Nth_bw_xor : 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.
Qed.
......@@ -314,10 +309,8 @@ Definition bw_not: t -> t.
Defined.
(* Why3 goal *)
Lemma Nth_bw_not :
forall (v:t) (n:Z),
((0%Z <= n)%Z /\ (n < size)%Z) ->
((nth (bw_not v) n) = (Init.Datatypes.negb (nth v n))).
Lemma Nth_bw_not : 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.
Qed.
......@@ -344,21 +337,17 @@ Lemma bshiftRl_iter_nth : forall b s m,
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)))).
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)))).
intros b n s h1 h2 h3.
rewrite <-Z2Nat.id with (n := s) at 2; auto.
apply bshiftRl_iter_nth; omega.
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))).
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))).
intros b n s h1 h2 h3.
unfold nth,lsr.
cut (nth_aux b (n + Z.of_nat (Z.to_nat s)) = false).
......@@ -370,8 +359,7 @@ forall (b:t) (n:Z) (s:Z),
Qed.
(* Why3 goal *)
Lemma lsr_zeros :
forall (x:t), ((lsr x 0%Z) = x).
Lemma lsr_zeros : forall (x:t), ((lsr x 0%Z) = x).
auto.
Qed.
......@@ -452,11 +440,9 @@ Lemma BshiftRa_iter_nth_low : forall (b:t) (s:nat) (n:Z),
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)))).
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)))).
unfold nth, lsr.
intros.
assert ((n + s)%Z = (n + Z.of_nat (Z.to_nat s))%Z).
......@@ -500,11 +486,9 @@ Lemma BhiftRa_iter_nth_high : forall (b:t) (s:nat) (n:Z),
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)))).
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)))).
unfold nth, asr.
intros.
apply BhiftRa_iter_nth_high.
......@@ -513,8 +497,7 @@ forall (b:t) (n:Z) (s:Z),
Qed.
(* Why3 goal *)
Lemma asr_zeros :
forall (x:t), ((asr x 0%Z) = x).
Lemma asr_zeros : forall (x:t), ((asr x 0%Z) = x).
auto.
Qed.
......@@ -540,10 +523,8 @@ Lemma bshiftL_iter_nth_high : forall {l} v s m, (0 <= Z.of_nat s)%Z -> (Z.of_nat
Qed.
(* Why3 goal *)
Lemma Lsl_nth_high :
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)).
Lemma Lsl_nth_high : 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.
rewrite <-Z2Nat.id with (n := s) at 2 by omega.
......@@ -571,17 +552,15 @@ Lemma Lsl_nth_low_aux : forall {l} x b (n : int),
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).
Lemma Lsl_nth_low : 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.
rewrite Z2Nat.id; omega.
Qed.
(* Why3 goal *)
Lemma lsl_zeros :
forall (x:t), ((lsl x 0%Z) = x).
Lemma lsl_zeros : forall (x:t), ((lsl x 0%Z) = x).
auto.
Qed.
......@@ -1113,12 +1092,9 @@ Definition rotate_right: t -> Z -> t.
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 ->
((nth (rotate_right v n) i) = (nth v
(int.EuclideanDivision.mod1 (i + n)%Z size)))).
Lemma Nth_rotate_right : 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.
revert h2; revert n.
apply Z_of_nat_prop.
......@@ -1139,12 +1115,9 @@ Definition rotate_left: t -> Z -> t.
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 ->
((nth (rotate_left v n) i) = (nth v
(int.EuclideanDivision.mod1 (i - n)%Z size)))).
Lemma Nth_rotate_left : 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.
revert h2; revert n.
apply Z_of_nat_prop.
......@@ -1170,14 +1143,12 @@ Definition max_int: Z.
Defined.
(* Why3 goal *)
Lemma two_power_size_val :
(two_power_size = (bv.Pow2int.pow2 size)).
Lemma two_power_size_val : (two_power_size = (bv.Pow2int.pow2 size)).
trivial.
Qed.
(* Why3 goal *)
Lemma max_int_val :
(max_int = (two_power_size - 1%Z)%Z).
Lemma max_int_val : (max_int = (two_power_size - 1%Z)%Z).
trivial.
Qed.
......@@ -1206,11 +1177,9 @@ Definition to_int: t -> Z.
Defined.
(* Why3 goal *)
Lemma to_int_def :
forall (x:t),
((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)).
Lemma to_int_def : forall (x:t), ((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.
intros.
......@@ -1231,8 +1200,8 @@ forall (x:t),
Qed.
(* Why3 goal *)
Lemma to_uint_extensionality :
forall (v:t) (v':t), ((to_uint v) = (to_uint v')) -> (v = v').
Lemma to_uint_extensionality : forall (v:t) (v':t),
((to_uint v) = (to_uint v')) -> (v = v').
unfold to_uint.
intros v v'.
rewrite Nat2Z.inj_iff.
......@@ -1240,8 +1209,8 @@ forall (v:t) (v':t), ((to_uint v) = (to_uint v')) -> (v = v').
Qed.
(* Why3 goal *)
Lemma to_int_extensionality :
forall (v:t) (v':t), ((to_int v) = (to_int v')) -> (v = v').
Lemma to_int_extensionality : forall (v:t) (v':t),
((to_int v) = (to_int v')) -> (v = v').
apply twos_complement_extensionality.
Qed.
......@@ -1249,8 +1218,8 @@ Qed.
Definition uint_in_range (i:Z): Prop := (0%Z <= i)%Z /\ (i <= max_int)%Z.
(* Why3 goal *)
Lemma to_uint_bounds :
forall (v:t), (0%Z <= (to_uint v))%Z /\ ((to_uint v) < two_power_size)%Z.
Lemma to_uint_bounds : forall (v:t), (0%Z <= (to_uint v))%Z /\
((to_uint v) < two_power_size)%Z.
intros v.
unfold to_uint, uint_in_range.
split.
......@@ -1354,9 +1323,8 @@ Qed.
(* end of to_uint helpers *)
(* Why3 goal *)
Lemma to_uint_of_int :
forall (i:Z),
((0%Z <= i)%Z /\ (i < two_power_size)%Z) -> ((to_uint (of_int i)) = i).
Lemma to_uint_of_int : 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.
rewrite bvec_to_nat_nat_to_bvec.
......@@ -1370,8 +1338,7 @@ Definition size_bv: t.
Defined.
(* Why3 goal *)
Lemma to_uint_size_bv :
((to_uint size_bv) = size).
Lemma to_uint_size_bv : ((to_uint size_bv) = size).
apply to_uint_of_int.
rewrite max_int_S.
destruct size_in_range; auto with zarith.
......@@ -1382,8 +1349,7 @@ apply Nat_to_bvec_zeros.
Qed.
(* Why3 goal *)
Lemma to_uint_zeros :
((to_uint zeros) = 0%Z).
Lemma to_uint_zeros : ((to_uint zeros) = 0%Z).
rewrite Of_int_zeros.
apply to_uint_of_int; easy.
Qed.
......@@ -1406,8 +1372,7 @@ Lemma Of_int_one_aux : forall {l}, one_aux l = nat_to_bvec (S l) 1%nat.
Qed.
(* Why3 goal *)
Lemma to_uint_one :
((to_uint one) = 1%Z).
Lemma to_uint_one : ((to_uint one) = 1%Z).
unfold to_uint, one.
simpl.
rewrite bvec_to_nat_zeros.
......@@ -1423,8 +1388,7 @@ Lemma Of_int_ones: ones = of_int max_int.
Qed.
(* Why3 goal *)
Lemma to_uint_ones :
((to_uint ones) = max_int).
Lemma to_uint_ones : ((to_uint ones) = max_int).
rewrite Of_int_ones.
apply to_uint_of_int.
rewrite max_int_S.
......@@ -1464,8 +1428,8 @@ Lemma zeros_sign_false: Bsign last_bit zeros = false.
Qed.
(* Why3 goal *)
Lemma positive_is_ge_zeros :
forall (x:t), (is_signed_positive x) <-> (sge x zeros).
Lemma positive_is_ge_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.
......@@ -1490,20 +1454,18 @@ Definition add: t -> t -> t.
Defined.
(* Why3 goal *)
Lemma to_uint_add :
forall (v1:t) (v2:t),
((to_uint (add v1 v2)) = (int.EuclideanDivision.mod1 ((to_uint v1) +
(to_uint v2))%Z two_power_size)).
Lemma to_uint_add : forall (v1:t) (v2:t), ((to_uint (add v1
v2)) = (int.EuclideanDivision.mod1 ((to_uint v1) + (to_uint v2))%Z
two_power_size)).
intros v1 v2.
apply to_uint_of_int.
apply mod1_in_range2.
Qed.
(* Why3 goal *)
Lemma to_uint_add_bounded :
forall (v1:t) (v2:t),
(((to_uint v1) + (to_uint v2))%Z < two_power_size)%Z ->
((to_uint (add v1 v2)) = ((to_uint v1) + (to_uint v2))%Z).
Lemma to_uint_add_bounded : forall (v1:t) (v2:t),
(((to_uint v1) + (to_uint v2))%Z < two_power_size)%Z -> ((to_uint (add v1
v2)) = ((to_uint v1) + (to_uint v2))%Z).
intros v1 v2 h1.
rewrite <-(mod1_out (to_uint v1 + to_uint v2) two_power_size).
apply to_uint_add.
......@@ -1516,20 +1478,18 @@ Definition sub: t -> t -> t.
Defined.
(* Why3 goal *)
Lemma to_uint_sub :
forall (v1:t) (v2:t),
((to_uint (sub v1 v2)) = (int.EuclideanDivision.mod1 ((to_uint v1) -
(to_uint v2))%Z two_power_size)).
Lemma to_uint_sub : forall (v1:t) (v2:t), ((to_uint (sub v1
v2)) = (int.EuclideanDivision.mod1 ((to_uint v1) - (to_uint v2))%Z
two_power_size)).
intros v1 v2.
apply to_uint_of_int, mod1_in_range2.
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) ->
((to_uint (sub v1 v2)) = ((to_uint v1) - (to_uint v2))%Z).
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) -> ((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.
apply to_uint_sub.
......@@ -1541,10 +1501,9 @@ Definition neg: t -> t.
Defined.
(* Why3 goal *)
Lemma to_uint_neg :
forall (v:t),
((to_uint (neg v)) = (int.EuclideanDivision.mod1 (-(to_uint v))%Z
two_power_size)).
Lemma to_uint_neg : forall (v:t),
((to_uint (neg v)) = (int.EuclideanDivision.mod1 (-(to_uint v))%Z
two_power_size)).
intros v.
apply to_uint_of_int, mod1_in_range2.
Qed.
......@@ -1555,19 +1514,17 @@ Definition mul: t -> t -> t.
Defined.
(* Why3 goal *)
Lemma to_uint_mul :
forall (v1:t) (v2:t),
((to_uint (mul v1 v2)) = (int.EuclideanDivision.mod1 ((to_uint v1) *
(to_uint v2))%Z two_power_size)).
Lemma to_uint_mul : forall (v1:t) (v2:t), ((to_uint (mul v1
v2)) = (int.EuclideanDivision.mod1 ((to_uint v1) * (to_uint v2))%Z
two_power_size)).
intros v1 v2.
apply to_uint_of_int, mod1_in_range2.
Qed.
(* Why3 goal *)
Lemma to_uint_mul_bounded :
forall (v1:t) (v2:t),
(((to_uint v1) * (to_uint v2))%Z < two_power_size)%Z ->
((to_uint (mul v1 v2)) = ((to_uint v1) * (to_uint v2))%Z).
Lemma to_uint_mul_bounded : forall (v1:t) (v2:t),
(((to_uint v1) * (to_uint v2))%Z < two_power_size)%Z -> ((to_uint (mul v1
v2)) = ((to_uint v1) * (to_uint v2))%Z).
intros v1 v2 h1.
rewrite <-(mod1_out (to_uint v1 * to_uint v2) two_power_size).
apply to_uint_mul.
......@@ -1582,10 +1539,8 @@ Definition udiv: t -> t -> t.
Defined.
(* Why3 goal *)
Lemma to_uint_udiv :
forall (v1:t) (v2:t),
((to_uint (udiv v1 v2)) = (int.EuclideanDivision.div (to_uint v1)
(to_uint v2))).
Lemma to_uint_udiv : forall (v1:t) (v2:t), ((to_uint (udiv v1
v2)) = (int.EuclideanDivision.div (to_uint v1) (to_uint v2))).
intros v1 v2.
apply to_uint_of_int.
case (Z.eq_dec (to_uint v2) 0); intro.
......@@ -1606,10 +1561,8 @@ Definition urem: t -> t -> t.
Defined.
(* Why3 goal *)
Lemma to_uint_urem :
forall (v1:t) (v2:t),
((to_uint (urem v1 v2)) = (int.EuclideanDivision.mod1 (to_uint v1)
(to_uint v2))).
Lemma to_uint_urem : forall (v1:t) (v2:t), ((to_uint (urem v1
v2)) = (int.EuclideanDivision.mod1 (to_uint v1) (to_uint v2))).
intros v1 v2.
apply to_uint_of_int.
case (Z.eq_dec (to_uint v2) 0); intro.
......@@ -1629,16 +1582,15 @@ Definition lsr_bv: t -> t -> t.
Defined.
(* Why3 goal *)
Lemma lsr_bv_is_lsr :
forall (x:t) (n:t), ((lsr_bv x n) = (lsr x (to_uint n))).
Lemma lsr_bv_is_lsr : forall (x:t) (n:t), ((lsr_bv x n) = (lsr x
(to_uint n))).
easy.
Qed.
(* Why3 goal *)
Lemma to_uint_lsr :