import .lovelib


/- # LoVe Final 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 (16 points): Huffman trees

Consider the following type of weighted binary trees: -/

inductive tree (α : Type)
| leaf  : ℕ → α → tree
| inner : ℕ → tree → tree → tree

/- Each constructor corresponds to a kind of node. A `leaf` node stores a
numeric weight and a label of some type `α`, and an `inner` node stores a
numeric weight, a left subtree, and a right subtree.

1a (4 points). Define a polymorphic Lean function called `weight` that takes a
tree over some type variable `α` and that returns the weight component of the
root node of the tree: -/

def weight {α : Type} : tree α → ℕ
--sol
| (tree.leaf w _)    := w
| (tree.inner w _ _) := w
--los

/- 1b (4 points). Define a polymorphic Lean function called `unite` that takes
two trees `l, r : tree α` and that returns a new tree such that (1) its left
child is `l`; (2) its right child is `r`; and (3) its weight is the sum of the
weights of `l` and `r`. -/

--sol
def unite {α : Type} : tree α → tree α → tree α
| l r := tree.inner (weight l + weight r) l r
--los

/- 1c (8 points). Consider the following `insort` function, which inserts a tree
`u` in a list of trees that is sorted by increasing weight and which preserves
the sorting. (If the input list is not sorted, the result is not necessarily
sorted.) -/

def insort {α : Type} (u : tree α) : list (tree α) → list (tree α)
| []        := [u]
| (t :: ts) :=
  if weight u ≤ weight t then u :: t :: ts else t :: insort ts

/- Prove that `insort`ing a tree into a list cannot yield the empty list: -/

lemma insort_ne_nil {α : Type} (t : tree α) :
  ∀ts : list (tree α), insort t ts ≠ []
