- I implemented a function to simplify rationals and added a few more auxiliary functions to Rationals.idr
- I updated some of the types from
`Integer`

to`ZZ`

, and provided casts for ease of use.

- I created the initial framework for solving linear equations, in the commit Linear.idr
- I completed the last case in the proof (which was
*difficult*), and finished the single equation solver with proof, in the commit Linear.idr

- I defined a divisibility type, which is useful for multiple purposes, and is present in different files as well (introduced in commit gcd.idr)

- I created the file MultiSolver, (originally Linear.MultiSolver) and defined a bunch of useful computations required to solve a system of linear equations.
- I defined minors and cofactors for a
`n x n`

square matrix with entries as`ZZPairs`

and created the adjoint matrix to help make inverses. - I defined the inverse for a matrix (only the case where the determinant is non-zero)
- I used the inverse to solve a system of linear equations, again only when the system is consistent.
- This was in the commit Linear.MultiSolver.idr

- I defined minors and cofactors for a
- I defined the
`Num`

and`Neg`

interfaces for`ZZPairs`

, which are useful, as inbuilt functions require input of such an interface. This was mostly in commit Linear.MultiSolver.idr

- I added one lemma which given
`LTE a b`

and`LTE c d`

, returns the type`LTE (a+c) (b+d)`

. This is useful in an independent context as well.

- I created the
`Primes`

module and defined some useful lemmas and definitions.- I created a divisibility type with slight modifications to ensure that it does not admit zero divisors (originally created in
**gcd.idr**) - I implemented a type
`totOrdNat`

, which, given`a`

,`b`

:`Nat`

returns a type with a proof if either`a = b`

,`a < b`

or`a > b`

- I defined various other functions as auxiliary for the
`decDiv`

function, but are useful in their own right in providing contradictions and contrapositives.

