examples/euler001/euler001_SumMultiple_Closed_Formula_1.v

   1 (* This file is generated by Why3's Coq driver *)
   2 (* Beware! Only edit allowed sections below    *)
   3 Require Import ZArith.
   4 Require Import Rbase.
   5 Require Import ZOdiv.
   6 Require int.Int.
   7 Require int.Abs.
   8 Require int.ComputerDivision.
   9
  10 Parameter sum_multiple_3_5_lt: Z -> Z.
  11
  12 Axiom SumEmpty : ((sum_multiple_3_5_lt 0%Z) = 0%Z).
  13
  14 Axiom SumNo : forall (n:Z), (0%Z <= n)%Z -> (((~ ((ZOmod n 3%Z) = 0%Z)) /\
  15   ~ ((ZOmod n 5%Z) = 0%Z)) ->
  16   ((sum_multiple_3_5_lt (n + 1%Z)%Z) = (sum_multiple_3_5_lt n))).
  17
  18 Axiom SumYes : forall (n:Z), (0%Z <= n)%Z -> ((((ZOmod n 3%Z) = 0%Z) \/
  19   ((ZOmod n 5%Z) = 0%Z)) ->
  20   ((sum_multiple_3_5_lt (n + 1%Z)%Z) = ((sum_multiple_3_5_lt n) + n)%Z)).
  21
  22 Axiom div2 : forall (x:Z), exists y:Z, (x = (2%Z * y)%Z) \/
  23   (x = ((2%Z * y)%Z + 1%Z)%Z).
  24
  25 Axiom mod_div_unique : forall (x:Z) (y:Z) (q:Z) (r:Z), ((0%Z <= x)%Z /\
  26   ((0%Z < y)%Z /\ ((x = ((q * y)%Z + r)%Z) /\ ((0%Z <= r)%Z /\
  27   (r < y)%Z)))) -> ((q = (ZOdiv x y)) /\ (r = (ZOmod x y))).
  28
  29 Axiom mod_succ_1 : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z < y)%Z) ->
  30   ((~ ((ZOmod (x + 1%Z)%Z y) = 0%Z)) ->
  31   ((ZOmod (x + 1%Z)%Z y) = ((ZOmod x y) + 1%Z)%Z)).
  32
  33 Axiom mod_succ_2 : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z < y)%Z) ->
  34   (((ZOmod (x + 1%Z)%Z y) = 0%Z) -> ((ZOmod x y) = (y - 1%Z)%Z)).
  35
  36 Axiom div_succ_1 : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z < y)%Z) ->
  37   (((ZOmod (x + 1%Z)%Z y) = 0%Z) ->
  38   ((ZOdiv (x + 1%Z)%Z y) = ((ZOdiv x y) + 1%Z)%Z)).
  39
  40 Axiom div_succ_2 : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z < y)%Z) ->
  41   ((~ ((ZOmod (x + 1%Z)%Z y) = 0%Z)) ->
  42   ((ZOdiv (x + 1%Z)%Z y) = (ZOdiv x y))).
  43
  44 Axiom mod2_mul2 : forall (x:Z), ((ZOmod (2%Z * x)%Z 2%Z) = 0%Z).
  45
  46 Axiom mod2_mul2_aux : forall (x:Z) (y:Z),
  47   ((ZOmod (y * (2%Z * x)%Z)%Z 2%Z) = 0%Z).
  48
  49 Axiom mod2_mul2_aux2 : forall (x:Z) (y:Z) (z:Z) (t:Z),
  50   ((ZOmod ((y * (2%Z * x)%Z)%Z + (z * (2%Z * t)%Z)%Z)%Z 2%Z) = 0%Z).
  51
  52 Axiom div2_mul2 : forall (x:Z), ((ZOdiv (2%Z * x)%Z 2%Z) = x).
  53
  54 Axiom div2_mul2_aux : forall (x:Z) (y:Z),
  55   ((ZOdiv (y * (2%Z * x)%Z)%Z 2%Z) = (y * x)%Z).
  56
  57 Axiom div2_add : forall (x:Z) (y:Z), (((ZOmod x 2%Z) = 0%Z) /\
  58   ((ZOmod y 2%Z) = 0%Z)) ->
  59   ((ZOdiv (x + y)%Z 2%Z) = ((ZOdiv x 2%Z) + (ZOdiv y 2%Z))%Z).
  60
  61 Axiom div2_sub : forall (x:Z) (y:Z), (((ZOmod x 2%Z) = 0%Z) /\
  62   ((ZOmod y 2%Z) = 0%Z)) ->
  63   ((ZOdiv (x - y)%Z 2%Z) = ((ZOdiv x 2%Z) - (ZOdiv y 2%Z))%Z).
  64
  65 Axiom tr_mod_2 : forall (n:Z), (0%Z <= n)%Z ->
  66   ((ZOmod (n * (n + 1%Z)%Z)%Z 2%Z) = 0%Z).
  67
  68 (* Why3 assumption *)
  69 Definition tr(n:Z): Z := (ZOdiv (n * (n + 1%Z)%Z)%Z 2%Z).
  70
  71 Axiom tr_repr : forall (n:Z), (0%Z <= n)%Z ->
  72   ((n * (n + 1%Z)%Z)%Z = (2%Z * (tr n))%Z).
  73
  74 Axiom tr_succ : forall (n:Z), (0%Z <= n)%Z ->
  75   ((tr (n + 1%Z)%Z) = (((tr n) + n)%Z + 1%Z)%Z).
  76
  77 (* Why3 assumption *)
  78 Definition closed_formula_aux(n:Z): Z := let n3 := (ZOdiv n 3%Z) in let n5 :=
  79   (ZOdiv n 5%Z) in let n15 := (ZOdiv n 15%Z) in
  80   (((3%Z * (tr n3))%Z + (5%Z * (tr n5))%Z)%Z - (15%Z * (tr n15))%Z)%Z.
  81
  82 (* Why3 assumption *)
  83 Definition p(n:Z): Prop :=
  84   ((sum_multiple_3_5_lt (n + 1%Z)%Z) = (closed_formula_aux n)).
  85
  86 Axiom mod_15 : forall (n:Z), ((ZOmod n 15%Z) = 0%Z) <->
  87   (((ZOmod n 3%Z) = 0%Z) /\ ((ZOmod n 5%Z) = 0%Z)).
  88
  89 Axiom Closed_formula_0 : (p 0%Z).
  90
  91 Axiom Closed_formula_n : forall (n:Z), (0%Z < n)%Z -> ((p (n - 1%Z)%Z) ->
  92   (((~ ((ZOmod n 3%Z) = 0%Z)) /\ ~ ((ZOmod n 5%Z) = 0%Z)) -> (p n))).
  93
  94 Axiom Closed_formula_n_3 : forall (n:Z), (0%Z < n)%Z -> ((p (n - 1%Z)%Z) ->
  95   ((((ZOmod n 3%Z) = 0%Z) /\ ~ ((ZOmod n 5%Z) = 0%Z)) -> (p n))).
  96
  97 Axiom Closed_formula_n_5 : forall (n:Z), (0%Z < n)%Z -> ((p (n - 1%Z)%Z) ->
  98   (((~ ((ZOmod n 3%Z) = 0%Z)) /\ ((ZOmod n 5%Z) = 0%Z)) -> (p n))).
  99
 100 Axiom Closed_formula_n_15 : forall (n:Z), (0%Z < n)%Z -> ((p (n - 1%Z)%Z) ->
 101   ((((ZOmod n 3%Z) = 0%Z) /\ ((ZOmod n 5%Z) = 0%Z)) -> (p n))).
 102
 103 Axiom Induction : (forall (n:Z), (0%Z <= n)%Z -> ((forall (k:Z),
 104   ((0%Z <= k)%Z /\ (k < n)%Z) -> (p k)) -> (p n))) -> forall (n:Z),
 105   (0%Z <= n)%Z -> (p n).
 106
 107 Axiom Induction_bound : (forall (n:Z), (0%Z <= n)%Z -> ((forall (k:Z),
 108   ((0%Z <= k)%Z /\ (k < n)%Z) -> (p k)) -> (p n))) -> forall (n:Z),
 109   (0%Z <= n)%Z -> (p n).
 110
 111 Axiom Closed_formula_ind : forall (n:Z), (0%Z <= n)%Z -> (p n).
 112
 113 (* Why3 assumption *)
 114 Definition closed_formula(n:Z): Z := let n3 := (ZOdiv n 3%Z) in let n5 :=
 115   (ZOdiv n 5%Z) in let n15 := (ZOdiv n 15%Z) in
 116   (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).
 117
 118 Axiom div_15 : forall (n:Z), (0%Z <= n)%Z -> (0%Z <= (ZOdiv n 15%Z))%Z.
 119
 120 Axiom div_5 : forall (n:Z), (0%Z <= n)%Z -> (0%Z <= (ZOdiv n 5%Z))%Z.
 121
 122 Axiom div_3 : forall (n:Z), (0%Z <= n)%Z -> (0%Z <= (ZOdiv n 3%Z))%Z.
 123
 124 (* Why3 goal *)
 125 Theorem Closed_Formula : forall (n:Z), (0%Z <= n)%Z ->
 126   ((sum_multiple_3_5_lt (n + 1%Z)%Z) = (closed_formula n)).
 127 intros n Hn.
 128 rewrite Closed_formula_ind; auto.
 129 unfold closed_formula_aux, closed_formula.
 130 repeat rewrite tr_repr.
 131 rewrite div2_sub.
 132 rewrite div2_mul2_aux.
 133 rewrite div2_add.
 134 do 2 rewrite div2_mul2_aux.
 135 auto.
 136 repeat rewrite mod2_mul2_aux; auto.
 137 rewrite mod2_mul2_aux; auto.
 138 rewrite mod2_mul2_aux2; auto.
 139 apply div_15; auto.
 140 apply div_5; auto.
 141 apply div_3; auto.
 142 Qed.
 143
 144