import lovelib

namespace LoVe

-- 1. Functional programming (3+4+7 = 14pt)

/-
For this question, consider the type `btree` of binary trees where each node has at most one child:
-/
inductive btree : Type
| empty : btree
| node  : btree → btree → btree

/-
The height of a tree is the largest number of nodes along a path from the root node to a leaf.
This means an empty tree has height `0` and a tree containing only one node has height `1`.
-/
def height : btree → ℕ
| btree.empty := 0
| (btree.node l r) := 1 + max (height l) (height r)

-- (3pt) Complete the following definition of the function `btree.with_height`.
-- Given a natural number `n`, `btree.with_height n` should have height `n`.
-- You do not have to prove that your definition satisfies the specification.
def btree.with_height : ℕ → btree
| 0 := btree.empty
| (n+1) := btree.node btree.empty (btree.with_height n)
-- 1pt for recursion on `n`
-- 1pt for 0 case
-- 1pt for the successor case

-- (4pt) Define a predicate `is_balanced` on a tree.
-- A tree is balanced if it is empty, or for *each* node in the tree, its two subtrees have the same height.
-- You can use the `height` function.
--   is_balanced : btree → Prop
def is_balanced : btree → Prop
| btree.empty := true
| (btree.node l r) := is_balanced l ∧ is_balanced r ∧ height l = height r
-- Or:
inductive is_balanced' : btree → Prop
| empty : is_balanced' btree.empty
| node : ∀ l r, is_balanced' l → is_balanced' r → height l = height r → is_balanced' (btree.node l r)

-- 1pt for recursion on the tree
-- 1pt for the empty case
-- 1pt for checking the subtrees are balanced
-- 1pt for checking the heights are the same

-- (7pt)
/- The `graft` function takes two trees and attaches copies of the second tree to each leaf of the first tree. -/
def graft : btree → btree → btree
| btree.empty      u := u
| (btree.node l r) u := btree.node (graft l u) (graft r u)

-- Give a proof by induction of the following lemma, showing that the height of a grafted tree is the sum of the heights of the original tree.
-- For each case, clearly indicate the inductive hypotheses and the goal to be proved.
-- You can make use of the following two lemmas:
#check max_add_add_left -- ∀ (a b c : ℕ), max (a + b) (a + c) = a + max b c
#check max_add_add_right -- ∀ (a b c : ℕ), max (a + b) (c + b) = max a c + b

lemma height_graft : ∀ (t u : btree), height (graft t u) = height t + height u :=
begin
  intros t u,
  induction' t with l r,
  case empty { /- show height u = 0 + height u -/ simp [height, graft] },
  case node { /- height (graft l u) = height l + height u, height (graft r u) = height r + height u ⊢ height (node (graft l) (graft r)) = height (node (graft l) (graft r)) + height u -/
    simp [height, graft, ih_l, ih_r, max_add_add_left, max_add_add_right, add_assoc],
  }
end
-- 1pt induction on t
-- 1pt induction hypothesis in empty case
-- 1pt solve by refl / simp
-- 2pt goal of node case
-- 2pt solve by simp

-- 2. Inductive predicates (4 + 3 = 7pt)

-- (4pt) Define an inductive predicate `is_repeat` on two strings `xs` and `ys`,
-- stating that `ys` is the string `xs` concatenated with itself one or more times.
-- Examples of strings where this relation holds: `is_repeat "exam" "exam"`, `is_repeat "love" "lovelove"`, and `is_repeat "abab" "abababababab"`.
-- Examples of strings where this relation does not hold: `¬(is_repeat "abc" "")`, `¬(is_repeat "abab" "ab")`, `¬(is_repeat "aaa" "aaaa")`, `¬(is_repeat "abc" "dabcabcd")`.
-- Your definition should consider two cases: `ys` repeats `xs` one time and `ys` repeats `xs` more than one time
inductive is_repeat : list char → list char → Prop
| once : ∀ xs, is_repeat xs xs
| many : ∀ xs ys, is_repeat xs ys → is_repeat xs (xs ++ ys)
-- or:
inductive is_repeat' : list char → list char → Prop
| once : ∀ xs, is_repeat' xs xs
| many : ∀ xs ys, is_repeat' xs ys → is_repeat' xs (ys ++ xs)

