Skip to content

Commit

Permalink
Update for consistent capitalization
Browse files Browse the repository at this point in the history
david-christiansen committed Sep 30, 2014

Verified

This commit was signed with the committer’s verified signature.
sdispater Sébastien Eustace
1 parent 919cd5f commit 20572cd
Showing 12 changed files with 102 additions and 102 deletions.
26 changes: 13 additions & 13 deletions content/interp.tex
Original file line number Diff line number Diff line change
@@ -42,8 +42,8 @@ \section{Example: The Well-Typed Interpreter}

\begin{code}[caption={Expression representation},label=exprty, float=htp]
data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where
stop : HasType fZ (t :: G) t
pop : HasType k G t -> HasType (fS k) (u :: G) t
Stop : HasType FZ (t :: G) t
Pop : HasType k G t -> HasType (FS k) (u :: G) t

data Expr : Vect n Ty -> Ty -> Type where
Var : HasType i G t -> Expr G t
@@ -61,20 +61,20 @@ \section{Example: The Well-Typed Interpreter}

\begin{code}
data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where
stop : HasType fZ (t :: G) t
pop : HasType k G t -> HasType (fS k) (u :: G) t
Stop : HasType FZ (t :: G) t
Pop : HasType k G t -> HasType (FS k) (u :: G) t
\end{code}

\noindent
We can treat \emph{stop} as a proof that the most recently defined variable is well-typed, and \emph{pop n} as a proof that, if the \texttt{n}th most recently defined variable is well-typed, so is the \texttt{n+1}th.
In practice, this means we use \texttt{stop} to refer to the most recently defined variable, \texttt{pop stop} to refer to the next, and so on, via the \texttt{Var} constructor:
We can treat \emph{Stop} as a proof that the most recently defined variable is well-typed, and \emph{Pop n} as a proof that, if the \texttt{n}th most recently defined variable is well-typed, so is the \texttt{n+1}th.
In practice, this means we use \texttt{Stop} to refer to the most recently defined variable, \texttt{Pop Stop} to refer to the next, and so on, via the \texttt{Var} constructor:

\begin{code}
Var : HasType i G t -> Expr G t
\end{code}

\noindent
So, in an expression \texttt{$\backslash$x. $\backslash$y. x y}, the variable \texttt{x} would have a de Bruijn index of 1, represented as \texttt{pop stop}, and \texttt{y 0}, represented as \texttt{stop}.
So, in an expression \texttt{$\backslash$x. $\backslash$y. x y}, the variable \texttt{x} would have a de Bruijn index of 1, represented as \texttt{Pop Stop}, and \texttt{y 0}, represented as \texttt{Stop}.
We find these by counting the number of lambdas between the definition and the use.

\noindent
@@ -128,8 +128,8 @@ \section{Example: The Well-Typed Interpreter}
(::) : interpTy a -> Env G -> Env (a :: G)

lookup : HasType i G t -> Env G -> interpTy t
lookup stop (x :: xs) = x
lookup (pop k) (x :: xs) = lookup k xs
lookup Stop (x :: xs) = x
lookup (Pop k) (x :: xs) = lookup k xs
\end{code}

\begin{code}[caption={Intepreter definition},label=interpdef]
@@ -197,7 +197,7 @@ \section{Example: The Well-Typed Interpreter}

\begin{code}
add : Expr G (TyFun TyInt (TyFun TyInt TyInt))
add = Lam (Lam (Op (+) (Var stop) (Var (pop stop))))
add = Lam (Lam (Op (+) (Var Stop) (Var (Pop Stop))))
\end{code}

\noindent
@@ -206,9 +206,9 @@ \section{Example: The Well-Typed Interpreter}

\begin{code}
fact : Expr G (TyFun TyInt TyInt)
fact = Lam (If (Op (==) (Var stop) (Val 0))
(Val 1) (Op (*) (App fact (Op (-) (Var stop) (Val 1)))
(Var stop)))
fact = Lam (If (Op (==) (Var Stop) (Val 0))
(Val 1) (Op (*) (App fact (Op (-) (Var Stop) (Val 1)))
(Var Stop)))
\end{code}

