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

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).

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).

Submission

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)