MA 210: Logic, Types and Spaces

Project Report for Logic, Types, Spaces 2019

Chinmaya Kausik

Outline of the work done

All functions defined are now total.

Groups

Definitions

Defined Abelian Groups by the type IsAbelianGrp in the file Group.idr
Defined the type of Injective functions in the file Group.idr by the type Inj in the file Group.idr
Defined the data type Group for Groups in Group.idr
Defined Homomorphisms in the file Group.idr by the type Hom in the file Group.idr
Defined Subgroups in the file Group.idr by the type Subgroup
Defined Self-Conjugate Subgroups in the file Group.idr by the type NSub

Cosets and Quotienting

Definitions

Defined Transversals in the file Cosets.idr using the type IsTransversal (composed of types CosetInj and CosetAll)
Defined the data type for Transversals using the type Transversal in the file Cosets.idr

Functions and Proofs

Defined Coset Multiplication using the function MulTrans in the file Cosets.idr
Generated the Representative of an element of group in a given transversal using the function repgen in the file CosetRep.idr
Proved that Coset Representatives thus generated for the embedding of a transversal in its underlying group are the same as the transversal elements. This is, in some sense, the uniqueness of coset representatives.

Rings

Definitions (in the file `Ring.idr`)

Corrected the definition of the type IsDistributive
Corrected the definition of the type IsRing to match apparent intentions and for defining ideals.
Defined data types for Rings, Commutative Rings, Useful Rings, Rings with Identity, Integral Domains, Euclidean Domains and PID’s (also defined the raw type for PID’s) in the file
Defined some of the functions that show the appropriate relations between these types (e.g URingisCRing generates the data type of a commutative ring structure from a useful one on a given type)
Defined some of the functions that extract the ring operations and multiplicative identity from elements of these data types (e.g. Ring_Mult_identity provides the multiplicative identity of a ring with identity)
Defined Ring Homomorphisms between general rings through the type RHom
Defined Ring Homomorphisms between rings with identity through the type IRHom
Defined Ideals of rings through the type IsIdeal
Defined Principal Ideals through the type IsPrincipalIdeal
Defined PID’s through the type IsPID

Functions and Proofs (in the file `Ring.Properties.idr`)

Proved that if a+a = a in a given ring, then a = 0
Proved that a0 = 0 and 0a = 0
Proved that if f is a ring homomorphism between general rings (without multplicative identities), then f(0) = 0
Proved that if f is a ring homomorphism between rings with multiplicative identities, then f(0) = 0

Examples (in the file `RingExamples.idr`)

Proved that ZZ forms a ring under + and *

Arithmetic in Base n

Defined the inductive type Base (with argument n) of numbers in Base n

Functions and Algorithms (in the file `Basen.idr`)

Defined the function Rev (and an auxiliary Revonto) that Reverses the base n representation of a number
Defined the function concat that Concatenates two numbers in base n
Defined the functions tonatFin and tonat that Convert a number in Fin n and Base n respectively to their natural number equivalents
Defined the functions tofinNat and tofin that Convert a natural number to its modular Fin n reduction and representation base n respectively
Defined the function Eucl that finds the Quotient and Remainder for two numbers along the way
Defined the function embn that Vertically Embeds a member of Fin n in Fin (S n)
Defined the function Predec that finds the Predecessor in Fin n of a number in Fin (S n) if it is not equal to n itself.
Defined the function addfin that Adds two numbers in Fin n
Defined the function addfinlist that Adds two numbers in base n
Defined the function mulfinList that Multiplies two numbers in base n

Lists

Proofs (in the file `Lists.idr`)

Proved that the reverse function for lists is, in some sense, Pseudo-contravariant with concatenation through the function reviscontra
Proved that the reverse function for lists is Self-Inverse through the function reveq

Nat Utilities

Proofs (in the file `NatUtils.idr`)

Proved that a witness of LTE m n implies a witness of (lte m n = True)

Log of git commits by author


commit 8921da8e78790d35bde529a11bb56652c053342b
Author:     Chinmaya Kausik <39112310+Chinmaya-Kausik@users.noreply.github.com>
AuthorDate: Sat Apr 20 02:48:34 2019 +0530
Commit:     GitHub 
CommitDate: Sat Apr 20 02:48:34 2019 +0530

    Update chinmaya.md

 _reports/chinmaya/chinmaya.md | 12 +++++++++---
 1 file changed, 9 insertions(+), 3 deletions(-)

