module Homework4-answers where

open import Nat
open import Logic
open import Equality
open import Ordering
open import EvenOdd
open import Decidable

-- ----------------------------------------------------------------------
-- * Lists

-- We start by defining the list datatype and some functions.
data List (A : Set) : Set where
  nil : List A
  _::_ : A -> List A -> List A

infixr 6 _::_

-- Calculate the length of a list.
length : {A : Set} -> List A -> ℕ
length nil = 0
length (x :: xs) = succ (length xs)

-- Append an element to the end of the list.
_:>_ : {A : Set} -> List A -> A -> List A
nil :> y = y :: nil
(x :: xs) :> y = x :: (xs :> y)

-- Reverse a list.
reverse : {A : Set} -> List A -> List A
reverse nil = nil
reverse (x :: xs) = reverse xs :> x

-- ----------------------------------------------------------------------
-- * The append function

-- 1. Define an "append" function that concatenates two lists. 
_++_ : {A : Set} -> List A -> List A -> List A
nil ++ ys = ys
(x :: xs) ++ ys = x :: (xs ++ ys)

module Example-lists where

  -- Some example lists. We put these in a module so that we can use
  -- them only when we need them.

  list1 = 1 :: 2 :: 3 :: nil
  list2 =  9 :: 8 :: 7 :: nil
  list3 = 1 :: 2 :: 3 :: 9 :: 8 :: 7 :: nil
  list4 = 4 :: 2 :: nil

module Test-append where

  open Example-lists

  -- 2. Your append function should pass the following test.
  test-append : list1 ++ list2 == list3
  test-append = refl

-- 3. Prove that appending a list to an empty list gives us the same list.
lemma-append-nil : ∀ {A : Set} -> (xs : List A) -> xs ++ nil == xs
lemma-append-nil nil = refl
lemma-append-nil (x :: xs) = context (\xs -> x :: xs)  (lemma-append-nil xs)

-- 4. Prove that append is associative.
lemma-append-assoc : ∀ {A : Set} -> (xs ys zs : List A) -> (xs ++ ys) ++ zs == xs ++ (ys ++ zs)
lemma-append-assoc nil ys zs = refl
lemma-append-assoc (x :: xs) ys zs = context (\xs -> x :: xs) (lemma-append-assoc xs ys zs)

-- 5. Prove that "++" interacts with ":>" as expected.
lemma-++-:> : ∀ {A} (xs ys : List A) (y : A) -> xs ++ (y :: ys) == (xs :> y) ++ ys
lemma-++-:> nil ys y = refl
lemma-++-:> (x :: xs) ys y = context (λ xs → x :: xs) (lemma-++-:> xs ys y)

-- ----------------------------------------------------------------------
-- * The map function

-- 6. Define a map function. This function should satisfy the
-- following property:
--
-- map f [x, y, z] = [f x, f y, f z].
--
map : {A B : Set} -> (A -> B) -> List A -> List B
map f nil = nil
map f (x :: xs) = f x :: map f xs

module Test-map where

  open Example-lists

  -- 7. Your map function should pass this test.
  test-map : map (\x -> x + 1) list3 == 2 :: 3 :: 4 :: 10 :: 9 :: 8 :: nil
  test-map = refl

-- 8. Prove that map distributes over append.
lemma-map-append : ∀ {A B : Set} -> (f : A -> B) -> (xs ys : List A) -> map f (xs ++ ys) == map f xs ++ map f ys
lemma-map-append f nil ys = refl
lemma-map-append f (x :: xs) ys = context (\xs -> f x :: xs) (lemma-map-append f xs ys)

-- ----------------------------------------------------------------------
-- * More efficient reversing of lists.

-- The "reverse" function defined above is computationally
-- inefficient. The problem is that appending one element to a list of
-- length n requires O(n) operations, and the "reverse" function does
-- this n times, resulting in a runtime of O(n²).

-- The following is a more efficient way to define list reverse. 
reverse-aux :  {A : Set} -> List A -> List A -> List A
reverse-aux nil ys = ys
reverse-aux (x :: xs) ys = reverse-aux xs (x :: ys)

reverse' : {A : Set} -> List A -> List A
reverse' {A} xs = reverse-aux {A} xs nil

-- Stop and think about why reverse' works. You can run a few tests
-- youself to get a better intuition of what reverse-aux does.

-- 9. Prove that reverse' preserves length. You will probably need a
-- lemma about reverse-aux.

lemma-reverse-aux-length : ∀ {A : Set} -> (xs ys : List A) -> length (reverse-aux xs ys) == length xs + length ys
lemma-reverse-aux-length nil ys = refl
lemma-reverse-aux-length (x :: xs) ys =
  equational length (reverse-aux xs (x :: ys))
    by lemma-reverse-aux-length xs (x :: ys)
  equals length xs + succ (length ys)
   by symm (lemma-add-succ (length xs) (length ys))
  equals succ (length xs + length ys)

