#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
Defined addition and multiplication over SimpQ using AddQ and multQ
#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.
commit b5abba879102b74b08e5358f2461ffbee63191ba
Author: rathivrunda <47008758+rathivrunda@users.noreply.github.com>
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
Author: rathivrunda <47008758+rathivrunda@users.noreply.github.com>
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(+)
commit 8256efad53e85df32b17d99402af49aece7e8131
Author: rathivrunda <47008758+rathivrunda@users.noreply.github.com>
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(-)
commit 77cdadbbff5c007cae36ca04de693837245ed314
Author: rathivrunda <47008758+rathivrunda@users.noreply.github.com>
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(-)
commit 69a6d22cf2df1ad9b83ba5efcc717ef3570268de
Author: rathivrunda <47008758+rathivrunda@users.noreply.github.com>
AuthorDate: Sun Apr 14 01:07:33 2019 +0530
Commit: GitHub
CommitDate: Sun Apr 14 01:07:33 2019 +0530
Update Rats.idr
added some functions for Rats
Code/Rats.idr | 61 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++---
1 file changed, 58 insertions(+), 3 deletions(-)
commit 707ce724246543572b04ac02c54a312323356d2e
Author: rathivrunda <47008758+rathivrunda@users.noreply.github.com>
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
Author: rathivrunda <47008758+rathivrunda@users.noreply.github.com>
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
Author: rathivrunda <47008758+rathivrunda@users.noreply.github.com>
AuthorDate: Fri Feb 15 19:04:36 2019 +0530
Commit: GitHub
CommitDate: Fri Feb 15 19:04:36 2019 +0530
Update Rationals.idr
added isFactorZZ
Code/Rationals.idr | 3 +++
1 file changed, 3 insertions(+)
commit d5451aace6ce7d34dd320e8f6d192cc54b0377db
Author: rathivrunda <47008758+rathivrunda@users.noreply.github.com>
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
Author: rathivrunda <47008758+rathivrunda@users.noreply.github.com>
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
Author: rathivrunda <47008758+rathivrunda@users.noreply.github.com>
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
Author: rathivrunda <47008758+rathivrunda@users.noreply.github.com>
AuthorDate: Fri Feb 15 18:56:59 2019 +0530
Commit: GitHub
CommitDate: Fri Feb 15 18:56:59 2019 +0530
Update Bezout.idr
Added a function to prove if p|a and p|b p|a+b
Code/Bezout.idr | 24 ++++++++++++++++++------
1 file changed, 18 insertions(+), 6 deletions(-)