Please e-mail your assignments to with "LTS2019" in the subject. The submissions will be added to the repository the day after the due date, and no late submissions will be accepted.

Odds and Evens

Due date: Thu, 24 Jan 2019

All problems should be solved in an Idris file which should be in a folder including the files Intro.idr and Evens.idr from the course. If your user name is, begin the idris file with the following.

module Myusername.Odds

import Evens

import Intro

  1. Define an inductive type family IsOdd : Nat -> Type such that IsOdd n is inhabited if and only if n is odd.
  2. Show that $3$ is odd.
  3. Show that $2$ is not odd.
  4. Show that if n: Nat is odd, then its successor S n is even.
  5. Show that if n: Nat is even, then its successor S n is odd.
  6. Show that every number n : Nat is either even or odd.
  7. Show that no number n: Nat is both even and odd.
  8. Show that if n: Nat and m: Nat are odd, then add n m is even (here add is from the intro).
  9. Show that if n: Nat is odd, then there exists m: Nat such that n = S (double m).

Recursion rules

Due date: Wed, 03 Apr 2019

In this assignment, you will work out some cases of using recursion and induction (including for indexed types) by:

The motivation for this is that rec and induc are cleanly defined, and any code in terms of these is correct (i.e., valid - it can of course still give the wrong results).


Below is skeleton code for the assignment, also available on the repository. To submit the assignment,

module AssRecRule

import Data.Fin
import Data.Vect

 The recursion function for lists of type `a`. Define this by pattern matching
recList : (a: Type) ->  (x: Type) -> x -> (a -> List a -> x -> x) -> (List a -> x)

Given a list of type `a` and a function `f: a -> b` get a list of type `b`
by applying `f` to each element.
Note: Define using `recList` and without pattern matching on lists.
mapList : (a: Type) -> (b: Type) -> (f: a -> b) -> List a -> List b

Given a list of type `a`, an initial value `init: a` and an operation `op: a -> a -> a`,
get an element of `a` by starting with init and repeatedly applying the elements of the
e.g. fold Nat 1 (*) ([22] :: [3] :: [])  = 1 * 22 * 3
Note: Define using `recList` and without pattern matching on lists.
foldList : (a: Type) ->  (init: a) -> (op : a -> a -> a) -> List a -> a

The induction function on the `Fin` indexed type family. Define this by pattern matching.
inducFin : (xs : (n: Nat) -> Fin n -> Type) ->
  (base : (m: Nat) -> xs (S m) FZ) ->
  (step : (p: Nat) -> (k: Fin p) ->  (prev: xs p k) -> (xs (S p) (FS k))) ->
  (q: Nat) -> (j: Fin q) -> xs q j

Given a type `a`, a natural number `q`, an element `j : Fin q` and a vector `v` of length q with entries of type `a`,
get the element in position `j` of `v`. Note that this is always well defined.

Note: Define using `inducList` and without pattern matching on the `Fin` family. You may pattern match on Vectors.
The definition should have only one case, and there should be no case splitting on `Fin`.
fetchElem : (a: Type) -> (q: Nat) -> (j: Fin q) -> (Vect q a -> a)