From c295f0772c77b5335c70b59f8e01efd064cabd61 Mon Sep 17 00:00:00 2001
From: Jean-Christophe <Jean-Christophe.Filliatre@lri.fr>
Date: Thu, 26 Jul 2012 01:46:27 +0200
Subject: [PATCH] simplified example power, by making use of int.Power Coq
 realization for int.Power (mostly to keep Coq proofs that were in power.mlw)

---
 Makefile.in                                   |   2 +-
 examples/programs/power.mlw                   |  27 +-
 ...wer_M_WP_parameter_fast_exp_imperative_1.v |  54 ++++
 .../power/power_Power_Power_mult2_1.v         |  60 ----
 .../programs/power/power_Power_Power_mult_1.v |  55 ----
 .../programs/power/power_Power_Power_sum_1.v  |  41 ---
 ..._WP_M_WP_parameter_fast_exp_imperative_3.v |  62 ++--
 examples/programs/power/why3session.xml       | 268 +++++++-----------
 lib/coq/int/Power.v                           |  95 +++++++
 modules/array.mlw                             |   1 +
 theories/int.why                              |   5 +-
 11 files changed, 278 insertions(+), 392 deletions(-)
 create mode 100644 examples/programs/power/power_M_WP_parameter_fast_exp_imperative_1.v
 delete mode 100644 examples/programs/power/power_Power_Power_mult2_1.v
 delete mode 100644 examples/programs/power/power_Power_Power_mult_1.v
 delete mode 100644 examples/programs/power/power_Power_Power_sum_1.v
 create mode 100644 lib/coq/int/Power.v

diff --git a/Makefile.in b/Makefile.in
index bbc7400c6..b06c9be09 100644
--- a/Makefile.in
+++ b/Makefile.in
@@ -877,7 +877,7 @@ endif
 
 ifeq (@enable_coq_libs@,yes)
 
-COQLIBS_INT_FILES = Abs ComputerDivision EuclideanDivision Int MinMax
+COQLIBS_INT_FILES = Abs ComputerDivision EuclideanDivision Int MinMax Power
 COQLIBS_INT = $(addprefix lib/coq/int/, $(COQLIBS_INT_FILES))
 
 COQLIBS_REAL_FILES = Abs ExpLog FromInt MinMax Real Square RealInfix
diff --git a/examples/programs/power.mlw b/examples/programs/power.mlw
index d48919646..3d3a06dc8 100644
--- a/examples/programs/power.mlw
+++ b/examples/programs/power.mlw
@@ -1,32 +1,11 @@
 
-theory Power
+(* fast exponentiation *)
 
-  use import int.Int
-
-  function power int int : int
-
-  axiom Power_0 : forall x : int. power x 0 = 1
-
-  axiom Power_s : forall x n : int. 0 < n -> power x n = x * power x (n-1)
-
-  lemma Power_1 : forall x : int. power x 1 = x
-
-  lemma Power_sum : forall x n m : int. 0 <= n -> 0 <= m ->
-    power x (n + m) = power x n * power x m
-
-  lemma Power_mult : forall x n m : int. 0 <= n -> 0 <= m ->
-    power x (n * m) = power (power x n) m
-
-  lemma Power_mult2 : forall x y n : int. 0 <= n ->
-    power (x * y) n = power x n * power y n
-
-end
-
-module M
+module FastExponentiation
 
   use import int.Int
+  use import int.Power
   use import int.ComputerDivision
-  use import Power
 
   (* recursive implementation *)
 
