Commit c295f077 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

simplified example power, by making use of int.Power

Coq realization for int.Power (mostly to keep Coq proofs that were in power.mlw)
parent 0654f137
......@@ -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
......
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 *)
......
(* 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.
(* 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 *)
(* 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 *)
(* 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.
......@@ -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 *)
<?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">