Coq proofs for euler001

examples/programs/euler001.mlw

@@ -13,8 +13,8 @@ theory DivModHints
   use import int.ComputerDivision
 
   lemma mod_div_unique :
-    forall x y q r:int. y > 0 /\ x = q*y + r /\ 0 <= r < y ->
-      r = mod x y /\ q = div x y
+    forall x y q r:int. x >= 0 /\ y > 0 /\ x = q*y + r /\ 0 <= r < y ->
+      q = div x y /\ r = mod x y 
 
   lemma mod_succ_1 :
     forall x y:int. x >= 0 /\ y > 0 ->
@@ -72,21 +72,25 @@ theory SumMultiple
     forall n:int.
       mod n 15 = 0 <-> mod n 3 = 0 /\ mod n 5 = 0
 
+  lemma triangle_numbers:
+    forall n:int.
+      2 * div (n*(n+1)) 2 = n*(n+1)
+
   lemma Closed_formula_n:
-    forall n:int. n > 0 -> p (n-1) ->
-      mod n 3 <> 0 /\ mod n 5 <> 0 -> p n
+    forall n:int. n >= 0 -> p n ->
+      mod (n+1) 3 <> 0 /\ mod (n+1) 5 <> 0 -> p (n+1)
 
   lemma Closed_formula_n_3:
-    forall n:int. n > 0 -> p (n-1) ->
-      mod n 3 = 0 /\ mod n 5 <> 0 -> p n
+    forall n:int. n >= 0 -> p n ->
+      mod (n+1) 3 = 0 /\ mod (n+1) 5 <> 0 -> p (n+1)
 
   lemma Closed_formula_n_5:
-    forall n:int. n > 0 -> p (n-1) ->
-      mod n 3 <> 0 /\ mod n 5 = 0 -> p n
+    forall n:int. n >= 0 -> p n ->
+      mod (n+1) 3 <> 0 /\ mod (n+1) 5 = 0 -> p (n+1)
 
   lemma Closed_formula_n_15:
-    forall n:int. n > 0 -> p (n-1) ->
-      mod n 3 = 0 /\ mod n 5 = 0 -> p n
+    forall n:int. n >= 0 -> p n ->
+      mod (n+1) 3 = 0 /\ mod (n+1) 5 = 0 -> p (n+1)
 
   clone int.Induction as I with predicate p = p
 

examples/programs/euler001/euler001_DivModHints_mod_div_unique_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 ZOdiv.
+Axiom Abs_le : forall (x:Z) (y:Z), ((Zabs x) <= y)%Z <-> (((-y)%Z <= x)%Z /\
+  (x <= y)%Z).
+
+(* YOU MAY EDIT THE CONTEXT BELOW *)
+
+(* DO NOT EDIT BELOW *)
+
+Theorem mod_div_unique : forall (x:Z) (y:Z) (q:Z) (r:Z), ((0%Z <= x)%Z /\
+  ((0%Z <  y)%Z /\ ((x = ((q * y)%Z + r)%Z) /\ ((0%Z <= r)%Z /\
+  (r <  y)%Z)))) -> ((q = (ZOdiv x y)) /\ (r = (ZOmod x y))).
+(* YOU MAY EDIT THE PROOF BELOW *)
+intros x y q r (H1,(H2,(H3,(H4,H5)))).
+apply ZOdiv_mod_unique_full.
+2: rewrite H3; ring.
+red.
+left.
+rewrite Zabs_eq; auto with zarith.
+Qed.
+(* DO NOT EDIT BELOW *)
+
+

examples/programs/euler001/euler001_DivModHints_mod_succ_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 ZOdiv.
+Axiom Abs_le : forall (x:Z) (y:Z), ((Zabs x) <= y)%Z <-> (((-y)%Z <= x)%Z /\
+  (x <= y)%Z).
+
+Axiom mod_div_unique : forall (x:Z) (y:Z) (q:Z) (r:Z), ((0%Z <  y)%Z /\
+  ((x = ((q * y)%Z + r)%Z) /\ ((0%Z <= r)%Z /\ (r <  y)%Z))) ->
+  ((r = (ZOmod x y)) /\ (q = (ZOdiv x y))).
+
+(* YOU MAY EDIT THE CONTEXT BELOW *)
+Open Scope Z_scope.
+(* DO NOT EDIT BELOW *)
+
+Theorem mod_succ_1 : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z <  y)%Z) ->
+  ((~ ((ZOmod (x + 1%Z)%Z y) = 0%Z)) ->
+  ((ZOmod (x + 1%Z)%Z y) = ((ZOmod x y) + 1%Z)%Z)).
+(* YOU MAY EDIT THE PROOF BELOW *)
+intros x y (Hx,Hy) H.
+assert (h: y>0) by omega.
+generalize (ZO_div_mod_eq x y); intro h1.
+generalize (ZO_div_mod_eq (x+1) y); intro h2.
+assert (h3:x = y * ((x + 1) / y) + ((x + 1) mod y - 1)) by omega.
+generalize (mod_div_unique x y ((x + 1) / y) ((x + 1) mod y - 1)).
+intuition.
+destruct H1; auto with zarith.
+rewrite h3 at 1.
+ring.
+assert (0 <= (x + 1) mod y < y).
+  apply ZOmod_lt_pos_pos; omega.
+omega.
+Qed.
+(* DO NOT EDIT BELOW *)
+
+

