\import Algebra.Monoid
\import Algebra.Ordered
\import Algebra.Ring.Solver
\import Algebra.Semiring
\import Arith.Nat
\import Data.Array
\import Data.Bool
\import Function.Meta
\import Logic
\import Logic.Meta
\import Order.LinearOrder
\import Order.PartialOrder
\import Order.StrictOrder
\import Paths

\data Operation | Less | LessOrEquals | Equals

\class LinearData \extends AlgData {
  \override R : LinearlyOrderedSemiring

  \func Equation => \Sigma (RingTerm C V) Operation (RingTerm C V)

  \func interpretEq (e : Equation) : \Prop \elim e
    | (t1, Less, t2) => interpret t1 < interpret t2
    | (t1, LessOrEquals, t2) => interpret t1 <= interpret t2
    | (t1, Equals, t2) => interpret t1 = interpret t2

  \lemma interpretEq_<= (e : Equation) (h : interpretEq e) : interpret e. <= interpret e. \elim e
    | (t1, Less, t2) => LinearOrder.<_<= h
    | (t1, LessOrEquals, t2) => h
    | (t1, Equals, t2) => Preorder.=_<= h

  \func Problem => Array Equation

  \func isConst (t : RingTerm C V) : Bool \elim t
    | coef c => true
    | var v => false
    | :zro => true
    | :ide => true
    | :negative t => isConst t
    | t :+ t1 => isConst t and isConst t1
    | t :* t1 => isConst t and isConst t1

  \func Cert (n : Nat) => Array Nat n

  \func certSum (l : Array (RingTerm C V)) (c : Cert l.len)
    => R.BigSum (\lam j => R.natCoef (c j) * interpret (l j))

  \func cert-toTerm (l : Array (RingTerm C V)) (c : Cert l.len) : RingTerm C V \elim l, c
    | nil, nil => :zro
    | t :: l, k :: c => coef (natCoef k) :* t :+ cert-toTerm l c

  \func interpretCert (l : Array (RingTerm C V)) (c : Cert l.len)
    => interpretNF (normalize (cert-toTerm l c))

  \lemma cert-toRingTerm-correct (l : Array (RingTerm C V)) (c : Cert l.len) : AlgData.interpret (cert-toTerm l c) = certSum l c \elim l, c
    | nil, nil => idp
    | t :: l, k :: c => pmap2 (+) (pmap (`* _) alg.func-natCoef) (cert-toRingTerm-correct l c)

  \lemma interpretCert_certSum (l : Array (RingTerm C V)) {c : Cert l.len} : interpretCert l c = certSum l c
    => inv (normalize-consistent (cert-toTerm l c)) *> cert-toRingTerm-correct l c

  \func isLess (o : Operation) : Bool
    | Less => true
    | _ => false
    \where
      \lemma correct {o : Operation} (p : isLess o = true) : o = Less \elim o
        | Less => idp
        | LessOrEquals => \case p
        | Equals => \case p

  \func isSuc (n : Nat) : Bool
    | suc _ => true
    |  => false
    \where
      \lemma correct {n : Nat} (p : isSuc n = true) :  < n \elim n
        |  => \case p
        | suc n => NatSemiring.zero<suc

  \func hasNegative (p : Problem) (c : Cert p.len) : Bool \elim p, c
    | nil, nil => false
    | e :: p, k :: c => isLess e. and isSuc k or hasNegative p c

  \func hasNegative-correct (p : Problem) (c : Cert p.len) (q : hasNegative p c = true) : ∃ (j : Fin p.len) ( < c j) ((p j). = Less) \elim p, c
    | nil, nil => \case q
    | e :: p, k :: c => \case or.toOr q \with {
      | byLeft s => inP (, isSuc.correct (and.toSigma s)., isLess.correct (and.toSigma s).)
      | byRight q' => \have (inP t) => hasNegative-correct p c q'
                      \in inP (suc t., t., t.)
    }

  \func CorrectCert (p : Problem) => \Sigma (c : Cert p.len) (f : Nat) (interpretCert (map __. p) c = interpretCert (:ide :: map __. p) (f :: c)) (hasNegative p c or isSuc f = true)

  \lemma certToLeq (p : Problem) (c : CorrectCert p) : certSum (map __. p) c. <= certSum (map __. p) c.
    => transport2 (<=) zro-left (inv aux) $ <=_+ (transport (`<= _) ide-right $ <=_*_positive-left natCoef>=0 (LinearOrder.<_<= zro<ide)) <=-refl
    \where \lemma aux => inv (interpretCert_certSum (map __. p)) *> c. *> interpretCert_certSum (:ide :: map __. p) {c. :: c.}

  \lemma certToLess (p : Problem) (c : CorrectCert p) (q : isSuc c. = true) : certSum (map __. p) c. < certSum (map __. p) c.
    => transport2 (<) zro-left (inv $ certToLeq.aux p c) $ <=_+-right (transport (`< _) ide-right $ <_*_positive-left (natCoef>0 (isSuc.correct q)) zro<ide) <=-refl

  \lemma solveContrProblem (p : Problem) (c : CorrectCert p) (h : DArray (\lam j => interpretEq (p j))) : Empty
    => \case or.toOr c. \with {
      | byLeft q => certToLeq p c (aux p c. (hasNegative-correct p c. q) h)
      | byRight q => <-irreflexive $ <-transitive-left (certToLess p c q) (aux_<= p c. h)
    }
    \where {
      \lemma aux_<= (p : Problem) (c : Cert p.len) (h : ∀ (e : p) (interpretEq e))
        : certSum (map __. p) c <= certSum (map __. p) c \elim p, c
        | nil, nil => <=-refl
        | e :: p, k :: c => <=_+ (<=_*_positive-right natCoef>=0 (interpretEq_<= e (h ))) (aux_<= p c (\lam j => h (suc j)))

      \lemma aux (p : Problem) (c : Cert p.len) (cc : ∃ (j : Fin p.len) ( < c j) ((p j). = Less)) (h : ∀ (e : p) (interpretEq e))
        : certSum (map __. p) c < certSum (map __. p) c \elim p, c, cc
        | nil, nil, inP ((),_,_)
        | e :: p, k :: c, inP (, k>0, p0=less) => <=_+-right (<_*_positive-right (transport (`< _) natCoefZero $ OrderedSemiring.natCoef_< k>0) (transport (\lam r => interpretEq (e.,r,e.)) p0=less (h ))) (aux_<= p c (\lam j => h (suc j)))
        | e :: p, k :: c, inP (suc j, cj>0, pj=less) => <=_+-left (<=_*_positive-right natCoef>=0 (interpretEq_<= e (h ))) (aux p c (inP (j, cj>0, pj=less)) (\lam j => h (suc j)))
    }

  \lemma solve<=Problem (p : Problem) (t1 t2 : RingTerm C V) (c : CorrectCert (toContr p t1 t2))
                        (h : DArray (\lam j => interpretEq (p j))) : interpret t1 <= interpret t2
    => \lam e => solveContrProblem (toContr p t1 t2) c (e :: h)
    \where
      \func toContr (p : Problem) (t1 t2 : RingTerm C V) : Problem
        => (t2,Less,t1) :: p

  \lemma solve=Problem (p : Problem) (t1 t2 : RingTerm C V) (c1 : CorrectCert (toContr1 p t1 t2)) (c2 : CorrectCert (toContr2 p t1 t2))
                       (h : DArray (\lam j => interpretEq (p j))) : interpret t1 = interpret t2
    => <-connectedness (\lam e => solveContrProblem (toContr1 p t1 t2) c1 (e :: h))
                       (\lam e => solveContrProblem (toContr2 p t1 t2) c2 (e :: h))
    \where {
      \func toContr1 (p : Problem) (t1 t2 : RingTerm C V) : Problem
        => (t1,Less,t2) :: p

      \func toContr2 (p : Problem) (t1 t2 : RingTerm C V) : Problem
        => (t2,Less,t1) :: p
    }

  \lemma solve<Problem (p : Problem) (t1 t2 : RingTerm C V) (c : CorrectCert (toContr p t1 t2))
                       (h : DArray (\lam j => interpretEq (p j))) : interpret t1 < interpret t2
    => \case <_*-cancel-left (natCoef (c. )) (interpret t1) (interpret t2) (\case or.toOr c. \with {
        | byLeft q => <_+-invert-right (certToLeq (toContr p t1 t2) c) $ solveContrProblem.aux p (\lam j => c. (suc j)) (hasNegative-correct p _ q) h
        | byRight q => <_+-invert-left (certToLess (toContr p t1 t2) c q) (solveContrProblem.aux_<= p (tail c.) h)
      }) \with {
         | byLeft r => r.
         | byRight r => absurd $ <-irreflexive $ <-transitive-left r. natCoef>=0
       }
    \where
      \func toContr (p : Problem) (t1 t2 : RingTerm C V) : Problem => (t2,LessOrEquals,t1) :: p
} \where \open LinearlyOrderedSemiring

\class LinearSemiringData \extends LinearData, SemiringData

\class LinearRingData \extends LinearData, RingData {
  \override R : OrderedRing
}

\class LinearRatData \extends LinearData, RatData {
  \override R : OrderedRing
}