\noindent
2 changes: 1 addition & 1 deletion content/provisional.tex
Original file line number Diff line number Diff line change
@@ -123,7 +123,7 @@ \subsection{Provisional definitions}

\begin{lstlisting}[style=stdout]
sym : l = r -> r = l
sym refl = refl
sym Refl = Refl
\end{lstlisting}

\noindent
12 changes: 6 additions & 6 deletions content/syntax/dsl.tex
Original file line number Diff line number Diff line change
@@ -9,9 +9,9 @@ \subsection{\texttt{dsl} notation}

\begin{code}
fact : Expr G (TyFun TyInt TyInt)
fact = Lam (If (Op (==) (Var stop) (Val 0))
(Val 1) (Op (*) (app fact (Op (-) (Var stop) (Val 1)))
(Var stop)))
fact = Lam (If (Op (==) (Var Stop) (Val 0))
(Val 1) (Op (*) (app fact (Op (-) (Var Stop) (Val 1)))
(Var Stop)))
\end{code}

\noindent
@@ -21,13 +21,13 @@ \subsection{\texttt{dsl} notation}
dsl expr
lambda = Lam
variable = Var
index_first = stop
index_next = pop
index_first = Stop
index_next = Pop
\end{code}

\noindent
A \texttt{dsl} block describes how each syntactic construct is represented in an object language.
Here, in the \texttt{expr} language, any \Idris{} lambda is translated to a \texttt{Lam} constructor; any variable is translated to the \texttt{Var} constructor, using \texttt{pop} and \texttt{stop} to construct the de Bruijn index (i.e., to count how many bindings since the variable itself was bound).
Here, in the \texttt{expr} language, any \Idris{} lambda is translated to a \texttt{Lam} constructor; any variable is translated to the \texttt{Var} constructor, using \texttt{Pop} and \texttt{Stop} to construct the de Bruijn index (i.e., to count how many bindings since the variable itself was bound).
It is also possible to overload \texttt{let} in this way. We can now write \texttt{fact} as follows:

\begin{code}
27 changes: 13 additions & 14 deletions content/theorems.tex
Original file line number Diff line number Diff line change
@@ -8,7 +8,7 @@ \subsection{Equality}

\begin{code}
data (=) : a -> b -> Type where
refl : x = x
Refl : x = x
\end{code}

\noindent
@@ -17,10 +17,10 @@ \subsection{Equality}

\begin{code}
fiveIsFive : 5 = 5
fiveIsFive = refl
fiveIsFive = Refl

twoPlusTwo : 2 + 2 = 4
twoPlusTwo = refl
twoPlusTwo = Refl
\end{code}

\subsection{The Empty Type}
@@ -69,7 +69,7 @@ \subsection{Simple Theorems}
The proof itself is trivial, because \texttt{plus Z n} normalises to \texttt{n} by the definition of \texttt{plus}:

\begin{code}
plusReduces n = refl
plusReduces n = Refl
\end{code}

\noindent
@@ -78,7 +78,7 @@ \subsection{Simple Theorems}

\begin{code}
plusReducesZ : (n:Nat) -> n = plus n Z
plusReducesZ Z = refl
plusReducesZ Z = Refl
plusReducesZ (S k) = cong (plusReducesZ k)
\end{code}

@@ -94,7 +94,7 @@ \subsection{Simple Theorems}

\begin{code}
plusReducesS : (n:Nat) -> (m:Nat) -> S (plus n m) = plus n (S m)
plusReducesS Z m = refl
plusReducesS Z m = Refl
plusReducesS (S k) m = cong (plusReducesS k m)
\end{code}

@@ -157,25 +157,24 @@ \subsection{Interactive theorem proving}
\end{lstlisting}

\noindent
Now we have to prove that \texttt{Z} equals \texttt{Z}, which is easy to prove by \texttt{refl}.
To apply a function, such as \texttt{refl}, we use \texttt{refine} which introduces subgoals for each of the function's explicit arguments (\texttt{refl} has none):
Now we have to prove that \texttt{Z} equals \texttt{Z}, which is easy to prove by \texttt{Refl}.
To apply a function, such as \texttt{Refl}, we use \texttt{refine} which introduces subgoals for each of the function's explicit arguments (\texttt{Refl} has none):

