## Groups

#### Definitions

1. Defined Monoid in the file Monoid.idr by the type IsMonoid in the file Monoid.idr
2. Defined Group in the file Group.idr by the type IsGroup in the file Group.idr.
3. Corrected the definition of Image of a homomorphism given by Chinmoy, in the file Quotient_Group.idr.
4. Defined free group generated by a type in the file FreeGroup.idr.
5. Defined kernel of a homomorphism in the file Group_kernel.idr.

#### Properties

Proved the following property for groups in the file Group_property.idr.

1. Identity is unique for groups. (Group_property_1)
2. Inverse of an element is unique. (Group_property_2)
3. b = c implies a*b = a*c. (Group_property_3)
4. a*b = a*c implies b = c. (Group_property_4)
5. b = c implies b*a = c*a. (_Group_property_5)
6. b*a = c*a implies b = c. (_Group_property_6)
7. One sided inverse is two sided inverse. (Group_property_7)
8. If f : g -> h is group homomorphism then f(inv(a)) = inv(f(a)) (Proof has holes to fill) (Group_property_8)
9. Proved that elements of a free group has inverses.

### Quotient Groups

All are done in the file Quotient_Group.idr.

1. Defined the type of Coset of an element.
2. Given the type which represents that a particular element is in the Coset of an element by Is_in_Coset.
3. Given the type of the proposition - If b is in the coset of a, then a is in the coset of b.
4. Given the type of the proposition - A proof that Coset(a) * Coset(b) and Coset(a*b) are equal as sets.

## Rings

Defined rings in the file Ring.idr.

## Sorting with proof

#### Type of sorted vectors

Defined the type of sorted vectors by the type SortedVect in the file sorting_with_proof.idr

#### Permutation

1. Defined permutations as bijections by two functions PermB and Perm2 in the file Permutation.idr.
2. Defined application of a permutation by the function applyFunin the file Permutation.idr.
3. Defined a type Finite and proved that it is equivalent to the type Fin. Finite is easier to work with as it makes the size explicit.
4. Defined permutations by constructors by the type PermC in the file PermCons.idr.
5. Proved that permutations defined using constructors are bijections in the file PermCons.idr. Some helper functions are given in the file PermConsProperties.idr

#### Incomplete Proof of Sorting

Started a proof that the sorting algorithm is correct in the file InsertionProof.idr. Had to stop working on it as the code became very complicated and was taking too long to compile.

## Graph

Gave an alternate definition of graphs using adjacency matrix in the file Graph_alt.idr. Gave a method (fn_to_vect) to convert a function on (Fin n, Fin n) to a matrix. This is very useful to define identity matrices.

## Quotient Types

1. Quotient types are defined as types along with an equivalence relation.
2. Type of non-dependent functions between two quotient types (A,relA) and (B,relB) isdefined as the function type (A -> B) along with the condition of passing through the relations.
3. Family of quotient types is defined to be a type family along with transports
4. Defined the type of non_dependent function as a quotient type by defining a relation on (A -> B) and proving that it is a equivalence relation.

## Relations

Defined a addition operation on the type of relations on a type. Proved the following

1. The type of relations form a commutative monoid.
2. If we consider only equivalence relations then each element is an idempotent.

## Parsers

1. Created a method to parse floating point numbers
2. Defined the type of expressions as definitions (assigning a value to a variable), Expressions (stands for constants), Function(Curried function on double)

## Integers

1. Defined Integers as the quotient type (Nat, Nat) along with a relation ZZ_rel. Also proved it is an equivalence relation. (In the file ZZ_alt.idr)
2. Defined addition for Integers and proved that it respects the relation ZZ_rel.(In the file ZZ_plus.idr)
3. Defined substraction for Integers and proved that it respects the relation ZZ_rel.(In the file ZZ_subs.idr).
4. Defined the property of being a zero element w.r.t. plus and proved that it is equivalent to being of the form (n,n).

## Left Overs

1. Defined a more explicit version of congruence in the file congruence.idr
2. Proved that the equality for product type is generated by the equalities of components.

### Log of git commits by author


commit 6a783d4fb242cd80c079cb3f6de7d6356a433da8
AuthorDate: Sun Apr 21 12:36:31 2019 +0530
Commit:     GitHub
CommitDate: Sun Apr 21 12:36:31 2019 +0530

Characterised the property of being the zero element w.r.t. plus

Code/ZZplus.idr | 64 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++
1 file changed, 64 insertions(+)

commit a02b5afaf51be458ce7af126a5fdcf92378e4017
AuthorDate: Sun Apr 21 11:29:13 2019 +0530
Commit:     GitHub
CommitDate: Sun Apr 21 11:29:13 2019 +0530

Update arka.md

_reports/arka/arka.md | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)

commit e53c1190a1af5bf5d6567cb845d0863e10dbc5cc
AuthorDate: Sun Apr 21 11:28:33 2019 +0530
Commit:     GitHub
CommitDate: Sun Apr 21 11:28:33 2019 +0530

Update arka.md

_reports/arka/arka.md | 3 +++
1 file changed, 3 insertions(+)

commit 208677ed09b03008b828c235c65448879fb522dd
AuthorDate: Thu Apr 11 00:37:07 2019 +0530
Commit:     GitHub
CommitDate: Thu Apr 11 00:37:07 2019 +0530

Patching

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

commit da1c06e46f6bee33c57380c3e7c031a4e798da81
AuthorDate: Thu Apr 11 00:34:02 2019 +0530
Commit:     GitHub
CommitDate: Thu Apr 11 00:34:02 2019 +0530

Update arka.md

_reports/arka/arka.md | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)

commit cdffe73d43309db9075bbd7fc7197d32353aa902
AuthorDate: Thu Apr 11 00:27:36 2019 +0530
Commit:     GitHub
CommitDate: Thu Apr 11 00:27:36 2019 +0530

Updated report

_reports/arka/arka.md | 79 ++++++++++++++++++++++++++++++++++++++++++++++-----
1 file changed, 72 insertions(+), 7 deletions(-)

commit a92a6d3e7a8257ebdcf67c969be67233eb3bb951
AuthorDate: Thu Apr 11 00:26:55 2019 +0530
Commit:     GitHub
CommitDate: Thu Apr 11 00:26:55 2019 +0530

Code/Relations.idr | 24 +++++++++++++++++++++++-
1 file changed, 23 insertions(+), 1 deletion(-)

commit 5428caedf11a784fca8f201f5db6680bdc92a6b0
AuthorDate: Thu Apr 11 00:25:51 2019 +0530
Commit:     GitHub
CommitDate: Thu Apr 11 00:25:51 2019 +0530

Finished some remaining proof

commit aa99fa7c9d9b612b283443585717bd51f3371cb7
AuthorDate: Sat Apr 6 11:13:18 2019 +0530
Commit:     GitHub
CommitDate: Sat Apr 6 11:13:18 2019 +0530

Code/FreeGroup.idr          |  73 ++++++++++++++++++++++++++++++++++++++++++++
Code/Graph_alt.idr          |   1 +
Code/Product_Type_Eq.idr    |   2 ++
Code/Quotient_Type.idr      |  10 +++++-
Code/Relations.idr          |  61 ++++++++++++++++++++----------------
Code/Scheme_Expressions.idr |  12 ++++++--
Code/ZZsubs.ibc             | Bin 0 -> 4659 bytes
Code/congruence.idr         |   2 +-
Code/pigeonhole.idr         |  13 +++++++-
9 files changed, 141 insertions(+), 33 deletions(-)

