## Report on contributions to Projects in LTS 2019

#### Merge

1. I implemented the merge1 function that merges two sorted lists such that the resulting list is sorted in Merge.idr

## Bezout’s lemma

1. I implemented an function, Bezout that (given two natural numbers a and b) performs Euclidean algorithm and returns two integers x and y such that d = ax +by where d = GCD (a,b) in Bezout.idr
2. inplemented EuclList which gives a list of quotients and remainders when applying Euclid’s algorithm to two natural numbers a and b. Link here. This commit consists of both my code and Rohit’s code as Rohit had accidentally put his code outside the code folder.

## Divisors

1. Implemented IsDivisibleZ and IsCommonFactorZ types which are based on the corresponding data types for natural numbers created by Sriram and Rohit respectively. Also the function oneDiv is based on Sriram’s code. The rest of the code in Divisors.idr is my code as of the time of writing this report.
2. I proved a few theorems about divisibility of integers and about GCD.

## ZZ

1. I had to create many auxiliary functions and data types in ZZ.idr for use in Divisors.idr. Some of these are
2. Implemented LTEZ type which is the less than or equal to type for integers. Link here

3. Proved antisymmetry of LTE type for natural numbers and LTEZ type for integers. Link here
4. Implemented IsPositive data type and DecidePositive ,a function that returns whether an integer is positive or not with proof.
5. isLTEZ function that works just like isLTE for Nat
6. And a few other auxiliary functions.
7. I copied some of Vrunda Rathi’s code into ZZ.idr when I was fixing some errors Link here

## gcd.idr

1. Implemented PlusDiv and MultDiv for natural numbers which were later changed to integers in Divisors.idr.Link here
2. Made the euclDivide function total Link here

## Graph.idr

1. The AdjacentsAreConnected function returns a proof that 2 adjacent vertices are connected by an edge or nothing if they are not connected.
2. EdgeisPath function proves that adjacent vertices (i.e. vertices that have an edge between them) are connected
3. ConnectedComponents takes a simple graph (symmetric matrix with 0’s and 1’s) and returns a list of connected components as a list of lists of Nats
4. PathWithProof function returns a simple path between two vertices if there is a path with proof or Nothing if there is no path. Here a path is represented as a List of vertices that were traversed.
5. Most of the functions used are not total, and they will work properly only as long as the adjacency matrix of a simple graph is given as input.
6. The file Graphexamples.idr has a few examples of how to use these functions.

## GCD of integers

1.The file GCDZZ.idr has a function gcdZZ which returns the gcd of two integers with proof given that not both of them are zero

# Post Midterm

## Divisors.idr

1.The function divideByGcdThenGcdOne proves that gcd ( (a/gcd(a,b)),(b/gcd(a,b)) ) =1

## GCD of integers GCDZZ.idr

1. The function bezoutCoeffs takes two integers and a proof that they are not both zero and returns the GCD of the two integers, a proof that it is the gcd and the Bezout coefficients with proof.
2. The function, gcdOfMultiple proves the theorem that if m>0 and a and b are not both zero, then gcd(ma,mb) = m *gcd (a,b)
3.  The function, caCoprimeThencDivb proves the theorem that if c ab and gcd (a,c) =1 , then c b
4. Introduced GCDZr type which defines GCD as the greatest of the common divisors and proved the equivalence of the two definitions in the functions GCDZImpliesGCDZr and GCDZrImpliesGCDZ
5. Introduced a SmallestPosLinComb which defines the smallest positive linear combination of two integers. Showed that this is equivalent to GCDZ in the functions gcdIsSmallestPosLinComb smallestPosLinCombIsGcd.
6. gcdIsLinComb function proves that gcd (a,b) is a linear combination of a and b .

## decDivZ.idr

1. The function decDivisibleZ checks whether one integer is divisible by the other with proof. (It depends on Sriram’s decDiv function.) It works for any two integers.

## ZZUtils.idr

1. Defined types , IsNonNegative, IsNegative, NotZero for integers.
2. Proved multiplication and addition cancellation laws for integers.
3. productOneThenNumbersOne function proves that if (a*b=1) then either (a=1,b=1) or (a=-1,b=-1)
4. There are also other useful functions in ZZUtils

## TwoVarDiophEq.idr

(Done in collaboration with Abhishek)

1. aByd and bByd functions extract the values of a/gcd(a,b) and b/gcd(a,b) respectively from the definition of GCDZ.
2. Implemented findAllSolutions function which given three integers a, b and c, it outputs either a proof that c = xa +yb is impossible or a proof that all integers x and y satisfy the equation (this happens when a=b=c=0) or 4 integers x1 , y1 , pa and pb such that for any integer k, x=x1+k*pa y=y1+k*pb is a solution of c=xa+yb and whenever c=xa+yb ,there exists an integer, k such that x=x1+k*pa y=y1+k*pb.

### Log of git commits by author


AuthorDate: Sun Mar 31 09:30:25 2019 +0530
Commit:     GitHub
CommitDate: Sun Mar 31 09:30:25 2019 +0530

