module Decidable where

import Logic
import Nat
import Equality
import Bool

open Nat

data Even : ℕ → Set where
  even-base : Even zero
  even-step : ∀ {n : ℕ} → Even n → Even (succ (succ n))

-- Decidability

-- Definition: a proposition A is "decidable" in case ¬A ∨ A is true.

module Attempt1 where

  open Logic

  Decidable : Set -> Set
  Decidable A = ¬ A ∨ A

  -- What are the elements of Decidable A?
  -- They are exactly the same as the elements of ¬ A ∨ A.
  -- I.e.: there are two kinds:
  -- left x  -- where x is a proof of ¬ A
 -- right y -- where y is a proof of A

  -- Compare this with the elements of Maybe A:
  -- Nothing   -- when A isn't provable
  -- Just y    -- where y is a proof of A

  is-even? : (n : ℕ) -> Decidable (Even n)
  is-even? zero = right even-base
  is-even? (succ zero) = left (λ ())
  is-even? (succ (succ n)) with is-even? n
  is-even? (succ (succ n)) | left x = left (λ { (even-step hyp) → x hyp})
  is-even? (succ (succ n)) | right x = right (even-step x)

  -- left : ¬ A -> ¬ A ∨ A
  -- right : A -> ¬ A ∨ A

  -- left : A -> A ∨ B
  -- right : B -> A ∨ B

module Attempt2 where

  open Logic

  data Decidable (A : Set) : Set where
    yes : A -> Decidable A
    no : ¬ A -> Decidable A

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

open Attempt2

-- A list of A is a finite sequence of elements of A.

module List-Attempt1 where

  data List (A : Set) : Set where
    nil : List A
    cons : A -> List A -> List A

  -- Example: the list [1, 2, 3] is a list of natural numbers.
  my-list : List ℕ
  my-list = cons 1 (cons 2 (cons 3 nil))

module List-Attempt2 where

  data List (A : Set) : Set where
    nil : List A
    _::_ : A -> List A -> List A

  infixr 4 _::_

  -- Example: the list [1, 2, 3] is a list of natural numbers.
  my-list : List ℕ
  my-list = 1 :: 2 :: 3 :: nil

  -- We often use x : A and xs : List A

open List-Attempt2

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

-- Add all of the numbers in a list.
sum : List ℕ -> ℕ
sum nil = 0
sum (x :: ns) = x + sum ns

-- Add an element to the right of a list.
_>::_ : ∀ {A} -> List A -> A -> List A
nil >:: x = x :: nil
(y :: xs) >:: x = y :: (xs >:: x)

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

open Equality

lemma-length-of->:: : ∀ {A} -> (xs : List A) -> (x : A) -> length (xs >:: x) == succ (length xs)
lemma-length-of->:: nil x = refl
lemma-length-of->:: (y :: xs) x = context succ (lemma-length-of->:: xs x)

-- A theorem about lists.
theorem-length-of-reverse : ∀ {A} (xs : List A) -> length xs == length (reverse xs)
theorem-length-of-reverse nil = refl
theorem-length-of-reverse (x :: xs) =
   equational succ (length xs)
           by context succ (theorem-length-of-reverse xs)
       equals succ (length (reverse xs))
           by symm (lemma-length-of->:: (reverse xs) x)
       equals length (reverse xs >:: x)

open Bool
open Logic

-- Equality of natural numbers is decidable
nat-eq? : ∀ (x y : ℕ) -> Decidable (x == y)
nat-eq? zero zero = yes refl
nat-eq? zero (succ y) = no (λ ())
nat-eq? (succ x) zero = no (λ ())
nat-eq? (succ x) (succ y) with nat-eq? x y
nat-eq? (succ x) (succ y) | yes h = yes (context succ h)
nat-eq? (succ x) (succ y) | no h = no (λ { refl → h refl })

bool-of-decidable : ∀ {A} -> Decidable A -> Bool
bool-of-decidable (yes x) = true
bool-of-decidable (no x) = false

module list-equal1 where

  -- Check if two lists are equal.
  list-equal : ∀ {A} -> (∀ (x y : A) -> Decidable (x == y)) -> List A -> List A -> Bool
  list-equal eq? nil nil = true
  list-equal eq? nil (y :: ys) = false
  list-equal eq? (x :: xs) nil = false
  list-equal {A} eq? (x :: xs) (y :: ys) = equals? x y and list-equal eq? xs ys
    where
      equals? : A -> A -> Bool
      equals? x y with eq? x y
      equals? x y | yes h = true
      equals? x y | no h = false

module list-equal2 where

  -- Check if two lists are equal.
  list-equal? : ∀ {A} -> (∀ (x y : A) -> Decidable (x == y)) -> (xs ys : List A) -> Decidable (xs == ys)
  list-equal? eq? nil nil = yes refl
  list-equal? eq? nil (y :: ys) = no (λ ())
  list-equal? eq? (x :: xs) nil = no (λ ())
  list-equal? {A} eq? (x :: xs) (y :: ys) with eq? x y | list-equal? eq? xs ys
  list-equal? {A} eq? (x :: xs) (y :: ys) | yes hyp1 | yes hyp2 = yes (cong _::_ hyp1 hyp2)
  list-equal? {A} eq? (x :: xs) (y :: ys) | yes hyp1 | no hyp2 = no (λ { refl → hyp2 refl})
  list-equal? {A} eq? (x :: xs) (y :: ys) | no hyp1 | hyp2 = no (λ { refl → hyp1 refl})

module Example1 where

  open list-equal2

  my-list-list : List (List ℕ)
  my-list-list = (3 :: 2 :: 1 :: nil) :: (6 :: 5 :: 4 :: nil) :: nil

  my-list-list2 : List (List ℕ)
  my-list-list2 = (3 :: 2 :: nil) :: (1 :: 6 :: nil) :: (5 :: 4 :: nil) :: nil

  x : {!!}
  x = {!(list-equal? (list-equal? nat-eq?)) my-list-list my-list-list!}

  -- It would be nice if we were able to "overload" an equality
  -- operator, so that it works on any set with decidable equality.

  -- _==?_ : (x y : ℕ) -> Decidable (x == y)
  -- _==?_ : (xs ys : List ℕ -> Decidable (xs == ys)
  -- _==?_ : (xss yss : List (List ℕ) -> Decidable (xss == yss)

  -- It would be great if we could have decidable equality on all set A, like this:
  -- _==?_ : ∀ {A} -> (x y : A) -> Decidable (x == y)

  -- But we can't have this, because it cannot work on *all*
  -- sets. There are many sets on which equality is not decidable!

  -- Maybe this?
  -- _==?_ : ∀ {A} -> ((x y : A) -> Decidable (x == y)) -> (x y : A) -> Decidable (x == y)