module Homework4 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
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 = {!!}

-- 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 = {!!}

-- 5. Prove that "++" interacts with ":>" as expected.
lemma-++-:> : ∀ {A} (xs ys : List A) (y : A) -> xs ++ (y :: ys) == (xs :> y) ++ ys
lemma-++-:> = {!!}

-- ----------------------------------------------------------------------
-- * 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 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 = {!!}

-- ----------------------------------------------------------------------
-- * 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.
thm-reverse'-length : ∀ {A : Set} -> (xs : List A) -> length xs == length (reverse' xs)
thm-reverse'-length = {!!}

-- 10. Prove that reverse' is the same as reverse. You will probably
-- need a lemma about reverse-aux.
thm-reverse'-is-reverse : ∀ {A : Set} -> (xs : List A) -> reverse' xs == reverse xs
thm-reverse'-is-reverse = {!!}

-- ----------------------------------------------------------------------
-- * 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 = {!!}
  
  -- 12. Prove that not all elements of list1 are even.
  test-not-list1 : ¬ (List-∀ Even list1)
  test-not-list1 = {!!}

-- 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 = {!!}

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

-- ----------------------------------------------------------------------
-- * 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?

module Test-SortedNat where

  open Example-lists

  -- 16. Your SortedNat property should have the following properties.
  sorted-list1 : SortedNat list1
  sorted-list1 = {!!}

  not-sorted-list2 : ¬ (SortedNat list2)
  not-sorted-list2 = {!!}

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

-- 17. Prove that SortedNat is decidable
sortDecide : ∀ (xs : List ℕ) -> Decidable (SortedNat xs)
sortDecide xs = {!!}

-- ----------------------------------------------------------------------
-- 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 = {!!}

-- 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 = {!!}

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 : {!!}
tactic-even-list = {!!}

-- 22. Write a tactic for proving that not all elements of a list are
-- even.
tactic-not-even-list : {!!}
tactic-not-even-list = {!!}

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 <>!}