Update report

Update report

_reports/shafil/shafil.md | 35 ++++++++++++++++++++++++++++++++++-
1 file changed, 34 insertions(+), 1 deletion(-)

commit 869efe59b6292916d32931e4e4c3e4e0fb887a46
AuthorDate: Sun Mar 31 09:29:09 2019 +0530
Commit:     GitHub
CommitDate: Sun Mar 31 09:29:09 2019 +0530

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

AuthorDate: Wed Mar 13 15:13:09 2019 +0530
Commit:     GitHub
CommitDate: Wed Mar 13 15:13:09 2019 +0530

Changed implicit arguments to explicit in findAllSolutions

Changed implicit arguments to explicit in findAllSolutions

Code/TwoVarDiophEq.idr | 45 +++++++++++++++++++++++++--------------------
1 file changed, 25 insertions(+), 20 deletions(-)

commit d7835b1311f71ee500db005643c42e6fd14ca72c
AuthorDate: Wed Mar 13 07:08:56 2019 +0530
Commit:     GitHub
CommitDate: Wed Mar 13 07:08:56 2019 +0530

Completed findAllSolutions function

Completed findAllSolutions function

Code/TwoVarDiophEq.idr | 140 ++++++++++++++++++++++++++++++++++++++-----------
1 file changed, 108 insertions(+), 32 deletions(-)

commit a0655ce72230985d241f9a949036ec7b169260bb
AuthorDate: Mon Mar 11 15:09:10 2019 +0530
Commit:     GitHub
CommitDate: Mon Mar 11 15:09:10 2019 +0530

Created a findAllSolutions function (not complete)

|||Given three integers a, b and c, the findAllSolutions function outputs either
|||a proof that c = xa +yb is impossible or
|||a proof that all integers x and y satisfy the equation (this happens when a=b=c=0)
|||or 4 integers x1 , y1 , pa and pb such that for any integer k,
|||x=x1+k*pa  y=y1+k*pb is a solution of c=xa+yb
|||and whenever c=xa+yb ,there exists an integer, k such that
||| x=x1+k*pa  y=y1+k*pb

Code/TwoVarDiophEq.idr | 46 ++++++++++++++++++++++++++++++++++++++++++++++
1 file changed, 46 insertions(+)

commit 2f1e0139b683d91996cfb5c0470fa974dc399876
AuthorDate: Mon Mar 11 15:07:41 2019 +0530
Commit:     GitHub
CommitDate: Mon Mar 11 15:07:41 2019 +0530

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

commit c704d8a0e730623b7c5f028d4ae9a9877f4e1ce8
AuthorDate: Sun Mar 10 16:39:35 2019 +0530
Commit:     GitHub
CommitDate: Sun Mar 10 16:39:35 2019 +0530

a typo correction

a typo correction

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

AuthorDate: Sun Mar 10 16:38:28 2019 +0530
Commit:     GitHub
CommitDate: Sun Mar 10 16:38:28 2019 +0530

a typo correction

a typo correction

Code/TwoVarDiophEq.idr | 3 +--
1 file changed, 1 insertion(+), 2 deletions(-)

commit bc4affa9e53daf80f5c5fdd0a00f2570b8a471e1
AuthorDate: Sun Mar 10 16:35:07 2019 +0530
Commit:     GitHub
CommitDate: Sun Mar 10 16:35:07 2019 +0530

Complete characterization of solutions of two variable linear homogenous Diophantine equations

Gave a general formula with proof of solutions of two variable linear homogenous Diophantine equations and proved that all solutions are of this form when the first integer is not zero.

Code/TwoVarDiophEq.idr | 114 +++++++++++++++++++++++++++++++++++++++++++++++++
1 file changed, 114 insertions(+)

commit eb4e6a1e1c79a2b459d6ff581bd81606ed81f690
AuthorDate: Sun Mar 10 16:32:05 2019 +0530
Commit:     GitHub
CommitDate: Sun Mar 10 16:32:05 2019 +0530

and some other helper functions

Code/ZZUtils.idr | 51 ++++++++++++++++++++++++++++++++++++++++++++++++++-
1 file changed, 50 insertions(+), 1 deletion(-)

commit 54b5b7f61439ce6866114e0eaa452a52b00b25b3
AuthorDate: Sun Mar 10 16:30:45 2019 +0530
Commit:     GitHub
CommitDate: Sun Mar 10 16:30:45 2019 +0530

A helper function

A helper function

Code/Divisors.idr | 10 ++++++++--
1 file changed, 8 insertions(+), 2 deletions(-)

commit 1936d776f16cc22f6007898b096bd89e13159282
AuthorDate: Sun Mar 10 08:53:24 2019 +0530
Commit:     GitHub
CommitDate: Sun Mar 10 08:53:24 2019 +0530

Proved that (d|a) implies ((-d)|(-a))

Proved that (d|a) implies ((-d)|(-a))

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

commit 51d7334df7f9cd0e280e16537b33c0bf6fe01d65
AuthorDate: Sun Mar 10 08:52:14 2019 +0530
Commit:     GitHub
CommitDate: Sun Mar 10 08:52:14 2019 +0530