-- 1pt for defining a `once` case and a `many` case
-- 1pt for completing the `once` case
-- 1pt for depending on `is_repeat xs ys`
-- 1pt for constructing a `is_repeat xs (xs ++ ys)` or `is_repeat xs (ys ++ xs)`

-- (3pt) Give a short proof of the proposition `is_repeat "a" "aaa"`.
lemma a_aaa : is_repeat "a".1 "aaa".1 :=
begin
  apply is_repeat.many,
  apply is_repeat.many,
  apply is_repeat.once,
end
-- 1pt: apply `is_repeat.many`
-- 1pt: ... the correct amount of times
-- 1pt: finish with `is_repeat.once`


-- 3. The IFFY language (6+9+6 = 21pt)
/-
The IFFY programming language is like the WHILE language, except its `if` statement doesn't quite work right. It has the following kinds of statements:
 * `skip` does nothing
 * `x := a` assigns the integer `a` to the variable `x`
 * `S₁ ; S₂` executes the statements of `S₁` followed by the statements of `S₂`
 * `iffy b then S` does nothing if `b` is false. If `b` is true, it nondeterministically chooses between executing `S` or doing nothing.

In Lean we can model the IFFY language's abstract syntax as follows:
-/
inductive stmt : Type
| skip : stmt
| assign : string → ℤ → stmt
| seq : stmt → stmt → stmt
| iffy : bool → stmt → stmt
open stmt

infix ` ;; `:100 := stmt.seq

-- (6pt) The big-step semantics of the IFFY language relates a program `S : stmt` and an input state `s : string → ℤ` to an output state `t : string → ℤ`.
-- Complete the following big-step semantics by giving the derivation rules for `iffy`:
-- [COPY FROM WHILE]

/-
       (S, s) => t
----------------------- if `b` is true (if-true-exec)
(iffy b then S, s) => t

----------------------- if `b` is true (if-true-skip)
(iffy b then S, s) => s

----------------------- if `b` is false (if-false)
(iffy b then S, s) => s

-- or:

       (S, s) => t
----------------------- if `b` is true (if-exec)
(iffy b then S, s) => t

----------------------- if `b` is true or false (if-skip)
(iffy b then S, s) => s

-/

-- 1pt for distinguishing "if `b` is true" and "if `b` is false"
-- 1pt for distinguishing between "if true + execute S" and "if true + do nothing"
-- 2pt for correct "execute S" semantics
-- 2pt for correct "do nothing" semantics

-- (9pt) Specify the same big-step semantics as an inductive predicate by completing the following Lean definition.

inductive big_step : (stmt × (string → ℤ)) → (string → ℤ) → Prop
| skip {s} : big_step (skip, s) s
-- snip
| assign {x a s} : big_step (assign x a, s) (λ y, if x = y then a else s y)
| seq {S₁ S₂ s t u} : big_step (S₁, s) t → big_step (S₂, t) u → big_step (S₁ ;; S₂, s) u

| if_true_exec {S s t} : big_step (S, s) t → big_step (iffy tt S, s) t
| if_true_skip {S s} : big_step (iffy tt S, s) s
| if_false {S s} : big_step (iffy ff S, s) s
-- or:
| if_exec {S s t} : big_step (S, s) t → big_step (iffy tt S, s) t
| if_skip {b S s} : big_step (iffy b S, s) s

-- 1pt for one constructor per rule
-- 1pt for correct quantificationa
-- 1pt for correct syntax
-- 1pt each for assign, seq
-- 2pt each for if-true, if-false

-- (6pt) Give a derivation tree in the big-step semantics for an execution of the program `P(b)` defined below,
-- such that the variable `x` gets assigned the value `1`.
-- Clearly indicate the name of each derivation rule.
def P : stmt :=
assign "x" 0 ;; iffy b (assign "x" 1)

