updated proof sessions

parent 105f8b56
(* 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 Import Zdiv.
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.
Definition divides(a:Z) (b:Z): Prop := exists q:Z, (b = (q * a)%Z).
Axiom Divides_x_zero : forall (x:Z), (divides x 0%Z).
Axiom Divides_one_x : forall (x:Z), (divides 1%Z x).
Definition gcd(a:Z) (b:Z) (g:Z): Prop := (divides g a) /\ ((divides g b) /\
forall (x:Z), (divides x a) -> ((divides x b) -> (divides x g))).
Axiom Gcd_sym : forall (a:Z) (b:Z) (g:Z), (gcd a b g) -> (gcd b a g).
Axiom Gcd_0 : forall (a:Z), (gcd a 0%Z a).
Axiom Gcd_euclid : forall (a:Z) (b:Z) (q:Z) (g:Z), (gcd a (b - (q * a)%Z)%Z
g) -> (gcd a b g).
Axiom Abs_pos : forall (x:Z), (0%Z <= (Zabs x))%Z.
Axiom Div_mod : forall (x:Z) (y:Z), (~ (y = 0%Z)) ->
(x = ((y * (ZOdiv x y))%Z + (ZOmod x y))%Z).
Axiom Div_bound : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z < y)%Z) ->
((0%Z <= (ZOdiv x y))%Z /\ ((ZOdiv x y) <= x)%Z).
Axiom Mod_bound : forall (x:Z) (y:Z), (~ (y = 0%Z)) ->
(((-(Zabs y))%Z < (ZOmod x y))%Z /\ ((ZOmod x y) < (Zabs y))%Z).
Axiom Div_sign_pos : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z < y)%Z) ->
(0%Z <= (ZOdiv x y))%Z.
Axiom Div_sign_neg : forall (x:Z) (y:Z), ((x <= 0%Z)%Z /\ (0%Z < y)%Z) ->
((ZOdiv x y) <= 0%Z)%Z.
Axiom Mod_sign_pos : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ ~ (y = 0%Z)) ->
(0%Z <= (ZOmod x y))%Z.
Axiom Mod_sign_neg : forall (x:Z) (y:Z), ((x <= 0%Z)%Z /\ ~ (y = 0%Z)) ->
((ZOmod x y) <= 0%Z)%Z.
Axiom Rounds_toward_zero : forall (x:Z) (y:Z), (~ (y = 0%Z)) ->
((Zabs ((ZOdiv x y) * y)%Z) <= (Zabs x))%Z.
Axiom Div_1 : forall (x:Z), ((ZOdiv x 1%Z) = x).
Axiom Mod_1 : forall (x:Z), ((ZOmod x 1%Z) = 0%Z).
Axiom Div_inf : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (x < y)%Z) ->
((ZOdiv x y) = 0%Z).
Axiom Mod_inf : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (x < y)%Z) ->
((ZOmod x y) = x).
Axiom Div_mult : forall (x:Z) (y:Z) (z:Z), ((0%Z < x)%Z /\ ((0%Z <= y)%Z /\
(0%Z <= z)%Z)) -> ((ZOdiv ((x * y)%Z + z)%Z x) = (y + (ZOdiv z x))%Z).
Axiom Mod_mult : forall (x:Z) (y:Z) (z:Z), ((0%Z < x)%Z /\ ((0%Z <= y)%Z /\
(0%Z <= z)%Z)) -> ((ZOmod ((x * y)%Z + z)%Z x) = (ZOmod z x)).
Axiom Gcd_computer_mod : forall (a:Z) (b:Z) (g:Z), (~ (b = 0%Z)) -> ((gcd a
(ZOmod a b) g) -> (gcd a b g)).
Axiom Div_mod1 : forall (x:Z) (y:Z), (~ (y = 0%Z)) ->
(x = ((y * (Zdiv x y))%Z + (Zmod x y))%Z).
Axiom Div_bound1 : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z < y)%Z) ->
((0%Z <= (Zdiv x y))%Z /\ ((Zdiv x y) <= x)%Z).
Axiom Mod_bound1 : forall (x:Z) (y:Z), (~ (y = 0%Z)) ->
((0%Z <= (Zmod x y))%Z /\ ((Zmod x y) < (Zabs y))%Z).
Axiom Mod_11 : forall (x:Z), ((Zmod x 1%Z) = 0%Z).
Axiom Div_11 : forall (x:Z), ((Zdiv x 1%Z) = x).
Axiom Gcd_euclidean_mod : forall (a:Z) (b:Z) (g:Z), (~ (b = 0%Z)) -> ((gcd a
(Zmod a b) g) -> (gcd a b g)).
Theorem WP_parameter_gcd : forall (u:Z), forall (v:Z), ((0%Z <= u)%Z /\
(0%Z <= v)%Z) -> ((~ (v = 0%Z)) -> ((((0%Z <= v)%Z /\
((ZOmod u v) < v)%Z) /\ ((0%Z <= v)%Z /\ (0%Z <= (ZOmod u v))%Z)) ->
forall (result:Z), (gcd v (ZOmod u v) result) -> (gcd u v result))).
(* YOU MAY EDIT THE PROOF BELOW *)
intuition.
apply Gcd_sym.
apply Gcd_euclid with (q:=(ZOdiv u v)).
assert (u - (ZOdiv u v) * v = ZOmod u v)%Z.
generalize (Div_mod u v); intuition.
replace ((ZOdiv u v) * v) with (v * (ZOdiv u v)) by ring.
omega.
rewrite H7; assumption.
Qed.
(* DO NOT EDIT BELOW *)
......@@ -3,28 +3,28 @@
<why3session name="examples/programs/gcd/why3session.xml">
<file name="../gcd.mlw" verified="true" expanded="true">
<theory name="WP EuclideanAlgorithm" verified="true" expanded="true">
<goal name="WP_parameter gcd" expl="correctness of parameter gcd" sum="bfbae7b37de6ad9ac15a7666cdb75bce" proved="true" expanded="true">
<goal name="WP_parameter gcd" expl="correctness of parameter gcd" sum="322244ca4eb191447c5e003581d46441" proved="true" expanded="true">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter gcd.1" expl="normal postcondition" sum="3893c6278b0c6d2e8a61ff8df2953fcb" proved="true" expanded="true">
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
<proof prover="simplify" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="1.12"/>
</proof>
</goal>
<goal name="WP_parameter gcd.2" expl="precondition" sum="af7096cc1cd7bdcb9f88d52ad341c488" proved="true" expanded="true">
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
<proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.06"/>
<result status="valid" time="0.02"/>
</proof>
<proof prover="simplify" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.00"/>
......@@ -34,8 +34,8 @@
</proof>
</goal>
<goal name="WP_parameter gcd.3" expl="normal postcondition" sum="9ac7a295784dbed7c5dfdb55575495d7" proved="true" expanded="true">
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="6.84"/>
<proof prover="coq" timelimit="10" edited="gcd_WP_EuclideanAlgorithm_WP_parameter_gcd_1.v" obsolete="false">
<result status="valid" time="0.63"/>
</proof>
</goal>
</transf>
......
(* McCarthy's ``91'' function. *)
module M
module McCarthy91
use import int.Int
......@@ -55,6 +55,6 @@ end
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. examples/programs/mac_carthy"
compile-command: "unset LANG; make -C ../.. examples/programs/mccarthy.gui"
End:
*)
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="examples/programs/mac_carthy/why3session.xml">
<file name="../mac_carthy.mlw" verified="true" expanded="true">
<theory name="WP M" verified="true" expanded="true">
<goal name="WP_parameter f91" expl="correctness of parameter f91" sum="7abacd70509916020a75c246a162149a" proved="true" expanded="true">
<why3session name="examples/programs/mccarthy/why3session.xml">
<file name="../mccarthy.mlw" verified="true" expanded="true">
<theory name="WP McCarthy91" verified="true" expanded="true">
<goal name="WP_parameter f91" expl="correctness of parameter f91" sum="e18e58e303b9b8ee4937723c698568ca" proved="true" expanded="true">
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
......@@ -17,9 +17,9 @@
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter f91_nonrec" expl="correctness of parameter f91_nonrec" sum="dd51d83389d374c543e554d535df25d2" proved="true" expanded="true">
<goal name="WP_parameter f91_nonrec" expl="correctness of parameter f91_nonrec" sum="75f22cdba2f4a634d9942900b5b0c525" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.52"/>
<result status="valid" time="0.64"/>
</proof>
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.02"/>
......
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