{-
    Agda in a hurry
    ---------------

    Martín Hötzel Escardó
    5th October 2017, updated 10th November 2020 and 9th December 2021.

    An html rendering with syntax highlighting and internal links is available at
    https://www.cs.bham.ac.uk/~mhe/fp-learning-2017-2018/html/Agda-in-a-Hurry.html

    This is a brief introduction to Agda, originally written for
    (Haskell) functional programming students.

    Agda is a language similar to Haskell, but it includes dependent
    types, which have many uses, including writing specifications of
    functional programs.

    http://wiki.portal.chalmers.se/agda/pmwiki.php
    http://agda.readthedocs.io/en/latest/

    This tutorial doesn't cover the interactive construction of types
    and programs (and hence propositions and proofs).

    This file is also an introduction to dependent types.

    Organization:

      1. We first develop our own mini-library.

      2. We then discuss how to encode propositions as types in Agda.

      3. We then discuss list reversal, in particular the correctness
         of the "clever" algorithm that runs in linear, rather than
         quadratic, time.

      4. We conclude by giving a non-trivial example of the
         specification and proof of a non-trivial functional program
         with binary trees. This program is a direct translation of a
         Haskell program.

-}

{-

    What Agda calls sets is what we normally call types in programming:

-}

Type = Set

{-

    The type of booleans:

-}

data Bool : Type where
  False True : Bool

if_then_else_ : {A : Type} → Bool → A → A → A
if False then x else y = y
if True  then x else y = x

{-
    Curly braces "{" and "}" are for implicit arguments, that we don't
    mention explictly, provided Agda can infer them. If it cannot, we
    have to write them explicitly when we call the function, enclosed
    in curly braces.

    http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.ImplicitArguments

    There is a slightly more general version of if_then_else_, using
    dependent types, which says that if we have P False and P True,
    then we have P b for any given b : Bool:
-}

Bool-induction : {P : Bool → Type}

              → P False
              → P True
              --------------------
              → (b : Bool) → P b

Bool-induction x y False = x
Bool-induction x y True  = y


data Maybe (A : Type) : Type where
  Nothing : Maybe A
  Just    : A → Maybe A


Maybe-induction : {A : Type} {P : Maybe A → Type}

               → P Nothing
               → ((x : A) → P(Just x))
               ------------------------
               → (m : Maybe A) → P m

Maybe-induction p f Nothing  = p
Maybe-induction p f (Just x) = f x

{-
    This corresponds to Haskell's Either type constructor:
-}

data _+_ (A B : Type) : Type where
  inl : A → A + B
  inr : B → A + B


+-induction : {A B : Type} {P : A + B → Type}

            → ((x : A) → P(inl x))
            → ((y : B) → P(inr y))
            -----------------------
            → ((z : A + B) → P z)


+-induction f g (inl x) = f x
+-induction f g (inr y) = g y

{-
    Maybe A ≅ A + 𝟙, where 𝟙 is the unit type.
-}

data 𝟙 : Type where
  ₀ : 𝟙

{-
    The empty type has no constructors:
-}

data ∅ : Type where

{-
    The empty type has a function to any other type, defined by an empty
    set of equations. Its induction principle is a generalization of that.
-}

∅-induction : {A : ∅ → Type} → (e : ∅) → A e
∅-induction ()

{-
    A pattern () means that what is required is impossible, because
    the type under consideration is empty.
-}

∅-elim : {A : Type} → ∅ → A
∅-elim {A} = ∅-induction {λ _ → A}


data List (A : Type) : Type where
  []  : List A
  _∷_ : A → List A → List A


{-
    When we want to use an infix operator as a prefix function, we
    write underscores around it. So for example (_∷_ x) is equivalent
    to λ xs → x ∷ xs. However, we prefer to write (cons x) in this
    particular case, as (_∷_ x) occurs often in the following
    development, and we find (cons x) more readable:
-}

singleton : {A : Type} → A → List A
singleton x = x ∷ []


_++_ : {A : Type} → List A → List A → List A
[]       ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)


-- Induction over lists is a functional program too:

List-induction : {A : Type} {P : List A → Type}

              →  P []                                        -- base case
              → ((x : A) (xs : List A) → P xs → P(x ∷ xs))   -- induction step
              ----------------------------------------------
              → (xs : List A) → P xs

List-induction base step []       = base
List-induction base step (x ∷ xs) = step x xs (List-induction base step xs)

{-
    Just as if_then_else_ is a particular case of Bool-induction, the
    infamous function foldr is a particular case of List-induction,
    where the type family P is constant:
-}

foldr : {A B : Type} → (A → B → B) → B → List A → B
foldr {A} {B} f y = List-induction {A} {P} base step
  where
    P : List A → Type
    P _ = B

    base : B
    base = y

    step : (x : A) (xs : List A) → P xs → P(x ∷ xs)
    step x _ y = f x y

