more proofs in euler

8f71d7f5 · MARCHE Claude · 106abed1 · 8f71d7f5 · 8f71d7f5 · 8f71d7f5
Commit 8f71d7f5 authored Sep 06, 2011 by MARCHE Claude
--- a/examples/programs/euler001.mlw
+++ b/examples/programs/euler001.mlw
@@ -43,21 +43,31 @@ theory SumMultiple
         5 * n5 * (n5+1) -
         15 * n15 * (n15+1)) 2

+(*
  lemma mod_15 :
    forall n:int. n >= 0 ->
      mod n 15 = 0 <-> (mod n 3 = 0 /\ mod n 5 = 0)
+*)

  predicate p (n:int) = sum_multiple_3_5_lt (n+1) = closed_formula n

  lemma Closed_formula_0: p 0

-  lemma Closed_formula_n_1:
+  lemma Closed_formula_n:
    forall n:int. n > 0 -> p (n-1) ->
      mod n 3 <> 0 /\ mod n 5 <> 0 -> p n

-  lemma Closed_formula_n_2:
+  lemma Closed_formula_n_3:
+    forall n:int. n > 0 -> p (n-1) ->
+      mod n 3 = 0 /\ mod n 5 <> 0 -> p n
+
+  lemma Closed_formula_n_5:
+    forall n:int. n > 0 -> p (n-1) ->
+      mod n 3 <> 0 /\ mod n 5 = 0 -> p n
+
+  lemma Closed_formula_n_15:
    forall n:int. n > 0 -> p (n-1) ->
-      mod n 3 = 0 \/ mod n 5 = 0 -> p n
+      mod n 3 = 0 /\ mod n 5 = 0 -> p n

  clone int.Induction as I with predicate p = p


--- a/examples/programs/euler001/euler001_SumMultiple_div_minus1_1_1.v
+++ b/examples/programs/euler001/euler001_SumMultiple_div_minus1_1_1.v
+(* This file is generated by Why3's Coq driver *)
+(* Beware! Only edit allowed sections below    *)
+Require Import ZArith.
+Require Import Rbase.
+Require Import Zdiv.
+Axiom Abs_le : forall (x:Z) (y:Z), ((Zabs x) <= y)%Z <-> (((-y)%Z <= x)%Z /\
+  (x <= y)%Z).
+
+Parameter sum_multiple_3_5_lt: Z -> Z.
+
+
+Axiom SumEmpty : ((sum_multiple_3_5_lt 0%Z) = 0%Z).
+
+Axiom SumNo : forall (n:Z), (0%Z <= n)%Z -> (((~ ((Zmod n 3%Z) = 0%Z)) /\
+  ~ ((Zmod n 5%Z) = 0%Z)) ->
+  ((sum_multiple_3_5_lt (n + 1%Z)%Z) = (sum_multiple_3_5_lt n))).
+
+Axiom SumYes : forall (n:Z), (0%Z <= n)%Z -> ((((Zmod n 3%Z) = 0%Z) \/
+  ((Zmod n 5%Z) = 0%Z)) ->
+  ((sum_multiple_3_5_lt (n + 1%Z)%Z) = ((sum_multiple_3_5_lt n) + n)%Z)).
+
+(* YOU MAY EDIT THE CONTEXT BELOW *)
+
+(* DO NOT EDIT BELOW *)
+
+Theorem div_minus1_1 : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z <  y)%Z) ->
+  (((Zmod (x + 1%Z)%Z y) = 0%Z) ->
+  ((Zdiv (x + 1%Z)%Z y) = ((Zdiv x y) + 1%Z)%Z)).
+(* YOU MAY EDIT THE PROOF BELOW *)
+intros x y (Hx,Hy) H.
+pose (q := ((x+1)/ y)%Z).
+assert (h2: (x = y * q - 1)%Z).
+  replace x with (x+1-1)%Z by omega.
+  rewrite (Z_div_mod_eq (x+1) y); auto with zarith.
+  rewrite H.
+  subst q; omega.
+rewrite h2; clear h2.
+replace (y * q - 1 + 1)%Z with (y*q)%Z by omega.
+rewrite Zmult_comm. 
+rewrite Z_div_mult; auto with zarith.
+replace (q*y-1)%Z with (q*y+(-1))%Z by omega.
+rewrite Z_div_plus_full_l; auto with zarith.
+assert (h:(y=1 \/ y > 1)%Z) by omega.
+destruct h.
+subst q y.
+replace (-1 / 1)%Z with (-1)%Z.
+  omega.
+  rewrite Zdiv_1_r; auto.
+replace (-1)%Z with (-(1))%Z; auto with zarith.
+rewrite (Z_div_nz_opp_full 1 y).
+rewrite Zdiv_1_l; auto with zarith.
+rewrite Zmod_1_l; auto with zarith.
+Qed.
+(* DO NOT EDIT BELOW *)
+
+
--- a/examples/programs/euler001/why3session.xml
+++ b/examples/programs/euler001/why3session.xml
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session SYSTEM "why3session.dtd">
 <why3session name="examples/programs/euler001/why3session.xml">
