Project Report for Logic, Types, Spaces 2019

Rohit Kumar

Outline of the work done

Algebra :

Added the definitions of :-

1. An Intergal Domains
2. An Euclidean Norm over an Integral Domain
3. An Euclidean Domain

Added a file called Module.idr and added

1. The definitions of the types for distributivity of the action of the ring on the module
2. Added the definition for the IsLeftModule type
3. Added functions to recover the individual Distributivity types from the IsLeftModule type.
4. Added functions to recover the zero of the module from the IsLeftModule type
5. Proved that r.0 = 0 (Action of any ring element on zero is zero)
6. Proved that 0.m = 0 (Action of zero of the ring on any element is zero)

Number Theory :

1. Provided a partial proof of Euclid’s Division Lemma (Existence of Quotient and Remainders when we divide a natural number by another), which was later improved upon by other people. (This also had 5 auxiliary proofs, which include Trichotomy of the order on integers and Anti-symmetry of LTE)
2. Provided the definitions of a Common Factor Type and a GCD Type. (I did not prove that such a GCD would be unique)
3. Proved the following facts about the GCD (This had about 4 auxiliary proofs): (Which was also later improved upon by other people)
   1. If d is a GCD of a and b, then d is also a GCD of a + b and b.
   2. If d is a GCD of a + b and b, then d is also a GCD of a and b.
   3. If d is a GCD of a and b, then d is also a GCD of b and a.

Log of git commits by author

commit e5b8b2db46834ed2328c1085d65485c507968b49
Author:     rohit3499 <47004225+rohit3499@users.noreply.github.com>
AuthorDate: Mon Apr 22 11:54:13 2019 +0530
Commit:     GitHub 
CommitDate: Mon Apr 22 11:54:13 2019 +0530

    Updated Report
    
    Added my contributions after the midsems.

 _reports/rohit/rohit.md | 7 +++++++
 1 file changed, 7 insertions(+)

commit e25deca402b42d13d639be174cd1de7f635b380f
Author:     rohit3499 <47004225+rohit3499@users.noreply.github.com>
AuthorDate: Thu Apr 18 16:33:16 2019 +0530
Commit:     GitHub 
CommitDate: Thu Apr 18 16:33:16 2019 +0530

    Added a more general function extending equality
    
    Now the function can map one type to a different type, instead of the same type

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

commit 4acf1f296eac60ce36b79a2e8f68b6629c327055
Author:     rohit3499 <47004225+rohit3499@users.noreply.github.com>
AuthorDate: Thu Apr 18 16:29:27 2019 +0530
Commit:     GitHub 
CommitDate: Thu Apr 18 16:29:27 2019 +0530

    Created File Module.idr with definitions and some properties
    
    Created the IsLeftModule type and proved some basic properties like r*0 = 0 and 0*m = 0.

 Code/Module.idr | 135 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 135 insertions(+)

commit 86fdf1a3c136695ea4336bfdebe980f86138c104
Author:     rohit3499 <47004225+rohit3499@users.noreply.github.com>
AuthorDate: Mon Feb 25 01:45:48 2019 +0530
Commit:     GitHub 
CommitDate: Mon Feb 25 01:45:48 2019 +0530

    Updated Report

 _reports/rohit/rohit.md | 18 +++++++++++++++++-
 1 file changed, 17 insertions(+), 1 deletion(-)

commit 1ea453bc165ffdc61ba458e229f36968afbcc6fe
Author:     rohit3499 <47004225+rohit3499@users.noreply.github.com>
AuthorDate: Mon Feb 25 00:58:03 2019 +0530
Commit:     GitHub 
CommitDate: Mon Feb 25 00:58:03 2019 +0530

    Definitions of Euclidian Domains
    
    Euclidian Norms and Euclidian Domains and also updated the definition of an Integral Domain.

 Code/Ring.idr | 36 ++++++++++++++++++++++--------------
 1 file changed, 22 insertions(+), 14 deletions(-)

commit 4da929e6969f7a1e549c23a0cabceaaa2850275d
Author:     rohit3499 <47004225+rohit3499@users.noreply.github.com>
AuthorDate: Sun Feb 24 18:56:10 2019 +0530
Commit:     GitHub 
CommitDate: Sun Feb 24 18:56:10 2019 +0530

    Added definitions for zero divisors and Integral Domains
    
    Zero Divisors and Integral Domains

 Code/Ring.idr | 11 +++++++++++
 1 file changed, 11 insertions(+)

commit c8ad0d45487523d6ad5fa570750350a7fcec07d3
Author:     rohit3499 <47004225+rohit3499@users.noreply.github.com>
AuthorDate: Mon Feb 11 01:27:40 2019 +0530
Commit:     GitHub 
CommitDate: Mon Feb 11 01:27:40 2019 +0530

    Add files via upload

 bezout.idr | 204 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 204 insertions(+)

commit 260b1e8ba1453a79e1c54f120656a8ae870546e7
Author:     rohit3499 <47004225+rohit3499@users.noreply.github.com>
AuthorDate: Tue Jan 29 22:47:58 2019 +0530
Commit:     GitHub 
CommitDate: Tue Jan 29 22:47:58 2019 +0530

    Euclid's Division Lemma with partial proof
    
    proved that given a and b, there exist a quotient and a remainder (not necessarily unique)

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

commit 5d44076d116d6889499d7b97a90c15ccef9ae502
Author:     rohit3499 <47004225+rohit3499@users.noreply.github.com>
AuthorDate: Tue Jan 29 22:19:50 2019 +0530
Commit:     GitHub 
CommitDate: Tue Jan 29 22:19:50 2019 +0530

    Euclid's division lemma with proof
    
    Provided a partial proof for Euclid's Division Lemma. Given a and b, there exist (not necessarily unique at this point) a quotient and remainder.

 Code/Bezout.idr | 98 +++++++++++++++++++++++++++++++++++++++++++++++++++------
 1 file changed, 89 insertions(+), 9 deletions(-)