## Project Report for Logic, Types, Spaces 2019

### Outline of the work done

#Q.idr Defined the data type SimpQ as a transversal group for Rationals, where each element of the type contains the proof that the numerator and denominator are coprime. The proof was included using Erasure and when implemented correctly (which I could not manage to do) will not require equality of proofs, when proving equality.

Made functions to take any Rational number Q to its simplified form SimpQ.

Defined addition, multiplication over Q. Proved that zero is the additive identity and one is the multiplicative identity in the form pre-defined in Monoids.idr. Proved commutativity of addition and multiplication over Q

#Rats.idr Defined addition, multiplication and the equality function for the data type Rats defined in class, as a better definition for the field of Rational numbers as all the deinitions in Field.idr require the proof to be within the type.

Abandoned this definition later, as it required the equality of proofs at every stage which is very cumbersome.

#Rationals.idr Defined the type isFactorZZ (Was later deleted as an identical type isDivisibleZ was created in Divisors.idr and was used more frequently)

#ZZUtils.idr

Defined auxillary functions required to prove stuff in Q.idr, Rationals.idr etc.

#bezout.idr

 proved that if p a and p b , p (a+b).

#NatUtils.idr

proved auxillary functions to be used in bezout.idr

Please fill in this with references to code.

### Log of git commits by author


commit b5abba879102b74b08e5358f2461ffbee63191ba
AuthorDate: Sat Apr 20 19:42:05 2019 +0530
Commit:     GitHub
CommitDate: Sat Apr 20 19:42:05 2019 +0530

Update rathivrunda.md

_reports/rathivrunda/rathivrunda.md | 43 +++++++++++++++++++++++++++++++++++++
1 file changed, 43 insertions(+)

commit 9ecb7c63c57113cde59e5af1ccfa44db5bd7fb7f
AuthorDate: Wed Apr 17 00:32:09 2019 +0530
Commit:     GitHub
CommitDate: Wed Apr 17 00:32:09 2019 +0530

Update ZZUtils.idr

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

AuthorDate: Wed Apr 17 00:27:22 2019 +0530
Commit:     GitHub
CommitDate: Wed Apr 17 00:27:22 2019 +0530

Update Q.idr

Defined a transversal type as the simplified form of a Rational no. using erasure

Code/Q.idr | 79 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++----
1 file changed, 74 insertions(+), 5 deletions(-)

AuthorDate: Sun Apr 14 16:39:15 2019 +0530
Commit:     GitHub
CommitDate: Sun Apr 14 16:39:15 2019 +0530

Update Q.idr

Added functions to prove identity and commutativity

Code/Q.idr | 94 ++++++++++++++++++++++++++++++++++++++++++++++++++++----------
1 file changed, 80 insertions(+), 14 deletions(-)

AuthorDate: Sun Apr 14 01:07:33 2019 +0530
Commit:     GitHub
CommitDate: Sun Apr 14 01:07:33 2019 +0530

Update Rats.idr

Code/Rats.idr | 61 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++---
1 file changed, 58 insertions(+), 3 deletions(-)

commit 707ce724246543572b04ac02c54a312323356d2e
AuthorDate: Fri Feb 15 19:41:02 2019 +0530
Commit:     GitHub
CommitDate: Fri Feb 15 19:41:02 2019 +0530

Update NatUtils.idr

imported ZZ as per Shahfils suggestion

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

commit fb01ac1a599286747f392719aa1452590d170026
AuthorDate: Fri Feb 15 19:16:55 2019 +0530
Commit:     GitHub
CommitDate: Fri Feb 15 19:16:55 2019 +0530

Update Rationals.idr

had an error in the last commit

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

commit 913c35e473ee0809bd1e376a9ab35ef29dc068a1
AuthorDate: Fri Feb 15 19:04:36 2019 +0530
Commit:     GitHub
CommitDate: Fri Feb 15 19:04:36 2019 +0530

Update Rationals.idr

Code/Rationals.idr | 3 +++
1 file changed, 3 insertions(+)

commit d5451aace6ce7d34dd320e8f6d192cc54b0377db
AuthorDate: Fri Feb 15 19:02:53 2019 +0530
Commit:     GitHub
CommitDate: Fri Feb 15 19:02:53 2019 +0530

Update Bezout.idr

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

commit 3f68bf6d5cf2067da809c1a10a17ca0e7810a750
AuthorDate: Fri Feb 15 19:01:39 2019 +0530
Commit:     GitHub
CommitDate: Fri Feb 15 19:01:39 2019 +0530

Update Bezout.idr

Code/Bezout.idr | 1 +
1 file changed, 1 insertion(+)

commit 881c4f993bce6ccd6bac605aa70a4c058566ae74
AuthorDate: Fri Feb 15 18:59:10 2019 +0530
Commit:     GitHub
CommitDate: Fri Feb 15 18:59:10 2019 +0530

Update NatUtils.idr

auxillary proofs required for the equality type

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

commit 81fc050558d73ac378d8228847aeb3ef6a2173b7