diff --git a/examples/programs/power/power_M_WP_parameter_fast_exp_imperative_1.v b/examples/programs/power/power_M_WP_parameter_fast_exp_imperative_1.v
new file mode 100644
index 000000000..46f0778d7
--- /dev/null
+++ b/examples/programs/power/power_M_WP_parameter_fast_exp_imperative_1.v
@@ -0,0 +1,54 @@
+(* This file is generated by Why3's Coq driver *)
+(* Beware! Only edit allowed sections below    *)
+Require Import ZArith.
+Require Import Rbase.
+Require Import ZOdiv.
+Require int.Int.
+Require int.Abs.
+Require int.ComputerDivision.
+Require int.Power.
+
+(* Why3 assumption *)
+Definition unit  := unit.
+
+(* Why3 assumption *)
+Inductive ref (a:Type) :=
+  | mk_ref : a -> ref a.
+Implicit Arguments mk_ref.
+
+(* Why3 assumption *)
+Definition contents (a:Type)(v:(ref a)): a :=
+  match v with
+  | (mk_ref x) => x
+  end.
+Implicit Arguments contents.
+
+Import int.ComputerDivision.
+Import Power.
+
+(* Why3 goal *)
+Theorem WP_parameter_fast_exp_imperative : forall (x:Z) (n:Z),
+  (0%Z <= n)%Z -> forall (e:Z) (p:Z) (r:Z), ((0%Z <= e)%Z /\
+  ((r * (int.Power.power p e))%Z = (int.Power.power x n))) -> ((0%Z < e)%Z ->
+  (((ZOmod e 2%Z) = 1%Z) -> forall (r1:Z), (r1 = (r * p)%Z) -> forall (p1:Z),
+  (p1 = (p * p)%Z) -> forall (e1:Z), (e1 = (ZOdiv e 2%Z)) ->
+  ((r1 * (int.Power.power p1 e1))%Z = (int.Power.power x n)))).
+intros x n h1 e p r (h2,h3) h4 h5 r1 h6 p1 h7 e1 h8.
+subst.
+assert (h: (2 <> 0)%Z) by omega.
+generalize (Div_mod e 2 h). clear h.
+assert (h: (0 < 2)%Z) by omega.
+generalize (Div_bound e 2 (conj h2 h)). clear h.
+rewrite h5; clear h5.
+intros.
+rewrite <- h3; clear h3.
+rewrite H0 at 2. clear H0.
+rewrite Power_sum. 2:omega.
+replace (2 * (e / 2))%Z with (e/2 + e/2)%Z by omega.
+rewrite Power_sum. 2:omega.
+rewrite Power_mult2. 2:omega.
+rewrite Power_1.
+ring.
+Qed.
+
+
diff --git a/examples/programs/power/power_Power_Power_mult2_1.v b/examples/programs/power/power_Power_Power_mult2_1.v
deleted file mode 100644
index 57a4d5610..000000000
--- a/examples/programs/power/power_Power_Power_mult2_1.v
+++ /dev/null
@@ -1,60 +0,0 @@
-(* This file is generated by Why3's Coq driver *)
-(* Beware! Only edit allowed sections below    *)
-Require Import ZArith.
-Require Import Rbase.
-Definition unit  := unit.
-
-Parameter ignore: forall (a:Type), a  -> unit.
-
-Implicit Arguments ignore.
-
-Parameter label_ : Type.
-
-Parameter at1: forall (a:Type), a -> label_  -> a.
-
-Implicit Arguments at1.
-
-Parameter old: forall (a:Type), a  -> a.
-
-Implicit Arguments old.
-
-Parameter power: Z -> Z  -> Z.
-
-
-Axiom Power_0 : forall (x:Z), ((power x 0%Z) = 1%Z).
-
-Axiom Power_s : forall (x:Z) (n:Z), (0%Z <  n)%Z -> ((power x
-  n) = (x * (power x (n - 1%Z)%Z))%Z).
-
-Axiom Power_1 : forall (x:Z), ((power x 1%Z) = x).
-
-Axiom Power_sum : forall (x:Z) (n:Z) (m:Z), (0%Z <= n)%Z -> ((0%Z <= m)%Z ->
-  ((power x (n + m)%Z) = ((power x n) * (power x m))%Z)).
-
-Axiom Power_mult : forall (x:Z) (n:Z) (m:Z), (0%Z <= n)%Z -> ((0%Z <= m)%Z ->
-  ((power x (n * m)%Z) = (power (power x n) m))).
-
-Theorem Power_mult2 : forall (x:Z) (y:Z) (n:Z), (0%Z <= n)%Z ->
-  ((power (x * y)%Z n) = ((power x n) * (power y n))%Z).
-(* YOU MAY EDIT THE PROOF BELOW *)
-intros x y n Hn.
-generalize Hn.
-pattern n.
-apply natlike_ind; auto.
-intros; do 3 rewrite Power_0.
-omega.
-intros.
-rewrite Power_s.
-2:omega.
-rewrite (Power_s x (Zsucc x0)).
-rewrite (Power_s y (Zsucc x0)).
-replace (Zsucc x0 - 1)%Z with x0 by omega.
-rewrite H0.
-ring.
-omega.
-omega.
-omega.
-Qed.
-(* DO NOT EDIT BELOW *)
-
-
diff --git a/examples/programs/power/power_Power_Power_mult_1.v b/examples/programs/power/power_Power_Power_mult_1.v
deleted file mode 100644
index b93242742..000000000
--- a/examples/programs/power/power_Power_Power_mult_1.v
+++ /dev/null
@@ -1,55 +0,0 @@
-(* This file is generated by Why3's Coq driver *)
-(* Beware! Only edit allowed sections below    *)
-Require Import ZArith.
-Require Import Rbase.
-Definition unit  := unit.
-
-Parameter ignore: forall (a:Type), a  -> unit.
-
-Implicit Arguments ignore.
-
-Parameter label_ : Type.
-
-Parameter at1: forall (a:Type), a -> label_  -> a.
-
-Implicit Arguments at1.
-
-Parameter old: forall (a:Type), a  -> a.
-
-Implicit Arguments old.
-
-Parameter power: Z -> Z  -> Z.
-
-
-Axiom Power_0 : forall (x:Z), ((power x 0%Z) = 1%Z).
-
-Axiom Power_s : forall (x:Z) (n:Z), (0%Z <  n)%Z -> ((power x
-  n) = (x * (power x (n - 1%Z)%Z))%Z).
-
-Axiom Power_1 : forall (x:Z), ((power x 1%Z) = x).
-
-Axiom Power_sum : forall (x:Z) (n:Z) (m:Z), (0%Z <= n)%Z -> ((0%Z <= m)%Z ->
-  ((power x (n + m)%Z) = ((power x n) * (power x m))%Z)).
-
-Theorem Power_mult : forall (x:Z) (n:Z) (m:Z), (0%Z <= n)%Z ->
-  ((0%Z <= m)%Z -> ((power x (n * m)%Z) = (power (power x n) m))).
-(* YOU MAY EDIT THE PROOF BELOW *)
-intros x n m Hn Hm.
-generalize Hm.
-pattern m.
-apply Z_lt_induction; auto.
-intros n0 Hind Hn0.
-assert (h:(n0 = 0 \/ n0 > 0)%Z) by omega.
-destruct h.
-subst n0; rewrite Power_0; ring_simplify (n * 0)%Z.
-apply Power_0.
-replace (n*n0)%Z with (n*(n0-1)+n)%Z by ring.
-rewrite Power_sum; auto with zarith.
-rewrite Hind; auto with zarith.
-rewrite <- (Power_1 (power x n)) at 2.
-rewrite <- Power_sum; auto with zarith.
-ring_simplify (n0 - 1 + 1)%Z; auto.
-Qed.
-(* DO NOT EDIT BELOW *)
-
-
diff --git a/examples/programs/power/power_Power_Power_sum_1.v b/examples/programs/power/power_Power_Power_sum_1.v
deleted file mode 100644
index a14e866bb..000000000
--- a/examples/programs/power/power_Power_Power_sum_1.v
+++ /dev/null
@@ -1,41 +0,0 @@
-(* This file is generated by Why3's Coq driver *)
-(* Beware! Only edit allowed sections below    *)
-Require Import ZArith.
-Require Import Rbase.
-Require int.Int.
-
-Parameter power: Z -> Z -> Z.
-
-Axiom Power_0 : forall (x:Z), ((power x 0%Z) = 1%Z).
-
-Axiom Power_s : forall (x:Z) (n:Z), (0%Z <  n)%Z -> ((power x
-  n) = (x * (power x (n - 1%Z)%Z))%Z).
-
-Axiom Power_1 : forall (x:Z), ((power x 1%Z) = x).
-
-Require Import Why3.
-
-(* Why3 goal *)
-Theorem Power_sum : forall (x:Z) (n:Z) (m:Z), (0%Z <= n)%Z ->
-  ((0%Z <= m)%Z -> ((power x (n + m)%Z) = ((power x n) * (power x m))%Z)).
-(* YOU MAY EDIT THE PROOF BELOW *)
-intros x n m Hn Hm.
-generalize Hm.
-pattern m.
-apply Z_lt_induction; auto.
-why3 "alt-ergo".
-(*
-intros n0 Hind Hn0.
-assert (h:(n0 = 0 \/ n0 > 0)%Z) by omega.
-destruct h.
-subst n0; rewrite Power_0; ring_simplify (n+0)%Z; ring.
-rewrite Power_s; auto with zarith.
-replace (n+n0-1)%Z with (n+(n0-1))%Z by omega.
-rewrite Hind; auto with zarith.
-rewrite (Power_s x n0).
-ring.
-omega.
-*)
-Qed.
-
-
diff --git a/examples/programs/power/power_WP_M_WP_parameter_fast_exp_imperative_3.v b/examples/programs/power/power_WP_M_WP_parameter_fast_exp_imperative_3.v
index 312b7960c..42ecfe547 100644
--- a/examples/programs/power/power_WP_M_WP_parameter_fast_exp_imperative_3.v
+++ b/examples/programs/power/power_WP_M_WP_parameter_fast_exp_imperative_3.v
@@ -3,60 +3,35 @@
 Require Import ZArith.
 Require Import Rbase.
 Require Import ZOdiv.
-Definition unit  := unit.
-
-Parameter mark : Type.
-
-Parameter at1: forall (a:Type), a -> mark -> a.
-
-Implicit Arguments at1.
-
-Parameter old: forall (a:Type), a -> a.
-
-Implicit Arguments old.
-
-Axiom Abs_le : forall (x:Z) (y:Z), ((Zabs x) <= y)%Z <-> (((-y)%Z <= x)%Z /\
-  (x <= y)%Z).
-
-Parameter power: Z -> Z -> Z.
+Require int.Int.
+Require int.Abs.
+Require int.ComputerDivision.
+Require int.Power.
 
+(* Why3 assumption *)
+Definition unit  := unit.
 
-Axiom Power_0 : forall (x:Z), ((power x 0%Z) = 1%Z).
-
-Axiom Power_s : forall (x:Z) (n:Z), (0%Z <  n)%Z -> ((power x
-  n) = (x * (power x (n - 1%Z)%Z))%Z).
-
-Axiom Power_1 : forall (x:Z), ((power x 1%Z) = x).
-
-Axiom Power_sum : forall (x:Z) (n:Z) (m:Z), (0%Z <= n)%Z -> ((0%Z <= m)%Z ->
-  ((power x (n + m)%Z) = ((power x n) * (power x m))%Z)).
-
-Axiom Power_mult : forall (x:Z) (n:Z) (m:Z), (0%Z <= n)%Z -> ((0%Z <= m)%Z ->
-  ((power x (n * m)%Z) = (power (power x n) m))).
-
-Axiom Power_mult2 : forall (x:Z) (y:Z) (n:Z), (0%Z <= n)%Z ->
-  ((power (x * y)%Z n) = ((power x n) * (power y n))%Z).
-
+(* Why3 assumption *)
 Inductive ref (a:Type) :=
   | mk_ref : a -> ref a.
 Implicit Arguments mk_ref.
 
-Definition contents (a:Type)(u:(ref a)): a :=
-  match u with
-  | mk_ref contents1 => contents1
+(* Why3 assumption *)
+Definition contents (a:Type)(v:(ref a)): a :=
+  match v with
+  | (mk_ref x) => x
   end.
 Implicit Arguments contents.
 
-(* YOU MAY EDIT THE CONTEXT BELOW *)
-
-(* DO NOT EDIT BELOW *)
+Import Power.
 
-Theorem WP_parameter_fast_exp_imperative : forall (x:Z), forall (n:Z),
-  (0%Z <= n)%Z -> forall (e:Z), forall (p:Z), forall (r:Z), ((0%Z <= e)%Z /\
-  ((r * (power p e))%Z = (power x n))) -> ((0%Z <  e)%Z ->
+(* Why3 goal *)
+Theorem WP_parameter_fast_exp_imperative : forall (x:Z) (n:Z),
+  (0%Z <= n)%Z -> forall (e:Z) (p:Z) (r:Z), ((0%Z <= e)%Z /\
+  ((r * (int.Power.power p e))%Z = (int.Power.power x n))) -> ((0%Z < e)%Z ->
   ((~ ((ZOmod e 2%Z) = 1%Z)) -> forall (p1:Z), (p1 = (p * p)%Z) ->
-  forall (e1:Z), (e1 = (ZOdiv e 2%Z)) -> ((r * (power p1 e1))%Z = (power x
-  n)))).
+  forall (e1:Z), (e1 = (ZOdiv e 2%Z)) -> ((r * (int.Power.power p1
+  e1))%Z = (int.Power.power x n)))).
 (* YOU MAY EDIT THE PROOF BELOW *)
 intros x n Hn e0 p0 r0 (He0,Hind).
 intros He0' Hmod p1 Hp e1 He.
@@ -72,6 +47,5 @@ rewrite Power_mult2; auto with zarith.
 rewrite h at 3.
 rewrite Power_sum; omega.
 Qed.
-(* DO NOT EDIT BELOW *)
 
 
diff --git a/examples/programs/power/why3session.xml b/examples/programs/power/why3session.xml
index 5939dcc30..a47e93e59 100644
--- a/examples/programs/power/why3session.xml
+++ b/examples/programs/power/why3session.xml
@@ -1,7 +1,7 @@
 <?xml version="1.0" encoding="UTF-8"?>
-<!DOCTYPE why3session SYSTEM "/home/andrei/prj/why-git/share/why3session.dtd">
+<!DOCTYPE why3session SYSTEM "/home/jc/why3/share/why3session.dtd">
 <why3session
- name="programs/power/why3session.xml" shape_version="2">
+ name="power/why3session.xml" shape_version="2">
  <prover
   id="0"
   name="Alt-Ergo"
@@ -21,105 +21,19 @@
  <file
   name="../power.mlw"
   verified="true"
-  expanded="false">
+  expanded="true">
   <theory
-   name="Power"
-   locfile="programs/power/../power.mlw"
-   loclnum="2" loccnumb="7" loccnume="12"
-   verified="true"
-   expanded="true">
-   <goal
-    name="Power_1"
-    locfile="programs/power/../power.mlw"
-    loclnum="12" loccnumb="8" loccnume="15"
-    sum="bdeb3f9ad05e1dc3b13cd428c8946ebb"
-    proved="true"
-    expanded="true"
-    shape="ainfix =apowerV0c1V0F">
-    <proof
-     prover="3"
-     timelimit="2"
-     memlimit="0"
-     obsolete="false"
-     archived="false">
-     <result status="valid" time="0.01"/>
-    </proof>
-    <proof
-     prover="1"
-     timelimit="2"
-     memlimit="0"
-     obsolete="false"
-     archived="false">
-     <result status="valid" time="0.00"/>
-    </proof>
-   </goal>
-   <goal
-    name="Power_sum"
-    locfile="programs/power/../power.mlw"
-    loclnum="14" loccnumb="8" loccnume="17"
-    sum="9762280403897367fe27961be8abcd84"
-    proved="true"
-    expanded="true"
-    shape="ainfix =apowerV0ainfix +V1V2ainfix *apowerV0V1apowerV0V2Iainfix &lt;=c0V2Iainfix &lt;=c0V1F">
-    <proof
-     prover="2"
-     timelimit="10"
-     memlimit="0"
-     edited="power_Power_Power_sum_1.v"
-     obsolete="false"
-     archived="false">
-     <result status="valid" time="1.23"/>
-    </proof>
-   </goal>
-   <goal
-    name="Power_mult"
-    locfile="programs/power/../power.mlw"
-    loclnum="17" loccnumb="8" loccnume="18"
-    sum="e99359f55abd122604307bcf989669a8"
-    proved="true"
-    expanded="true"
-    shape="ainfix =apowerV0ainfix *V1V2apowerapowerV0V1V2Iainfix &lt;=c0V2Iainfix &lt;=c0V1F">
-    <proof
-     prover="2"
-     timelimit="2"
-     memlimit="0"
-     edited="power_Power_Power_mult_1.v"
-     obsolete="false"
-     archived="false">
-     <result status="valid" time="0.51"/>
-    </proof>
-   </goal>
-   <goal
-    name="Power_mult2"
-    locfile="programs/power/../power.mlw"
-    loclnum="20" loccnumb="8" loccnume="19"
-    sum="b9b87f974a9380e1286402f7dae71e1b"
-    proved="true"
-    expanded="true"
-    shape="ainfix =apowerainfix *V0V1V2ainfix *apowerV0V2apowerV1V2Iainfix &lt;=c0V2F">
-    <proof
-     prover="2"
-     timelimit="5"
-     memlimit="0"
-     edited="power_Power_Power_mult2_1.v"
-     obsolete="false"
-     archived="false">
-     <result status="valid" time="0.49"/>
-    </proof>
-   </goal>
-  </theory>
-  <theory
-   name="M"
-   locfile="programs/power/../power.mlw"
-   loclnum="25" loccnumb="7" loccnume="8"
+   name="FastExponentiation"
+   locfile="power/../power.mlw"
+   loclnum="4" loccnumb="7" loccnume="25"
    verified="true"
    expanded="true">
    <goal
     name="WP_parameter fast_exp"
-    locfile="programs/power/../power.mlw"
-    loclnum="33" loccnumb="10" loccnume="18"
+    locfile="power/../power.mlw"
+    loclnum="12" loccnumb="10" loccnume="18"
     expl="parameter fast_exp"
-    sum="814f38a73df419e7883e04ed9b3a32b4"
+    sum="a54357cacf0604bf08df1c4956b43747"
     proved="true"
     expanded="true"
     shape="iainfix =V1c0ainfix =c1apowerV0V1ainfix =iainfix =amodV1c2c0ainfix *V2V2ainfix *ainfix *V2V2V0apowerV0V1LapowerV0adivV1c2Aainfix &lt;=c0adivV1c2Aainfix &lt;adivV1c2V1Aainfix &lt;=c0V1Iainfix &lt;=c0V1F">
@@ -127,19 +41,19 @@
      name="expl:parameter fast_exp"/>
     <proof
      prover="0"
-     timelimit="2"
+     timelimit="3"
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.78"/>
+     <result status="valid" time="1.46"/>
     </proof>
    </goal>
    <goal
     name="WP_parameter fast_exp_imperative"
-    locfile="programs/power/../power.mlw"
-    loclnum="47" loccnumb="6" loccnume="25"
+    locfile="power/../power.mlw"
+    loclnum="26" loccnumb="6" loccnume="25"
     expl="parameter fast_exp_imperative"
-    sum="4ec486864cb2a292d80444d23dbffe77"
+    sum="e357274f33787a0c791a5b2ba0626a8e"
     proved="true"
     expanded="true"
     shape="iainfix &gt;V2c0iainfix =amodV2c2c1ainfix &lt;V7V2Aainfix &lt;=c0V2Aainfix =ainfix *V5apowerV6V7apowerV0V1Aainfix &lt;=c0V7Iainfix =V7adivV2c2FIainfix =V6ainfix *V3V3FIainfix =V5ainfix *V4V3Fainfix &lt;V9V2Aainfix &lt;=c0V2Aainfix =ainfix *V4apowerV8V9apowerV0V1Aainfix &lt;=c0V9Iainfix =V9adivV2c2FIainfix =V8ainfix *V3V3Fainfix =V4apowerV0V1Iainfix =ainfix *V4apowerV3V2apowerV0V1Aainfix &lt;=c0V2FAainfix =ainfix *c1apowerV0V1apowerV0V1Aainfix &lt;=c0V1Iainfix &lt;=c0V1F">
@@ -151,10 +65,10 @@
      expanded="true">
      <goal
       name="WP_parameter fast_exp_imperative.1"
-      locfile="programs/power/../power.mlw"
-      loclnum="47" loccnumb="6" loccnume="25"
+      locfile="power/../power.mlw"
+      loclnum="26" loccnumb="6" loccnume="25"
       expl="loop invariant init"
-      sum="1ea603222e2a2f47dd633108c29e482f"
+      sum="fcf5b7e1ac0b575f3a89dd5c8babea5a"
       proved="true"
       expanded="true"
       shape="ainfix =ainfix *c1apowerV0V1apowerV0V1Aainfix &lt;=c0V1Iainfix &lt;=c0V1F">
@@ -174,7 +88,7 @@
        memlimit="0"
        obsolete="false"
        archived="false">
-       <result status="valid" time="0.01"/>
+       <result status="valid" time="0.02"/>
       </proof>
       <proof
        prover="1"
@@ -182,43 +96,73 @@
        memlimit="0"
        obsolete="false"
        archived="false">
-       <result status="valid" time="0.00"/>
+       <result status="valid" time="0.02"/>
       </proof>
      </goal>
      <goal
       name="WP_parameter fast_exp_imperative.2"
-      locfile="programs/power/../power.mlw"
-      loclnum="47" loccnumb="6" loccnume="25"
+      locfile="power/../power.mlw"
+      loclnum="26" loccnumb="6" loccnume="25"
       expl="loop invariant preservation"
-      sum="ab41d447c8bf2fa920fbbb078c62a90e"
+      sum="256ba83d8b3300d6bff0e9ad193e5154"
       proved="true"
       expanded="true"
       shape="ainfix =ainfix *V5apowerV6V7apowerV0V1Aainfix &lt;=c0V7Iainfix =V7adivV2c2FIainfix =V6ainfix *V3V3FIainfix =V5ainfix *V4V3FIainfix =amodV2c2c1Iainfix &gt;V2c0Iainfix =ainfix *V4apowerV3V2apowerV0V1Aainfix &lt;=c0V2FIainfix &lt;=c0V1F">
       <label
        name="expl:parameter fast_exp_imperative"/>
-      <proof
-       prover="1"
-       timelimit="5"
-       memlimit="0"
-       obsolete="false"
-       archived="false">
-       <result status="valid" time="0.06"/>
-      </proof>
-      <proof
-       prover="0"
-       timelimit="10"
-       memlimit="0"
-       obsolete="false"
-       archived="false">
-       <result status="valid" time="0.38"/>
-      </proof>
+      <transf
+       name="split_goal"
+       proved="true"
+       expanded="true">
+       <goal
+        name="WP_parameter fast_exp_imperative.2.1"
+        locfile="power/../power.mlw"
+        loclnum="26" loccnumb="6" loccnume="25"
+        expl="parameter fast_exp_imperative"
+        sum="14f9c70b0bf2d1c884642c26485002d5"
+        proved="true"
+        expanded="true"
+        shape="ainfix &lt;=c0V7Iainfix =V7adivV2c2FIainfix =V6ainfix *V3V3FIainfix =V5ainfix *V4V3FIainfix =amodV2c2c1Iainfix &gt;V2c0Iainfix =ainfix *V4apowerV3V2apowerV0V1Aainfix &lt;=c0V2FIainfix &lt;=c0V1F">
+        <label
+         name="expl:parameter fast_exp_imperative"/>
+        <proof
+         prover="0"
+         timelimit="10"
+         memlimit="1000"
+         obsolete="false"
+         archived="false">
+         <result status="valid" time="0.04"/>
+        </proof>
+       </goal>
+       <goal
+        name="WP_parameter fast_exp_imperative.2.2"
+        locfile="power/../power.mlw"
+        loclnum="26" loccnumb="6" loccnume="25"
+        expl="parameter fast_exp_imperative"
+        sum="f7b20cd04aa4fb5aeb9bbd0fd3a439ce"
+        proved="true"
+        expanded="true"
+        shape="ainfix =ainfix *V5apowerV6V7apowerV0V1Iainfix =V7adivV2c2FIainfix =V6ainfix *V3V3FIainfix =V5ainfix *V4V3FIainfix =amodV2c2c1Iainfix &gt;V2c0Iainfix =ainfix *V4apowerV3V2apowerV0V1Aainfix &lt;=c0V2FIainfix &lt;=c0V1F">
+        <label
+         name="expl:parameter fast_exp_imperative"/>
+        <proof
+         prover="2"
+         timelimit="10"
+         memlimit="1000"
+         edited="power_M_WP_parameter_fast_exp_imperative_1.v"
+         obsolete="false"
+         archived="false">
+         <result status="valid" time="1.86"/>
+        </proof>
+       </goal>
+      </transf>
      </goal>
      <goal
       name="WP_parameter fast_exp_imperative.3"
-      locfile="programs/power/../power.mlw"
-      loclnum="47" loccnumb="6" loccnume="25"
+      locfile="power/../power.mlw"
+      loclnum="26" loccnumb="6" loccnume="25"
       expl="loop variant decreases"
-      sum="d9dd38a86db776be3af0503dea622195"
+      sum="466373ea4474a5944e9eaae46d1eb50c"
       proved="true"
       expanded="true"
       shape="ainfix &lt;V7V2Aainfix &lt;=c0V2Iainfix =V7adivV2c2FIainfix =V6ainfix *V3V3FIainfix =V5ainfix *V4V3FIainfix =amodV2c2c1Iainfix &gt;V2c0Iainfix =ainfix *V4apowerV3V2apowerV0V1Aainfix &lt;=c0V2FIainfix &lt;=c0V1F">
@@ -230,7 +174,7 @@
        memlimit="0"
        obsolete="false"
        archived="false">
-       <result status="valid" time="0.01"/>
+       <result status="valid" time="0.06"/>
       </proof>
       <proof
        prover="1"
@@ -238,7 +182,7 @@
        memlimit="0"
        obsolete="false"
        archived="false">
-       <result status="valid" time="0.00"/>
+       <result status="valid" time="0.03"/>
       </proof>
       <proof
        prover="0"
@@ -246,15 +190,15 @@
        memlimit="0"
        obsolete="false"
        archived="false">
-       <result status="valid" time="0.04"/>
+       <result status="valid" time="0.08"/>
       </proof>
      </goal>
      <goal
       name="WP_parameter fast_exp_imperative.4"
-      locfile="programs/power/../power.mlw"
-      loclnum="47" loccnumb="6" loccnume="25"
+      locfile="power/../power.mlw"
+      loclnum="26" loccnumb="6" loccnume="25"
       expl="loop invariant preservation"
-      sum="f3f5ee4a09483b032c1f7342000a7c0b"
+      sum="d15cf473282989047e96c2c98daef7c4"
       proved="true"
       expanded="true"
       shape="ainfix =ainfix *V4apowerV5V6apowerV0V1Aainfix &lt;=c0V6Iainfix =V6adivV2c2FIainfix =V5ainfix *V3V3FIainfix =amodV2c2c1NIainfix &gt;V2c0Iainfix =ainfix *V4apowerV3V2apowerV0V1Aainfix &lt;=c0V2FIainfix &lt;=c0V1F">
@@ -266,10 +210,10 @@
        expanded="true">
        <goal
         name="WP_parameter fast_exp_imperative.4.1"
-        locfile="programs/power/../power.mlw"
-        loclnum="47" loccnumb="6" loccnume="25"
+        locfile="power/../power.mlw"
+        loclnum="26" loccnumb="6" loccnume="25"
         expl="parameter fast_exp_imperative"
-        sum="85098cef6a21dbd62b15d95630a75a4a"
+        sum="62691eb5ff96b85681fb8ce3a79164cf"
         proved="true"
         expanded="true"
         shape="ainfix &lt;=c0V6Iainfix =V6adivV2c2FIainfix =V5ainfix *V3V3FIainfix =amodV2c2c1NIainfix &gt;V2c0Iainfix =ainfix *V4apowerV3V2apowerV0V1Aainfix &lt;=c0V2FIainfix &lt;=c0V1F">
@@ -281,7 +225,7 @@
          memlimit="0"
          obsolete="false"
          archived="false">
-         <result status="valid" time="0.01"/>
+         <result status="valid" time="0.06"/>
         </proof>
         <proof
          prover="1"
@@ -289,7 +233,7 @@
          memlimit="0"
          obsolete="false"
          archived="false">
-         <result status="valid" time="0.01"/>
+         <result status="valid" time="0.04"/>
         </proof>
         <proof
          prover="0"
@@ -297,15 +241,15 @@
          memlimit="0"
          obsolete="false"
          archived="false">
-         <result status="valid" time="0.00"/>
+         <result status="valid" time="0.03"/>
         </proof>
        </goal>
        <goal
         name="WP_parameter fast_exp_imperative.4.2"
-        locfile="programs/power/../power.mlw"
-        loclnum="47" loccnumb="6" loccnume="25"
+        locfile="power/../power.mlw"
+        loclnum="26" loccnumb="6" loccnume="25"
         expl="parameter fast_exp_imperative"
-        sum="ac407a6824d3ad28b655599b0dd5a17f"
+        sum="290c5b9b8ce31c03351b45e7f23caf17"
         proved="true"
         expanded="true"
         shape="ainfix =ainfix *V4apowerV5V6apowerV0V1Iainfix =V6adivV2c2FIainfix =V5ainfix *V3V3FIainfix =amodV2c2c1NIainfix &gt;V2c0Iainfix =ainfix *V4apowerV3V2apowerV0V1Aainfix &lt;=c0V2FIainfix &lt;=c0V1F">
@@ -313,22 +257,22 @@
          name="expl:parameter fast_exp_imperative"/>
         <proof
          prover="2"
-         timelimit="5"
-         memlimit="0"
+         timelimit="10"
+         memlimit="1000"
          edited="power_WP_M_WP_parameter_fast_exp_imperative_3.v"
          obsolete="false"
          archived="false">
-         <result status="valid" time="0.60"/>
+         <result status="valid" time="1.92"/>
         </proof>
        </goal>
       </transf>
      </goal>
      <goal
       name="WP_parameter fast_exp_imperative.5"
-      locfile="programs/power/../power.mlw"
-      loclnum="47" loccnumb="6" loccnume="25"
+      locfile="power/../power.mlw"
+      loclnum="26" loccnumb="6" loccnume="25"
       expl="loop variant decreases"
-      sum="191b1c13954893a41b66478059c8677f"
+      sum="52537f6b60d8c23a5d1728b5381a798d"
       proved="true"
       expanded="true"
       shape="ainfix &lt;V6V2Aainfix &lt;=c0V2Iainfix =V6adivV2c2FIainfix =V5ainfix *V3V3FIainfix =amodV2c2c1NIainfix &gt;V2c0Iainfix =ainfix *V4apowerV3V2apowerV0V1Aainfix &lt;=c0V2FIainfix &lt;=c0V1F">
@@ -340,7 +284,7 @@
        memlimit="0"
        obsolete="false"
        archived="false">
-       <result status="valid" time="0.01"/>
+       <result status="valid" time="0.06"/>
       </proof>
       <proof
        prover="1"
@@ -348,7 +292,7 @@
        memlimit="0"
        obsolete="false"
        archived="false">
-       <result status="valid" time="0.00"/>
+       <result status="valid" time="0.03"/>
       </proof>
       <proof
        prover="0"
@@ -356,15 +300,15 @@
        memlimit="0"
        obsolete="false"
        archived="false">
-       <result status="valid" time="0.02"/>
+       <result status="valid" time="0.05"/>
       </proof>
      </goal>
      <goal
       name="WP_parameter fast_exp_imperative.6"
-      locfile="programs/power/../power.mlw"
-      loclnum="47" loccnumb="6" loccnume="25"
+      locfile="power/../power.mlw"
+      loclnum="26" loccnumb="6" loccnume="25"
       expl="normal postcondition"
-      sum="06f2c4535e4c0cfacf33b0871e33fb46"
+      sum="c6936210ab6c13115f0e3dbbb056954d"
       proved="true"
       expanded="true"
       shape="ainfix =V4apowerV0V1Iainfix &gt;V2c0NIainfix =ainfix *V4apowerV3V2apowerV0V1Aainfix &lt;=c0V2FIainfix &lt;=c0V1F">
@@ -376,30 +320,22 @@
        expanded="true">
        <goal
         name="WP_parameter fast_exp_imperative.6.1"
-        locfile="programs/power/../power.mlw"
-        loclnum="47" loccnumb="6" loccnume="25"
+        locfile="power/../power.mlw"
+        loclnum="26" loccnumb="6" loccnume="25"
         expl="normal postcondition"
-        sum="06f2c4535e4c0cfacf33b0871e33fb46"
+        sum="c6936210ab6c13115f0e3dbbb056954d"
         proved="true"
         expanded="true"
         shape="ainfix =V4apowerV0V1Iainfix &gt;V2c0NIainfix =ainfix *V4apowerV3V2apowerV0V1Aainfix &lt;=c0V2FIainfix &lt;=c0V1F">
         <label
          name="expl:parameter fast_exp_imperative"/>
-        <proof
-         prover="1"
-         timelimit="5"
-         memlimit="0"
-         obsolete="false"
-         archived="false">
-         <result status="valid" time="0.00"/>
-        </proof>
         <proof
          prover="0"
          timelimit="5"
          memlimit="0"
          obsolete="false"
          archived="false">
-         <result status="valid" time="0.00"/>
+         <result status="valid" time="0.03"/>
         </proof>
        </goal>
       </transf>
diff --git a/lib/coq/int/Power.v b/lib/coq/int/Power.v
new file mode 100644
index 000000000..5a1306e9b
--- /dev/null
+++ b/lib/coq/int/Power.v
@@ -0,0 +1,95 @@
+(* This file is generated by Why3's Coq driver *)
+(* Beware! Only edit allowed sections below    *)
+Require Import ZArith.
+Require Import Rbase.
+Require int.Int.
+
+(* Why3 goal *)
+Definition power: Z -> Z -> Z.
+Admitted.
+
+(* Why3 goal *)
+Lemma Power_0 : forall (x:Z), ((power x 0%Z) = 1%Z).
+intros x.
+
+Admitted.
+
+(* Why3 goal *)
+Lemma Power_s : forall (x:Z) (n:Z), (0%Z <= n)%Z -> ((power x
+  (n + 1%Z)%Z) = (x * (power x n))%Z).
+intros x n h1.
+
+Admitted.
+
+(* Why3 goal *)
+Lemma Power_1 : forall (x:Z), ((power x 1%Z) = x).
+intros x.
+
+Admitted.
+
+(* Why3 goal *)
+Lemma Power_sum : forall (x:Z) (n:Z) (m:Z), ((0%Z <= n)%Z /\ (0%Z <= m)%Z) ->
+  ((power x (n + m)%Z) = ((power x n) * (power x m))%Z).
+intros x n m (Hn, Hm).
+generalize Hm.
+pattern m.
+apply Z_lt_induction; auto.
+intros n0 Hind Hn0.
+assert (h:(n0 = 0 \/ n0 > 0)%Z) by omega.
+destruct h.
+subst n0; rewrite Power_0; ring_simplify (n+0)%Z; ring.
+replace (n+n0)%Z with ((n+n0-1)+1)%Z by omega.
+rewrite Power_s; auto with zarith.
+replace (n+n0-1)%Z with (n+(n0-1))%Z by omega.
+rewrite Hind; auto with zarith.
+replace (power x n0) with (power x ((n0-1)+1)%Z).
+rewrite (Power_s x (n0-1)%Z).
+ring.
+omega.
+apply f_equal2; auto.
+omega.
+Qed.
+
+(* Why3 goal *)
+Lemma Power_mult : forall (x:Z) (n:Z) (m:Z), (0%Z <= n)%Z -> ((0%Z <= m)%Z ->
+  ((power x (n * m)%Z) = (power (power x n) m))).
+intros x n m Hn Hm.
+generalize Hm.
+pattern m.
+apply Z_lt_induction; auto.
+intros n0 Hind Hn0.
+assert (h:(n0 = 0 \/ n0 > 0)%Z) by omega.
+destruct h.
+subst n0; rewrite Power_0; ring_simplify (n * 0)%Z.
+apply Power_0.
+replace (n*n0)%Z with (n*(n0-1)+n)%Z by ring.
+rewrite Power_sum; auto with zarith.
+rewrite Hind; auto with zarith.
+rewrite <- (Power_1 (power x n)) at 2.
+rewrite <- Power_sum; auto with zarith.
+ring_simplify (n0 - 1 + 1)%Z; auto.
+Qed.
+
+(* Why3 goal *)
+Lemma Power_mult2 : forall (x:Z) (y:Z) (n:Z), (0%Z <= n)%Z ->
+  ((power (x * y)%Z n) = ((power x n) * (power y n))%Z).
+intros x y n Hn.
+generalize Hn.
+pattern n.
+apply natlike_ind; auto.
+intros; do 3 rewrite Power_0.
+omega.
+intros.
+replace (Zsucc x0) with (x0+1)%Z by omega.
+rewrite Power_s.
+2:omega.
+rewrite (Power_s x x0).
+rewrite (Power_s y x0).
+rewrite H0.
+ring.
+omega.
+omega.
+omega.
+Qed.
+
+
diff --git a/modules/array.mlw b/modules/array.mlw
index 994d146f9..621509dab 100644
--- a/modules/array.mlw
+++ b/modules/array.mlw
@@ -217,6 +217,7 @@ module NumOfParam
   predicate pr_ (p: param_) (i: int) = let (a, p) = p in pr p i a[i]
   clone import int.NumOfParam with type param = param_, predicate pr = pr_
 
+  (* the number of a[i] such that [l <= i < u] and [pr p i a[i]] *)
   function numof (a: array elt) (p: param) (l u: int) : int = num_of (a, p) l u
 end
 
diff --git a/theories/int.why b/theories/int.why
index 94ba5670f..1e65a290c 100644
--- a/theories/int.why
+++ b/theories/int.why
@@ -205,6 +205,9 @@ theory Exponentiation
   lemma Power_mult : forall x:t, n m : int. 0 <= n -> 0 <= m ->
     power x (Int.(*) n m) = power (power x n) m
 
+  lemma Power_mult2 : forall x y: t, n: int. 0 <= n ->
+    power (x * y) n = power x n * power y n
+
 end
 
 (** {2 Power of an integer to an integer } *)
@@ -234,7 +237,7 @@ theory NumOfParam
 
   predicate pr param int
 
-  (** number of [n] such that [a <= n < b] and [pr(p,n)] *)
+  (** number of [n] such that [a <= n < b] and [pr p n] *)
   function num_of (p : param) (a b : int) : int
 
   axiom Num_of_empty :
-- 
GitLab