Commit 016edab9 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

Euler example fully proved

parent 85aa8844
(* Euler Project, problem 1
(** {1 Euler Project, problem 1}
If we list all the natural numbers below 10 that are multiples of 3 or
5, we get 3, 5, 6 and 9. The sum of these multiples is 23.
......@@ -14,7 +14,7 @@ theory DivModHints
lemma mod_div_unique :
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
q = div x y /\ r = mod x y
lemma mod_succ_1 :
forall x y:int. x >= 0 /\ y > 0 ->
......@@ -32,6 +32,49 @@ theory DivModHints
forall x y:int. x >= 0 /\ y > 0 ->
mod (x+1) y <> 0 -> div (x+1) y = (div x y)
lemma mod2_mul2:
forall x:int. mod (2 * x) 2 = 0
lemma mod2_mul2_aux:
forall x y:int. mod (y * (2 * x)) 2 = 0
lemma mod2_mul2_aux2:
forall x y z t:int. mod (y * (2 * x) + z * (2 * t)) 2 = 0
lemma div2_mul2:
forall x:int. div (2 * x) 2 = x
lemma div2_mul2_aux:
forall x y:int. div (y * (2 * x)) 2 = y * x
lemma div2_add:
forall x y:int. mod x 2 = 0 /\ mod y 2 = 0 ->
div (x+y) 2 = div x 2 + div y 2
lemma div2_sub:
forall x y:int. mod x 2 = 0 /\ mod y 2 = 0 ->
div (x-y) 2 = div x 2 - div y 2
end
theory TriangularNumbers
use import int.Int
use import int.ComputerDivision
use import int.Div2
use DivModHints
lemma tr_mod_2:
forall n:int. n >= 0 -> mod (n*(n+1)) 2 = 0
function tr (n:int) : int = div (n*(n+1)) 2
lemma tr_repr:
forall n:int. n >= 0 -> n*(n+1) = 2 * tr n
lemma tr_succ:
forall n:int. n >= 0 -> tr (n+1) = tr n + n + 1
end
......@@ -54,49 +97,63 @@ theory SumMultiple
mod n 3 = 0 \/ mod n 5 = 0 ->
sum_multiple_3_5_lt (n+1) = sum_multiple_3_5_lt n + n
function closed_formula (n:int) : int =
use import TriangularNumbers
function closed_formula_aux (n:int) : int =
let n3 = div n 3 in
let n5 = div n 5 in
let n15 = div n 15 in
div (3 * n3 * (n3+1) +
5 * n5 * (n5+1) -
15 * n15 * (n15+1)) 2
3 * tr n3 + 5 * tr n5 - 15 * tr n15
predicate p (n:int) = sum_multiple_3_5_lt (n+1) = closed_formula n
lemma Closed_formula_0: p 0
predicate p (n:int) = sum_multiple_3_5_lt (n+1) = closed_formula_aux n
use DivModHints
use TriangularNumbers
lemma mod_15:
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_0: p 0
lemma Closed_formula_n:
forall n:int. n >= 0 -> p n ->
mod (n+1) 3 <> 0 /\ mod (n+1) 5 <> 0 -> p (n+1)
forall n:int. n > 0 -> p (n-1) ->
mod n 3 <> 0 /\ mod n 5 <> 0 -> p n
lemma Closed_formula_n_3:
forall n:int. n >= 0 -> p n ->
mod (n+1) 3 = 0 /\ mod (n+1) 5 <> 0 -> p (n+1)
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 ->
mod (n+1) 3 <> 0 /\ mod (n+1) 5 = 0 -> p (n+1)
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 ->
mod (n+1) 3 = 0 /\ mod (n+1) 5 = 0 -> p (n+1)
forall n:int. n > 0 -> p (n-1) ->
mod n 3 = 0 /\ mod n 5 = 0 -> p n
clone int.Induction as I with predicate p = p
constant b : int = 0
lemma Closed_formula:
clone int.Induction as I with constant bound = b, predicate p = p
lemma Closed_formula_ind:
forall n:int. 0 <= n -> p n
function closed_formula (n:int) : int =
let n3 = div n 3 in
let n5 = div n 5 in
let n15 = div n 15 in
div (3 * (n3 * (n3+1)) +
5 * (n5 * (n5+1)) -
15 * (n15 * (n15+1))) 2
lemma div_15: forall n:int. 0 <= n -> div n 15 >= 0
lemma div_5: forall n:int. 0 <= n -> div n 5 >= 0
lemma div_3: forall n:int. 0 <= n -> div n 3 >= 0
lemma Closed_Formula:
forall n:int. 0 <= n -> sum_multiple_3_5_lt (n+1) = closed_formula n
end
module Euler001
......@@ -115,7 +172,7 @@ module Euler001
end
(*
(***
Local Variables:
compile-command: "unset LANG; make -C ../.. examples/programs/euler001.gui"
End:
......
(* 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 int.Int.
Require int.Abs.
Require int.ComputerDivision.
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 div2_simpl : forall (x:Z) (y:Z), ((2%Z * x)%Z = y) ->
(x = (ZOdiv y 2%Z)).
(* Why3 goal *)
Theorem add_div2 : forall (x:Z) (y:Z), ((ZOmod x 2%Z) = 0%Z) ->
((ZOdiv (x + y)%Z 2%Z) = ((ZOdiv x 2%Z) + (ZOdiv y 2%Z))%Z).
intros x y Hx.
generalize (ZO_div_mod_eq x 2); intro h1.
rewrite Hx in h1.
rewrite h1.
simpl.
Qed.
(* 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 int.Int.
Require int.Abs.
Require int.ComputerDivision.
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)).
Axiom div2 : forall (x:Z), exists y:Z, (x = (2%Z * y)%Z) \/
(x = ((2%Z * y)%Z + 1%Z)%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 mod2_mul2 : forall (x:Z), ((ZOmod (2%Z * x)%Z 2%Z) = 0%Z).
Axiom mod2_mul2_aux : forall (x:Z) (y:Z),
((ZOmod (y * (2%Z * x)%Z)%Z 2%Z) = 0%Z).
Axiom mod2_mul2_aux2 : forall (x:Z) (y:Z) (z:Z) (t:Z),
((ZOmod ((y * (2%Z * x)%Z)%Z + (z * (2%Z * t)%Z)%Z)%Z 2%Z) = 0%Z).
Axiom div2_mul2 : forall (x:Z), ((ZOdiv (2%Z * x)%Z 2%Z) = x).
Axiom div2_mul2_aux : forall (x:Z) (y:Z),
((ZOdiv (y * (2%Z * x)%Z)%Z 2%Z) = (y * x)%Z).
Axiom div2_add : forall (x:Z) (y:Z), (((ZOmod x 2%Z) = 0%Z) /\
((ZOmod y 2%Z) = 0%Z)) ->
((ZOdiv (x + y)%Z 2%Z) = ((ZOdiv x 2%Z) + (ZOdiv y 2%Z))%Z).
Axiom div2_sub : forall (x:Z) (y:Z), (((ZOmod x 2%Z) = 0%Z) /\
((ZOmod y 2%Z) = 0%Z)) ->
((ZOdiv (x - y)%Z 2%Z) = ((ZOdiv x 2%Z) - (ZOdiv y 2%Z))%Z).
Axiom tr_mod_2 : forall (n:Z), (0%Z <= n)%Z ->
((ZOmod (n * (n + 1%Z)%Z)%Z 2%Z) = 0%Z).
(* Why3 assumption *)
Definition tr(n:Z): Z := (ZOdiv (n * (n + 1%Z)%Z)%Z 2%Z).
Axiom tr_repr : forall (n:Z), (0%Z <= n)%Z ->
((n * (n + 1%Z)%Z)%Z = (2%Z * (tr n))%Z).
Axiom tr_succ : forall (n:Z), (0%Z <= n)%Z ->
((tr (n + 1%Z)%Z) = (((tr n) + n)%Z + 1%Z)%Z).
(* Why3 assumption *)
Definition closed_formula_aux(n:Z): Z := let n3 := (ZOdiv n 3%Z) in let n5 :=
(ZOdiv n 5%Z) in let n15 := (ZOdiv n 15%Z) in
(((3%Z * (tr n3))%Z + (5%Z * (tr n5))%Z)%Z - (15%Z * (tr n15))%Z)%Z.
(* Why3 assumption *)
Definition p(n:Z): Prop :=
((sum_multiple_3_5_lt (n + 1%Z)%Z) = (closed_formula_aux n)).
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 Closed_formula_0 : (p 0%Z).
Axiom Closed_formula_n : forall (n:Z), (0%Z < n)%Z -> ((p (n - 1%Z)%Z) ->
(((~ ((ZOmod n 3%Z) = 0%Z)) /\ ~ ((ZOmod n 5%Z) = 0%Z)) -> (p n))).
Axiom Closed_formula_n_3 : forall (n:Z), (0%Z < n)%Z -> ((p (n - 1%Z)%Z) ->
((((ZOmod n 3%Z) = 0%Z) /\ ~ ((ZOmod n 5%Z) = 0%Z)) -> (p n))).
Axiom Closed_formula_n_5 : forall (n:Z), (0%Z < n)%Z -> ((p (n - 1%Z)%Z) ->
(((~ ((ZOmod n 3%Z) = 0%Z)) /\ ((ZOmod n 5%Z) = 0%Z)) -> (p n))).
Axiom Closed_formula_n_15 : forall (n:Z), (0%Z < n)%Z -> ((p (n - 1%Z)%Z) ->
((((ZOmod n 3%Z) = 0%Z) /\ ((ZOmod n 5%Z) = 0%Z)) -> (p n))).
Axiom Induction : (forall (n:Z), (0%Z <= n)%Z -> ((forall (k:Z),
((0%Z <= k)%Z /\ (k < n)%Z) -> (p k)) -> (p n))) -> forall (n:Z),
(0%Z <= n)%Z -> (p n).
Axiom Induction_bound : (forall (n:Z), (0%Z <= n)%Z -> ((forall (k:Z),
((0%Z <= k)%Z /\ (k < n)%Z) -> (p k)) -> (p n))) -> forall (n:Z),
(0%Z <= n)%Z -> (p n).
Axiom Closed_formula_ind : forall (n:Z), (0%Z <= n)%Z -> (p n).
(* Why3 assumption *)
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 * (n3 + 1%Z)%Z)%Z)%Z + (5%Z * (n5 * (n5 + 1%Z)%Z)%Z)%Z)%Z - (15%Z * (n15 * (n15 + 1%Z)%Z)%Z)%Z)%Z 2%Z).
Axiom div_15 : forall (n:Z), (0%Z <= n)%Z -> (0%Z <= (ZOdiv n 15%Z))%Z.
Axiom div_5 : forall (n:Z), (0%Z <= n)%Z -> (0%Z <= (ZOdiv n 5%Z))%Z.
Axiom div_3 : forall (n:Z), (0%Z <= n)%Z -> (0%Z <= (ZOdiv n 3%Z))%Z.
(* Why3 goal *)
Theorem Closed_Formula : forall (n:Z), (0%Z <= n)%Z ->
((sum_multiple_3_5_lt (n + 1%Z)%Z) = (closed_formula n)).
intros n Hn.
rewrite Closed_formula_ind; auto.
unfold closed_formula_aux, closed_formula.
repeat rewrite tr_repr.
rewrite div2_sub.
rewrite div2_mul2_aux.
rewrite div2_add.
do 2 rewrite div2_mul2_aux.
auto.
repeat rewrite mod2_mul2_aux; auto.
rewrite mod2_mul2_aux; auto.
rewrite mod2_mul2_aux2; auto.
apply div_15; auto.
apply div_5; auto.
apply div_3; auto.
Qed.
(* 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 int.Int.
Require int.Abs.
Require int.ComputerDivision.
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)).
Axiom div2 : forall (x:Z), exists y:Z, (x = (2%Z * y)%Z) \/
(x = ((2%Z * y)%Z + 1%Z)%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 mod2_mul2 : forall (x:Z), ((ZOmod (2%Z * x)%Z 2%Z) = 0%Z).
Axiom mod2_mul2_aux : forall (x:Z) (y:Z),
((ZOmod (y * (2%Z * x)%Z)%Z 2%Z) = 0%Z).
Axiom mod2_mul2_aux2 : forall (x:Z) (y:Z) (z:Z),
((ZOmod ((y * (2%Z * x)%Z)%Z + z)%Z 2%Z) = (ZOmod z 2%Z)).
Axiom div2_mul2 : forall (x:Z), ((ZOdiv (2%Z * x)%Z 2%Z) = x).
Axiom div2_mul2_aux : forall (x:Z) (y:Z),
((ZOdiv (y * (2%Z * x)%Z)%Z 2%Z) = (y * x)%Z).
Axiom div2_add : forall (x:Z) (y:Z), (((ZOmod x 2%Z) = 0%Z) /\
((ZOmod y 2%Z) = 0%Z)) ->
((ZOdiv (x + y)%Z 2%Z) = ((ZOdiv x 2%Z) + (ZOdiv y 2%Z))%Z).
Axiom div2_sub : forall (x:Z) (y:Z), (((ZOmod x 2%Z) = 0%Z) /\
((ZOmod y 2%Z) = 0%Z)) ->
((ZOdiv (x - y)%Z 2%Z) = ((ZOdiv x 2%Z) - (ZOdiv y 2%Z))%Z).
Axiom tr_mod_2 : forall (n:Z), (0%Z <= n)%Z ->
((ZOmod (n * (n + 1%Z)%Z)%Z 2%Z) = 0%Z).
(* Why3 assumption *)
Definition tr(n:Z): Z := (ZOdiv (n * (n + 1%Z)%Z)%Z 2%Z).
Axiom tr_repr : forall (n:Z), (0%Z <= n)%Z ->
((n * (n + 1%Z)%Z)%Z = (2%Z * (tr n))%Z).
Axiom tr_succ : forall (n:Z), (0%Z <= n)%Z ->
((tr (n + 1%Z)%Z) = (((tr n) + n)%Z + 1%Z)%Z).
(* Why3 assumption *)
Definition closed_formula_aux(n:Z): Z := let n3 := (ZOdiv n 3%Z) in let n5 :=
(ZOdiv n 5%Z) in let n15 := (ZOdiv n 15%Z) in
(((3%Z * (tr n3))%Z + (5%Z * (tr n5))%Z)%Z - (15%Z * (tr n15))%Z)%Z.
(* Why3 assumption *)
Definition p(n:Z): Prop :=
((sum_multiple_3_5_lt (n + 1%Z)%Z) = (closed_formula_aux n)).
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 Closed_formula_0 : (p 0%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))).
Axiom 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))).
Axiom Closed_formula_n_5 : 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))).
Axiom Closed_formula_n_15 : 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))).
Axiom Induction : (forall (n:Z), (0%Z <= n)%Z -> ((forall (k:Z),
((0%Z <= k)%Z /\ (k < n)%Z) -> (p k)) -> (p n))) -> forall (n:Z),
(0%Z <= n)%Z -> (p n).
Axiom Induction_bound : (forall (n:Z), (0%Z <= n)%Z -> ((forall (k:Z),
((0%Z <= k)%Z /\ (k < n)%Z) -> (p k)) -> (p n))) -> forall (n:Z),
(0%Z <= n)%Z -> (p n).
(* Why3 goal *)
Theorem Closed_formula_ind : forall (n:Z), (0%Z <= n)%Z -> (p n).
apply Induction_bound.
intros n Hn Hind.
assert (h: (n=0 \/ n > 0)) by omega.
destruct h.
subst; apply Closed_formula_0.
assert (h: (Z0mod n=0 \/ n > 0)) by omega.
Qed.
......@@ -3,12 +3,12 @@
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).
Require int.Int.
Require int.Abs.
Require int.ComputerDivision.
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)) /\
......@@ -19,31 +19,33 @@ 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)).
(* Why3 assumption *)
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).
(* Why3 assumption *)
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))).
((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) ->
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) ->
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) ->
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) ->
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))).
......@@ -51,16 +53,22 @@ 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).
((ZOmod (n * (n + 1%Z)%Z)%Z 2%Z) = 0%Z).
Axiom div2_simpl : forall (x:Z) (y:Z), ((2%Z * x)%Z = y) ->
(x = (ZOdiv y 2%Z)).
Axiom add_div2 : forall (x:Z) (y:Z), ((ZOmod x 2%Z) = 0%Z) ->
((ZOdiv (x + y)%Z 2%Z) = ((ZOdiv x 2%Z) + (ZOdiv y 2%Z))%Z).
Axiom Closed_formula_n : forall (n:Z), (0%Z <= n)%Z -> ((p n) ->
(((~ ((ZOmod (n + 1%Z)%Z 3%Z) = 0%Z)) /\