commit d774cfc9d2fa2e17308fc7acc7dffdb62f0d7ea8
AuthorDate: Sat Apr 6 10:56:41 2019 +0530
Commit:     GitHub
CommitDate: Sat Apr 6 10:56:41 2019 +0530

Defined some operations and proved some properties of equivalence relations.

Code/Relations.idr | 51 +++++++++++++++++++++++++++++++++++++++++++++++++++
1 file changed, 51 insertions(+)

AuthorDate: Sat Apr 6 10:48:55 2019 +0530
Commit:     GitHub
CommitDate: Sat Apr 6 10:48:55 2019 +0530

Defined subtraction for ZZ_alt and proved that it passes through

Code/ZZmult.idr | 14 ++++++++++++++
Code/ZZplus.idr |  3 +++
Code/ZZsubs.idr | 34 ++++++++++++++++++++++++++++++++++
3 files changed, 51 insertions(+)

commit 1bcbe2cfcff072f7a9b4ff296c4cccb548ed1014
AuthorDate: Sat Mar 30 22:46:17 2019 +0530
Commit:     GitHub
CommitDate: Sat Mar 30 22:46:17 2019 +0530

Proved that the relation on the function type is indeed an equivalence relation.

Code/Quotient_Type.idr | 79 ++++++++++++++++++++++++++++++++++++++++++++++++++
1 file changed, 79 insertions(+)

commit f221d3f832685ed9d470d4a6bd305b8679bdccf4
AuthorDate: Sat Mar 30 22:16:42 2019 +0530
Commit:     GitHub
CommitDate: Sat Mar 30 22:16:42 2019 +0530

Hopefully fixed the error

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

commit 55ffda117a2955ee7b131dd8543332a666c2f462
AuthorDate: Sat Mar 30 20:54:29 2019 +0530
Commit:     GitHub
CommitDate: Sat Mar 30 20:54:29 2019 +0530

Changed capitalisation error. Gave a relation on the functions between quotient types to have the function type between quotient types to be a quotient type itself.

Code/Quotient_Type.idr | 78 +++++++++++++++++++++++++++++---------------------
1 file changed, 46 insertions(+), 32 deletions(-)

AuthorDate: Sat Mar 30 16:23:27 2019 +0530
Commit:     GitHub
CommitDate: Sat Mar 30 16:23:27 2019 +0530

Finished the proof that ZZplus passes through the equivalence relation

Code/ZZplus.idr | 29 ++++++++++++++++++++++++++++-
1 file changed, 28 insertions(+), 1 deletion(-)

commit 9a868d4c40673a954e3cdbd9dc91e7b34365531d
AuthorDate: Sat Mar 30 15:53:17 2019 +0530
Commit:     GitHub
CommitDate: Sat Mar 30 15:53:17 2019 +0530

Started a proof that ZZplus passes through the equivalence relation

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

commit 3b8e31523726f596dfd3f73c26acfe978072b5ed
AuthorDate: Sun Mar 24 20:52:23 2019 +0530
Commit:     GitHub
CommitDate: Sun Mar 24 20:52:23 2019 +0530

Started defining functions on ZZ1 (please check description)

1. Defined plus for ZZ1
2. Proved that any equivalence relation factors through Equality
3. Proved that component wise equality is enough of Product types

Code/Product_Type_Eq.idr | 17 +++++++++++++++++
Code/Quotient_Type.idr   |  8 ++++++++
Code/ZZ_alt.idr          |  7 ++++++-
Code/ZZplus.idr          | 23 +++++++++++++++++++++++
4 files changed, 54 insertions(+), 1 deletion(-)

commit 787b64c19d1aee48142964437da2605a3ab6bae1
AuthorDate: Sun Mar 24 15:19:00 2019 +0530
Commit:     GitHub
CommitDate: Sun Mar 24 15:19:00 2019 +0530

Added a notion of transportation for quotients.

Code/Quotient_Type.idr | 16 ++++++++++------
1 file changed, 10 insertions(+), 6 deletions(-)

commit 21a046e64952c6f1cbd1278f3d85d62898bd4c98
AuthorDate: Sun Mar 24 14:43:51 2019 +0530
Commit:     GitHub
CommitDate: Sun Mar 24 14:43:51 2019 +0530

Given a definition of a type family from a quotient type

Code/Quotient_Type.idr | 25 +++++++++++++++++++++++--
1 file changed, 23 insertions(+), 2 deletions(-)

commit 322186071d193e5245997f0a91d3a8ca5864a34f
AuthorDate: Sun Mar 24 11:19:09 2019 +0530
Commit:     GitHub
CommitDate: Sun Mar 24 11:19:09 2019 +0530

Given a definition of quotient types and functions between them.

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

AuthorDate: Sun Mar 24 09:53:09 2019 +0530
Commit:     GitHub
CommitDate: Sun Mar 24 09:53:09 2019 +0530

Finished the proof of transitivity

Code/ZZ_alt.idr | 144 +++++++++++++++++++++++++++++++++++++++++++-------------
1 file changed, 110 insertions(+), 34 deletions(-)

AuthorDate: Sun Mar 24 01:01:58 2019 +0530
Commit:     GitHub
CommitDate: Sun Mar 24 01:01:58 2019 +0530

Added an alternate definition of ZZ using quotients.

1. Added an alternate definition of ZZ using quotients.
2. Proved reflexivity and symmetry.
3. Proof is transitivity is going on.

Code/ZZ_alt.idr | 99 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++
1 file changed, 99 insertions(+)

commit ca986f5d96479e1c9149b75cebe2771064b50d19
AuthorDate: Sun Mar 24 00:59:59 2019 +0530
Commit:     GitHub
CommitDate: Sun Mar 24 00:59:59 2019 +0530

Deleted Misplaced file

ZZ_alt.idr | 99 --------------------------------------------------------------
1 file changed, 99 deletions(-)

commit 41e509b2773ea7c9c72a66fed68ba886897bc795
AuthorDate: Sun Mar 24 00:59:24 2019 +0530
Commit:     GitHub
CommitDate: Sun Mar 24 00:59:24 2019 +0530

Added an alternate definition of Integers using quotients.

1. Added an alternate definition of Integer using quotients.
2. Proved reflexivity.
3. Proved Symmetry.
4. Proof of transitivity is going on.

ZZ_alt.idr | 99 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
1 file changed, 99 insertions(+)

commit 26d64f8d1c06f1bc3a2f07ae64fb7b8869f3feb9
AuthorDate: Fri Mar 22 23:00:26 2019 +0530
Commit:     GitHub
CommitDate: Fri Mar 22 23:00:26 2019 +0530

Added a method to parse floating point numbers.

Note - It only takes inputs of the form 'a.bc'(as list of characters) where both a and b are non empty lists of characters in 0 - 9, and c is an arbitrary list of characters.

Code/Scheme_Expressions.idr |   9 +++
Code/Scheme_Parsers.idr     | 161 ++++++++++++++++++++++++++++++++++++++++++++
2 files changed, 170 insertions(+)

commit 3de24a992d743dfe2456c07c587b133b046701be
AuthorDate: Sat Mar 16 01:40:15 2019 +0530
Commit:     GitHub
CommitDate: Sat Mar 16 01:40:15 2019 +0530

Some progress in insertion sort. The code is taking too long to compile.

Code/InsertionHelpers.idr   | 105 ++++++++++++++++
Code/InsertionProof.idr     | 300 ++++++++++++++++++++++++++++++++++++++++++++
Code/InsertionSort.idr      | 142 ---------------------
Code/PermCons.idr           |   4 +-
Code/PermConsProperties.idr |  53 ++++++++
Code/SortingWithProof.idr   |   2 +-
6 files changed, 460 insertions(+), 146 deletions(-)