A decide divisibility function for integers

Given any two integers a and b, The decDivisibleZ function returns proof that b|a when it is the case or a proof that b does not divide a.
Depends on Sriram's decDiv function.
Also showed the equivalence of isDivisible from Primes.idr and IsDivisibleZ from Divisors.idr for positive integers

Code/decDivZ.idr | 78 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++
1 file changed, 78 insertions(+)

commit 50be649c390cbbbdd302dc837f37d55666ce619a
AuthorDate: Sat Mar 9 11:00:43 2019 +0530
Commit:     GitHub
CommitDate: Sat Mar 9 11:00:43 2019 +0530

All the functions that depended on the Euclid's algorithm are now total.
These include GCDCalc, gcdZZ, bez and bezoutCoeffs

Code/GCDZZ.idr | 93 +++++++++++++++++++++++++++++++---------------------------
1 file changed, 49 insertions(+), 44 deletions(-)

commit d4b9bc8057f5f9454a724ded36eb4455385c5def
AuthorDate: Sat Mar 9 10:59:07 2019 +0530
Commit:     GitHub
CommitDate: Sat Mar 9 10:59:07 2019 +0530

total Euclid algorithm with bezout coefficients

Implemented a bounded gcd function which returns gcd along with bezout coefficients along with proofs

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

commit 7a03388bdc2ab34b063a9325e96a662e12ec78b0
AuthorDate: Fri Mar 8 21:42:17 2019 +0530
Commit:     GitHub
CommitDate: Fri Mar 8 21:42:17 2019 +0530

Some helper functions for creating a total Euclid algorithm

Some helper functions for creating a total Euclid algorithm

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

commit c86f457ae75e981af52e90e0052fd36f212202d2
AuthorDate: Fri Mar 8 21:40:55 2019 +0530
Commit:     GitHub
CommitDate: Fri Mar 8 21:40:55 2019 +0530

GCDCalc is now total

GCDCalc is now total

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

commit 90d74014114bdbc80fd908f9f0471709b6e37220
AuthorDate: Fri Mar 8 21:39:49 2019 +0530
Commit:     GitHub
CommitDate: Fri Mar 8 21:39:49 2019 +0530

Proved that gcd (a,1) =1 for all integers a

Proved that gcd (a,1) =1 for all integers a

Code/Divisors.idr | 17 ++++++++++++++---
1 file changed, 14 insertions(+), 3 deletions(-)

commit 38666a17ff2f4ea837d868cb968617b330430c17
AuthorDate: Fri Mar 8 21:38:48 2019 +0530
Commit:     GitHub
CommitDate: Fri Mar 8 21:38:48 2019 +0530

boundedGCDZ which gives gcd with proof

boundedGCDZ gives gcd with proof for two Non negative integers not both zero

Code/BoundedGCD.idr | 56 +++++++++++++++++++++++++++++++++++++++++++++++++++++
1 file changed, 56 insertions(+)

commit db43c3904e4522f452a5ba76f2775595e3513f1f
AuthorDate: Mon Mar 4 22:32:50 2019 +0530
Commit:     GitHub
CommitDate: Mon Mar 4 22:32:50 2019 +0530

corrected a minor typo

corrected a minor typo

Code/ZZUtils.idr | 24 ++++++++++++++++++------
1 file changed, 18 insertions(+), 6 deletions(-)

commit a544b6eda03a7fc607f1351224f0be02978b901e
AuthorDate: Mon Mar 4 22:31:54 2019 +0530
Commit:     GitHub
CommitDate: Mon Mar 4 22:31:54 2019 +0530

Proved c|ab and gcd(c,a) =1 implies c|b

Also defines a type, SmallestPosLinComb a b d that is inhabited iff  d is the smallest positive linear combination of a and b.
Proved that this is equivalent to GCDZ a b d

Code/GCDZZ.idr | 94 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++-
1 file changed, 93 insertions(+), 1 deletion(-)

commit 38bb9c724ca5dfd38cce47545345bae3d01958a0
AuthorDate: Sun Mar 3 22:38:37 2019 +0530
Commit:     GitHub
CommitDate: Sun Mar 3 22:38:37 2019 +0530

Proved that LTE (S a)  a is impossible

Proved that LTE (S a)  a is impossible

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

commit 5f89fdae0810b4790591b3219a13f935440195fd
AuthorDate: Sun Mar 3 22:37:02 2019 +0530
Commit:     GitHub
CommitDate: Sun Mar 3 22:37:02 2019 +0530

Created a decide function for notbothzeroZ

Created a decide function for notbothzeroZ and a few other helper functions

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

commit 8e4382bac9061924d2d8705b1a30bf7c1d5b99f9
AuthorDate: Sun Mar 3 22:35:45 2019 +0530
Commit:     GitHub
CommitDate: Sun Mar 3 22:35:45 2019 +0530

Defined GCD using the actual definition and showed that both definitions are equivalent

