\documentclass{exam}
\usepackage{agda}
\usepackage{ucs}
\usepackage[utf8x]{inputenc}
\usepackage[greek,english]{babel}
\usepackage{hyperref}

\begin{document}
\AgdaHide{
\begin{code}
module Exercise1 where
\end{code}
}

\title{Types for Programs and Proofs 2017/2018\\Exercise Session 1}
\date{September 4, 2017}
\maketitle

\href{http://www.cse.chalmers.se/edu/course/DAT350/Homework1.agda}{Homework 1}
is now available. It is due on \textit{Monday 18 September at 13.15}. Please
submit it in \href{https://tpp-lp1-17.frs.cse.chalmers.se/}{Fire}. You should
\textit{be prepared} to present your solutions in the exercise session the same
day at 15.15 - 17.00.

%\section{Installation}
%\section{Emacs mode}
%\subsection{Unicode input}
%\subsection{Interactive Agda commands}
\section{Exercises}
\AgdaHide{
\begin{code}
data Bool : Set where
  true  : Bool
  false : Bool

if_then_else_ : {A : Set} → Bool → A → A → A
if true  then x else y = x
if false then x else y = y

_&&_ : Bool → Bool → Bool
b && true  = b
b && false = false
infixl 6 _&&_

data Nat : Set where
  zero : Nat
  succ : Nat → Nat

data _≡_ {A : Set} : A → A → Set where
  refl : {a : A} → a ≡ a
infix 3 _≡_

data _⊎_ (A : Set) (B : Set) : Set where
  inj₁ : (x : A) → A ⊎ B
  inj₂ : (y : B) → A ⊎ B
infixr 0 _⊎_

_∨_ : ∀ (A : Set) (B : Set) → Set
_∨_ = _⊎_
infixr 0 _∨_

data Σ (A : Set) (B : A → Set) : Set where
  _,_ : (a : A) → (b : B a) → Σ A B
infixr 4 _,_

_×_ : ∀ (A : Set) (B : Set) → Set
A × B = Σ A (λ x → B)
infixr 2 _×_

_∧_ : ∀ (A : Set) (B : Set) → Set
_∧_ = _×_
infixr 2 _∧_

iszero : Nat → Bool
iszero zero = true
iszero _    = false
\end{code}
}

\begin{questions}
\question Define the operation \AgdaFunction{not} by gradual refinement and pattern matching.
\begin{code}
not : Bool → Bool
not p = {!!}
\end{code}

\question Define logical or \AgdaFunction{\_||\_}, logical implication \AgdaFunction{\_=>\_}, and logical equivalence \AgdaFunction{\_<=>\_} by gradual refinement and pattern matching.
\begin{AgdaSuppressSpace}{2}
\begin{code}
-- Homework 1, Problem 1 a)
_||_ : Bool → Bool → Bool
p || q = {!!}
\end{code}
\AgdaHide{
\begin{code}
infixl 5 _||_
\end{code}}
\end{AgdaSuppressSpace}
\begin{code}
_=>_ : Bool → Bool → Bool
p => q = {!!}

-- Homework 1, Problem 1 b)
_<=>_ : Bool → Bool → Bool
p <=> q = {!!}
\end{code}

\question Define cut-off subtraction \AgdaFunction{\_-\_}.
\begin{code}
_-_ : Nat → Nat → Nat
n - m = {!!}
\end{code}

\question Define the less than function \AgdaFunction{\_<\_}.
\begin{code}
_<_ : Nat → Nat → Bool
n < m = {!!}
\end{code}

\question Define a version of the conditional \AgdaFunction{ifn\_then\_else\_} which returns natural numbers.
\begin{code}
ifn_then_else_ : Bool → Nat → Nat → Nat
ifn b then n else m = {!!}
\end{code}

\question Define the power function \AgdaFunction{power}.
\begin{code}
-- Homework 1, Problem 2 b)
power : Nat → Nat → Nat
power n m = {!!}
\end{code}

\question Define the factorial function \AgdaFunction{factorial}. Compute the result of factorial for some arguments by normalizing. How large factorials can Agda compute?
\begin{code}
-- Homework 1, Problem 2 a)
factorial : Nat → Nat
factorial n = {!!}
\end{code}

\question Define the Ackermann function\cite{wiki17,nordstrom14}.
\begin{code}
ack : Nat → Nat → Nat
ack n = {!!}
\end{code}

\question Define binary numbers in Agda as a data type \AgdaDatatype{Bin} with four constuctors \AgdaInductiveConstructor{bO}, \AgdaInductiveConstructor{bI}, \AgdaInductiveConstructor{\_O}, \AgdaInductiveConstructor{\_I}: For 0 and 1 standing alone and for adding 0 and 1 at the end of a binary number. Define translation functions \AgdaFunction{bin2nat} and \AgdaFunction{nat2bin} between the binary and the unary numbers. Define addition of binary numbers \AgdaFunction{\_+Bin\_}.
\begin{code}
data Bin : Set where
  -- ...