commit 5dd763d6a2559e62bdbe9e886d7ddd7c219f95b5
AuthorDate: Sat Mar 16 01:11:00 2019 +0530
Commit:     GitHub
CommitDate: Sat Mar 16 01:11:00 2019 +0530

Delete ZZUtils.idr

ZZUtils.idr | 61 -------------------------------------------------------------
1 file changed, 61 deletions(-)

commit 42f7d3f3213f507f91c72d5bf3fafb2cf2423377
AuthorDate: Sat Mar 16 01:10:47 2019 +0530
Commit:     GitHub
CommitDate: Sat Mar 16 01:10:47 2019 +0530

Delete Sign.idr

Sign.idr | 39 ---------------------------------------
1 file changed, 39 deletions(-)

commit c3b339172545a5fe6c10fa26eb1f86fa761d8c48
AuthorDate: Sat Mar 16 01:10:30 2019 +0530
Commit:     GitHub
CommitDate: Sat Mar 16 01:10:30 2019 +0530

Delete Quotient_Group.idr

Quotient_Group.idr | 65 ------------------------------------------------------
1 file changed, 65 deletions(-)

commit 441c8e96f3f8a4822cbe870476973812278c765b
AuthorDate: Sat Mar 16 01:10:15 2019 +0530
Commit:     GitHub
CommitDate: Sat Mar 16 01:10:15 2019 +0530

Delete PermConsProperties.idr

PermConsProperties.idr | 53 --------------------------------------------------
1 file changed, 53 deletions(-)

commit 7e7b6ccaeeeb0cd0f2a5c2e42892d5f959845d23
AuthorDate: Sat Mar 16 01:10:02 2019 +0530
Commit:     GitHub
CommitDate: Sat Mar 16 01:10:02 2019 +0530

Delete Order.idr

Order.idr | 120 --------------------------------------------------------------
1 file changed, 120 deletions(-)

commit 90e70d0a5fa0190b18b3c8010df4a1f4d60c8d88
AuthorDate: Sat Mar 16 01:09:48 2019 +0530
Commit:     GitHub
CommitDate: Sat Mar 16 01:09:48 2019 +0530

Delete Merge.idr

Merge.idr | 179 --------------------------------------------------------------
1 file changed, 179 deletions(-)

commit caac0593b2807b10df74c96af3aef1a2e447935f
AuthorDate: Sat Mar 16 01:09:34 2019 +0530
Commit:     GitHub
CommitDate: Sat Mar 16 01:09:34 2019 +0530

Delete midterm-check.txt

midterm-check.txt | 85 -------------------------------------------------------
1 file changed, 85 deletions(-)

commit d4f5035eb6168a3c31031706628b7a0874ddbd39
AuthorDate: Sat Mar 16 01:09:19 2019 +0530
Commit:     GitHub
CommitDate: Sat Mar 16 01:09:19 2019 +0530

Delete Lecture.NatTree.idr

Lecture.NatTree.idr | 53 -----------------------------------------------------
1 file changed, 53 deletions(-)

commit 9482efa7ce3a226b2f3204286467b0bd2a58b321
AuthorDate: Sat Mar 16 01:09:03 2019 +0530
Commit:     GitHub
CommitDate: Sat Mar 16 01:09:03 2019 +0530

Delete Group.FiniteGenerate.idr

Group.FiniteGenerate.idr | 26 --------------------------
1 file changed, 26 deletions(-)

commit 7a871e29c303aae2f42fb4683a473c56ca43579f
AuthorDate: Sat Mar 16 01:08:50 2019 +0530
Commit:     GitHub
CommitDate: Sat Mar 16 01:08:50 2019 +0530

Delete gcd.idr

gcd.idr | 92 -----------------------------------------------------------------
1 file changed, 92 deletions(-)

commit 725b0d372eb635197910ea0b3c5fbbe1318dc2eb
AuthorDate: Sat Mar 16 01:08:36 2019 +0530
Commit:     GitHub
CommitDate: Sat Mar 16 01:08:36 2019 +0530

Delete ZZ.idr

ZZ.idr | 515 -----------------------------------------------------------------
1 file changed, 515 deletions(-)

commit 23fb43413c76cc6bd08158d4442568e34207db3c
AuthorDate: Sat Mar 16 01:08:23 2019 +0530
Commit:     GitHub
CommitDate: Sat Mar 16 01:08:23 2019 +0530

Delete PermCons.idr

PermCons.idr | 247 -----------------------------------------------------------
1 file changed, 247 deletions(-)

commit 0fa8593bae6dda1d79de375fa99c4bc6c95ec640
AuthorDate: Sat Mar 16 01:08:12 2019 +0530
Commit:     GitHub
CommitDate: Sat Mar 16 01:08:12 2019 +0530

Delete Ring.idr

Ring.idr | 153 ---------------------------------------------------------------
1 file changed, 153 deletions(-)

commit 505a3f768944ceb1343d59a85eaff29912966e60
AuthorDate: Sat Mar 16 01:08:00 2019 +0530
Commit:     GitHub
CommitDate: Sat Mar 16 01:08:00 2019 +0530

Delete Lists.idr

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

commit 7418f44f1fe8c5fbbe5be9389663e074e38ebe69
AuthorDate: Sat Mar 16 01:07:48 2019 +0530
Commit:     GitHub
CommitDate: Sat Mar 16 01:07:48 2019 +0530

Delete Group_property.idr

Group_property.idr | 129 -----------------------------------------------------
1 file changed, 129 deletions(-)

commit cd6bf282e535d13c0a03eb8db7a33895339238dc
AuthorDate: Sat Mar 16 01:07:35 2019 +0530
Commit:     GitHub
CommitDate: Sat Mar 16 01:07:35 2019 +0530

Delete Lecture.RecRule.idr

Lecture.RecRule.idr | 46 ----------------------------------------------
1 file changed, 46 deletions(-)

AuthorDate: Sat Mar 16 01:07:24 2019 +0530
Commit:     GitHub
CommitDate: Sat Mar 16 01:07:24 2019 +0530

Delete NatUtils.idr

NatUtils.idr | 233 -----------------------------------------------------------
1 file changed, 233 deletions(-)

commit fa2f962cc7a9f3f5b106e7fc8a6dd5178cb96ffa
AuthorDate: Sat Mar 16 01:07:12 2019 +0530
Commit:     GitHub
CommitDate: Sat Mar 16 01:07:12 2019 +0530

Delete Matrix.idr

Matrix.idr | 56 --------------------------------------------------------
1 file changed, 56 deletions(-)

commit 9a17dfc7ce2a82ce17ddb91d7873c3172062ebf7
AuthorDate: Sat Mar 16 01:07:01 2019 +0530
Commit:     GitHub
CommitDate: Sat Mar 16 01:07:01 2019 +0530

Delete Quicksort.idr

Quicksort.idr | 13 -------------
1 file changed, 13 deletions(-)

AuthorDate: Sat Mar 16 01:06:52 2019 +0530
Commit:     GitHub
CommitDate: Sat Mar 16 01:06:52 2019 +0530

Delete SortingWithProof.idr

SortingWithProof.idr | 37 -------------------------------------
1 file changed, 37 deletions(-)

commit 18451ca10c162b940bab04bb400ce74baab9d179
AuthorDate: Sat Mar 16 01:06:42 2019 +0530
Commit:     GitHub
CommitDate: Sat Mar 16 01:06:42 2019 +0530

Delete congruence.idr

congruence.idr | 6 ------
1 file changed, 6 deletions(-)