Defined a GCDZr type which is the actual definition of GCD as the greatest of the common divisors and proved that it is equivalent to my earlier definition.

Code/GCDZZ.idr | 75 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
1 file changed, 75 insertions(+)

AuthorDate: Sun Mar 3 14:58:39 2019 +0530
Commit:     GitHub
CommitDate: Sun Mar 3 14:58:39 2019 +0530

A helper function for gcdOfmultiple

A helper function for gcdOfmultiple

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

commit 027bf6e0eaf5220bb7544b27f9c023c5a48e4076
AuthorDate: Sun Mar 3 14:57:29 2019 +0530
Commit:     GitHub
CommitDate: Sun Mar 3 14:57:29 2019 +0530

Proved that gcd (ma,mb) = m(gcd(a,b))

Proved that gcd (ma,mb) = m(gcd(a,b))
Also used assert total on a few functions for now

Code/GCDZZ.idr | 47 +++++++++++++++++++++++++++++++++++++++++------
1 file changed, 41 insertions(+), 6 deletions(-)

commit 7eb59b86df3524c5b34bb16f3f727c70aabcb094
AuthorDate: Fri Mar 1 18:28:39 2019 +0530
Commit:     GitHub
CommitDate: Fri Mar 1 18:28:39 2019 +0530

Proof that (-a)*(-b) = a*b

Proof that (-a)*(-b) = a*b

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

commit ca4a15f0110647e52be4ec3ec1b5990a34f0883f
AuthorDate: Fri Mar 1 18:27:45 2019 +0530
Commit:     GitHub
CommitDate: Fri Mar 1 18:27:45 2019 +0530

Bezout coefficients for integers

The bezoutCoeffs function returns bezout coefficients with proof for any two integers not both zero

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

commit e68a5e0350e879fee38df8c9bc7992ed9480a18a
AuthorDate: Thu Feb 28 22:53:14 2019 +0530
Commit:     GitHub
CommitDate: Thu Feb 28 22:53:14 2019 +0530

A helper function for Bezout Lemma

A helper function for Bezout Lemma

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

commit 5256ffaaeca0c8812c5fa67056e4b3202fd946ca
AuthorDate: Thu Feb 28 22:52:12 2019 +0530
Commit:     GitHub
CommitDate: Thu Feb 28 22:52:12 2019 +0530

Bezout coefficients with proof

The bez function returns the Bezout coefficients with proof that d = gcd (a,b) and d= m*a +n*b
for positive a and nonnegative b

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

commit 4378d3f240b7bf94ddb2ef7788175938830fe69a
AuthorDate: Thu Feb 28 15:48:56 2019 +0530
Commit:     GitHub
CommitDate: Thu Feb 28 15:48:56 2019 +0530

Proved Cancellation law for multiplication of integers

Proved Cancellation law for multiplication of integers.
Also proved that if ab =1 , then a=1 and b=1 or a=-1 and b=-1

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

commit eded6bcc0c2db3bbc7a350f67076afe1046d94da
AuthorDate: Thu Feb 28 15:47:17 2019 +0530
Commit:     GitHub
CommitDate: Thu Feb 28 15:47:17 2019 +0530

Proved that gcd ( (a/gcd(a,b)),(b/gcd(a,b)) ) =1

Proved that  when two numbers are divided by their gcd, then the gcd of the new numbers is 1

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

commit 241dc9c4d3ffa47f8c0ac4e940c3fdfc80e99559
AuthorDate: Mon Feb 25 23:31:48 2019 +0530
Commit:     GitHub
CommitDate: Mon Feb 25 23:31:48 2019 +0530

Some useful functions required for Divisors.idr

Defined NotZero type inhabited by nonzero integers
and some basic proofs

Code/ZZUtils.idr | 37 +++++++++++++++++++++++++++++++------
1 file changed, 31 insertions(+), 6 deletions(-)

AuthorDate: Mon Feb 25 23:30:09 2019 +0530
Commit:     GitHub
CommitDate: Mon Feb 25 23:30:09 2019 +0530

Completed multiplication cancellation laws

Completed multiplication cancellation laws and 2 theorems about LT

Code/NatUtils.idr | 32 ++++++++++++++++++++++++++------
1 file changed, 26 insertions(+), 6 deletions(-)

commit 4edfc4c70b53cf0b94ca3057640792de94f653be
AuthorDate: Mon Feb 25 23:28:48 2019 +0530
Commit:     GitHub
CommitDate: Mon Feb 25 23:28:48 2019 +0530

Proved that 0 cannot divide a non zero number
Also -1 divides anything

Code/Divisors.idr | 23 +++++++++++++++++++++++
1 file changed, 23 insertions(+)

commit 7040bd71e3ed10410ca039065708650468f41b7b
AuthorDate: Sun Feb 24 21:06:19 2019 +0530
Commit:     GitHub
CommitDate: Sun Feb 24 21:06:19 2019 +0530

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