- I created a divisibility type with slight modifications to ensure that it does not admit zero divisors (originally created in
- Using all the helper functions defined previously, I defined a
`decDiv`

function that given`a`

,`b`

, returns a`Dec (isDivisible a b)`

type with proofs and contradictions depending on the values.- All cases are complete and
`decDiv`

is total as well (Required a lot of helpers and extensive use of`rewrite`

s for the last case, and was*very difficult*). This will be an important building block for the rest of the*Primes*project. This was completed in commit Primes.idr - Lots of the named helper functions are useful in an independent setting as well; with respect to divisibility.

- All cases are complete and
- I started work on Prime factorization. Some of the important functions:
`factor2`

returns two factors of a number such that the first one is prime. (Not proved yet)`factorise`

factors a number completely with proof that the factors fold back under multiplication to generate the original input.- (
`List Nat`

needs to be augmented to be`List (n : Nat ** isPrime n)`

for the final version) These were done in commits Prime.idr and PrimeApple.idr

```
commit 86c07a7db67befa9208f1bb75a8587081ed43aa9
Author: SS-C4
```
AuthorDate: Sun Apr 21 10:47:56 2019 +0530
Commit: SS-C4
CommitDate: Sun Apr 21 10:47:56 2019 +0530
mistakes corrected.
_reports/ss/ss.md | 6 +++---
1 file changed, 3 insertions(+), 3 deletions(-)
commit bb9d20d3736c072fcd72401316fe89e227f92c0d
Author: SS-C4
AuthorDate: Sun Apr 21 10:40:12 2019 +0530
Commit: SS-C4
CommitDate: Sun Apr 21 10:40:12 2019 +0530
Update report
_reports/ss/ss.md | 7 ++++++-
1 file changed, 6 insertions(+), 1 deletion(-)
commit c09dba524d9ea98d4084b66954a301197c7e969f
Author: SS-C4
AuthorDate: Fri Apr 12 18:16:25 2019 +0530
Commit: SS-C4
CommitDate: Fri Apr 12 18:16:25 2019 +0530
Auxiliary function for proving that each factor is prime or 1.
Code/PrimeApple.idr | 74 +++++++++++++++++++++++++++++++++++------------------
1 file changed, 49 insertions(+), 25 deletions(-)
commit 251328143d1b5797105bda7651e76037741c25a0
Author: SS-C4
AuthorDate: Thu Apr 11 18:11:33 2019 +0530
Commit: SS-C4
CommitDate: Thu Apr 11 18:11:33 2019 +0530
Modularised Primes
Code/PrimeApple.idr | 167 ++++++++++++++++++++++++++++++++++++++++++++++++++++
Code/Primes.idr | 147 ---------------------------------------------
2 files changed, 167 insertions(+), 147 deletions(-)
commit 5908506dd6bd982fed94422cd9c4eea002976eb3
Author: SS-C4
AuthorDate: Wed Apr 10 20:44:21 2019 +0530
Commit: SS-C4
CommitDate: Wed Apr 10 20:44:21 2019 +0530
Updated and cleaned `factorise`
Code/Primes.idr | 101 ++++++++++++++------------------------------------------
1 file changed, 24 insertions(+), 77 deletions(-)
commit 0703c874a001167014734bce2c7541ed2d8b1f11
Author: SS-C4
AuthorDate: Wed Apr 10 01:11:15 2019 +0530
Commit: SS-C4
CommitDate: Wed Apr 10 01:11:15 2019 +0530
Factorisation of numbers is done.
Code/Primes.idr | 62 +++++++++++++++++++++++++++++++++------------------------
1 file changed, 36 insertions(+), 26 deletions(-)
commit 8f48fd8193e9573cf3ca7d6bf7f9c4114f1bae53
Author: SS-C4
AuthorDate: Tue Apr 9 15:33:15 2019 +0530
Commit: SS-C4
CommitDate: Tue Apr 9 15:33:15 2019 +0530
`factor2` factorises a number into two others
Code/Primes.idr | 44 ++++++++++++++++++++++++++++++++++++++++++--
Code/SriramAssRecRule.idr | 1 +
2 files changed, 43 insertions(+), 2 deletions(-)
commit de6436613e290efb4423e1233a1a0cccdf8d6a4c
Author: SS-C4
AuthorDate: Wed Mar 27 10:41:32 2019 +0530
Commit: SS-C4
CommitDate: Wed Mar 27 10:41:32 2019 +0530
Update report
_reports/ss/ss.md | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
commit 7c03bcab4445d716b3734f5f454dd19c657445ae
Author: SS-C4
AuthorDate: Wed Mar 27 06:46:37 2019 +0530
Commit: SS-C4
CommitDate: Wed Mar 27 06:46:37 2019 +0530
Update report
_reports/ss/ss.md | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
commit 66aad165c174a867ceb7032e8fed93cc327e5fb6
Author: SS-C4
AuthorDate: Sat Mar 2 12:26:02 2019 +0530
Commit: SS-C4
CommitDate: Sat Mar 2 12:26:02 2019 +0530
decDiv is complete!
Code/Primes.idr | 57 ++++++++++++++++++++++++++++++++++++++++++++++++---------
1 file changed, 48 insertions(+), 9 deletions(-)
commit ae26265530c494ce865b3c39d68b646c3bac9a84
Author: SS-C4
AuthorDate: Fri Mar 1 18:31:55 2019 +0530
Commit: SS-C4
CommitDate: Fri Mar 1 18:31:55 2019 +0530
Closer to completing the decDiv function. Hopefully only one case left.
Code/Primes.idr | 49 ++++++++++++++++++++++++++++++++++++++++++++++++-
1 file changed, 48 insertions(+), 1 deletion(-)
commit 1798fc49166d84bb76a1469bda812231b6c5dfac
Author: SS-C4
AuthorDate: Fri Feb 22 08:38:45 2019 +0530
Commit: SS-C4
CommitDate: Fri Feb 22 08:38:45 2019 +0530
More fixes
Code/Primes.idr | 5 ++++-
1 file changed, 4 insertions(+), 1 deletion(-)
commit c082b340180b0ef56116b2fc02ba35af0a2feee7
Author: SS-C4
AuthorDate: Fri Feb 22 08:35:19 2019 +0530
Commit: SS-C4
CommitDate: Fri Feb 22 08:35:19 2019 +0530
Some more fixes
Code/Primes.idr | 33 +++++++++++++++++++++++++++++++++
1 file changed, 33 insertions(+)
commit e1f48fc88b9722de00977c1ade68bfaec1792c0b
Author: SS-C4
AuthorDate: Fri Feb 22 08:31:51 2019 +0530
Commit: SS-C4
CommitDate: Fri Feb 22 08:31:51 2019 +0530
Fixed code broken by subsequent commits.
Code/Primes.idr | 66 ++++++++++-----------------------------------------------
Code/gcd.idr | 15 +++++++------
2 files changed, 19 insertions(+), 62 deletions(-)
commit 8fce576a81fbd3f6a1904ccdbe09694abd54a256
Author: SS-C4
AuthorDate: Thu Feb 21 14:59:08 2019 +0530
Commit: SS-C4
CommitDate: Thu Feb 21 14:59:08 2019 +0530
Updated NatUtils with a few functions and almost completed the `decDiv` type
Code/NatUtils.idr | 18 ++++++++---
Code/Primes.idr | 95 +++++++++++++++++++++++++++++++++++++++++++++----------
Code/gcd.idr | 2 +-
3 files changed, 92 insertions(+), 23 deletions(-)
commit d2e8f0b3964fcabd5521f7e8a6ba19be539a7068
Author: SS-C4
AuthorDate: Wed Feb 20 18:23:55 2019 +0530
Commit: SS-C4
CommitDate: Wed Feb 20 18:23:55 2019 +0530
Update report
_reports/ss/ss.md | 11 +++++++++++
1 file changed, 11 insertions(+)
commit 17f3801c5a952ff603b19726e20f923c9ab9933c
Author: SS-C4
AuthorDate: Tue Feb 19 18:32:51 2019 +0530
Commit: SS-C4
CommitDate: Tue Feb 19 18:32:51 2019 +0530
decidability updated - one case left
Code/Primes.idr | 69 ++++++++++++++++++++++++++++++++++++++++++++++++++-------
1 file changed, 61 insertions(+), 8 deletions(-)
commit c082b7e4ba83d14b8d8ebb2ec576f6581d2edc26
Author: SS-C4
AuthorDate: Sat Feb 16 17:05:44 2019 +0530
Commit: SS-C4
CommitDate: Sat Feb 16 17:05:44 2019 +0530
Commented out the code producing errors
Code/NatUtils.idr | 6 +++---
1 file changed, 3 insertions(+), 3 deletions(-)
commit 6e97ab4697f5bd80ea08b4092c78eb279142249d
Author: SS-C4
AuthorDate: Sat Feb 16 16:57:26 2019 +0530
Commit: SS-C4
CommitDate: Sat Feb 16 16:57:26 2019 +0530
Started work on a decidable routine for divisibility
Code/Primes.idr | 29 +++++++++++++++++++----------
1 file changed, 19 insertions(+), 10 deletions(-)
commit fde49aa31786e86e4a8f9ce622225c357ae40ab9
Author: SS-C4
AuthorDate: Sat Feb 16 14:55:56 2019 +0530
Commit: SS-C4
CommitDate: Sat Feb 16 14:55:56 2019 +0530
Added some lemmas to Primes and NatUtils, will be useful in defining a decidable type for divisibility.
Code/NatUtils.idr | 10 ++++++++
Code/Primes.idr | 77 +++++++++++++++++++++++++++++++++++++++++++++----------
2 files changed, 74 insertions(+), 13 deletions(-)
commit 08869b00f722e0dffe01f86478762397bda444ac
Author: SS-C4
AuthorDate: Fri Feb 15 18:55:37 2019 +0530
Commit: SS-C4
CommitDate: Fri Feb 15 18:55:37 2019 +0530
Updated the report with current progress
_reports/ss/ss.md | 20 +++++++++++++++++++-
1 file changed, 19 insertions(+), 1 deletion(-)
commit f6b8654ee55cd3d58a7452dd68d206c7cd63605e
Author: SS-C4
AuthorDate: Fri Feb 15 18:18:27 2019 +0530
Commit: SS-C4
CommitDate: Fri Feb 15 18:18:27 2019 +0530
Started work on primes. Defined a total order for Nats, and created a primitive primality checker
Code/Primes.idr | 57 ++++++++++++++++++++++++++++++++++++++++++++++++---------
1 file changed, 48 insertions(+), 9 deletions(-)
commit 4ec18e3787fe0c4c6874f8ecedcc14931c70dca7
Author: SS-C4
AuthorDate: Thu Feb 14 10:35:32 2019 +0530
Commit: SS-C4
CommitDate: Thu Feb 14 10:35:32 2019 +0530
Pushing.
Code/Primes.idr | 27 +++++++++++++++++++++++++++
1 file changed, 27 insertions(+)
commit 8d438c15a8a4837bd6dde5a066970f8d3eeda4a8
Author: SS-C4
AuthorDate: Thu Feb 14 10:00:12 2019 +0530
Commit: SS-C4
CommitDate: Thu Feb 14 10:00:12 2019 +0530
Changed filename, and added the divZZ function in MultiSolver.idr (for Abishek's LinearAlgebra to compile)
Code/LinearAlgebra.idr | 8 ++++++--
Code/{Linear.MultiSolver.idr => MultiSolver.idr} | 8 ++++++--
2 files changed, 12 insertions(+), 4 deletions(-)
commit 4d81e7e8dfb585de2e09997a5537b62092fbe4b5
Author: SS-C4
AuthorDate: Tue Feb 12 11:14:40 2019 +0530
Commit: SS-C4
CommitDate: Tue Feb 12 11:14:40 2019 +0530
Completed the proof.
GeneralEqSolver now can solve an equation
ax+b=c (a,b,c :ZZ)with proof that it is actually a solution.
Code/Linear.idr | 13 ++++++-------
1 file changed, 6 insertions(+), 7 deletions(-)
commit 5071a3bbe4ae3da0e2013e105ab3c20ae5aa6752
Author: SS-C4
AuthorDate: Sun Feb 10 09:16:59 2019 +0530
Commit: SS-C4
CommitDate: Sun Feb 10 09:16:59 2019 +0530
Added usage instructions
Code/Linear.MultiSolver.idr | 5 +++++
1 file changed, 5 insertions(+)
commit 74a47fb42abdeb7281f7524a1460922cb7fb8bff
Author: SS-C4
AuthorDate: Sun Feb 10 09:09:13 2019 +0530
Commit: SS-C4
CommitDate: Sun Feb 10 09:09:13 2019 +0530
Changed input type to ZZPair and implemented a solver for a system of linear equations
Code/Linear.MultiSolver.idr | 98 +++++++++++++++++++++++++++++----------------
1 file changed, 63 insertions(+), 35 deletions(-)
commit 228398917996fa51a64aa4eb5d312d59dc796a63
Author: SS-C4
AuthorDate: Sat Feb 9 21:42:41 2019 +0530
Commit: SS-C4
CommitDate: Sat Feb 9 21:42:41 2019 +0530
Defined inverses for matrices of ZZPairsand framework for solving systems of linear equations
Code/BaseN.idr | 1 +
Code/Linear.MultiSolver.idr | 147 ++++++++++++++++++++++++++++++++++++++++++++
2 files changed, 148 insertions(+)
commit 62a2c8e960d6ecf9956b21e8d3037b0f71ac3521
Author: SS-C4
AuthorDate: Thu Feb 7 06:38:16 2019 +0530
Commit: SS-C4
CommitDate: Thu Feb 7 06:38:16 2019 +0530
Minor changes in Bezout (to ZZ) and almost complete proof of gcd dividing both a and b.
Code/Bezout.idr | 17 +++++++--------
Code/gcd.idr | 64 +++++++++++++++++++++++++++++++++++++++++----------------
2 files changed, 55 insertions(+), 26 deletions(-)
commit 4c3f41272d4ae7351a8dd44ba1012ed612f8a947
Author: SS-C4
AuthorDate: Wed Feb 6 05:56:57 2019 +0530
Commit: SS-C4
CommitDate: Wed Feb 6 05:56:57 2019 +0530
update simplifyRational and aux functions
Code/Rationals.idr | 26 ++++++++++++++++++--------
1 file changed, 18 insertions(+), 8 deletions(-)
commit 6be8c52558546ca254c4b1bc498e3b257d4ca280
Author: SS-C4
AuthorDate: Wed Feb 6 05:55:44 2019 +0530
Commit: SS-C4
CommitDate: Wed Feb 6 05:55:44 2019 +0530
added ZZ.idr and converted some functions to ZZ
Code/ZZ.idr | 355 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
1 file changed, 355 insertions(+)
commit 55bd91abd5b018088f85c3af26941d2d7a788f11
Author: SS-C4
AuthorDate: Mon Feb 4 13:04:20 2019 +0530
Commit: SS-C4
CommitDate: Mon Feb 4 13:04:20 2019 +0530
Added solver for single equation, also checking if the solution exists.
Proofs TBD.
Code/Linear.idr | 16 ++++++++++++++++
Code/Rationals.idr | 2 ++
2 files changed, 18 insertions(+)
commit c92a54c3a915e40b049eabfa008c3bb482ca878a
Author: SS-C4
AuthorDate: Tue Jan 29 13:59:56 2019 +0530
Commit: SS-C4
CommitDate: Tue Jan 29 13:59:56 2019 +0530
Shifted Rationals.idr to Code/
Code/Rationals.idr | 96 ++++++++++++++++++++++++++++++++++++------------------
Rationals.idr | 87 -------------------------------------------------
2 files changed, 64 insertions(+), 119 deletions(-)
commit 20442039fe1f17278007c319120729b7755a2c89
Author: SS-C4
AuthorDate: Mon Jan 28 07:41:05 2019 +0530
Commit: SS-C4
CommitDate: Mon Jan 28 07:41:05 2019 +0530
Added equality type and simplifyRational
Rationals.idr | 36 +++++++++++++++++++++++++++++++++---
1 file changed, 33 insertions(+), 3 deletions(-)
commit f3333ebc609f4807cebee152a4b4691fdff298bb
Author: SS-C4
AuthorDate: Sun Jan 27 22:59:07 2019 +0530
Commit: SS-C4
CommitDate: Sun Jan 27 22:59:07 2019 +0530
Added function to simplify rationals and to generate inverses of rationals.
Proofs still remain to be done. Boolean version of equality implemented.
Code/Rationals.idr | 35 ++++++++++++++++++++++++++++++++---
1 file changed, 32 insertions(+), 3 deletions(-)