I created a function (**partitionVect**) that accepts a pivot and a vector and partitions the vector into two vectors according to whether the elements are smaller than or larger than the pivot, and returns the lengths of the parts as well as a proof that the sum of their lengths is equal to the length of the original vector.

Shafil had written an incomplete code that had a merge function to merge to sorted vectors into one sorted vector. I completed the code by creating a mergesort function. The work I did for this is :

- I created two functions that partition a Vector into two parts, the parts being equal if the length of the vector is even (
**halfVectEven**), and the parts being unequal if the length of the vector is odd (**halfVectOdd**). - I created a mergesort function that splits cases on whether the length of the Vector is Even or Odd, partitions it by the two functions I created earlier, and then applies mergesort recursively to both the parts.

This mergesort function was not total however, because the **Vecttake** function that Shafil defined was not total. So I made it total by adding a condition that the length of the Vector that we take is LTE the length of the original Vector. To make the rest of the auxiliary functions total, I had to prove a lot of lemmas and Theorems (eg : **nLTESn**,**halfnLTEn**, etc.). However, I was unable to make the proof that if (a = b), then (a is LTE b) total.

I also started working on proving that the result of the mergesort function is sorted. For this, I thought of the following strategy :

- First, prove that the merge (
**merge1**) function returns a sorted Vector. For this, I proved the auxiliary theorem that if I have a sorted Vector, v, and an element, x, which is LTE the first element of v, then the vector (x :: v) is also sorted. - Use the auxiliary theorem to construct a recursive prove that merge1 returns a sorted Vector.
- Use this to Prove that mergesort returns a sorted Vector.

*I provided a quicksort function (for Lists) that sorts and also provides a proof that the output List is sorted and is a permutation of the input List.
*I started by creating types for a Preorder and a Totalorder.
*Then I created a type (**ForAll**) that acts as a proposition that all the elements of a list satisfy some property p. I proved some theorems on this property (eg. mapping a list to another preserves the forall property, concatenation preserves it etc.)
*I defined a LTE type for length of lists just like LTE for nat. I proved a few simple lemmas on this lte property of lists (**lemma1**, **lemma2** and **lemma3**). * I created types for a sorted list and permutation of a list. I proved theorems on permutation

- I created a partition function (
**partitionFunc**) that partitions the list and gives proof that the concatenation of the parts is a permutation of the original list. - I created a partition function (
**ordPartition**) that partitions based on a total order and gives a proof that the elements in the two parts are ordered according to the pivot - Finally, I created an auxiliary function that will help perform quicksort and give proofs that the output is sorted according to the totatl order and that it is a permutation of the input.
- I also gave an example for quicksort of natural numbers.

