Project Report for Logic, Types, Spaces 2019

Abishek Rajan

Outline of the work done

MA 210 : Final Report

Sorting

I implemented the insertion sort algorithm.

Files: InsertionSort.idr, VectPerm.idr

Everything is total in InsertionSort.idr and VectPerm.idr.

  1. I defined the Insert function which takes a natural number, a sorted list, and adds it into its appropriate position in the list by comparison.
  2. Using this, I implemented the algorithm through the function Sort. Link Here
  3. In the function CheckSortedVect, I implemented a Boolean test to check if a Vector is Sorted. This will be upgraded to a proof. Link Here
  4. For working on permutations, I implemented a function which behaves like the elem function (which checks for membership of an element in a list or Vector), but with proof, called improveElem. Using this, I compared vectors and found all instances of a particular element of a Vector x in another Vector y with proof with findIn.
  5. Using the above, I implemented functions which remove an element from a position given a proof that it is at that position removeElem.
  6. Using this, I implemented some Boolean tests to check whether a Vector is a permutation of another Vector in recursiveTest and `listDifference’.
  7. In the case where two Vectors have the same elements, the function PermutationBijection produces the permutation which takes the Vector x to the Vector y. Link Here (contains everything for items 4-7).

Remaining

Although the permutation problem is done, integrating it with the sortedness is very difficult.

Linear Algebra

One Variable Equations

I solved linear equations in one variable with proof.

Everything is total in Linear.idr.

File: Linear.idr

  1. I found with proof that the equation ax = 0 has the solution x = (0,1) when a is not zero in trivialeqSolver.Link Here
  2. I found with proof that the equation ax + b = 0 has the solution x = (-b,a) when a,b are not zero in eqSolver.Link Here
  3. I found with proof that the equation ax + b = c has the solution x = (c-b,a) when a,b,c are not zero in GeneralEqSolver. Link Here
  4. I checked whether a Diophantine equation in one variable has an integer solution in the function IsSolutionZ. Link Here

All of the above functions include proofs that the solution (a rational number) is a valid number (nonzero denominator).

Each of these functions had their own associated helper functions to transition between proofs of equalities.

Diophantine Equations

File: TwoVarDiophEq.idr

Everything is total in TwoVarDiophEq.idr.

The work on two variable Diophantine equations was done in collaboration with Shafil (who had already proven the Bezout Identity).

  1. I found with proof whether or not the equation ax + b = c has an integer solution using the function DiophantineSolver. Thus, linear Diophantine equations in one variable are complete.
  2. For the two variable case, the function homogeneous is a helper function which transitions between proofs of equalities in the homogeneous case of the two variable Diophantine equation.
  3. I wrote the function solDifference which along with diffIsHomogeneous proves that if any two pairs satisfy the non-homogeneous equation, then their difference satisfies the homogeneous equation
  4. The function addToSol is a helper function which is used in conjugation with differByHomogeneous (which was done by Shafil, I only defined the function type) to show that any solution is a particular solution + a homogeneous solution.

The Diophantine solver produces a valid rational solution of the equation in case it has no integer solution.

Remaining

This could possibly be extended to n-variable Diophantine equations.

Linear Systems

File: LinearAlgebra.idr

Everything is total in LinearAlgebra.idr.

I implemented the Gauss-Jordan process which due to its versatility has many applications.

  1. Implemented the basic elementary operations on matrices. Link Here
    1. Swap Rows in Swap_Rows
    2. Scale a Row in Scale_Row
    3. Subtract a multiple of a row from another in Row_Operation
  2. I used these to appropriately convert elements to zero in a matrix with MakeElementZero.
  3. The function MakeColumnZero uses this technique to fill columns with zeroes. Link Here
  4. The function UpperTriangularize is a helper function for UpperTriangularForm which converts a matrix to Upper Triangular Form.Link Here
  5. I found a diagonal form of a matrix using DiagonalForm using the above and extended it to convert any matrix to an identity (if all the diagonal elements are non-zero) in TotalReduce. If not, the zero rows are left as they are while the others are reduced. Link Here
  6. I found the magnitude of the determinant using DetUpToSign on the diagonal form of a matrix. Link Here
  7. Also, as computation time signifcantly increases with larger numbers, I added in some functions, culminating in simplifyMatrix, which convert a matrix to simplified form. Link Here

Remaining

Here are a few possible applications of this process.

  1. Solving linear systems (from upper triangular form, or from diagonal form) with proof.
  2. Calculating the inverse of a matrix (and proving basic facts about it).
  3. Finding the rank of a linear transformation, showing that it is independent of the choice of basis.

Rationals

Files: Rationals.idr, FieldAxioms.idr.

Everything is total in Rationals.idr and FieldAxioms.idr

I implemented the non-unique representation of the rational numbers.

  1. I defined the rational numbers as a type ZZPair (a pair of ZZs, where ZZ is a form of integers over which proofs can be done easily). Link Here
  2. I defined the type for divisibility of Integers isFactorInt which was subsequently renamed for the ZZ type.
  3. Using this, I defined the arithmetic operations and the inclusion of integers into the rationals, with implementation of proofs wherever necessary that denominators/numerators should not be zero. Link Here
  4. I made the function simplifyRational work over all ZZPairs by extending the CalcGCD function to work over pairs of ZZ instead of pairs of Nat. Link Here
  5. I started proofs that the sum of a rational and its additive inverse is the additive identity. Link Here
  6. The function CheckIsQuotientZ checks if the rational number is equivalent to an integer with proof (for example, 12/4 is 3). Link Here
  7. I implemented simplification of rational numbers using a theorem that Shafil proved (dividing two numbers by their GCD makes them coprime) in the function simplifyWithProof which returns a simplified rational along with a proof that it is simplified.
  8. I implemented a type representing equalit of rational numbers EqRat which sets two rational numbers (a,b) (c,d) as equal if ad=bc.
  9. I proved the analogues of reflexivity, symmetry, and transitivity for this type.
    1. EqRatRefl creates an EqRat element of every valid (a,b) (a,b).
    2. EqRatRefl creates an EqRat element of (c,d) (a,b) given an EqRat element of (a,b) (c,d) (the analogue of symmetry)
    3. EqRatTrans creates an EqRat element of (a,b) (e,f) given an EqRat element of (a,b) (c,d) and an EqRat element of (c,d) (e,f). (all of the constructions are done only in the case of valid rational numbers).
  10. Using the above, I proved associativity and commutativity of addition and multiplication, and the existence of (both left and right) identities and inverses for addition and multiplication, which involved a lot of rewrite statements. (which is most of the field axioms).
  11. The above proofs (with explanations) can be found in the file FieldAxioms.idr
    • addIdRightEqRat and addIdLeftEqRat
    • multIdRightEqRat andmultIdLeftEqRat
    • addInverseLeftEqRat and addInverseRightEqRat
    • multInverseLeftEqRat andmultInverseRightEqRat
    • plusCommQEqRat
    • multCommQEqRat
    • plusAssocQEqRat
    • multAssocQEqRat

Remaining

The distributive laws need to be proved. In addition, a rational number is different from a pair of integers in the respect that the second integer should not be zero. In every function which has an argument involving ZZPair, the following argument is usually a proof that the second integer is nonzero. I believe that a new data type (called QQ) could be created, consisting of a ZZPair and a proof that the second integer is nonzero. It would be cleaner to define functions using such a data type and would possibly be easier to use in computation/as arguments to other functions.

Helper files (ZZUtils, etc)

I added various helper functions to these. In these files, everything is total.

Log of git commits by author 


commit 0b4706289b8c80ebdc17564bc412dfce16f75082
Author:     AR-MA210 <46956815+AR-MA210@users.noreply.github.com>
AuthorDate: Mon Apr 22 09:29:57 2019 +0530
Commit:     GitHub 
CommitDate: Mon Apr 22 09:29:57 2019 +0530

    Update ar.md

 _reports/ar/ar.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

commit 3e897cad106bc86619f52d1deeb86ab14d42152b
Author:     AR-MA210 <46956815+AR-MA210@users.noreply.github.com>
AuthorDate: Mon Apr 22 09:29:03 2019 +0530
Commit:     GitHub 
CommitDate: Mon Apr 22 09:29:03 2019 +0530

    filled a hole
    
    I filled a hole that I forgot was here.

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

commit 4cfaf271b49ef4c6b7b561e0f3f5ec2facdfa1b5
Author:     AR-MA210 <46956815+AR-MA210@users.noreply.github.com>
AuthorDate: Thu Apr 11 15:10:36 2019 +0530
Commit:     GitHub 
CommitDate: Thu Apr 11 15:10:36 2019 +0530

    Update LinearAlgebra.idr

 Code/LinearAlgebra.idr | 4 ++++
 1 file changed, 4 insertions(+)

commit cb71957d0dd887477748cda8d20d46a0ef66776c
Author:     AR-MA210 <46956815+AR-MA210@users.noreply.github.com>
AuthorDate: Thu Apr 11 14:44:09 2019 +0530
Commit:     GitHub 
CommitDate: Thu Apr 11 14:44:09 2019 +0530

    LinearAlgebra.idr is now Total

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

commit d2f0a02377956872940aaceaebe02651a8014982
Author:     AR-MA210 <46956815+AR-MA210@users.noreply.github.com>
AuthorDate: Thu Apr 11 14:43:30 2019 +0530
Commit:     GitHub 
CommitDate: Thu Apr 11 14:43:30 2019 +0530

    FieldAxioms.idr is now Total

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

commit 903ffb59e3ad1179c05f321ed29247d177239cd7
Author:     AR-MA210 <46956815+AR-MA210@users.noreply.github.com>
AuthorDate: Thu Apr 11 14:42:39 2019 +0530
Commit:     GitHub 
CommitDate: Thu Apr 11 14:42:39 2019 +0530

    FinUtils.idr is now Total
    
    NOTE: To make this total, I needed to change the function `tonatFin`. Previously, it was used for modular values (as it was originally written for Base N arithmetic), but for other uses, this feature (which was blocking totality) is unnecessary.
    
    -- Abishek.

 Code/FinUtils.idr | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

commit 7da1dc2176831402585d231a05c63be487913bef
Author:     AR-MA210 <46956815+AR-MA210@users.noreply.github.com>
AuthorDate: Thu Apr 11 14:41:23 2019 +0530
Commit:     GitHub 
CommitDate: Thu Apr 11 14:41:23 2019 +0530

    VectPerm.idr is now total.

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

commit 19e85846db1af8860bd6fb269bb8248dc2d12b4d
Author:     AR-MA210 <46956815+AR-MA210@users.noreply.github.com>
AuthorDate: Thu Apr 11 14:39:54 2019 +0530
Commit:     GitHub 
CommitDate: Thu Apr 11 14:39:54 2019 +0530

    Updated for Totality.
    
    All files that I have contributed to are total.

 _reports/ar/ar.md | 26 +++++++++++++++++++++++---
 1 file changed, 23 insertions(+), 3 deletions(-)

commit 7b741092307d65a97a051df9a389af0005b8e715
Author:     AR-MA210 <46956815+AR-MA210@users.noreply.github.com>
AuthorDate: Thu Apr 11 14:02:46 2019 +0530
Commit:     GitHub 
CommitDate: Thu Apr 11 14:02:46 2019 +0530

    Rationals.idr is Total
    
    Everything in this file is total now.

 Code/Rationals.idr | 16 +++++++++++-----
 1 file changed, 11 insertions(+), 5 deletions(-)

commit c1d4de437c24f0d1e520724b5ac71286f64267f5
Author:     AR-MA210 <46956815+AR-MA210@users.noreply.github.com>
AuthorDate: Thu Apr 4 14:23:32 2019 +0530
Commit:     GitHub 
CommitDate: Thu Apr 4 14:23:32 2019 +0530

    Update ar.md

 _reports/ar/ar.md | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

commit 2cab5820a02c86a3e1570e4de13e14fd3d71e732
Author:     AR-MA210 <46956815+AR-MA210@users.noreply.github.com>
AuthorDate: Thu Apr 4 14:22:34 2019 +0530
Commit:     GitHub 
CommitDate: Thu Apr 4 14:22:34 2019 +0530

    Update ar.md

 _reports/ar/ar.md | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

commit df20483e0dc8c169ff4f0469e6af126e5a6a20e6
Author:     AR-MA210 <46956815+AR-MA210@users.noreply.github.com>
AuthorDate: Thu Apr 4 14:21:56 2019 +0530
Commit:     GitHub 
CommitDate: Thu Apr 4 14:21:56 2019 +0530

    elaborated on report

 _reports/ar/ar.md | 24 +++++++++++++++++++++---
 1 file changed, 21 insertions(+), 3 deletions(-)

commit 696e4623a4e66c0ba5894c407e13a5b8b1683440
Author:     AR-MA210 <46956815+AR-MA210@users.noreply.github.com>
AuthorDate: Thu Apr 4 14:00:36 2019 +0530
Commit:     GitHub 
CommitDate: Thu Apr 4 14:00:36 2019 +0530

    cleaned up some code
    
    I included proofs that the solution to some equation is a valid rational number (nonzero denominator). I cleaned up code that was used before but has been improved upon by something with proofs. I've left the previously used code for reference purposes (someone might find the ideas in there useful). I also made everything in here total.
    
    -- Abishek (AR-MA210)

 Code/Linear.idr | 45 ++++++++++++++++++++++++++++-----------------
 1 file changed, 28 insertions(+), 17 deletions(-)

commit 1f6523c3fdbbcaefd70d109a112be72e1f204fb4
Author:     AR-MA210 <46956815+AR-MA210@users.noreply.github.com>
AuthorDate: Wed Mar 27 18:05:55 2019 +0530
Commit:     GitHub 
CommitDate: Wed Mar 27 18:05:55 2019 +0530

    Update FieldAxioms.idr

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

commit 1de0415b0ef64c8acb57dabb64b0018d8c924a0d
Author:     AR-MA210 <46956815+AR-MA210@users.noreply.github.com>
AuthorDate: Wed Mar 27 17:56:59 2019 +0530
Commit:     GitHub 
CommitDate: Wed Mar 27 17:56:59 2019 +0530

    updated report for post-midterm
    
    I updated my report.
    
    -- Abishek (AR-MA210)

 _reports/ar/ar.md | 25 +++++++++++++++++++++----
 1 file changed, 21 insertions(+), 4 deletions(-)

commit 2ba0ed896f7843f33fc1b5573d5cddc1e0061280
Author:     AR-MA210 <46956815+AR-MA210@users.noreply.github.com>
AuthorDate: Wed Mar 27 17:35:01 2019 +0530
Commit:     GitHub 
CommitDate: Wed Mar 27 17:35:01 2019 +0530

    Field Axioms Proven with EqRat
    
    I verified all the field axioms (except for the distributive laws for now) using the data type `EqRat` and its properties (symmetry, reflexivity, transitivity) for the rational numbers.
    
    -- Abishek (AR-MA210)

 Code/FieldAxioms.idr | 89 ++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 89 insertions(+)

commit 97a87e385b09e612cc42ada0ab33c95ac96e0c13
Author:     AR-MA210 <46956815+AR-MA210@users.noreply.github.com>
AuthorDate: Wed Mar 27 17:32:41 2019 +0530
Commit:     GitHub 
CommitDate: Wed Mar 27 17:32:41 2019 +0530

    some edits
    
    I needed to make some minor edits.
    
    -- Abishek (AR-MA210)

 Code/Rationals.idr | 24 +++++++++++-------------
 1 file changed, 11 insertions(+), 13 deletions(-)

commit 6ff899e9925dda5f393fe4ec78ec333e1297f2f4
Author:     AR-MA210 <46956815+AR-MA210@users.noreply.github.com>
AuthorDate: Mon Mar 25 15:15:03 2019 +0530
Commit:     GitHub 
CommitDate: Mon Mar 25 15:15:03 2019 +0530

    finished transitivity
    
    I finished the proof of transitivity of `EqRat`.
    
    -- Abishek

 Code/Rationals.idr | 40 +++++++++++++++++++++++++++++++++++++++-
 1 file changed, 39 insertions(+), 1 deletion(-)

commit 17ad9cec17709829c5e4fe653f33be654d272e88
Author:     AR-MA210 <46956815+AR-MA210@users.noreply.github.com>
AuthorDate: Sun Mar 24 14:34:02 2019 +0530
Commit:     GitHub 
CommitDate: Sun Mar 24 14:34:02 2019 +0530

    proved one case of transitivity
    
    I proved one case of transitivity of equality of rational numbers.
    
    If X, Y, and Z are rationals, X=a/b, Y=c/d, Z=e/f, and ad=bc, cf=de, then I showed that af=be in the case where c is not 0, which is one of the cases of transitivity). It remains to be shown that if c is zero, then a and e are zero (and thus X and Z are equal).
    
    -- Abishek (AR-MA210).

 Code/Rationals.idr | 55 ++++++++++++++++++++++++++++++++++++++++++++++++------
 1 file changed, 49 insertions(+), 6 deletions(-)

commit 1cdb0b3e7257c33c64c84dbcefefa9d025d9a343
Author:     AR-MA210 <46956815+AR-MA210@users.noreply.github.com>
AuthorDate: Sat Mar 23 14:42:39 2019 +0530
Commit:     GitHub 
CommitDate: Sat Mar 23 14:42:39 2019 +0530

    some equality facts
    
    I made (0,1) the canonical representation of the rational number 0 and likewise (1,1) for 1.

 Code/Rationals.idr | 43 ++++++++++++++++++++++++++++++++++++++++---
 1 file changed, 40 insertions(+), 3 deletions(-)

commit 4c53b137b92168c6544b571117227cc2e2cc773c
Author:     AR-MA210 <46956815+AR-MA210@users.noreply.github.com>
AuthorDate: Fri Mar 22 20:44:59 2019 +0530
Commit:     GitHub 
CommitDate: Fri Mar 22 20:44:59 2019 +0530

    implemented Shafil's suggestion
    
    I renamed the functions to avoid name clashes.

 Code/Rationals.idr | 13 +++++--------
 1 file changed, 5 insertions(+), 8 deletions(-)

commit 1d3578673116e17cdf0bcf02f020c426a341f0cc
Author:     AR-MA210 <46956815+AR-MA210@users.noreply.github.com>
AuthorDate: Fri Mar 22 19:38:04 2019 +0530
Commit:     GitHub 
CommitDate: Fri Mar 22 19:38:04 2019 +0530

    simplification with proof + equality of rationals
    
    I added a function which takes a rational number and produces the simplified form with proof.
    Also, I started working on a custom equality type for rationals (a/b = c/d if ad=bc). I proved reflexivity and symmetry for this type. I am trying to be as careful as possible with this equality type.
    
    -- Abishek (AR-MA210).

 Code/Rationals.idr | 58 ++++++++++++++++++++++++++++++++++++++++++++++--------
 1 file changed, 50 insertions(+), 8 deletions(-)

commit edae7ff09cc1f6d32950709cd036dc700019f871
Author:     AR-MA210 <46956815+AR-MA210@users.noreply.github.com>
AuthorDate: Sun Mar 17 18:16:04 2019 +0530
Commit:     GitHub 
CommitDate: Sun Mar 17 18:16:04 2019 +0530

    Associativity
    
    I verified associativity for addition and multiplication of rationals.
    
    I believe the distributive laws (to be done next) will require a custom equality type along with additive/multiplicative inverses.
    
    -- Abishek (AR-MA210)

 Code/Rationals.idr | 35 ++++++++++++++++++++++++++++++++++-
 1 file changed, 34 insertions(+), 1 deletion(-)

commit 22456e077b6f72af87352833c47986afc797c606
Author:     AR-MA210 <46956815+AR-MA210@users.noreply.github.com>
AuthorDate: Wed Mar 13 22:17:22 2019 +0530
Commit:     GitHub 
CommitDate: Wed Mar 13 22:17:22 2019 +0530

    multiplicative and additive inverse axioms
    
    I verified these axioms as well.
    
    -- Abishek (AR-MA210)

 Code/Rationals.idr | 42 +++++++++++++++++++++++++++++++++++++-----
 1 file changed, 37 insertions(+), 5 deletions(-)

commit 4cc705727bb2aedbbd367a5718f6a034a131f48e
Author:     AR-MA210 <46956815+AR-MA210@users.noreply.github.com>
AuthorDate: Wed Mar 13 20:45:21 2019 +0530
Commit:     GitHub 
CommitDate: Wed Mar 13 20:45:21 2019 +0530

    field axioms for Q
    
    I started verifying the field axioms for the rational numbers. For those involving equality of a rational number to 1 or equality of a rational number to 0, I think we may need to use a custom equality type (like `EqRat` which Sriram defined in this file).
    
    -- Abishek (AR-MA210)

 Code/Rationals.idr | 71 +++++++++++++++++++++++++++++++++++++++++++++++++-----
 1 file changed, 65 insertions(+), 6 deletions(-)

commit 06db52f045e7610bd3de660e649290f7b65bdb08
Author:     AR-MA210 <46956815+AR-MA210@users.noreply.github.com>
AuthorDate: Tue Mar 12 16:03:44 2019 +0530
Commit:     GitHub 
CommitDate: Tue Mar 12 16:03:44 2019 +0530

    started the non-homogeneous equation
    
    I proved that if (x1,y1) and (x2,y2) are solutions of c=ax+by, the difference (x1-x2,y1-y2) satisfies the homogeneous equation. This can be used to show that any solution is a particular solution plus a solution of the homogeneous equation.
    
    -- Abishek (AR-MA210).

 Code/TwoVarDiophEq.idr | 51 ++++++++++++++++++++++++++++++++++++++++++++++++--
 1 file changed, 49 insertions(+), 2 deletions(-)

commit 63a5544c3f03e608843a1be39d0ddd5300d27a51
Author:     AR-MA210 <46956815+AR-MA210@users.noreply.github.com>
AuthorDate: Sun Mar 10 10:49:34 2019 +0530
Commit:     GitHub 
CommitDate: Sun Mar 10 10:49:34 2019 +0530

    solved homogeneous 2 variable equation + filled hole
    
    I filled a hole in a helper function and added another helper function for transitioning between proofs of equalities in the homogeneous case.
    
    -- Abishek

 Code/Linear.idr | 20 +++++++++++++++++++-
 1 file changed, 19 insertions(+), 1 deletion(-)

commit 28046f4826534cb4873a8f7f124d527901858e85
Author:     AR-MA210 <46956815+AR-MA210@users.noreply.github.com>
AuthorDate: Sun Mar 10 00:46:07 2019 +0530
Commit:     GitHub 
CommitDate: Sun Mar 10 00:46:07 2019 +0530

    Update Linear.idr

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

commit 8e45d8cb8694fb15a925109ee4cd89367b60c695
Author:     AR-MA210 <46956815+AR-MA210@users.noreply.github.com>
AuthorDate: Sun Mar 10 00:35:19 2019 +0530
Commit:     GitHub 
CommitDate: Sun Mar 10 00:35:19 2019 +0530

    Update Linear.idr

 Code/Linear.idr | 43 ++++++++++++++++++++++++++++++++++++++-----
 1 file changed, 38 insertions(+), 5 deletions(-)

commit c4653702013e3fd9bffa16e4acd10fc6839c22a7
Author:     AR-MA210 <46956815+AR-MA210@users.noreply.github.com>
AuthorDate: Sun Mar 10 00:34:13 2019 +0530
Commit:     GitHub 
CommitDate: Sun Mar 10 00:34:13 2019 +0530

    Update ZZUtils.idr

 Code/ZZUtils.idr | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

commit 65d25b4c079774b3dc7b2717777386c832f08c11
Author:     AR-MA210 <46956815+AR-MA210@users.noreply.github.com>
AuthorDate: Sat Mar 9 16:24:48 2019 +0530
Commit:     GitHub 
CommitDate: Sat Mar 9 16:24:48 2019 +0530

    solved one variable Diophantine Equations
    
    The function `DiophantineSolver` solves one variable diophantine equations with proof (if an integer solution exists, it shows the solution with proof; if not, it outputs the rational solution with proof).
    
    -- Abishek (AR-MA210)

 Code/Linear.idr | 33 +++++++++++++++++++++++++++++++++
 1 file changed, 33 insertions(+)

commit 23981ade110dbaa1d8d05e6d421d57e7ec8462da
Author:     AR-MA210 <46956815+AR-MA210@users.noreply.github.com>
AuthorDate: Sat Mar 9 16:21:16 2019 +0530
Commit:     GitHub 
CommitDate: Sat Mar 9 16:21:16 2019 +0530

    filled in holes
    
    I filled in some holes once I found/made the auxiliary functions required to finish the proofs.
    
    -- Abishek.

 Code/ZZUtils.idr | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

commit fa1b0ebd26278f96eb1443b94e043ffc02bf72fe
Author:     AR-MA210 <46956815+AR-MA210@users.noreply.github.com>
AuthorDate: Fri Mar 8 22:35:33 2019 +0530
Commit:     GitHub 
CommitDate: Fri Mar 8 22:35:33 2019 +0530

    added in the necessary auxiliary functions
    
    I added in some functions required for the function `CheckIsQuotientZ` from the Rationals.idr file into this. There are some small holes to be filled but for the most part it is complete.
    
    
    -- Abishek

 Code/ZZUtils.idr | 56 +++++++++++++++++++++++++++++++++++++++++++++++++++++---
 1 file changed, 53 insertions(+), 3 deletions(-)

commit 97bf91ac84a01a63e0d6fc58c023a600992cb134
Author:     AR-MA210 <46956815+AR-MA210@users.noreply.github.com>
AuthorDate: Fri Mar 8 22:34:04 2019 +0530
Commit:     GitHub 
CommitDate: Fri Mar 8 22:34:04 2019 +0530

    Rationals and Integers in all cases
    
    I extended the function which checks if a rational number is an integer so that it works for any rational number. There were 6 possible cases.
    
    -- Abishek

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

commit 67b9c51b66720660cf150a0af6e7d26e0c3eea58
Author:     AR-MA210 <46956815+AR-MA210@users.noreply.github.com>
AuthorDate: Tue Mar 5 23:56:08 2019 +0530
Commit:     GitHub 
CommitDate: Tue Mar 5 23:56:08 2019 +0530

    some functions on zero cases
    
    Added some utility functions for decidability of NotZero.
    
    The function nonZeroNotZero has holes that need to be filled.

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

commit 3a1709e7e22facc2e57e3666f4a86bad4be2d6dc
Author:     AR-MA210 <46956815+AR-MA210@users.noreply.github.com>
AuthorDate: Tue Mar 5 23:54:34 2019 +0530
Commit:     GitHub 
CommitDate: Tue Mar 5 23:54:34 2019 +0530

    Rationals and Integers
    
    I added a function which checks if a rational number is equal to an integer.
    
    -- Abishek (AR-MA210)

 Code/Rationals.idr | 54 ++++++++++++++++++++++++++++++++++++------------------
 1 file changed, 36 insertions(+), 18 deletions(-)

commit fbf98d4cd75262d2d079240ab0a67d3f7a185372
Author:     AR-MA210 <46956815+AR-MA210@users.noreply.github.com>
AuthorDate: Sat Mar 2 16:44:07 2019 +0530
Commit:     GitHub 
CommitDate: Sat Mar 2 16:44:07 2019 +0530

    Permutations
    
    Based on what I did previously, I implemented two simple Boolean tests for permutations (which may be useful for other purposes in other projects). I also started implementing permutations as bijections. The function `PermutationBijection` (which works only given POSITIVE inputs) takes two Vectors of equal length (with possibly repeated elements) and tries to construct a bijection between them. When there exists one, it returns the bijection which takes one Vector to another in the form of a list (for example the list [0,2,3,1] means that X[0] = Y[0], X[1] = Y[2], X[2] = Y[3], X[3] = Y[1]). If there is no bijection between the two Vectors, it constructs one between whichever elements are present in both.
    
    It remains to prove that when the length of the list is `n`, the List produced by this function corresponds to a bijection.
    
    -- Abishek (AR-MA210)

 Code/VectPerm.idr | 73 +++++++++++++++++++++++++++++++++++++++++++++----------
 1 file changed, 60 insertions(+), 13 deletions(-)

commit 3b5326e473777a49b63ef75267290d598139f139
Author:     AR-MA210 <46956815+AR-MA210@users.noreply.github.com>
AuthorDate: Sat Mar 2 00:22:51 2019 +0530
Commit:     GitHub 
CommitDate: Sat Mar 2 00:22:51 2019 +0530

    comparing Vectors
    
    I used the function `improveElem` which I made before to start comparing elements between Vectors and deleting them if they were present in both Vectors. This can be used to define permutations recursively as follows:
    
    - two unit length Vectors are permutations if they are equal
    - two Vectors are permutations of each other if deleting any common element from both of them produces two Vectors which a permutations.
    
    Defining permutations and using the tools developed is the next step.
    
    -- Abishek (AR-MA210)

 Code/VectPerm.idr | 65 +++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 65 insertions(+)

commit 926114d308371979f47e1893d7255fe3ce4872bc
Author:     AR-MA210 <46956815+AR-MA210@users.noreply.github.com>
AuthorDate: Tue Feb 26 23:25:23 2019 +0530
Commit:     GitHub 
CommitDate: Tue Feb 26 23:25:23 2019 +0530

    elem function, but with proof
    
    The library function `elem` can tell you whether an element is in a vector or not (Bool), but not where and how many times it occurs. I created a function which does this with proof; it finds all occurrences of an element in a vector with proof. This will be used in checking with proof if a vector is a permutation of another.
    
    -- Abishek (AR-MA210)

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

commit 27d5f934c841f9f0dbe0c10b9a5417a98a6419b1
Author:     AR-MA210 <46956815+AR-MA210@users.noreply.github.com>
AuthorDate: Mon Feb 25 09:20:21 2019 +0530
Commit:     GitHub 
CommitDate: Mon Feb 25 09:20:21 2019 +0530

    fixed import

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

commit 05a234c4b2a40917df642cf39ef93465c30741a6
Author:     AR-MA210 <46956815+AR-MA210@users.noreply.github.com>
AuthorDate: Mon Feb 25 09:19:47 2019 +0530
Commit:     GitHub 
CommitDate: Mon Feb 25 09:19:47 2019 +0530

    fixed import

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

commit e9e111d19435554f0151ef2f3735912ca51f19c7
Author:     AR-MA210 <46956815+AR-MA210@users.noreply.github.com>
AuthorDate: Mon Feb 25 09:19:02 2019 +0530
Commit:     GitHub 
CommitDate: Mon Feb 25 09:19:02 2019 +0530

    fixed import

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

commit 024a827f928372325f9485ba1618e07747a3d309
Author:     AR-MA210 <46956815+AR-MA210@users.noreply.github.com>
AuthorDate: Mon Feb 25 09:18:19 2019 +0530
Commit:     GitHub 
CommitDate: Mon Feb 25 09:18:19 2019 +0530

    fixed import

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

commit 29e14f6be8cb6e36e41e61cceecc95cdec5ee5b2
Author:     AR-MA210 <46956815+AR-MA210@users.noreply.github.com>
AuthorDate: Mon Feb 25 00:25:31 2019 +0530
Commit:     GitHub 
CommitDate: Mon Feb 25 00:25:31 2019 +0530

    Finished Report
    
    I added the links to the relevant commits.
    
    -- Abishek (AR-MA210)

 _reports/ar/ar.md | 37 ++++++++++++++++++++-----------------
 1 file changed, 20 insertions(+), 17 deletions(-)

commit 56d26de18aed2ef923c0c51dbbc6d78127abeeca
Author:     AR-MA210 <46956815+AR-MA210@users.noreply.github.com>
AuthorDate: Mon Feb 25 00:14:19 2019 +0530
Commit:     GitHub 
CommitDate: Mon Feb 25 00:14:19 2019 +0530

    correction + more functions
    
    I made a correction in the simplification routine and also added some functions which will eventually used to find the rank of a linear transformation.
    
    -- Abishek (AR-MA210)

 Code/LinearAlgebra.idr | 14 +++++++++++++-
 1 file changed, 13 insertions(+), 1 deletion(-)

commit 975e01f95e5f1de41329b0a6b5058812fc99e432
Author:     AR-MA210 <46956815+AR-MA210@users.noreply.github.com>
AuthorDate: Sat Feb 23 17:07:45 2019 +0530
Commit:     GitHub 
CommitDate: Sat Feb 23 17:07:45 2019 +0530

    Update Report
    
    Added to Sorting.
    
    -- Abishek (AR-MA210)

 _reports/ar/ar.md | 5 +++++
 1 file changed, 5 insertions(+)

commit af78ca7a21e563d6e5c1568818fa6bd53ce08254
Author:     AR-MA210 <46956815+AR-MA210@users.noreply.github.com>
AuthorDate: Sat Feb 23 17:04:55 2019 +0530
Commit:     GitHub 
CommitDate: Sat Feb 23 17:04:55 2019 +0530

    switched to Vectors + more
    
    I made the code run using Vectors instead of lists. Also, I added a function which produces the minimum element in a Vector, and used it to check if a Vector is Sorted. This can be upgraded with a proof that the minimum element is the minimum and eventually that a Sorted Vector is Sorted.
    
    -- Abishek (AR-MA210)

 Code/InsertionSort.idr | 29 ++++++++++++++++++++++-------
 1 file changed, 22 insertions(+), 7 deletions(-)

commit a6f16af8aeb42880a6e96910f46e4f2456665b2c
Author:     AR-MA210 <46956815+AR-MA210@users.noreply.github.com>
AuthorDate: Sat Feb 23 16:38:32 2019 +0530
Commit:     GitHub 
CommitDate: Sat Feb 23 16:38:32 2019 +0530

    moved something from 'Remaining' to 'Done'
    
    Added simplification of matrices.
    
    -- Abishek (AR-MA210)

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

commit abd348d60ffca6de7adc9b87ceebb493d21aa375
Author:     AR-MA210 <46956815+AR-MA210@users.noreply.github.com>
AuthorDate: Sat Feb 23 16:35:07 2019 +0530
Commit:     GitHub 
CommitDate: Sat Feb 23 16:35:07 2019 +0530

    Added simplification routine, fixed import
    
    I added functions which convert a matrix of ZZPairs to a matrix in simplified form.
    
    The file BaseN was imported here, but it got changed and one function was lost, so I added it here.
    
    -- Abishek (AR-MA210)

 Code/LinearAlgebra.idr | 53 ++++++++++++++++++++++++++++++++++++++++++--------
 1 file changed, 45 insertions(+), 8 deletions(-)

commit 60e1cd5159aa90a194768c3f550f91e1407e9d11
Author:     AR-MA210 <46956815+AR-MA210@users.noreply.github.com>
AuthorDate: Sat Feb 16 01:06:46 2019 +0530
Commit:     GitHub 
CommitDate: Sat Feb 16 01:06:46 2019 +0530

    Update Linear.idr

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

commit 102c70349f413b6947b5fd2127c2c03ada68e307
Author:     AR-MA210 <46956815+AR-MA210@users.noreply.github.com>
AuthorDate: Sat Feb 16 01:04:59 2019 +0530
Commit:     GitHub 
CommitDate: Sat Feb 16 01:04:59 2019 +0530

    minor additions to report
    
    I added to the report.
    
    Abishek (AR-MA210).

 _reports/ar/ar.md | 18 ++++++++++--------
 1 file changed, 10 insertions(+), 8 deletions(-)

commit 6ff18f941f2321ae10cc025202d3e35b392274bf
Author:     AR-MA210 <46956815+AR-MA210@users.noreply.github.com>
AuthorDate: Sat Feb 16 00:59:45 2019 +0530
Commit:     GitHub 
CommitDate: Sat Feb 16 00:59:45 2019 +0530

    Tweaked ReduceRow
    
    I tweaked ReduceRow so that it reduces only those rows with non-zero elements.
    
    -- Abishek (AR-MA210)

 Code/LinearAlgebra.idr | 14 ++++++++++----
 1 file changed, 10 insertions(+), 4 deletions(-)

commit 393a0a25a43db9975a6db7bc5fe39583a3f8cf7e
Author:     AR-MA210 <46956815+AR-MA210@users.noreply.github.com>
AuthorDate: Sat Feb 16 00:47:20 2019 +0530
Commit:     GitHub 
CommitDate: Sat Feb 16 00:47:20 2019 +0530

    checking for Integer solutions
    
    I added a function which solves Diophantine equations by checking if the rational number can be simplified to an integer. This is at a rudimentary stage right now because implementing a proof of this would require a GCD function with proof that it is a GCD.
    
    -- Abishek (AR-MA210)

 Code/Linear.idr | 36 +++++++++++++++++++++++++++++++++---
 1 file changed, 33 insertions(+), 3 deletions(-)

commit a2d5af5a52ba61488a9c0e26fdb0d9ce2e03597d
Author:     AR-MA210 <46956815+AR-MA210@users.noreply.github.com>
AuthorDate: Thu Feb 14 15:57:13 2019 +0530
Commit:     GitHub 
CommitDate: Thu Feb 14 15:57:13 2019 +0530

    Update ar.md

 _reports/ar/ar.md | 36 ++++++++++++++++++------------------
 1 file changed, 18 insertions(+), 18 deletions(-)

commit 650094ed4a5784dc8220081b785741d35da06788
Author:     AR-MA210 <46956815+AR-MA210@users.noreply.github.com>
AuthorDate: Thu Feb 14 15:50:56 2019 +0530
Commit:     GitHub 
CommitDate: Thu Feb 14 15:50:56 2019 +0530

    magnitude of the Determinant + more
    
    I found the magnitude of the determinant as a simple extension of the previous functions. The sign can be calculated by a trick I describe in the file. I also propose a variety of extensions of this code:
    
    - finding the inverse by row operations (might be easier for proofs)
    - solving linear systems (with proof) using extensions to  Linear.idr
    - finding the rank of a linear transformation by counting the number of nonzero diagonal elements in the Diagonal Form.
    
    -- Abishek (AR-MA210)

 Code/LinearAlgebra.idr | 41 +++++++++++++++++++++++++++++++++++++++++
 1 file changed, 41 insertions(+)

commit 93aa06d16a4a1a7fb3e1e006d6ae05559286a6fc
Author:     AR-MA210 <46956815+AR-MA210@users.noreply.github.com>
AuthorDate: Thu Feb 14 15:44:18 2019 +0530
Commit:     GitHub 
CommitDate: Thu Feb 14 15:44:18 2019 +0530

    Added Report
    
    I filled in most of the report.
    
    -- Abishek (AR-MA210.

 _reports/ar/ar.md | 66 +++++++++++++++++++++++++++++++++++++++++++++++++++++--
 1 file changed, 64 insertions(+), 2 deletions(-)

commit a302e8f2a1708d4dad8b5b515a9bb4435fdd86c1
Author:     AR-MA210 <46956815+AR-MA210@users.noreply.github.com>
AuthorDate: Wed Feb 13 18:59:17 2019 +0530
Commit:     GitHub 
CommitDate: Wed Feb 13 18:59:17 2019 +0530

    correction + Diagonal Form of a matrix
    
    I made a minor correction in a line. Upper - Triangular forms can be found for all matrices now (n x n), modulo computational blow ups. Also, Diagonal Forms can be found as described in the code.
    
    Note: finding the magnitude of the determinant is easy using this, but due to Row Swaps, the sign of the determinant must be found in some other way (maybe a clever linear algebra trick).
    
    -- Abishek (AR-MA210)

 Code/LinearAlgebra.idr | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

commit a2a2b35f5907291b1aeecccc7f752f20cf9c84fe
Author:     AR-MA210 <46956815+AR-MA210@users.noreply.github.com>
AuthorDate: Tue Feb 12 22:16:50 2019 +0530
Commit:     GitHub 
CommitDate: Tue Feb 12 22:16:50 2019 +0530

    Gauss-Jordan implemented
    
    Using the MakeColumnZero function recursively, I implemented Gauss-Jordan elimination as far as to make a matrix upper triangular.
    
    -- Abishek (AR-MA210)

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

commit 1adc1e651b7b7f3d0f58505793e06ec13e93ae50
Author:     AR-MA210 <46956815+AR-MA210@users.noreply.github.com>
AuthorDate: Tue Feb 12 15:24:33 2019 +0530
Commit:     GitHub 
CommitDate: Tue Feb 12 15:24:33 2019 +0530

    Using Row Operations
    
    The row operations that I implemented earlier can now be put to use - namely for making a particular element in a matrix zero 'MakeElementZero' takes a matrix M, a row A, a row B, a position P in the row, and does a row operation to make M[A][P] equal to zero. 'MakeColumnZero' takes a matrix M, a specified column, and calls MakeElementZero to insert zeros appropriately (into upper triangular form). The next step here is to recursively use MakeColumnZero to make a matrix upper triangular (good for finding the determinant and solving linear equations/inverting).
    
    -- Abishek (AR-MA210)

 Code/LinearAlgebra.idr | 63 +++++++++++++++++++++++++++++++++++++++++++-------
 1 file changed, 55 insertions(+), 8 deletions(-)

commit 7a12fcc8932277255b89ad5143c43e0d5c01b7cc
Author:     AR-MA210 <46956815+AR-MA210@users.noreply.github.com>
AuthorDate: Sun Feb 10 20:36:52 2019 +0530
Commit:     GitHub 
CommitDate: Sun Feb 10 20:36:52 2019 +0530

    started Linear Dependence
    
    Checking if vectors are dependent can be done through the determinant. However, to check if vectors are linearly dependent (and to give a proof), we need a linear combination of them which is zero. For this, we can use standard elimination techniques in Linear Algebra. To do this, I started implementing elementary operations to do Gaussian elimination (row operations and swapping rows).
    
    -- Abishek (AR-MA210)

 Code/LinearAlgebra.idr | 59 ++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 59 insertions(+)

commit 17fca0022588c0c3d3e7e3a69e7b634df61dc2a8
Author:     AR-MA210 <46956815+AR-MA210@users.noreply.github.com>
AuthorDate: Sun Feb 10 20:35:27 2019 +0530
Commit:     GitHub 
CommitDate: Sun Feb 10 20:35:27 2019 +0530

    public export
    
    added export

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

commit 55fe7ea3e76e97f6fa4a7de852fec0ba9f3c93e2
Author:     AR-MA210 <46956815+AR-MA210@users.noreply.github.com>
AuthorDate: Sat Feb 9 19:49:07 2019 +0530
Commit:     GitHub 
CommitDate: Sat Feb 9 19:49:07 2019 +0530

    Done with 1 variable rational equations, moving to Diophantine
    
    The general linear equation ax+b=c can be solved using this with a proof that it is a solution. As explained in the program, I will extend this to Diophantine equations (this will require use of the quotient-remainder algorithm to check if the denominator is a divisor of the numerator, and if so, to print the quotient as the integer solution; details can be found in the previous update).
    
    Also, unfortunately, I am not able to prove that ( a*c + a*(-b) + b*a = a*c ) in the function helper4; the methods which worked to transform equalities in other helper functions somehow lead to type errors in this. I have left it as a hole for now.
    
    -- Abishek (AR-MA210)

 Code/Linear.idr | 35 ++++++++++++++++++++++++++++++++---
 1 file changed, 32 insertions(+), 3 deletions(-)

commit 0d2a515ea420abcfa9b0eb8a91b901d32db2dc01
Author:     AR-MA210 <46956815+AR-MA210@users.noreply.github.com>
AuthorDate: Thu Feb 7 14:21:39 2019 +0530
Commit:     GitHub 
CommitDate: Thu Feb 7 14:21:39 2019 +0530

    Added the proof of ncase
    
    I added the solution of (ax + b = 0) with proof. I also showed the equivalence between (ax + b = c) and (ax + b + (-c) = 0), so this solution technique can be extended to solve any equation ax + b = c over the rationals. Regarding the solution of Diophantine equations, I think the next step could be proving the reverse implication (any solution of such an equation is of this form) and conclude that the Diophantine equation in one variable has a solution iff the denominator of the rational is 1 or -1.
    
    --Abishek (AR-MA210)

 Code/Linear.idr | 54 +++++++++++++++++++++++++++++++++++++++++++++---------
 1 file changed, 45 insertions(+), 9 deletions(-)

commit 1f7cab801381a1f2b7e5c14c712d0893bc62effa
Author:     AR-MA210 <46956815+AR-MA210@users.noreply.github.com>
AuthorDate: Wed Feb 6 16:48:46 2019 +0530
Commit:     GitHub 
CommitDate: Wed Feb 6 16:48:46 2019 +0530

    Finished the proof of zcase
    
    The equation has been split into two cases based on the value of b. I added in the proof of zcase (the case where b = 0), using a bunch of helper functions. Also, the if-else flow of control was removed because it ensure that proofs can be done smoothly.
    
    -- Abishek (AR-MA210)

 Code/Linear.idr | 30 +++++++++++++++++++++++-------
 1 file changed, 23 insertions(+), 7 deletions(-)

commit 38ebca11b53fc2db493a99d45a858dd98098e9ff
Author:     AR-MA210 <46956815+AR-MA210@users.noreply.github.com>
AuthorDate: Sat Feb 2 22:42:08 2019 +0530
Commit:     GitHub 
CommitDate: Sat Feb 2 22:42:08 2019 +0530

    minor additions and shifting to ZZ
    
    The proof for the additive identity is nearly complete - all of the necessary helper proof functions are in place. It just needs to be shown that the sum of the numerator and denominator being zero implies that the rational is zero.
    
    Also, the shift from Integer to ZZ has been implemented in most parts of the code (this is useful as proofs can be done with ZZ in the ZZ library).
    
    -- Abishek (AR-MA210)

 Code/Rationals.idr | 65 +++++++++++++++++++++++-------------------------------
 1 file changed, 28 insertions(+), 37 deletions(-)

commit ac3ee364e84b3aa82fb602c401499e42bfc8cc0f
Author:     AR-MA210 <46956815+AR-MA210@users.noreply.github.com>
AuthorDate: Sat Feb 2 01:21:32 2019 +0530
Commit:     GitHub 
CommitDate: Sat Feb 2 01:21:32 2019 +0530

    partial proofs for additive identity
    
    I started the process of proving that the sum of a rational number and it's inverse is 0. For this, I needed the type ZZ (which is an implementation of that integers that allows proofs). I added a few functions for converting between pairs of ZZ and integers. I believe that using cong, the next step (showing that x = -y implies that x+y = 0) can be used to show that the first number in the pair of addition of a number and its inverse is always zero.
    
    A similar process can be used for multiplicative inverses, but will involve simplification of the rational generated and showing that it is equal to (1,1).
    
    Documentation for ZZ:
    
    https://github.com/idris-lang/Idris-dev/blob/master/libs/contrib/Data/ZZ.idr

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

commit 429fd11b09106392452f09a37a97eb25e7ecf189
Author:     AR-MA210 <46956815+AR-MA210@users.noreply.github.com>
AuthorDate: Tue Jan 29 17:03:27 2019 +0530
Commit:     GitHub 
CommitDate: Tue Jan 29 17:03:27 2019 +0530

    Some fixes to simplifyRational
    
    There was an issue in the simplifyRational function - it gave incorrect results due to an error in the gccd function (calculating the GCD when one number is negative leads to issues with examples such as (3,-6), which is erroneously simplified to (0,1)). I made a minor fix here by forcing the GCD to be a positive number.
    
    An issue related to this project: there were two files which were the predecessor of this one. Somehow they were merged, but some of the history seems to be lost in the history of this file. For reference, here are the previous edits:
    
    https://github.com/SS-C4/LTS2019/commits/c92a54c3a915e40b049eabfa008c3bb482ca878a/Code/Rationals.idr
    
    https://github.com/siddhartha-gadgil/LTS2019/commits/a2b3964a651f0d6dcd75f3985e736392602a7acd/Rationals.idr

 Code/Rationals.idr | 24 +++++++++++-------------
 1 file changed, 11 insertions(+), 13 deletions(-)

commit 080fd5d0065efffb0afb79720220d35fd9b757c7
Author:     AR-MA210 <46956815+AR-MA210@users.noreply.github.com>
AuthorDate: Sat Jan 26 23:56:21 2019 +0530
Commit:     GitHub 
CommitDate: Sat Jan 26 23:56:21 2019 +0530

    A few updates to the non-unique Q
    
    I added in proofs for validity of addition and multiplication (with inverses) and extended them to subtraction/division. Simplified form of rationals can be implemented with the necessary proof type for the GCD function (integer division is a bit cumbersome in this). Along with this, defining fields (and showing that this implementation is one) could be the next step.

 Rationals.idr | 57 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 57 insertions(+)

commit 4c261057f0b6b9edf38883015d19137bb9855465
Author:     AR-MA210 <46956815+AR-MA210@users.noreply.github.com>
AuthorDate: Fri Jan 25 15:49:21 2019 +0530
Commit:     GitHub 
CommitDate: Fri Jan 25 15:49:21 2019 +0530

    Basic Implementation of Q (non-unique version)
    
    This creates the framework for the implementation of Q as p/q. Arithmetic is partially defined (inverses need to be given and non-zero proofs will be inserted where appropriate).

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

commit e23e7f5b2d4df83ab81539da2efc5648da11c130
Author:     AR-MA210 <46956815+AR-MA210@users.noreply.github.com>
AuthorDate: Wed Jan 23 18:30:00 2019 +0530
Commit:     GitHub 
CommitDate: Wed Jan 23 18:30:00 2019 +0530

    Add files via upload
    
    This code performs insertion sort on an array. The sortedness and permutedness will be implemented.

 Code/InsertionSort.idr | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)



   Department of Mathematics,  Indian Institute of Science.