commit 99cccd49e89a4a1f64b1b283bcaa9840bf54321f
Author:     Chinmaya Kausik <39112310+Chinmaya-Kausik@users.noreply.github.com>
AuthorDate: Sat Apr 20 02:42:10 2019 +0530
Commit:     GitHub 
CommitDate: Sat Apr 20 02:42:10 2019 +0530

    Updated with new contributions

 _reports/chinmaya/chinmaya.md | 8 ++++++++
 1 file changed, 8 insertions(+)

commit e98ae755ff15837a541959f2efd34b767c2b67b0
Author:     Chinmaya Kausik <39112310+Chinmaya-Kausik@users.noreply.github.com>
AuthorDate: Sat Apr 20 02:27:10 2019 +0530
Commit:     GitHub 
CommitDate: Sat Apr 20 02:27:10 2019 +0530

    Totality annotations for Lists.idr

 Code/Lists.idr | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

commit b1f3636f62a4aaef4d5460e19a1bcd08cfc175a0
Author:     Chinmaya Kausik <39112310+Chinmaya-Kausik@users.noreply.github.com>
AuthorDate: Sat Apr 20 02:23:40 2019 +0530
Commit:     GitHub 
CommitDate: Sat Apr 20 02:23:40 2019 +0530

    Totality for RingProperties

 Code/RingProperties.idr | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

commit 1e5b4c3a59a1a0acd1246d682785e58bc129b6b4
Author:     Chinmaya Kausik <39112310+Chinmaya-Kausik@users.noreply.github.com>
AuthorDate: Sat Apr 20 02:20:59 2019 +0530
Commit:     GitHub 
CommitDate: Sat Apr 20 02:20:59 2019 +0530

    Update GroupCosetRep.idr

commit 27652c7717d320a61ded9dc173aafcaf96c618a1
Author:     Chinmaya Kausik <39112310+Chinmaya-Kausik@users.noreply.github.com>
AuthorDate: Sat Apr 20 02:17:48 2019 +0530
Commit:     GitHub 
CommitDate: Sat Apr 20 02:17:48 2019 +0530

    Totality annotations for GroupCosetRep

 Code/GroupCosetRep.idr | 2 ++
 1 file changed, 2 insertions(+)

commit ad4ef34a47886cd5d3fe9a5f18c7693f4daa48c7
Author:     Chinmaya Kausik <39112310+Chinmaya-Kausik@users.noreply.github.com>
AuthorDate: Sat Apr 20 02:13:51 2019 +0530
Commit:     GitHub 
CommitDate: Sat Apr 20 02:13:51 2019 +0530

    GroupCosets with totality annotations

 Code/GroupCosets.idr | 12 +++++++++---
 1 file changed, 9 insertions(+), 3 deletions(-)

commit 3e4607a21ae22244b6e9f0a1503b1ffe2d95ff43
Author:     Chinmaya Kausik <39112310+Chinmaya-Kausik@users.noreply.github.com>
AuthorDate: Sat Apr 20 02:10:21 2019 +0530
Commit:     GitHub 
CommitDate: Sat Apr 20 02:10:21 2019 +0530

    BaseN is now total

 Code/BaseN.idr | 138 ++++++++++++++++++++++++++-------------------------------
 1 file changed, 62 insertions(+), 76 deletions(-)

commit 42713635212bb06a245c322dc33da35563a8efe7
Author:     Chinmaya Kausik <39112310+Chinmaya-Kausik@users.noreply.github.com>
AuthorDate: Fri Apr 19 18:24:50 2019 +0530
Commit:     GitHub 
CommitDate: Fri Apr 19 18:24:50 2019 +0530

    Transversal multiplication is a homomorphism
    
    Proofs that MulTrans is, in some sense, a magma homomorphism

 Code/GroupTransversals.idr | 38 ++++++++++++++++++++++++++++++++++++++
 1 file changed, 38 insertions(+)

commit 94c0eede87d7a2e1fa3dbf635fab4c141adad2b3
Author:     Chinmaya Kausik <39112310+Chinmaya-Kausik@users.noreply.github.com>
AuthorDate: Fri Apr 19 18:22:42 2019 +0530
Commit:     GitHub 
CommitDate: Fri Apr 19 18:22:42 2019 +0530

    Alignment for module name and filename

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

commit aabc8cd1b3b6bece3d32d3504642788438345eb9
Author:     Chinmaya Kausik <39112310+Chinmaya-Kausik@users.noreply.github.com>
AuthorDate: Sun Apr 14 02:42:32 2019 +0530
Commit:     GitHub 
CommitDate: Sun Apr 14 02:42:32 2019 +0530

    LTE implies lte m n = True
    
    Added proof

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

