Solve Q14,Q15

Src.lean

@@ -1,5 +1,7 @@
 import Src.Problem1
 import Src.Problem10
+import Src.Problem14
+import Src.Problem15
 import Src.Problem2
 import Src.Problem3
 import Src.Problem31

Src/Problem14.lean

@@ -0,0 +1,21 @@
+/-
+  # Problem 14
+  Duplicate the elements of a list.
+-/
+
+variable {α : Type}
+
+def dupli (l : List α) : List α :=
+  -- sorry
+  match l with
+  | [] => []
+  | a :: b => a :: a :: dupli b
+  -- sorry
+
+-- The following code is a test case and you should not change it.
+
+example : dupli [1,2,3] = [1,1,2,2,3,3] := by rfl
+
+example : dupli ([] : List α) = [] := by rfl
+
+example : dupli ['a','b','c','c','d'] = ['a','a','b','b','c','c','c','c','d','d'] := by rfl

Src/Problem15.lean

@@ -0,0 +1,29 @@
+/-
+  # Problem 15
+  Replicate the elements of a list a given number of times.
+-/
+
+variable {α : Type}
+
+def repli (l : List α)(n : Nat) : List α :=
+  -- sorry
+  match l with
+  | [] => []
+  | a :: b => (solorepl a n) ++ repli b n
+  where solorepl (x : α)(n : Nat) : List α :=
+    match n with
+    | 0 => []
+    | Nat.succ m => x :: solorepl x m
+  -- sorry
+
+-- The following code is a test case and you should not change it.
+
+example : repli [1,2,3] 3 = [1,1,1,2,2,2,3,3,3] := by rfl
+
+example : repli [1,2,3] 2 = [1,1,2,2,3,3] := by rfl
+
+example : repli [1,2,3] 1 = [1,2,3] := by rfl
+
+example : repli [1,2,3] 0 = [] := by rfl
+
+example : repli ([] : List α) 255 = [] := by rfl

md/SUMMARY.md

@@ -15,6 +15,11 @@
 * [9: Pack consecutive duplicates](./build/Problem9.md)
 * [10: Run-length encoding](./build/Problem10.md)
 
+# 11-20: Lists, continued
+
+* [14: Duplicate elements](./build/Problem14.md)
+* [15: Replicate elements K times](./build/Problem15.md)
+
 # 31-40: Arithmetic
 
 * [31: Prime number detection](./build/Problem31.md)