Project Report for Logic, Types, Spaces 2019
S Sriram
Outline of the work done
Contributions (Final)
Rationals
- 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.
Linear Equations
- 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
GCD
- I defined a divisibility type, which is useful for multiple purposes, and is present in different files as well (introduced in commit gcd.idr)
Solving multiple linear Equations
- 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 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
NatUtils
- 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.
Primes
- 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.
- 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 rewrites 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.
- 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
Log of git commits by author
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(-)