commit 8c23c20530e8ae4a0aa3f2b0b221b5b76e6e10dd
Author:     Chinmaya Kausik <39112310+Chinmaya-Kausik@users.noreply.github.com>
AuthorDate: Sun Apr 14 02:08:41 2019 +0530
Commit:     GitHub 
CommitDate: Sun Apr 14 02:08:41 2019 +0530

    Totality and FinNatop
    
    Made some definitions total, and proved that tofinNat inverts tonatFin

 Code/BaseN.idr | 160 ++++++++++++++++++++++++++++++++++++++++++++++++---------
 1 file changed, 135 insertions(+), 25 deletions(-)

commit 9693eb4e15003bbcc23a0a286688350a9cbe6428
Author:     Chinmaya Kausik <39112310+Chinmaya-Kausik@users.noreply.github.com>
AuthorDate: Fri Apr 12 22:10:16 2019 +0530
Commit:     GitHub 
CommitDate: Fri Apr 12 22:10:16 2019 +0530

    Rename Ring.Properties.idr to RingProperties.idr

 Code/{Ring.Properties.idr => RingProperties.idr} | 0
 1 file changed, 0 insertions(+), 0 deletions(-)

commit 888eca995321eda2ec03fdd9137d03bb4c1a2207
Author:     Chinmaya Kausik <39112310+Chinmaya-Kausik@users.noreply.github.com>
AuthorDate: Fri Apr 12 22:06:30 2019 +0530
Commit:     GitHub 
CommitDate: Fri Apr 12 22:06:30 2019 +0530

    Ring.Properties is not an appropriate filename

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

commit f06ac6751a38bd8712a7d7e7a369c7728b6c1c73
Author:     Chinmaya Kausik <39112310+Chinmaya-Kausik@users.noreply.github.com>
AuthorDate: Fri Apr 12 21:42:40 2019 +0530
Commit:     GitHub 
CommitDate: Fri Apr 12 21:42:40 2019 +0530

    Fized another import (apologies)
    
    Checked the others this time

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

commit 672e46e88ea97e6d3bb0d8e15671d278c234e7d0
Author:     Chinmaya Kausik <39112310+Chinmaya-Kausik@users.noreply.github.com>
AuthorDate: Fri Apr 12 21:23:09 2019 +0530
Commit:     GitHub 
CommitDate: Fri Apr 12 21:23:09 2019 +0530

    Fixed Ring

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

commit cfa0920579de131a79e32532d5197874b51c0b92
Author:     Chinmaya Kausik <39112310+Chinmaya-Kausik@users.noreply.github.com>
AuthorDate: Fri Apr 12 20:44:50 2019 +0530
Commit:     GitHub 
CommitDate: Fri Apr 12 20:44:50 2019 +0530

    Created a file for concrete kinds of rings
    
    Proved that the integers form a ring

 Code/RingExamples.idr | 37 +++++++++++++++++++++++++++++++++++++
 1 file changed, 37 insertions(+)

commit 1f9126b00b42e17353a5118d086e229e963c7eae
Author:     Chinmaya Kausik <39112310+Chinmaya-Kausik@users.noreply.github.com>
AuthorDate: Fri Apr 12 17:04:00 2019 +0530
Commit:     GitHub 
CommitDate: Fri Apr 12 17:04:00 2019 +0530

    Proofs that for a ring homomorphism f, f(0) = 0
    
    Proofs for two kinds of rings. Proving that IRHom is RHom was not coming through

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

commit 9c8b18265a6ec0cb2405aab9c8f2164b796d1c12
Author:     Chinmaya Kausik <39112310+Chinmaya-Kausik@users.noreply.github.com>
AuthorDate: Mon Feb 25 10:51:54 2019 +0530
Commit:     GitHub 
CommitDate: Mon Feb 25 10:51:54 2019 +0530

    Fixed some broken function types
    
    Updated Subgroup call and a dependent type expression

 Code/Quotient_Group.idr | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

commit 042aa31ea748cd2b8e9c165c86ff45e86538a96f
Author:     Chinmaya Kausik <39112310+Chinmaya-Kausik@users.noreply.github.com>
AuthorDate: Mon Feb 25 09:38:47 2019 +0530
Commit:     GitHub 
CommitDate: Mon Feb 25 09:38:47 2019 +0530

    Removed functions already defined
    
    Functions defined in FinUtils with the same name

 Code/LinearAlgebra.idr | 14 --------------
 1 file changed, 14 deletions(-)

