Commit 4c763af2 authored by MARCHE Claude's avatar MARCHE Claude

Added a lemma on real.PowerInt.power + updated Coq realizations

parent 69dc560d
This diff is collapsed.
......@@ -20,7 +20,7 @@
name="pow_eps2_max_int"
locfile="tests-provers/coq-interval/../coq-interval.why"
loclnum="6" loccnumb="7" loccnume="23"
sum="b5f712d3c2d0add5ba666a70b3ff7137"
sum="a75e748716f4cb7390dac252de8caf94"
proved="true"
expanded="true"
shape="ainfix <=apowerainfix +c1.0ainfix +c0x7.p-50c0x3.p-53c2147483647c2.0">
......@@ -31,7 +31,7 @@
edited="coqmninterval_P_pow_eps2_max_int_1.v"
obsolete="false"
archived="false">
<result status="valid" time="2.36"/>
<result status="valid" time="2.32"/>
</proof>
</goal>
</theory>
......
(* 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 Import Rbasic_fun.
Require BuiltIn.
Require int.Int.
Require real.Real.
Require real.Abs.
......
(* 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 Import floating_point.GenFloat.
......
(* 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.
(* Why3 assumption *)
Inductive mode :=
......@@ -10,5 +10,7 @@ Inductive mode :=
| Up : mode
| Down : mode
| NearestTiesToAway : mode .
Axiom mode_WhyType : WhyType mode.
Existing Instance mode_WhyType.
(* 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 Import Rbasic_fun.
Require BuiltIn.
Require int.Int.
Require real.Real.
Require real.Abs.
......
(* 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 Import floating_point.GenFloat.
......
(* 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 goal *)
......
(* 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 Import ZOdiv.
Require BuiltIn.
Require int.Int.
Require int.Abs.
......
(* 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.
Require int.Abs.
......
......@@ -52,6 +52,14 @@ fold (Zsucc n).
now rewrite Zabs_nat_Zsucc.
Qed.
(* Why3 goal *)
Lemma Power_s_alt : forall (x:t) (n:Z), (0%Z < n)%Z -> ((power x
n) = (infix_as x (power x (n - 1%Z)%Z))).
intros x n h1.
rewrite <- Power_s; auto with zarith.
f_equal; omega.
Qed.
(* Why3 goal *)
Lemma Power_1 : forall (x:t), ((power x 1%Z) = x).
Proof.
......
(* 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 goal *)
......
......@@ -38,6 +38,15 @@ now apply Zle_ge.
easy.
Qed.
(* Why3 goal *)
Lemma Power_s_alt : forall (x:Z) (n:Z), (0%Z < n)%Z -> ((power x
n) = (x * (power x (n - 1%Z)%Z))%Z).
intros x n h1.
rewrite <- Power_s.
f_equal; auto with zarith.
omega.
Qed.
(* Why3 goal *)
Lemma Power_1 : forall (x:Z), ((power x 1%Z) = x).
Proof.
......
(* 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 Import ZOdiv.
Require BuiltIn.
Require int.Int.
Require int.Abs.
Require int.EuclideanDivision.
......
(* 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 Import ZOdiv.
Require BuiltIn.
Require int.Int.
Require int.Abs.
Require int.EuclideanDivision.
......
(* 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 *)
......
(* 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 Import ZOdiv.
Require BuiltIn.
Require int.Int.
Require int.Abs.
Require int.EuclideanDivision.
......
(* 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 Import Rbasic_fun.
Require BuiltIn.
Require real.Real.
(* Why3 goal *)
......
(* 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 Import Rtrigo_def.
Require Import Rpower.
Require BuiltIn.
Require real.Real.
(* Why3 goal *)
......
(* 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.
Require real.Real.
......
(* 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 real.Real.
Require Import Rbasic_fun.
......
......@@ -5,6 +5,7 @@ Require Import Rfunctions.
Require BuiltIn.
Require int.Int.
Require real.Real.
Require real.RealInfix.
Require Import Exponentiation.
......@@ -41,6 +42,15 @@ rewrite 2!power_is_exponentiation by auto with zarith.
now apply Power_s.
Qed.
(* Why3 goal *)
Lemma Power_s_alt : forall (x:R) (n:Z), (0%Z < n)%Z -> ((power x
n) = (x * (power x (n - 1%Z)%Z))%R).
intros x n h1.
rewrite <- Power_s.
f_equal; omega.
omega.
Qed.
(* Why3 goal *)
Lemma Power_1 : forall (x:R), ((power x 1%Z) = x).
Proof.
......@@ -74,4 +84,22 @@ rewrite 3!power_is_exponentiation by auto with zarith.
apply Power_mult2 ; auto with real.
Qed.
(* Why3 goal *)
Lemma Pow_ge_one : forall (x:R) (n:Z), ((0%Z <= n)%Z /\ (1%R <= x)%R) ->
(1%R <= (power x n))%R.
intros x n (h1,h2).
generalize h1.
pattern n; apply Z_lt_induction; auto.
clear n h1; intros n Hind h1.
assert (h: (n = 0 \/ 0 < n)%Z) by omega.
destruct h.
subst n; rewrite Power_0; auto with *.
replace n with ((n-1)+1)%Z by omega.
rewrite Power_s; auto with zarith.
assert (h : (1 <= power x (n-1))%R).
apply Hind; omega.
replace 1%R with (1*1)%R by auto with real.
apply Rmult_le_compat; auto with real.
Qed.
(* 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 real.Real.
(* 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 Import R_sqrt.
Require BuiltIn.
Require real.Real.
(* Why3 assumption *)
......
......@@ -232,14 +232,17 @@ end
theory PowerInt
use int.Int
use Real
use import int.Int
use import RealInfix
clone export int.Exponentiation with
type t = real, constant one = Real.one, function (*) = Real.(*),
goal CommutativeMonoid.Assoc, goal CommutativeMonoid.Unit_def_l,
goal CommutativeMonoid.Unit_def_r, goal CommutativeMonoid.Comm.Comm
lemma Pow_ge_one:
forall x:real, n:int. 0 <= n /\ 1.0 <=. x -> 1.0 <=. power x n
end
(** {2 Power of a real to a real exponent} *)
......
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