commit 1f3d8a2620e01a3aa336c809aea0773df2b68e89
AuthorDate: Sat Mar 16 01:06:20 2019 +0530
Commit:     GitHub
CommitDate: Sat Mar 16 01:06:20 2019 +0530

Delete MultiSolver.idr

MultiSolver.idr | 184 --------------------------------------------------------
1 file changed, 184 deletions(-)

commit e429cea2c52465f52acf37f901f15849133a4182
AuthorDate: Sat Mar 16 01:06:09 2019 +0530
Commit:     GitHub
CommitDate: Sat Mar 16 01:06:09 2019 +0530

Delete Lecture.Tuple.idr

Lecture.Tuple.idr | 12 ------------
1 file changed, 12 deletions(-)

commit 4527e2f628b2c6bab6aa24b9f5e72e09eafbe6df
AuthorDate: Sat Mar 16 01:05:56 2019 +0530
Commit:     GitHub
CommitDate: Sat Mar 16 01:05:56 2019 +0530

Delete FinUtils.idr

FinUtils.idr | 39 ---------------------------------------
1 file changed, 39 deletions(-)

commit a55787bb23de297ef2c725500303d51f631e6091
AuthorDate: Sat Mar 16 01:05:46 2019 +0530
Commit:     GitHub
CommitDate: Sat Mar 16 01:05:46 2019 +0530

Delete Linear.idr

Linear.idr | 129 -------------------------------------------------------------
1 file changed, 129 deletions(-)

commit fa078f2f4159b96f619eca9cf0a72e7d18a91902
AuthorDate: Sat Mar 16 01:05:34 2019 +0530
Commit:     GitHub
CommitDate: Sat Mar 16 01:05:34 2019 +0530

Delete InsertionHelpers.idr

InsertionHelpers.idr | 105 ---------------------------------------------------
1 file changed, 105 deletions(-)

commit d657210facac571fbb66998b59e11bb24f44b392
AuthorDate: Sat Mar 16 01:05:23 2019 +0530
Commit:     GitHub
CommitDate: Sat Mar 16 01:05:23 2019 +0530

Delete LinearAlgebra.idr

LinearAlgebra.idr | 210 ------------------------------------------------------
1 file changed, 210 deletions(-)

commit 4a89aab897f5519a95281c5d9e563ecfb49cb7e7
AuthorDate: Sat Mar 16 01:05:07 2019 +0530
Commit:     GitHub
CommitDate: Sat Mar 16 01:05:07 2019 +0530

Delete Primes.idr

Primes.idr | 361 -------------------------------------------------------------
1 file changed, 361 deletions(-)

commit 98bbbe75dfacf0a0987ac05e80ab51f72ffbfbcd
AuthorDate: Sat Mar 16 01:04:55 2019 +0530
Commit:     GitHub
CommitDate: Sat Mar 16 01:04:55 2019 +0530

Delete NatOrder.idr

NatOrder.idr | 229 -----------------------------------------------------------
1 file changed, 229 deletions(-)

commit 23270b252cb840e7180545fc4e7d604d4a9bc7d5
AuthorDate: Sat Mar 16 01:04:44 2019 +0530
Commit:     GitHub
CommitDate: Sat Mar 16 01:04:44 2019 +0530

Delete Lecture.Intro.idr

Lecture.Intro.idr | 58 -------------------------------------------------------
1 file changed, 58 deletions(-)

commit 6d9be75e65819738d9153dc41edfc4310519cec4
AuthorDate: Sat Mar 16 01:04:34 2019 +0530
Commit:     GitHub
CommitDate: Sat Mar 16 01:04:34 2019 +0530

Delete LectureEvens.idr

LectureEvens.idr | 88 --------------------------------------------------------
1 file changed, 88 deletions(-)

commit c27239c6187a697b5b52ee11de794b20031661e9
AuthorDate: Sat Mar 16 01:04:22 2019 +0530
Commit:     GitHub
CommitDate: Sat Mar 16 01:04:22 2019 +0530

Delete Lecture.GCD.idr

Lecture.GCD.idr | 20 --------------------
1 file changed, 20 deletions(-)

commit 85e3b59f26b994eb70c1b0f9077065051a476e3a
AuthorDate: Sat Mar 16 01:04:09 2019 +0530
Commit:     GitHub
CommitDate: Sat Mar 16 01:04:09 2019 +0530

Delete Graph_alt.idr.fixme

Graph_alt.idr.fixme | 45 ---------------------------------------------
1 file changed, 45 deletions(-)

AuthorDate: Sat Mar 16 01:03:58 2019 +0530
Commit:     GitHub
CommitDate: Sat Mar 16 01:03:58 2019 +0530

Delete Group_kernel.idr

Group_kernel.idr | 32 --------------------------------
1 file changed, 32 deletions(-)

commit 9d0daa332a193a87d49e08d1cd925d9fb91333df
AuthorDate: Sat Mar 16 01:03:46 2019 +0530
Commit:     GitHub
CommitDate: Sat Mar 16 01:03:46 2019 +0530

Delete Monoid.idr

Monoid.idr | 36 ------------------------------------
1 file changed, 36 deletions(-)

commit b7562bf667ac4b57d8f70a2935c1071bfc20c80a
AuthorDate: Sat Mar 16 00:43:33 2019 +0530
Commit:     GitHub
CommitDate: Sat Mar 16 00:43:33 2019 +0530

Delete Graphexamples.idr

Graphexamples.idr | 33 ---------------------------------
1 file changed, 33 deletions(-)

commit 47cd0fbed0ae4453f3d8eb55c23836b7cc739b3c
AuthorDate: Sat Mar 16 00:43:20 2019 +0530
Commit:     GitHub
CommitDate: Sat Mar 16 00:43:20 2019 +0530

Delete InsertionProof.idr

InsertionProof.idr | 295 -----------------------------------------------------
1 file changed, 295 deletions(-)

AuthorDate: Sat Mar 16 00:43:08 2019 +0530
Commit:     GitHub
CommitDate: Sat Mar 16 00:43:08 2019 +0530

Delete GroupCosets.idr

GroupCosets.idr | 45 ---------------------------------------------
1 file changed, 45 deletions(-)

commit ae9d04f3764924287bb76e6ef5ef92db0d180876
AuthorDate: Sat Mar 16 00:42:54 2019 +0530
Commit:     GitHub
CommitDate: Sat Mar 16 00:42:54 2019 +0530

Delete Insertion_backup

Insertion_backup | 163 -------------------------------------------------------
1 file changed, 163 deletions(-)

commit f06494de35956ecd5cdab10519ac114f23e49318
AuthorDate: Sat Mar 16 00:42:42 2019 +0530
Commit:     GitHub
CommitDate: Sat Mar 16 00:42:42 2019 +0530

Delete DecOrderNat.idr

DecOrderNat.idr | 24 ------------------------
1 file changed, 24 deletions(-)

commit 1376dd88d0891e23103ea86cd1bed157be8e186a
AuthorDate: Sat Mar 16 00:42:28 2019 +0530
Commit:     GitHub
CommitDate: Sat Mar 16 00:42:28 2019 +0530

Delete DetDec.idr

DetDec.idr | 12 ------------
1 file changed, 12 deletions(-)

commit 51772eacf4e66da1c1408fb59baafa71d5e7b141
AuthorDate: Sat Mar 16 00:41:49 2019 +0530
Commit:     GitHub
CommitDate: Sat Mar 16 00:41:49 2019 +0530

Delete Ring.Properties.idr

Ring.Properties.idr | 40 ----------------------------------------
1 file changed, 40 deletions(-)