commit 6d5b16cd3bfb0453e2f1b3ecc4b12176327e50e3
Author:     Chinmaya Kausik <39112310+Chinmaya-Kausik@users.noreply.github.com>
AuthorDate: Mon Feb 25 09:30:36 2019 +0530
Commit:     GitHub 
CommitDate: Mon Feb 25 09:30:36 2019 +0530

    Corrected broken code

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

commit 25b108c811936ce2dea7af50ca33fec272beda95
Author:     Chinmaya Kausik <39112310+Chinmaya-Kausik@users.noreply.github.com>
AuthorDate: Mon Feb 25 09:22:39 2019 +0530
Commit:     GitHub 
CommitDate: Mon Feb 25 09:22:39 2019 +0530

    Changed module name for Cosets
    
    Fixing import issue

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

commit 81e0ad3424d5e1dc13171fe2a21c2cd459a3b4a5
Author:     Chinmaya Kausik <39112310+Chinmaya-Kausik@users.noreply.github.com>
AuthorDate: Mon Feb 25 09:18:41 2019 +0530
Commit:     GitHub 
CommitDate: Mon Feb 25 09:18:41 2019 +0530

    Create FinUtils.idr
    
    To fix Sriram's broken code

 FinUtils.idr | 37 +++++++++++++++++++++++++++++++++++++
 1 file changed, 37 insertions(+)

commit 87ece1108102503ee67e493d2114d9a3ed78cf6e
Author:     Chinmaya Kausik <39112310+Chinmaya-Kausik@users.noreply.github.com>
AuthorDate: Mon Feb 25 09:18:20 2019 +0530
Commit:     GitHub 
CommitDate: Mon Feb 25 09:18:20 2019 +0530

    Update MultiSolver.idr
    
    Changed import from BaseN to FinUtils

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

commit 8d909f97ef2104bca45ddf4284fdc200a537aee5
Author:     Chinmaya Kausik <39112310+Chinmaya-Kausik@users.noreply.github.com>
AuthorDate: Mon Feb 25 08:16:55 2019 +0530
Commit:     GitHub 
CommitDate: Mon Feb 25 08:16:55 2019 +0530

    Added data types, ideals, PIDs
    
    Defined data types for different kinds of rings
    Adjusted some definitions (stemming from rings being defined as multiplicative monoids instead of magmas)
    Defined ring homomorphisms
    Defined ideals of rings
    Defined PIDs

 Code/Ring.idr | 150 +++++++++++++++++++++++++++++++++++++++++++++-------------
 1 file changed, 118 insertions(+), 32 deletions(-)

commit d9efdb0f4159a83c229bb5d24fd17ce0565f2e6a
Author:     Chinmaya Kausik <39112310+Chinmaya-Kausik@users.noreply.github.com>
AuthorDate: Mon Feb 25 06:27:23 2019 +0530
Commit:     GitHub 
CommitDate: Mon Feb 25 06:27:23 2019 +0530

    Update report for Chinmaya Kausik

 _reports/chinmaya/chinmaya.md | 70 ++++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 69 insertions(+), 1 deletion(-)

commit e7639fe2b7ebca1f56bfa25b3c1d7b640a6eab45
Author:     Chinmaya Kausik <39112310+Chinmaya-Kausik@users.noreply.github.com>
AuthorDate: Mon Feb 25 05:27:27 2019 +0530
Commit:     GitHub 
CommitDate: Mon Feb 25 05:27:27 2019 +0530

    Proofs about the reverse function
    
    Proofs establishing that the reverse function is:
    
    1) In some sense, pseudocontravariant with concatenation
    2) Self-inverse

 Code/Lists.idr | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)

commit 3ce383dbe4e3ea4741b024e414268d3f93107fef
Author:     Chinmaya Kausik <39112310+Chinmaya-Kausik@users.noreply.github.com>
AuthorDate: Mon Feb 25 04:54:26 2019 +0530
Commit:     GitHub 
CommitDate: Mon Feb 25 04:54:26 2019 +0530

    Created a file for properties of rings
    
    Added proofs that conclude 0*a = a*0 = 0

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

commit d11d38bbd060a50379d7be3bb11d4e187765fbe1
Author:     Chinmaya Kausik <39112310+Chinmaya-Kausik@users.noreply.github.com>
AuthorDate: Sat Feb 23 11:44:04 2019 +0530
Commit:     GitHub 
CommitDate: Sat Feb 23 11:44:04 2019 +0530

    Delete Group.CosetRep.idr
    
    It was added to the main directory by accident

 Group.CosetRep.idr | 30 ------------------------------
 1 file changed, 30 deletions(-)

