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

Martín Hötzel Escardó
5th October 2017

This is a brief introduction to Agda, written mainly for Haskell
programmers.

http://wiki.portal.chalmers.se/agda/pmwiki.php

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

-}

Type = Set

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

cons : {A : Type} → A → List A → List A
cons = _∷_

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 (cons 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 (cons 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 (cons x) (++assoc'' xs ys zs)

{-
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) []

{-
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'

{-
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

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

data Σ {A : Type} (B : A → Type) : Type where
_,_ : (x : A) → (y : B x) → Σ {A} B

{-
Notice that Σ {A} B is equivalent to Σ \(x : A) → B x, where \ is
a synonym for λ, which we use exclusively for Σ types.
-}

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

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

{-
Induction on Σ is uncurry:
-}

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

→ ((x : A) (y : B x) → P(x , y))
---------------------------------
→ (z : Σ 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 [] (Fork x l r) p
= Fork x l r , (refl _ ∶ subtree [] (Fork x l r) ≡ Just (Fork x l r))
∶ Σ \t' → subtree [] (Fork x l r) ≡ Just t'

valid-gives-just (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' → subtree (L ∷ ds) (Fork x l r) ≡ Just t')
∶  Σ \t' → subtree ds l ≡ Just t'

valid-gives-just (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' → subtree (R ∷ ds) (Fork x l r) ≡ Just t')
∶  Σ \t' → 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 (Fork _ l r) = (singleton [])
++ (map (cons L) (validAddresses l))
++ (map (cons 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'' _ (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(cons 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)
b : x ≡ x'
b = inj a
c : x ∈ 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 (cons L) (validAddresses l)
a = mapIsIn (cons L) IH
lemma : L ∷ ds ∈ map (cons L) (validAddresses l) ++ map (cons R) (validAddresses r)
lemma = inLHS (L ∷ ds) (map (cons L) (validAddresses l)) (map (cons 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 (cons R) (validAddresses r)
a = mapIsIn (cons R) IH
lemma : R ∷ ds ∈ map (cons L) (validAddresses l) ++ map (cons R) (validAddresses r)
lemma = inRHS (R ∷ ds) (map (cons L) (validAddresses l)) (map (cons 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
remark : L ∷ ds ∈ map (cons L) (validAddresses l) ++ map (cons R) (validAddresses r)
remark = i
c : (ds : _) (vl : _) (vr : _)
→ L ∷ ds ∈ map (cons L) vl ++ map (cons R) vr → L ∷ ds ∈ map (cons 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 (cons L) vl ++ map (cons R) vr → ds ∈ vl
b ds vl vr i = mapIsIn-converse cons-injective (c ds vl vr i)
a : ds ∈ validAddresses l
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
remark : R ∷ ds ∈ map (cons L) (validAddresses l) ++ map (cons R) (validAddresses r)
remark = i
c : (ds : _) (vl : _) (vr : _)
→ R ∷ ds ∈ map (cons L) vl ++ map (cons R) vr → R ∷ ds ∈ map (cons 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 (cons L) vl ++ map (cons R) vr → ds ∈ vr
b ds vl vr i = mapIsIn-converse cons-injective (c ds vl vr i)
a : ds ∈ validAddresses r
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

{-
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 3 _++_
infix  2 _≡_
infix  2 _∈_
infix  1 _⇔_
infixr 1 _,_
infixl 0 id
```