Skip to content

GitLab

why3
why3
Commit 1c782a4f authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files
Options

gallery: removed Coq proofs for 'power' with an assert

parent dee07b84
Hide whitespace changes
Inline Side-by-side
Showing with 31 additions and 133 deletions
examples/power.mlw
View file @ 1c782a4f
......@@ -32,9 +32,12 @@ module FastExponentiation
while !e > 0 do
invariant { 0 <= !e /\ !r * power !p !e = power x n }
variant { !e }
'L:
if mod !e 2 = 1 then r := !r * !p;
p := !p * !p;
e := div !e 2
e := div !e 2;
assert { power !p !e =
let x = power (at !p 'L) !e in x * x }
done;
!r
......
examples/power/power_M_WP_parameter_fast_exp_imperative_1.v deleted 100644 → 0
View file @ dee07b84
(* This file is generated by Why3's Coq 8.4 driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require int.Abs.
Require int.ComputerDivision.
Require int.Power.
(* Why3 assumption *)
Definition unit := unit.
Axiom qtmark : Type.
Parameter qtmark_WhyType : WhyType qtmark.
Existing Instance qtmark_WhyType.
(* Why3 assumption *)
Inductive ref (a:Type) {a_WT:WhyType a} :=
| mk_ref : a -> ref a.
Axiom ref_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (ref a).
Existing Instance ref_WhyType.
Implicit Arguments mk_ref [[a] [a_WT]].
(* Why3 assumption *)
Definition contents {a:Type} {a_WT:WhyType a} (v:(@ref a a_WT)): a :=
match v with
| (mk_ref x) => x
end.
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 ->
(((ZArith.BinInt.Z.rem e 2%Z) = 1%Z) -> forall (r1:Z), (r1 = (r * p)%Z) ->
forall (p1:Z), (p1 = (p * p)%Z) -> forall (e1:Z),
(e1 = (ZArith.BinInt.Z.quot e 2%Z)) -> ((r1 * (int.Power.power p1
e1))%Z = (int.Power.power x n)))).
(* Why3 intros x n h1 e p r (h2,h3) h4 h5 r1 h6 p1 h7 e1 h8. *)
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 by omega.
replace (2 * (Z.quot e 2))%Z with (Z.quot e 2 + Z.quot e 2)%Z by ring.
rewrite Power_sum by apply H.
rewrite Power_mult2 by apply H.
rewrite Power_1.
ring.
Qed.
examples/power/power_WP_M_WP_parameter_fast_exp_imperative_3.v deleted 100644 → 0
View file @ dee07b84
(* This file is generated by Why3's Coq 8.4 driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require int.Abs.
Require int.ComputerDivision.
Require int.Power.
(* Why3 assumption *)
Definition unit := unit.
Axiom qtmark : Type.
Parameter qtmark_WhyType : WhyType qtmark.
Existing Instance qtmark_WhyType.
(* Why3 assumption *)
Inductive ref (a:Type) {a_WT:WhyType a} :=
| mk_ref : a -> ref a.
Axiom ref_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (ref a).
Existing Instance ref_WhyType.
Implicit Arguments mk_ref [[a] [a_WT]].
(* Why3 assumption *)
Definition contents {a:Type} {a_WT:WhyType a} (v:(@ref a a_WT)): a :=
match v with
| (mk_ref x) => x
end.
Import Power Zquot.
Open Scope Z_scope.
(* 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 ->
((~ ((ZArith.BinInt.Z.rem e 2%Z) = 1%Z)) -> forall (p1:Z),
(p1 = (p * p)%Z) -> forall (e1:Z), (e1 = (ZArith.BinInt.Z.quot e 2%Z)) ->
((r * (int.Power.power p1 e1))%Z = (int.Power.power x n)))).
(* Why3 intros x n h1 e p r (h2,h3) h4 h5 p1 h6 e1 h7. *)
intros x n Hn e0 p0 r0 (He0,Hind).
intros He0' Hmod p1 Hp e1 He.
rewrite <- Hind.
apply f_equal.
subst.
assert (h: (e0 = Z.quot e0 2 + Z.quot e0 2)).
assert (Z.rem e0 2 = 0).
generalize (Zrem_lt_pos e0 2).
unfold Zabs; omega.
rewrite (Z_quot_rem_eq e0 2) at 1; omega.
rewrite Power_mult2; auto with zarith.
rewrite h at 3.
rewrite Power_sum; omega.
Qed.
examples/power/why3session.xml
View file @ 1c782a4f
......@@ -2,12 +2,13 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.01" timelimit="6" steplimit="0" memlimit="1000"/>
<prover id="1" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="2" name="Coq" version="8.4pl6" timelimit="10" steplimit="0" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.4" timelimit="6" steplimit="0" memlimit="1000"/>
<prover id="4" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="6" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="0"/>
<file name="../power.mlw" expanded="true">
<theory name="FastExponentiation" sum="52a121e21abafbdcaf06997eba2b4af7" expanded="true">
<theory name="FastExponentiation" sum="4d491a27c69448ee955d4dccb4ef7efb" expanded="true">
<goal name="WP_parameter fast_exp" expl="VC for fast_exp" expanded="true">
<proof prover="4" timelimit="3"><result status="valid" time="0.57" steps="55"/></proof>
</goal>
......@@ -18,41 +19,49 @@
<proof prover="4"><result status="valid" time="0.00" steps="1"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter fast_exp_imperative.2" expl="2. loop invariant preservation" expanded="true">
<goal name="WP_parameter fast_exp_imperative.2" expl="2. assertion" expanded="true">
<proof prover="0"><result status="valid" time="0.19" steps="14"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter fast_exp_imperative.3" expl="3. loop invariant preservation" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter fast_exp_imperative.2.1" expl="1. VC for fast_exp_imperative" expanded="true">
<proof prover="4" timelimit="10" memlimit="1000"><result status="valid" time="0.01" steps="12"/></proof>
<goal name="WP_parameter fast_exp_imperative.3.1" expl="1. VC for fast_exp_imperative" expanded="true">
<proof prover="4" timelimit="10" memlimit="1000"><result status="valid" time="0.13" steps="13"/></proof>
</goal>
<goal name="WP_parameter fast_exp_imperative.2.2" expl="2. VC for fast_exp_imperative" expanded="true">
<proof prover="2" edited="power_M_WP_parameter_fast_exp_imperative_1.v"><result status="valid" time="0.93"/></proof>
<goal name="WP_parameter fast_exp_imperative.3.2" expl="2. VC for fast_exp_imperative" expanded="true">
<proof prover="0"><result status="valid" time="2.01" steps="19"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter fast_exp_imperative.3" expl="3. loop variant decrease" expanded="true">
<goal name="WP_parameter fast_exp_imperative.4" expl="4. loop variant decrease" expanded="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="4" timelimit="10"><result status="valid" time="0.02" steps="12"/></proof>
<proof prover="4" timelimit="10"><result status="valid" time="0.22" steps="13"/></proof>
<proof prover="6"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter fast_exp_imperative.4" expl="4. loop invariant preservation" expanded="true">
<goal name="WP_parameter fast_exp_imperative.5" expl="5. assertion">
<proof prover="0"><result status="valid" time="0.10" steps="21"/></proof>
</goal>
<goal name="WP_parameter fast_exp_imperative.6" expl="6. loop invariant preservation" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter fast_exp_imperative.4.1" expl="1. VC for fast_exp_imperative" expanded="true">
<goal name="WP_parameter fast_exp_imperative.6.1" expl="1. VC for fast_exp_imperative" expanded="true">
<proof prover="0"><result status="valid" time="0.08" steps="16"/></proof>
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="15"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="16"/></proof>
<proof prover="6"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter fast_exp_imperative.4.2" expl="2. VC for fast_exp_imperative" expanded="true">
<proof prover="2" edited="power_WP_M_WP_parameter_fast_exp_imperative_3.v"><result status="valid" time="0.96"/></proof>
<goal name="WP_parameter fast_exp_imperative.6.2" expl="2. VC for fast_exp_imperative" expanded="true">
<proof prover="0"><result status="valid" time="3.10" steps="25"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter fast_exp_imperative.5" expl="5. loop variant decrease" expanded="true">
<goal name="WP_parameter fast_exp_imperative.7" expl="7. loop variant decrease" expanded="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="4" timelimit="10"><result status="valid" time="0.02" steps="15"/></proof>
<proof prover="4" timelimit="10"><result status="valid" time="2.38" steps="21"/></proof>
<proof prover="6"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter fast_exp_imperative.6" expl="6. postcondition" expanded="true">
<goal name="WP_parameter fast_exp_imperative.8" expl="8. postcondition" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter fast_exp_imperative.6.1" expl="1. postcondition" expanded="true">
<goal name="WP_parameter fast_exp_imperative.8.1" expl="1. postcondition" expanded="true">
<proof prover="4"><result status="valid" time="0.01" steps="5"/></proof>
</goal>
</transf>
......
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