Project Report for Logic, Types, Spaces 2019

Shafil Maheenn

Outline of the work done

Report on contributions to Projects in LTS 2019

Merge

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

Bezout’s lemma

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
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

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.
I proved a few theorems about divisibility of integers and about GCD.

ZZ

I had to create many auxiliary functions and data types in ZZ.idr for use in Divisors.idr. Some of these are
Implemented LTEZ type which is the less than or equal to type for integers. Link here
Proved antisymmetry of LTE type for natural numbers and LTEZ type for integers. Link here
Implemented IsPositive data type and DecidePositive ,a function that returns whether an integer is positive or not with proof.
isLTEZ function that works just like isLTE for Nat
And a few other auxiliary functions.
I copied some of Vrunda Rathi’s code into ZZ.idr when I was fixing some errors Link here

gcd.idr

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

Graph.idr

The AdjacentsAreConnected function returns a proof that 2 adjacent vertices are connected by an edge or nothing if they are not connected.
EdgeisPath function proves that adjacent vertices (i.e. vertices that have an edge between them) are connected
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
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.
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.
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

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.
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)
The function, caCoprimeThencDivb proves the theorem that if c ab and gcd (a,c) =1 , then c b
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
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.
gcdIsLinComb function proves that gcd (a,b) is a linear combination of a and b .

decDivZ.idr

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

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

TwoVarDiophEq.idr

(Done in collaboration with Abhishek)

aByd and bByd functions extract the values of a/gcd(a,b) and b/gcd(a,b) respectively from the definition of GCDZ.
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


commit be324c1e5649ad0a683830b611ced1c7855deb1a
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
AuthorDate: Sun Mar 31 09:29:09 2019 +0530
Commit:     GitHub 
CommitDate: Sun Mar 31 09:29:09 2019 +0530

    Corrected a misleading function name
    
    Corrected a misleading function name

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

commit 3e87c1bcc98912ff39fda17f12c684ad58a34485
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
AuthorDate: Mon Mar 11 15:07:41 2019 +0530
Commit:     GitHub 
CommitDate: Mon Mar 11 15:07:41 2019 +0530

    some helper functions about notzero
    
    some helper functions about notzero

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

commit c704d8a0e730623b7c5f028d4ae9a9877f4e1ce8
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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(-)

commit a28383f08769d144e8e2139b056849adbf1e52a1
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
AuthorDate: Sun Mar 10 16:32:05 2019 +0530
Commit:     GitHub 
CommitDate: Sun Mar 10 16:32:05 2019 +0530

    Cancellation laws for addition
    
    Proved cancellation laws for addition
    and some other helper functions

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

commit 54b5b7f61439ce6866114e0eaa452a52b00b25b3
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
AuthorDate: Sat Mar 9 11:00:43 2019 +0530
Commit:     GitHub 
CommitDate: Sat Mar 9 11:00:43 2019 +0530

    Made all functions total
    
    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
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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(+)

commit 236075cbcbdc31cbc2c4bb187a245daad1be43d0
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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(-)

commit 81965bc41a80f71457f3efadc2e1339d6d2de337
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
AuthorDate: Mon Feb 25 23:28:48 2019 +0530
Commit:     GitHub 
CommitDate: Mon Feb 25 23:28:48 2019 +0530

    Added some useful functions
    
    Proved that 0 cannot divide a non zero number
    Also -1 divides anything

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

commit 7040bd71e3ed10410ca039065708650468f41b7b
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
AuthorDate: Sun Feb 24 21:06:19 2019 +0530
Commit:     GitHub 
CommitDate: Sun Feb 24 21:06:19 2019 +0530

    Added some documentation
    
    Added some documentation

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

commit 3cc8b0b75378c9bc8f47fa938bf3cd27e6a12e63
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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(-)

commit c1ba88aaac4886a6d146d2add6150145a0871b7a
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
AuthorDate: Sat Feb 23 22:14:47 2019 +0530
Commit:     GitHub 
CommitDate: Sat Feb 23 22:14:47 2019 +0530

    Added the NonNegative data type
    
    Added the NonNegative data type

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

commit 1e286ac0f776da7d3094a578b966d210eca5ea76
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
AuthorDate: Sat Feb 23 20:47:29 2019 +0530
Commit:     GitHub 
CommitDate: Sat Feb 23 20:47:29 2019 +0530

    Added a subOnBothSides function
    
    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
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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(-)

commit 11b00d349f82cee4c88aad11c258e9979bcb16f3
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
AuthorDate: Tue Feb 19 19:38:15 2019 +0530
Commit:     GitHub 
CommitDate: Tue Feb 19 19:38:15 2019 +0530

    made euclidDivide total
    
    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(-)

commit ad081e2203ec13324df814328449a8b7b655043c
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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(-)

commit 5c6f8308ad7940bd56147edf505cb2431c916c3c
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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(+)

commit cea3972ad09579f374603e6c8c8379ba17e5fda0
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
AuthorDate: Tue Feb 12 23:58:18 2019 +0530
Commit:     GitHub 
CommitDate: Tue Feb 12 23:58:18 2019 +0530

    Added some useful theorems about gcd
    
    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
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
AuthorDate: Tue Feb 12 23:54:44 2019 +0530
Commit:     GitHub 
CommitDate: Tue Feb 12 23:54:44 2019 +0530

    Added some useful functions
    
    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
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
AuthorDate: Tue Feb 12 14:19:39 2019 +0530
Commit:     GitHub 
CommitDate: Tue Feb 12 14:19:39 2019 +0530

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

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

commit f7f05adfce47e5ccb93b231ec000c576f3d217b1
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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(-)

commit 727e4cc269adc852173a28c91fdad5a045cafffa
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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(+)

commit be28efe9bbe3c28da17edadb3d7770034a901178
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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(-)

commit 8b7ad87014481460ee0440b37e9287332b9e2ef3
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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(-)

commit 5c75d0add5fe4527bfffc93ea9bb2a786b32ad6a
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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(+)

commit ad53e8b17293af28066f32bf8a35ef216d5c7f0b
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
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
Author:     shafilmaheenn <46956366+shafilmaheenn@users.noreply.github.com>
AuthorDate: Wed Jan 23 19:12:24 2019 +0530
Commit:     GitHub 
CommitDate: Wed Jan 23 19:12:24 2019 +0530

    The 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 | 33 +++++++++++++++++++++++++++++++++
 1 file changed, 33 insertions(+)

Project Report for Logic, Types, Spaces 2019

Shafil Maheenn

Outline of the work done

Report on contributions to Projects in LTS 2019

Merge

Bezout’s lemma

Divisors

ZZ

gcd.idr

Graph.idr

GCD of integers

Post Midterm

Divisors.idr

GCD of integers GCDZZ.idr

decDivZ.idr

ZZUtils.idr

TwoVarDiophEq.idr

Log of git commits by author

Department of Mathematics, Indian Institute of Science.