{-
    To convince ourselves that this really is the usual function
    foldr, we need to define the equality type (also known as the
    identity type), whose only constructor is refl (for reflexivity of
    equality):
-}

data _≡_ {A : Type} : A → A → Type where
  refl : (x : A) → x ≡ x


≡-induction : {A : Type} {P : {x y : A} → x ≡ y → Type}

            → ((x : A) → P(refl x))
            -------------------------------
            → (x y : A) (p : x ≡ y) → P p

≡-induction r x .x (refl .x) = r x


{-
    The following can be defined from ≡-induction, but pattern
    matching on refl probably gives clearer definitions.

    The dot in front of a variable in a pattern is to deal with
    non-linearity (multiple occurrences of the same variable) of the
    pattern. The first undotted variable is pattern matched, and the
    dotted one assumes the same value.
-}

trans : {A : Type} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
trans (refl x) (refl .x) = refl x

sym : {A : Type} {x y : A} → x ≡ y → y ≡ x
sym (refl x) = refl x

ap : {A B : Type} (f : A → B) {x y : A} → x ≡ y → f x ≡ f y
ap f (refl x) = refl (f x)

transport : {A : Type} (P : A → Type) {x y : A} → x ≡ y → P x → P y
transport P (refl x) p = p

{-
   We can now formulate and prove the claim that the above
   construction does give the usual function foldr on lists:
-}

foldr-base : {A B : Type} (f : A → B → B) (y : B)

          → foldr f y [] ≡ y

foldr-base f y = refl y


foldr-step : {A B : Type} (f : A → B → B) (y : B) (x : A) (xs : List A)

          → foldr f y (x ∷ xs) ≡ f x (foldr f y xs)

foldr-step f y x xs = refl _

{-
    In the above uses of refl in the right-hand side of an equation,
    Agda normalizes the two sides of the equation, and sees that they
    are the same, and accepts refl as a term with the required type.

    An underscore in the right-hand side of a definition represents a
    term that we don't bother to write because Agda can infer it. In
    the last example, the term can be either side of the equation we
    want to prove.

    But it has to be remarked that not all equations can be proved
    with refl. Here is an example, which needs to be done by induction
    on the list xs. But instead of using List-induction directly, we
    can have a proof by recursion on xs, like that of List-induction
    itself:
-}

++assoc : {A : Type} (xs ys zs : List A)

         → (xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs)

++assoc []       ys zs = refl (ys ++ zs)
++assoc (x ∷ xs) ys zs = conclusion
  where
    IH : xs ++ ys ++ zs ≡ xs ++ (ys ++ zs)
    IH = ++assoc xs ys zs

    conclusion' : x ∷ (xs ++ ys ++ zs) ≡ x ∷ (xs ++ (ys ++ zs))
    conclusion' = ap (x ∷_) IH

    conclusion : ((x ∷ xs) ++ ys) ++ zs ≡ (x ∷ xs) ++ (ys ++ zs)
    conclusion = conclusion'

{-
    Although the types of goal' and goal look different, they are the
    same in the sense that they simplify to the same type, applying
    the definition of _++_. In practice, we avoid conclusion' and
    define conclusion directly.
-}

{-
    In Haskell, it is possible to explicitly indicate the type of a
    subterm. In Agda we can achieve this with a user defined syntax
    extension. We use the unicode symbol "∶", which looks like the
    Agda reserved symbol ":".

    What the following says is that when we write "x ∶ A", what we
    actually mean is "id {A} x", where id is the identity function.
-}

id : {A : Type} → A → A
id {A} x = x

syntax id {A} x = x ∶ A

have : {A B : Type} → A → B → B
have _ y = y

{-
    Notice that we can also write x ∶ A ∶ B (which associates as
    (x ∶ A) ∶ B) when the types A and B are "definitionally equal",
    meaning that they are the same when we expand the definitions.

    We exploit this to shorten the above proof while adding more
    information that is not needed for the computer to the reader:
-}

++assoc' : {A : Type} (xs ys zs : List A)

         → (xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs)

++assoc' []       ys zs = refl (ys ++ zs)
                        ∶  ([] ++ ys) ++ zs ≡ [] ++ (ys ++ zs)