commit f883fe9650c6157973714559416894995403310e
AuthorDate: Sat Mar 16 00:41:32 2019 +0530
Commit:     GitHub
CommitDate: Sat Mar 16 00:41:32 2019 +0530

Delete Graph_alt.idr

Graph_alt.idr | 45 ---------------------------------------------
1 file changed, 45 deletions(-)

commit a9c3978a7bb9069672e155f0d08a4ed4f885543c
AuthorDate: Sat Mar 16 00:41:14 2019 +0530
Commit:     GitHub
CommitDate: Sat Mar 16 00:41:14 2019 +0530

Delete Group_property2.idr

Group_property2.idr | 81 -----------------------------------------------------
1 file changed, 81 deletions(-)

commit 3fa2b1c7681b8663978425372b1b5cb5f51f5fe7
AuthorDate: Sat Mar 16 00:41:03 2019 +0530
Commit:     GitHub
CommitDate: Sat Mar 16 00:41:03 2019 +0530

Delete GroupCosetRep.idr

GroupCosetRep.idr | 29 -----------------------------
1 file changed, 29 deletions(-)

commit d456c43aafbbeeb0e46097f026641d7b3a288265
AuthorDate: Sat Mar 16 00:40:52 2019 +0530
Commit:     GitHub
CommitDate: Sat Mar 16 00:40:52 2019 +0530

Delete Group.idr

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

commit 2f24946b38d8e26973f315474a985b3a36e71068
AuthorDate: Sat Mar 16 00:40:34 2019 +0530
Commit:     GitHub
CommitDate: Sat Mar 16 00:40:34 2019 +0530

Delete pigeonhole.idr

pigeonhole.idr | 91 ----------------------------------------------------------
1 file changed, 91 deletions(-)

commit ea7519ca7073ba7e115875a8a7bfe621d926d227
AuthorDate: Sat Mar 16 00:38:59 2019 +0530
Commit:     GitHub
CommitDate: Sat Mar 16 00:38:59 2019 +0530

Delete InsertionSort.idr

InsertionSort.idr | 59 -------------------------------------------------------
1 file changed, 59 deletions(-)

commit 3b499e04acac2480a488c645a88545dba7e77c57
AuthorDate: Sat Mar 16 00:38:47 2019 +0530
Commit:     GitHub
CommitDate: Sat Mar 16 00:38:47 2019 +0530

Delete fn_to_vect.idr

fn_to_vect.idr | 74 ----------------------------------------------------------
1 file changed, 74 deletions(-)

AuthorDate: Sat Mar 16 00:38:31 2019 +0530
Commit:     GitHub
CommitDate: Sat Mar 16 00:38:31 2019 +0530

Delete Choice.idr

Choice.idr | 3 ---
1 file changed, 3 deletions(-)

commit d5593d8039a646d36dd72eca831a8459c4e27381
AuthorDate: Sat Mar 16 00:38:19 2019 +0530
Commit:     GitHub
CommitDate: Sat Mar 16 00:38:19 2019 +0530

Delete bezout.idr

bezout.idr | 204 -------------------------------------------------------------
1 file changed, 204 deletions(-)

commit 2abfba7fb7b88d7c228e90d6bcc517b05aa1df4b
AuthorDate: Sat Mar 16 00:36:58 2019 +0530
Commit:     GitHub
CommitDate: Sat Mar 16 00:36:58 2019 +0530

Delete Field.idr

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

commit 4fb777c530248ebe6ee6007e73c62230714efd23
AuthorDate: Sat Mar 16 00:14:42 2019 +0530
Commit:     GitHub
CommitDate: Sat Mar 16 00:14:42 2019 +0530

Delete Finite.idr

Finite.idr | 36 ------------------------------------
1 file changed, 36 deletions(-)

commit cf53c4ebe8702e49a241de0a4689dc519dd2ec9e
AuthorDate: Sat Mar 16 00:14:29 2019 +0530
Commit:     GitHub
CommitDate: Sat Mar 16 00:14:29 2019 +0530

Delete Rationals.idr

Rationals.idr | 119 ----------------------------------------------------------
1 file changed, 119 deletions(-)

commit afd0d7a1744c243f86d5404de6220dbcdb4c1b40
AuthorDate: Sat Mar 16 00:14:17 2019 +0530
Commit:     GitHub
CommitDate: Sat Mar 16 00:14:17 2019 +0530

Delete LTE_Properties.idr

LTE_Properties.idr | 15 ---------------
1 file changed, 15 deletions(-)

commit b8373108268720f69526d5af6b7352fa6d44eac6
AuthorDate: Sat Mar 16 00:14:06 2019 +0530
Commit:     GitHub
CommitDate: Sat Mar 16 00:14:06 2019 +0530

Delete Group_property3.idr

Group_property3.idr | 47 -----------------------------------------------
1 file changed, 47 deletions(-)

commit f439e0db70b64e4d07a40cfc276341ce3e49fff6
AuthorDate: Sat Mar 16 00:13:54 2019 +0530
Commit:     GitHub
CommitDate: Sat Mar 16 00:13:54 2019 +0530

Delete Divisors.idr

Divisors.idr | 193 -----------------------------------------------------------
1 file changed, 193 deletions(-)

commit dd86a78d55b7774831a19116a52e2f7b7cc07451
AuthorDate: Sat Mar 16 00:13:43 2019 +0530
Commit:     GitHub
CommitDate: Sat Mar 16 00:13:43 2019 +0530

Deleted Misplaced File

GCDZZ.idr | 52 ----------------------------------------------------
1 file changed, 52 deletions(-)

commit d36f88d47d1681f3abe8c7ac8b3a8881fa8c88f6
AuthorDate: Sat Mar 16 00:13:31 2019 +0530
Commit:     GitHub
CommitDate: Sat Mar 16 00:13:31 2019 +0530

Deleted Misplaced File

Graph.idr | 142 --------------------------------------------------------------
1 file changed, 142 deletions(-)

commit 59aee1c9b59b3da69b3296c4e0506f33e9c4084d
AuthorDate: Sat Mar 16 00:13:18 2019 +0530
Commit:     GitHub
CommitDate: Sat Mar 16 00:13:18 2019 +0530

Deleted Misplaced File

Bezout.idr | 155 -------------------------------------------------------------
1 file changed, 155 deletions(-)

commit 5e1c35c97614cc87e9e4d851f88c050f19edcc40
AuthorDate: Sat Mar 16 00:13:05 2019 +0530
Commit:     GitHub
CommitDate: Sat Mar 16 00:13:05 2019 +0530

Deleted Misplaced File

FreeGroup.idr | 1 -
1 file changed, 1 deletion(-)

commit 34d7de4a9889d4089898c2bdc5d0f347f5ed4da0
AuthorDate: Sat Mar 16 00:11:25 2019 +0530
Commit:     GitHub
CommitDate: Sat Mar 16 00:11:25 2019 +0530

Deleted Misplaced File

BaseN.idr | 151 --------------------------------------------------------------
1 file changed, 151 deletions(-)

AuthorDate: Sat Mar 16 00:10:18 2019 +0530
Commit:     GitHub
CommitDate: Sat Mar 16 00:10:18 2019 +0530

Deleted Misplaces File

All_is_Refl.idr | 5 -----
1 file changed, 5 deletions(-)

commit 6452dccf43053e64a8bb7f7fdfd1e9bbb3e64510
AuthorDate: Sat Mar 16 00:09:50 2019 +0530
Commit:     GitHub
CommitDate: Sat Mar 16 00:09:50 2019 +0530

Deleted Misplaced file

Permutation.idr | 59 ---------------------------------------------------------
1 file changed, 59 deletions(-)

