Skip to content

GitLab

why3
why3
Commit 41badd75 authored by MARCHE Claude's avatar MARCHE Claude
Browse files
Options

Coq proofs for power

parent d6c29088
Show whitespace changes
Inline Side-by-side
Showing with 20 additions and 223 deletions
examples/programs/isqrt/isqrt.mlw_M_WP_isqrt_1.v deleted 100644 → 0
View file @ d6c29088
(* Beware! Only edit allowed sections below *)
(* This file is generated by Why3's Coq driver *)
Require Import ZArith.
Require Import Rbase.
Parameter ghost : forall (a:Type), Type.
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 ref : forall (a:Type), Type.
Definition sqr(x:Z): Z := (x * x)%Z.
Theorem WP_isqrt : forall (x:Z), (0%Z <= x)%Z -> forall (result:Z),
(result = 0%Z) -> forall (result1:Z), (result1 = 1%Z) ->
(((0%Z <= result)%Z /\ (((sqr result) <= x)%Z /\
(result1 = (sqr (result + 1%Z)%Z)))) -> forall (sum:Z), forall (count:Z),
((0%Z <= count)%Z /\ (((sqr count) <= x)%Z /\
(sum = (sqr (count + 1%Z)%Z)))) -> forall (result2:Z), (result2 = sum) ->
((result2 <= x)%Z -> forall (result3:Z), (result3 = count) ->
forall (count1:Z), (count1 = (result3 + 1%Z)%Z) -> forall (result4:Z),
(result4 = sum) -> forall (result5:Z), (result5 = count1) ->
forall (sum1:Z), (sum1 = ((result4 + (2%Z * result5)%Z)%Z + 1%Z)%Z) ->
(((0%Z <= count1)%Z /\ (((sqr count1) <= x)%Z /\
(sum1 = (sqr (count1 + 1%Z)%Z)))) -> (0%Z <= (x - count)%Z)%Z))).
(* YOU MAY EDIT THE PROOF BELOW *)
intros.
Qed.
(* DO NOT EDIT BELOW *)
examples/programs/isqrt/isqrt.mlw_M_WP_main_1.v deleted 100644 → 0
View file @ d6c29088
(* Beware! Only edit allowed sections below *)
(* This file is generated by Why3's Coq driver *)
Require Import ZArith.
Require Import Rbase.
Parameter ghost : forall (a:Type), Type.
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 ref : forall (a:Type), Type.
Definition sqr(x:Z): Z := (x * x)%Z.
Theorem WP_main : (0%Z <= 17%Z)%Z /\ forall (result:Z), ((0%Z <= result)%Z /\
(((sqr result) <= 17%Z)%Z /\ (17%Z < (sqr (result + 1%Z)%Z))%Z)) ->
(result = 4%Z).
(* YOU MAY EDIT THE PROOF BELOW *)
intros.
Qed.
(* DO NOT EDIT BELOW *)
examples/programs/isqrt/isqrt.mlw_M_WP_main_2.v deleted 100644 → 0
View file @ d6c29088
(* Beware! Only edit allowed sections below *)
(* This file is generated by Why3's Coq driver *)
Require Import ZArith.
Require Import Rbase.
Parameter ghost : forall (a:Type), Type.
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 ref : forall (a:Type), Type.
Definition sqr(x:Z): Z := (x * x)%Z.
Theorem WP_main : (0%Z <= 17%Z)%Z -> forall (result:Z), ((0%Z <= result)%Z /\
(((sqr result) <= 17%Z)%Z /\ (17%Z < (sqr (result + 1%Z)%Z))%Z)) ->
(result = 4%Z).
(* YOU MAY EDIT THE PROOF BELOW *)
intros.
assert (h:(result < 4 \/ result = 4 \/ result > 4)%Z) by omega.
destruct h as [h1|[h2|h3]]; auto.
Qed.
(* DO NOT EDIT BELOW *)
examples/programs/power/power.mlw_Power_Power_mult_1.v
View file @ 41badd75
(* Beware! Only edit allowed sections 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
......
examples/programs/power/power.mlw_Power_Power_mult_2.v deleted 100644 → 0
View file @ d6c29088
(* Beware! Only edit allowed sections below *)
(* This file is generated by Why3's Coq driver *)
Require Import ZArith.
Require Import Rbase.
Parameter ghost : forall (a:Type), Type.
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 *)
admit.
Qed.
(* DO NOT EDIT BELOW *)
examples/programs/power/power.mlw_Power_Power_sum_1.v
View file @ 41badd75
(* Beware! Only edit allowed sections 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
......
examples/programs/power/power.mlw_Power_Power_sum_2.v deleted 100644 → 0
View file @ d6c29088
(* Beware! Only edit allowed sections below *)
(* This file is generated by Why3's Coq driver *)
Require Import ZArith.
Require Import Rbase.
Parameter ghost : forall (a:Type), Type.
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).
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.
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.
(* DO NOT EDIT BELOW *)
examples/programs/power/why3session.xml
View file @ 41badd75
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="programs/power/why3session.xml">
<why3session name="power/why3session.xml">
<file name="../power.mlw" verified="false" expanded="true">
<theory name="Power" verified="false" expanded="true">
<theory name="Power" verified="true" expanded="false">
<goal name="Power_1" sum="1db7c130e0faaa3525077846831aadf3" proved="true" expanded="false">
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.01"/>
......@@ -17,7 +17,10 @@
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="Power_sum" sum="0222179599018e583f47a3d214f2e604" proved="false" expanded="true">
<goal name="Power_sum" sum="0222179599018e583f47a3d214f2e604" proved="true" expanded="false">
<proof prover="coq" timelimit="2" edited="power/power.mlw_Power_Power_sum_1.v" obsolete="false">
<result status="valid" time="0.46"/>
</proof>
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.08"/>
</proof>
......@@ -31,7 +34,10 @@
<result status="timeout" time="2.07"/>
</proof>
</goal>
<goal name="Power_mult" sum="9d09d633adb75294ad19c24d7ad24bf4" proved="false" expanded="true">
<goal name="Power_mult" sum="9d09d633adb75294ad19c24d7ad24bf4" proved="true" expanded="false">
<proof prover="coq" timelimit="2" edited="power/power.mlw_Power_Power_mult_1.v" obsolete="false">
<result status="valid" time="0.52"/>
</proof>
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="unknown" time="1.50"/>
</proof>
......
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