theory Hw01_Comments
imports Main
begin
text \This file contains the solution for homework 1,
and some comments on the solution variants I saw
during correction:\
fun snoc :: "'a list \ 'a \ 'a list" where
"snoc [] x = [x]" |
"snoc (y # ys) x = y # (snoc ys x)"
fun reverse :: "'a list \ 'a list" where
"reverse [] = []" |
"reverse (x # xs) = snoc (reverse xs) x"
text \Here, the most common solution was the following:\
fun lsum :: "nat list \ nat" where
"lsum [] = 0"
| "lsum (x#xs) = x + lsum xs"
text \This was also solved by most people, using the straightforward approach\
lemma "lsum (reverse xs) = lsum xs"
apply (induction xs)
apply auto
(** here, you see in the remaining subgoal:
lsum (snoc (reverse xs) a) = ...
and you would like to rewrite it to a + lsum (snoc ...) to apply the
induction hypothesis. So, prove the following auxiliary lemma:
**)
oops
lemma aux: "lsum (snoc xs x) = x + lsum xs" by (induction xs) auto
text \Now, the proof goes through:\
lemma "lsum (reverse xs) = lsum xs"
by (induction xs) (auto simp: aux)
text \Some stated the auxiliary lemma directed in the other way, i.e.,
@{term "x + lsum xs = lsum (snoc xs x)"}.
While this works for this part, it will cause trouble when proving Gauss:
Adding this lemma to the simplifier, instructs the simplifier
to rewrite all additions to an lsum to a "snoc".
Thus, there is no chance to apply lemmas about addition ...
\
text \This was solved by most people like this: \
fun nlist :: "nat \ nat list" where
"nlist 0 = []"
| "nlist (Suc n) = snoc (nlist n) (Suc n)"
lemma "lsum (nlist n) = n * (n+1) div 2"
by (induction n) (auto simp: aux)
text \Some people discovered list-comprehension syntax: \
definition "nlist' n \ [1..Then, an auxiliary lemma about lsum and list concatenation is required:\
lemma aux2: "lsum (xs@ys) = lsum xs + lsum ys" by (induction xs) auto
lemma "lsum (nlist' n) = n * (n+1) div 2"
unfolding nlist'_def
by (induction n) (auto simp: aux2)
end