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

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

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

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

-}

{-

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

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 (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'' _ (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)
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 (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

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

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

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