commit 3cc8b0b75378c9bc8f47fa938bf3cd27e6a12e63
AuthorDate: Sun Feb 24 21:02:07 2019 +0530
Commit:     GitHub
CommitDate: Sun Feb 24 21:02:07 2019 +0530

Fixed an error in the documentation

Fixed an error in the documentation

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

commit 151a3b374fb9d69aca91fe2f812410fe746ede9d
AuthorDate: Sun Feb 24 21:00:32 2019 +0530
Commit:     GitHub
CommitDate: Sun Feb 24 21:00:32 2019 +0530

Update report

Update report

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

AuthorDate: Sat Feb 23 22:14:47 2019 +0530
Commit:     GitHub
CommitDate: Sat Feb 23 22:14:47 2019 +0530

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

commit 1e286ac0f776da7d3094a578b966d210eca5ea76
AuthorDate: Sat Feb 23 22:05:53 2019 +0530
Commit:     GitHub
CommitDate: Sat Feb 23 22:05:53 2019 +0530

exported it

exported it

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

commit cabe3ee49e3995300e52993d717294e29ed6124e
AuthorDate: Sat Feb 23 21:59:51 2019 +0530
Commit:     GitHub
CommitDate: Sat Feb 23 21:59:51 2019 +0530

gcdZZ returns gcd with proof for a and b where a and b are not both zero

gcdZZ returns gcd with proof for a and b where a and b are not both zero

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

commit 73af360c14ae88bbbbb385aaa447e48187f55b65
AuthorDate: Sat Feb 23 21:57:51 2019 +0530
Commit:     GitHub
CommitDate: Sat Feb 23 21:57:51 2019 +0530

A minor name change

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

commit d0c7a97ea7447cd14e544e5b688005686bf7ccc7
AuthorDate: Sat Feb 23 20:50:14 2019 +0530
Commit:     GitHub
CommitDate: Sat Feb 23 20:50:14 2019 +0530

Created a GCDCalc function

Created a GCDCalc function that returns GCD with proof for two integers a and  such that a is positive and b is non negative.
I couldn't convince idris that it is total. So I did this in a new file.

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

commit 806336344553fcfce20edd3a40e4c77528744736
AuthorDate: Sat Feb 23 20:47:29 2019 +0530
Commit:     GitHub
CommitDate: Sat Feb 23 20:47:29 2019 +0530

Added a subOnBothSides function which states that if a = b+c , then a+(-c)=b

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

commit 24a18b9e0ed934f9ec563e7dc8963b5142cd24f7
AuthorDate: Sat Feb 23 20:46:16 2019 +0530
Commit:     GitHub
CommitDate: Sat Feb 23 20:46:16 2019 +0530

A utility file for ZZ

Created a utility file for ZZ .

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

commit 099b3a34fdd34529526fab7e5823ddd195aa9bbb
AuthorDate: Sat Feb 23 20:44:49 2019 +0530
Commit:     GitHub
CommitDate: Sat Feb 23 20:44:49 2019 +0530

Added a few functions that help in finding Gcd

Added a few functions that help in finding Gcd which include different versions of euclidConservesGcd and also that gcd (-a,b)=gcd (a,b)
and other auxiliary functions

Code/Divisors.idr | 70 +++++++++++++++++++++++++++++++++++++++++++++++++++----
1 file changed, 66 insertions(+), 4 deletions(-)

commit 8b72b8e7f55bd58a2cca4c3d15d6c2f3c168a761
AuthorDate: Wed Feb 20 13:59:19 2019 +0530
Commit:     GitHub
CommitDate: Wed Feb 20 13:59:19 2019 +0530

Made sure the import is working

Changed the name of Lecture.Evens and imported it into Merge.idr

Code/Merge.idr | 26 +++++++++++++-------------
1 file changed, 13 insertions(+), 13 deletions(-)

commit b8820d084173839192dff38a044fab851a0dbeb6
AuthorDate: Wed Feb 20 13:57:53 2019 +0530
Commit:     GitHub
CommitDate: Wed Feb 20 13:57:53 2019 +0530

renaming so that it is importable

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

commit 5a74f42697c26f4d01bd371a1634fb8e261a979b
AuthorDate: Wed Feb 20 13:41:28 2019 +0530
Commit:     GitHub
CommitDate: Wed Feb 20 13:41:28 2019 +0530

Update shafil.md

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

commit f568ccbbed255260657d6671625dc63d93e0d941
AuthorDate: Wed Feb 20 13:41:00 2019 +0530
Commit:     GitHub
CommitDate: Wed Feb 20 13:41:00 2019 +0530

Update report

The report

_reports/shafil/shafil.md | 37 ++++++++++++++++++++++++++++++++++++-
1 file changed, 36 insertions(+), 1 deletion(-)

AuthorDate: Tue Feb 19 19:38:15 2019 +0530
Commit:     GitHub
CommitDate: Tue Feb 19 19:38:15 2019 +0530

euclidDivide function gives quotient and remainder on division with proof . It wasnt total before .

Code/gcd.idr | 23 +++++++++++++++--------
1 file changed, 15 insertions(+), 8 deletions(-)