commit 611fdc4d78357d6da8fe1cea2d98d6f8c8809c65
AuthorDate: Sat Mar 16 00:05:28 2019 +0530
Commit:     GitHub
CommitDate: Sat Mar 16 00:05:28 2019 +0530

Some progress in insertionSort

Idris is taking too long to run the code

All_is_Refl.idr          |   5 +
BaseN.idr                | 151 ++++++++++++++
Bezout.idr               | 155 ++++++++++++++
Choice.idr               |   3 +
DecOrderNat.idr          |  24 +++
DetDec.idr               |  12 ++
Divisors.idr             | 193 ++++++++++++++++++
Field.idr                |  30 +++
FinUtils.idr             |  39 ++++
Finite.idr               |  36 ++++
FreeGroup.idr            |   1 +
GCDZZ.idr                |  52 +++++
Graph.idr                | 142 +++++++++++++
Graph_alt.idr            |  45 +++++
Graph_alt.idr.fixme      |  45 +++++
Graphexamples.idr        |  33 +++
Group.FiniteGenerate.idr |  26 +++
Group.idr                |  93 +++++++++
GroupCosetRep.idr        |  29 +++
GroupCosets.idr          |  45 +++++
Group_kernel.idr         |  32 +++
Group_property.idr       | 129 ++++++++++++
Group_property2.idr      |  81 ++++++++
Group_property3.idr      |  47 +++++
InsertionHelpers.idr     | 105 ++++++++++
InsertionProof.idr       | 295 +++++++++++++++++++++++++++
InsertionSort.idr        |  59 ++++++
Insertion_backup         | 163 +++++++++++++++
LTE_Properties.idr       |  15 ++
Lecture.GCD.idr          |  20 ++
Lecture.Intro.idr        |  58 ++++++
Lecture.NatTree.idr      |  53 +++++
Lecture.RecRule.idr      |  46 +++++
Lecture.Tuple.idr        |  12 ++
LectureEvens.idr         |  88 ++++++++
Linear.idr               | 129 ++++++++++++
LinearAlgebra.idr        | 210 +++++++++++++++++++
Lists.idr                |  30 +++
Matrix.idr               |  56 ++++++
Merge.idr                | 179 ++++++++++++++++
Monoid.idr               |  36 ++++
MultiSolver.idr          | 184 +++++++++++++++++
NatOrder.idr             | 229 +++++++++++++++++++++
NatUtils.idr             | 233 +++++++++++++++++++++
Order.idr                | 120 +++++++++++
PermCons.idr             | 247 +++++++++++++++++++++++
PermConsProperties.idr   |  53 +++++
Permutation.idr          |  59 ++++++
Primes.idr               | 361 +++++++++++++++++++++++++++++++++
Quicksort.idr            |  13 ++
Quotient_Group.idr       |  65 ++++++
Rationals.idr            | 119 +++++++++++
Ring.Properties.idr      |  40 ++++
Ring.idr                 | 153 ++++++++++++++
Sign.idr                 |  39 ++++
SortingWithProof.idr     |  37 ++++
ZZ.idr                   | 515 +++++++++++++++++++++++++++++++++++++++++++++++
ZZUtils.idr              |  61 ++++++
congruence.idr           |   6 +
fn_to_vect.idr           |  74 +++++++
gcd.idr                  |  92 +++++++++
midterm-check.txt        |  85 ++++++++
pigeonhole.idr           |  91 +++++++++
63 files changed, 5878 insertions(+)

AuthorDate: Fri Mar 8 22:38:12 2019 +0530
Commit:     GitHub
CommitDate: Fri Mar 8 22:38:12 2019 +0530

Code/InsertionSort.idr | 109 +++++++++++++++++++++++++++++++++++++++++++------
1 file changed, 97 insertions(+), 12 deletions(-)

commit 2d12be6bd2b092af54762751ed43864f49ae6cbf
AuthorDate: Fri Mar 8 02:26:11 2019 +0530
Commit:     GitHub
CommitDate: Fri Mar 8 02:26:11 2019 +0530

Added some methods in sorting(see description)

1. Started a proof based sorting.
2. Having problem with using case _ of
3. Gave proofs that LTE is reflexive and transitive

Code/DecOrderNat.idr      | 24 ++++++++++++
Code/InsertionSort.idr    | 93 +++++++++++++++++++++++++++++++++++++++++++----
Code/LTE_Properties.idr   | 15 ++++++++
Code/SortingWithProof.idr |  3 +-
4 files changed, 126 insertions(+), 9 deletions(-)

commit d9221e207abcc9752b932207f17daae0474736e9
AuthorDate: Thu Mar 7 21:51:25 2019 +0530
Commit:     GitHub
CommitDate: Thu Mar 7 21:51:25 2019 +0530

A proof that every loop is equal to Refl (as suggested by Prof. Gadgil)

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

AuthorDate: Thu Mar 7 02:49:07 2019 +0530
Commit:     GitHub
CommitDate: Thu Mar 7 02:49:07 2019 +0530

Proved that permutations defined using constructors are bijections

Code/PermCons.idr | 206 +++++++++++++++++++++++++++++++++++-------------------
1 file changed, 134 insertions(+), 72 deletions(-)

commit 22d03d6d28e90fb6346ef3a9ec4c3df32407794a
AuthorDate: Wed Mar 6 02:57:29 2019 +0530
Commit:     GitHub
CommitDate: Wed Mar 6 02:57:29 2019 +0530

Gave some methods for permutations

Code/PermCons.idr | 181 +++++++++++++++++++++++++++++++++++++++++++++++++++---
1 file changed, 173 insertions(+), 8 deletions(-)

commit 9d37b0d02dde56199216715c824bd350ba46f899
AuthorDate: Wed Feb 27 23:44:06 2019 +0530
Commit:     GitHub
CommitDate: Wed Feb 27 23:44:06 2019 +0530

Proved that for a group a*b = c implies b = inv(a) * c.

Code/Group_property2.idr | 13 ++++---------
Code/Group_property3.idr | 47 +++++++++++++++++++++++++++++++++++++++++++++++
2 files changed, 51 insertions(+), 9 deletions(-)

AuthorDate: Tue Feb 26 11:03:56 2019 +0530
Commit:     GitHub
CommitDate: Tue Feb 26 11:03:56 2019 +0530

Syncing

Code/BaseN.idr                | 177 +++++++++++++--------
Code/Bezout.idr               |  57 +++----
Code/Divisors.idr             | 175 +++++++++++++++-----
Code/FinUtils.idr             |  39 +++++
Code/GCDZZ.idr                |  52 ++++++
Code/Graph.idr                |  93 +++++++++--
Code/Graph_alt.idr.fixme      |  45 ++++++
Code/Graphexamples.idr        |   2 +-
Code/Group.FiniteGenerate.idr |  26 +++
Code/Group.idr                |  50 ++----
Code/GroupCosetRep.idr        |  29 ++++
Code/GroupCosets.idr          |  45 ++++++
Code/Group_property2.idr      |   2 +-
Code/InsertionSort.idr        |  29 +++-
Code/LectureEvens.idr         |  88 ++++++++++
Code/Linear.idr               |  34 +++-
Code/LinearAlgebra.idr        |  97 +++++++++++-
Code/Lists.idr                |  30 ++++
Code/Merge.idr                | 200 +++++++++++++++++------
Code/MultiSolver.idr          |   2 +-
Code/NatOrder.idr             | 229 +++++++++++++++++++++++++++
Code/NatUtils.idr             | 277 ++++++++++++++++++++++++++------
Code/Order.idr                | 120 ++++++++++++++
Code/Primes.idr               | 361 ++++++++++++++++++++++++++++++++++++++++++
Code/Quotient_Group.idr       |  77 ++++-----
Code/Rationals.idr            |   4 -
Code/Ring.Properties.idr      |  40 +++++
Code/Ring.idr                 | 147 ++++++++++++++---
Code/SortingWithProof.idr     |  34 ++--
Code/ZZ.idr                   |  90 +++++++----
Code/ZZUtils.idr              |  61 +++++++
Code/check-all.sh             |   5 +
Code/gcd.idr                  | 151 +++++++++---------
Code/midterm-check.txt        |  85 ++++++++++
34 files changed, 2463 insertions(+), 490 deletions(-)