\begin{lstlisting}[style=stdout]
-plusredZ_Z> refine refl
-plusredZ_Z> refine Refl
plusredZ_Z: no more goals
\end{lstlisting}

\noindent
Here, we could also have used the \texttt{trivial} tactic, which tries to refine by \texttt{refl}, and if that fails, tries to refine by each name in the local context.
Here, we could also have used the \texttt{trivial} tactic, which tries to refine by \texttt{Refl}, and if that fails, tries to refine by each name in the local context.
When a proof is complete, we use the \texttt{qed} tactic to add the proof to the global context, and remove the metavariable from the unsolved metavariables list.
This also outputs a trace of the proof:

\begin{code}
-plusredZ_Z> qed
plusredZ_Z = proof {
compute;
refine refl;
}
plusredZ_Z = proof
compute
refine Refl
\end{code}

\begin{lstlisting}[style=stdout]
47 changes: 24 additions & 23 deletions content/typesfuns.tex
Original file line number Diff line number Diff line change
@@ -246,12 +246,12 @@ \subsubsection{The Finite Sets}

\begin{code}
data Fin : Nat -> Type where
fZ : Fin (S k)
fS : Fin k -> Fin (S k)
FZ : Fin (S k)
FS : Fin k -> Fin (S k)
\end{code}

\noindent
\tDC{fZ} is the zeroth element of a finite set with \texttt{S k} elements; \texttt{fS n} is the \texttt{n+1}th element of a finite set with \texttt{S k} elements.
\tDC{FZ} is the zeroth element of a finite set with \texttt{S k} elements; \texttt{FS n} is the \texttt{n+1}th element of a finite set with \texttt{S k} elements.
\tTC{Fin} is indexed by a \tTC{Nat}, which represents the number of elements in the set.
Obviously we can't construct an element of an empty set, so neither constructor targets \texttt{Fin Z}.

@@ -262,8 +262,8 @@ \subsubsection{The Finite Sets}

\begin{code}
index : Fin n -> Vect n a -> a
index fZ (x :: xs) = x
index (fS k) (x :: xs) = index k xs
index FZ (x :: xs) = x
index (FS k) (x :: xs) = index k xs
\end{code}

\noindent
@@ -298,7 +298,7 @@ \subsubsection{Implicit Arguments}
Implicit arguments can still be given explicitly in applications, using \texttt{\{a=value\}} and \texttt{\{n=value\}}, for example:

\begin{code}
index {a=Int} {n=2} fZ (2 :: 3 :: Nil)
index {a=Int} {n=2} FZ (2 :: 3 :: Nil)
\end{code}

\noindent
@@ -322,22 +322,22 @@ \subsubsection{``\texttt{using}'' notation}

\begin{code}
data Elem : a -> Vect n a -> Type where
here : {x:a} -> {xs:Vect n a} -> Elem x (x :: xs)
there : {x,y:a} -> {xs:Vect n a} -> Elem x xs -> Elem x (y :: xs)
Here : {x:a} -> {xs:Vect n a} -> Elem x (x :: xs)
There : {x,y:a} -> {xs:Vect n a} -> Elem x xs -> Elem x (y :: xs)
\end{code}

\noindent
An instance of \texttt{Elem x xs} states that \texttt{x} is an element of
\texttt{xs}.
We can construct such a predicate if the required element is \texttt{here}, at the head of the vector, or \texttt{there}, in the tail of the vector.
We can construct such a predicate if the required element is \texttt{Here}, at the head of the vector, or \texttt{There}, in the tail of the vector.
For example:

\begin{code}
testVec : Vect 4 Int
testVec = 3 :: 4 :: 5 :: 6 :: Nil

inVect : Elem 5 testVec
inVect = there (there here)
inVect = There (There Here)
\end{code}

\noindent
@@ -347,8 +347,8 @@ \subsubsection{``\texttt{using}'' notation}
\begin{code}
using (x:a, y:a, xs:Vect n a)
data Elem : a -> Vect n a -> Type where
here : Elem x (x :: xs)
there : Elem x xs -> Elem x (y :: xs)
Here : Elem x (x :: xs)
There : Elem x xs -> Elem x (y :: xs)
\end{code}

\subsubsection*{Note: Declaration Order and \texttt{mutual} blocks}
@@ -641,11 +641,12 @@ \subsubsection{Tuples and Dependent Pairs}