commit ff01e90ca2e0205bc1cbca47f54138929d9a8840
Author:     Chinmaya Kausik <39112310+Chinmaya-Kausik@users.noreply.github.com>
AuthorDate: Sat Feb 23 11:43:19 2019 +0530
Commit:     GitHub 
CommitDate: Sat Feb 23 11:43:19 2019 +0530

    Updated CosetRep for fst and snd
    
    Also, the previous version was added to the main directory instead of code. It would be great if that could be deleted. My apologies.

 Code/Group.CosetRep.idr | 29 +++++++++++++++++++++++++++++
 1 file changed, 29 insertions(+)

commit 40b31095f9ce59dee55b5c3b409ec5825081e8cc
Author:     Chinmaya Kausik <39112310+Chinmaya-Kausik@users.noreply.github.com>
AuthorDate: Thu Feb 21 23:51:26 2019 +0530
Commit:     GitHub 
CommitDate: Thu Feb 21 23:51:26 2019 +0530

    Rename Cosets.idr to Group.Cosets.idr

 Code/{Cosets.idr => Group.Cosets.idr} | 0
 1 file changed, 0 insertions(+), 0 deletions(-)

commit 17aa68f9c4c0f2bf64df82c8561629d060d008d8
Author:     Chinmaya Kausik <39112310+Chinmaya-Kausik@users.noreply.github.com>
AuthorDate: Thu Feb 21 23:50:14 2019 +0530
Commit:     GitHub 
CommitDate: Thu Feb 21 23:50:14 2019 +0530

    Rename CosetRep.idr to Group.CosetRep.idr

 CosetRep.idr => Group.CosetRep.idr | 0
 1 file changed, 0 insertions(+), 0 deletions(-)

commit 9e5eac15ad423edd9adcc2d8d619a77c7c0c0d44
Author:     Chinmaya Kausik <39112310+Chinmaya-Kausik@users.noreply.github.com>
AuthorDate: Thu Feb 21 23:46:25 2019 +0530
Commit:     GitHub 
CommitDate: Thu Feb 21 23:46:25 2019 +0530

    Showed uniqueness of coset representatives
    
    Proof that the coset representative generated by taking the image of a transversal element in g and finding its representative in the transversal is the same as the original element

 CosetRep.idr | 30 ++++++++++++++++++++++++++++++
 1 file changed, 30 insertions(+)

commit 0498228cc7bdce361d0236898151a8c66fd378fe
Author:     Chinmaya Kausik <39112310+Chinmaya-Kausik@users.noreply.github.com>
AuthorDate: Thu Feb 21 23:31:18 2019 +0530
Commit:     GitHub 
CommitDate: Thu Feb 21 23:31:18 2019 +0530

    Made all cosets left cosets

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

commit bf0826f2174a15ae3a30dcd8eb26e43154c7b57a
Author:     Chinmaya Kausik <39112310+Chinmaya-Kausik@users.noreply.github.com>
AuthorDate: Thu Feb 21 21:57:23 2019 +0530
Commit:     GitHub 
CommitDate: Thu Feb 21 21:57:23 2019 +0530

    Deleted unused commented code

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

commit 613549b5800ca66cd14135351369e960a1bbb532
Author:     Chinmaya Kausik <39112310+Chinmaya-Kausik@users.noreply.github.com>
AuthorDate: Thu Feb 21 20:27:24 2019 +0530
Commit:     GitHub 
CommitDate: Thu Feb 21 20:27:24 2019 +0530

    Modified Groups for cosets

 Code/Group.idr | 42 ++++++++++++++++++++++++++++--------------
 1 file changed, 28 insertions(+), 14 deletions(-)

commit 82fc26a12b98e295678263f3ea10cd1cc46cefb7
Author:     Chinmaya Kausik <39112310+Chinmaya-Kausik@users.noreply.github.com>
AuthorDate: Thu Feb 21 20:26:31 2019 +0530
Commit:     GitHub 
CommitDate: Thu Feb 21 20:26:31 2019 +0530

    Modified the file so that it compiles in time

 Code/Cosets.idr | 79 ++++++++++++++++++++++++---------------------------------
 1 file changed, 33 insertions(+), 46 deletions(-)