AuthorDate: Tue Feb 19 17:33:55 2019 +0530
Commit:     GitHub
CommitDate: Tue Feb 19 17:33:55 2019 +0530

Implemented isLTE function for ZZ

Implemented isLTE function for ZZ and also LTEZSucc and LTEZPred which proves that the successors and predecessors of an integer have the same order as the original integers

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

commit 2499963e7bd8e8a576ce0d302760ac81537189b3
AuthorDate: Sat Feb 16 23:08:49 2019 +0530
Commit:     GitHub
CommitDate: Sat Feb 16 23:08:49 2019 +0530

Update gcd.idr

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

commit ff00d4e82d5a1c18cb1dc33f588cc47058931224
AuthorDate: Sat Feb 16 23:08:08 2019 +0530
Commit:     GitHub
CommitDate: Sat Feb 16 23:08:08 2019 +0530

Update Rationals.idr

Code/Rationals.idr | 7 -------
1 file changed, 7 deletions(-)

AuthorDate: Sat Feb 16 23:07:23 2019 +0530
Commit:     GitHub
CommitDate: Sat Feb 16 23:07:23 2019 +0530

Update Primes.idr

Code/Primes.idr | 30 +++++++++++++++++++-----------
1 file changed, 19 insertions(+), 11 deletions(-)

commit faa807e50e658f1a54c8640b85ffce140715eaa2
AuthorDate: Sat Feb 16 23:06:14 2019 +0530
Commit:     GitHub
CommitDate: Sat Feb 16 23:06:14 2019 +0530

Update ZZ.idr

Code/ZZ.idr | 39 ++++++++++++++++-----------------------
1 file changed, 16 insertions(+), 23 deletions(-)

commit dfc6cf315d3380d50d2c06a43701886c0ac70fd8
AuthorDate: Sat Feb 16 23:05:29 2019 +0530
Commit:     GitHub
CommitDate: Sat Feb 16 23:05:29 2019 +0530

Update Divisors.idr

Code/Divisors.idr | 52 ++++++++++++++++++++++++++--------------------------
1 file changed, 26 insertions(+), 26 deletions(-)

commit 82ac9e75b3f0da5d6080ca4969c898a75b1f551a
AuthorDate: Sat Feb 16 23:04:45 2019 +0530
Commit:     GitHub
CommitDate: Sat Feb 16 23:04:45 2019 +0530

Update Bezout.idr

Code/Bezout.idr | 50 +++++++++++++-------------------------------------
1 file changed, 13 insertions(+), 37 deletions(-)

commit e2325bf88a48a7f39cd13d2f3183d5eecd7c119b
AuthorDate: Sat Feb 16 23:04:09 2019 +0530
Commit:     GitHub
CommitDate: Sat Feb 16 23:04:09 2019 +0530

Update NatUtils.idr

Code/NatUtils.idr | 19 +------------------
1 file changed, 1 insertion(+), 18 deletions(-)

commit dab2e23b626b6d97f60cb10832e5f8dd1d47c074
AuthorDate: Fri Feb 15 20:26:45 2019 +0530
Commit:     GitHub
CommitDate: Fri Feb 15 20:26:45 2019 +0530

Update Divisors.idr

Code/Divisors.idr | 52 ++++++++++++++++++++++++++++------------------------
1 file changed, 28 insertions(+), 24 deletions(-)

commit 80d17770a56c23186b11091d396908b22e37fb21
AuthorDate: Wed Feb 13 22:30:40 2019 +0530
Commit:     GitHub
CommitDate: Wed Feb 13 22:30:40 2019 +0530

Copied some code from ZZ.idr which might be useful

Added some functions that deal with LTE and in particular, the theorem that (m<=n) and (n<=m) implies n=m

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

AuthorDate: Wed Feb 13 22:26:55 2019 +0530
Commit:     GitHub
CommitDate: Wed Feb 13 22:26:55 2019 +0530

The Theorem that if c and d are positive, d|c and c|d =>(c=d)

PosDivAndDivByImpliesEqual is the theorem that if c and d are positive, d|c and c|d =>(c=d)
Implemented using many auxiliary functions from ZZ.idr

Code/Divisors.idr | 10 ++++++++++
1 file changed, 10 insertions(+)

commit a9260c3fc1d4dfcbe515705cc7d670d50b260d8d
AuthorDate: Wed Feb 13 22:23:45 2019 +0530
Commit:     GitHub
CommitDate: Wed Feb 13 22:23:45 2019 +0530

Implemented LTE type for ZZ

Implemented LTE type for ZZ
Also wrote some other useful theorems and functions

Code/ZZ.idr | 93 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++---
1 file changed, 89 insertions(+), 4 deletions(-)

commit 41e311a76ed8086f09976080c00dde49446fe948
AuthorDate: Wed Feb 13 15:53:12 2019 +0530
Commit:     GitHub
CommitDate: Wed Feb 13 15:53:12 2019 +0530

Added the theorem gcd(a,b)=d => gcd (b, a+ b(-m))=d

