module Control.Algebra.ZZBezoutsIdentity

import Control.Algebra
import Classes.Verified

import Data.ZZ
import Control.Algebra.NumericInstances
import Control.Algebra.ZZVerifiedInstances
import Data.Matrix.AlgebraicVerified 	-- for (ringNeutralIsMultZeroL)

import Control.Algebra.ZZDivisors

import Data.Fin.FinOrdering
import Data.Fin.Structural

import Control.Isomorphism

-- Dependent pattern matching using (do) notation binds improves clarity
import Control.Monad.Identity
import Syntax.PreorderReasoning

import Control.Algebra.DiamondInstances

-- For example
import Data.ZZ.ZZModulo



{-
Table of contents:
* Lemmas for verifying the euclidean algorithm (bezoutsIdentityZZIfModulo)
* (bezoutsIdentityZZIfModulo) implementation
* (Commentary) "Goal: Separation of algorithm from verification."
* The GCD derived from (modZT), itself derived from (modNatT).
-}



{-
Lemmas for verifying the euclidean algorithm (bezoutsIdentityZZIfModulo)
-}



total
bezoutsIdentityLincombEqZZ :
	(a, b, c, d, q, r : ZZ)
	-> q<.>d = c <-> r
	-> b<.>c <+> (a <-> b <.> q)<.>d
		= a<.>d <+> b<.>r
bezoutsIdentityLincombEqZZ a b c d q r pr =
	(
	b<.>c <+> (a <-> b <.> q)<.>d
	) ={
		cong {f=((b<.>c) <+>)}
		$ (
		(a <-> b <.> q)<.>d
		) ={ ringOpIsDistributiveSubR _ _ _ }= (
		a<.>d <-> (b<.>q)<.>d
		) ={
			cong {f=((a<.>d) <->)}
			{- Bracketing style switch -}
			$ ( b<.>q<.>d ) ={ sym $ ringOpIsAssociative b q d }=
			( b<.>(q<.>d) ) ={ cong {f=(b<.>)} pr }=
			( b<.>(c <-> r) ) QED
			}= (
		a<.>d <-> b<.>(c <-> r)
		) ={ abelianGroupOpIsCommutative (a <.> d) _ }= (
		(inverse $ b<.>(c <-> r)) <+> a <.> d
		) QED
		}= (
	b <.> c <+> ( (inverse $ b<.>(c <-> r)) <+> a <.> d )
	) ={ semigroupOpIsAssociative _ _ _ }= (
	b <.> c <-> b<.>(c <-> r) <+> a <.> d
	) ={ abelianGroupOpIsCommutative _ (a <.> d) }= (
	a <.> d <+> ( b <.> c <-> b<.>(c <-> r) )
	) ={
		cong {f=((a <.> d) <+>)}
		$ trans (sym $ ringOpIsDistributiveSubL _ _ _)
		$ cong {f=(b<.>)}
		{- Bracketing style switch -}
		$ ( c <-> (c <-> r) )
			={
				cong {f=(c<+>)}
				$ trans (ringOpIsDistributiveR _ _ _)
				$ cong {f=((inverse c) <+>)}
				$ inverseIsInvolution r
				}=
		( c <+> (inverse c <+> r) )
			={ semigroupOpIsAssociative c (inverse c) r }=
		( (c <-> c) <+> r )
			={ cong {f=(<+> r)} $ groupInverseIsInverseL c }=
		( Algebra.neutral <+> r )
			={ monoidNeutralIsNeutralR _ }=
		( r ) QED
		}= (
	a<.>d <+> b<.>r
	) QED

total
bezoutsIdentityExtQuotientLincombZZ :
	(c, d, q, r, x : ZZ)
	-> (q<.>d <+> r = c)
	-> (d `quotientOverZZ` x)
	-> (r `quotientOverZZ` x)
	-> (c `quotientOverZZ` x)
bezoutsIdentityExtQuotientLincombZZ c d q r x eqpr (dq ** dqPr) (rq ** rqPr)
	= (q<.>dq <+> rq
	** trans (ringOpIsDistributiveR (q<.>dq) rq x)
	$ rewrite rqPr
	in trans ( cong { f= (<+>r) }
		$ trans (sym $ ringOpIsAssociative _ _ _)
		$ cong {f=(q<.>)} $ dqPr )
	$ eqpr)

total
bezQTy : (c, d, a, b : ZZ) -> Type
bezQTy c d a b =
	( c `quotientOverZZ` (a<.>c <+> b<.>d)
	, d `quotientOverZZ` (a<.>c <+> b<.>d) )



{-
(bezoutsIdentityZZIfModulo) implementation

Given a modulo operator giving the remainder in a remainder-division pair,
produce a linear combination of two input integers which divides them both.

Since every number dividing both integers divides every linear combination
of them, this gives the greatest common denominator.

The latter statement isn't proved here, though.
-}