/-
                                         ------------------------------------ assign
                                         ((assign "x" 1), s[x:=0]) => s[x:=1]
---------------------------- assign   ------------------------------------------- if-exec
(assign "x" 0, s) => s[x:=0]          (iffy b (assign "x" 1), s[x:=0]) => s[x:=1]
--------------------------------------------------------------------------------- seq
       (assign "x" 0 ;; iffy b (assign "x" 1), s) => s[x:=1]
-/
-- 1pt for ending up with state `s[x:=1]`
-- 2pt for assign x := 0, and seq
-- 2pt for if-exec
-- 1pt for pushing the states around correctly

-- 4. Logic (6+6+5 = 17pt)

-- (6pt) Give a detailed proof of the following lemma.
-- Make sure to emphasize and clearly label every introduction or elimination rule.
lemma about_exists_and_or {α : Type} {p q : α → Prop} :
  (∃ x, p x ∨ q x) → (∃ x, p x) ∨ (∃ x, q x) :=
λ h, exists.elim h (λ x hpq, or.elim hpq (λ hp, or.inl (exists.intro x hp)) (λ hq, or.inr (exists.intro x hq)))

-- 1pt: assume h : ∃ x, p x ∨ q x
-- 2pt: exists elimination on h giving x, hpq
-- 1pt: or elimination on hpq
-- 1pt: or introduction
-- 1pt: exists introduction

-- (6pt) Let `R : ℤ → ℤ → Prop` be a predicate on two integers,
variables {R : ℤ → ℤ → Prop}
-- that satisfies the following three introduction rules:
variables (R.refl : ∀ (a : ℤ), R a a) -- `R.refl : ∀ a, R a a`
variables (R.symm : ∀ {a b : ℤ}, R a b → R b a) -- `R.symm : R ?a ?b → R ?b ?a`
variables (R.trans : ∀ {a b c : ℤ}, R a b → R b c → R a c) -- `R.trans : R ?a ?b → R ?b ?c → R ?a ?c`
-- Give a detailed proof of the following theorem.
-- Clearly indicate when you use the rules `R.refl`, `R.symm` or `R.trans`:
theorem euclid : ∀ a b c : ℤ, R a b → R a c → R b c :=
λ a b c hab hac, R.trans (R.symm hab) hac
-- 1pt: introduce the assumptions
-- 2pt: use transitivity
-- 1pt: use symmetry
-- 2pt: type correctness

-- (5pt): One of the following two theorem statements is correct.
-- Indicate which is the correct theorem and give a detailed proof of that statement.
-- Make sure to emphasize and clearly label every introduction or elimination rule.

lemma or_of_and {p q : Prop} (h : p ∧ q) : p ∨ q := _

lemma and_of_or {p q : Prop} (h : p ∨ q) : p ∧ q := _

-- 2pt: `or_of_and` is true
-- 1pt: and elimination
-- 1pt: or introduction
-- 1pt: logically correct

-- 5. Monads (7 + 5 + 4 + 3 = 19pt)

-- (7pt) Complete the following recursive Lean definition taking a list of functions and a list of arguments.
-- It applies the first function to the first argument, the second function to the second argument, and so on, stopping when either list runs out.
-- For example, `list.pairwise [(λ x, x + 1), (λ x, x * 2)] [1, 3, 10] = [2, 6]`
def list.pairwise {α β : Type} : list (α → β) → list α → list β
| [] _ := []
| _ [] := []
| (f :: fs) (x :: xs) := f x :: list.pairwise fs xs

-- 2pt for recursion on both lists simultaneously
-- 2pt for nil cases
-- 1pt for `f x` in cons case
-- 1pt for `pairwise fs xs` in cons case
-- 1pt for type correctness

-- (5pt) Let `m` be a monad.
-- Recall that a monad `m` has two operations, `pure : ∀ {α}, α → m α` and `bind : ∀ {α β}, m α → (α → m β) → m β`; `bind mx f` is also written `mx >>= f`.
variables {m : Type → Type} [monad m]
-- Complete the following definition of the operation `ap mf mx` that monadically applies its first boxed argument to the second boxed argument,
-- putting the result in a box:
def ap {α β : Type} (mf : m (α → β)) (mx : m α) : m β :=
do f ← mf,
   x ← mx,
   pure (f x)
