/- Exercise 1.2: Basics — Proofs -/
/- Question 1: Natural numbers -/
namespace my_nat
def add : ℕ → ℕ → ℕ
| 0 n := n
| (nat.succ m) n := nat.succ (add m n)
/- We proved these properties already in the lecture, so we take them as axioms here. (We will often
use `sorry` like this to avoid clutter in exercise sheets. But keep in mind that `sorry` is a risky
construct.) -/
lemma add_zero : ∀m : ℕ, add m 0 = m := sorry
lemma add_succ : ∀m n : ℕ, add m (nat.succ n) = nat.succ (add m n) := sorry
lemma add_comm : ∀m n : ℕ, add m n = add n m := sorry
lemma add_assoc : ∀l m n : ℕ, add (add l m) n = add l (add m n) := sorry
instance : is_commutative ℕ add := ⟨add_comm⟩
instance : is_associative ℕ add := ⟨add_assoc⟩
def mul : ℕ → ℕ → ℕ
| 0 _ := 0
| (nat.succ m) n := add n (mul m n)
lemma mul_add (m n : ℕ) : ∀l : ℕ, mul (add l m) n = add (mul l n) (mul m n) := sorry
/- 1.1. Prove the following recursive equations on the second argument of `mul`. -/
lemma mul_zero : ∀m : ℕ, mul m 0 = 0
| 0 := by refl
| (nat.succ m) := by simp [add, mul, mul_zero m]
lemma mul_succ : ∀m n : ℕ, mul m (nat.succ n) = add (mul m n) m
| 0 n := by refl
| (nat.succ m) n := by simp [add, add_succ, add_assoc, mul, mul_succ m]
/- 1.2. Prove commutativity and associativity of multiplication by induction. Choose the induction
variable carefully. Use the pattern matching syntax. -/
lemma mul_comm : ∀m n : ℕ, mul m n = mul n m
| 0 n := by simp [mul, mul_zero]
| (nat.succ m) n := begin simp [mul, mul_succ, mul_comm m], ac_refl end
lemma mul_assoc : ∀l m n : ℕ, mul (mul l m) n = mul l (mul m n)
| 0 m n := by refl
| (nat.succ l) m n := begin simp [mul, mul_add, mul_assoc l] end
/- 1.3. Prove the same lemmas as in 1.2, but using the `induction` tactic instead. Try to reuse as
much of the above proof as possible. -/
example (m n : ℕ) : mul m n = mul n m :=
begin
induction m,
{ simp [mul, mul_zero] },
{ simp [mul, mul_succ, *], ac_refl }
end
example : ∀l m n : ℕ, mul (mul l m) n = mul l (mul m n) :=
begin
intros l m n,
induction l,
{ refl },
{ simp [mul, mul_add, *] }
end
/- 1.4. Prove the symmetric variant of `mul_add` using `rw`. To apply commutativity at a specific
position instantiate the rule (e.g. `mul_comm n`). -/
lemma add_mul (m n l : ℕ) : mul n (add l m) = add (mul n l) (mul n m) :=
by rw [mul_comm, mul_add, mul_comm n, mul_comm n]
end my_nat
/- Question 2: Lists -/
def reverse {α : Type} : list α → list α
| [] := []
| (x :: xs) := reverse xs ++ [x]
/- Another pesky `sorry`. -/
lemma reverse_reverse {α : Type} (xs : list α) : reverse (reverse xs) = xs := sorry
/- We define a new accumulator-based version of `reverse`. The first argument serves as the
accumulator. This definition is *tail-recursive*, meaning that compilers and interpreters can easily
optimize the recursion away, resulting in more efficient code. -/
def areverse {α : Type} : list α → list α → list α
| ys [] := ys
| ys (x :: xs) := areverse (x :: ys) xs
/- 2.1. Our intention is that `areverse [] xs` should be equal to `reverse xs`. But if we start an
induction, we quickly see that the induction hypothesis is not strong enough. Start by proving the
following generalization (using pattern matching or the `induction` tactic): -/
lemma areverse_eq_reverse_append {α : Type} : ∀ys xs : list α, areverse ys xs = reverse xs ++ ys
| ys [] := by refl
| ys (x :: xs) := by simp [reverse, areverse, areverse_eq_reverse_append _ xs]
/- 2.2. Derive the desired equation. -/
lemma areverse_eq_reverse {α : Type} (xs : list α) : areverse [] xs = reverse xs :=
by simp [areverse_eq_reverse_append]
/- 2.3. Prove the following property. Hint: A one-line inductionless proof is possible. -/
lemma areverse_areverse {α : Type} (xs : list α) : areverse [] (areverse [] xs) = xs :=
by simp [areverse_eq_reverse, reverse_reverse]