{- (bezoutsIdentityZZIfModulo) parameters -}
parameters (
	{-
	The nonnegative residue of the 1st modulo the subgroup generated by the 2nd.
	Can factor through a modulo on naturals, but must be everywhere defined.
	-}
	modZ : ZZ -> ZZ -> ZZ
	, quotientPartZ : (x, m : ZZ) -> (x <-> modZ x m) `quotientOverZZ` m
	) {

bezoutsIdentityZZIfModulo :
	( c, d : ZZ )
	-> ( zpar : (ZZ, ZZ) ** uncurry (bezQTy c d) zpar )
-- bezoutsIdentityZZIfModulo c (Pos Z) = ( (1, 0) ** ((1 ** _), (0 ** _)) )
bezoutsIdentityZZIfModulo c (Pos Z) = ( (Algebra.unity, Algebra.neutral)
	** rewrite ringWithUnityIsUnityR c
		in rewrite monoidNeutralIsNeutralL c
		in ( (Algebra.unity ** ringWithUnityIsUnityR c)
			, (Algebra.neutral ** ringNeutralIsMultZeroL c) ) )
bezoutsIdentityZZIfModulo c d with (bezoutsIdentityZZIfModulo d (c `modZ` d))
	| ((a,b) ** oldpr) = runIdentity $ do {
			(q ** qIsDivD) <- Id $ c `quotientPartZ` d
			((a' ** divsPrA), (b' ** divsPrB)) <- Id $ oldpr
			-- reverifyDivZ across the bind
			let reverifyDivZ' =
				trans (cong {f=(<+> (c `modZ` d))} qIsDivD)
				$ groupSubtractionIsRDivision c $ c `modZ` d
			-- the goal linear combo of c & d gives d `gcd` (c `modZ` d)
			let lincombEq = bezoutsIdentityLincombEqZZ
				a b c d q (c `modZ` d)
				$ groupDivisionAddLToSubR
					(q <.> d) (c `modZ` d) c
					$ reverifyDivZ'
			-- d `gcd` (c `modZ` d) | c
			let extQuotientLincombZZ = bezoutsIdentityExtQuotientLincombZZ
				c d q (c `modZ` d) ( a<.>d <+> b<.>(c `modZ` d) )
				reverifyDivZ'
				(a' ** divsPrA)
				(b' ** divsPrB)
			return $ ( (b, a <-> b <.> q)
				** ((getWitness extQuotientLincombZZ
					** trans (cong lincombEq)
					$ getProof extQuotientLincombZZ)
				, (a' ** trans (cong lincombEq) divsPrA)) )
		}

} {- (bezoutsIdentityZZIfModulo) parameters -}



{-
Goal: Separation of algorithm from verification.
Obstructions: (Problem 1), (Problem 2).

divZ : ZZ -> ZZ -> ZZ
divZ a b = getWitness $ quotientPartZ a b

reverifyDivZ : divZ a b <.> b <+> modZ a b = a
reverifyDivZ {a} {b}
	= trans (cong {f=(<+> (a `modZ` b))}
		$ getProof $ quotientPartZ a b)
	$ groupSubtractionIsRDivision a $ a `modZ` b

||| Greatest Common Denominator (GCD) linear combination factors
euclideanAlgPar : ZZ -> ZZ -> (ZZ, ZZ)
euclideanAlgPar c (Pos Z) = (1, 0)
euclideanAlgPar c d = (b, a <-> b <.> q)
	where
		eucParReduced : (ZZ, ZZ)
		eucParReduced = euclideanAlgPar d (c `modZ` d)
		a : ZZ
		a = fst eucParReduced
		b : ZZ
		b = snd eucParReduced
		q : ZZ
		q = c `divZ` d

||| Greatest Common Denominator (GCD)
euclideanAlg : ZZ -> ZZ -> ZZ
euclideanAlg c d = let (a, b) = euclideanAlgPar c d in a<.>c <+> b<.>d

bezoutsIdentity : (c, d : ZZ) -> uncurry (bezQTy c d) $ euclideanAlgPar c d

---
Problem 1)
rewrite did not change type uncurry (bezQTy c (Pos 0)) (euclideanAlgPar c (Pos 0))
---

bezoutsIdentity c (Pos Z)
	= rewrite ringWithUnityIsUnityR c
	in rewrite monoidNeutralIsNeutralL c
	in ( (Algebra.unity ** ringWithUnityIsUnityR c)
		, (Algebra.neutral ** ringNeutralIsMultZeroL c) )

---
Problem 2)
Proof must be repeated for positive and negative halves,
since otherwise the case can't be determined to not be the one for 2nd argument 0.
---

bezoutsIdentity c d@(Pos $ S d') = ?bezoutsIdentity_rhs_2
bezoutsIdentity c d@(NegS d') = ?bezoutsIdentity_rhs_3

-}



{-
The GCD derived from (modZT), itself derived from (modNatT).
-}



bezoutZT :
	( c, d : ZZ )
	-> ( zpar : (ZZ, ZZ) ** uncurry (bezQTy c d) zpar )
bezoutZT = bezoutsIdentityZZIfModulo modZT quotientPartModZT