\subsubsection*{Dependent Pairs}

Dependent pairs allow the type of the second element of a pair to depend on the value of the first element:
Dependent pairs allow the type of the second element of a pair to depend on the value of the first element.
Traditionally, these are referred to as ``sigma types'':

\begin{code}
data Exists : (A : Type) -> (P : A -> Type) -> Type where
Ex_intro : {P : A -> Type} -> (a : A) -> P a -> Exists A P
data Sigma : (A : Type) -> (P : A -> Type) -> Type where
MkSigma : {P : A -> Type} -> (a : A) -> P a -> Sigma A P
\end{code}

\noindent
@@ -661,8 +662,8 @@ \subsubsection*{Dependent Pairs}
If you like, you can write it out the long way, the two are precisely equivalent.

\begin{code}
vec : Exists Nat (\n => Vect n Int)
vec = Ex_intro 2 [3, 4]
vec : Sigma Nat (\n => Vect n Int)
vec = MkSigma 2 [3, 4]
\end{code}

The type checker could of course infer the value of the first element from the
@@ -712,24 +713,24 @@ \subsubsection*{Dependent Pairs}
\noindent
We will see more on \texttt{with} notation later.

\subsection{\texttt{so}}
\subsection{\texttt{So}}

The \texttt{so} data type is a predicate on \texttt{Bool} which guarantees that the value is true:
The \texttt{So} data type is a predicate on \texttt{Bool} which guarantees that the value is true:

\begin{code}
data so : Bool -> Type where
oh : so True
data So : Bool -> Type where
Oh : So True
\end{code}

\noindent
This is most useful for providing a static guarantee that a dynamic check has been made.
For example, we might provide a safe interface to a function which draws a pixel on a graphical display as follows, where \texttt{so (inBounds x y)} guarantees that the point \texttt{(x,y)} is within the bounds of a $640\times480$ window:
For example, we might provide a safe interface to a function which draws a pixel on a graphical display as follows, where \texttt{So (inBounds x y)} guarantees that the point \texttt{(x,y)} is within the bounds of a $640\times480$ window:

\begin{code}
inBounds : Int -> Int -> Bool
inBounds x y = x >= 0 && x < 640 && y >= 0 && y < 480

drawPoint : (x : Int) -> (y : Int) -> so (inBounds x y) -> IO ()
drawPoint : (x : Int) -> (y : Int) -> So (inBounds x y) -> IO ()
drawPoint x y p = unsafeDrawPoint x y
\end{code}

10 changes: 5 additions & 5 deletions content/views.tex
Original file line number Diff line number Diff line change
@@ -38,8 +38,8 @@ \subsection{The \texttt{with} rule --- matching intermediate values}

\begin{code}
data Parity : Nat -> Type where
even : Parity (n + n)
odd : Parity (S (n + n))
Even : Parity (n + n)
Odd : Parity (S (n + n))
\end{code}

\noindent
@@ -60,13 +60,13 @@ \subsection{The \texttt{with} rule --- matching intermediate values}
natToBin : Nat -> List Bool
natToBin Z = Nil
natToBin k with (parity k)
natToBin (j + j) | even = False :: natToBin j
natToBin (S (j + j)) | odd = True :: natToBin j
natToBin (j + j) | Even = False :: natToBin j
natToBin (S (j + j)) | Odd = True :: natToBin j
\end{code}

\noindent
The value of the result of \texttt{parity k} affects the form of \texttt{k}, because the result of \texttt{parity k} depends on \texttt{k}.
So, as well as the patterns for the result of the intermediate computation (\texttt{even} and \texttt{odd}) right of the \texttt{$\mid$}, we also write how the results affect the other patterns left of the $\mid$.
So, as well as the patterns for the result of the intermediate computation (\texttt{Even} and \texttt{odd}) right of the \texttt{$\mid$}, we also write how the results affect the other patterns left of the $\mid$.
Note that there is a function in the patterns (\texttt{+}) and repeated occurrences of \texttt{j}---this is allowed because another argument has determined the form of these patterns.