examples/programs/euler001/euler001_DivModHints_mod_succ_2_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 ZOdiv.
+Axiom Abs_le : forall (x:Z) (y:Z), ((Zabs x) <= y)%Z <-> (((-y)%Z <= x)%Z /\
+  (x <= y)%Z).
+
+Axiom mod_div_unique : forall (x:Z) (y:Z) (q:Z) (r:Z), ((0%Z <= x)%Z /\
+  ((0%Z <  y)%Z /\ ((x = ((q * y)%Z + r)%Z) /\ ((0%Z <= r)%Z /\
+  (r <  y)%Z)))) -> ((q = (ZOdiv x y)) /\ (r = (ZOmod x y))).
+
+Axiom mod_succ_1 : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z <  y)%Z) ->
+  ((~ ((ZOmod (x + 1%Z)%Z y) = 0%Z)) ->
+  ((ZOmod (x + 1%Z)%Z y) = ((ZOmod x y) + 1%Z)%Z)).
+
+(* YOU MAY EDIT THE CONTEXT BELOW *)
+
+(* DO NOT EDIT BELOW *)
+
+Theorem mod_succ_2 : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z <  y)%Z) ->
+  (((ZOmod (x + 1%Z)%Z y) = 0%Z) -> ((ZOmod x y) = (y - 1%Z)%Z)).
+(* YOU MAY EDIT THE PROOF BELOW *)
+intros x y (Hx,Hy) H.
+generalize (ZO_div_mod_eq x y); intro h1.
+generalize (ZO_div_mod_eq (x+1) y); intro h2.
+assert (h3:x = y * ((x + 1) / y - 1) + ((x + 1) mod y + y - 1)).
+  ring_simplify; omega.
+rewrite H in h3.
+generalize (mod_div_unique x y ((x + 1) / y - 1) (0 + y - 1)).
+intuition.
+destruct H1; auto with zarith.
+rewrite h3 at 1.
+ring.
+Qed.
+(* DO NOT EDIT BELOW *)
+
+

