Project Report for Logic, Types, Spaces 2019

Nabarun Deka

Outline of the work done

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 :

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 :

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

Log of git commits by author


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(+)