{-# OPTIONS --termination-depth=2 #-}

module Project4 where

-- In this final project, we'll explore induction a bit more. As
-- usual, you may need to formulate and prove your own lemmas.
--
-- The following imports require version 0.3 of the Topics in Logic
-- Library, found in the file library-v0.3.zip.

open import Nat
open import Ordering
open import Logic
open import Equality
open import List

-- ----------------------------------------------------------------------
-- * Sums

-- 1. Write a function to compute the sum of a list of numbers.
sum : List ℕ -> ℕ
sum = {!!}

module sum-test where

  -- Your definition of 'sum' should pass the following tests.
  -- You can also add your own tests if you want.
  test1 : sum nil == 0
  test1 = {!refl!}

  test2 : sum (1 :: 2 :: 3 :: nil) == 6
  test2 = {!refl!}

-- 2. A lemma about sums.
lemma-sum-++ : ∀ ns ms -> sum (ns ++ ms) == sum ns + sum ms
lemma-sum-++ = {!!}

-- 3. Another lemma about sums.
lemma-sum-reverse : ∀ ns -> sum ns == sum (reverse ns)
lemma-sum-reverse = {!!}

-- ----------------------------------------------------------------------
-- * Some proofs by induction

-- 4. Define a function that computes the list of the first n positive
-- integers.
first-numbers : (n : ℕ) -> List ℕ
first-numbers = {!!}

module first-numbers-test where

  -- Your definition of 'first-numbers' should pass the following tests.
  -- You can also add your own tests if you want.
  test1 : first-numbers 0 == nil
  test1 = {!refl!}

  test2 : first-numbers 5 == 1 :: 2 :: 3 :: 4 :: 5 :: nil
  test2 = {!refl!}

-- The usual formula for the sum of the first n numbers is
-- 1 + 2 + ... + n = ((n + 1) * n) / 2.  We don't want to bother
-- defining division, so we'll instead prove that
-- 2 * (1 + 2 + ... + n) = (n + 1) * n

-- 5. Prove that a formula about the sum of the first n numbers.
summation-formula : ∀ n -> 2 * sum (first-numbers n) == (n + 1) * n
summation-formula = {!!}

-- ----------------------------------------------------------------------
-- * Induction principle

-- Usually in Agda, we use the Curry-Howard isomorphism, and to prove
-- a theorem by induction is the same as defining a recursive
-- function. Agda's termination checker ensures that we cannot write
-- functions that are cyclically defined, such as f n = f n. It does
-- this by checking that the arguments of each recursive call are
-- "smaller" than the arguments of the function doing the recursive
-- call. However, sometimes the termination checker gets confused and
-- fails.

-- In mathematics, induction is usually formulated as a logical
-- formula, called an "induction principle". For example, the
-- induction principle for the natural numbers states that if P is any
-- property of numbers such that
--
-- (a)  P(0) holds, and
--
-- (b)  for all n ∈ ℕ, P(n) implies P(n+1),
--
-- then for all n ∈ ℕ, P(n) holds.
--
-- The statement (a) is called the "base case", the statement (b) is
-- called the "induction step", and in the induction step, the
-- assumption P(n) is called the "induction hypothesis".
--
-- In Agda, the induction principle can be expressed as follows:
--
-- ∀ (P : ℕ -> Set) -> P zero -> (∀ n -> P n -> P (succ n)) -> (∀ n -> P n)

-- 6. Prove the induction principle. You will have to prove it
-- recursively.
induction : ∀ (P : ℕ -> Set) -> P zero -> (∀ n -> P n -> P (succ n)) -> (∀ n -> P n)
induction = {!!}

-- 7. Example: The following lemma was one of the first ones we proved
-- in class about the natural numbers. We now prove the lemma again,
-- but this time we do not use recursion. We only use the induction
-- principle defined above. Fill in the missing pieces. Remember: do
-- not call the function lemma-add-m-zero-new recursively.
lemma-add-m-zero-new : ∀ (m : ℕ) -> m == m + zero
lemma-add-m-zero-new m = induction P base step m
  where
    -- The property that we are proving by induction.
    P : ℕ -> Set
    P m = (m == m + zero)

    -- The base case.
    base : P zero
    base = {!!}

    -- The induction step.
    step : ∀ m -> P m -> P (succ m)
    step m indhyp = {!!}

-- 8. Example: Here is another lemma we proved about addition. Prove
-- it without recursion, using only the induction principle. Fill in
-- the missing pieces.
--
-- Note: When proving something by induction, we must think carefully
-- about the following questions: (1) what variable are we doing the
-- induction on? (2) What exactly is the property we are proving by
-- induction?  For example, if the induction is on m, are we proving
-- the property "succ (m + n) == m + (succ n)" by induction on m, for
-- some *fixed* n? Or are we proving the property "∀ n -> succ (m + n)
-- == m + (succ n)" by induction on m, so that the induction
-- hypothesis assumes it is true for all n?
-- 
-- Sometimes it is necessary to do the latter, but not in this
-- example. Here, it is sufficient to consider a fixed n.
lemma-add-succ-new : ∀ (m n : ℕ) -> succ (m + n) == m + (succ n)
lemma-add-succ-new m n = induction P base step m
  where
    P : ℕ -> Set
    P m = succ (m + n) == m + (succ n)

    base : P zero
    base = {!!}

    step : ∀ m -> P m -> P (succ m)
    step m indhyp = {!!}
    
-- 9. Now prove the commutativity of addition, using only the
-- induction principle, without using recursion. I recommend you
-- follow a similar outline as 7. and 8. above. Do not use any lemmas
-- from the module Nat, either. Only use the lemmas proved above.
lemma-add-commutative-new : ∀ (n : ℕ) -> ∀ (m : ℕ) -> n + m == m + n
lemma-add-commutative-new = {!!}

-- Interestingly, because the property P in the induction principle is
-- actually a function from ℕ -> Set, we can not only prove theorems
-- by induction; we can also use induction to define elements of
-- sets. I.e., if P 0, P 1, P 2, ... is a family of sets, we can use
-- induction to define a function f such that f n ∈ P n. In
-- particular, if P is a constant function, so that P 0, P 1, P 2,
-- etc., are all the same set A, then we can use the induction
-- principle to define a function f : ℕ -> A. The is what is normally
-- called "recursion". So once again, we find that in Agda, induction
-- and recursion are essentially the same thing.
--
-- Here is an example. We use the induction principle to define a new
-- version of addition:
add-new : ℕ -> ℕ -> ℕ
add-new n m = induction P base step n
  where
    -- We define P as the constant function that returns the same set
    -- ℕ, no matter what n is.
    P : ℕ -> Set
    P n = ℕ

    -- Since P zero = ℕ, the base case is asking for an element of ℕ.
    -- In other words, it is asking what 0 + m is.
    base : P zero
    base = m

    -- Since P n = ℕ and P (succ n) = ℕ, the induction step is really
    -- asking us to define a function from ℕ -> ℕ. Specifically, given
    -- n, and assuming we know what n + m is (the induction
    -- hypothesis), it is asking what (succ n) + m is. Naturally, it
    -- is just one more than n + m.
    step : ∀ n -> P n -> P (succ n)
    step n indhyp = succ indhyp

module add-new-test where

  -- Let's check that the new addition function works!
  test1 : add-new 2 3 == 5
  test1 = {!refl!}

-- 10. Now use the same trick to define multiplication. Do not use
-- recursion, or any functions defined in the module Nat. Only use the
-- induction principle, and the function add-new defined above.
mult-new : ℕ -> ℕ -> ℕ
mult-new n m = induction P base step n
  where
    P : ℕ -> Set
    P n = {!!}

    base : P zero
    base = {!!}

    step : ∀ n -> P n -> P (succ n)
    step n indhyp = {!!}

module mult-new-test where

  -- Your definition of "mult-new" should pass the following tests.
  -- You can also add your own tests if you want.
  test1 : mult-new 0 3 == 0
  test1 = {!refl!}

  test2 : mult-new 2 0 == 0
  test2 = {!refl!}

  test3 : mult-new 2 3 == 6
  test3 = {!refl!}

-- ----------------------------------------------------------------------
-- * Strong induction

-- Sometimes, when we need to prove something by induction, it is not
-- sufficient in the induction step to go from n to n+1. Sometimes it
-- is necessary to assume as the induction hypothesis that the desired
-- property holds for *all* numbers less than n. This is called the
-- "strong induction principle" for the natural numbers. It can be
-- stated as follows: If P is any property of numbers such that
--
-- (a)  for all n ∈ ℕ, if P(k) holds for all k < n, then P(n) holds,
--
-- then for all n ∈ ℕ, P(n) holds.
--
-- The statement (a) is called the induction step, and the assumption
-- "P(k) holds for all k < n" is called the induction hypothesis.
--
-- Note that strong induction does not need a base case. In the
-- induction step for n=0, the assumption that P(k) holds for all
-- k < n is simply vacuously true, since there are no k < n in
-- that case.
--
-- In Agda, the strong induction principle can be expressed as follows:
--
-- ∀ (P : ℕ -> Set) -> (∀ n -> (∀ k -> k < n -> P k) -> P n) -> (∀ n -> P n)

-- 11. Prove the strong induction principle. Hint: you may have
-- trouble proving the conclusion (∀ n -> P n) directly. Instead,
-- prove something stronger, namely, the statement (∀ n k -> k < n -> P k).
-- It can be proved by induction on n, and it implies (∀ n -> P n).
--
-- To avoid misunderstandings: in your proof of the strong induction
-- principle, you are welcome to use recursion. You do not need to
-- prove it using the (weak) induction principle, although it is
-- possible to do so.

strong-induction : ∀ (P : ℕ -> Set) -> (∀ n -> (∀ k -> k < n -> P k) -> P n) -> (∀ n -> P n)
strong-induction = {!!}