++assoc' (x ∷ xs) ys zs = (have(++assoc' xs ys zs ∶ (xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs)))
                          ap (x ∷_) (++assoc' xs ys zs)
                          ∶ x ∷ ((xs ++ ys) ++ zs) ≡ x ∷ (xs ++ (ys ++ zs))
                          ∶ ((x ∷ xs) ++ ys) ++ zs ≡ (x ∷ xs) ++ (ys ++ zs)

{-
    The computer can do away with this additional information via type
    inference, and so can we in principle, but not always in practice.
-}

++assoc'' : {A : Type} (xs ys zs : List A) → (xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs)
++assoc'' []       ys zs = refl _
++assoc'' (x ∷ xs) ys zs = ap (x ∷_) (++assoc'' xs ys zs)

{-

    We now show that xs ++ [] for any list xs, by induction on xs. We
    do this in a terse way, given the above explanations.

-}

[]-right-neutral : {X : Type} (xs : List X) → xs ++ [] ≡ xs
[]-right-neutral [] = refl []
[]-right-neutral (x ∷ xs) = ap (x ∷_) ([]-right-neutral xs)

{-

List reversal.

-}

rev : {A : Type} → List A → List A
rev []       = []
rev (x ∷ xs) = rev xs ++ (x ∷ [])

rev-++ : {A : Type} (xs ys : List A) → rev (xs ++ ys) ≡ rev ys ++ rev xs
rev-++ [] ys       = sym ([]-right-neutral (rev ys))
rev-++ (x ∷ xs) ys = conclusion
 where
  IH : rev (xs ++ ys) ≡ rev ys ++ rev xs
  IH = rev-++ xs ys

  a : rev (xs ++ ys) ++ (x ∷ []) ≡ (rev ys ++ rev xs) ++ (x ∷ [])
  a = ap (_++ (x ∷ [])) IH

  b : (rev ys ++ rev xs) ++ (x ∷ []) ≡ rev ys ++ (rev xs ++ (x ∷ []))
  b = ++assoc (rev ys) (rev xs) (x ∷ [])

  conclusion : rev (xs ++ ys) ++ (x ∷ []) ≡ rev ys ++ (rev xs ++ (x ∷ []))
  conclusion = trans a b

rev-involutive : {A : Type} (xs : List A) → rev (rev xs) ≡ xs
rev-involutive []       = refl (rev (rev []))
rev-involutive (x ∷ xs) = conclusion
 where
  IH : rev (rev xs) ≡ xs
  IH = rev-involutive xs

  a : rev (rev (x ∷ xs)) ≡ rev (rev xs ++ (x ∷ []))
  a = refl _

  b : rev (rev xs ++ (x ∷ [])) ≡ rev (x ∷ []) ++ rev (rev xs)
  b = rev-++ (rev xs) (x ∷ [])

  c : rev (x ∷ []) ++ rev (rev xs) ≡ rev (x ∷ []) ++ xs
  c = ap (rev (x ∷ []) ++_) IH

  conclusion : rev (rev (x ∷ xs)) ≡ (x ∷ xs)
  conclusion = trans a (trans b c)

{-

 The above reversal function is quadratic time. It is well known that
 it can be defined in linear time using rev-append. Let's prove this.

-}

rev-append : {A : Type} → List A → List A → List A
rev-append []       ys = ys
rev-append (x ∷ xs) ys = rev-append xs (x ∷ ys)

rev-linear : {A : Type} → List A → List A
rev-linear xs = rev-append xs []

rev-append-spec : {A : Type}
                  (xs ys : List A)
                → rev-append xs ys ≡ rev xs ++ ys
rev-append-spec []       ys = refl ys
rev-append-spec (x ∷ xs) ys = conclusion
 where
  IH : rev-append xs (x ∷ ys) ≡ rev xs ++ (x ∷ ys)
  IH = rev-append-spec xs (x ∷ ys)

  a : rev xs ++ ((x ∷ []) ++ ys) ≡ (rev xs ++ (x ∷ [])) ++ ys
  a = sym (++assoc (rev xs) (x ∷ []) ys)

  conclusion : rev-append (x ∷ xs) ys ≡ rev (x ∷ xs) ++ ys
  conclusion = trans IH a

rev-linear-correct : {A : Type}
                     (xs : List A)
                   → rev-linear xs ≡ rev xs
rev-linear-correct xs = trans (rev-append-spec xs []) ([]-right-neutral (rev xs))

{-
    We now define the usual map function on lists in the two usual ways.
-}

map' : {A B : Type} → (A → B) → List A → List B
map' f []       = []
map' f (x ∷ xs) = f x ∷ map' f xs

map'' : {A B : Type} → (A → B) → List A → List B
map'' f = foldr (λ x ys → f x ∷ ys) []

maps-agreement : {A B : Type}
                 (f : A → B)
                 (xs : List A)
               → map' f xs ≡ map'' f xs
maps-agreement f []       = refl []
maps-agreement f (x ∷ xs) = conclusion
 where
  IH : map' f xs ≡ map'' f xs
  IH = maps-agreement f xs

  conclusion : f x ∷ map' f xs ≡ f x ∷ map'' f xs
  conclusion = ap (f x ∷_) IH

{-
    Can choose below whether we want map = map' or map = map''.

    The proofs given below about them don't not need to be changed as
    the definition with foldr has the same definitional behaviour, as
    illustrated by the theorems foldr-base and foldr-step
    above.
-}

map : {A B : Type} → (A → B) → List A → List B
map = map'

{-

    Some properties of map

-}

map-id : {A : Type}
         (xs : List A)
        → map id xs ≡ xs
map-id []       = refl []
map-id (x ∷ xs) = ap (x ∷_) (map-id xs)

_∘_ : {A B C : Type} → (B → C) → (A → B) → (A → C)
g ∘ f = λ x → g (f x)


map-∘ : {A B C : Type}
        (g : B → C)
        (f : A → B)
        (xs : List A)
      → map (g ∘ f) xs ≡ map g (map f xs)
map-∘ g f []       = refl []
map-∘ g f (x ∷ xs) = conclusion
 where
  IH : map (g ∘ f) xs ≡ map g (map f xs)
  IH = map-∘ g f xs

  conclusion : g (f x) ∷ map (g ∘ f) xs ≡ g (f x) ∷ map g (map f xs)
  conclusion = ap (g (f x) ∷_) IH

{-
    We now define binary trees and a function to pick subtrees
    specified by a list of directions left and right.
-}


data BT (A : Type) : Type where
  Empty : BT A
  Fork  : A → BT A → BT A → BT A


BT-induction : {A : Type} {P : BT A → Type}
             →  P Empty                                            -- base
             → ((x : A) (l r : BT A) → P l → P r → P(Fork x l r))  -- step
             -----------------------------------------------------
             → (t : BT A) → P t

BT-induction {A} {P} base step Empty        = base ∶ P Empty

BT-induction {A} {P} base step (Fork x l r) = step x l r (BT-induction base step l ∶ P l)
                                                         (BT-induction base step r ∶ P r)
                                            ∶ P(Fork x l r)


data Direction : Type where
  L R : Direction


Address : Type
Address = List Direction


subtree : {A : Type} → Address → BT A → Maybe(BT A)
subtree []       t            = Just t
subtree (_ ∷ _)  Empty        = Nothing
subtree (L ∷ ds) (Fork _ l _) = subtree ds l
subtree (R ∷ ds) (Fork _ _ r) = subtree ds r


isValid : {A : Type} → Address → BT A → Bool
isValid []       _            = True
isValid (_ ∷ _)  Empty        = False
isValid (L ∷ ds) (Fork _ l _) = isValid ds l
isValid (R ∷ ds) (Fork _ _ r) = isValid ds r

{-
    If an addrees is invalid, then the function subtree gives Nothing:
-}

false-premise : {P : Type} → True ≡ False → P
false-premise ()

invalid-gives-Nothing : {A : Type} (ds : Address) (t : BT A)

                     → isValid ds t ≡ False → subtree ds t ≡ Nothing

invalid-gives-Nothing {A} [] Empty p
  = false-premise(p ∶ isValid {A} [] Empty ≡ False)

invalid-gives-Nothing (d ∷ ds) Empty (refl False)
  = refl Nothing
  ∶  Nothing ≡ Nothing
  ∶  subtree (d ∷ ds) Empty ≡ Nothing

invalid-gives-Nothing [] (Fork x l r) p
  = false-premise(p ∶ isValid [] (Fork x l r) ≡ False)

invalid-gives-Nothing (L ∷ ds) (Fork x l r) p
  = invalid-gives-Nothing ds l (p ∶ isValid (L ∷ ds) (Fork x l r) ≡ False)
  ∶ subtree ds l ≡ Nothing
  ∶ subtree (L ∷ ds) (Fork x l r) ≡ Nothing

invalid-gives-Nothing (R ∷ ds) (Fork x l r) p
  = invalid-gives-Nothing ds r (p ∶ isValid (R ∷ ds) (Fork x l r) ≡ False)
  ∶ subtree ds r ≡ Nothing
  ∶ subtree (R ∷ ds) (Fork x l r) ≡ Nothing

{-

    Or, in concise form:

-}

invalid-gives-Nothing' : {A : Type} (ds : Address) (t : BT A)

                     → isValid ds t ≡ False → subtree ds t ≡ Nothing

invalid-gives-Nothing' []       Empty        ()
invalid-gives-Nothing' (d ∷ ds) Empty        (refl False) = refl Nothing
invalid-gives-Nothing' []       (Fork x l r) ()
invalid-gives-Nothing' (L ∷ ds) (Fork x l r) p            = invalid-gives-Nothing' ds l p
invalid-gives-Nothing' (R ∷ ds) (Fork x l r) p            = invalid-gives-Nothing' ds r p

{-
    We now show that if an address ds is valid for a tree t, then
    there is a tree t' with subtree ds t = Just t'.

    "There is ... with ..." can be expressed with Σ types, which we
    now explain and define.

    Given a type A and a type family B : A → Type, the type Σ {A} B
    has as elements the pairs (x , y) with x : A and y : B x.

    The brackets in pairs are not necessary, so that we can write just
    "x , y". This is because we define comma to be a constructor,
    written as a binary operator in infix notation:
-}

record Σ (A : Type) (B : A → Type) : Type where
  constructor
    _,_
  field
    x : A
    y : B x


{-
   We define special syntax to be able to write expressions involving
   Σ in a more friendly way, so that, for example,

       Σ x ∶ A , B x

   is the type of pairs (x,y) with x : A and y : B x.

   Notice that, for some reason, the syntax declaration is backwards
   (what is defined in on the right rather than the left:
-}

syntax Σ A (λ x → y) = Σ x ꞉ A , y

pr₁ : {A : Type} {B : A → Type} → (Σ x ꞉ A , B x) → A
pr₁ (x , y) = x

pr₂ : {A : Type} {B : A → Type} → ((x , y) : Σ x ꞉ A , B x) → B x
pr₂ (x , y) = y

{-
    Induction on Σ is uncurry:
-}

Σ-induction : {A : Type} {B : A → Type} {P : Σ A B → Type}

            → ((x : A) (y : B x) → P(x , y))
            ---------------------------------
            → (z : Σ A B) → P z

Σ-induction f (x , y) = f x y

{-
    We could have defined the projections by induction:
-}

pr₁' : {A : Type} {B : A → Type} → Σ A B → A
pr₁' {A} {B} = Σ-induction {A} {B} {λ _ → A} (λ x y → x)


pr₂' : {A : Type} {B : A → Type} → (z : Σ A B) → B(pr₁ z)
pr₂' {A} {B} = Σ-induction {A} {B} {λ z → B (pr₁ z)} (λ x y → y)

{-
    A particular case of Σ {A} C is when the family C : A → Type is constant,
    that is, we have C x = B for some type B, in which case we get the
    cartesian product A × B.
-}

_×_ : Type → Type → Type
A × B = Σ x ꞉ A , B

{-
    We can now formulate and prove that if an address is valid, then
    it gives some subtree.
-}

false-premise' : {P : Type} → False ≡ True → P
false-premise' ()


valid-gives-just : {A : Type} (ds : Address) (t : BT A)

                → isValid ds t ≡ True
                → Σ t' ꞉ BT A , (subtree ds t ≡ Just t')

valid-gives-just {A} [] Empty p
  = (have(p ∶ isValid {A} [] Empty ≡ True))
    (Empty , (refl _ ∶ subtree [] Empty ≡ Just Empty))

valid-gives-just {A} (d ∷ ds) Empty p
  = false-premise'(p ∶ isValid {A} (d ∷ ds) Empty ≡ True)

valid-gives-just {A} [] (Fork x l r) p
  = Fork x l r , (refl _ ∶ subtree [] (Fork x l r) ≡ Just (Fork x l r))
  ∶ Σ t' ꞉ BT A , (subtree [] (Fork x l r) ≡ Just t')

