MA 210: Logic, Types and Spaces

Project Report for Logic, Types, Spaces 2019

Adithya Upadhya

Outline of the work done

NatUtils

NatUtils.idr

I created the file NatUtils.idr and added proofs useful for working with naturals numbers in the file, such as proofs extending equality and order (as defined by the type LTE on Nat).

Possible issues

Currently, all the functions I have added to this file appear to be working.

Order

Order.idr

I created the file Order.idr to model orders. It currently includes types such as isReflexive, isAntiSymmetric, isTransitive, isPartialOrder, isTotalOrder.

Possible issues

I am not sure whether the type for well-ordering as I have stated it is useful.

To be done

Defining greatest elements and least elements.
Perhaps defining orders with more structure and proving theorems about them.
The sorting algorithms could perhaps use these types to sort lists.

NatOrder

NatOrder.idr

I created the file NatOrder.idr to implement the usual order on the naturals with the type LEQ, along with several proofs that are useful for working with them, such as cancellation laws and proofs to show that it is a total order. I have also put in functions: leqToLTE lneqToLT lteToLEQ ltToLNEQ to interconvert between them.

Possible issues

Currently, all the functions I have added to this file appear to be working.

Divisors

NatDivisors.idr

I modified the definition of divisibility created by Sriram to allow divisibility to be defined only for non-zero natural numbers.
I added an algorithm euclidDivide that given two natural numbers, returns the quotient and reminder under division with proof that they are the quotient and reminder. Rohit had added one previously, and I removed possible problems with it, with modifications to the algorithm.
I have defined a recursive function type euclidRecursion that can be used to generate proofs of statements recursively using Euclid’s division algorithm.
Added proofs involving divisibility such as dividesAntiSymmetric, multipleDivides multipleDividesMultiple.
Added the fuction decDivisible for the decidability of divisibility. Added helper functions for this including dividesImpliesGEQ and notDivisible.

Possible issues

Currently, all the functions I have added to this file appear to be working.

GCD

NatGCD.idr

Added basic proofs about the GCD such as gcdUnique and divImpliesGCDOne.
Added proofs used to generate the GCD recursively, and used the euclidRecursion function type to write euclidGCD which returns the GCD of two numbers.
Added another recursive function type euclidGCDExtend which canbe used to generate recursive proofs involving the GCD. (Most of this can probably done with Bezout’s lemma, but since I was working within the natural numbers, I wrote this)
Added functions gcdMult and coprimeImpliesDiv later used in Primes.

Possible issues

Currently, all the functions I have added to this file appear to be working. Extending this to Integers would allow some proofs to be easier.

Primes

NatPrimes.idr

Added types isIrreducible and isPrime, and showed their equivalence with primeIsIrreducible and irreducibleIsPrime.
Added a proof that if an irreducible either divides a number or is coprime to it, as irreducibleDividesOrCoprime. (These were intended as helper functions for the decidability of primality)

To be done

Decidability of primality. This will require a recursive function that searches for the smallest factor of a number. This is yet to be written.

Log of git commits by author


commit b7cd4b678330ad1028400187bfb66684505fa725
Author:     Adithya Upadhya <37117201+adithyaupadhya@users.noreply.github.com>
AuthorDate: Mon Apr 22 12:22:45 2019 +0530
Commit:     Adithya Upadhya <37117201+adithyaupadhya@users.noreply.github.com>
CommitDate: Mon Apr 22 12:22:45 2019 +0530

    Added report

 Code/NatPrimes.idr          | 28 +---------------------------
 _reports/adithya/adithya.md | 44 +++++++++++++++++++++++++++++---------------
 2 files changed, 30 insertions(+), 42 deletions(-)

commit 02523fd7d0c9bc60d530d420fad406e9e98f3dad
Author:     Adithya Upadhya <37117201+adithyaupadhya@users.noreply.github.com>
AuthorDate: Sat Apr 20 21:47:37 2019 +0530
Commit:     Adithya Upadhya <37117201+adithyaupadhya@users.noreply.github.com>
CommitDate: Sat Apr 20 21:47:37 2019 +0530

    I'm not sure what changed, but nothing seems to be broken

 Code/GCDZZ.idr | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