We will return to this function in Section~\ref{sect:provisional} to complete the definition of \texttt{parity}.
16 changes: 8 additions & 8 deletions examples/binary.idr
Original file line number Diff line number Diff line change
@@ -11,21 +11,21 @@ instance Show (Binary n) where
show bEnd = ""

data Parity : Nat -> Type where
even : Parity (n + n)
odd : Parity (S (n + n))
Even : Parity (n + n)
Odd : Parity (S (n + n))

parity : (n:Nat) -> Parity n
parity Z = even {n=Z}
parity (S Z) = odd {n=Z}
parity Z = Even {n=Z}
parity (S Z) = Odd {n=Z}
parity (S (S k)) with (parity k)
parity (S (S (j + j))) | even ?= even {n=S j}
parity (S (S (S (j + j)))) | odd ?= odd {n=S j}
parity (S (S (j + j))) | Even ?= Even {n=S j}
parity (S (S (S (j + j)))) | Odd ?= Odd {n=S j}

natToBin : (n:Nat) -> Binary n
natToBin Z = bEnd
natToBin (S k) with (parity k)
natToBin (S (j + j)) | even = bI (natToBin j)
natToBin (S (S (j + j))) | odd ?= bO (natToBin (S j))
natToBin (S (j + j)) | Even = bI (natToBin j)
natToBin (S (S (j + j))) | Odd ?= bO (natToBin (S j))

intToNat : Int -> Nat
intToNat 0 = Z
20 changes: 10 additions & 10 deletions examples/interp.idr
Original file line number Diff line number Diff line change
@@ -14,12 +14,12 @@ using (G : Vect n Ty)
(::) : interpTy a -> Env G -> Env (a :: G)

data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where
stop : HasType fZ (t :: G) t
pop : HasType k G t -> HasType (fS k) (u :: G) t
Stop : HasType FZ (t :: G) t
Pop : HasType k G t -> HasType (FS k) (u :: G) t

lookup : HasType i G t -> Env G -> interpTy t
lookup stop (x :: xs) = x
lookup (pop k) (x :: xs) = lookup k xs
lookup Stop (x :: xs) = x
lookup (Pop k) (x :: xs) = lookup k xs

data Expr : Vect n Ty -> Ty -> Type where
Var : HasType i G t -> Expr G t
@@ -40,20 +40,20 @@ using (G : Vect n Ty)
else interp env e

eId : Expr G (TyFun TyInt TyInt)
eId = Lam (Var stop)
eId = Lam (Var Stop)

eAdd : Expr G (TyFun TyInt (TyFun TyInt TyInt))
eAdd = Lam (Lam (Op (+) (Var stop) (Var (pop stop))))
eAdd = Lam (Lam (Op (+) (Var Stop) (Var (Pop Stop))))

eEq : Expr G (TyFun TyInt (TyFun TyInt TyBool))
eEq = Lam (Lam (Op (==) (Var stop) (Var (pop stop))))
eEq = Lam (Lam (Op (==) (Var Stop) (Var (Pop Stop))))

eDouble : Expr G (TyFun TyInt TyInt)
eDouble = Lam (App (App eAdd (Var stop)) (Var stop))
eDouble = Lam (App (App eAdd (Var Stop)) (Var Stop))

fact : Expr G (TyFun TyInt TyInt)
fact = Lam (If (Op (==) (Var stop) (Val 0))
(Val 1) (Op (*) (App fact (Op (-) (Var stop) (Val 1))) (Var stop)))
fact = Lam (If (Op (==) (Var Stop) (Val 0))
(Val 1) (Op (*) (App fact (Op (-) (Var Stop) (Val 1))) (Var Stop)))

testFac : Int
testFac = interp [] fact 4
10 changes: 5 additions & 5 deletions examples/theorems.idr
Original file line number Diff line number Diff line change
@@ -1,9 +1,9 @@

fiveIsFive : 5 = 5
fiveIsFive = refl
fiveIsFive = Refl

twoPlusTwo : 2 + 2 = 4
twoPlusTwo = refl
twoPlusTwo = Refl

total disjoint : (n : Nat) -> Z = S n -> _|_
disjoint n p = replace {P = disjointTy} p ()
@@ -25,14 +25,14 @@ empty2 : _|_
empty2 = empty2

plusReduces : (n:Nat) -> plus Z n = n
plusReduces n = refl
plusReduces n = Refl