+ <prover id="alt-ergo" name="Alt-Ergo" version="0.93"/>
+ <prover id="coq" name="Coq" version="8.2pl1"/>
+ <prover id="cvc3" name="CVC3" version="2.2"/>
+ <prover id="gappa" name="Gappa" version="0.13.0"/>
+ <prover id="simplify" name="Simplify" version="1.5.4"/>
+ <prover id="z3" name="Z3" version="2.19"/>
 <file name="../euler001.mlw" verified="false" expanded="true">
  <theory name="SumMultiple" verified="false" expanded="true">
-   <goal name="div_minus1_1" sum="799200a5112f46b45ab595bbe99aa9fe" proved="false" expanded="true">
-   </goal>
-   <goal name="div_minus1_2" sum="7b0639aa2f9bead033faaeae5c5303fe" proved="false" expanded="true">
+   <goal name="div_minus1_1" sum="5266791566cb9e131f79837e51b72de8" proved="true" expanded="true" shape="ainfix =adivainfix +V0c1V1ainfix +adivV0V1c1Iainfix =amodainfix +V0c1V1c0Iainfix >V1c0Aainfix >=V0c0F">
+    <proof prover="coq" timelimit="5" edited="euler001_SumMultiple_div_minus1_1_1.v" obsolete="false">
+     <result status="valid" time="0.48"/>
+    </proof>
   </goal>
-   <goal name="mod_15" sum="e5478c4f7dd1e8e51f1b59c6f48d52b7" proved="true" expanded="true">
-    <proof prover="cvc3" timelimit="2" edited="" obsolete="false">
-     <result status="valid" time="0.04"/>
+   <goal name="div_minus1_2" sum="b75e15f7119a97ac29920a7a789b8e15" proved="false" expanded="true" shape="ainfix =adivainfix +V0c1V1adivV0V1Iainfix =amodainfix +V0c1V1c0NIainfix >V1c0Aainfix >=V0c0F">
+    <proof prover="simplify" timelimit="5" edited="" obsolete="false">
+     <result status="unknown" time="0.05"/>
    </proof>
-    <proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
-     <result status="valid" time="0.11"/>
+    <proof prover="cvc3" timelimit="5" edited="" obsolete="false">
+     <result status="timeout" time="5.01"/>
    </proof>
-    <proof prover="z3" timelimit="2" edited="" obsolete="false">
-     <result status="valid" time="0.02"/>
+    <proof prover="alt-ergo" timelimit="5" edited="" obsolete="false">
+     <result status="unknown" time="0.23"/>
+    </proof>
+    <proof prover="z3" timelimit="5" edited="" obsolete="false">
+     <result status="timeout" time="5.06"/>
    </proof>
   </goal>
-   <goal name="Closed_formula_0" sum="a49fafd7dea8767fc52287a6d759cc28" proved="true" expanded="true">
+   <goal name="Closed_formula_0" sum="9d635abb360eeba223e62aea7d54449e" proved="true" expanded="true" shape="apc0">
    <proof prover="cvc3" timelimit="2" edited="" obsolete="false">
-     <result status="valid" time="0.03"/>
+     <result status="valid" time="0.12"/>
    </proof>
    <proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
-     <result status="valid" time="0.01"/>
+     <result status="valid" time="0.02"/>
    </proof>
    <proof prover="z3" timelimit="2" edited="" obsolete="false">
-     <result status="valid" time="0.00"/>
+     <result status="valid" time="0.03"/>
    </proof>
   </goal>