commit ccca3992434f94bb3a4085ec97651c7fe2736572
AuthorDate: Tue Feb 26 10:41:37 2019 +0530
Commit:     GitHub
CommitDate: Tue Feb 26 10:41:37 2019 +0530

AuthorDate: Tue Feb 26 10:41:02 2019 +0530
Commit:     GitHub
CommitDate: Tue Feb 26 10:41:02 2019 +0530

commit a9730da6b6a3607eae7c9ec225b1bb45b31f6c76
AuthorDate: Tue Feb 26 10:40:17 2019 +0530
Commit:     GitHub
CommitDate: Tue Feb 26 10:40:17 2019 +0530

Defined Some basic methods for graphs

Code/Graph.idr  | 93 ++++++++-------------------------------------------------
Code/Matrix.idr | 56 ++++++++++++++++++++++++++++++++++
2 files changed, 69 insertions(+), 80 deletions(-)

AuthorDate: Sat Feb 23 15:57:45 2019 +0530
Commit:     GitHub
CommitDate: Sat Feb 23 15:57:45 2019 +0530

started a proof of pigeonhole principle

Code/pigeonhole.idr | 80 +++++++++++++++++++++++++++++++++++++++++++++++++++++
1 file changed, 80 insertions(+)

commit 515d7e6f0128a7143e70e0e5d37c935b8a741584
AuthorDate: Sat Feb 23 00:25:43 2019 +0530
Commit:     GitHub
CommitDate: Sat Feb 23 00:25:43 2019 +0530

Some basics methods on graphs

Code/Graph_alt.idr | 45 +++++++++++++++++++++++++++++++++++++++++++++
1 file changed, 45 insertions(+)

commit 08d30b2885f0abb37e1cd550b6f4c0b982041a7f
AuthorDate: Fri Feb 22 22:36:19 2019 +0530
Commit:     GitHub
CommitDate: Fri Feb 22 22:36:19 2019 +0530

Added a method to convert functions to vectors.

Code/fn_to_vect.idr | 74 +++++++++++++++++++++++++++++++++++++++++++++++++++++
1 file changed, 74 insertions(+)

commit b62debd1b054cb8227abd7ce8c456a954d62c548
AuthorDate: Fri Feb 22 22:34:15 2019 +0530
Commit:     GitHub
CommitDate: Fri Feb 22 22:34:15 2019 +0530

Deleted misplaced file

fn_to_vect.idr | 74 ----------------------------------------------------------
1 file changed, 74 deletions(-)

AuthorDate: Fri Feb 22 22:33:47 2019 +0530
Commit:     GitHub
CommitDate: Fri Feb 22 22:33:47 2019 +0530

Uploaded a method to convert functions to vectors and back.

fn_to_vect.idr | 74 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
1 file changed, 74 insertions(+)

commit e1da1ae775eaaedb227c8e2a640659e19bf43f52
AuthorDate: Thu Feb 14 10:52:52 2019 +0530
Commit:     GitHub
CommitDate: Thu Feb 14 10:52:52 2019 +0530

updated report file

_reports/arka/arka.md | 62 ++++++++++++++++++++++++++++++++++++++++++++++++++-
1 file changed, 61 insertions(+), 1 deletion(-)

commit 0932f51f086b75d19e26eb296d6e50ff5101dc5e
AuthorDate: Thu Feb 14 10:49:37 2019 +0530
Commit:     GitHub
CommitDate: Thu Feb 14 10:49:37 2019 +0530

Finished property 8. Started proving properties of Cosets

Code/Group.idr           | 95 ++++++++++++++++--------------------------------
Code/Group_property.idr  | 56 +---------------------------
Code/Group_property2.idr | 86 +++++++++++++++++++++++++++++++++++++++++++
Code/Quotient_Group.idr  | 35 +++++++++++++++++-
4 files changed, 152 insertions(+), 120 deletions(-)

commit ef9f6d860d4f73112ca89938bdcc683486fb5e20
AuthorDate: Thu Feb 14 10:48:24 2019 +0530
Commit:     GitHub
CommitDate: Thu Feb 14 10:48:24 2019 +0530

Delete Ring.idr

Ring.idr | 48 ------------------------------------------------
1 file changed, 48 deletions(-)

commit a92809a0d69707ce8688656a8b9028267fa9c0a9
AuthorDate: Thu Feb 14 10:48:13 2019 +0530
Commit:     GitHub
CommitDate: Thu Feb 14 10:48:13 2019 +0530

Delete Group_property2.idr

Group_property2.idr | 86 -----------------------------------------------------
1 file changed, 86 deletions(-)

commit 05011a0463d430396b26b6a6bb45eb1a8d83509b
AuthorDate: Thu Feb 14 10:48:03 2019 +0530
Commit:     GitHub
CommitDate: Thu Feb 14 10:48:03 2019 +0530

Delete Group_property.idr

Group_property.idr | 129 -----------------------------------------------------
1 file changed, 129 deletions(-)

commit f0088e6e1ae14dee2ff62af84445bebeea37672c
AuthorDate: Thu Feb 14 10:47:53 2019 +0530
Commit:     GitHub
CommitDate: Thu Feb 14 10:47:53 2019 +0530

Delete Quotient_Group.idr

Quotient_Group.idr | 72 ------------------------------------------------------
1 file changed, 72 deletions(-)

commit 0438d8f008737dee4db6a4cc26e32d0f21e0fdc9
AuthorDate: Thu Feb 14 10:47:42 2019 +0530
Commit:     GitHub
CommitDate: Thu Feb 14 10:47:42 2019 +0530

Delete Monoid.idr

Monoid.idr | 36 ------------------------------------
1 file changed, 36 deletions(-)

commit 051be30b5b7dc64b8b2474d22fd587470c617383
AuthorDate: Thu Feb 14 10:47:31 2019 +0530
Commit:     GitHub
CommitDate: Thu Feb 14 10:47:31 2019 +0530

Delete Group.idr

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

commit aec202e2dd3bb7a3344ccc1cd01325f6ff852f25
AuthorDate: Thu Feb 14 10:47:20 2019 +0530
Commit:     GitHub
CommitDate: Thu Feb 14 10:47:20 2019 +0530

Delete Choice.idr

Choice.idr | 3 ---
1 file changed, 3 deletions(-)

commit 6c3ef31672a661f37c26dc36c909c58dbf4c9842
AuthorDate: Thu Feb 14 10:47:11 2019 +0530
Commit:     GitHub
CommitDate: Thu Feb 14 10:47:11 2019 +0530

Delete congruence.idr

congruence.idr | 6 ------
1 file changed, 6 deletions(-)

commit 0f3477cd11de4966705a29ec14b922a60ed31568
AuthorDate: Thu Feb 14 10:45:08 2019 +0530
Commit:     GitHub
CommitDate: Thu Feb 14 10:45:08 2019 +0530

Finished property_7. Started proving properties of Cosets

Choice.idr          |   3 ++
Group.idr           |  97 +++++++++++++++++++++++++++++++++++++++
Group_property.idr  | 129 ++++++++++++++++++++++++++++++++++++++++++++++++++++
Group_property2.idr |  86 +++++++++++++++++++++++++++++++++++
Monoid.idr          |  36 +++++++++++++++
Quotient_Group.idr  |  72 +++++++++++++++++++++++++++++
Ring.idr            |  48 +++++++++++++++++++
congruence.idr      |   6 +++
8 files changed, 477 insertions(+)

commit 27328963239decafa1f4b329e01f33f8a3f102c1
AuthorDate: Sun Feb 10 23:03:09 2019 +0530
Commit:     GitHub
CommitDate: Sun Feb 10 23:03:09 2019 +0530

Minor changes

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

commit c2d6523360ccc74ecb2b7c9b3e6dc57715786673
AuthorDate: Sun Feb 10 23:00:10 2019 +0530
Commit:     GitHub
CommitDate: Sun Feb 10 23:00:10 2019 +0530

Added a proof that for an element in a group, one sided inverse is the inverse.

Code/Group.idr          |  3 ++-
Code/Group_property.idr | 60 ++++++++++++++++++++++++++++++++++++++++++-------
2 files changed, 54 insertions(+), 9 deletions(-)

commit 68a7e1d329bf3fa3a32e7d7e88157b30263ae294
AuthorDate: Sun Feb 10 14:47:34 2019 +0530
Commit:     GitHub
CommitDate: Sun Feb 10 14:47:34 2019 +0530

Started a proof that f( inv(a)) = inv( f(a))

Code/Group.idr          |  2 +-
Code/Group_property.idr | 61 ++++++++++++++++++++++++++++++++++++++++++++++++-
2 files changed, 61 insertions(+), 2 deletions(-)

commit 0768d716365ce23c89679d362f6191d28735a5f8
AuthorDate: Fri Feb 8 22:39:47 2019 +0530
Commit:     GitHub
CommitDate: Fri Feb 8 22:39:47 2019 +0530

Deleted misplaced file

perm_cons.idr | 20 --------------------
1 file changed, 20 deletions(-)

commit bbb05b601749b1a7e00434d57fd033b474d59567
AuthorDate: Fri Feb 8 22:39:25 2019 +0530
Commit:     GitHub
CommitDate: Fri Feb 8 22:39:25 2019 +0530

Deleted misplaced file

permutation.idr | 59 ---------------------------------------------------------
1 file changed, 59 deletions(-)

commit cc067b2ecc8e738df4c15cfd4eca0565cd940eff
AuthorDate: Fri Feb 8 22:38:59 2019 +0530
Commit:     GitHub
CommitDate: Fri Feb 8 22:38:59 2019 +0530

Deleted misplaced file

sorting_with_proof.idr | 54 --------------------------------------------------
1 file changed, 54 deletions(-)

commit aabf62caef2348b1dfb423c82e5f3c60b63f242e
AuthorDate: Thu Feb 7 18:43:43 2019 +0530
Commit:     GitHub
CommitDate: Thu Feb 7 18:43:43 2019 +0530

Code/Choice.idr         |  3 +++
Code/Group_property.idr | 25 +++++++++++++++++++++++--
Code/congruence.idr     |  6 ++++++
3 files changed, 32 insertions(+), 2 deletions(-)

commit 38e0e7d3c646ea9fee80b38c47c51680abc84f5e
AuthorDate: Thu Feb 7 15:07:31 2019 +0530
Commit:     GitHub
CommitDate: Thu Feb 7 15:07:31 2019 +0530

Added left cancellation law for groups.

Code/Group.idr          |  8 +++++++-
Code/Group_property.idr | 30 +++++++++++++++++++++++++++++-
2 files changed, 36 insertions(+), 2 deletions(-)

commit dc0e820bff69d118aeac360d8128fe49126887bf
AuthorDate: Thu Feb 7 11:22:22 2019 +0530
Commit:     GitHub
CommitDate: Thu Feb 7 11:22:22 2019 +0530

Added uniqueness property for inverses and identity for groups

Code/Group.idr          | 48 ++++++++++++++++--------------------------------
Code/Group_property.idr | 29 +++++++++++++++++++++++++++++
Code/Monoid.idr         | 36 ++++++++++++++++++++++++++++++++++++
Code/Quotient_Group.idr | 41 +++++++++++++++++++++++++++++++++++++++++
4 files changed, 122 insertions(+), 32 deletions(-)

commit bb58463b3ece9b9a4f03530cdcb5052cfc7984e3
AuthorDate: Thu Jan 31 02:02:53 2019 +0530
Commit:     GitHub
CommitDate: Thu Jan 31 02:02:53 2019 +0530

Added definition of commutative rings with identity.

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

commit 0ee2f48e2700ff701aab0c39fb8e29bc56e902db
AuthorDate: Wed Jan 30 18:47:58 2019 +0530
Commit:     GitHub
CommitDate: Wed Jan 30 18:47:58 2019 +0530

Added a definition of rings in Rings.idr. Created a separate file for monoids.

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

AuthorDate: Wed Jan 30 17:34:42 2019 +0530
Commit:     GitHub
CommitDate: Wed Jan 30 17:34:42 2019 +0530

Some minor changes and addition in Groups.idr

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

commit 92e36c301d27377fea7165ea5e5bf2fbe3f47248
AuthorDate: Sat Jan 26 00:36:30 2019 +0530
Commit:     GitHub
CommitDate: Sat Jan 26 00:36:30 2019 +0530

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

commit 37bfac50bf94c8ae7e0e46b4807bcc95d435a667
AuthorDate: Fri Jan 25 22:50:25 2019 +0530
Commit:     GitHub
CommitDate: Fri Jan 25 22:50:25 2019 +0530

Divided the code into four files
1. Finite.idr - Defined the type Finite n(Finite set of n elements). It is same as the Fin except the 'n' is made explicit
2. perm_cons.idr - Defined permutation with constructors.
3. permutation.idr - Defined permutation as bijections
4. sorting_with_proof - Defined the required SortedVect type
Please check the documentations for explanations.

Code/Finite.idr             | 36 +++++++++++++++++++
Code/perm_cons.idr          | 22 ++++++++++++
Code/permutation.idr        | 59 +++++++++++++++++++++++++++++++
Code/sorting_with_proof.idr | 86 +++++++++++++--------------------------------
4 files changed, 141 insertions(+), 62 deletions(-)

commit b523f3d0518e18f068d3eeefd73614e13c635721
AuthorDate: Thu Jan 24 14:19:07 2019 +0530
Commit:     GitHub
CommitDate: Thu Jan 24 14:19:07 2019 +0530

Added definition of Permutation using constructors (in the file perm_cons).

perm_cons.idr          | 20 ++++++++++++++++++++
permutation.idr        |  6 ------
sorting_with_proof.idr |  1 +
3 files changed, 21 insertions(+), 6 deletions(-)

commit 41b4b66608180d9ce5217bd929f9a217c5004531
AuthorDate: Thu Jan 24 12:31:04 2019 +0530
Commit:     GitHub
CommitDate: Thu Jan 24 12:31:04 2019 +0530

Created a different file to deal with permutations.
Applying a permutation is getting too complicated.

permutation.idr        | 65 ++++++++++++++++++++++++++++++++++++++++++++++++++
sorting_with_proof.idr | 53 ++++++++++++++++++++++++++++++++++++++++
2 files changed, 118 insertions(+)

commit b0e48d69d487d4384481f5b1f19485210ee82bdb