--sol
| []         := by simp [insort]
| (t' :: ts) :=
  begin
    clear insort_ne_nil,
    cases classical.em (weight t ≤ weight t'),
    { simp [insort, h] },
    { simp [insort, h] }
  end

/-
The proof is by case distinction (or induction) on `ts`.

Case `ts = []`. The goal is `insort t [] ≠ []`. We have `insort t ts = [t] ≠
[]`.

Case `ts = t' :: ts`. The goal is `insort t (t' :: ts) ≠ []`. We have `insort t
(t' :: ts) = if weight t ≤ weight t' then t :: t' :: ts else t' :: insort ts`.
If `weight t ≤ weight t'`, then we have `insort t ts = t :: t' :: ts ≠ []` by
distinctness of constructors. Otherwise, we have `insort t ts = t' :: insort ts
≠ []`. QED -/
--los


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

The following two subquestions are about basic mastery of logic. Please provide
highly detailed proofs.

2a (7 points). Give a detailed proof of the following __currying__ rule. Make
sure to emphasize and clearly label every step corresponding to the
introduction or elimination of a `∧` or `↔` connective. -/

lemma currying (p q r : Prop) :
  (p ∧ q → r) ↔ (p → q → r) :=
--sol
begin
  apply iff.intro,
  { intros hpqr hp hq,
    exact hpqr (and.intro hp hq) },
  { intros hpqr hpq,
    exact hpqr (and.elim_left hpq) (and.elim_right hpq) }
end

/- We will prove the two directions of the equivalence separately
(`↔`-introduction).

Assume `p ∧ q → r`. We must show `p → q → r`. I.e. assuming `p` and `q`,
show `r`. From `p` and `q`, we derive `p ∧ q` (`∧`-introduction). Hence, from
`p ∧ q → r`, we obtain `r`, as desired.

Assume `p → q → r`. We must show `p ∧ q → r`. I.e. assuming `p ∧ q`, show `r`.
From `p ∧ q`, we obtain `p` and `q` (`∧`-elimination). Hence, from the
assumption `p → q → r`, we obtain `r`, as desired. -/
--los

/- 2b (8 points). Prove the following lemma about quantifiers and implication.
Make sure to record and clearly label every step corresponding to the
introduction or elimination of a quantifier. -/

lemma about_quantifiers_and_implication {α : Type} {p q : α → Prop} :
  (∀x, p x → q x) → (∃x, p x) → (∃x, q x) :=
--sol
begin
  intros hpq hex,
  apply exists.elim hex,
  intros y hex,
  apply exists.intro y,
  apply hpq _ hex
end

/- Assuming `∀x, p x → q x` and `∃x, p x`, we must show `∃x, q x`.
From `∃x, p x`, obtain `y` such that `p y` (`∃`-elimination). From
`∀x, p x → q x`, derive the instance `p y → q y`. Hence, by `p y`, we get `q y`.
Thus, we obtain `∃x, q x` (`∃`-introduction). -/
--los


/- ## Question 3 (13 points): Symmetric and reflexive closures

The following subquestions are about specifying and reasoning about inductive
predicates representing closures of relations.

3a (6 points). The symmetric closure `r^s` of a binary relation `r` over a set
`A` is the smallest relation satisfying the following rules:

    (base) for all `a, b ∈ A`, if `(a, b) ∈ r`, then `(a, b) ∈ r^s`;
    (symm) for all `a, b ∈ A`, if `(a, b) ∈ r`, then `(b, a) ∈ r^s`.

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

inductive sc {α : Type} (r : α → α → Prop) : α → α → Prop
--sol
| base (x y : α) : r x y → sc x y
| symm (x y : α) : r x y → sc y x
--los

/- 3b (7 points). The reflexive closure `r^?` of a binary relation `r` is the
smallest reflexive relation that contains `r`. In Lean, we can define it as
follows: -/

inductive rc {α : Type} (r : α → α → Prop) : α → α → Prop
| base (x y : α) : r x y → rc x y
| refl (x : α)   : rc x x

/- Prove that if a relation `r` is already reflexive, then `rc r` is the same
relation: -/

lemma rc_of_reflexive {α : Type} (r : α → α → Prop)
    (hrefl : ∀x, r x x) (y z : α) :
  rc r y z ↔ r y z :=
--sol
begin
  apply iff.intro,
  { intro rcxy,
    cases' rcxy,
    { assumption },
    { exact hrefl x } },
  { intro hryz,
    exact rc.base y z hryz }
end

/- As usual with `↔`, it suffices to prove two directions (`↔`-introduction).

Assuming `rc r y z`, we must show `r y z`. Case distinction on `rc r y z`:
In the (base) case, we have `r y z`, as desired. In the (refl) case, we have
`y = z`. By `hrefl`, we have `r y y`, i.e., `r y z`, as desired.

Assuming `r y z`, we must show `rc r y z`. This follows immediately from
`rc.base`. QED -/
--los


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

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

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

    true
    ℤ
    list (list ℤ)
    list
    Type 255
-/

--sol
#check (true : Prop)
#check (ℤ : Type)
#check (list (list ℤ) : Type)
#check (list : Type → Type)
#check (Type 255 : Type 256)
--los

/- 4b (4 points). Recall that any integer `i` can be represented as a pair
`(p, n)` such that `i = p - n`, where `-` denotes integer (nontruncated)
subtraction. The pairs `(3, 0)`, `(4, 1)`, and `(5, 2)` all represent the
integer 3, but intuitively `(3, 0)` seems more appropriate. We will say that a
pair `(p, n)` is __canonical__ if `p` or `n` (or both) is 0: -/

inductive int.is_canonical : ℕ × ℕ → Prop
| nonpos (n : ℕ) : int.is_canonical (0, n)
| nonneg (p : ℕ) : int.is_canonical (p, 0)

/- We can then define the integers as consisting of the canonical pairs of
natural numbers: -/

def int : Type :=
{pn : ℕ × ℕ // int.is_canonical pn}

/- Which of the following values are equal? Which are different? -/

def i := subtype.mk (1, 0) (int.is_canonical.nonneg 1)
def j := subtype.mk (0, 0) (int.is_canonical.nonpos 0)
def k := subtype.mk (0, 0) (int.is_canonical.nonneg 0)
def m := subtype.mk (0, 1) (int.is_canonical.nonpos 1)

--sol
/- `j` and `k` are equal; the other values are different. -/
--los

/- 4c (6 points). Recall the definition of the Lean predicate `even`: -/

inductive even : ℕ → Prop
| zero    : even 0
| add_two : ∀k : ℕ, even k → even (k + 2)

/- Also assume the following lemma about `even`: -/

lemma even.add {m n : ℕ} (hm : even m) (hn : even n) :
  even (m + n) :=
sorry

/- Using `even`, we define the type `eveN` of even natural numbers as
follows: -/

def eveN : Type :=
{n : ℕ // even n}

/- Define zero and addition of even numbers. Recall that `subtype.mk x h`
constructs a subtype value `y` from a base value `x` and a proof `h`, whereas
`subtype.val y` and `subtype.property y` retrieve the `x` and `h` components
from the subtype value `y`. -/

def eveN.zero : eveN :=
--sol
subtype.mk 0 even.zero
--los

def eveN.add (m n : eveN) : eveN :=
--sol
subtype.mk (subtype.val m + subtype.val n)
  (even.add (subtype.property m) (subtype.property n))
--los

/- 4d (3 points). The following lemma states that any unary operation `f` over
`ℕ` has an input `n` at which it returns the minimal element in `f`'s image: -/

lemma exists_minimal_arg (f : ℕ → ℕ) :
  ∃n : ℕ, ∀i : ℕ, f n ≤ f i :=
sorry

/- For example, if `f` is `λn, (n - 100) + (100 - n)`, where `-` denotes
truncated subtraction (i.e., `0 - k = 0`), then the minimum is at `n = 100`.

Use `classical.some : (∃x : ?α, ?p x) → ?α` to define the following Lean
function, which returns some input `n` corresponding to the minimal element in
`f`'s image. -/

noncomputable def minimal_arg (f : ℕ → ℕ) : ℕ
--sol
:= classical.some (exists_minimal_arg f)
--los

/- 4e (2 points). Using the representation of p-adic numbers as left-infinite
streams of digits, compute the following addition in base p = 11:
`...6666666666 + 1`. -/

--sol
/- `...6666666667` -/
--los


/- ## Question 5 (16 points): Arithmetic expressions

Consider the following type of arithmetic expressions, where `num` represents an
integer constant, `var` represents a variable, and `add` represents addition: -/

inductive aexp : Type
| num : ℤ → aexp
| var : string → aexp
| add : aexp → aexp → aexp

/- An environment maps variable names to values: -/

def envir := string → ℤ

/- 5a (4 points). Complete the following Lean definition of an evaluation
function for arithmetic expressions. -/

def eval (env : envir) : aexp → ℤ
| (aexp.num i)     := i
| (aexp.var x)     := env x
--sol
| (aexp.add a₁ a₂) := eval a₁ + eval a₂
--los

/- 5b (4 points). Complete the following Lean definition of a big-step-style
semantics for arithmetic expressions. The predicate `big_step` (`⟹`) relates
an arithmetic expression, an environment, and the value to which it the
expression evaluates in the given environment: -/

inductive big_step : aexp × envir → ℤ → Prop
| num {i env} : big_step (aexp.num i, env) i
--sol
| var {x env} : big_step (aexp.var x, env) (env x)
--los
| add {a₁ a₂ i₁ i₂ env} :
  big_step (a₁, env) i₁ → big_step (a₂, env) i₂ →
  big_step (aexp.add a₁ a₂, env) (i₁ + i₂)

infix ` ⟹ ` : 110 := big_step

/- 5c (8 points). Prove that the big-step semantics is sound with respect to the
`eval` function: -/

lemma big_step_sound (env : envir) (a : aexp) (i : ℤ) :
  (a, env) ⟹ i → eval env a = i :=
--sol
begin
  intro hstep,
  induction' hstep,
  case num {
    apply refl },
  case var {
    apply refl },
  case add {
    simp [eval, ih_hstep, ih_hstep_1] }
end

/- Assuming `(a, env) ⟹ i`, we show `eval env a = i`.

The proof is by rule induction on `(a, env) ⟹ i`.

In the `num` case, we must show the goal for `a = aexp.num i`. Hence
`eval env a = eval env (aexp.num i) = i` by definition of `eval`.

In the `var` case, we must show the goal for `a = aexp.var x`. Hence
`eval env a = eval env (aexp.var x) = env x = i` by definition of `eval`.

In the `add` case, we must show the goal for `a = aexp.add a₁ a₂`, with
`(a₁, env) ⟹ i₁`, `(a₂, env) ⟹ i₂`, and `i = i₁ + i₂`. By the induction
hypotheses, `eval env a₁ = i₁` and `eval env a₂ = i₂`. Hence
`eval env a = eval env (aexp.add a₁ a₂) = eval env a₁ + eval env a₂ = i₁ + i₂`.
QED -/
--los


/- ## Question 6 (10 points): Metaprogramming

Consider the following tactics `split_hyp` and `split_once`. The main tactic,
`split_once`, looks for a hypothesis of the form `h : a ∨ b` in the context,
then applies the `cases` tactic to generate two subgoals, one with `h : a` and
one with `h : b`. -/

meta def split_hyp (h : expr) : tactic unit :=
do
  T ← tactic.infer_type h,
  match T with
  | `(_ ∨ _) :=
    do
      tactic.cases h,
      pure ()
  | _        := tactic.failed
  end

meta def split_once : tactic unit :=
do
  hs ← tactic.local_context,
  list.mfirst split_hyp hs

/- 6a (6 points). For each line of `split_hyp` and `split_once`, write a brief
comment explaining what it does. -/

--sol
  -- get the type `T` of the hypothesis `h`
  -- match on `T`
  -- if `T` is of the form `a ∨ b` for some `a` and `b`
    -- apply the `cases` tactic to `h`, generating two subgoals
    -- return the trivial unit value
  -- if `T` is not of the form `a ∨ b`, fail

  -- get all hypotheses
  -- try to apply `split_hyp` to each hypothesis in turn; stop if `split_hyp`
  -- succeeds on any of the hypotheses; fail if `split_hyp` succeeds on none of
  -- the hypotheses
--los

/- 6b (4 points). Consider the following `case_bash` tactic: -/

meta def case_bash : tactic unit :=
do
  tactic.repeat split_once,
  tactic.all_goals (tactic.try tactic.assumption),
  pure ()

/- Suppose we invoke `case_bash` on the following goal:

    n m : ℕ,
    h : n < m ∨ n = m ∨ n > m
    ⊢ n < m

What subgoal or subgoals does this produce? -/

--sol
/-
n m : ℕ,
h : n = m
⊢ n < m

n m : ℕ,
h : n > m
⊢ n < m
-/

example (n m : ℕ) (h : n < m ∨ n = m ∨ n > m) : n < m :=
begin
  case_bash,
  { sorry },
  { sorry }
end
--los

end LoVe