valid-gives-just {A} (L ∷ ds) (Fork x l r) p
  = valid-gives-just ds l (p ∶ isValid (L ∷ ds) (Fork x l r) ≡ True
                             ∶ isValid ds l ≡ True)
  ∶ (Σ t' ꞉ BT A , (subtree (L ∷ ds) (Fork x l r) ≡ Just t'))
  ∶  Σ t' ꞉ BT A , (subtree ds l ≡ Just t')

valid-gives-just {A} (R ∷ ds) (Fork x l r) p
  = valid-gives-just ds r (p ∶ isValid (R ∷ ds) (Fork x l r) ≡ True
                             ∶ isValid ds r ≡ True)
  ∶ (Σ t' ꞉ BT A , (subtree (R ∷ ds) (Fork x l r) ≡ Just t'))
  ∶  Σ t' ꞉ BT A , (subtree ds r ≡ Just t')


{-
    Or, in concise form:
-}

valid-gives-Just' : {A : Type} (ds : Address) (t : BT A)

                 → isValid ds t ≡ True → Σ t' ꞉ BT A , (subtree ds t ≡ Just t')

valid-gives-Just' []       Empty        p = Empty , (refl _)
valid-gives-Just' (d ∷ ds) Empty       ()
valid-gives-Just' []       (Fork x l r) p = Fork x l r , (refl _)
valid-gives-Just' (L ∷ ds) (Fork x l r) p = valid-gives-Just' ds l p
valid-gives-Just' (R ∷ ds) (Fork x l r) p = valid-gives-Just' ds r p