thm-reverse'-length : ∀ {A : Set} -> (xs : List A) -> length xs == length (reverse' xs)
thm-reverse'-length xs =
  equational length xs
    by lemma-add-m-zero (length xs)
   equals length xs + 0
    by symm (lemma-reverse-aux-length xs nil)
   equals length (reverse' xs)

-- 10. Prove that reverse' is the same as reverse. You will probably
-- need a lemma about reverse-aux.

lemma-reverse-aux : ∀ {A : Set} -> (xs ys : List A) -> reverse-aux xs ys == reverse xs ++ ys
lemma-reverse-aux nil ys = refl
lemma-reverse-aux (x :: xs) ys =
  equational reverse-aux (x :: xs) ys
          by definition   -- "definition" is a synonym for "refl", defined in Equality.agda
      equals reverse-aux xs (x :: ys)
          by lemma-reverse-aux xs (x :: ys)
      equals reverse xs ++ (x :: ys)
          by lemma-++-:> (reverse xs) ys x
      equals (reverse xs :> x) ++ ys
          by definition
      equals reverse (x :: xs) ++ ys

thm-reverse'-is-reverse : ∀ {A : Set} -> (xs : List A) -> reverse' xs == reverse xs
thm-reverse'-is-reverse xs =
  equational reverse' xs
          by definition
      equals reverse-aux xs nil
          by lemma-reverse-aux xs nil
      equals reverse xs ++ nil
          by lemma-append-nil (reverse xs)
      equals reverse xs

-- ----------------------------------------------------------------------
-- * Decidable properties for lists

-- Decidability of evenness (from class).
is-even? : (n : ℕ) -> Decidable (Even n)
is-even? zero = yes even-base
is-even? (succ zero) = no (λ ())
is-even? (succ (succ n)) with is-even? n
is-even? (succ (succ n)) | yes x = yes (even-step _ x)
is-even? (succ (succ n)) | no x = no (λ { (even-step _ hyp) → x hyp})

-- The following defines a quantifier List-∀.
-- If xs : List A is a list and P : A -> Set is a property then
--
-- List-∀ P xs
--
-- means that P is true for all elements of xs.
data List-∀ {A : Set} : (A -> Set) -> List A -> Set where
  base-nil : ∀ P -> List-∀ P nil
  step-cons : ∀ P x xs -> P x -> List-∀ P xs -> List-∀ P (x :: xs)

module Test-List-∀ where

  open Example-lists

  -- 11. Prove that all elements of list4 are even.
  test-list4 : List-∀ Even list4
  test-list4 = step-cons Even 4 (2 :: nil) (even-step 2 (even-step zero even-base))
                    (step-cons Even 2 nil (even-step zero even-base) (base-nil Even))
  
  -- 12. Prove that not all elements of list1 are even.
  test-not-list1 : ¬ (List-∀ Even list1)
  test-not-list1 (step-cons .Even .1 .(2 :: 3 :: nil) () hyp)

-- 13. Prove that List-∀ P xs is decidable if P is decidable.
elemDecide : ∀ {A : Set} -> (P : A -> Set) -> (∀ x -> Decidable (P x)) -> (∀ xs -> Decidable (List-∀ P xs))
elemDecide P decP nil = yes (base-nil P)
elemDecide P decP (x :: xs) with decP x | elemDecide P decP xs
elemDecide P decP (x :: xs) | yes Px | yes Pxs = yes (step-cons P x xs Px Pxs)
elemDecide P decP (x :: xs) | yes Px | no nPxs = no λ { (step-cons .P .x .xs Px' Pxs) → nPxs Pxs}
elemDecide P decP (x :: xs) | no nPx | hyp2 = no (λ { (step-cons .P .x .xs Px Pxs) → nPx Px})

-- 14. Prove that the property "all elements of the list are even" is
-- decidable.
even-list : (xs : List ℕ) -> Decidable (List-∀ Even xs)
even-list xs = elemDecide Even is-even? xs

-- ----------------------------------------------------------------------
-- * Sorting

-- 15. Define a predicate to express when a list of natural number is sorted.
-- e.g. [a, b, c, d] is sorted iff a ≤ b ≤ c ≤ d. 
data SortedNat : List ℕ -> Set where
  -- You need to provide the constructors here. Hint: when is an empty
  -- list sorted? When is a list of length 1 sorted? When is a list of
  -- length ≥ 2 sorted?
  sorted-nil : SortedNat nil
  sorted-cons-1 : (x : ℕ) -> SortedNat (x :: nil)
  sorted-cons-2 : (x y : ℕ) -> (xs : List ℕ) -> SortedNat (y :: xs) -> x ≤ y -> SortedNat (x :: y :: xs)

module Test-SortedNat where

  open Example-lists

  -- 16. Your SortedNat property should have the following properties.
  sorted-list1 : SortedNat list1
  sorted-list1 = sorted-cons-2 1 2 (3 :: nil)
                   (sorted-cons-2 2 3 nil (sorted-cons-1 3)
                    (s≤s 1 2 (s≤s zero 1 (z≤n 1))))
                   (s≤s zero 1 (z≤n 1))

  not-sorted-list2 : ¬ (SortedNat list2)
  not-sorted-list2 = λ { (sorted-cons-2 .9 .8 .(7 :: nil) x (s≤s .8 .7 (s≤s .7 .6 (s≤s .6 .5 (s≤s .5 .4 (s≤s .4 .3 (s≤s .3 .2 (s≤s .2 .1 (s≤s .1 .0 ())))))))))}

lemma-order : ∀ (x y : ℕ) -> x ≤ y -> y < x -> False
lemma-order .(succ n) .(succ m) (s≤s n m h1) (less-succ h2) = lemma-order n m h1 h2

-- Decision function for ≤.
leq? : (n m : ℕ) -> Decidable (n ≤ m)
leq? zero m = yes (z≤n m)
leq? (succ n) zero = no (λ ())
leq? (succ n) (succ m) with leq? n m
leq? (succ n) (succ m) | yes x = yes (s≤s n m x)
leq? (succ n) (succ m) | no x = no (λ { (s≤s n m hyp) → x hyp})

-- 17. Prove that SortedNat is decidable
sortDecide : ∀ (xs : List ℕ) -> Decidable (SortedNat xs)
sortDecide nil = yes sorted-nil
sortDecide (x :: nil) = yes (sorted-cons-1 x)
sortDecide (x :: y :: xs) with leq? x y | sortDecide (y :: xs)
sortDecide (x :: y :: xs) | yes h1 | yes h2 = yes (sorted-cons-2 x y xs h2 h1)
sortDecide (x :: y :: xs) | yes h1 | no h2 = no λ { (sorted-cons-2 x y xs h3 h4) → h2 h3}
sortDecide (x :: y :: xs) | no h1 | h2 = no (λ { (sorted-cons-2 x y xs h3 h4) → h1 h4})

-- ----------------------------------------------------------------------
-- Tactics from Decidability

-- From any decidable property, we can create a tactic to
-- automatically prove (or disprove) the property. This is analogous
-- to the tactics we constructed using the Maybe type. But when a
-- property is decidable, we have a two-sided decision procedure, so
-- we can get a tactic for proving A and a tactic for proving ¬ A.

-- The following functions are analogous to isJust from Tactics.agda.
isYes : ∀ {A} -> Decidable A -> Set
isYes (yes x) = True
isYes (no x) = False

isNo : ∀ {A} -> Decidable A -> Set
isNo (yes x) = False
isNo (no x) = True

fromYes : ∀ {A} -> (x : Decidable A) -> isYes x -> A
fromYes (yes x) <> = x

fromNo : ∀ {A} -> (x : Decidable A) -> isNo x -> ¬ A
fromNo (no x) <> = x

-- 18. Write a tactic for proving that a list of numbers is sorted.
tactic-sorted : (xs : List ℕ) -> isYes (sortDecide xs) -> SortedNat xs
tactic-sorted xs x = fromYes (sortDecide xs) x

-- 19. Write a tactic for proving that a list of numbers is not sorted.
tactic-not-sorted : (xs : List ℕ) -> isNo (sortDecide xs) -> ¬ (SortedNat xs)
tactic-not-sorted xs x = fromNo (sortDecide xs) x

module Test-Tactic-Sorted where

  open Example-lists

  -- 20. Your tactics should be able to prove the following
  -- properties, i.e., that list1 is sorted and that list2 is not
  -- sorted.  Note that the proofs are far shorter than in module
  -- Test-SortedNat above.
  sorted-list1 : SortedNat list1
  sorted-list1 = tactic-sorted list1 <>

  not-sorted-list2 : ¬ (SortedNat list2)
  not-sorted-list2 = tactic-not-sorted list2 <>

-- 21. Write a tactic for proving that all elements of a list are even.
tactic-even-list : (xs : List ℕ) -> isYes (elemDecide Even is-even? xs) -> List-∀ Even xs
tactic-even-list xs x = fromYes (elemDecide Even is-even? xs) x

-- 22. Write a tactic for proving that not all elements of a list are
-- even.
tactic-not-even-list : (xs : List ℕ) -> isNo (elemDecide Even is-even? xs) -> ¬ (List-∀ Even xs)
tactic-not-even-list xs x = fromNo (elemDecide Even is-even? xs) x

module Test-Tactic-Even-List where

  open Example-lists

  -- 23. Your tactics should be able to prove that list4 is a list of
  -- even numbers and that list1 is not a list of even numbers. Note
  -- that the proofs are far shorter than in modeul Test-List-∀ above.
  test-list4 : List-∀ Even list4
  test-list4 = tactic-even-list list4 <>

  test-not-list1 : ¬ (List-∀ Even list1)
  test-not-list1 = tactic-not-even-list list1 <>