commit 5888e9ece95499ba617d4787edeca0ad84772c25
Author:     Adithya Upadhya <37117201+adithyaupadhya@users.noreply.github.com>
AuthorDate: Sat Apr 20 21:36:09 2019 +0530
Commit:     Adithya Upadhya <37117201+adithyaupadhya@users.noreply.github.com>
CommitDate: Sat Apr 20 21:36:09 2019 +0530

    more breaks fixed

 Code/NatUtils.idr | 5 +++++
 1 file changed, 5 insertions(+)

commit 0b385fa5a59be21f5919299185fb33c29507623a
Author:     Adithya Upadhya <37117201+adithyaupadhya@users.noreply.github.com>
AuthorDate: Sat Apr 20 21:23:43 2019 +0530
Commit:     Adithya Upadhya <37117201+adithyaupadhya@users.noreply.github.com>
CommitDate: Sat Apr 20 21:23:43 2019 +0530

    fixed more breaks

 Code/GCDZZ.idr | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

commit 22ff15dd42dc612d53cca9a4e673103fdb78d4d2
Author:     Adithya Upadhya <37117201+adithyaupadhya@users.noreply.github.com>
AuthorDate: Sat Apr 20 21:13:25 2019 +0530
Commit:     Adithya Upadhya <37117201+adithyaupadhya@users.noreply.github.com>
CommitDate: Sat Apr 20 21:13:25 2019 +0530

    Fixed more breaks

 Code/Divisors.idr | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

commit d8386f7a92b4e4ac8b764122ac030aee30c7d6ef
Author:     Adithya Upadhya <37117201+adithyaupadhya@users.noreply.github.com>
AuthorDate: Sat Apr 20 20:58:10 2019 +0530
Commit:     Adithya Upadhya <37117201+adithyaupadhya@users.noreply.github.com>
CommitDate: Sat Apr 20 20:58:10 2019 +0530

    Removed redundant definitions

 Code/gcd.idr | 16 ----------------
 1 file changed, 16 deletions(-)

commit 5da0d637a7a052f376898e4e4956c2827b7bfdce
Author:     Adithya Upadhya <37117201+adithyaupadhya@users.noreply.github.com>
AuthorDate: Sat Apr 20 20:00:53 2019 +0530
Commit:     Adithya Upadhya <37117201+adithyaupadhya@users.noreply.github.com>
CommitDate: Sat Apr 20 20:00:53 2019 +0530

    One more, because of random keyboard mash changes

 Code/ZZ.idr | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

commit 5ac2363d12bf11bf8b776ab768734987153e9b7f
Author:     Adithya Upadhya <37117201+adithyaupadhya@users.noreply.github.com>
AuthorDate: Sat Apr 20 19:52:04 2019 +0530
Commit:     Adithya Upadhya <37117201+adithyaupadhya@users.noreply.github.com>
CommitDate: Sat Apr 20 19:52:04 2019 +0530

    fixed some breaks

 Code/ZZ.idr | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

commit c22774f9b5ac92ca577897b0a5753584c75237db
Author:     Adithya Upadhya <37117201+adithyaupadhya@users.noreply.github.com>
AuthorDate: Sat Apr 20 19:44:24 2019 +0530
Commit:     Adithya Upadhya <37117201+adithyaupadhya@users.noreply.github.com>
CommitDate: Sat Apr 20 19:44:24 2019 +0530

    Changed 1 character, literally

 Code/NatUtils.idr | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

