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 *myusername@iisc.ac.in*, begin the idris file with the following.

```
module Myusername.Odds
import Evens
import Intro
```

- Define an inductive type family
`IsOdd : Nat -> Type`

such that`IsOdd n`

is inhabited if and only if`n`

is odd. - Show that
`$3$`

is odd. - Show that
`$2$`

is not odd. - Show that if
`n: Nat`

is odd, then its successor`S n`

is even. - Show that if
`n: Nat`

is even, then its successor`S n`

is odd. - Show that every number
`n : Nat`

is either even or odd. - Show that no number
`n: Nat`

is both even and odd. - Show that if
`n: Nat`

and`m: Nat`

are odd, then`add n m`

is even (here add is from the intro). - Show that if
`n: Nat`

is odd, then there exists`m: Nat`

such that`n = S (double m)`

.

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

- defining appropriate
`rec`

and`induc`

functions by pattern matching in*Idris* - after that, only using these, not direct pattern matching

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,

- create a file with this code with filename
*[YourName]AssRecRule.idr*, e.g.*MickeyMouseAssRecRule.idr* - fill in all the definitions, with pattern matching used to define
`recList`

and`inducFin`

, but pattern matching for`List`

and`Fin`

not used after that (you can use pattern matching for vectors while defining`fetchElem`

). - e-mail the solution as a single file (with no dependencies) with subject
*LTS2019 Assignment 2*by the due date.

```
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
list,
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)
```