commit b02f6d2014a10f9b59300951b52c1a66d88a4b68
Author:     Chinmaya Kausik <39112310+Chinmaya-Kausik@users.noreply.github.com>
AuthorDate: Fri Feb 15 15:11:49 2019 +0530
Commit:     GitHub 
CommitDate: Fri Feb 15 15:11:49 2019 +0530

    Modified the data type Base
    
    Added an explicit argument for the base in each constructor and redid the file

 Code/BaseN.idr | 63 +++++++++++++++++++++++++++++++---------------------------
 1 file changed, 34 insertions(+), 29 deletions(-)

commit 7d8d6365b484d5899611edbeb86f97b1fecadc1e
Author:     Chinmaya Kausik <39112310+Chinmaya-Kausik@users.noreply.github.com>
AuthorDate: Fri Feb 15 01:33:09 2019 +0530
Commit:     GitHub 
CommitDate: Fri Feb 15 01:33:09 2019 +0530

    Added multiplication
    
    The algorithms for Basen have been rewritten with the custom data type
    
    We can now start proving things again

 Code/BaseN.idr | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

commit 605c36a899765974b13561188c6e907b713b725f
Author:     Chinmaya Kausik <39112310+Chinmaya-Kausik@users.noreply.github.com>
AuthorDate: Fri Feb 15 01:18:58 2019 +0530
Commit:     GitHub 
CommitDate: Fri Feb 15 01:18:58 2019 +0530

    Redid addition in custom dat type
    
    Defined Base as a custom data type emulating lists, and:
    
    1) Defined a rev function, a left strip function, a concatenation function, etc.
    2) Appropriately modified the definition of addition in Base (S n)
    3) Modified conversion functions slightly

 Code/BaseN.idr | 185 +++++++++++++++++++++++++++------------------------------
 1 file changed, 86 insertions(+), 99 deletions(-)

commit 8c1e07f21c30ce1e98f14fde186478710614cbba
Author:     Chinmaya Kausik <39112310+Chinmaya-Kausik@users.noreply.github.com>
AuthorDate: Thu Feb 14 23:44:57 2019 +0530
Commit:     GitHub 
CommitDate: Thu Feb 14 23:44:57 2019 +0530

    Changed a comment

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

commit 9a136469118fe812c03ce67c6ba6ca3426a9afe9
Author:     Chinmaya Kausik <39112310+Chinmaya-Kausik@users.noreply.github.com>
AuthorDate: Thu Feb 14 23:43:06 2019 +0530
Commit:     GitHub 
CommitDate: Thu Feb 14 23:43:06 2019 +0530

    Added Fin-based addition for Fin n
    
    Used auxiliary proofs for case-work on the sum exceeding n in (Fin (S n))
    
    1) Isn: Checks whether a given (Fin(S n)) is n itself
    2) IsnisIsn: Proves the definitional equality for Isn
    3) IsNotnPf: Pulls back falsity of Isn (S n) (FS x) to Isn n x
    4) Predec: Predecessor function for values not equal to n
    5) DecIsn: Somewhat like the decidable type for truth of Isn
    6) addfin: the actual addition function

 Code/BaseN.idr | 41 +++++++++++++++++++++++++++++++++++++----
 1 file changed, 37 insertions(+), 4 deletions(-)

commit f94349acf98a14849e19c5a25033c1494d98229c
Author:     Chinmaya Kausik <39112310+Chinmaya-Kausik@users.noreply.github.com>
AuthorDate: Thu Feb 14 20:21:38 2019 +0530
Commit:     GitHub 
CommitDate: Thu Feb 14 20:21:38 2019 +0530

    Added functions for Fin based addfin
    
    Added:
    1) A generator for n in Fin (S n)
    2) A function that checks whether a given element of (Fin (S n)) is n

 Code/BaseN.idr | 20 ++++++++++++++++----
 1 file changed, 16 insertions(+), 4 deletions(-)

commit 2a33ec0b88ec2e9cd1f51d85d63017ea0d5cf9c9
Author:     Chinmaya Kausik <39112310+Chinmaya-Kausik@users.noreply.github.com>
AuthorDate: Thu Feb 14 17:21:16 2019 +0530
Commit:     GitHub 
CommitDate: Thu Feb 14 17:21:16 2019 +0530

    Corrected some indentation etc

 Code/Cosets.idr | 69 +++++++++++++--------------------------------------------
 1 file changed, 15 insertions(+), 54 deletions(-)

commit 174815a027a7bc55143eb6843bf7915d4cd3846b
Author:     Chinmaya Kausik <39112310+Chinmaya-Kausik@users.noreply.github.com>
AuthorDate: Thu Feb 14 17:16:19 2019 +0530
Commit:     GitHub 
CommitDate: Thu Feb 14 17:16:19 2019 +0530

    Removed coset code from Group.idr
    
    Following the request from @SideArt

 Code/Group.idr | 54 ------------------------------------------------------
 1 file changed, 54 deletions(-)