{-
    We have been working with "propositions as types" and "proofs as
    (functional) programs", also known as the Curry--Howard
    interpretation of logic.

     A implies B                    A → B
     A and B                        A × B
     A or B                         A + B
     for all x : A, P(x)            (x : A) → P x
     there is x : A with P(x)       Σ x : A , P x
     false                          ∅
     not A                          A → ∅

    (https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence)

    We now construct the list of valid addresses for a given tree. The
    construction is short, but the proof that it does produce
    precisely the valid addresses is long and requires many lemmas,
    particularly in our self-imposed absence of a library.
-}


validAddresses : {A : Type} → BT A → List Address
validAddresses Empty        = singleton []
validAddresses (Fork _ l r) = (singleton [])
                           ++ (map (L ∷_) (validAddresses l))
                           ++ (map (R ∷_) (validAddresses r))

{-
    The remainder of this tutorial is devoted to showing the following:

        For any given address ds and tree t : BT A,

            isValid ds t ≡ True if and only if ds is in validAddresses t.

    This is formulated and proved in the function main-theorem below.


    We define when an element x : A is in a list xs : List A, written
    x ∈ xs, borrowing the membership symbol ∈ from set theory:
-}

data _∈_ {A : Type} : A → List A → Type where
  inHead : (x : A) (xs : List A) → x ∈ x ∷ xs
  inTail : (x y : A) (xs : List A) → y ∈ xs → y ∈ x ∷ xs

