\subsection{Exercises}

\begin{comment}
\begin{code}
module Exercise2 where

open import Data.List
open import Data.Nat
open import Logic.Id
\end{code}
\end{comment}

\NewExercise{Natural numbers}

Here is a view on pairs of natural numbers.

\begin{code}
data Compare : Nat -> Nat -> Set where
  less : forall {n} k -> Compare n (n + suc k)
  more : forall {n} k -> Compare (n + suc k) n
  same : forall {n} -> Compare n n
\end{code}


\Exercise{Define the view function}

\begin{code}
compare : (n m : Nat) -> Compare n m
compare n m = {! !}
\end{code}

\Exercise{Now use the view to compute the difference between two numbers}

\begin{code}
difference : Nat -> Nat -> Nat
difference n m = {! !}
\end{code}

\NewExercise{Type checking λ-calculus}

Change the type checker from Section~\ref{Views} to include precise
information also in the failing case.

\Exercise{Define inequality on types and change the type comparison to
include inequality proofs. Hint: to figure out what the constructors of {\tt \_≠\_}
should be you can start defining the {\tt \_=?=\_} function and see what you need
from {\tt \_≠\_}.}

\begin{comment}
\begin{code}
infixr 30 _→_
data Type : Set where
  ι   : Type                  -- TeX mode: \iota
  _→_ : Type -> Type -> Type  -- TeX mode: \to
\end{code}
\end{comment}

\begin{code}
data _≠_ : Type -> Type -> Set where
  -- ...

data Equal? : Type -> Type -> Set where
  yes : forall {τ} -> Equal? τ τ
  no  : forall {σ τ} -> σ ≠ τ -> Equal? σ τ

_=?=_ : (σ τ : Type) -> Equal? σ τ
σ =?= τ = {! !}
\end{code}

\Exercise{Define a type of illtyped terms and change {\tt infer} to return such a term upon failure.
Look to the definition of {\tt infer} for clues to the constructors of {\tt BadTerm}.}

\begin{comment}
\begin{code}
data _∈_ {A : Set}(x : A) : List A -> Set where
  hd : forall {xs}   -> x ∈ x :: xs
  tl : forall {y xs} -> x ∈ xs -> x ∈ y :: xs

index : forall {A}{x : A}{xs} -> x ∈ xs -> Nat
index hd     = zero
index (tl p) = suc (index p)

Cxt = List Type

infixl 80 _$_
data Raw : Set where
  var : Nat -> Raw
  _$_ : Raw -> Raw -> Raw
  lam : Type -> Raw -> Raw

data Term (Γ : Cxt) : Type -> Set where
  var : forall {τ} -> τ ∈ Γ -> Term Γ τ
  _$_ : forall {σ τ} -> Term Γ (σ → τ) -> Term Γ σ -> Term Γ τ
  lam : forall σ {τ} -> Term (σ :: Γ) τ -> Term Γ (σ → τ)

erase : forall {Γ τ} -> Term Γ τ -> Raw
erase (var x)   = var (index x)
erase (t $ u)   = erase t $ erase u
erase (lam σ t) = lam σ (erase t)
\end{code}
\end{comment}

\begin{code}
data BadTerm (Γ : Cxt) : Set where
  -- ...

eraseBad : {Γ : Cxt} -> BadTerm Γ -> Raw
eraseBad b = {! !}

data Infer (Γ : Cxt) : Raw -> Set where
  ok  : (τ : Type)(t : Term Γ τ) -> Infer Γ (erase t)
  bad : (b : BadTerm Γ) -> Infer Γ (eraseBad b)

infer : (Γ : Cxt)(e : Raw) -> Infer Γ e
infer Γ e = {! !}
\end{code}

\NewExercise{Properties of list functions}

\begin{comment}
\begin{code}
open import Data.Bool
\end{code}
\end{comment}

Remember the following predicates on lists from Section~\ref{Views}

\begin{fakecode}
data _∈_ {A : Set}(x : A) : List A -> Set where
  hd : forall {xs} -> x ∈ x :: xs
  tl : forall {y xs} -> x ∈ xs -> x ∈ y :: xs
