import .lovelib

noncomputable theory

local attribute [instance, priority 0] classical.prop_decidable


/- # LoVe Resit Exam

## Proof Guidelines

We expect detailed, rigorous, mathematical proofs, but we do not ask you to
write Lean proofs. You are welcome to use standard mathematical notation or Lean
structured commands (e.g., `assume`, `have`, `show`, `calc`). You can even use
tactical proofs (e.g., `intro`, `apply`), but then please indicate some of the
intermediate goals, so that we can follow the chain of reasoning.

Major proof steps, including applications of induction and invocation of the
induction hypothesis, must be stated explicitly. For each case of a proof by
induction, you must list the inductive hypotheses assumed (if any) and the goal
to be proved. Unless specified otherwise, minor proof steps corresponding to
`refl`, `simp`, or `linarith` need not be justified if you think they are
obvious, but you should say which key lemmas they depend on.

You should be explicit whenever you use a function definition or an introduction
rule for an inductive predicate, especially for functions and predicates that
are specific to an exam question.

## In Case of Ambiguities or Errors in an Exam Question

The lecturers cannot answer questions during the exam. We strongly recommend
that you work things out by yourselves, stating explicitly any ambiguity or
error and explaining how you interpret or repair the question. The more explicit
you are, the easier it will be for the lecturers to give you points. -/


set_option pp.beta true
set_option pp.generalized_field_notation false

namespace LoVe


/- ## Question 1 (10 points): Term inhabitation

The following questions ask you to discuss whether a type is inhabited.

1a (6 points). Complete the following Lean definitions by supplying arbitrary
terms of the expected type, thereby showing that the types are inhabited. -/

constants α β γ : Type

def weidenbach : α → β → β :=
--sol _
λa b, b
--los

def sturm : (α → α → γ) → β → α → γ :=
--sol sorry
λg b a, g a a
--los

def waldmann : (α → γ → β) → (α → β) → α → β :=
--sol sorry
λg f a, f a
--los

def mueller : (γ → γ) → (β → γ) → (α → β) → α → γ :=
--sol sorry
λh g f a, g (f a)
--los

/- 1b (4 points). Explain briefly why the following definitions cannot be
completed. You can for example refer to the typing rules of the simply typed
calculus in your justification. -/

def perfect_sturm : (α → β → γ) → α → α → γ := sorry

def angry_mueller : (γ → γ) → (β → β) → (α → β) → α → γ := sorry


/- ## Question 2 (14 points): Connectives and quantifiers

The following two questions are about basic mastery of logic. As an exception
to the proof guidelines given at the beginning of the exam, please provide
highly detailed proofs, including steps we would normally regard as obvious.

2a (6 points). Give a detailed proof of the following lemma about conjunction
and disjunction. Make sure to emphasize and clearly label every step
corresponding to the introduction or elimination of a connective. -/

lemma about_conjunction_and_disjunction {p q r : Prop} :
  (p ∨ q → r) → (p ∧ q → r) :=
--sol
begin
  intros h hpq,
  apply h,
  exact or.intro_left _ (and.elim_left hpq)
end

/- Assume `p ∨ q → r` and `p ∧ q`. From `p ∧ q`, we derive `p`
(`∧`-elimination). From `p`, we derive `p ∨ q` (`∨`-introduction). Hence, from
the assumption `p ∨ q → r`, we obtain `r`, as desired. -/
--los

/- 2b (8 points). Consider the following proposition:

  ∀p q, p ∨ q → p

Is this true? If so, prove it. If not, prove its negation.

In either case, give a detailed proof, emphasizing and clearly labeling every
step corresponding to the introduction or elimination of a connective or
quantifier. -/

--sol
lemma given_prop_is_false : ¬ (∀p q, p ∨ q → p) :=
begin
  intro contra,
  have h₀ : false ∨ true → false :=
    contra false true,
  have h₁ : false ∨ true :=
    or.intro_right _ true.intro,
  exact h₀ h₁
end

/- The proposition is false, so we prove its negation. Recall that `¬ P` means
`P → false`, so we prove `(∀ p q, p ∨ q → p) → false`. Assume `∀ p q, p ∨ q →
p`. From this, we derive the instance `false ∨ true → false` (`∀`-elimination).
We have `true` since this is the trivially true proposition, so we also have
`false ∨ true` (`∨`-introduction). Hence, from `false ∨ true → false`, we obtain
`false`, as desired. -/
--los