{-
    This is a so-called inductive definition of a predicate (the
    membership relation).

    (1) x ∈ x ∷ xs

    (2) y ∈ xs → y ∈ x ∷ xs

    We construct a proof of (1) with inHead, and a proof of (2) with
    inTail.

    The following proof is by induction on "x ∈ xs".
-}

mapIsIn : {A B : Type} (f : A → B) {x : A} {xs : List A}

        → x ∈ xs → f x ∈ map f xs

mapIsIn f (inHead x xs) = inHead (f x) (map f xs)
                        ∶ f x ∈ f x ∷ map f xs
                        ∶ f x ∈ map f (x ∷ xs)

mapIsIn f (inTail x y xs i) = (have(i ∶ y ∈ xs))
                              (have(mapIsIn f i ∶ f y ∈ map f xs))
                              inTail (f x) (f y) (map f xs) (mapIsIn f i)
                            ∶ f y ∈ f x ∷ map f xs
                            ∶ f y ∈ map f (x ∷ xs)

{-
    Or, in concise form:
-}

mapIsIn' : {A B : Type} (f : A → B) {x : A} {xs : List A}

        → x ∈ xs → f x ∈ map f xs

mapIsIn' f (inHead x xs) = inHead (f x) (map f xs)

mapIsIn' f (inTail x y xs i) = inTail (f x) (f y) (map f xs) (mapIsIn' f i)

{-
    Even more concise:
-}

mapIsIn'' : {A B : Type} (f : A → B) {x : A} {xs : List A}

        → x ∈ xs → f x ∈ map f xs

mapIsIn'' _ (inHead _ _) = inHead _ _

mapIsIn'' _ (inTail _ _ x_ i) = inTail _ _ _ (mapIsIn'' _ i)

{-
    Which means that we could have made all the "_" arguments into
    implicit arguments (greatly sacrificing clarity). Also, there is
    no guarantee that these implicit arguments will be inferrable in
    other contexts. In any case, it seems to be an art to decide which
    arguments should be left implicit with a good balance of
    conciseness and clarity.
-}


equal-heads : {A : Type} {x y : A} {xs ys : List A} → (x ∷ xs) ≡ (y ∷ ys) → x ≡ y
equal-heads {A} {x} {.x} {xs} {.xs} (refl .(x ∷ xs)) = refl x


equal-tails : {A : Type} {x y : A} {xs ys : List A} → (x ∷ xs) ≡ (y ∷ ys) → xs ≡ ys
equal-tails {A} {x} {.x} {xs} {.xs} (refl .(x ∷ xs)) = refl xs


isInjective : {A B : Type} → (A → B) → Type
isInjective f = {x y : _} → f x ≡ f y → x ≡ y


cons-injective : {A : Type} {x : A} → isInjective(x ∷_)
cons-injective {A} {x} = equal-tails {A} {x}


{-
    The following is by induction on xs. We introduce an auxiliary
    function g to do this induction, with the other parameters
    fixed. Because we need to pattern-match on the value of (map f xs)
    in the induction, we introduce an extra parameter for the value ys
    of (map f xs). Agda has a special keywork "with" for that purpose,
    but we don't discuss it in this brief introduction.
-}

mapIsIn-converse : {A B : Type} {f : A → B} {x : A} {xs : List A}

                  → isInjective f → f x ∈ map f xs → x ∈ xs

