Merge pull request #3 from siddhartha-gadgil/master

Syncing files

Code/BaseN.idr

@@ -2,6 +2,7 @@ module Basen
 
 import Data.Fin
 
+%access public export
 --Fin to Nat
 tonatFin: (n: Nat) -> Fin(n) -> Nat
 tonatFin (S k) FZ = Z

Code/Bezout.idr

@@ -1,7 +1,9 @@
 module Bezout
-
+import Divisors
+import ZZ
 import Data.Vect
 import Data.Fin
+%access public export
 
 {-Copied from Chinmaya's code. Gives quotient and remainder on divison-}
 {-This just computes the qoutient and the remainder, but it doesn't prove that they indeed satisfy the conditions a = b*q + r and r < b -}
@@ -20,99 +22,145 @@ rem (S k) b = case (lte (S (S k)) b) of
 Let rk = ak*r0 + bk*r1 where r0 and r1 are the original inputs.Correspondingly  rsk = ask*r0 + bsk*r1 where sk = k+1
 Then the I am going to the next step in the Euclid algorithm and changing the coefficients.
 These formulas can be easily derived.-}
-Euclnos: (Int,Int,Int,Int,Int,Int)->(Int,Int,Int,Int,Int,Int)
+Euclnos: (Integer,Integer,Integer,Integer,Integer,Integer)->(Integer,Integer,Integer,Integer,Integer,Integer)
 Euclnos (rk, rsk ,ak ,ask, bk ,bsk) = (rsk,rssk,ask,assk,bsk,bssk) where
   rssk = cast(snd (Eucl (cast rk) (cast rsk)))
   bssk =bk-bsk* (cast(fst (Eucl (cast rk) (cast rsk))))
   assk =ak-ask* (cast(fst (Eucl (cast rk) (cast rsk))))
 {-Does the Euclnos repeatedy until the remainder is zero. Then the previous remainder is the GCD.-}
-Bezouttuple: (Int,Int,Int,Int,Int,Int)->(Int,Int,Int,Int,Int,Int)
+Bezouttuple: (Integer,Integer,Integer,Integer,Integer,Integer)->(Integer,Integer,Integer,Integer,Integer,Integer)
 Bezouttuple (rk, rsk ,ak ,ask, bk, bsk) = case rsk of
                                         0 => (rk, rsk, ak, ask, bk, bsk)
                                         _ => (Bezouttuple (Euclnos (rk ,rsk, ak ,ask ,bk ,bsk)))
-{-Returns 2 particular integers out of a 6 tuple-}
-returnab: (Int,Int,Int,Int,Int,Int)->(Int,Int)
-returnab (a ,b ,c ,d, e ,f)  = (c,e)
+{-Returns 2 particular Integers out of a 6 tuple-}
+returnab: (Integer,Integer,Integer,Integer,Integer,Integer)->(ZZ,ZZ)
+returnab (a ,b ,c ,d, e ,f)  = (cast c,cast e)
 {-Returns the Bezout coefficients-}
-Bezout : Nat ->Nat ->(Int, Int)
+Bezout : Nat ->Nat ->(ZZ,ZZ)
 Bezout k j =  (returnab(Bezouttuple((cast k) , (cast j),1, 0 ,0 ,1)))
 
+|||Same as Euclnos wxcept that it stores the quotient and remainder in a list
+MEuclnos:((Integer,Integer,Integer,Integer,Integer,Integer),(List (Integer,Integer)))->((Integer,Integer,Integer,Integer,Integer,Integer),(List (Integer,Integer)))
+MEuclnos ((rk, rsk ,ak ,ask, bk ,bsk),xs) = ((Euclnos (rk, rsk ,ak ,ask, bk ,bsk)),((q,r)::xs)) where
+  q = (cast(fst (Eucl (cast rk) (cast rsk))))
+  r = (cast(snd (Eucl(cast rk) (cast rsk))))
+|||Same as Bezouttuple except that it stores the quotient and remainder in a list
+MBezout:((Integer,Integer,Integer,Integer,Integer,Integer),(List (Integer,Integer)))->((Integer,Integer,Integer,Integer,Integer,Integer),(List (Integer,Integer)))
+MBezout ((rk, rsk ,ak ,ask, bk ,bsk),xs) = case rsk of
+                                                0 =>  ((rk, rsk ,ak ,ask, bk ,bsk),xs)
+                                                _ =>MBezout (MEuclnos ((rk, rsk ,ak ,ask, bk ,bsk),xs))
+
+|||Gives a list of quotients and remainders in Euclid's Algorithm
+EuclList:(a:Nat)->(b:Nat)->List (Integer,Integer)
+EuclList a b = (snd (MBezout (((cast a)  ,(cast b), 1,0,0,1),[])))
+
+gcd2 : Nat -> Nat -> ZZ
+gcd2 a b = ( (((cast a)*(snd (Bezout a b))) + ((cast b)*(fst (Bezout a b)))))
+
+
+
+
+
 {-}
 just the functions to compute the GCD in two different ways.
 {-}
+{-
+gcd2 : Nat -> Nat -> ZZ
+gcd2 a b = ( (((cast a)*(snd (Bezout a b))) + ((cast b)*(fst (Bezout a b)))))
 
-gcd2 : Nat -> Nat -> Nat
-gcd2 a b = (cast (((cast a)*(snd (Bezout a b))) + ((cast b)*(fst (Bezout a b)))))
 
 gcdab : Nat -> Nat -> Nat
 gcdab b Z = b
 gcdab a b = gcdab b (snd (Eucl a b))
 
 {-}
-given below are the auxilary functions to the proof that given a and b, there exist q and r such that a = b*q + r.
-The algorithm above just computes these two numbers, but it doesn't prove that (a = b*q + r and r < b)
 
-f1 is the proof that a + 1 = b*q + (r + 1) given that a = b*q + r
 
-aux1f2 is the proof that given a + 1 <= b, a <= b
-aux2f2 is the proof that given a and b, either a <= b or a >= b + 1
+{-proof of existence of remainders and quotients is necessary to define the concept of divisibilty -}
+{-The next step ahead might be to proof the uniqueness of these remainders and quotients probably -}
+
+-- defining divisibilty as b | a if there exists q such that a = b*q + Z
+-- if b | a and c | b, then c | a.
+-- if c | a and c | b, then c | (a + b)
 
-aux1f3 is the proof that given a <= b and b <= a, a = b
-aux2f3 proves that a = b + c and c = d together imply a = b + d
-aux3f3 is the proof that given a = b*c + b, a = b*(c + 1) + 0
+-- auxplusDiv 1 to 4 are just auxilary proofs.
+auxtransDiv : (a : Nat) -> (b : Nat) -> (c : Nat) -> (d : Nat) -> (b = c*q)
+auxtransDiv a b c d = ?auxtransDiv_rhs
 
-All these proofs (except maybe aux2f3) were necessary to avoid various type mismatch errors.
-{-}
+auxplusDiv1 : (a : Nat) -> (b : Nat) -> (c : Nat) -> (d : Nat) -> (a = b) -> (c = d) -> (a + c = b + d)
+auxplusDiv1 b b d d Refl Refl = Refl
 
-apNat2 : (a : Nat) -> (b : Nat) -> (a = b) -> (S a = S b)
-apNat2 a a Refl = Refl
-
-aux1f2 : (a : Nat) -> (b : Nat) -> (LTE (S a) b) -> (LTE a b)
-aux1f2 Z Z LTEZero impossible
-aux1f2 Z Z (LTESucc _) impossible
-aux1f2 Z (S k) x = LTEZero
-aux1f2 (S a) (S k) (LTESucc x) = (LTESucc (aux1f2 a k x))
-
-aux2f2 : (a : Nat) -> (b : Nat) -> (Either (LTE a b) (LTE (S b) a))
-aux2f2 Z Z  = Left LTEZero
-aux2f2 Z (S b) = Left LTEZero
-aux2f2 (S k) Z = Right (LTESucc LTEZero)
-aux2f2 (S k) (S b) = step where
-                  step = case (aux2f2 k b) of
-                    (Left l) => (Left (LTESucc l))
-                    (Right r) => (Right (LTESucc r))
-
-f1 : (a : Nat) -> (b : Nat) -> (c : Nat) -> (a = b + c) -> ((S a) = b + (S c))
-f1 a c k pf = (trans (apNat2 a (c + k) pf) (plusSuccRightSucc c k))
-
-aux1f3 : (a : Nat) -> (b : Nat) -> (LTE a b) -> (LTE b a) -> (a = b)
-aux1f3 Z Z LTEZero LTEZero = Refl
-aux1f3 Z (S _) LTEZero LTEZero impossible
-aux1f3 Z (S _) LTEZero (LTESucc _) impossible
-aux1f3 (S _) Z LTEZero LTEZero impossible
-aux1f3 (S _) Z (LTESucc _) LTEZero impossible
-aux1f3 (S k) (S j) (LTESucc x) (LTESucc y) = (apNat2 k j (aux1f3 k j x y))
-
-aux2f3 : (a : Nat) -> (b : Nat) -> (c : Nat) -> (d : Nat) -> (a = b + c) -> (c = d) -> (a = b + d)
-aux2f3 a b Z Z prf Refl = prf
-aux2f3 _ _ Z (S _) _ Refl impossible
-aux2f3 _ _ (S _) Z _ Refl impossible
-aux2f3 (b + (S j)) b (S j) (S j) Refl Refl = Refl
-
-
-aux3f3 : (a : Nat) -> (b : Nat) -> (c : Nat) -> (a = (b*c) + b) -> (a = b*(S c) + Z)
-aux3f3 a b k prf = (trans (trans (trans (prf) (plusCommutative (b*k) b)) (sym (multRightSuccPlus b k))) (sym (plusZeroRightNeutral (b*(S k)))))
-
-{-Caveat : the function elemproof hasn't been programmed for the divisor b being equal to zero -}
-{-replacig b with (S b) everywhere in the proof has been done to avoid the case b = 0-}
-
-elemproof1 : (a : Nat) -> (b : Nat) -> (x : (Nat, Nat) ** ((a = (b*(fst x)) + (snd x)) , (LTE (S (snd x)) b)))
-elemproof1 Z (S b) = ((0,0) ** ((sym (trans (trans (plusCommutative ((S b)*Z) Z) (sym (multLeftSuccPlus (S b) Z))) (multZeroRightZero (S (S b))))), (LTESucc LTEZero)))
-elemproof1 (S k) (S b) = step where
-                     step = case (elemproof1 k (S b)) of
-                       ((q,r) ** (pf , pff)) => case (aux2f2 (S (S r)) (S b)) of
-                                                  Left l => ((q , (S r)) ** ((f1 k ((S b)*q) r pf) , l))
-                                                  Right (LTESucc ri) => (((S q) , Z) ** ((aux3f3 (S k) (S b) q (aux2f3 (S k) ((S b)*q) (S r) (S b) (f1 k ((S b)*q) r pf) (aux1f3 (S r) (S b) pff ri))) , (LTESucc LTEZero)))
+auxplusDiv2 : (a : Nat) -> (b : Nat) -> (c : Nat) -> (q : Nat) -> (p : Nat) -> (a = c*q) -> (b = c*p) -> (a + b = c*(q + p))
+auxplusDiv2 a b c q p pf1 pf2 = (trans (auxplusDiv1 a (c*q) b (c*p) pf1 pf2) (sym(multDistributesOverPlusRight c q p)))
 
-{-proof of existence of remainders and quotients is necessary to define the concept of divisibilty -}
-{-The next step ahead might be to proof the uniqueness of these remainders and quotients probably -}
+auxplusDiv3 : (a : Nat) -> (b : Nat) -> (c : Nat) -> (d : Nat) -> (a = c) -> (b = d) -> ((minus a b) = (minus c d))
+auxplusDiv3 c d c d Refl Refl = Refl
+
+-- Holes !!
+auxplusDiv4 : (a : Nat) -> (b : Nat) -> (c : Nat) -> (q : Nat) -> (p : Nat) -> (a + b = c*q) -> (b = c*p) -> (a = c*(minus q p))
+auxplusDiv4 a b c q p pf1 pf2 = ?auxplusDiv3_rhs
+
+--These statements are the two main facts we might be Integererested in.
+plusDiv1 : (a : Nat) -> (b : Nat) -> (c : Nat) -> (q : Nat ** a = c*q) -> (p : Nat ** b = c*p) -> (f : Nat ** a + b = c*f)
+plusDiv1 a b c (q ** pf1) (p ** pf2) = ((q + p) ** (auxplusDiv2 a b c q p pf1 pf2))
+
+plusDiv2 : (a : Nat) -> (b : Nat) -> (c : Nat) -> (q : Nat ** a + b = c*q) -> (p : Nat ** b = c*p) -> (f : Nat ** a = c*f)
+plusDiv2 a b c (q ** pf1) (p ** pf2) = ((minus q p) ** (auxplusDiv4 a b c q p pf1 pf2))
+
+
+-- I'll try and prove some (possibly useful) facts about the gcd.
+-- weak definition of the gcd : d | a, d | b and if c | a and c | b, then c <= d.
+--This is the common Factor Type
+
+isCommonFactor : Nat -> Nat -> Nat -> Type
+isCommonFactor a b c = ((q : Nat ** a = c*q),(p : Nat ** b = c*p))
+
+--This is the GCD type
+-- d is "a" gcd of a and b if isGCD a b d type is inhabited.
+-- Uniqueness of GCD not assumed !!
+-- the gcd is just assumed to be bigger than any other common divisor, not a multiple of it.
+
+isGCD : Nat -> Nat -> Nat -> Type
+isGCD a b d = ((isCommonFactor a b d) , ((c : Nat) -> (isCommonFactor a b c) -> (LTE c d)))
+
+-- try to prove that if d is "a" gcd of (a,b) then it is "a" gcd of (a+b,a)
+
+gcdfact1 : (a : Nat) -> (b : Nat) -> (d : Nat) -> (isGCD a b d) -> (isCommonFactor (a + b) b d)
+gcdfact1 a b d (((q ** pf1),(p ** pf2)),f) = ((plusDiv1 a b d (q ** pf1) (p ** pf2)),(p ** pf2))
+
+gcdfact2 : (a : Nat) -> (b : Nat) -> (d : Nat) -> (isGCD a b d) -> (c : Nat) -> (isCommonFactor (a + b) b c) -> (LTE c d)
+gcdfact2 a b d (pf , f) c ((q ** pf1),(p ** pf2)) = (f c ((plusDiv2 a b c (q ** pf1) (p ** pf2)),(p ** pf2)))
+
+maingcdfact1 : (a : Nat) -> (b : Nat) -> (d : Nat) -> (isGCD a b d) -> (isGCD (a + b) b d)
+maingcdfact1 a b d pf = ((gcdfact1 a b d pf),(gcdfact2 a b d pf))
+
+-- now the proof that if d is "a" gcd of (a+b,b), then it is "a" gcd of (a,b)
+
+gcdfact3 : (a : Nat) -> (b : Nat) -> (d : Nat) -> (isGCD (a + b) b d) -> (isCommonFactor a b d)
+gcdfact3 a b d (((q ** pf1),(p ** pf2)),f) = ((plusDiv2 a b d (q ** pf1) (p ** pf2)),(p ** pf2))
+
+gcdfact4 : (a : Nat) -> (b : Nat) -> (d : Nat) -> (isGCD (a + b) b d) -> (c : Nat) -> (isCommonFactor a b c) -> (LTE c d)
+gcdfact4 a b d (pf, f) c ((q ** pf1),(p ** pf2)) = (f c ((plusDiv1 a b c (q ** pf1) (p ** pf2)),(p ** pf2)))
+
+maingcdFact2 : (a : Nat) -> (b : Nat) -> (d : Nat) -> (isGCD (a + b) b d) -> (isGCD a b d)
+maingcdFact2 a b d pf = ((gcdfact3 a b d pf),(gcdfact4 a b d pf))
+
+-- now the proof that if d is "a" gcd of (a,b), it is also "a" gcd of (b,a)
+
+symCommonFactor : (a : Nat) -> (b : Nat) -> (c : Nat) -> (isCommonFactor a b c) -> (isCommonFactor b a c)
+symCommonFactor a b c ((p ** pf1),(q ** pf2)) = ((q ** pf2),(p ** pf1))
+
+symGCD1 : (a : Nat) -> (b : Nat) -> (d : Nat) -> (isGCD a b d) -> ((c : Nat) -> (isCommonFactor b a c) -> (LTE c d))
+symGCD1 a b d (pf, f) = g where
+                          g c ((p ** pf1),(q ** pf2)) = f c ((q ** pf2),(p ** pf1))
+
+symGCD : (a : Nat) -> (b : Nat) -> (d : Nat) -> (isGCD a b d) -> (isGCD b a d)
+symGCD a b d (pf , f) = ((symCommonFactor a b d pf) , (symGCD1 a b d (pf , f)))
+
+-- I'll list the types and functions that might be useful
+-- The GCD type : isGCD : Nat -> Nat -> Nat -> Type
+--                isGCD a b d = ((isCommonFactor a b d) , ((c : Nat) -> (isCommonFactor a b c) -> (LTE c d)))
+-- maingcdfact1 , maingcdfact2 , symGCD.
+
+-- The next step might be to show that the natural number that the euclidian algorithm gives us is indeed a gcd
+-- also uniqueness of gcd.

Code/Divisors.idr

@@ -0,0 +1,104 @@
+module Divisors
+
+import ZZ
+%access public export
+%default total
+|||isDivisible a b can be constucted if b divides a
+isDivisible : ZZ -> ZZ -> Type
+isDivisible a b = (n : ZZ ** a = b * n)
+
+
+|||1 divides everything
+oneDiv : (a : ZZ) -> isDivisible a 1
+oneDiv a = (a ** rewrite sym (multOneLeftNeutralZ a) in Refl)
+
+|||Genetes a proof of (a+b) = d*(n+m) from (a=d*n)and (b=d*m)
+DistributeProof: (a:ZZ)->(b:ZZ)->(d:ZZ)->
+  (n:ZZ)->(m:ZZ)->(a=d*n)->(b=d*m)->((a+b) = d*(n+m))
+DistributeProof a b d n m pf1 pf2 =
+  rewrite  (multDistributesOverPlusRightZ d n m) in
+    (trans (the (a+b=(d*n)+b) (v1)) v2) where
+      v1 =plusConstantRightZ a (d*n) b pf1
+      v2 =plusConstantLeftZ b (d*m) (d*n) pf2
+
+|||The theorem d|a =>d|ac
+MultDiv:(isDivisible a d) ->(c:ZZ)->(isDivisible (a*c) d)
+MultDiv {d} (n**Refl) c =
+  ((n*c)** (rewrite sym (multAssociativeZ d n c) in (Refl)))
+
+|||The theorem d|a and d|b =>d|(a+b)
+PlusDiv : (isDivisible a d)->(isDivisible b d)->(isDivisible (a+b) d)
+PlusDiv {d}{a}{b} (n**prf1) (m**prf2) =
+  ((n+m)**(DistributeProof a b d n m prf1 prf2))
+|||The theorem b|a and c|b =>c|a
+TransDivide : (isDivisible a b)->(isDivisible b c)->(isDivisible a c)
+TransDivide {c} (x ** pf1) (y ** pf2) =
+  (y*x ** (rewrite  multAssociativeZ c y x in  (rewrite pf1 in (rewrite pf2 in Refl))))
+
+
+|||If d divides a and b it divides a linear combination of a and b
+LinCombDiv:(m:ZZ)->(n:ZZ)->(isDivisible a d)->(isDivisible b d)->(isDivisible ((a*m)+(b*n)) d)
+LinCombDiv m n dDiva dDivb =
+  PlusDiv (MultDiv  dDiva m) (MultDiv  dDivb n)
+
+
+EuclidConservesDivisor:(m:ZZ)->(isDivisible a d)->(isDivisible b d)->
+  (isDivisible (a+(b*(-m))) d)
+EuclidConservesDivisor m dDiva dDivb = PlusDiv dDiva (MultDiv dDivb (-m) )
+
+|||Any integer divides zero
+ZZDividesZero:(a:ZZ)->(isDivisible 0 a )
+ZZDividesZero a = (0**(sym (multZeroRightZeroZ a)))
+|||A type that is occupied iff c is a common factor of a and b
+isCommonFactorZ : (a:ZZ) -> (b:ZZ) -> (c:ZZ) -> Type
+isCommonFactorZ a b c = ((isDivisible a c),(isDivisible b c))
+|||The GCD type that is occupied iff d = gcd (a,b).
+||| Here GCD is defined as that positive integer such that any common factor
+||| of a and b divides it
+GCDZ : (a:ZZ) -> (b:ZZ) -> (d:ZZ) -> Type
+GCDZ a b d = ((IsPositive d),(isCommonFactorZ a b d),
+  ({c:ZZ}->(isCommonFactorZ a b c)->(isDivisible d c)))
+|||Anything divides itself
+SelfDivide:(a:ZZ)->(isDivisible a a)
+SelfDivide a = (1**sym (multOneRightNeutralZ a))
+
+|||Generates the proof that if c is a common factor of a and 0 then c divides a
+GCDCondition : (a:ZZ) -> ({c:ZZ}->(isCommonFactorZ a 0 c)->(isDivisible a c))
+GCDCondition  a {c} (cDiva,cDiv0) = cDiva
+|||Proves that the GCD of a and 0 is a
+gcdOfZeroAndInteger:(a:ZZ)->IsPositive a ->GCDZ a 0 a
+gcdOfZeroAndInteger a pf =
+  (pf,((SelfDivide a),(ZZDividesZero a)),((GCDCondition a)))
+|||The theorem, d|a =>d|(-a)
+dDividesNegative:(isDivisible a d)->(isDivisible  (-a) d)
+dDividesNegative{a}{d} (x ** pf) =
+  ((-x)**(multNegateRightIsNegateZ a d x pf))
+|||The theorem c|b and c|(a+bp) then c|a
+cDiva :{p:ZZ} ->(cDIvb :(isDivisible b c))->
+  (cDIvExp:isDivisible (a+(b*p)) c)->(isDivisible a c)
+cDiva {p}{b}{a}{c} cDivb cDivExp =
+  rewrite (sym (addAndSubNeutralZ a (b*p))) in (
+    PlusDiv cDivExp (dDividesNegative(MultDiv cDivb (p))))
+|||A helper function for euclidConservesGcd function
+genFunctionForGcd :(f:({c:ZZ}->(isCommonFactorZ a b c)->(isDivisible d c)))->
+  (({c:ZZ}->(isCommonFactorZ b (a+(b*(-m)))  c)->(isDivisible d c)))
+genFunctionForGcd f (cDivb,cDivExp) =
+  f((cDiva cDivb cDivExp,cDivb))
+
+|||The theorem, gcd(a,b)=d => gcd (b, a+ b(-m))=d
+euclidConservesGcd :(m:ZZ)->(GCDZ a b d)->(GCDZ b  (a+(b*(-m))) d)
+euclidConservesGcd m  (posProof, (dDiva,dDivb), f) =
+  (posProof,(dDivb,(EuclidConservesDivisor m  dDiva dDivb)),genFunctionForGcd f)
+|||The theorem that if c and d are positive d|c => (d is less than or equal to c)
+posDivPosImpliesLte:(isDivisible c d)->(IsPositive c)->
+  (IsPositive d)->LTEZ d c
+posDivPosImpliesLte {d}{c}(x ** pf) cPos dPos =
+  posLteMultPosPosEqZ {q=x} d c dPos cPos pf
+
+
+|||The Theorem that if c and d are positive, d|c and c|d =>(c=d)
+PosDivAndDivByImpliesEqual: (isDivisible c d)->(isDivisible d c)->(IsPositive c)
+  ->(IsPositive d) -> (c=d)
+PosDivAndDivByImpliesEqual x y z x1 =lteAndGteImpliesEqualZ dLtec cLted where
+  dLtec =posDivPosImpliesLte x z x1
+  cLted =posDivPosImpliesLte y x1 z

Code/Field.idr

@@ -0,0 +1,30 @@
+module Field
+
+import Group
+import Monoid
+import Ring
+
+%access public export
+
+
+-- For field, proof that multiplicative inverse exists when only non zero elements are considered
+total
+InvExistsNonZero : (fld : Type) -> ((+) : fld -> fld -> fld) -> ((*) : fld -> fld -> fld) -> (IsGroup fld (+)) -> Type
+InvExistsNonZero fld (+) (*) pfgrp = (a : fld) -> (pfid : (IdentityExists fld (*)) ** ((a = fst(fst(snd(pfgrp)))) -> Void) -> (a_inv : fld ** ((a*a_inv) = fst(pfid) , (a_inv*a) = fst(pfid))))
+
+
+-- multiplication has associativity, identity, but inverse only for non-zero elements
+total
+IsModGrp : (fld : Type) -> ((+) : fld -> fld -> fld) -> ((*) : fld -> fld -> fld) -> (pfgrp : IsGroup fld (+)) -> Type
+IsModGrp fld (+) (*) pfgrp = (Associative fld (*), (IdentityExists fld (*), InvExistsNonZero fld (+) (*) pfgrp))
+
+
+-- modified abelian property added to the above proof
+IsModAbelGrp : (fld : Type) -> ((+) : fld -> fld -> fld) -> ((*) : fld -> fld -> fld) -> (pfgrp : IsGroup fld (+)) -> Type
+IsModAbelGrp fld (+) (*) pfgrp = (IsModGrp fld (+) (*) pfgrp, Commutative fld (*))
+
+
+-- similar to Arka's file on monoids
+total
+IsField : (fld : Type) -> ((+) : fld -> fld -> fld) -> ((*) : fld -> fld -> fld) -> Type
+IsField fld (+) (*) = (pfgrp: IsAbelianGrp fld (+) ** ((IsModAbelGrp fld (+) (*) (fst pfgrp)), IsDistributive fld (+) (*)))