-- or: bind mf (λ f, bind mx (λ x, pure (f x)))

-- 1pt for syntax
-- 2pt for putting mf and mx on the left of bind / on the right of ←
-- 1pt for applying f to x
-- 1pt for type correctness (e.g. not forgetting pure)

-- (4pt) The operations `pure` and `bind` on lists are defined as follows:
--  * `pure x = [x]`
--  * `bind [] f = []`
--  * `bind (x :: xs) f = f x ++ bind xs f`
--
-- What are the values returned by the following two calls to `list.length`?
--  * `list.length (list.pairwise [(λ x, x + 1), (λ x, x - 1)] [10])`
--  * `list.length (ap [(λ x, x + 1), (λ x, x - 1)] [10])`
--
-- `list.pairwise [(λ x, x + 1) (λ x, x - 1)] [10] = [10 + 1] = [11]`; length = 1 (2pt)
-- `ap [(λ x, x + 1) (λ x, x - 1)] [10] = [(λ x, x + 1) (λ x, x - 1)] >>= λ f, [10] >>= λ x, [f x] = ([10] >>= λ x, [x + 1]) ++ ([10] >>= λ x, [x - 1]) = [11] ++ [9] = [11, 9]`; length = 2 (2pt)

-- (3pt) Does applying `ap` to two lists always give the same result as `list.pairwise` on those lists? Briefly explain your answer.
-- No (2pt): for example the lengths are different in the previous question (1pt).

-- 6. Mathematics in Lean (5+5+2 = 12pt)

-- (5pt) What are the types of the following expressions?
#check ℕ             -- : Type (1pt)
#check ((1 : ℕ) + 2) -- : ℕ (1pt)
#check (ℕ → ℕ) → ℤ -- : Type (1pt)
#check Type → Type -- : Type 1 (1pt)
#check Prop → Prop -- : Type (1pt)

-- (5pt) The type class `monoid` of monoid is defined as follows in Lean:
class monoid (α : Type) :=
(mul : α → α → α)
(one : α)
(mul_assoc : ∀ (a b c : α), mul (mul a b) c = mul a (mul b c))
(one_mul : ∀ (a : α), mul one a = a)
(mul_one : ∀ (a : α), mul a one = a)

-- The type of booleans can be viewed as a monoid,
-- with `tt : bool` as `one` and conjunction `&&` as `mul`.
-- Complete the following instantiation of `bool` as a monoid by providing a suitable definition of
-- the five fields of the monoid. For each of the three boolerties, state the boolerty to prove and
-- very briefly explain why it holds.
instance bool.monoid : monoid bool :=
{ mul := (&&),
  one := tt,
  mul_assoc := show ∀ a b c : bool, (a && b) && c = a && (b && c), from λ a b c, by simp,
  mul_one := show ∀ a : bool, a && tt = a, from λ a, by simp,
  one_mul := show ∀ a : bool, tt && a = a, from λ a, by simp }

-- (2pt) The mathlib linters reject the following proof. Briefly point out at least one improvement you would make.
lemma linty_mul_left_comm {α : Type} [field α]
  (x y z : α) (hx : x ≠ 0) (hy : y ≠ 0) (hz : z ≠ 0) :
  x * (y * z) = y * (x * z) :=
have hxy : x * y ≠ 0, from mul_ne_zero hx hy,
calc x * (y * z) = (x * y) * z : by rw mul_assoc
             ... = (y * x) * z : by rw mul_comm x y
             ... = y * (x * z) : by rw mul_assoc

-- Example answers:
--  * `field α` can become `comm_monoid` or `comm_semigroup`
--  * the `have hxy` is unnecessary
--  * the variables `hx`, `hy` or `hz` can be deleted

#eval 14 + 7 + 23 + 17 + 18 + 11

end LoVe
