## Project Report for Logic, Types, Spaces 2019

### 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

1. Defining greatest elements and least elements.
2. Perhaps defining orders with more structure and proving theorems about them.
3. 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

1. I modified the definition of divisibility created by Sriram to allow divisibility to be defined only for non-zero natural numbers.
2. 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.
3. I have defined a recursive function type euclidRecursion that can be used to generate proofs of statements recursively using Euclid’s division algorithm.
4. Added proofs involving divisibility such as dividesAntiSymmetric, multipleDivides multipleDividesMultiple.
5. 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

1. Added basic proofs about the GCD such as gcdUnique and divImpliesGCDOne.
2. Added proofs used to generate the GCD recursively, and used the euclidRecursion function type to write euclidGCD which returns the GCD of two numbers.
3. 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)
4. 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

1. Added types isIrreducible and isPrime, and showed their equivalence with primeIsIrreducible and irreducibleIsPrime.
2. 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


AuthorDate: Mon Apr 22 12:22:45 2019 +0530
CommitDate: Mon Apr 22 12:22:45 2019 +0530

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

AuthorDate: Sat Apr 20 21:47:37 2019 +0530
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(-)

AuthorDate: Sat Apr 20 21:36:09 2019 +0530
CommitDate: Sat Apr 20 21:36:09 2019 +0530

more breaks fixed

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

commit 0b385fa5a59be21f5919299185fb33c29507623a
AuthorDate: Sat Apr 20 21:23:43 2019 +0530
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
AuthorDate: Sat Apr 20 21:13:25 2019 +0530
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
AuthorDate: Sat Apr 20 20:58:10 2019 +0530
CommitDate: Sat Apr 20 20:58:10 2019 +0530

Removed redundant definitions

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

commit 5da0d637a7a052f376898e4e4956c2827b7bfdce
AuthorDate: Sat Apr 20 20:00:53 2019 +0530
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
AuthorDate: Sat Apr 20 19:52:04 2019 +0530
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
AuthorDate: Sat Apr 20 19:44:24 2019 +0530
CommitDate: Sat Apr 20 19:44:24 2019 +0530

Changed 1 character, literally

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

AuthorDate: Sat Apr 20 18:57:12 2019 +0530
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
AuthorDate: Sat Apr 20 03:52:40 2019 +0530
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(+)

AuthorDate: Thu Apr 11 10:43:43 2019 +0530
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(-)

AuthorDate: Mon Apr 1 01:12:57 2019 +0530
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
AuthorDate: Tue Feb 26 11:52:59 2019 +0530
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
AuthorDate: Mon Feb 25 01:20:10 2019 +0530
CommitDate: Mon Feb 25 01:20:10 2019 +0530

minor change to report

1 file changed, 1 insertion(+), 1 deletion(-)

commit ca95d24091d62ebb8234b68fb201545802d2aa19
AuthorDate: Mon Feb 25 01:18:19 2019 +0530
CommitDate: Mon Feb 25 01:18:19 2019 +0530

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

commit 2024a1d453be04004733efe0d8d21aa9ba329f05
AuthorDate: Sun Feb 24 23:54:24 2019 +0530
CommitDate: Sun Feb 24 23:54:24 2019 +0530

minor changes

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

commit 26407399234d823f3dea035b318f07a5e33fa37b
AuthorDate: Sun Feb 24 23:05:25 2019 +0530
CommitDate: Sun Feb 24 23:05:25 2019 +0530

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

AuthorDate: Sun Feb 24 02:35:54 2019 +0530
CommitDate: Sun Feb 24 02:35:54 2019 +0530

Small correction

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

commit 02250c2cd0abefde9354431139c2ffc083045de7
AuthorDate: Sun Feb 24 02:32:54 2019 +0530
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
AuthorDate: Fri Feb 22 12:25:23 2019 +0530
CommitDate: Fri Feb 22 12:25:23 2019 +0530

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

commit 2731d4c73ac7568b5348c3542e8220430bd8bf0c
AuthorDate: Thu Feb 21 21:09:04 2019 +0530
CommitDate: Thu Feb 21 21:09:04 2019 +0530

More minor changes

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

commit f74ce2c03c10ca107bbf3a7a740ff972ce3e8958
AuthorDate: Thu Feb 21 21:04:10 2019 +0530
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
AuthorDate: Thu Feb 21 19:25:55 2019 +0530
CommitDate: Thu Feb 21 19:25:55 2019 +0530

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

commit edafff6583985e7571bcbe3cee1892aeba6d3673
AuthorDate: Thu Feb 21 18:38:17 2019 +0530
CommitDate: Thu Feb 21 18:38:17 2019 +0530

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

commit 5f9bce2c2ca2a045a3391e3904c97638629a3ffe
AuthorDate: Thu Feb 21 17:02:59 2019 +0530
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
AuthorDate: Thu Feb 21 12:55:18 2019 +0530
CommitDate: Thu Feb 21 12:55:18 2019 +0530

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

commit cb1cd18450e1ff7e8ff1c0ea2beeae6de676367b
AuthorDate: Thu Feb 21 12:50:29 2019 +0530
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
AuthorDate: Thu Feb 21 11:51:13 2019 +0530
CommitDate: Thu Feb 21 11:51:13 2019 +0530

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

commit 8b176c51867e7e133bbb2c387fd2ca80d8ed78ae
AuthorDate: Wed Feb 13 10:33:41 2019 +0530
CommitDate: Wed Feb 13 10:33:41 2019 +0530

small change

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

commit 6d43420e23df349993f7895d14b9790518bf98bd
AuthorDate: Wed Feb 13 10:30:02 2019 +0530
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
AuthorDate: Mon Feb 11 10:26:58 2019 +0530
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