commit 64ea83ac17f772166bc5768491ad4593c4e8733d
Author:     Adithya Upadhya <37117201+adithyaupadhya@users.noreply.github.com>
AuthorDate: Sat Apr 20 18:57:12 2019 +0530
Commit:     Adithya Upadhya <37117201+adithyaupadhya@users.noreply.github.com>
CommitDate: Sat Apr 20 18:57:12 2019 +0530

    Added final copies of changes, deleted temporary files

 Code/Divisors.idr                                |   2 +-
 Code/InductiveTypes.idr                          |  36 +++
 Code/{sandboxNatDivisors.idr => NatDivisors.idr} |  84 +++---
 Code/{sandboxGCD.idr => NatGCD.idr}              |  21 +-
 Code/NatOrder.idr                                | 121 ++++++---
 Code/{sandboxPrime.idr => NatPrimes.idr}         |  58 ++++-
 Code/NatUtils.idr                                | 182 +++++++++----
 Code/sandboxNatOrder.idr                         | 316 -----------------------
 Code/sandboxNatUtils.idr                         | 200 --------------
 Code/sandboxOrder.idr                            | 122 ---------
 10 files changed, 350 insertions(+), 792 deletions(-)

commit 668fa3e3586cdf0104d4b682d5fdd85a20efa69c
Author:     Adithya Upadhya <37117201+adithyaupadhya@users.noreply.github.com>
AuthorDate: Sat Apr 20 03:52:40 2019 +0530
Commit:     Adithya Upadhya <37117201+adithyaupadhya@users.noreply.github.com>
CommitDate: Sat Apr 20 03:52:40 2019 +0530

    Temporarily added files to ensure I don't lose all my work

 Code/sandboxGCD.idr         | 222 +++++++++++++++++++++++++++++++
 Code/sandboxNatDivisors.idr | 251 +++++++++++++++++++++++++++++++++++
 Code/sandboxNatOrder.idr    | 316 ++++++++++++++++++++++++++++++++++++++++++++
 Code/sandboxNatUtils.idr    | 200 ++++++++++++++++++++++++++++
 Code/sandboxOrder.idr       | 122 +++++++++++++++++
 Code/sandboxPrime.idr       |  98 ++++++++++++++
 6 files changed, 1209 insertions(+)

commit d9b8bc6e0ade0ccbdb7a2108a122faa24fc4c04f
Author:     Adithya Upadhya <37117201+adithyaupadhya@users.noreply.github.com>
AuthorDate: Thu Apr 11 10:43:43 2019 +0530
Commit:     Adithya Upadhya <37117201+adithyaupadhya@users.noreply.github.com>
CommitDate: Thu Apr 11 10:43:43 2019 +0530

    Made gcd total, fixed breaking of code in Primes

 Code/Primes.idr | 11 ++++-------
 Code/gcd.idr    | 20 +++++++++++---------
 2 files changed, 15 insertions(+), 16 deletions(-)

commit 1bbbcaa25846ab900fbcdca3ceceafaad40318a2
Author:     Adithya Upadhya <37117201+adithyaupadhya@users.noreply.github.com>
AuthorDate: Mon Apr 1 01:12:57 2019 +0530
Commit:     Adithya Upadhya <37117201+adithyaupadhya@users.noreply.github.com>
CommitDate: Mon Apr 1 01:12:57 2019 +0530

    Completed GCD with proof

 Code/GCDZZ.idr    |   3 +-
 Code/NatOrder.idr |  60 +++++++++++++++++++++++++------
 Code/NatUtils.idr |  44 +++++++++++++++++------
 Code/Primes.idr   |   2 +-
 Code/decDivZ.idr  |   2 +-
 Code/gcd.idr      | 106 ++++++++++++++++++++++++++++++++++++++++++++++--------
 6 files changed, 178 insertions(+), 39 deletions(-)

commit 10cb35bccf7766f925c9c00813b6837fa4d7abf0
Author:     Adithya Upadhya <37117201+adithyaupadhya@users.noreply.github.com>
AuthorDate: Tue Feb 26 11:52:59 2019 +0530
Commit:     Adithya Upadhya <37117201+adithyaupadhya@users.noreply.github.com>
CommitDate: Tue Feb 26 11:52:59 2019 +0530

    Minor correction to NatOrder.idr

 Code/NatOrder.idr | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

commit 8878b26f73c90ec209d93c690020b3e8eb80de56
Author:     Adithya Upadhya <37117201+adithyaupadhya@users.noreply.github.com>
AuthorDate: Mon Feb 25 01:20:10 2019 +0530
Commit:     Adithya Upadhya <37117201+adithyaupadhya@users.noreply.github.com>
CommitDate: Mon Feb 25 01:20:10 2019 +0530

    minor change to report

 _reports/adithya/adithya.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

commit ca95d24091d62ebb8234b68fb201545802d2aa19
Author:     Adithya Upadhya <37117201+adithyaupadhya@users.noreply.github.com>
AuthorDate: Mon Feb 25 01:18:19 2019 +0530
Commit:     Adithya Upadhya <37117201+adithyaupadhya@users.noreply.github.com>
CommitDate: Mon Feb 25 01:18:19 2019 +0530

    added report

 Code/NatOrder.idr           |  3 +++
 _reports/adithya/adithya.md | 44 +++++++++++++++++++++++++++++++++++++++-----
 2 files changed, 42 insertions(+), 5 deletions(-)

commit 2024a1d453be04004733efe0d8d21aa9ba329f05
Author:     Adithya Upadhya <37117201+adithyaupadhya@users.noreply.github.com>
AuthorDate: Sun Feb 24 23:54:24 2019 +0530
Commit:     Adithya Upadhya <37117201+adithyaupadhya@users.noreply.github.com>
CommitDate: Sun Feb 24 23:54:24 2019 +0530

    minor changes

 Code/NatUtils.idr           |  1 -
 _reports/adithya/adithya.md | 16 ++++++++++++++--
 2 files changed, 14 insertions(+), 3 deletions(-)

commit 26407399234d823f3dea035b318f07a5e33fa37b
Author:     Adithya Upadhya <37117201+adithyaupadhya@users.noreply.github.com>
AuthorDate: Sun Feb 24 23:05:25 2019 +0530
Commit:     Adithya Upadhya <37117201+adithyaupadhya@users.noreply.github.com>
CommitDate: Sun Feb 24 23:05:25 2019 +0530

    Added proofs about order

 Code/NatOrder.idr |  20 +++++++++++
 Code/NatUtils.idr |  24 +++++++++++--
 Code/Order.idr    | 100 ++++++++++++++++++++++++++++++++++++++++++++++++++----
 3 files changed, 135 insertions(+), 9 deletions(-)

commit 6c266f22c331efb44035e754b4adea1fe18b1756
Author:     Adithya Upadhya <37117201+adithyaupadhya@users.noreply.github.com>
AuthorDate: Sun Feb 24 02:35:54 2019 +0530
Commit:     Adithya Upadhya <37117201+adithyaupadhya@users.noreply.github.com>
CommitDate: Sun Feb 24 02:35:54 2019 +0530

    Small correction

 Code/NatOrder.idr | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

commit 02250c2cd0abefde9354431139c2ffc083045de7
Author:     Adithya Upadhya <37117201+adithyaupadhya@users.noreply.github.com>
AuthorDate: Sun Feb 24 02:32:54 2019 +0530
Commit:     Adithya Upadhya <37117201+adithyaupadhya@users.noreply.github.com>
CommitDate: Sun Feb 24 02:32:54 2019 +0530

    Added functions to NatUtils.idr and NatOrder.idr

 Code/NatOrder.idr | 118 ++++++++++++++++++++++++++++++++++++++++++------------
 Code/NatUtils.idr |  64 ++++++++++++++++++++---------
 2 files changed, 137 insertions(+), 45 deletions(-)

