author lammich Mon, 14 Aug 2017 18:32:46 -0400 changeset 69892 e8e97a214e48 parent 69891 6625f13189b9 child 69893 7ca4cbbd7bb9
updated
```--- a/Exercises/hwsubm/OR/Keinholz_Jonas_jonas.keinholz@tum.de_658/project_euler.thy	Fri Aug 11 13:40:41 2017 +0200
+++ b/Exercises/hwsubm/OR/Keinholz_Jonas_jonas.keinholz@tum.de_658/project_euler.thy	Mon Aug 14 18:32:46 2017 -0400
@@ -1,7 +1,44 @@
-(*\<Rightarrow> Max *)
+(** Score: 13/15
+
+The student took the first two problems of Project Euler and came up with solutions
+via functional programs, proved that the programs compute the desired results and
+finally extracted the code equations to Haskell.
+With some unverified wrapper the two programscould be submitted to hackerrank and be tested.
+The students does not state what the results of these submissions are, but it seems
+reasonable that they perform well.
+
+The two problems are:
+
+1:
+for a number n, find the sum of all numbers smaller n that are multiples of 3 or 5.
+
+evaluation:
++ direct definition of the desired result (solve001)
++ naive implementation + correctness proof (solve001_naive)
++ implementation with closed form + correctness proof (solve001_ap)
++ successfull code extraction
+
+2:
+for a number n, find the sum of all even-valued fibonacci numbers smaller than n.
+evaluation:
++ definition of fibonacci sequence (generalized starting numbers) (fibonacci_seq)
++ efficient enumeration of fibonacci sequence (fibonaccis)
++ correctness proof wrt to fibonacci_seq
++ implementation of desired result with "fibonaccis", filter, sum (solve002)
+- missing proof whether this matches the desired result (definition, + correctness proof), which
+  on the other hand would not have been too much more work.
++ successfull code extraction
+
+ideas for improvements:
+for a better runtime one could as a first step observe that every forth fib-number is even...
+
+
+
+*)

section \<open>Formally verified solutions to Project Euler problems\<close>

+
text \<open>
Formally verified solutions to the first two Project Euler problems (https://projecteuler.net)

@@ -89,6 +126,22 @@
finally show ?thesis .
qed

+(** maybe a shorter proof is possible,
+ try to reuse the lemmas you find in the library to ease your life :)
+lemma assumes inj_f: "inj f"
+  shows "\<Sum>{f k | k. k \<le> n} = sum f {..n}"
+proof -
+  have "{f k | k. k \<le> n} = (f ` {..n})" by auto
+      then
+  have "\<Sum>{f k | k. k \<le> n} = \<Sum> (f ` {..n})" by auto
+  moreover have
+    "\<dots> = sum f {..n}" using inj_f
+    by (metis injD inj_on_def sum.reindex_cong)
+  finally show ?thesis .
+qed
+*)
+
+
lemma Sum_f:
fixes f :: "nat \<Rightarrow> nat"
assumes "inj f"
@@ -184,7 +237,7 @@
using sum_distrib_left[where r = m and f = "\<lambda>k. k"] by auto
also have "\<dots> = m * (((n - 1) div m) * ((n - 1) div m + 1) div 2)"
proof -
-    {
+    { (** move out as a lemma for better proof structure *)
fix n :: nat
have "\<Sum>{..n} = n * (n + 1) div 2"
by (induction n) auto```
`Binary file Exercises/hwsubm/scores.ods has changed`