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

proofs using the improved interval tactic

parent 2d5f8cef
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Require Import Rfunctions.
Require real.Real.
Require int.Int.
Axiom Power_s : forall (x:R) (n:Z), (0%Z <= n)%Z ->
((powerRZ x (n + 1%Z)%Z) = (x * (powerRZ x n))%R).
Axiom Power_sum : forall (x:R) (n:Z) (m:Z), ((0%Z <= n)%Z /\ (0%Z <= m)%Z) ->
((powerRZ x (n + m)%Z) = ((powerRZ x n) * (powerRZ x m))%R).
Axiom Power_mult : forall (x:R) (n:Z) (m:Z), (0%Z <= n)%Z -> ((0%Z <= m)%Z ->
((powerRZ x (n * m)%Z) = (powerRZ (powerRZ x n) m))).
Require Import Interval_tactic.
(* Why3 goal *)
Theorem pow_eps2_max_int : ((powerRZ (1%R + ((7 / 1125899906842624)%R + (3 / 9007199254740992)%R)%R)%R 2147483647%Z) <= 2%R)%R.
Strategy 1000 [powerRZ].
interval with (i_prec 34).
Qed.
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/usr/local/share/why3/why3session.dtd">
<why3session
name="coq-interval/why3session.xml">
<prover
id="0"
name="Coq"
version="8.3pl3"/>
<file
name="../coq-interval.why"
verified="true"
expanded="true">
<theory
name="P"
locfile="coq-interval/../coq-interval.why"
loclnum="1" loccnumb="7" loccnume="8"
verified="true"
expanded="true">
<goal
name="pow_eps2_max_int"
locfile="coq-interval/../coq-interval.why"
loclnum="6" loccnumb="7" loccnume="23"
sum="9751302b92e170e5fd1ee453a899e142"
proved="true"
expanded="true"
shape="ainfix &lt;=apowerainfix +c1.0ainfix +c0x7.p-50c0x3.p-53c2147483647c2.0">
<proof
prover="0"
timelimit="20"
memlimit="1000"
edited="coqmninterval_P_pow_eps2_max_int_1.v"
obsolete="false"
archived="false">
<result status="valid" time="4.06"/>
</proof>
</goal>
</theory>
</file>
</why3session>
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment