Skip to content

GitLab

why3
why3
Commit 4b4da5ee authored by MARCHE Claude's avatar MARCHE Claude
Browse files
Options

Improved theory real.PowerReal, compatible with MetiTarski, and with a Coq realization

parent 329f88f1
Hide whitespace changes
Inline Side-by-side
Showing with 464 additions and 533 deletions
Makefile.in
View file @ 4b4da5ee
......@@ -847,7 +847,7 @@ COQLIBS_INT = $(addprefix lib/coq/int/, $(COQLIBS_INT_ALL_FILES))
COQLIBS_BOOL_FILES = Bool
COQLIBS_BOOL = $(addprefix lib/coq/bool/, $(COQLIBS_BOOL_FILES))
COQLIBS_REAL_FILES = Abs ExpLog FromInt MinMax PowerInt Real RealInfix Square Trigonometry
COQLIBS_REAL_FILES = Abs ExpLog FromInt MinMax PowerInt PowerReal Real RealInfix Square Trigonometry
COQLIBS_REAL = $(addprefix lib/coq/real/, $(COQLIBS_REAL_FILES))
COQLIBS_NUMBER_FILES = Divisibility Gcd Parity Prime Coprime
......
ROADMAP
View file @ 4b4da5ee
......@@ -165,7 +165,7 @@ support for Yices2 recent
-> DONE: 2.3.0, but still does not support quantifiers
solve issues with metitarski
. theory PowerReal
. DONE theory PowerReal
. crashes when applied on a WP (see examples/my_cosine.mlw)
clean up the support for SMTLIB bitvectors
......
drivers/metitarski.drv
View file @ 4b4da5ee
......@@ -222,8 +222,8 @@ theory real.PowerReal
prelude "include('Axioms/pow.ax')."
(* These follow from Metitarski's axioms. *)
remove prop Pow_def
remove prop Pow_one_y
remove prop Pow_exp_log
end
(* support for integers disabled because may be inconsistent
......
examples/tests-provers/metitarski/why3session.xml
View file @ 4b4da5ee
......@@ -8,31 +8,38 @@
<theory name="P" sum="1d04567a049f848cb57260f3bbd2cdfa" expanded="true">
<goal name="x_mul_x_pos" expanded="true">
<proof prover="0" memlimit="1000"><result status="valid" time="0.00"/></proof>
<proof prover="1"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="sqr_pos" expanded="true">
<proof prover="0" timelimit="5"><result status="valid" time="0.01"/></proof>
<proof prover="1"><result status="valid" time="0.00"/></proof>
</goal>
</theory>
<theory name="P2" sum="4c1a6e36bab92d102d254173153460e3" expanded="true">
<goal name="sqr_pos" expanded="true">
<proof prover="0" memlimit="1000"><result status="valid" time="0.05"/></proof>
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
</theory>
<theory name="P3" sum="bbf0c651ac8241eae35a2ee034b75f93" expanded="true">
<goal name="cos_bound" expanded="true">
<proof prover="0" memlimit="1000"><result status="unknown" time="2.62"/></proof>
<proof prover="1"><result status="unknown" time="1.86"/></proof>
</goal>
<goal name="cos_bound_harder" expanded="true">
<proof prover="0" memlimit="1000"><result status="valid" time="0.19"/></proof>
<proof prover="1"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="MethodErrorOK" expanded="true">
<proof prover="0" memlimit="1000"><result status="valid" time="0.15"/></proof>
<proof prover="1"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="MethodErrorWrong" expanded="true">
<proof prover="0" memlimit="1000"><result status="unknown" time="3.24"/></proof>
<proof prover="1"><result status="unknown" time="4.14"/></proof>
</goal>
</theory>
<theory name="Power" sum="f1807c022587c3770e4e7984d0a322b9" expanded="true">
<theory name="Power" sum="99784816af5084fd1d900784082e2924" expanded="true">
<goal name="G" expanded="true">
<proof prover="1"><result status="unknown" time="0.17"/></proof>
</goal>
......@@ -40,7 +47,7 @@
<proof prover="1"><result status="unknown" time="0.19"/></proof>
</goal>
<goal name="G2" expanded="true">
<proof prover="1" edited="metitarski-Power-G2_1.tptp"><result status="unknown" time="0.20"/></proof>
<proof prover="1"><result status="unknown" time="0.23"/></proof>
</goal>
</theory>
</file>
......
lib/coq/bool/Bool.v
View file @ 4b4da5ee
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2015 -- 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.
Require BuiltIn.
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
......
lib/coq/floating_point/Double.v
View file @ 4b4da5ee
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2015 -- 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.
Require Reals.Rbasic_fun.
Require BuiltIn.
Require int.Int.
Require real.Real.
Require real.Abs.
Require real.FromInt.
Require floating_point.Rounding.
Require floating_point.DoubleFormat.
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
......
lib/coq/floating_point/DoubleFormat.v
View file @ 4b4da5ee
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2015 -- 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.
Require BuiltIn.
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
......
lib/coq/floating_point/Rounding.v
View file @ 4b4da5ee
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2015 -- 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.
Require BuiltIn.
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
......
lib/coq/floating_point/Single.v
View file @ 4b4da5ee
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2015 -- 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.
Require Reals.Rbasic_fun.
Require BuiltIn.
Require int.Int.
Require real.Real.
Require real.Abs.
Require real.FromInt.
Require floating_point.Rounding.
Require floating_point.SingleFormat.
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
......
lib/coq/floating_point/SingleFormat.v
View file @ 4b4da5ee
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2015 -- 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.
Require BuiltIn.
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
......
lib/coq/int/Abs.v
View file @ 4b4da5ee
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2015 -- 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.
Require BuiltIn.
Require int.Int.
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
......
lib/coq/int/ComputerDivision.v
View file @ 4b4da5ee
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2015 -- 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.
Require BuiltIn.
Require int.Int.
Require int.Abs.
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
......
lib/coq/int/Div2.v
View file @ 4b4da5ee
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2015 -- 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.
Require BuiltIn.
Require int.Int.
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
......
lib/coq/int/EuclideanDivision.v
View file @ 4b4da5ee
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2015 -- 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.
Require BuiltIn.
Require int.Int.
Require int.Abs.
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
......
lib/coq/int/Exponentiation.v
View file @ 4b4da5ee
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2015 -- 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.
Require BuiltIn.
Require int.Int.
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
......
lib/coq/int/Int.v
View file @ 4b4da5ee
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2015 -- 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.
Require BuiltIn.
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
......
lib/coq/int/MinMax.v
View file @ 4b4da5ee
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2015 -- 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.
Require BuiltIn.
Require int.Int.
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
......
lib/coq/int/Power.v
View file @ 4b4da5ee
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2015 -- 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.
Require BuiltIn.
Require int.Int.
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
......
lib/coq/list/Append.v
View file @ 4b4da5ee
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2015 -- 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.
Require BuiltIn.
Require int.Int.
Require list.List.
Require list.Length.
Require list.Mem.
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
......
lib/coq/list/Combine.v
View file @ 4b4da5ee
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2015 -- 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.
Require BuiltIn.
Require list.List.
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
......
lib/coq/list/Distinct.v
View file @ 4b4da5ee
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2015 -- 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.
Require BuiltIn.
Require int.Int.
Require list.List.
Require list.Length.
Require list.Mem.
Require list.Append.
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
......
lib/coq/list/HdTl.v
View file @ 4b4da5ee
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2015 -- 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.
Require BuiltIn.
Require list.List.
Require option.Option.
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
......
lib/coq/list/HdTlNoOpt.v
View file @ 4b4da5ee
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2015 -- 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.
Require BuiltIn.
Require list.List.
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
......
lib/coq/list/Length.v
View file @ 4b4da5ee
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2015 -- 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.
Require BuiltIn.
Require int.Int.
Require list.List.
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
......
lib/coq/list/List.v
View file @ 4b4da5ee
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2015 -- 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.
Require BuiltIn.
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
......
lib/coq/list/Mem.v
View file @ 4b4da5ee
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2015 -- 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.
Require BuiltIn.
Require list.List.
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
......
lib/coq/list/Nth.v
View file @ 4b4da5ee
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2015 -- 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.
Require BuiltIn.
Require int.Int.
Require list.List.
Require option.Option.
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
......
lib/coq/list/NthHdTl.v
View file @ 4b4da5ee
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2015 -- 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.
Require BuiltIn.
Require int.Int.
Require list.List.
Require list.Nth.
Require option.Option.
Require list.HdTl.
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
......
lib/coq/list/NthLength.v
View file @ 4b4da5ee
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2015 -- 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.
Require BuiltIn.
Require int.Int.
Require list.List.
Require list.Length.
Require list.Nth.
Require option.Option.