Commit d0e1f7b5 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

Merge branch 'master' into itp

parents e4b1478b c7703c36
......@@ -154,7 +154,6 @@ why3.conf
/src/coq-tactic/.why3-vo-*
# Coq
/lib/coq/bv/BV_Gen.v
# PVS
.pvscontext
......
......@@ -261,6 +261,10 @@ endif
src/util/strings.cmo:: WARNINGS:=$(WARNINGS)-3
src/util/strings.cmx:: WARNINGS:=$(WARNINGS)-3
# hide warning 'no cmx file was found in path for module ..., and its interface was not compiled with -opaque' for the coq tactic
src/coq-tactic/why3tac.cmx:: WARNINGS:=$(WARNINGS)-58
# build targets
byte: lib/why3/why3.cma
......@@ -995,7 +999,7 @@ ifeq (@enable_coq_support@,yes)
ifeq (@enable_coq_libs@,yes)
COQVERSIONSPECIFIC=bv/BV_Gen.v
COQVERSIONSPECIFIC=
COQVERSIONSPECIFICTARGETS=$(addprefix lib/coq/, $(COQVERSIONSPECIFIC))
COQVERSIONSPECIFICSOURCES=$(addsuffix .@coq_compat_version@, $(COQVERSIONSPECIFICTARGETS))
......@@ -1041,7 +1045,11 @@ COQLIBS_OPTION = $(addprefix lib/coq/option/, $(COQLIBS_OPTION_FILES))
COQLIBS_SEQ_FILES = Seq
COQLIBS_SEQ = $(addprefix lib/coq/seq/, $(COQLIBS_SEQ_FILES))
ifeq (@coq_compat_version@,COQ84)
COQLIBS_BV_FILES = Pow2int
else
COQLIBS_BV_FILES = Pow2int BV_Gen
endif
COQLIBS_BV = $(addprefix lib/coq/bv/, $(COQLIBS_BV_FILES))
ifeq (@enable_coq_fp_libs@,yes)
......@@ -1384,48 +1392,57 @@ update-isabelle: $(ISABELLELIBS_INT) $(ISABELLELIBS_BOOL) $(ISABELLELIBS_REAL) $
$(ISABELLELIBS_INT): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen theories/int.why
mkdir -p lib/isabelle/int
WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T int.$(notdir $(basename $@)) -o lib/isabelle/int/
$(SHOW) "Generating Isabelle realization for int.$(notdir $(basename $@))"
$(HIDE)mkdir -p lib/isabelle/int
$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T int.$(notdir $(basename $@)) -o lib/isabelle/int/
$(ISABELLELIBS_BOOL): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen theories/bool.why
mkdir -p lib/isabelle/bool
WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T bool.$(notdir $(basename $@)) -o lib/isabelle/bool/
$(SHOW) "Generating Isabelle realization for bool.$(notdir $(basename $@))"
$(HIDE)mkdir -p lib/isabelle/bool
$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T bool.$(notdir $(basename $@)) -o lib/isabelle/bool/
$(ISABELLELIBS_REAL): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen theories/real.why
mkdir -p lib/isabelle/real
WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T real.$(notdir $(basename $@)) -o lib/isabelle/real/
$(SHOW) "Generating Isabelle realization for real.$(notdir $(basename $@))"
$(HIDE)mkdir -p lib/isabelle/real
$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T real.$(notdir $(basename $@)) -o lib/isabelle/real/
$(ISABELLELIBS_NUMBER): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen theories/number.why
mkdir -p lib/isabelle/number
WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T number.$(notdir $(basename $@)) -o lib/isabelle/number/
$(SHOW) "Generating Isabelle realization for number.$(notdir $(basename $@))"
$(HIDE)mkdir -p lib/isabelle/number
$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T number.$(notdir $(basename $@)) -o lib/isabelle/number/
$(ISABELLELIBS_SET): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen theories/set.why
mkdir -p lib/isabelle/set
WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T set.$(notdir $(basename $@)) -o lib/isabelle/set/
$(SHOW) "Generating Isabelle realization for set.$(notdir $(basename $@))"
$(HIDE)mkdir -p lib/isabelle/set
$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T set.$(notdir $(basename $@)) -o lib/isabelle/set/
$(ISABELLELIBS_MAP): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen theories/map.why
mkdir -p lib/isabelle/map
WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T map.$(notdir $(basename $@)) -o lib/isabelle/map/
$(SHOW) "Generating Isabelle realization for map.$(notdir $(basename $@))"
$(HIDE)mkdir -p lib/isabelle/map
$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T map.$(notdir $(basename $@)) -o lib/isabelle/map/
$(ISABELLELIBS_LIST): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen theories/list.why
mkdir -p lib/isabelle/list
WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T list.$(notdir $(basename $@)) -o lib/isabelle/list/
$(SHOW) "Generating Isabelle realization for list.$(notdir $(basename $@))"
$(HIDE)mkdir -p lib/isabelle/list
$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T list.$(notdir $(basename $@)) -o lib/isabelle/list/
$(ISABELLELIBS_OPTION): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen theories/option.why
mkdir -p lib/isabelle/option
WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T option.$(notdir $(basename $@)) -o lib/isabelle/option/
$(SHOW) "Generating Isabelle realization for option.$(notdir $(basename $@))"
$(HIDE)mkdir -p lib/isabelle/option
$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T option.$(notdir $(basename $@)) -o lib/isabelle/option/
$(ISABELLELIBS_BV): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen theories/bv.why
mkdir -p lib/isabelle/bv
WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T bv.$(notdir $(basename $@)) -o lib/isabelle/bv/
$(SHOW) "Generating Isabelle realization for bv.$(notdir $(basename $@))"
$(HIDE)mkdir -p lib/isabelle/bv
$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T bv.$(notdir $(basename $@)) -o lib/isabelle/bv/
# do not update isabelle realizations systematically
# all: update-isabelle
......
......@@ -126,6 +126,71 @@ Note that the syntax for type
expressions notably differs from the usual ML syntax (\eg the
type of polymorphic lists is written \texttt{list 'a}, not \texttt{'a list}).
\subsection{Formulas}
The syntax for formulas is given Figure~\ref{fig:bnf:formula}.
The various constructs have the following priorities and
associativities, from lowest to greatest priority:
\begin{center}
\begin{tabular}{|l|l|}
\hline
construct & associativity \\
\hline\hline
\texttt{if then else} / \texttt{let in} & -- \\
label & -- \\
\texttt{->} / \texttt{<->} & right \\
\texttt{by} / \texttt{so} & right \\
\verb!\/! / \verb!||! & right \\
\verb|/\| / \verb!&&! & right \\
\texttt{not} & -- \\
infix level 1 & left \\
infix level 2 & left \\
infix level 3 & left \\
infix level 4 & left \\
prefix & -- \\
\hline
\end{tabular}
\end{center}
Note that infix symbols of level 1 include equality (\texttt{=}) and
disequality (\texttt{<>}).
\begin{figure}
\begin{center}\framebox{\input{./formula_bnf.tex}}\end{center}
\caption{Syntax for formulas.}
\label{fig:bnf:formula}
\end{figure}
Notice that there are two symbols for the conjunction: \verb|/\|
and \verb|&&|, and similarly for disjunction. They are logically
equivalent, but may be treated slightly differently by some
transformations. For instance, \texttt{split} transforms the goal
\verb|A /\ B| into subgoals \verb|A| and \verb|B|, whereas it transforms
\verb|A && B| into subgoals \verb|A| and \verb|A -> B|. Similarly, it
transforms \verb!not (A || B)! into subgoals \verb|not A| and
\verb|not ((not A) /\ B)|.
The \texttt{by}/\texttt{so} connectives are proof indications. They are
logically equivalent to their first argument, but may affect the result
of some transformations. For instance, the \texttt{split\_goal}
transformations interpret those connectives as introduction of logical cuts
(see~\ref{tech:trans:split} for details).
\subsection{Theories}
The syntax for theories is given on Figure~\ref{fig:bnf:theorya} and~\ref{fig:bnf:theoryb}.
\begin{figure}
\begin{center}\framebox{\input{./theory_bnf.tex}}\end{center}
\caption{Syntax for theories (part 1).}
\label{fig:bnf:theorya}
\end{figure}
\begin{figure}
\begin{center}\framebox{\input{./theory2_bnf.tex}}\end{center}
\caption{Syntax for theories (part 2).}
\label{fig:bnf:theoryb}
\end{figure}
\subsubsection{Algebraic types}
TO BE COMPLETED
......@@ -221,70 +286,6 @@ axiom fliteral42_axiom : f'real fliteral42 = 0.5 /\ f'isFinite fliteral42
This type is used in the standard library in the theories
\texttt{ieee\_float.Float32} and \texttt{ieee\_float.Float64}.
\subsection{Formulas}
The syntax for formulas is given Figure~\ref{fig:bnf:formula}.
The various constructs have the following priorities and
associativities, from lowest to greatest priority:
\begin{center}
\begin{tabular}{|l|l|}
\hline
construct & associativity \\
\hline\hline
\texttt{if then else} / \texttt{let in} & -- \\
label & -- \\
\texttt{->} / \texttt{<->} & right \\
\texttt{by} / \texttt{so} & right \\
\verb!\/! / \verb!||! & right \\
\verb|/\| / \verb!&&! & right \\
\texttt{not} & -- \\
infix level 1 & left \\
infix level 2 & left \\
infix level 3 & left \\
infix level 4 & left \\
prefix & -- \\
\hline
\end{tabular}
\end{center}
Note that infix symbols of level 1 include equality (\texttt{=}) and
disequality (\texttt{<>}).
\begin{figure}
\begin{center}\framebox{\input{./formula_bnf.tex}}\end{center}
\caption{Syntax for formulas.}
\label{fig:bnf:formula}
\end{figure}
Notice that there are two symbols for the conjunction: \verb|/\|
and \verb|&&|, and similarly for disjunction. They are logically
equivalent, but may be treated slightly differently by some
transformations. For instance, \texttt{split} transforms the goal
\verb|A /\ B| into subgoals \verb|A| and \verb|B|, whereas it transforms
\verb|A && B| into subgoals \verb|A| and \verb|A -> B|. Similarly, it
transforms \verb!not (A || B)! into subgoals \verb|not A| and
\verb|not ((not A) /\ B)|.
The \texttt{by}/\texttt{so} connectives are proof indications. They are
logically equivalent to their first argument, but may affect the result
of some transformations. For instance, the \texttt{split\_goal}
transformations interpret those connectives as introduction of logical cuts
(see~\ref{tech:trans:split} for details).
\subsection{Theories}
The syntax for theories is given on Figure~\ref{fig:bnf:theorya} and~\ref{fig:bnf:theoryb}.
\begin{figure}
\begin{center}\framebox{\input{./theory_bnf.tex}}\end{center}
\caption{Syntax for theories (part 1).}
\label{fig:bnf:theorya}
\end{figure}
\begin{figure}
\begin{center}\framebox{\input{./theory2_bnf.tex}}\end{center}
\caption{Syntax for theories (part 2).}
\label{fig:bnf:theoryb}
\end{figure}
\subsection{Files}
A \why input file is a (possibly empty) list of theories.
......
......@@ -3,6 +3,8 @@
| "=" type ; alias type
| "=" "|"? type-case ("|" type-case)* ; algebraic type
| "=" "{" record-field (";" record-field)* "}" ; record type
| "<" "range" integer integer ">" ; range type
| "<" "float" integer integer ">" ; float type
\
type-case ::= uident label* type-param*
\
......
......@@ -3,7 +3,5 @@
| "'" lident ; type variable
| "()" ; empty tuple type
| "(" type ("," type)+ ")" ; tuple type
| "(" type ")" ; parentheses
| "<" "range" integer integer ">" ; range type
| "<" "float" integer integer ">" ; float type %
| "(" type ")" ; parentheses %
\end{syntax}
\ No newline at end of file
......@@ -6,7 +6,6 @@ valid "Finished Why3 theory"
fail "\\*\\*\\* \\(.*\\)$" "\\1"
time "why3cpulimit time : %s s"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
transformation "eliminate_if_fmla"
transformation "eliminate_let_fmla"
......
......@@ -2,6 +2,7 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Coq" version="8.6" timelimit="5" steplimit="1" memlimit="4000"/>
<prover id="1" name="CVC4" version="1.2" timelimit="60" steplimit="1" memlimit="1000"/>
<prover id="2" name="Zenon" version="0.8.0" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="3" name="CVC3" version="2.4.1" timelimit="5" steplimit="1" memlimit="0"/>
......@@ -28,13 +29,13 @@
<prover id="24" name="veriT" version="201410" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="25" name="Alt-Ergo" version="1.00.prv" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="26" name="Zenon Modulo" version="0.4.1" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="27" name="Coq" version="8.4pl6" timelimit="5" steplimit="1" memlimit="4000"/>
<prover id="28" name="Z3" version="4.4.1" timelimit="5" steplimit="1" memlimit="4000"/>
<prover id="29" name="Alt-Ergo" version="1.30" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="30" name="Isabelle" version="2016-1" timelimit="100" steplimit="1" memlimit="1000"/>
<file name="../genealogy.why" expanded="true">
<theory name="Genealogy" sum="35e1439432a79e05534b2c5cf39ad9dc" expanded="true">
<goal name="Child_is_son_or_daughter">
<proof prover="0" edited="genealogy_Genealogy_Child_is_son_or_daughter_1.v"><result status="valid" time="0.31"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
<proof prover="4"><result status="valid" time="0.00"/></proof>
......@@ -57,10 +58,9 @@
<proof prover="24"><result status="valid" time="0.00"/></proof>
<proof prover="25"><result status="valid" time="0.00" steps="7"/></proof>
<proof prover="26"><result status="valid" time="0.02"/></proof>
<proof prover="27" edited="genealogy_Genealogy_Child_is_son_or_daughter_1.v"><result status="valid" time="0.80"/></proof>
<proof prover="28"><result status="valid" time="0.01"/></proof>
<proof prover="29"><result status="valid" time="0.00" steps="10"/></proof>
<proof prover="30" edited="genealogy_Genealogy_Child_is_son_or_daughter_1.xml"><result status="valid" time="25.12"/></proof>
<proof prover="30" edited="genealogy_Genealogy_Child_is_son_or_daughter_1.xml"><result status="valid" time="21.67"/></proof>
</goal>
<goal name="Sibling_sym">
<proof prover="1"><result status="valid" time="0.00"/></proof>
......@@ -114,7 +114,7 @@
<proof prover="26"><result status="valid" time="0.01"/></proof>
<proof prover="28"><result status="valid" time="0.01"/></proof>
<proof prover="29"><result status="valid" time="0.00" steps="10"/></proof>
<proof prover="30" edited="genealogy_Genealogy_Sibling_is_brother_or_sister_1.xml"><result status="valid" time="24.35"/></proof>
<proof prover="30" edited="genealogy_Genealogy_Sibling_is_brother_or_sister_1.xml"><result status="valid" time="20.20"/></proof>
</goal>
<goal name="Grandparent_is_grandfather_or_grandmother">
<proof prover="1"><result status="valid" time="0.01"/></proof>
......@@ -141,7 +141,7 @@
<proof prover="26"><result status="valid" time="0.02"/></proof>
<proof prover="28"><result status="valid" time="0.01"/></proof>
<proof prover="29"><result status="valid" time="0.00" steps="36"/></proof>
<proof prover="30" edited="genealogy_Genealogy_Grandparent_is_grandfather_or_grandmother_1.xml"><result status="valid" time="22.72"/></proof>
<proof prover="30" edited="genealogy_Genealogy_Grandparent_is_grandfather_or_grandmother_1.xml"><result status="valid" time="20.18"/></proof>
</goal>
<goal name="Grandfather_male">
<proof prover="1"><result status="valid" time="0.00"/></proof>
......
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2016 -- INRIA - CNRS - Paris-Sud University *)
(* *)
(* This software is distributed under the terms of the GNU Lesser *)
(* General Public License version 2.1, with the special exception *)
(* on linking described in file LICENSE. *)
(* *)
(********************************************************************)
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
......@@ -8,7 +19,10 @@ Require int.Abs.
Require int.EuclideanDivision.
Require bv.Pow2int.
Parameter last_bit : nat.
Local Parameter last_bit : nat.
(* Important notice: do not remove 'Local' above, otherwise 'why3 realize' will
assume it comes from Why3 and will remove it. We use 'Parameter' instead of
'Variable' to avoid a Coq warning *)
Definition size_nat: nat := S last_bit.
......@@ -205,7 +219,6 @@ unfold nth.
rewrite nth_aux_out_of_bound; auto with zarith.
Qed.
Definition zeros_aux {l} : Vector.t bool l.
exact (Vector.const false l).
Defined.
......@@ -716,18 +729,17 @@ Lemma twos_complement_extensionality : forall {m} (v v' : Bvector m),
apply Vector.case0 with (v := v'); trivial.
revert v h H.
apply Vector.caseS with (v := v'); intros.
assert (tmp : forall {n} v v',
twos_complement (S n) (false :: v) <> twos_complement (S n) (true :: v')).
intros n1 v0 v'0 H1.
assert ((twos_complement (S n1) (true :: v'0) >= 0)%Z).
rewrite <- H1; apply twos_complement_pos.
assert ((twos_complement (S n1) (true :: v'0) < 0)%Z).
apply twos_complement_neg.
easy.
case h, h0; intros.
inversion H.
apply bvec_to_nat_extensionality; simpl; omega.
Lemma tmp : forall {n} v v', twos_complement (S n) (false :: v) <> twos_complement (S n) (true :: v').
intros.
intro.
assert ((twos_complement (S n) (true :: v') >= 0)%Z).
rewrite <- H; apply twos_complement_pos.
assert ((twos_complement (S n) (true :: v') < 0)%Z).
apply twos_complement_neg.
easy.
Qed.
assert (twos_complement (S n0) (false :: v) <>
twos_complement (S n0) (true :: t0)).
apply tmp.
......@@ -1596,7 +1608,7 @@ Lemma nth_bv_def : forall (x:t) (i:t), ((nth_bv x i) = true) <->
apply to_uint_bounds.
unfold nth.
rewrite (nth_high x (to_uint i)); auto.
Lemma tmmp: forall x i, to_uint i >= size -> lsr_bv x i = zeros_aux.
assert (tmmp: forall x i, to_uint i >= size -> lsr_bv x i = zeros_aux).
intros.
apply Extensionality_aux; unfold eq_aux; intros.
unfold lsr_bv, zeros_aux.
......@@ -1605,7 +1617,6 @@ Lemma nth_bv_def : forall (x:t) (i:t), ((nth_bv x i) = true) <->
unfold size in H; auto with zarith.
easy.
auto with zarith.
Qed.
rewrite tmmp by auto.
split; intro.
assert False by easy; auto.
......@@ -1705,55 +1716,55 @@ Lemma mask_succ :
apply to_uint_sub.
Qed.
Definition add_aux {l} (v w : Vector.t bool l) : Vector.t bool l :=
nat_to_bvec l (Z.to_nat (mod1
(Z.of_nat (bvec_to_nat l v) + Z.of_nat (bvec_to_nat l w))
(Pow2int.pow2 (Z.of_nat l)))).
Lemma mask_succ_tmp :
forall n,
add (lsl (sub (lsl (of_int 1%Z) (Z.of_nat n)) (of_int 1%Z)) (Z.of_nat 1)) (of_int 1%Z)
= bw_or (lsl (sub (lsl (of_int 1%Z) (Z.of_nat n)) (of_int 1%Z)) (Z.of_nat 1)) (of_int 1%Z).
intro.
Lemma add_and_or :
assert (add_and_or :
forall v, nth v 0 = false ->
add v (of_int 1) = bw_or v (of_int 1).
Definition add_aux {l} (v w : Vector.t bool l) : Vector.t bool l.
exact (nat_to_bvec l (Z.to_nat (mod1 (Z.of_nat (bvec_to_nat l v) + Z.of_nat (bvec_to_nat l w)) (Pow2int.pow2 (Z.of_nat l))))).
Defined.
Lemma add_is_add_aux : forall v w, add v w = add_aux v w.
auto.
Qed.
Lemma add_and_or_aux :
add v (of_int 1) = bw_or v (of_int 1)).
assert (add_is_add_aux : forall v w, add v w = add_aux v w) by auto.
assert (add_and_or_aux :
forall {l} v, @nth_aux l v 0 = false ->
add_aux v (nat_to_bvec l 1)
= Vector.map2 (fun x y => x || y) v (nat_to_bvec l 1).
= Vector.map2 (fun x y => x || y) v (nat_to_bvec l 1)).
destruct v; auto.
intro.
assert (h = false) as hf by auto; rewrite hf.
simpl.
unfold add_aux.
change (
nat_to_bvec (S n)
nat_to_bvec (S n0)
(Z.to_nat
(mod1
(Z.of_nat (2 * (bvec_to_nat n v)) +
Z.of_nat (1 + 2 * (bvec_to_nat n (nat_to_bvec n 0))))
(Pow2int.pow2 (Z.of_nat (S n))))) =
true :: Vector.map2 (fun x y : bool => x || y) v (nat_to_bvec n 0)).
(Z.of_nat (2 * (bvec_to_nat n0 v)) +
Z.of_nat (1 + 2 * (bvec_to_nat n0 (nat_to_bvec n0 0))))
(Pow2int.pow2 (Z.of_nat (S n0))))) =
true :: Vector.map2 (fun x y : bool => x || y) v (nat_to_bvec n0 0)).
rewrite <-Nat_to_bvec_zeros, bvec_to_nat_zeros.
change (Z.of_nat (1 + 2 * 0)) with 1.
set (mod1 (Z.of_nat (2 * bvec_to_nat n v) + 1)
(Pow2int.pow2 (Z.of_nat (S n)))).
set (mod1 (Z.of_nat (2 * bvec_to_nat n0 v) + 1)
(Pow2int.pow2 (Z.of_nat (S n0)))).
simpl nat_to_bvec.
rewrite Z2Nat.id by (apply mod1_nat, Z.lt_le_pred, max_int_nat).
assert (Z.odd z = true).
subst z.
rewrite Zodd_mod, mod1_is_mod by auto with zarith.
rewrite Nat2Z.inj_succ, <- Z.add_1_r, Pow2int.Power_s by auto with zarith.
rewrite Int.Comm1, (mod_mod_mult _ 2 _)by auto with zarith.
rewrite <-Zodd_mod, Int.Comm, Nat2Z.inj_mul, Z.odd_add_mul_2; trivial.
assert (H0: Z.odd z = true).
subst z.
rewrite Zodd_mod, mod1_is_mod by auto with zarith.
rewrite Nat2Z.inj_succ, <- Z.add_1_r, Pow2int.Power_s by auto with zarith.
rewrite Int.Comm1, (mod_mod_mult _ 2 _)by auto with zarith.
rewrite <-Zodd_mod, Int.Comm, Nat2Z.inj_mul, Z.odd_add_mul_2; trivial.
rewrite H0.
cut (nat_to_bvec n (Div2.div2 (Z.to_nat z))
= Vector.map2 (fun x y : bool => x || y) v (Vector.const false n)).
cut (nat_to_bvec n0 (Div2.div2 (Z.to_nat z))
= Vector.map2 (fun x y : bool => x || y) v (Vector.const false n0)).
intro t; rewrite t; trivial.
case (Z_lt_le_dec (Z.of_nat (2 * bvec_to_nat n v) + 1) (Pow2int.pow2 (Z.of_nat (S n)))); intro.
case (Z_lt_le_dec (Z.of_nat (2 * bvec_to_nat n0 v) + 1) (Pow2int.pow2 (Z.of_nat (S n0)))); intro.
subst z.
revert H0.
rewrite mod1_out by auto with zarith.
......@@ -1762,25 +1773,24 @@ Lemma mask_succ_tmp :
rewrite <-Nat2Z.inj_succ, Nat2Z.id.
rewrite Z.odd_succ, <-even_is_even in H0.
rewrite <-(Div2.even_div2 _ H0), Div2.div2_double.
Lemma nat_to_bvec_bvec_to_nat:
forall {l} v, nat_to_bvec l (bvec_to_nat l v) = v.
assert (nat_to_bvec_bvec_to_nat:
forall {l} v, nat_to_bvec l (bvec_to_nat l v) = v).
intros; apply bvec_to_nat_extensionality.
apply bvec_to_nat_nat_to_bvec.
apply Z.lt_le_pred.
rewrite <-Z2Nat.id by (transitivity (Pow2int.pow2 (Z.of_nat l) - 1); [apply max_int_nat|auto with zarith]).
rewrite <-Z2Nat.id by (transitivity (Pow2int.pow2 (Z.of_nat l0) - 1);
[apply max_int_nat|auto with zarith]).
apply inj_lt, bvec_to_nat_range.
Qed.
rewrite nat_to_bvec_bvec_to_nat.
Lemma tmp2:
assert (tmp2:
forall {l} v,
Vector.map2 (fun x y : bool => x || y) v (Vector.const false l) = v.
induction v; auto.
Vector.map2 (fun x y : bool => x || y) v (Vector.const false l) = v).
induction v0; auto.
simpl.
rewrite orb_false_r.
rewrite IHv; trivial.
Qed.
rewrite IHv0; trivial.
symmetry; apply tmp2.
absurd (Z.of_nat (bvec_to_nat n v) < Pow2int.pow2 (Z.of_nat n)).
absurd (Z.of_nat (bvec_to_nat n0 v) < Pow2int.pow2 (Z.of_nat n0)).
apply Zle_not_lt.
rewrite Nat2Z.inj_succ in l.
rewrite <- Z.add_1_r, Pow2int.Power_s in l by auto with zarith.
......@@ -1794,15 +1804,13 @@ Lemma mask_succ_tmp :
rewrite Z2Nat.inj_lt, Nat2Z.id.
apply (bvec_to_nat_range v).
auto with zarith.
transitivity (Pow2int.pow2 (Z.of_nat n) - 1).
transitivity (Pow2int.pow2 (Z.of_nat n0) - 1).
apply max_int_nat.
auto with zarith.
Qed.
intros.
rewrite add_is_add_aux.
apply add_and_or_aux.
trivial.
Qed.
simpl.
apply add_and_or.
intros; apply Lsl_nth_low; auto with zarith.
......@@ -2016,3 +2024,4 @@ Lemma Extensionality : forall (x:t) (y:t), (eq_sub x y 0%Z size) -> (x = y).
intros x y.
apply Extensionality_aux.
Qed.
This diff is collapsed.
This diff is collapsed.
......@@ -15,12 +15,6 @@ Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
(* Why3 goal *)
Definition pow2: Z -> Z.
exact (two_p).
......
......@@ -21,10 +21,10 @@ Require Import ZArith.
Require Import Fourier.
Require Import real.Truncate.
Implicit Arguments B754_zero [[prec] [emax]].
Implicit Arguments B754_infinity [[prec] [emax]].
Implicit Arguments B754_nan [[prec] [emax]].
Implicit Arguments B754_finite [[prec] [emax]].
Arguments B754_zero {prec} {emax}.
Arguments B754_infinity {prec} {emax}.
Arguments B754_nan {prec} {emax}.
Arguments B754_finite {prec} {emax}.
(* Why3 assumption *)
Inductive mode :=
......@@ -52,7 +52,10 @@ Defined.
Coercion mode_to_IEEE : mode >-> Fappli_IEEE.mode.
Variable eb_pos sb_pos : positive.
Local Axiom eb_pos sb_pos : positive.
(* Important notice: do not remove 'Local' above, otherwise 'why3 realize' will
assume it comes from Why3 and will remove it. We use 'Axiom' instead of
'Hypothesis' to avoid a Coq warning *)
(* Why3 goal *)
Definition eb: Z.
......@@ -64,8 +67,8 @@ Definition sb: Z.
exact (Z.pos sb_pos).
Defined.
Hypothesis Heb : Zlt_bool 1 eb = true.
Hypotheses Hsbb : Zlt_bool 1 sb = true.
Local Axiom Heb : Zlt_bool 1 eb = true.
Local Axiom Hsbb : Zlt_bool 1 sb = true.