commit 49e9fb7a87f02dcc6d021e125d8a3293c4431a63
Author:     Adithya Upadhya <37117201+adithyaupadhya@users.noreply.github.com>
AuthorDate: Fri Feb 22 12:25:23 2019 +0530
Commit:     Adithya Upadhya <37117201+adithyaupadhya@users.noreply.github.com>
CommitDate: Fri Feb 22 12:25:23 2019 +0530

    Added new order to Nat

 Code/NatOrder.idr | 139 ++++++++++++++++++++++++++++++++++++++++++++++++++++++
 Code/NatUtils.idr |  15 +++---
 2 files changed, 146 insertions(+), 8 deletions(-)

commit 2731d4c73ac7568b5348c3542e8220430bd8bf0c
Author:     Adithya Upadhya <37117201+adithyaupadhya@users.noreply.github.com>
AuthorDate: Thu Feb 21 21:09:04 2019 +0530
Commit:     Adithya Upadhya <37117201+adithyaupadhya@users.noreply.github.com>
CommitDate: Thu Feb 21 21:09:04 2019 +0530

    More minor changes

 Code/gcd.idr | 12 ++++++++++++
 1 file changed, 12 insertions(+)

commit f74ce2c03c10ca107bbf3a7a740ff972ce3e8958
Author:     Adithya Upadhya <37117201+adithyaupadhya@users.noreply.github.com>
AuthorDate: Thu Feb 21 21:04:10 2019 +0530
Commit:     Adithya Upadhya <37117201+adithyaupadhya@users.noreply.github.com>
CommitDate: Thu Feb 21 21:04:10 2019 +0530

    Changes to fix broken dependencies that were my fault.

 Code/NatUtils.idr | 27 +++++++++++++++------------
 Code/ZZ.idr       |  6 +++---
 Code/gcd.idr      |  3 +++
 3 files changed, 21 insertions(+), 15 deletions(-)

commit 284bdfe3784c30a89243125b02bc738691c70cc3
Author:     Adithya Upadhya <37117201+adithyaupadhya@users.noreply.github.com>
AuthorDate: Thu Feb 21 19:25:55 2019 +0530
Commit:     Adithya Upadhya <37117201+adithyaupadhya@users.noreply.github.com>
CommitDate: Thu Feb 21 19:25:55 2019 +0530

    Added more functions to NatUtils.idr

 Code/NatUtils.idr | 112 ++++++++++++++++++++++++++++++------------------------
 1 file changed, 63 insertions(+), 49 deletions(-)

commit edafff6583985e7571bcbe3cee1892aeba6d3673
Author:     Adithya Upadhya <37117201+adithyaupadhya@users.noreply.github.com>
AuthorDate: Thu Feb 21 18:38:17 2019 +0530
Commit:     Adithya Upadhya <37117201+adithyaupadhya@users.noreply.github.com>
CommitDate: Thu Feb 21 18:38:17 2019 +0530

    changed proof for lteAddConstant

 Code/NatUtils.idr | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

commit 5f9bce2c2ca2a045a3391e3904c97638629a3ffe
Author:     Adithya Upadhya <37117201+adithyaupadhya@users.noreply.github.com>
AuthorDate: Thu Feb 21 17:02:59 2019 +0530
Commit:     Adithya Upadhya <37117201+adithyaupadhya@users.noreply.github.com>
CommitDate: Thu Feb 21 17:02:59 2019 +0530

    Corrected errors due to change in function names

 Code/NatUtils.idr | 15 +++++++--------
 Code/gcd.idr      | 11 +++++++++--
 2 files changed, 16 insertions(+), 10 deletions(-)

commit aea6b6dbc47651939d42784a2d2f180d2153dc27
Author:     Adithya Upadhya <37117201+adithyaupadhya@users.noreply.github.com>
AuthorDate: Thu Feb 21 12:55:18 2019 +0530
Commit:     Adithya Upadhya <37117201+adithyaupadhya@users.noreply.github.com>
CommitDate: Thu Feb 21 12:55:18 2019 +0530

    Added types to model Orders.

 Code/Order.idr | 34 ++++++++++++++++++++++++++++++++++
 1 file changed, 34 insertions(+)