commit e38c4b475f6f8dada6668b148a533b083fc0653a
Author:     Chinmaya Kausik <39112310+Chinmaya-Kausik@users.noreply.github.com>
AuthorDate: Thu Feb 14 17:15:07 2019 +0530
Commit:     GitHub 
CommitDate: Thu Feb 14 17:15:07 2019 +0530

    Moved coset code to a new file
    
    On a request from @SideArt

 Code/Cosets.idr | 97 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 97 insertions(+)

commit d1302b7a9413fc96e6fd8fa5051141032275f3fa
Author:     Chinmaya Kausik <39112310+Chinmaya-Kausik@users.noreply.github.com>
AuthorDate: Thu Feb 14 16:44:17 2019 +0530
Commit:     GitHub 
CommitDate: Thu Feb 14 16:44:17 2019 +0530

    Added proofs about lists and basen addition
    
    Including commented proofs that don't work

 Code/BaseN.idr | 36 ++++++++++++++++++++++++++++++++++++
 1 file changed, 36 insertions(+)

commit 2bbac7238ee8ab1efd44775d0695ea6b0e418b72
Author:     Chinmaya Kausik <39112310+Chinmaya-Kausik@users.noreply.github.com>
AuthorDate: Thu Feb 14 16:37:36 2019 +0530
Commit:     GitHub 
CommitDate: Thu Feb 14 16:37:36 2019 +0530

    Added the code removed by Arka's pull request
    
    He used an older fork

 Code/Group.idr | 77 +++++++++++++++++++++++++++++++++++++++++-----------------
 1 file changed, 55 insertions(+), 22 deletions(-)

commit 518c550a061971b0b4ad2a0d069394f10352cdc0
Author:     Chinmaya Kausik <39112310+Chinmaya-Kausik@users.noreply.github.com>
AuthorDate: Wed Feb 13 23:04:29 2019 +0530
Commit:     GitHub 
CommitDate: Wed Feb 13 23:04:29 2019 +0530

    Added proofs about the coset rep maps
    
    Proofs that the coset representative map arising from CosetAll, is in some specific useful case, a magma homomorphism

 Code/Group.idr | 25 +++++++++++++++++++++++++
 1 file changed, 25 insertions(+)

commit c72431ce5cafc0807f854f8ee39ae23157342e0e
Author:     Chinmaya Kausik <39112310+Chinmaya-Kausik@users.noreply.github.com>
AuthorDate: Wed Feb 13 16:50:29 2019 +0530
Commit:     GitHub 
CommitDate: Wed Feb 13 16:50:29 2019 +0530

    Added a proof of uniqueness of coset reps
    
    A proof that the operation that generates coset representative in trav for an element of g (from CosetAll) inverts the function generating a coset representative by going from trav to g (the first coordinate of IsTraversal)
    
    Also added a comment above the mult operation in trav

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

commit 6cd1a64540990951ca87b7719ad3962c2a8e0d6b
Author:     Chinmaya Kausik <39112310+Chinmaya-Kausik@users.noreply.github.com>
AuthorDate: Wed Feb 13 16:24:41 2019 +0530
Commit:     GitHub 
CommitDate: Wed Feb 13 16:24:41 2019 +0530

    Added coset traversals and induced multiplication
    
    The group multiplication for traversals is defined.
    
    Proofs that this does indeed form a group is under way.

 Code/Group.idr | 42 +++++++++++++++++++-----------------------
 1 file changed, 19 insertions(+), 23 deletions(-)

commit 0d831df109f93f942f3cd573f114b9b034fec627
Author:     Chinmaya Kausik <39112310+Chinmaya-Kausik@users.noreply.github.com>
AuthorDate: Wed Jan 30 04:29:28 2019 +0530
Commit:     GitHub 
CommitDate: Wed Jan 30 04:29:28 2019 +0530

    Proofs about the reverse function
    
    Proofs that the reverse function:
    
    1) Is in some sense, "pseudo-contravariant" with concatentation
    2) Is self inverse (this will be important in proving the agreement of arithmetic in base n with Nat)
    
    Along with 2 auxiliary lemmas

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