/- ## Question 3 (14 points): Transitive closure

The following questions are about specifying and reasoning about inductive
predicates representing the transitive closure of a relation.

3a (6 points). The transitive closure `r^+` of a binary relation `r` over a set
`A` can be defined as the smallest relation satisfying these two rules:

    (base) for all `a, b ∈ A`, if `(a, b) ∈ r`, then `(a, b) ∈ r^+`;
    (step) for all `a, b, c ∈ A`, if `(a, b) ∈ r` and `(b, c) ∈ r^+`, then `(a, c) ∈ r^+`.

Complete the following Lean definition of the transitive closure, in which
relations are represented by binary predicates. Your definition should follow
the structure of the above mathematical definition. -/

inductive tc {α : Type} (r : α → α → Prop) : α → α → Prop
--sol
| base (a b : α)   : r a b → tc a b
| step (a b c : α) : r a b → tc b c → tc a c
--los

/- 3b (8 points). The transitive closure can also be defined like this: -/

inductive tc_alt {α : Type} (r : α → α → Prop) : α → α → Prop
| base (a b : α) : r a b → tc_alt a b
| trans (a b c : α) : tc_alt a b → tc_alt b c → tc_alt a c

/- Prove that for any relation `r`, its closure `tc r` is contained in
`tc_alt r`: -/

lemma tc_tc_alt {α : Type} {r : α → α → Prop} {a b} :
  tc r a b → tc_alt r a b :=
--sol
begin
  intro h,
  induction h,
  case base : a b hab {
    exact tc_alt.base a b hab },
  case step : a b c hab hbc ih {
    exact tc_alt.trans a b c (tc_alt.base a b hab) ih }
end

/- Assume `tc r a b`. We prove `tc_alt r a b` by induction on the derivation of
`tc r a b`.

(base) If `tc r a b` was derived by the `base` rule, we have `r a b`. By
`tc_alt.base`, we conclude `tc_alt r a b`.

(step) If `tc r a b` was derived by the `step` rule, we have `r a x` and
`tc r x b` for some `x`. The induction hypothesis is `tc_alt r x b`. From
`r a x`, we derive `tc_alt r a x` by `tc_alt.base`. From this and the induction
hypothesis, we conclude `tc_alt r a b` by `tc_alt.step`. -/
--los


/- ## Question 4 (18 points): Logical foundations and mathematics

The following questions concern Lean's logical foundations and its applications
to mathematics.

4a (5 points). What are the types of the following Lean expressions?

    ℕ
    option (list ℕ)
    option
    (0 : nat)
    Prop
-/

--sol
#check (ℕ : Type)
#check (option (list ℕ) : Type)
#check (option : Type → Type)
#check (0 : nat)
#check (Prop : Type)

-- 1 point per correct answer
--los

/- 4b (7 points). Consider the equivalence relation `neg_rel` that relates
`x : ℤ` with `x` itself and with `- x`. -/

inductive neg_rel : ℤ → ℤ → Prop
| pos (x y : ℤ) : x = y → neg_rel x y
| neg (x y : ℤ) : x = - y → neg_rel x y

/- You may assume the following lemma about negation: -/

lemma int.neg_neg (x : ℤ) :
  - - x = x :=
--sol
int.neg_neg x
--los

/- Prove that `neg_rel` is reflexive and symmetric. -/

lemma neg_rel.refl (x : ℤ) :
  neg_rel x x :=
--sol
neg_rel.pos x x (by refl)

-- 1 point for using `neg_rel.pos`
-- 1 point for proving `x = x`
--los

lemma neg_rel.symm (x y : ℤ) :
  neg_rel x y → neg_rel y x
--sol
| (neg_rel.pos x y h) := neg_rel.pos y x h.symm
| (neg_rel.neg x y h) := neg_rel.neg y x (by simp [h])

-- 1 points for the correct case distinction
-- 1 points for applying `neg_rel.pos` and `neg_rel.neg`
-- 1 point for proving `y = x`
-- 2 points for proving `y = - x`
--los

/- 4c (4 points). Now, we will define our own copy of the natural numbers `ℕ`
as a quotient of the integers `ℤ`. First, observe that the `neg_rel` relation is
transitive (in addition to reflexive and symmetric): -/

