From e37d1692c9288adc54d42c2791efb8a445079a1f Mon Sep 17 00:00:00 2001
From: wadler <wadler@inf.ed.ac.uk>
Date: Wed, 7 Feb 2018 11:46:48 -0400
Subject: [PATCH] added ListsAns

---
 src/Lists.lagda         | 68 ++++++++++++++++++++++++-----------------
 src/ListsAns.lagda      | 56 +++++++++++++++++++++++++++++++++
 src/PropertiesAns.lagda |  2 +-
 3 files changed, 97 insertions(+), 29 deletions(-)
 create mode 100644 src/ListsAns.lagda

diff --git a/src/Lists.lagda b/src/Lists.lagda
index 330049a9..7da395f5 100644
--- a/src/Lists.lagda
+++ b/src/Lists.lagda
@@ -14,7 +14,7 @@ import Relation.Binary.PropositionalEquality as Eq
 open Eq using (_≡_; refl; sym; trans; cong)
 open Eq.≡-Reasoning
 open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
-open import Data.Nat.Properties.Simple using (distribʳ-*-+)
+open import Data.Nat.Properties.Simple using (distribʳ-*-+; *-comm)
 \end{code}
 
 ## Lists
@@ -380,33 +380,6 @@ of the first list, reversing a list in this way takes
 time proportional to the *square* of the length of the
 list, since `1 + ⋯ + n ≡ n * (n + 1) / 2`.
 
-\begin{code}
-upto : ℕ → List ℕ
-upto zero = []
-upto (suc n) = suc n ∷ upto n
-
-sum : List ℕ → ℕ
-sum [] = zero
-sum (x ∷ xs) = x + sum xs
-
-sum-upto : ∀ (n : ℕ) → 2 * sum (upto n) ≡ n * suc n
-sum-upto zero = refl
-sum-upto (suc n) = {!!}
-{-
-  begin
-    2 * sum (upto (suc n))
-  ≡⟨⟩
-    2 * sum (suc n ∷ upto n)
-  ≡⟨⟩
-    2 * (suc n + sum (upto n))
-  ≡⟨ +-dist-* 2 (suc n) (sum (upto n)) ⟩
-    (2 * suc n) + (2 * sum (upto n))
-  ≡⟨ cong (_+_ (2 * suc n)) (sup-upto n) ⟩
-    (2 * suc n) + (n * suc n)
-  ≡⟨ sym (+-dist-* 
--}
-\end{code}
-
 
 
 ## Reverse
@@ -431,6 +404,45 @@ ex₆ : foldr _+_ 0 ([ 1 , 2 , 3 ]) ≡ 6
 ex₆ = refl
 \end{code}
 
+\begin{code}
+downto : ℕ → List ℕ
+downto zero = []
+downto (suc n) = suc n ∷ downto n
+
+sum : List ℕ → ℕ
+sum = foldr _+_ 0
+
+infix 6 _+
+
+_+ : ℕ → ℕ → ℕ
+(m +) n = m + n
+
+cong2 : ∀ {A B C : Set} {x x′ : A} {y y′ : B} →
+  (f : A → B → C) → (x ≡ x′) → (y ≡ y′) → (f x y ≡ f x′ y′)
+cong2 f x≡x′ y≡y′ rewrite x≡x′ | y≡y′ = refl
+
+sum-downto : ∀ (n : ℕ) → sum (downto n) * 2 ≡ suc n * n
+sum-downto zero = refl
+sum-downto (suc n) = 
+  begin
+    sum (downto (suc n)) * 2
+  ≡⟨⟩
+    sum (suc n ∷ downto n) * 2
+  ≡⟨⟩
+    (suc n + sum (downto n)) * 2
+  ≡⟨ distribʳ-*-+ 2 (suc n) (sum (downto n)) ⟩
+    suc n * 2 + sum (downto n) * 2
+  ≡⟨ cong (suc n * 2 +) (sum-downto n) ⟩
+    suc n * 2 + suc n * n
+  ≡⟨ cong2 _+_ (*-comm (suc n) 2) (*-comm (suc n) n) ⟩
+    2 * suc n + n * suc n
+  ≡⟨ sym (distribʳ-*-+ (suc n) 2 n)⟩
+    (2 + n) * suc n
+  ∎
+\end{code}
+
+
+
 
 \begin{code}
 data _∈_ {A : Set} (x : A) : List A → Set where
diff --git a/src/ListsAns.lagda b/src/ListsAns.lagda
new file mode 100644
index 00000000..2218490d
--- /dev/null
+++ b/src/ListsAns.lagda
@@ -0,0 +1,56 @@
+---
+title     : "Lists Answers"
+layout    : page
+permalink : /ListsAns
+---
+
+\begin{code}
+import Relation.Binary.PropositionalEquality as Eq
+open Eq using (_≡_; refl; sym; trans; cong)
+open Eq.≡-Reasoning
+open import Data.Nat using (ℕ; suc; zero; _+_; _*_)
+open import Data.Nat.Properties.Simple using (*-comm; distribʳ-*-+)
+open import Data.List using (List; []; _∷_; _++_; foldr)
+
+*-distrib-+ : ∀ (m n p : ℕ) → (m + n) * p ≡ m * p + n * p
+*-distrib-+ m n p = distribʳ-*-+ p m n
+\end{code}
+
+*Sum of count*
+
+\begin{code}
+sum : List ℕ → ℕ
+sum = foldr _+_ 0
+
+countdown : ℕ → List ℕ
+countdown zero = []
+countdown (suc n) = suc n ∷ countdown n
+
+infix 6 _+
+
+_+ : ℕ → ℕ → ℕ
+(m +) n = m + n
+
+cong2 : ∀ {A B C : Set} {x x′ : A} {y y′ : B} →
+  (f : A → B → C) → (x ≡ x′) → (y ≡ y′) → (f x y ≡ f x′ y′)
+cong2 f x≡x′ y≡y′ rewrite x≡x′ | y≡y′ = refl
+
+sum-countdown : ∀ (n : ℕ) → sum (countdown n) * 2 ≡ suc n * n
+sum-countdown zero = refl
+sum-countdown (suc n) = 
+  begin
+    sum (countdown (suc n)) * 2
+  ≡⟨⟩
+    sum (suc n ∷ countdown n) * 2
+  ≡⟨⟩
+    (suc n + sum (countdown n)) * 2
+  ≡⟨ *-distrib-+ (suc n) (sum (countdown n)) 2 ⟩
+    suc n * 2 + sum (countdown n) * 2
+  ≡⟨ cong (suc n * 2 +) (sum-countdown n) ⟩
+    suc n * 2 + suc n * n
+  ≡⟨ cong2 _+_ (*-comm (suc n) 2) (*-comm (suc n) n) ⟩
+    2 * suc n + n * suc n
+  ≡⟨ sym (*-distrib-+ 2 n (suc n))⟩
+    (2 + n) * suc n
+  ∎
+\end{code}
diff --git a/src/PropertiesAns.lagda b/src/PropertiesAns.lagda
index 9883bf94..06c6da6f 100644
--- a/src/PropertiesAns.lagda
+++ b/src/PropertiesAns.lagda
@@ -6,7 +6,7 @@ permalink : /PropertiesAns
 
 \begin{code}
 open import Data.Nat using (ℕ; suc; zero; _+_; _*_; _∸_)
-open import Properties using (+-assoc; +-comm)
+open import Data.Nat.Properties.Simple using (+-assoc; +-comm)
 open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym)
 
 \end{code}