examples/programs/euler001/euler001_SumMultiple_Closed_formula_n_3_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 ZOdiv.
+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 -> (((~ ((ZOmod n 3%Z) = 0%Z)) /\
+  ~ ((ZOmod 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 -> ((((ZOmod n 3%Z) = 0%Z) \/
+  ((ZOmod n 5%Z) = 0%Z)) ->
+  ((sum_multiple_3_5_lt (n + 1%Z)%Z) = ((sum_multiple_3_5_lt n) + n)%Z)).
+
+Definition closed_formula(n:Z): Z := let n3 := (ZOdiv n 3%Z) in let n5 :=
+  (ZOdiv n 5%Z) in let n15 := (ZOdiv n 15%Z) in
+  (ZOdiv ((((3%Z * n3)%Z * (n3 + 1%Z)%Z)%Z + ((5%Z * n5)%Z * (n5 + 1%Z)%Z)%Z)%Z - ((15%Z * n15)%Z * (n15 + 1%Z)%Z)%Z)%Z 2%Z).
+
+Definition p(n:Z): Prop :=
+  ((sum_multiple_3_5_lt (n + 1%Z)%Z) = (closed_formula n)).
+
+Axiom Closed_formula_0 : (p 0%Z).
+
+Axiom mod_div_unique : forall (x:Z) (y:Z) (q:Z) (r:Z), ((0%Z <= x)%Z /\
+  ((0%Z <  y)%Z /\ ((x = ((q * y)%Z + r)%Z) /\ ((0%Z <= r)%Z /\
+  (r <  y)%Z)))) -> ((q = (ZOdiv x y)) /\ (r = (ZOmod x y))).
+
+Axiom mod_succ_1 : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z <  y)%Z) ->
+  ((~ ((ZOmod (x + 1%Z)%Z y) = 0%Z)) ->
+  ((ZOmod (x + 1%Z)%Z y) = ((ZOmod x y) + 1%Z)%Z)).
+
+Axiom mod_succ_2 : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z <  y)%Z) ->
+  (((ZOmod (x + 1%Z)%Z y) = 0%Z) -> ((ZOmod x y) = (y - 1%Z)%Z)).
+
+Axiom div_succ_1 : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z <  y)%Z) ->
+  (((ZOmod (x + 1%Z)%Z y) = 0%Z) ->
+  ((ZOdiv (x + 1%Z)%Z y) = ((ZOdiv x y) + 1%Z)%Z)).
+
+Axiom div_succ_2 : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z <  y)%Z) ->
+  ((~ ((ZOmod (x + 1%Z)%Z y) = 0%Z)) ->
+  ((ZOdiv (x + 1%Z)%Z y) = (ZOdiv x y))).
+
+Axiom mod_15 : forall (n:Z), ((ZOmod n 15%Z) = 0%Z) <->
+  (((ZOmod n 3%Z) = 0%Z) /\ ((ZOmod n 5%Z) = 0%Z)).
+
+Axiom triangle_numbers : forall (n:Z),
+  ((2%Z * (ZOdiv (n * (n + 1%Z)%Z)%Z 2%Z))%Z = (n * (n + 1%Z)%Z)%Z).
+
+Axiom Closed_formula_n : forall (n:Z), (0%Z <= n)%Z -> ((p n) ->
+  (((~ ((ZOmod (n + 1%Z)%Z 3%Z) = 0%Z)) /\
+  ~ ((ZOmod (n + 1%Z)%Z 5%Z) = 0%Z)) -> (p (n + 1%Z)%Z))).
+
+(* YOU MAY EDIT THE CONTEXT BELOW *)
+
+(* DO NOT EDIT BELOW *)
+
+Theorem Closed_formula_n_3 : forall (n:Z), (0%Z <= n)%Z -> ((p n) ->
+  ((((ZOmod (n + 1%Z)%Z 3%Z) = 0%Z) /\ ~ ((ZOmod (n + 1%Z)%Z 5%Z) = 0%Z)) ->
+  (p (n + 1%Z)%Z))).
+(* YOU MAY EDIT THE PROOF BELOW *)
+intros n Hn Hind (H3,H5).
+unfold p in *.
+rewrite SumYes; auto with zarith.
+rewrite Hind; clear Hind.
+unfold closed_formula.
+rewrite (div_succ_1 n 3); auto with zarith.
+rewrite (div_succ_2 n 5); auto with zarith.
+rewrite (div_succ_2 n 15); auto with zarith.
+2: generalize (mod_15 (n+1)); intuition.
+
+ring_simplify.
+
+Qed.
+(* DO NOT EDIT BELOW *)
+
+

examples/programs/euler001/euler001_SumMultiple_div_minus1_2_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)).
+
+Axiom 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 CONTEXT BELOW *)
+
+(* DO NOT EDIT BELOW *)
+
+Theorem div_minus1_2 : 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))).
+(* YOU MAY EDIT THE PROOF BELOW *)
+intros x y (Hx,Hy) H.
+pose (q := (x/ y)%Z).
+pose (r := (x mod y)%Z).
+assert (h2: (x = y * q + r)%Z).
+  apply (Z_div_mod_eq x y); auto with zarith.
+assert (h3: (0 <= r < y - 1)%Z).
+  admit.
+rewrite h2.
+rewrite Zmult_comm.
+rewrite <- Zplus_assoc.
+rewrite Z_div_plus_full_l; auto with zarith.
+rewrite Z_div_plus_full_l; auto with zarith.
+rewrite Zdiv_small; auto with zarith.
+rewrite Zdiv_small; auto with zarith.
+Qed.
+(* DO NOT EDIT BELOW *)
+
+

examples/programs/euler001/euler001_SumMultiple_div_minus1_2_2.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)).
+
+Axiom 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 CONTEXT BELOW *)
+
+(* DO NOT EDIT BELOW *)
+
+Theorem div_minus1_2 : 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))).
+(* YOU MAY EDIT THE PROOF BELOW *)
+intros x y (Hx,Hy) H.
+pose (q := (x/ y)%Z).
+pose (r := (x mod y)%Z).
+assert (h2: (x = y * q + r)%Z).
+  apply (Z_div_mod_eq x y); auto with zarith.
+assert (h3: (0 < r <= y - 1)%Z).
+  admit.
+Qed.
+(* DO NOT EDIT BELOW *)
+
+