Add a Coq realization for real.PowerInt.

Makefile.in

@@ -869,7 +869,7 @@ COQLIBS_INT_FILES = Abs ComputerDivision Div2 EuclideanDivision Int MinMax Power
 COQLIBS_INT_ALL_FILES = Exponentiation $(COQLIBS_INT_FILES)
 COQLIBS_INT = $(addprefix lib/coq/int/, $(COQLIBS_INT_ALL_FILES))
 
-COQLIBS_REAL_FILES = Abs ExpLog FromInt MinMax Real Square RealInfix
+COQLIBS_REAL_FILES = Abs ExpLog FromInt MinMax PowerInt Real Square RealInfix
 COQLIBS_REAL = $(addprefix lib/coq/real/, $(COQLIBS_REAL_FILES))
 
 COQLIBS_NUMBER_FILES = Divisibility Gcd Parity Prime

lib/coq/real/PowerInt.v

+(* This file is generated by Why3's Coq driver *)
+(* Beware! Only edit allowed sections below    *)
+Require Import BuiltIn.
+Require Import Rfunctions.
+Require BuiltIn.
+Require int.Int.
+Require real.Real.
+
+Require Import Exponentiation.
+
+(* Why3 goal *)
+Notation power := powerRZ.
+
+Lemma power_is_exponentiation :
+  forall x n, (0 <= n)%Z -> power x n = Exponentiation.power _ R1 Rmult x n.
+Proof.
+intros x [|n|n] H.
+easy.
+2: now elim H.
+unfold Exponentiation.power, powerRZ.
+simpl.
+induction (nat_of_P n).
+easy.
+simpl.
+now rewrite IHn0.
+Qed.
+
+(* Why3 goal *)
+Lemma Power_0 : forall (x:R), ((power x 0%Z) = 1%R).
+Proof.
+intros x.
+easy.
+Qed.
+
+(* Why3 goal *)
+Lemma Power_s : forall (x:R) (n:Z), (0%Z <= n)%Z -> ((power x
+  (n + 1%Z)%Z) = (x * (power x n))%R).
+Proof.
+intros x n h1.
+rewrite 2!power_is_exponentiation by auto with zarith.
+now apply Power_s.
+Qed.
+
+(* Why3 goal *)
+Lemma Power_1 : forall (x:R), ((power x 1%Z) = x).
+Proof.
+exact Rmult_1_r.
+Qed.
+
+(* Why3 goal *)
+Lemma Power_sum : forall (x:R) (n:Z) (m:Z), (0%Z <= n)%Z -> ((0%Z <= m)%Z ->
+  ((power x (n + m)%Z) = ((power x n) * (power x m))%R)).
+Proof.
+intros x n m h1 h2.
+rewrite 3!power_is_exponentiation by auto with zarith.
+apply Power_sum ; auto with real.
+Qed.
+
+(* Why3 goal *)
+Lemma Power_mult : forall (x:R) (n:Z) (m:Z), (0%Z <= n)%Z -> ((0%Z <= m)%Z ->
+  ((power x (n * m)%Z) = (power (power x n) m))).
+Proof.
+intros x n m h1 h2.
+rewrite 3!power_is_exponentiation by auto with zarith.
+apply Power_mult ; auto with real.
+Qed.
+
+(* Why3 goal *)
+Lemma Power_mult2 : forall (x:R) (y:R) (n:Z), (0%Z <= n)%Z ->
+  ((power (x * y)%R n) = ((power x n) * (power y n))%R).
+Proof.
+intros x y n h1.
+rewrite 3!power_is_exponentiation by auto with zarith.
+apply Power_mult2 ; auto with real.
+Qed.
+
+

theories/real.why

@@ -236,7 +236,9 @@ theory PowerInt
   use Real
 
   clone export int.Exponentiation with
-    type t = real, constant one = Real.one, function (*) = Real.(*)
+    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
 
 end