This theorem can be used to show that that the Gcd is conserved in each step of the Euclid's algorithm

Code/Divisors.idr | 22 ++++++++++++----------
1 file changed, 12 insertions(+), 10 deletions(-)

commit 7c9388fb666202f5c0ee843e7bedc5c097b231af
AuthorDate: Wed Feb 13 15:50:22 2019 +0530
Commit:     GitHub
CommitDate: Wed Feb 13 15:50:22 2019 +0530

Added a few functions that can be used for rewriting

addAndSubNeutralZ function gives a proof that  (((a+b)+(-b))=a)

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

commit 37108182ab621afd71e949eab8bc410ace5c3583
AuthorDate: Tue Feb 12 23:58:18 2019 +0530
Commit:     GitHub
CommitDate: Tue Feb 12 23:58:18 2019 +0530

proved that gcd(a,0)=a
proved that a|a
A sketch of a proof that Euclid's algorithm preserves gcd in each step.

Code/Divisors.idr | 33 +++++++++++++++++++++++++++++++--
1 file changed, 31 insertions(+), 2 deletions(-)

commit 35e6d26e5ae359b3922ef63bd26966777ec50584
AuthorDate: Tue Feb 12 23:54:44 2019 +0530
Commit:     GitHub
CommitDate: Tue Feb 12 23:54:44 2019 +0530

multNegateRightZ gives a proof that k*(-j)=-(k*j)
multNegateRightIsNegateZ takes a proof of a=bc and creates a proof of (-a)=b(-c)

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

commit 6bd8d9b3db72d5e0dae70ff954fb82c1f6c9eaed
AuthorDate: Tue Feb 12 20:39:42 2019 +0530
Commit:     GitHub
CommitDate: Tue Feb 12 20:39:42 2019 +0530

Included a Gcd type that may be easier to use

Expanded on Rohit's ideas for defining common factors and Gcd. The Gcd is defined in a slightly different way.

Code/Divisors.idr | 15 +++++++++++++--
1 file changed, 13 insertions(+), 2 deletions(-)

commit 7c510cd0790d8b175b267e57264cf0102d22dc8e
AuthorDate: Tue Feb 12 20:31:37 2019 +0530
Commit:     GitHub
CommitDate: Tue Feb 12 20:31:37 2019 +0530

Created an IsPositive Data type

Created a function that returns a either a  proof that an integer is positive or a contradiction to the statement that the integer is positive

Code/ZZ.idr | 17 +++++++++++++++++
1 file changed, 17 insertions(+)

commit 519e30325385a58254f35020cea7e08180bb4850
AuthorDate: Tue Feb 12 14:21:35 2019 +0530
Commit:     GitHub
CommitDate: Tue Feb 12 14:21:35 2019 +0530

Changed import Evens to import Lecture.Evens

Changed import Evens to import Lecture.Evens

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

commit 5e61f6060314f68d4c9851f14965ca307ae61357
AuthorDate: Tue Feb 12 14:19:39 2019 +0530
Commit:     GitHub
CommitDate: Tue Feb 12 14:19:39 2019 +0530

Added a TransDivide function which states that b|a and c|b =>c|a

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

AuthorDate: Tue Feb 12 14:16:18 2019 +0530
Commit:     GitHub
CommitDate: Tue Feb 12 14:16:18 2019 +0530

Copied Rohit's code into File Bezout.idr and added a EuclList function

Copied Rohit's code into File Bezout.idr and added a EuclList function which returns a list of quotients and remainders on applying Euclid's Algorithm which may be useful in future proofs

Code/Bezout.idr | 132 ++++++++++++++++++++++++++++++++++++++++++++++++++------
1 file changed, 120 insertions(+), 12 deletions(-)

commit 5172740e01ca549f7b7490084c0545c142677c17
AuthorDate: Tue Feb 12 10:46:59 2019 +0530
Commit:     GitHub
CommitDate: Tue Feb 12 10:46:59 2019 +0530

Changed all Nats to ZZ in gcd.idr

This is just part of the file gcd.idr with all Nats changed to ZZ

Code/Divisors.idr | 27 +++++++++++++++++++++++++++
1 file changed, 27 insertions(+)

commit a275fc1c07c2dd6073d385351419d4abe1e3dd55
AuthorDate: Tue Feb 12 10:45:44 2019 +0530
Commit:     GitHub
CommitDate: Tue Feb 12 10:45:44 2019 +0530

Delete Divisors.idr

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

AuthorDate: Tue Feb 12 10:34:38 2019 +0530
Commit:     GitHub
CommitDate: Tue Feb 12 10:34:38 2019 +0530

Just changed all Nats to ZZ in gcd.idr

This is just some of the functions from gcd.idr with Nats changed to ZZ. I didnt delete the original file.

Divisors.idr | 27 +++++++++++++++++++++++++++
1 file changed, 27 insertions(+)

commit 6395fa5de4c1b394275b1307a77f8a80ea6e7b60
AuthorDate: Tue Feb 12 10:31:47 2019 +0530
Commit:     GitHub
CommitDate: Tue Feb 12 10:31:47 2019 +0530

