Commit ccf22a40 authored by MARCHE Claude's avatar MARCHE Claude

nightly bench: update obsolete sessions and fixed some proofs

parent 2ae67ad1
......@@ -78,8 +78,14 @@ scheduled on ? 2012
== New Features to announce ==
o
o [ocaml API] incompatible changes in Set/Map/Hashtbl modules
o [prover] fixed Coq 8.4 support for theory real.Trigonometry
o [prover] support for Z3 4.2
o [prover] support for Alt-Ergo 0.95
o [prover] support for CVC4
o [stdlib] fixed inconsistency in map.MapPermut theory
o [prover] support of PVS 6
o [prover] support for mathematica
o [prover] support for MathSAT5
......
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
(* Why3 assumption *)
Definition implb(x:bool) (y:bool): bool := match (x,
y) with
| (true, false) => false
| (_, _) => true
end.
Require int.Abs.
Require int.EuclideanDivision.
Parameter pow2: Z -> Z.
......@@ -23,6 +18,8 @@ Axiom Power_1 : ((pow2 1%Z) = 2%Z).
Axiom Power_sum : forall (n:Z) (m:Z), ((0%Z <= n)%Z /\ (0%Z <= m)%Z) ->
((pow2 (n + m)%Z) = ((pow2 n) * (pow2 m))%Z).
Axiom pow2pos : forall (i:Z), (0%Z <= i)%Z -> (0%Z < (pow2 i))%Z.
Axiom pow2_0 : ((pow2 0%Z) = 1%Z).
Axiom pow2_1 : ((pow2 1%Z) = 2%Z).
......@@ -151,125 +148,139 @@ Axiom pow2_62 : ((pow2 62%Z) = 4611686018427387904%Z).
Axiom pow2_63 : ((pow2 63%Z) = 9223372036854775808%Z).
Axiom Div_pow : forall (x:Z) (i:Z), (((pow2 (i - 1%Z)%Z) <= x)%Z /\
(x < (pow2 i))%Z) -> ((int.EuclideanDivision.div x
(pow2 (i - 1%Z)%Z)) = 1%Z).
Axiom Div_pow2 : forall (x:Z) (i:Z), (((-(pow2 i))%Z <= x)%Z /\
(x < (-(pow2 (i - 1%Z)%Z))%Z)%Z) -> ((int.EuclideanDivision.div x
(pow2 (i - 1%Z)%Z)) = (-2%Z)%Z).
Axiom Mod_pow2_gen : forall (x:Z) (i:Z) (k:Z), ((0%Z <= k)%Z /\ (k < i)%Z) ->
((int.EuclideanDivision.mod1 (int.EuclideanDivision.div (x + (pow2 i))%Z
(pow2 k)) 2%Z) = (int.EuclideanDivision.mod1 (int.EuclideanDivision.div x
(pow2 k)) 2%Z)).
Parameter size: Z.
Axiom size_positive : (1%Z < size)%Z.
Axiom size_positive : (1%Z < size)%Z.
Parameter bv : Type.
Axiom bv : Type.
Parameter bv_WhyType : WhyType bv.
Existing Instance bv_WhyType.
Parameter nth: bv -> Z -> bool.
Parameter bvzero: bv.
Axiom Nth_zero : forall (n:Z), ((0%Z <= n)%Z /\ (n < size)%Z) ->
((nth bvzero n) = false).
Axiom Nth_zero : forall (n:Z), ((0%Z <= n)%Z /\ (n < size)%Z) -> ((nth bvzero
n) = false).
Parameter bvone: bv.
Axiom Nth_one : forall (n:Z), ((0%Z <= n)%Z /\ (n < size)%Z) -> ((nth bvone
Axiom Nth_one : forall (n:Z), ((0%Z <= n)%Z /\ (n < size)%Z) -> ((nth bvone
n) = true).
(* Why3 assumption *)
Definition eq(v1:bv) (v2:bv): Prop := forall (n:Z), ((0%Z <= n)%Z /\
(n < size)%Z) -> ((nth v1 n) = (nth v2 n)).
(n < size)%Z) -> ((nth v1 n) = (nth v2 n)).
Axiom extensionality : forall (v1:bv) (v2:bv), (eq v1 v2) -> (v1 = v2).
Parameter bw_and: bv -> bv -> bv.
Axiom Nth_bw_and : forall (v1:bv) (v2:bv) (n:Z), ((0%Z <= n)%Z /\
(n < size)%Z) -> ((nth (bw_and v1 v2) n) = (andb (nth v1 n) (nth v2 n))).
(n < size)%Z) -> ((nth (bw_and v1 v2) n) = (andb (nth v1 n) (nth v2 n))).
Parameter bw_or: bv -> bv -> bv.
Axiom Nth_bw_or : forall (v1:bv) (v2:bv) (n:Z), ((0%Z <= n)%Z /\
(n < size)%Z) -> ((nth (bw_or v1 v2) n) = (orb (nth v1 n) (nth v2 n))).
(n < size)%Z) -> ((nth (bw_or v1 v2) n) = (orb (nth v1 n) (nth v2 n))).
Parameter bw_xor: bv -> bv -> bv.
Axiom Nth_bw_xor : forall (v1:bv) (v2:bv) (n:Z), ((0%Z <= n)%Z /\
(n < size)%Z) -> ((nth (bw_xor v1 v2) n) = (xorb (nth v1 n) (nth v2 n))).
(n < size)%Z) -> ((nth (bw_xor v1 v2) n) = (xorb (nth v1 n) (nth v2 n))).
Axiom Nth_bw_xor_v1true : forall (v1:bv) (v2:bv) (n:Z), (((0%Z <= n)%Z /\
(n < size)%Z) /\ ((nth v1 n) = true)) -> ((nth (bw_xor v1 v2)
(n < size)%Z) /\ ((nth v1 n) = true)) -> ((nth (bw_xor v1 v2)
n) = (negb (nth v2 n))).
Axiom Nth_bw_xor_v1false : forall (v1:bv) (v2:bv) (n:Z), (((0%Z <= n)%Z /\
(n < size)%Z) /\ ((nth v1 n) = false)) -> ((nth (bw_xor v1 v2)
n) = (nth v2 n)).
(n < size)%Z) /\ ((nth v1 n) = false)) -> ((nth (bw_xor v1 v2) n) = (nth v2
n)).
Axiom Nth_bw_xor_v2true : forall (v1:bv) (v2:bv) (n:Z), (((0%Z <= n)%Z /\
(n < size)%Z) /\ ((nth v2 n) = true)) -> ((nth (bw_xor v1 v2)
(n < size)%Z) /\ ((nth v2 n) = true)) -> ((nth (bw_xor v1 v2)
n) = (negb (nth v1 n))).
Axiom Nth_bw_xor_v2false : forall (v1:bv) (v2:bv) (n:Z), (((0%Z <= n)%Z /\
(n < size)%Z) /\ ((nth v2 n) = false)) -> ((nth (bw_xor v1 v2)
n) = (nth v1 n)).
(n < size)%Z) /\ ((nth v2 n) = false)) -> ((nth (bw_xor v1 v2) n) = (nth v1
n)).
Parameter bw_not: bv -> bv.
Axiom Nth_bw_not : forall (v:bv) (n:Z), ((0%Z <= n)%Z /\ (n < size)%Z) ->
Axiom Nth_bw_not : forall (v:bv) (n:Z), ((0%Z <= n)%Z /\ (n < size)%Z) ->
((nth (bw_not v) n) = (negb (nth v n))).
Parameter lsr: bv -> Z -> bv.
Axiom lsr_nth_low : forall (b:bv) (n:Z) (s:Z), (((0%Z <= n)%Z /\
(n < size)%Z) /\ (((0%Z <= s)%Z /\ (s < size)%Z) /\
((n + s)%Z < size)%Z)) -> ((nth (lsr b s) n) = (nth b (n + s)%Z)).
(n < size)%Z) /\ (((0%Z <= s)%Z /\ (s < size)%Z) /\
((n + s)%Z < size)%Z)) -> ((nth (lsr b s) n) = (nth b (n + s)%Z)).
Axiom lsr_nth_high : forall (b:bv) (n:Z) (s:Z), (((0%Z <= n)%Z /\
(n < size)%Z) /\ (((0%Z <= s)%Z /\ (s < size)%Z) /\
(n < size)%Z) /\ (((0%Z <= s)%Z /\ (s < size)%Z) /\
(size <= (n + s)%Z)%Z)) -> ((nth (lsr b s) n) = false).
Parameter asr: bv -> Z -> bv.
Axiom asr_nth_low : forall (b:bv) (n:Z) (s:Z), ((0%Z <= n)%Z /\
(n < size)%Z) -> ((0%Z <= s)%Z -> (((n + s)%Z < size)%Z -> ((nth (asr b
s) n) = (nth b (n + s)%Z)))).
(n < size)%Z) -> ((0%Z <= s)%Z -> (((n + s)%Z < size)%Z -> ((nth (asr b s)
n) = (nth b (n + s)%Z)))).
Axiom asr_nth_high : forall (b:bv) (n:Z) (s:Z), ((0%Z <= n)%Z /\
(n < size)%Z) -> ((0%Z <= s)%Z -> ((size <= (n + s)%Z)%Z -> ((nth (asr b
s) n) = (nth b (size - 1%Z)%Z)))).
(n < size)%Z) -> ((0%Z <= s)%Z -> ((size <= (n + s)%Z)%Z -> ((nth (asr b s)
n) = (nth b (size - 1%Z)%Z)))).
Parameter lsl: bv -> Z -> bv.
Axiom lsl_nth_high : forall (b:bv) (n:Z) (s:Z), ((0%Z <= n)%Z /\
(n < size)%Z) -> ((0%Z <= s)%Z -> ((0%Z <= (n - s)%Z)%Z -> ((nth (lsl b s)
(n < size)%Z) -> ((0%Z <= s)%Z -> ((0%Z <= (n - s)%Z)%Z -> ((nth (lsl b s)
n) = (nth b (n - s)%Z)))).
Axiom lsl_nth_low : forall (b:bv) (n:Z) (s:Z), ((0%Z <= n)%Z /\
(n < size)%Z) -> ((0%Z <= s)%Z -> (((n - s)%Z < 0%Z)%Z -> ((nth (lsl b s)
(n < size)%Z) -> ((0%Z <= s)%Z -> (((n - s)%Z < 0%Z)%Z -> ((nth (lsl b s)
n) = false))).
Parameter to_nat_sub: bv -> Z -> Z -> Z.
Axiom to_nat_sub_zero : forall (b:bv) (j:Z) (i:Z), (((0%Z <= i)%Z /\
(i <= j)%Z) /\ (j < size)%Z) -> (((nth b j) = false) -> ((to_nat_sub b j
(i <= j)%Z) /\ (j < size)%Z) -> (((nth b j) = false) -> ((to_nat_sub b j
i) = (to_nat_sub b (j - 1%Z)%Z i))).
Axiom to_nat_sub_one : forall (b:bv) (j:Z) (i:Z), (((0%Z <= i)%Z /\
(i <= j)%Z) /\ (j < size)%Z) -> (((nth b j) = true) -> ((to_nat_sub b j
(i <= j)%Z) /\ (j < size)%Z) -> (((nth b j) = true) -> ((to_nat_sub b j
i) = ((pow2 (j - i)%Z) + (to_nat_sub b (j - 1%Z)%Z i))%Z)).
Axiom to_nat_sub_high : forall (b:bv) (j:Z) (i:Z), (j < i)%Z ->
Axiom to_nat_sub_high : forall (b:bv) (j:Z) (i:Z), (j < i)%Z ->
((to_nat_sub b j i) = 0%Z).
Axiom to_nat_of_zero2 : forall (b:bv) (i:Z) (j:Z), (((j < size)%Z /\
Axiom to_nat_of_zero2 : forall (b:bv) (i:Z) (j:Z), (((j < size)%Z /\
(i <= j)%Z) /\ (0%Z <= i)%Z) -> ((forall (k:Z), ((k <= j)%Z /\
(i < k)%Z) -> ((nth b k) = false)) -> ((to_nat_sub b j
0%Z) = (to_nat_sub b i 0%Z))).
(i < k)%Z) -> ((nth b k) = false)) -> ((to_nat_sub b j 0%Z) = (to_nat_sub b
i 0%Z))).
Axiom to_nat_of_zero : forall (b:bv) (i:Z) (j:Z), ((j < size)%Z /\
Axiom to_nat_of_zero : forall (b:bv) (i:Z) (j:Z), ((j < size)%Z /\
(0%Z <= i)%Z) -> ((forall (k:Z), ((k <= j)%Z /\ (i <= k)%Z) -> ((nth b
k) = false)) -> ((to_nat_sub b j i) = 0%Z)).
Require Import Why3.
Ltac ae := why3 "alt-ergo" timelimit 2.
Ltac ae := why3 "alt-ergo" timelimit 5.
Open Scope Z_scope.
(* Why3 goal *)
Theorem to_nat_of_one : forall (b:bv) (i:Z) (j:Z), (((j < size)%Z /\
Theorem to_nat_of_one : forall (b:bv) (i:Z) (j:Z), (((j < size)%Z /\
(i <= j)%Z) /\ (0%Z <= i)%Z) -> ((forall (k:Z), ((k <= j)%Z /\
(i <= k)%Z) -> ((nth b k) = true)) -> ((to_nat_sub b j
i) = ((pow2 ((j - i)%Z + 1%Z)%Z) - 1%Z)%Z)).
......
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
(* Why3 assumption *)
Definition implb(x:bool) (y:bool): bool := match (x,
y) with
| (true, false) => false
| (_, _) => true
end.
Require int.Abs.
Require int.EuclideanDivision.
Parameter pow2: Z -> Z.
......@@ -23,6 +18,8 @@ Axiom Power_1 : ((pow2 1%Z) = 2%Z).
Axiom Power_sum : forall (n:Z) (m:Z), ((0%Z <= n)%Z /\ (0%Z <= m)%Z) ->
((pow2 (n + m)%Z) = ((pow2 n) * (pow2 m))%Z).
Axiom pow2pos : forall (i:Z), (0%Z <= i)%Z -> (0%Z < (pow2 i))%Z.
Axiom pow2_0 : ((pow2 0%Z) = 1%Z).
Axiom pow2_1 : ((pow2 1%Z) = 2%Z).
......@@ -151,118 +148,133 @@ Axiom pow2_62 : ((pow2 62%Z) = 4611686018427387904%Z).
Axiom pow2_63 : ((pow2 63%Z) = 9223372036854775808%Z).
Axiom Div_pow : forall (x:Z) (i:Z), (((pow2 (i - 1%Z)%Z) <= x)%Z /\
(x < (pow2 i))%Z) -> ((int.EuclideanDivision.div x
(pow2 (i - 1%Z)%Z)) = 1%Z).
Axiom Div_pow2 : forall (x:Z) (i:Z), (((-(pow2 i))%Z <= x)%Z /\
(x < (-(pow2 (i - 1%Z)%Z))%Z)%Z) -> ((int.EuclideanDivision.div x
(pow2 (i - 1%Z)%Z)) = (-2%Z)%Z).
Axiom Mod_pow2_gen : forall (x:Z) (i:Z) (k:Z), ((0%Z <= k)%Z /\ (k < i)%Z) ->
((int.EuclideanDivision.mod1 (int.EuclideanDivision.div (x + (pow2 i))%Z
(pow2 k)) 2%Z) = (int.EuclideanDivision.mod1 (int.EuclideanDivision.div x
(pow2 k)) 2%Z)).
Parameter size: Z.
Axiom size_positive : (1%Z < size)%Z.
Axiom size_positive : (1%Z < size)%Z.
Parameter bv : Type.
Axiom bv : Type.
Parameter bv_WhyType : WhyType bv.
Existing Instance bv_WhyType.
Parameter nth: bv -> Z -> bool.
Parameter bvzero: bv.
Axiom Nth_zero : forall (n:Z), ((0%Z <= n)%Z /\ (n < size)%Z) ->
((nth bvzero n) = false).
Axiom Nth_zero : forall (n:Z), ((0%Z <= n)%Z /\ (n < size)%Z) -> ((nth bvzero
n) = false).
Parameter bvone: bv.
Axiom Nth_one : forall (n:Z), ((0%Z <= n)%Z /\ (n < size)%Z) -> ((nth bvone
Axiom Nth_one : forall (n:Z), ((0%Z <= n)%Z /\ (n < size)%Z) -> ((nth bvone
n) = true).
(* Why3 assumption *)
Definition eq(v1:bv) (v2:bv): Prop := forall (n:Z), ((0%Z <= n)%Z /\
(n < size)%Z) -> ((nth v1 n) = (nth v2 n)).
(n < size)%Z) -> ((nth v1 n) = (nth v2 n)).
Axiom extensionality : forall (v1:bv) (v2:bv), (eq v1 v2) -> (v1 = v2).
Parameter bw_and: bv -> bv -> bv.
Axiom Nth_bw_and : forall (v1:bv) (v2:bv) (n:Z), ((0%Z <= n)%Z /\
(n < size)%Z) -> ((nth (bw_and v1 v2) n) = (andb (nth v1 n) (nth v2 n))).
(n < size)%Z) -> ((nth (bw_and v1 v2) n) = (andb (nth v1 n) (nth v2 n))).
Parameter bw_or: bv -> bv -> bv.
Axiom Nth_bw_or : forall (v1:bv) (v2:bv) (n:Z), ((0%Z <= n)%Z /\
(n < size)%Z) -> ((nth (bw_or v1 v2) n) = (orb (nth v1 n) (nth v2 n))).
(n < size)%Z) -> ((nth (bw_or v1 v2) n) = (orb (nth v1 n) (nth v2 n))).
Parameter bw_xor: bv -> bv -> bv.
Axiom Nth_bw_xor : forall (v1:bv) (v2:bv) (n:Z), ((0%Z <= n)%Z /\
(n < size)%Z) -> ((nth (bw_xor v1 v2) n) = (xorb (nth v1 n) (nth v2 n))).
(n < size)%Z) -> ((nth (bw_xor v1 v2) n) = (xorb (nth v1 n) (nth v2 n))).
Axiom Nth_bw_xor_v1true : forall (v1:bv) (v2:bv) (n:Z), (((0%Z <= n)%Z /\
(n < size)%Z) /\ ((nth v1 n) = true)) -> ((nth (bw_xor v1 v2)
(n < size)%Z) /\ ((nth v1 n) = true)) -> ((nth (bw_xor v1 v2)
n) = (negb (nth v2 n))).
Axiom Nth_bw_xor_v1false : forall (v1:bv) (v2:bv) (n:Z), (((0%Z <= n)%Z /\
(n < size)%Z) /\ ((nth v1 n) = false)) -> ((nth (bw_xor v1 v2)
n) = (nth v2 n)).
(n < size)%Z) /\ ((nth v1 n) = false)) -> ((nth (bw_xor v1 v2) n) = (nth v2
n)).
Axiom Nth_bw_xor_v2true : forall (v1:bv) (v2:bv) (n:Z), (((0%Z <= n)%Z /\
(n < size)%Z) /\ ((nth v2 n) = true)) -> ((nth (bw_xor v1 v2)
(n < size)%Z) /\ ((nth v2 n) = true)) -> ((nth (bw_xor v1 v2)
n) = (negb (nth v1 n))).
Axiom Nth_bw_xor_v2false : forall (v1:bv) (v2:bv) (n:Z), (((0%Z <= n)%Z /\
(n < size)%Z) /\ ((nth v2 n) = false)) -> ((nth (bw_xor v1 v2)
n) = (nth v1 n)).
(n < size)%Z) /\ ((nth v2 n) = false)) -> ((nth (bw_xor v1 v2) n) = (nth v1
n)).
Parameter bw_not: bv -> bv.
Axiom Nth_bw_not : forall (v:bv) (n:Z), ((0%Z <= n)%Z /\ (n < size)%Z) ->
Axiom Nth_bw_not : forall (v:bv) (n:Z), ((0%Z <= n)%Z /\ (n < size)%Z) ->
((nth (bw_not v) n) = (negb (nth v n))).
Parameter lsr: bv -> Z -> bv.
Axiom lsr_nth_low : forall (b:bv) (n:Z) (s:Z), (((0%Z <= n)%Z /\
(n < size)%Z) /\ (((0%Z <= s)%Z /\ (s < size)%Z) /\
((n + s)%Z < size)%Z)) -> ((nth (lsr b s) n) = (nth b (n + s)%Z)).
(n < size)%Z) /\ (((0%Z <= s)%Z /\ (s < size)%Z) /\
((n + s)%Z < size)%Z)) -> ((nth (lsr b s) n) = (nth b (n + s)%Z)).
Axiom lsr_nth_high : forall (b:bv) (n:Z) (s:Z), (((0%Z <= n)%Z /\
(n < size)%Z) /\ (((0%Z <= s)%Z /\ (s < size)%Z) /\
(n < size)%Z) /\ (((0%Z <= s)%Z /\ (s < size)%Z) /\
(size <= (n + s)%Z)%Z)) -> ((nth (lsr b s) n) = false).
Parameter asr: bv -> Z -> bv.
Axiom asr_nth_low : forall (b:bv) (n:Z) (s:Z), ((0%Z <= n)%Z /\
(n < size)%Z) -> ((0%Z <= s)%Z -> (((n + s)%Z < size)%Z -> ((nth (asr b
s) n) = (nth b (n + s)%Z)))).
(n < size)%Z) -> ((0%Z <= s)%Z -> (((n + s)%Z < size)%Z -> ((nth (asr b s)
n) = (nth b (n + s)%Z)))).
Axiom asr_nth_high : forall (b:bv) (n:Z) (s:Z), ((0%Z <= n)%Z /\
(n < size)%Z) -> ((0%Z <= s)%Z -> ((size <= (n + s)%Z)%Z -> ((nth (asr b
s) n) = (nth b (size - 1%Z)%Z)))).
(n < size)%Z) -> ((0%Z <= s)%Z -> ((size <= (n + s)%Z)%Z -> ((nth (asr b s)
n) = (nth b (size - 1%Z)%Z)))).
Parameter lsl: bv -> Z -> bv.
Axiom lsl_nth_high : forall (b:bv) (n:Z) (s:Z), ((0%Z <= n)%Z /\
(n < size)%Z) -> ((0%Z <= s)%Z -> ((0%Z <= (n - s)%Z)%Z -> ((nth (lsl b s)
(n < size)%Z) -> ((0%Z <= s)%Z -> ((0%Z <= (n - s)%Z)%Z -> ((nth (lsl b s)
n) = (nth b (n - s)%Z)))).
Axiom lsl_nth_low : forall (b:bv) (n:Z) (s:Z), ((0%Z <= n)%Z /\
(n < size)%Z) -> ((0%Z <= s)%Z -> (((n - s)%Z < 0%Z)%Z -> ((nth (lsl b s)
(n < size)%Z) -> ((0%Z <= s)%Z -> (((n - s)%Z < 0%Z)%Z -> ((nth (lsl b s)
n) = false))).
Parameter to_nat_sub: bv -> Z -> Z -> Z.
Axiom to_nat_sub_zero : forall (b:bv) (j:Z) (i:Z), (((0%Z <= i)%Z /\
(i <= j)%Z) /\ (j < size)%Z) -> (((nth b j) = false) -> ((to_nat_sub b j
(i <= j)%Z) /\ (j < size)%Z) -> (((nth b j) = false) -> ((to_nat_sub b j
i) = (to_nat_sub b (j - 1%Z)%Z i))).
Axiom to_nat_sub_one : forall (b:bv) (j:Z) (i:Z), (((0%Z <= i)%Z /\
(i <= j)%Z) /\ (j < size)%Z) -> (((nth b j) = true) -> ((to_nat_sub b j
(i <= j)%Z) /\ (j < size)%Z) -> (((nth b j) = true) -> ((to_nat_sub b j
i) = ((pow2 (j - i)%Z) + (to_nat_sub b (j - 1%Z)%Z i))%Z)).
Axiom to_nat_sub_high : forall (b:bv) (j:Z) (i:Z), (j < i)%Z ->
Axiom to_nat_sub_high : forall (b:bv) (j:Z) (i:Z), (j < i)%Z ->
((to_nat_sub b j i) = 0%Z).
Require Import Why3.
Ltac ae := why3 "alt-ergo" timelimit 2.
Ltac ae := why3 "Alt-Ergo,0.94" timelimit 5.
Open Scope Z_scope.
(* Why3 goal *)
Theorem to_nat_of_zero2 : forall (b:bv) (i:Z) (j:Z), (((j < size)%Z /\
Theorem to_nat_of_zero2 : forall (b:bv) (i:Z) (j:Z), (((j < size)%Z /\
(i <= j)%Z) /\ (0%Z <= i)%Z) -> ((forall (k:Z), ((k <= j)%Z /\
(i < k)%Z) -> ((nth b k) = false)) -> ((to_nat_sub b j
0%Z) = (to_nat_sub b i 0%Z))).
(i < k)%Z) -> ((nth b k) = false)) -> ((to_nat_sub b j 0%Z) = (to_nat_sub b
i 0%Z))).
intros b i j ((Hj,Hij),Hipos).
generalize Hj.
pattern j; apply Zlt_lower_bound_ind with (z:=i); auto.
......
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
(* Why3 assumption *)
Definition implb(x:bool) (y:bool): bool := match (x,
y) with
| (true, false) => false
| (_, _) => true
end.
Require int.Abs.
Require int.EuclideanDivision.
Parameter pow2: Z -> Z.
......@@ -23,6 +18,8 @@ Axiom Power_1 : ((pow2 1%Z) = 2%Z).
Axiom Power_sum : forall (n:Z) (m:Z), ((0%Z <= n)%Z /\ (0%Z <= m)%Z) ->
((pow2 (n + m)%Z) = ((pow2 n) * (pow2 m))%Z).
Axiom pow2pos : forall (i:Z), (0%Z <= i)%Z -> (0%Z < (pow2 i))%Z.
Axiom pow2_0 : ((pow2 0%Z) = 1%Z).
Axiom pow2_1 : ((pow2 1%Z) = 2%Z).
......@@ -151,130 +148,145 @@ Axiom pow2_62 : ((pow2 62%Z) = 4611686018427387904%Z).
Axiom pow2_63 : ((pow2 63%Z) = 9223372036854775808%Z).
Axiom Div_pow : forall (x:Z) (i:Z), (((pow2 (i - 1%Z)%Z) <= x)%Z /\
(x < (pow2 i))%Z) -> ((int.EuclideanDivision.div x
(pow2 (i - 1%Z)%Z)) = 1%Z).
Axiom Div_pow2 : forall (x:Z) (i:Z), (((-(pow2 i))%Z <= x)%Z /\
(x < (-(pow2 (i - 1%Z)%Z))%Z)%Z) -> ((int.EuclideanDivision.div x
(pow2 (i - 1%Z)%Z)) = (-2%Z)%Z).
Axiom Mod_pow2_gen : forall (x:Z) (i:Z) (k:Z), ((0%Z <= k)%Z /\ (k < i)%Z) ->
((int.EuclideanDivision.mod1 (int.EuclideanDivision.div (x + (pow2 i))%Z
(pow2 k)) 2%Z) = (int.EuclideanDivision.mod1 (int.EuclideanDivision.div x
(pow2 k)) 2%Z)).
Parameter size: Z.
Axiom size_positive : (1%Z < size)%Z.
Axiom size_positive : (1%Z < size)%Z.
Parameter bv : Type.
Axiom bv : Type.
Parameter bv_WhyType : WhyType bv.
Existing Instance bv_WhyType.
Parameter nth: bv -> Z -> bool.
Parameter bvzero: bv.
Axiom Nth_zero : forall (n:Z), ((0%Z <= n)%Z /\ (n < size)%Z) ->
((nth bvzero n) = false).
Axiom Nth_zero : forall (n:Z), ((0%Z <= n)%Z /\ (n < size)%Z) -> ((nth bvzero
n) = false).
Parameter bvone: bv.
Axiom Nth_one : forall (n:Z), ((0%Z <= n)%Z /\ (n < size)%Z) -> ((nth bvone
Axiom Nth_one : forall (n:Z), ((0%Z <= n)%Z /\ (n < size)%Z) -> ((nth bvone
n) = true).
(* Why3 assumption *)
Definition eq(v1:bv) (v2:bv): Prop := forall (n:Z), ((0%Z <= n)%Z /\
(n < size)%Z) -> ((nth v1 n) = (nth v2 n)).
(n < size)%Z) -> ((nth v1 n) = (nth v2 n)).
Axiom extensionality : forall (v1:bv) (v2:bv), (eq v1 v2) -> (v1 = v2).
Parameter bw_and: bv -> bv -> bv.
Axiom Nth_bw_and : forall (v1:bv) (v2:bv) (n:Z), ((0%Z <= n)%Z /\
(n < size)%Z) -> ((nth (bw_and v1 v2) n) = (andb (nth v1 n) (nth v2 n))).
(n < size)%Z) -> ((nth (bw_and v1 v2) n) = (andb (nth v1 n) (nth v2 n))).
Parameter bw_or: bv -> bv -> bv.
Axiom Nth_bw_or : forall (v1:bv) (v2:bv) (n:Z), ((0%Z <= n)%Z /\
(n < size)%Z) -> ((nth (bw_or v1 v2) n) = (orb (nth v1 n) (nth v2 n))).
(n < size)%Z) -> ((nth (bw_or v1 v2) n) = (orb (nth v1 n) (nth v2 n))).
Parameter bw_xor: bv -> bv -> bv.
Axiom Nth_bw_xor : forall (v1:bv) (v2:bv) (n:Z), ((0%Z <= n)%Z /\
(n < size)%Z) -> ((nth (bw_xor v1 v2) n) = (xorb (nth v1 n) (nth v2 n))).
(n < size)%Z) -> ((nth (bw_xor v1 v2) n) = (xorb (nth v1 n) (nth v2 n))).
Axiom Nth_bw_xor_v1true : forall (v1:bv) (v2:bv) (n:Z), (((0%Z <= n)%Z /\
(n < size)%Z) /\ ((nth v1 n) = true)) -> ((nth (bw_xor v1 v2)
(n < size)%Z) /\ ((nth v1 n) = true)) -> ((nth (bw_xor v1 v2)
n) = (negb (nth v2 n))).
Axiom Nth_bw_xor_v1false : forall (v1:bv) (v2:bv) (n:Z), (((0%Z <= n)%Z /\
(n < size)%Z) /\ ((nth v1 n) = false)) -> ((nth (bw_xor v1 v2)
n) = (nth v2 n)).
(n < size)%Z) /\ ((nth v1 n) = false)) -> ((nth (bw_xor v1 v2) n) = (nth v2
n)).
Axiom Nth_bw_xor_v2true : forall (v1:bv) (v2:bv) (n:Z), (((0%Z <= n)%Z /\
(n < size)%Z) /\ ((nth v2 n) = true)) -> ((nth (bw_xor v1 v2)
(n < size)%Z) /\ ((nth v2 n) = true)) -> ((nth (bw_xor v1 v2)
n) = (negb (nth v1 n))).
Axiom Nth_bw_xor_v2false : forall (v1:bv) (v2:bv) (n:Z), (((0%Z <= n)%Z /\
(n < size)%Z) /\ ((nth v2 n) = false)) -> ((nth (bw_xor v1 v2)
n) = (nth v1 n)).
(n < size)%Z) /\ ((nth v2 n) = false)) -> ((nth (bw_xor v1 v2) n) = (nth v1
n)).
Parameter bw_not: bv -> bv.