merge1
function that merges two sorted lists such that
the resulting list is sorted in Merge.idr 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.idrEuclList
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.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.Implemented LTEZ
type which is the less than or equal to type for integers. Link here
DecidePositive
,a function that returns whether an integer is positive or not with proof.isLTEZ
function that works just like isLTE for NatZZ.idr
when I was fixing some errors Link herePlusDiv
and MultDiv
for natural numbers which were later changed to integers in Divisors.idr
.Link hereeuclDivide
function total Link hereAdjacentsAreConnected
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 connectedConnectedComponents
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 NatsPathWithProof
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.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
1.The function divideByGcdThenGcdOne
proves that
gcd ( (a/gcd(a,b)),(b/gcd(a,b)) ) =1
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.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 |
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
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 .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.IsNonNegative
, IsNegative
, NotZero
for integers.productOneThenNumbersOne
function proves that if (a*b=1) then either (a=1,b=1) or (a=-1,b=-1)ZZUtils
(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.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.
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(+)