commit 99cda667088e58d66c547369d444a9da4bd0e0c3
Author:     Chinmaya Kausik <39112310+Chinmaya-Kausik@users.noreply.github.com>
AuthorDate: Sun Jan 27 04:29:44 2019 +0530
Commit:     GitHub 
CommitDate: Sun Jan 27 04:29:44 2019 +0530

    Optional implementation of cosets as image types
    
    The issue is that it generates a "coset" for each element, whose embeddings are the same for elements with the same coset, but are otherwise different types
    This may or may not be advisable to use

 Code/Group.idr | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

commit bde218ab55db4c7adb09bf4fd83ec12b09fabd80
Author:     Chinmaya Kausik <39112310+Chinmaya-Kausik@users.noreply.github.com>
AuthorDate: Sat Jan 26 20:21:35 2019 +0530
Commit:     GitHub 
CommitDate: Sat Jan 26 20:21:35 2019 +0530

    Added more definitions and infix operations for ease of use
    
    Definitions for abelian groups, subgroups, structure homomorphisms and self-conjugate subgroups
    Infix functions for group operations

 Code/Group.idr | 55 ++++++++++++++++++++++++++++++++++++++++++-------------
 1 file changed, 42 insertions(+), 13 deletions(-)

commit b99366a553e243e6eccace76db1b7d9056748689
Author:     Chinmaya Kausik <39112310+Chinmaya-Kausik@users.noreply.github.com>
AuthorDate: Fri Jan 25 00:44:45 2019 +0530
Commit:     GitHub 
CommitDate: Fri Jan 25 00:44:45 2019 +0530

    Adding multiplication functions plus corrections in some auxiliary functions
    
    The arithmetic in base n is now set, if we are not considering subtraction

 Code/Basen.idr | 28 ++++++++++++++++++++++++++--
 1 file changed, 26 insertions(+), 2 deletions(-)

commit dc2aa22fe52f716f85439d886d747b60b6b4d90c
Author:     Chinmaya Kausik <39112310+Chinmaya-Kausik@users.noreply.github.com>
AuthorDate: Fri Jan 25 00:43:05 2019 +0530
Commit:     GitHub 
CommitDate: Fri Jan 25 00:43:05 2019 +0530

    Spacing and correcting my name's spelling (Pull when convenient)
    
    I apologize for the inconvenience caused.

 Code/Bezout.idr | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

commit a8a07b303eb11465720510985af0d844b95aa386
Author:     Chinmaya Kausik <39112310+Chinmaya-Kausik@users.noreply.github.com>
AuthorDate: Thu Jan 24 04:39:11 2019 +0530
Commit:     GitHub 
CommitDate: Thu Jan 24 04:39:11 2019 +0530

    Update Basen.idr

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

commit 36a46e23126bfa1fcf1651cde43ad39a72ece450
Author:     Chinmaya Kausik <39112310+Chinmaya-Kausik@users.noreply.github.com>
AuthorDate: Thu Jan 24 04:34:55 2019 +0530
Commit:     GitHub 
CommitDate: Thu Jan 24 04:34:55 2019 +0530

    Adding lists

 Code/Basen.idr | 19 +++++++++++++++++--
 1 file changed, 17 insertions(+), 2 deletions(-)

commit 45de83dc108870c9805d204fa54cf5cfe3996ab2
Author:     Chinmaya Kausik <39112310+Chinmaya-Kausik@users.noreply.github.com>
AuthorDate: Thu Jan 24 04:00:30 2019 +0530
Commit:     GitHub 
CommitDate: Thu Jan 24 04:00:30 2019 +0530

    Basen with conversions and adding two Fin Types

 Code/Basen.idr | 39 +++++++++++++++++++++++++++++++++++++++
 1 file changed, 39 insertions(+)

Project Report for Logic, Types, Spaces 2019

Chinmaya Kausik

Outline of the work done

Groups

Definitions

Cosets and Quotienting

Definitions

Functions and Proofs

Rings

Definitions (in the file Ring.idr)

Functions and Proofs (in the file Ring.Properties.idr)

Examples (in the file RingExamples.idr)

Arithmetic in Base n

Functions and Algorithms (in the file Basen.idr)

Lists

Proofs (in the file Lists.idr)

Nat Utilities

Proofs (in the file NatUtils.idr)

Log of git commits by author

Department of Mathematics, Indian Institute of Science.

Definitions (in the file `Ring.idr`)

Functions and Proofs (in the file `Ring.Properties.idr`)

Examples (in the file `RingExamples.idr`)

Functions and Algorithms (in the file `Basen.idr`)

Proofs (in the file `Lists.idr`)

Proofs (in the file `NatUtils.idr`)