plusReducesZ : (n:Nat) -> n = plus n Z
plusReducesZ Z = refl
plusReducesZ Z = Refl
plusReducesZ (S k) = cong (plusReducesZ k)

plusReducesS : (n:Nat) -> (m:Nat) -> S (plus n m) = plus n (S m)
plusReducesS Z m = refl
plusReducesS Z m = Refl
plusReducesS (S k) m = cong (plusReducesS k m)

plusReducesZ' : (n:Nat) -> n = plus n Z
16 changes: 8 additions & 8 deletions examples/views.idr
Original file line number Diff line number Diff line change
@@ -1,21 +1,21 @@
module views

data Parity : Nat -> Type where
even : Parity (n + n)
odd : Parity (S (n + n))
Even : Parity (n + n)
Odd : Parity (S (n + n))

parity : (n:Nat) -> Parity n
parity Z = even {n=Z}
parity (S Z) = odd {n=Z}
parity Z = Even {n=Z}
parity (S Z) = Odd {n=Z}
parity (S (S k)) with (parity k)
parity (S (S (j + j))) | even ?= even {n=S j}
parity (S (S (S (j + j)))) | odd ?= odd {n=S j}
parity (S (S (j + j))) | Even ?= Even {n=S j}
parity (S (S (S (j + j)))) | Odd ?= Odd {n=S j}

natToBin : Nat -> List Bool
natToBin Z = Nil
natToBin k with (parity k)
natToBin (j + j) | even = False :: natToBin j
natToBin (S (j + j)) | odd = True :: natToBin j
natToBin (j + j) | Even = False :: natToBin j
natToBin (S (j + j)) | Odd = True :: natToBin j


---------- Proofs ----------
12 changes: 6 additions & 6 deletions examples/viewsbroken.idr
Original file line number Diff line number Diff line change
@@ -1,12 +1,12 @@

data Parity : Nat -> Type where
even : Parity (n + n)
odd : Parity (S (n + n))
Even : Parity (n + n)
Odd : Parity (S (n + n))

parity : (n:Nat) -> Parity n
parity Z = even {n=Z}
parity (S Z) = odd {n=Z}
parity Z = Even {n=Z}
parity (S Z) = Odd {n=Z}
parity (S (S k)) with (parity k)
parity (S (S (j + j))) | even = even {n=S j}
parity (S (S (S (j + j)))) | odd = odd {n=S j}
parity (S (S (j + j))) | Even = Even {n=S j}
parity (S (S (S (j + j)))) | Odd = Odd {n=S j}

6 changes: 3 additions & 3 deletions fpmacros.sty
Original file line number Diff line number Diff line change
@@ -453,7 +453,7 @@ Program & Version & Instructions & Thunks & Memory Accesses & Cells \\
\newcommand{\hq}{\pad{\:}{=}}
\newcommand{\defq}{\mapsto}

\newcommand{\refl}{\TC{refl}}
\newcommand{\refl}{\TC{Refl}}



@@ -558,7 +558,7 @@ Program & Version & Instructions & Thunks & Memory Accesses & Cells \\
\newcommand{\Exists}{\DC{Exists}}

\newcommand{\ListPair}[2]{\sig{#1}{\List\:\vA}.#2 = \FN{length}\:#1}
\newcommand{\lpNilDef}{\lpNil{\FN{refl}\:\Z}}
\newcommand{\lpNilDef}{\lpNil{\FN{Refl}\:\Z}}
\newcommand{\lpNil}[1]{(\nil\:\vA,#1)}
\newcommand{\lpConsDef}[3]{\lpCons{#1}{(\FN{fst\:#2})}{\FN{resp}\:(\FN{snd}\:#2)}}
\newcommand{\lpCons}[3]{(\cons\:#1\:#2,#3)}
@@ -656,7 +656,7 @@ Program & Version & Instructions & Thunks & Memory Accesses & Cells \\

% Equality

\newcommand{\Refl}{\DC{refl}}
\newcommand{\Refl}{\DC{Refl}}
\newcommand{\leZ}{\DC{O_{\le}}}
\newcommand{\leS}{\DC{S_{\le}}}

0 comments on commit 20572cd

Please sign in to comment.