Two useful functions and import Sign.idr

Added two functions that plusConstantRightZ and plusConstantLeftZ that give proofs that adding constants to equals  does not change equality
Modelled on the corresponding functions for Nat

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

commit 3e5c7d75bf1c1cd8a6873f77eaa6c89f43f2982b
AuthorDate: Tue Feb 12 10:27:50 2019 +0530
Commit:     GitHub
CommitDate: Tue Feb 12 10:27:50 2019 +0530

Copied Sign.idr into the folder for easy access

This is not my Code

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

AuthorDate: Sun Feb 10 15:31:31 2019 +0530
Commit:     GitHub
CommitDate: Sun Feb 10 15:31:31 2019 +0530

Update gcd.idr

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

commit c19cbf1c7064121fe551b75304ab797d95f739e2
AuthorDate: Fri Feb 8 19:33:09 2019 +0530
Commit:     GitHub
CommitDate: Fri Feb 8 19:33:09 2019 +0530

Rename graphexamples.idr to Graphexamples.idr

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

commit 21b2fa9e938d2865e346187463663d90663905e3
AuthorDate: Fri Feb 8 19:32:33 2019 +0530
Commit:     GitHub
CommitDate: Fri Feb 8 19:32:33 2019 +0530

Create graphexamples.idr

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

commit 50a4094370a05a05f8c38a08bfc1517ed1d68577
AuthorDate: Fri Feb 8 19:31:10 2019 +0530
Commit:     GitHub
CommitDate: Fri Feb 8 19:31:10 2019 +0530

Update Graph.idr

Code/Graph.idr | 14 +++++---------
1 file changed, 5 insertions(+), 9 deletions(-)

AuthorDate: Mon Feb 4 17:42:34 2019 +0530
Commit:     GitHub
CommitDate: Mon Feb 4 17:42:34 2019 +0530

Update Graph.idr

Code/Graph.idr | 44 ++++++++++++++++++++++++++++++++++++++++----
1 file changed, 40 insertions(+), 4 deletions(-)

commit 8afdd47a839d4991403158ceb3943dfcb15747de
AuthorDate: Mon Feb 4 15:11:15 2019 +0530
Commit:     GitHub
CommitDate: Mon Feb 4 15:11:15 2019 +0530

Update Graph.idr

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

commit a9f7cc46d45735ab8dbdf88bcf93fcaae0706843
AuthorDate: Sat Feb 2 11:59:38 2019 +0530
Commit:     GitHub
CommitDate: Sat Feb 2 11:59:38 2019 +0530

Update Graph.idr

Code/Graph.idr | 35 ++++++++++++++++++++++++++++++-----
1 file changed, 30 insertions(+), 5 deletions(-)

commit 289c48281868bd78b149b27410dba3481d85ed34
AuthorDate: Sat Feb 2 10:16:44 2019 +0530
Commit:     GitHub
CommitDate: Sat Feb 2 10:16:44 2019 +0530

Update Graph.idr

Code/Graph.idr | 15 +++++++++++++++
1 file changed, 15 insertions(+)

commit ae10a14435004be0a6fbcbc05455272c21c75b8e
AuthorDate: Sat Feb 2 07:26:29 2019 +0530
Commit:     GitHub
CommitDate: Sat Feb 2 07:26:29 2019 +0530

Update Graph.idr

Code/Graph.idr | 39 ++++++++++++++++++++-------------------
1 file changed, 20 insertions(+), 19 deletions(-)

AuthorDate: Sat Feb 2 07:14:50 2019 +0530
Commit:     GitHub
CommitDate: Sat Feb 2 07:14:50 2019 +0530

Create Graph.idr

Code/Graph.idr | 48 ++++++++++++++++++++++++++++++++++++++++++++++++
1 file changed, 48 insertions(+)

commit ff3a44a60c4ba678eb03dae47b46205fa7159e67
AuthorDate: Thu Jan 24 14:41:27 2019 +0530
Commit:     GitHub
CommitDate: Thu Jan 24 14:41:27 2019 +0530

Finding the Bezout coefficients

The Bezout function in this program gives the coefficients in the Bezout Lemma

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

AuthorDate: Wed Jan 23 21:44:39 2019 +0530
Commit:     GitHub
CommitDate: Wed Jan 23 21:44:39 2019 +0530

Correction to merge function

I have corrected the merge function and (i think) it works fine now.
again, I couldnt do mergesort yet

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

commit 23a7fc48800b8d9aff18b5b74db4a20a6632520d
AuthorDate: Wed Jan 23 19:22:32 2019 +0530
Commit:     GitHub
CommitDate: Wed Jan 23 19:22:32 2019 +0530

merge function for the mergesort

I implemented the merge function required for mergesort. I had to change it a little so that the types matched. You will see that i had to transfer x from one vector to the other . I tried to implement mergesort. The code is given as comment. But it doesnt work (I think it is because it cant recognise that (n-s)+s =n )

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

commit a37ff8a84b5910ba896991a3994960d65269ab39