-   <goal name="Closed_formula_n_1" sum="53f650c14f94ca7656e6b83261ea0a3d" proved="true" expanded="true">
-    <proof prover="cvc3" timelimit="2" edited="" obsolete="false">
-     <result status="valid" time="0.12"/>
+   <goal name="Closed_formula_n" sum="14a06794c39f504fc3c7c61434c31a89" proved="true" expanded="true" shape="apV0Iainfix =amodV0c5c0NAainfix =amodV0c3c0NIapainfix -V0c1Iainfix >V0c0F">
+    <proof prover="cvc3" timelimit="5" edited="" obsolete="false">
+     <result status="valid" time="0.23"/>
    </proof>
-    <proof prover="simplify" timelimit="2" edited="" obsolete="false">
-     <result status="valid" time="0.00"/>
+   </goal>
+   <goal name="Closed_formula_n_3" sum="759e99918260c7a3c5b1f4b5c33f42dd" proved="true" expanded="true" shape="apV0Iainfix =amodV0c5c0NAainfix =amodV0c3c0Iapainfix -V0c1Iainfix >V0c0F">
+    <proof prover="alt-ergo" timelimit="5" edited="" obsolete="false">
+     <result status="valid" time="0.02"/>
+    </proof>
+   </goal>
+   <goal name="Closed_formula_n_5" sum="380bc8b386b3035b1711cb23fa17a9da" proved="true" expanded="true" shape="apV0Iainfix =amodV0c5c0Aainfix =amodV0c3c0NIapainfix -V0c1Iainfix >V0c0F">
+    <proof prover="alt-ergo" timelimit="5" edited="" obsolete="false">
+     <result status="valid" time="0.05"/>
    </proof>
   </goal>
-   <goal name="Closed_formula_n_2" sum="ce02a5758f2253ac1e0edc7f916ce957" proved="false" expanded="true">
+   <goal name="Closed_formula_n_15" sum="cc0a4b0b292325909c6a8a65262645c3" proved="true" expanded="true" shape="apV0Iainfix =amodV0c5c0Aainfix =amodV0c3c0Iapainfix -V0c1Iainfix >V0c0F">
+    <proof prover="alt-ergo" timelimit="5" edited="" obsolete="false">
+     <result status="valid" time="0.04"/>
+    </proof>
   </goal>
-   <goal name="Closed_formula" sum="aa724d9368ec95db9867b2ea2062c3a0" proved="true" expanded="true">
+   <goal name="Closed_formula" sum="8e356511ca2b540b119a8650fd1519c4" proved="true" expanded="true" shape="apV0Iainfix <=c0V0F">
    <proof prover="cvc3" timelimit="2" edited="" obsolete="false">
-     <result status="valid" time="0.01"/>
+     <result status="valid" time="0.10"/>
    </proof>
    <proof prover="simplify" timelimit="2" edited="" obsolete="false">
-     <result status="valid" time="0.03"/>
+     <result status="valid" time="0.13"/>
    </proof>
   </goal>
  </theory>
  <theory name="WP Euler001" verified="true" expanded="true">
-   <goal name="WP_parameter solve" expl="normal postcondition" sum="1d462fc3346a429205b44caaf3f0a839" proved="true" expanded="true">
-    <proof prover="cvc3" timelimit="2" edited="" obsolete="false">
-     <result status="valid" time="0.51"/>
+   <goal name="WP_parameter solve" expl="normal postcondition" sum="76b404cbe7788d104d79907f50ebed27" proved="true" expanded="true" shape="ainfix =adivainfix -ainfix +ainfix *ainfix *c3adivainfix -V0c1c3ainfix +adivainfix -V0c1c3c1ainfix *ainfix *c5adivainfix -V0c1c5ainfix +adivainfix -V0c1c5c1ainfix *ainfix *c15adivainfix -V0c1c15ainfix +adivainfix -V0c1c15c1c2asum_multiple_3_5_ltV0Iainfix >=V0c1F">
+    <proof prover="cvc3" timelimit="5" edited="" obsolete="false">
+     <result status="valid" time="2.63"/>
    </proof>
    <proof prover="simplify" timelimit="2" edited="" obsolete="false">
-     <result status="valid" time="0.10"/>
+     <result status="valid" time="0.13"/>
    </proof>
   </goal>
  </theory>