## Project Report for Logic, Types, Spaces 2019

### 1. Quicksort function

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.

### 2. Mergesort

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.

### 3. Completing Quicksort

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

### Log of git commits by author


commit 61531e577c313975418f440bf9f6afe21a31ac81
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
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
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
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
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
AuthorDate: Thu Feb 21 22:05:44 2019 +0530
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
AuthorDate: Thu Feb 21 21:57:02 2019 +0530
Commit:     GitHub
CommitDate: Thu Feb 21 21:57:02 2019 +0530

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
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
AuthorDate: Tue Feb 5 16:28:21 2019 +0530
Commit:     GitHub
CommitDate: Tue Feb 5 16:28:21 2019 +0530

Code/Merge.idr | 112 +++++++++++++++++++++++++++++++++++++--------------------
1 file changed, 73 insertions(+), 39 deletions(-)