mapIsIn-converse {A} {B} {f} {x} {xs} inj = g xs (map f xs) (refl _)
  where
    g : (xs : List A) (ys : List B) → ys ≡ map f xs → f x ∈ ys → x ∈ xs
    g [] .(f x ∷ xs) () (inHead .(f x) xs)
    g [] .(x' ∷ xs) () (inTail x' .(f x) xs i)
    g (x' ∷ xs) .(f x ∷ ys) e (inHead .(f x) ys) = conclusion
      where
        a : f x ≡ f x'
        a = have(e ∶ f x ∷ ys ≡ map f (x' ∷ xs)
                   ∶ f x ∷ ys ≡ f x' ∷ map f xs)
            equal-heads e
        b : x ≡ x'
        b = inj a
        c : x ∈ x ∷ xs
        c = inHead x xs
        conclusion : x ∈ x' ∷ xs
        conclusion = transport (λ x' → x ∈ x' ∷ xs) b c
    g (x' ∷ xs) .(y ∷ ys) e (inTail y .(f x) ys i) = conclusion
      where
        et : ys ≡ map f xs
        et = have(e ∶ y ∷ ys ≡ map f (x' ∷ xs)
                    ∶ y ∷ ys ≡ f x' ∷ map f xs)
             equal-tails e
        IH : f x ∈ ys → x ∈ xs
        IH i = g xs ys et i
        conclusion : x ∈ x' ∷ xs
        conclusion = inTail x' x xs (IH i)

{-
    "Not A" holds, written, ¬A, if A is empty, or equivalently if there
    is a function A → ∅:
-}

¬ : Type → Type
¬ A = A → ∅


{-
    By induction on xs:
-}

not-in-map-if-not-in-image : {A B : Type} {f : A → B} {y : B}

                           → ((x : A) → ¬(f x ≡ y)) → (xs : List A) → ¬(y ∈ map f xs)

not-in-map-if-not-in-image {A} {B} {f} {y} ni = g
  where
    remark : (x : A) → f x ≡ y → ∅
    remark = ni

    g : (xs : List A) → y ∈ map f xs → ∅
    g []       ()
    g (x ∷ xs) (inHead .(f x) .(map f xs))      = ni x (refl (f x))
    g (x ∷ xs) (inTail .(f x) .y .(map f xs) i) = g xs i


{-
    By induction on zs:
-}

left-if-not-in-image : {A B : Type} {f : A → B} {y : B} (xs : List A) {zs : List B}

                    → ((x : A) → ¬(f x ≡ y)) → y ∈ zs ++ map f xs → y ∈ zs

left-if-not-in-image {A} {B} {f} {y} xs {zs} ni = g zs
  where
    g : (zs : List B) → y ∈ zs ++ map f xs → y ∈ zs
    g [] i = (have (i ∶ y ∈ map f xs))
             ∅-elim (not-in-map-if-not-in-image ni xs i) ∶ y ∈ []
    g (z ∷ zs) (inHead .z .(zs ++ map f xs)) = inHead z zs ∶ z ∈ z ∷ zs
    g (z ∷ zs) (inTail .z y .(zs ++ map f xs) i) = inTail z y zs (g zs i ∶ y ∈ zs)

{-
    By induction on xs:
-}

right-if-not-in-image : {A B : Type} {f : A → B} {y : B} (xs : List A) {zs : List B}

                      → ((x : A) → ¬(f x ≡ y)) → y ∈ map f xs ++ zs → y ∈ zs

right-if-not-in-image {A} {B} {f} {y} xs {zs} ni = g xs
  where
    g : (xs : List A) → y ∈ map f xs ++ zs → y ∈ zs
    g [] i = i
    g (x ∷ xs) (inHead .(f x) .(map f xs ++ zs)) = ∅-elim (ni x (refl (f x)))
    g (x ∷ xs) (inTail .(f x) y .(map f xs ++ zs) i) = g xs i


{-
    By induction on xs:
-}

inLHS : {A : Type} (x : A) (xs ys : List A) → x ∈ xs → x ∈ xs ++ ys
inLHS {A} x xs ys i = g xs i
  where
    g : (xs : List A) → x ∈ xs → x ∈ xs ++ ys
    g (x ∷ xs) (inHead .x .xs)     = inHead x (xs ++ ys)
    g (x ∷ xs) (inTail .x y .xs i) = inTail x y (xs ++ ys) (g xs i)


{-
    Agda checks that the patterns in any definition are exhaustive.
    Notice that the function g doesn't have a case for the empty list
    because this case is impossible and Agda can see that from the
    definition of ∈.

    By induction on xs:
-}

inRHS : {A : Type} (x : A) (xs ys : List A) → x ∈ ys → x ∈ xs ++ ys
inRHS {A} x xs ys i = g xs i
  where
    g : (xs : List A) → x ∈ ys → x ∈ xs ++ ys
    g [] i = i
    g (x' ∷ xs) i = inTail x' x (xs ++ ys) (g xs i)

{-
    With the above lemmas, we can finally prove our main theorem. We
    prove each direction separately.
-}


isValid-∈-validAddresses : {A : Type} (ds : Address) (t : BT A)

                         → isValid ds t ≡ True → ds ∈ validAddresses t

isValid-∈-validAddresses [] Empty e              = inHead [] _ ∶ [] ∈ singleton []
isValid-∈-validAddresses [] (Fork x l r) e       = inHead [] _ ∶ [] ∈ validAddresses (Fork x l r)
isValid-∈-validAddresses (L ∷ ds) Empty ()
isValid-∈-validAddresses (L ∷ ds) (Fork x l r) e = inTail [] _ _ lemma
 where
  IH : ds ∈ validAddresses l
  IH = isValid-∈-validAddresses ds l (e ∶ isValid (L ∷ ds) (Fork x l r) ≡ True)

  a : L ∷ ds ∈ map (L ∷_) (validAddresses l)
  a = mapIsIn (L ∷_) IH

  lemma : L ∷ ds ∈ map (L ∷_) (validAddresses l) ++ map (R ∷_) (validAddresses r)
  lemma = inLHS (L ∷ ds) (map (L ∷_) (validAddresses l)) (map (R ∷_) (validAddresses r)) a

isValid-∈-validAddresses (R ∷ ds) Empty ()
isValid-∈-validAddresses (R ∷ ds) (Fork x l r) e = inTail [] _ _ lemma
 where
  IH : ds ∈ validAddresses r
  IH = isValid-∈-validAddresses ds r (e ∶ isValid (R ∷ ds) (Fork x l r) ≡ True)

  a : R ∷ ds ∈ map (R ∷_) (validAddresses r)
  a = mapIsIn (R ∷_) IH

  lemma : R ∷ ds ∈ map (L ∷_) (validAddresses l) ++ map (R ∷_) (validAddresses r)
  lemma = inRHS (R ∷ ds) (map (L ∷_) (validAddresses l)) (map (R ∷_) (validAddresses r)) a


∈-validAddresses-implies-isValid : {A : Type} (ds : Address) (t : BT A)

                                 → ds ∈ validAddresses t → isValid ds t ≡ True

∈-validAddresses-implies-isValid {A} [] t i = refl (isValid [] t)
∈-validAddresses-implies-isValid {A} (L ∷ ds) Empty (inTail _ _ _ ())
∈-validAddresses-implies-isValid {A} (L ∷ ds) (Fork x l r) (inTail _ _ _ i) = conclusion
  where
    IH : ds ∈ validAddresses l → isValid ds l ≡ True
    IH = ∈-validAddresses-implies-isValid ds l

    remark : L ∷ ds ∈ map (L ∷_) (validAddresses l) ++ map (R ∷_) (validAddresses r)
    remark = i

    c : (ds : _) (vl : _) (vr : _)
      → L ∷ ds ∈ map (L ∷_) vl ++ map (R ∷_) vr → L ∷ ds ∈ map (L ∷_) vl
    c ds vl vr = left-if-not-in-image vr ni
      where
        ni : (es : _) → ¬((R ∷ es) ≡ (L ∷ ds))
        ni es ()

    b : (ds : _) (vl : _) (vr : _) → L ∷ ds ∈ map (L ∷_) vl ++ map (R ∷_) vr → ds ∈ vl
    b ds vl vr i = mapIsIn-converse cons-injective (c ds vl vr i)

    a : ds ∈ validAddresses l
    a = b ds (validAddresses l) (validAddresses r) i

    conclusion : isValid ds l ≡ True
    conclusion = IH a


∈-validAddresses-implies-isValid {A} (R ∷ ds) Empty (inTail _ _ _ ())
∈-validAddresses-implies-isValid {A} (R ∷ ds) (Fork x l r) (inTail _ _ _ i) = conclusion
  where
    IH : ds ∈ validAddresses r → isValid ds r ≡ True
    IH = ∈-validAddresses-implies-isValid ds r

    remark : R ∷ ds ∈ map (L ∷_) (validAddresses l) ++ map (R ∷_) (validAddresses r)
    remark = i

    c : (ds : _) (vl : _) (vr : _)
      → R ∷ ds ∈ map (L ∷_) vl ++ map (R ∷_) vr → R ∷ ds ∈ map (R ∷_) vr
    c ds vl vr = right-if-not-in-image vl ni
      where
        ni : (es : _) → ¬((L ∷ es) ≡ (R ∷ ds))
        ni es ()

    b : (ds : _) (vl : _) (vr : _) → R ∷ ds ∈ map (L ∷_) vl ++ map (R ∷_) vr → ds ∈ vr
    b ds vl vr i = mapIsIn-converse cons-injective (c ds vl vr i)

    a : ds ∈ validAddresses r
    a = b ds (validAddresses l) (validAddresses r) i

    conclusion : isValid ds r ≡ True
    conclusion = IH a

{-
    We now package the last two facts into a single one, to get our main theorem.
-}

_⇔_ : Type → Type → Type
A ⇔ B = (A → B) × (B → A)


main-theorem : {A : Type} (ds : Address) (t : BT A)

            → isValid ds t ≡ True ⇔ ds ∈ validAddresses t

main-theorem ds t = isValid-∈-validAddresses ds t , ∈-validAddresses-implies-isValid ds t

{-
    We conclude by declaring the associativity and precedence of the
    binary operations defined above, so that many round brackets can
    be avoided. Without this, we would get syntax errors above.
-}

infixl  _++_
infix   _≡_
infix   _∈_
infix   _⇔_
infixr  _,_
infixl  id