lemma neg_rel.trans (x y z : ℤ) : neg_rel x y → neg_rel y z → neg_rel x z
--hide
| (neg_rel.pos x y h) (neg_rel.pos _ z h') := neg_rel.pos x z (by simp [h, h'])
| (neg_rel.pos x y h) (neg_rel.neg _ z h') := neg_rel.neg x z (by simp [h, h'])
| (neg_rel.neg x y h) (neg_rel.pos _ z h') := neg_rel.neg x z (by simp [h, h'])
| (neg_rel.neg x y h) (neg_rel.neg _ z h') := neg_rel.pos x z (by simp [h, h'])
--edih

/- We now have all the ingredients to define our new copy of the natural numbers
as a quotient: -/

@[instance] def new_nat.setoid : setoid ℤ :=
{ r     := neg_rel,
  iseqv := and.intro neg_rel.refl (and.intro neg_rel.symm neg_rel.trans) }

def new_nat : Type := quotient new_nat.setoid

/- Dana Hacker claims that `- x` and `x` correspond to the same element in the
type `new_nat`—i.e., `[[- x]] = [[x]]` for all `x : ℤ`. Do you agree? If so,
sketch a proof. Otherwise, give a counterexample. -/

--sol
lemma mk_neg_eq_mk (x : ℤ) :
⟦- x⟧ = ⟦x⟧ :=
quotient.sound (neg_rel.neg (- x) x (by refl))
-- 2 points for using quotient.sound
-- 1 point for `neg_rel.neg`
-- 1 point for proving `-x = -x`
--los

/- 4d (2 points). Consider the sequence 3, 3.1, 3.14, 3.141, 3.1415, 3.14159, …,
where elements contain more and more digits of π. According to the
representation of real numbers as Cauchy sequences, which number does the
sequence represent? -/

--sol
/- `π` -/
--los


/- ## Question 5 (18 points): Monads

The following questions concern monads.

5a (5 points). For an arbitrary type `σ`, we define the reader monad
`reader σ : Type → Type`. We may think of the values of `reader σ α` as programs
that return an `α` value but also have access to some input value of type `σ`.
This monad is similar to the state monad, but `reader` programs cannot change
the input `σ`. The type `reader σ α` is defined as follows: -/

def reader (σ α : Type) := σ → α

/- Complete the following Lean definitions of the monad operations `pure` and
`bind` for `reader`.

Hint: You can use the type inhabitation procedure to find the answers. -/

def reader.pure {σ α} : α → reader σ α :=
--sol
λa s, a

-- 2 points for correct answer.
--los

def reader.bind {σ α β} (ma : reader σ α) (f : α → reader σ β) : reader σ β :=
--sol
λs, f (ma s) s

-- 1 point for introducing `s : σ`
-- 1 point for getting `ma s : α`
-- 1 point for getting `f _ s : β`
--los

--hide
/- We need this instance to enable the >>= notation below. -/
instance {σ} : monad (reader σ) :=
{ pure := @reader.pure σ,
  bind := @reader.bind σ }
--edih

/- 5b (8 points). Assume that `ma >>= f` is notation for `reader.bind ma f`.
Prove that your `reader.pure` and `reader.bind` definitions satisfy the
following monad laws. Your proofs should be step-by-step calculational, with at
most one rewrite rule or definition expansion per step, so that we can clearly
see what happens. -/

lemma reader.pure_bind {σ α β} (a : α) (f : α → reader σ β) :
  (reader.pure a >>= f) = f a :=
--sol
calc  reader.pure a >>= f
    = (λs, a) >>= f :
  by refl /- definition of reader.pure -/
... = λs, f ((λs, a) s) s :
  by refl /- definition of reader.bind -/
... = λs, f a s :
  by refl /- beta reduction -/
... = f a :
  by refl /- eta reduction -/

-- 2 points for expanding definitions
-- 2 points for β/η reduction
--los

lemma reader.bind_pure {σ α} (ma : reader σ α) :
  (ma >>= reader.pure) = ma :=
--sol
calc  ma >>= reader.pure
    = λs, reader.pure (ma s) s :
  by refl /- definition of reader.bind -/