```
commit 61531e577c313975418f440bf9f6afe21a31ac81
Author: NabarunDeka <37304450+NabarunDeka@users.noreply.github.com>
AuthorDate: Mon Apr 22 13:51:05 2019 +0530
Commit: GitHub
```
CommitDate: Mon Apr 22 13:51:05 2019 +0530
Updated report file
_reports/nabarun/nabarun.md | 12 ++++++++++++
1 file changed, 12 insertions(+)
commit 79eb67bf335758eb5531ae233e8e15ed4744e3af
Author: NabarunDeka <37304450+NabarunDeka@users.noreply.github.com>
AuthorDate: Mon Apr 22 11:20:08 2019 +0530
Commit: GitHub
CommitDate: Mon Apr 22 11:20:08 2019 +0530
Updated quicksort
Code/Quicksort.idr | 131 ++++++++++++++++++++++++++++++++++++++++++++++++-----
1 file changed, 120 insertions(+), 11 deletions(-)
commit 42d3e728d6377521e17a8b84199638ba35d831cc
Author: NabarunDeka <37304450+NabarunDeka@users.noreply.github.com>
AuthorDate: Thu Apr 18 18:59:48 2019 +0530
Commit: GitHub
CommitDate: Thu Apr 18 18:59:48 2019 +0530
Updated Quicksort
Code/Quicksort.idr | 77 ++++++++++++++++++++++++++++++++++++++++++++++++++----
1 file changed, 72 insertions(+), 5 deletions(-)
commit 8947e9eaf17acafcc833a9d51418d97d1a1d803b
Author: NabarunDeka <37304450+NabarunDeka@users.noreply.github.com>
AuthorDate: Mon Feb 25 01:26:18 2019 +0530
Commit: GitHub
CommitDate: Mon Feb 25 01:26:18 2019 +0530
Update my reports file
_reports/nabarun/nabarun.md | 29 +++++++++++++++++++++++------
1 file changed, 23 insertions(+), 6 deletions(-)
commit b59712d9b12ff73fe21e5ed1abf0debb78ac8000
Author: NabarunDeka <37304450+NabarunDeka@users.noreply.github.com>
AuthorDate: Mon Feb 25 01:25:03 2019 +0530
Commit: GitHub
CommitDate: Mon Feb 25 01:25:03 2019 +0530
started work on proving that mergesort returns a sorted vector
Code/Merge.idr | 34 +++++++++++++++++++++++++++++++++-
1 file changed, 33 insertions(+), 1 deletion(-)
commit 4b9089bd6eb2b5b17778f70ba189d966ef19beba
Author: NabarunDeka <37304450+NabarunDeka@users.noreply.github.com>
AuthorDate: Thu Feb 21 22:05:44 2019 +0530
Commit: NabarunDeka <37304450+NabarunDeka@users.noreply.github.com>
CommitDate: Thu Feb 21 22:05:44 2019 +0530
Update Merge.idr
Code/Merge.idr | 168 +++++++++++++++++++++++++++++++++++++++++----------------
1 file changed, 121 insertions(+), 47 deletions(-)
commit d2ddda7c3ba5db45fe0cde6d37192c57160bf0a0
Author: NabarunDeka <37304450+NabarunDeka@users.noreply.github.com>
AuthorDate: Thu Feb 21 21:57:02 2019 +0530
Commit: GitHub
CommitDate: Thu Feb 21 21:57:02 2019 +0530
made mergesort almost total.
the proof that (a = b) implies a is LTE b for all natural nos. a,b is not total.
Code/Merge.idr | 146 +++++++++++++++++++++++++++++++++++++++++++--------------
1 file changed, 110 insertions(+), 36 deletions(-)
commit a844527d9bec49923ec52c1d4e19e4b448bebf8c
Author: NabarunDeka <37304450+NabarunDeka@users.noreply.github.com>
AuthorDate: Mon Feb 11 22:02:39 2019 +0530
Commit: GitHub
CommitDate: Mon Feb 11 22:02:39 2019 +0530
created file Quicksort with a partition function
Code/Quicksort.idr | 13 +++++++++++++
1 file changed, 13 insertions(+)
commit 8171d1e58823ab87631c5acf5b0b773b21038f44
Author: NabarunDeka <37304450+NabarunDeka@users.noreply.github.com>
AuthorDate: Tue Feb 5 16:28:21 2019 +0530
Commit: GitHub
CommitDate: Tue Feb 5 16:28:21 2019 +0530
Add files via upload
Code/Merge.idr | 112 +++++++++++++++++++++++++++++++++++++--------------------
1 file changed, 73 insertions(+), 39 deletions(-)
commit 82c90fbff5e534addcc23a81a560f0781a5be349
Author: NabarunDeka <37304450+NabarunDeka@users.noreply.github.com>
AuthorDate: Thu Jan 24 11:48:43 2019 +0530
Commit: GitHub
CommitDate: Thu Jan 24 11:48:43 2019 +0530
Add files via upload
Code/gcd.idr | 20 ++++++++++++++++++++
1 file changed, 20 insertions(+)