commit cb1cd18450e1ff7e8ff1c0ea2beeae6de676367b
Author:     Adithya Upadhya <37117201+adithyaupadhya@users.noreply.github.com>
AuthorDate: Thu Feb 21 12:50:29 2019 +0530
Commit:     Adithya Upadhya <37117201+adithyaupadhya@users.noreply.github.com>
CommitDate: Thu Feb 21 12:50:29 2019 +0530

    Added functions to Natutils and modified definitions of divisibility in gcd. Cleaned up both files.

 Code/NatUtils.idr | 171 ++++++++++++++++++++++++++++++++++++------------------
 Code/gcd.idr      | 149 ++++++++++++++++++++---------------------------
 sandbox.idr       | 159 --------------------------------------------------
 sandbox1.idr      |  34 -----------
 sandbox2.idr      |  48 ---------------
 5 files changed, 178 insertions(+), 383 deletions(-)

commit af2501a8aac1a17c32f1aba4e7fac21912c8441d
Author:     Adithya Upadhya <37117201+adithyaupadhya@users.noreply.github.com>
AuthorDate: Thu Feb 21 11:51:13 2019 +0530
Commit:     Adithya Upadhya <37117201+adithyaupadhya@users.noreply.github.com>
CommitDate: Thu Feb 21 11:51:13 2019 +0530

    Temporary additions

 sandbox.idr  | 159 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 sandbox1.idr |  34 +++++++++++++
 sandbox2.idr |  48 ++++++++++++++++++
 3 files changed, 241 insertions(+)

commit 8b176c51867e7e133bbb2c387fd2ca80d8ed78ae
Author:     Adithya Upadhya <37117201+adithyaupadhya@users.noreply.github.com>
AuthorDate: Wed Feb 13 10:33:41 2019 +0530
Commit:     Adithya Upadhya <37117201+adithyaupadhya@users.noreply.github.com>
CommitDate: Wed Feb 13 10:33:41 2019 +0530

    small change

 Code/Bezout.idr | 1 -
 1 file changed, 1 deletion(-)

commit 6d43420e23df349993f7895d14b9790518bf98bd
Author:     Adithya Upadhya <37117201+adithyaupadhya@users.noreply.github.com>
AuthorDate: Wed Feb 13 10:30:02 2019 +0530
Commit:     Adithya Upadhya <37117201+adithyaupadhya@users.noreply.github.com>
CommitDate: Wed Feb 13 10:30:02 2019 +0530

    Wrote in division algorithm with proof

 Code/Bezout.idr   | 61 -------------------------------------------------------
 Code/NatUtils.idr |  8 ++++++++
 Code/gcd.idr      | 14 ++++++++++++-
 3 files changed, 21 insertions(+), 62 deletions(-)

commit 5685ce5964efeab8f358c470669c204c7c5a82d5
Author:     Adithya Upadhya <37117201+adithyaupadhya@users.noreply.github.com>
AuthorDate: Mon Feb 11 10:26:58 2019 +0530
Commit:     Adithya Upadhya <37117201+adithyaupadhya@users.noreply.github.com>
CommitDate: Mon Feb 11 10:26:58 2019 +0530

    Renamed Tools.idr to NatUtils.idr

 Code/NatUtils.idr | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)

commit de7bcecfff1137ef62b3361f4e90350d9698b209
Author:     Adithya Upadhya <37117201+adithyaupadhya@users.noreply.github.com>
AuthorDate: Sun Feb 10 22:08:11 2019 +0530
Commit:     Adithya Upadhya <37117201+adithyaupadhya@users.noreply.github.com>
CommitDate: Sun Feb 10 22:08:11 2019 +0530

    Added Tools file

 Code/Tools.idr | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)

Project Report for Logic, Types, Spaces 2019

Adithya Upadhya

Outline of the work done

NatUtils

Possible issues

Order

Possible issues

To be done

NatOrder

Possible issues

Divisors

Possible issues

GCD

Possible issues

Primes

To be done

Log of git commits by author

Department of Mathematics, Indian Institute of Science.