\end{fakecode}

\begin{code}
infixr 30 _::_
data All {A : Set}(P : A -> Set) : List A -> Set where
  []   : All P []
  _::_ : forall {x xs} -> P x -> All P xs -> All P (x :: xs)
\end{code}

\Exercise{Prove the following lemma stating that {\tt All} is sound.}

\begin{code}
lemma-All-∈ : forall {A x xs}{P : A -> Set} ->
              All P xs -> x ∈ xs -> P x
lemma-All-∈ p i = {! !}
\end{code}

We proved that filter computes a sublist of its input. Now let's finish the job.

\Exercise{Below is the proof that all elements of {\tt filter p xs} satisfies {\tt p}. Doing this without any
auxiliary lemmas involves some rather subtle use of with-abstraction.

Figure out what is going on by replaying the construction of the program
and looking at the goal and context in each step.
}

\begin{code}
lem-filter-sound : {A : Set}(p : A -> Bool)(xs : List A) ->
                   All (satisfies p) (filter p xs)
lem-filter-sound p [] = []
lem-filter-sound p (x :: xs) with inspect (p x)
lem-filter-sound p (x :: xs) | it y prf with p x | prf
lem-filter-sound p (x :: xs) | it .true prf  | true  | refl =
  trueIsTrue prf :: lem-filter-sound p xs
lem-filter-sound p (x :: xs) | it .false prf | false | refl =
  lem-filter-sound p xs
\end{code}

\Exercise{Finally prove {\tt filter} complete, by proving that all elements of the original
list satisfying the predicate are present in the result.}

\begin{code}
lem-filter-complete : {A : Set}(p : A -> Bool)(x : A){xs : List A} ->
                      x ∈ xs -> satisfies p x -> x ∈ filter p xs
lem-filter-complete p x el px = {! !}
\end{code}

\NewExercise{An XML universe}

\begin{comment}
\begin{code}
open import Data.String
open import Logic.Base
\end{code}
\end{comment}

Here is simplified universe of XML schemas:
%
\begin{code}
Tag = String

mutual
  data Schema : Set where
    tag : Tag -> List Child -> Schema

  data Child : Set where
    text : Child
    elem : Nat -> Nat -> Schema -> Child
\end{code}
%
The number arguments to {\tt elem} specifies the minimum and maximum number of
repetitions of the subschema. For instance, {\tt elem 0 1 s} would be an optional
child and {\tt elem 1 1 s} would be a child which has to be present.

To define the decoding function we need a type of lists of between $n$ and $m$ elements.
This is the {\tt FList} type below.
\begin{code}
data BList (A : Set) : Nat -> Set where
  []   : forall {n} -> BList A n
  _::_ : forall {n} -> A -> BList A n -> BList A (suc n)

data Cons (A B : Set) : Set where
  _::_ : A -> B -> Cons A B

FList : Set -> Nat -> Nat -> Set
FList A zero    m       = BList A m
FList A (suc n) zero    = False
FList A (suc n) (suc m) = Cons A (FList A n m)
\end{code}
%
Now we define the decoding function as a datatype {\tt XML}.
%
\begin{code}
mutual
  data XML : Schema -> Set where
    element : forall {kids}(t : Tag) -> All Element kids ->
              XML (tag t kids)

  Element : Child -> Set
  Element text         = String
  Element (elem n m s) = FList (XML s) n m
\end{code}

\begin{comment}
\begin{code}
-- Example
schema : Schema
schema = tag "html"
         ( elem 0 1 (tag "head" (elem 0 1 (tag "title" (text :: [])) :: [])) ::
           elem 1 1 (tag "body" (text :: [])) :: []
         )

xml : XML schema
xml = element "html" ([] :: (element "body" ("Some text" :: []) :: []) :: [])
\end{code}
\end{comment}

\Exercise{Implement a function to print XML documents. The string concatenation
function is {\tt \_+++\_}.}

\begin{code}
mutual
  printXML : {s : Schema} -> XML s -> String
  printXML xml = {! !}

  printChildren : {kids : List Child} -> All Element kids -> String
  printChildren xs = {! !}
\end{code}