bin2nat : Bin → Nat
bin2nat x = {!!}

nat2bin : Nat → Bin
nat2bin n = {!!}

_+Bin_ : Bin → Bin → Bin
x +Bin y = {!!}
\end{code}

\question How would you define integers as a data type \AgdaDatatype{Int} in Agda? Then define addition of integers \AgdaFunction{\_+Int\_}.
\begin{code}
data Int : Set where
  -- ...

_+Int_ : Int → Int → Int
n +Int m = {!!}
\end{code}

\question Define a modified type of natural numbers \AgdaDatatype{Nat∗} with a special error value \AgdaInductiveConstructor{error}. Then try to redefine division \AgdaFunction{\_÷∗\_} by repeated subtraction so that

\AgdaBound{m} \AgdaFunction{÷∗} \AgdaInductiveConstructor{zero} \AgdaSymbol{=} \AgdaInductiveConstructor{error}

and note that the termination checker will not accept this definition.
\AgdaHide{
\begin{code}
{-# NON_TERMINATING #-}
_÷_ : Nat → Nat → Nat
m ÷ n = ifn (iszero n || m < n) then zero else succ ((m - n) ÷ n)
\end{code}
}
\begin{code}
data Nat∗ : Set where
  -- ...

_÷∗_ : Nat → Nat → Nat∗
x ÷∗ y = {!!}
\end{code}

\question Define equality of natural numbers \AgdaFunction{\_==\_} using only official primitive recursion \AgdaFunction{natrec}. Hint: Use cut-off subtraction \AgdaFunction{\_-\_}.
\begin{code}
natrec : Nat → (Nat → Nat) → Nat → Nat
natrec c d zero = c
natrec c d (succ n) = d (natrec c d n)

_==_ : Nat → Nat → Nat
n == m = {!!}
\end{code}

\question Pick a theorem from \cite[Chapter 2]{stump16} and prove it.
% https://svn.divms.uiowa.edu/repos/clc/projects/agda/ial/bool-thms.agda
\begin{code}
notnot-elim : ∀ (b : Bool) → not (not b) ≡ b
notnot-elim b = {!!}

&&-idem : ∀ (p : Bool) → p && p ≡ p
&&-idem p = {!!}

||-idem : ∀ (p : Bool) → p || p ≡ p
||-idem p = {!!}

||≡ff₁ : ∀ (p q : Bool) → p || q ≡ false → false ≡ p
||≡ff₁ = {!!}

||≡ff₂ : ∀ (p q : Bool) → p || q ≡ false → q ≡ false
||≡ff₂ = {!!}

||-tt : ∀ (p : Bool) → p || true ≡ true
||-tt = {!!}

||-cong₁ : ∀ (p p' q : Bool) → p ≡ p' → p || q ≡ p' || q
||-cong₁ = {!!}

||-cong₂ : ∀ (p q q' : Bool) → q ≡ q' → p || q ≡ p || q'
||-cong₂ = {!!}

ite-same : ∀ {A : Set} (b : Bool) (x : A) → if b then x else x ≡ x
ite-same = {!!}

ite-arg : ∀ {A B : Set} (f : A → B) (b : Bool) (x y : A) →
            f (if b then x else y) ≡ if b then f x else f y
ite-arg = {!!}

contra : false ≡ true → ∀ {P : Set} → P
contra = {!!}

||-split : ∀ (p q : Bool) → p || q ≡ true → p ≡ true ⊎ q ≡ true
||-split = {!!}

canon : ∀ (p : Bool) → p ≡ true ⊎ p ≡ false
canon = {!!}

&&-snd : ∀ (p q : Bool) → p && q ≡ true → q ≡ true
&&-snd = {!!}

&&-fst : ∀ (p q : Bool) → p && q ≡ true → p ≡ true
&&-fst = {!!}

&&-combo : ∀ (p q : Bool) → p ≡ true → q ≡ true → p && q ≡ true
&&-combo = {!!}

&&-false : ∀ (p : Bool) → p && false ≡ false
&&-false = {!!}
\end{code}
% https://svn.divms.uiowa.edu/repos/clc/projects/agda/ial/bool-thms2.agda
\begin{code}
false-imp : ∀ (b : Bool) → false => b ≡ true
false-imp = {!!}

=>-true : ∀ (b : Bool) → b => true ≡ true
=>-true = {!!}

=>-false : ∀ (b : Bool) → b => false ≡ not b
=>-false = {!!}

true-=> : ∀ (b : Bool) → true => b ≡ b
true-=> = {!!}

&&-true : ∀ (b : Bool) → b && true ≡ b
&&-true = {!!}

||-false : ∀ (b : Bool) → b || false ≡ b
||-false = {!!}

&&-contra : ∀ (b : Bool) → b && not b ≡ false
&&-contra = {!!}

&&-comm : ∀ (p q : Bool) → p && q ≡ q && p
&&-comm = {!!}

||-comm : ∀ (p q : Bool) → p || q ≡ q || p
||-comm = {!!}

&&-assoc : ∀ (p q b3 : Bool) → p && (q && b3) ≡ (p && q) && b3
&&-assoc = {!!}

||-assoc : ∀ (p q b3 : Bool) → p || (q || b3) ≡ (p || q) || b3
||-assoc = {!!}

not-over-&& : ∀ (p q : Bool) → not ( p && q ) ≡ (not p || not q)
not-over-&& = {!!}

not-over-|| : ∀ (p q : Bool) → not ( p || q ) ≡ (not p && not q)
not-over-|| = {!!}

&&-over-||-l : ∀ (p q r : Bool) → p && (q || r) ≡ (p && q) || (p && r)
&&-over-||-l = {!!}

&&-over-||-r : ∀ (p q r : Bool) → (p || q) && r ≡ (p && r) || (q && r)
&&-over-||-r = {!!}

||-over-&&-l : ∀ (p q r : Bool) → p || (q && r) ≡ (p || q) && (p || r)
||-over-&&-l = {!!}

||-over-&&-r : ∀ (p q r : Bool) → (p && q) || r ≡ (p || r) && (q || r)
||-over-&&-r = {!!}

&&-cong₁ : ∀ (p p' q : Bool) → p ≡ p' → p && q ≡ p' && q
&&-cong₁ = {!!}

&&-cong₂ : ∀ (p q q' : Bool) → q ≡ q' → p && q ≡ p && q'
&&-cong₂ = {!!}

&&-intro : ∀ (p q : Bool) → p ≡ true → q ≡ true → p && q ≡ true
&&-intro = {!!}

||-intro₁ : ∀ (p q : Bool) → p ≡ true → p || q ≡ true
||-intro₁ = {!!}

&&-elim : ∀ (p q : Bool) → p && q ≡ true → p ≡ true ∧ q ≡ true
&&-elim = {!!}

&&-elim₁ : ∀ (p q : Bool) → p && q ≡ true → p ≡ true
&&-elim₁ = {!!}

&&-elim₂ : ∀ (p q : Bool) → p && q ≡ true → q ≡ true
&&-elim₂ = {!!}

||-elim : ∀ (p q : Bool) → p || q ≡ true → p ≡ true ∨ q ≡ true
||-elim = {!!}

not-cong : ∀ (p q : Bool) → p ≡ q → not p ≡ not q
not-cong = {!!}

ite-cong₁ : ∀ {A : Set} (b b' : Bool) {x y : A} → b ≡ b' → (if b then x else y) ≡ (if b' then x else y)
ite-cong₁ = {!!}

ite-cong₂ : ∀ {A : Set} (b : Bool) {x x' y : A} → x ≡ x' → (if b then x else y) ≡ (if b then x' else y)
ite-cong₂ = {!!}

ite-cong₃ : ∀ {A : Set} (b : Bool) (x y y' : A) → y ≡ y' → if b then x else y ≡ if b then x else y'
ite-cong₃ = {!!}

&&-split : ∀ (p q : Bool) → p && q ≡ false → p ≡ false ⊎ q ≡ false
&&-split = {!!}

=>-same : ∀ (p : Bool) → p => p ≡ true
=>-same = {!!}

=>-to-|| : ∀ (p q : Bool) → (p => q) ≡ (not p || q)
=>-to-|| = {!!}

=>-mp : ∀ (p q : Bool) → p => q ≡ true → p ≡ true → q ≡ true
=>-mp = {!!}

=>-antisymm : ∀ {p q : Bool} → p => q ≡ true → q => p ≡ true → p ≡ q
=>-antisymm = {!!}
\end{code}
\end{questions}

\begin{thebibliography}{9}
\bibitem{dybjer17}
  Peter Dybjer,
  \textit{An Introduction to Programming and Proving in Agda},
  2017.
\bibitem{stump16}
  Aaron Stump,
  \textit{Verified Functional Programming in Agda},
  Association for Computing Machinery and Morgan \& Claypool Publishers,
  2016.
\bibitem{wiki17}
  Wikipedia contributors,
  \textit{Ackermann function},
  \url{https://en.wikipedia.org/wiki/Ackermann_function},
  2017.
\bibitem{nordstrom14}
  Bengt Nordström,
  \textit{The primitive recursive functions},
  \url{http://www.cse.chalmers.se/edu/course/DIT310_Models_of_Computation/reading/The_primitive_recursive_functions.pdf},
  2014.
\bibitem{agda17}
  Agda contributors,
  \textit{The Agda User Manual},
  \url{https://agda.readthedocs.io/en/latest/},
  2017.
\end{thebibliography}
\end{document}