... = λs, (λa (s : σ), a) (ma s) s :
  by refl /- definition of reader.pure -/
... = λs, ma s :
  by refl /- beta reduction -/
... = ma :
  by refl /- eta reduction -/

-- 2 points for expanding definitions
-- 2 points for β/η reduction
--los

/- 5c (5 points). Prove the following equation for any lawful monad `m`.
Your proofs should be step-by-step calculational, with at most one rewrite rule
or definition expansion per step, so that we can clearly see what happens. -/

lemma pure_bind_pure {m} [monad m] [is_lawful_monad m] {α β} {a : α} {mb : m β} :
  pure a >>= (λ_, mb >>= pure) = mb :=
--sol
calc  pure a >>= (λ_, mb >>= pure)
    = (λ_, mb >>= pure) a :
  by rw pure_bind
... = mb >>= pure :
  by refl /- beta reduction -/
... = mb :
  by rw bind_pure

/- or:
calc  pure a >>= (λ_, mb >>= pure)
    = pure a >>= (λ_, mb) :
  by simp only [bind_pure]
... = mb :
  by rw pure_bind
-/

-- 2 points for correctly applying pure_bind
-- 2 points for correctly applying bind_pure
-- 1 point for joining the results up correctly
--los


/- ## Question 6 (16 points): Run-length encoding

In computer science, the run-length encoding is used to compress lists with many
repetitions. For example, "AABBB" is coded as "2A3B". The following Lean type
can be used to store run-length encoded lists: -/

inductive rle (α : Type)
| empty : rle
| ncons : ℕ → α → rle → rle

/- This type is similar to the standard `list` type, except that `ncons` also
includes a repetition count. The `empty` constructor represents a list with no
elements. The `ncons` constructor stores a repetition count, an element, and the
remainder of the list. Thus, we can encode "AABBB" as
`ncons 2 'A' (ncons 3 'B' empty)`. -/

/- 6a (4 points). Define a Lean function called `is_ncons` that tests whether
`rle` is of the form `ncons …`. -/

def is_ncons {α : Type} : rle α → bool
--sol
| rle.empty         := ff
| (rle.ncons _ _ _) := tt

-- 2 points for pattern matching on the `rle`.
-- 1 point for the empty list case.
-- 1 point for the `ncons` case.
--los

/- 6b (6 points). Define a Lean function `rle_length` that takes an `rle` and
returns the sum of all repetition counts in the list. For example, it would
return 5 for the encoding of "AABBB". -/

def rle_length {α : Type} : rle α → ℕ
--sol
| rle.empty         := 0
| (rle.ncons n _ t) := n + rle_length t

-- 1 point for pattern matching on the `rle`.
-- 1 point for the empty list case.
-- 2 points for adding `n` in an `ncons`.
-- 2 points for applying recursion.
--los

/- 6c (6 points). Consider the following `insert` function, which inserts an
element `a` at the front of an `rle`: -/

def insert {α : Type} (a : α) : rle α → rle α
| rle.empty         := rle.ncons 1 a rle.empty
| (rle.ncons n b t) :=
  if a = b then rle.ncons (n + 1) a t else rle.ncons 1 a (rle.ncons n b t)

/- Prove that `insert`ing an element into an `rle` cannot return `rle.empty`: -/

lemma insert_ne_empty {α : Type} (a : α) (l : rle α) :
  insert a l ≠ rle.empty :=
--sol
begin
  cases l,
  case empty {
    simp [insert] },
  case ncons : n b t {
    cases classical.em (a = b),
    { simp [insert, h] },
    { simp [insert, h] } }
end

/- The proof is by case distinction on `l`.

In the case that `l = empty`, the goal is `insert a empty ≠ empty`.
We have `insert a empty = ncons 1 a empty ≠ empty`.

In the case that `l = ncons n b t`, the goal is `insert a (ncons n b t) ≠ empty`.
If `a = b` then we have `insert a (ncons n b t) = ncons (n + 1) b t ≠ empty`.
If `a ≠ b` then we have `insert a (ncons n b t) = ncons 1 a (ncons n b t) ≠ empty`.
-/

-- 2 points for induction / cases on the `rle`.
-- 1 point for the `empty` case.
-- 2 points for case distinction on `a = b`.
-- 1 point for the `ncons` case.
--los

end LoVe
