{-# OPTIONS --safe #-}
module Cubical.Tactics.CommRingSolver.Solver where

open import Cubical.Foundations.Prelude

open import Cubical.Data.FinData
open import Cubical.Data.Nat using ()
open import Cubical.Data.Nat.Order using (zero-≤)
open import Cubical.Data.Vec.Base
open import Cubical.Algebra.CommRing
open import Cubical.Algebra.Ring
open import Cubical.Tactics.CommRingSolver.RawAlgebra renaming (⟨_⟩ to ⟨_⟩ᵣ)
open import Cubical.Tactics.CommRingSolver.AlgebraExpression
open import Cubical.Tactics.CommRingSolver.IntAsRawRing
open import Cubical.Tactics.CommRingSolver.HornerForms
open import Cubical.Tactics.CommRingSolver.EvalHom
open import Cubical.Tactics.CommRingSolver.HornerEval

private
  variable
     : Level

module EqualityToNormalform (R : CommRing ) where
  νR = CommRing→RawℤAlgebra R
  open CommRingStr (snd R)
  open RingTheory (CommRing→Ring R)
  open Eval ℤAsRawRing νR
  open IteratedHornerOperations νR
  open HomomorphismProperties R

  ℤExpr : (n : )  Type _
  ℤExpr = Expr ℤAsRawRing (fst R)

  normalize : {n : }  ℤExpr n  IteratedHornerForms νR n
  normalize {n = n} (K r) = Constant n νR r
  normalize {n = n} ( k) = Variable n νR k
  normalize (x +' y) =
    (normalize x) +ₕ (normalize y)
  normalize (x ·' y) =
    (normalize x) ·ₕ (normalize y)
  normalize (-' x) =  -ₕ (normalize x)

  isEqualToNormalform :
       {n : } (e : ℤExpr n) (xs : Vec (fst R) n)
      eval (normalize e) xs   e  xs
  isEqualToNormalform (K r) [] = refl
  isEqualToNormalform {n = ℕ.suc n} (K r) (x  xs) =
     eval (Constant (ℕ.suc n) νR r) (x  xs)         ≡⟨ refl 
     eval (0ₕ ·X+ Constant n νR r) (x  xs)           ≡⟨ combineCasesEval R 0ₕ (Constant n νR r) x xs 
     eval 0ₕ (x  xs) · x + eval (Constant n νR r) xs ≡⟨ cong  u  u · x + eval (Constant n νR r) xs)
                                                             (Eval0H (x  xs)) 
     0r · x + eval (Constant n νR r) xs               ≡⟨ cong
                                                           u  u + eval (Constant n νR r) xs)
                                                          (0LeftAnnihilates _) 
     0r + eval (Constant n νR r) xs                   ≡⟨ +IdL _ 
     eval (Constant n νR r) xs                        ≡⟨ isEqualToNormalform (K r) xs 
     _ 

  isEqualToNormalform ( zero) (x  xs) =
    eval (1ₕ ·X+ 0ₕ) (x  xs)           ≡⟨ combineCasesEval R 1ₕ 0ₕ x xs 
    eval 1ₕ (x  xs) · x + eval 0ₕ xs   ≡⟨ cong  u  u · x + eval 0ₕ xs)
                                              (Eval1ₕ (x  xs)) 
    1r · x + eval 0ₕ xs                 ≡⟨ cong  u  1r · x + u ) (Eval0H xs) 
    1r · x + 0r                        ≡⟨ +IdR _ 
    1r · x                             ≡⟨ ·IdL _ 
    x 
  isEqualToNormalform {n = ℕ.suc n} ( (suc k)) (x  xs) =
      eval (0ₕ ·X+ Variable n νR k) (x  xs)           ≡⟨ combineCasesEval R 0ₕ (Variable n νR k) x xs 
      eval 0ₕ (x  xs) · x + eval (Variable n νR k) xs ≡⟨ cong  u  u · x + eval (Variable n νR k) xs)
                                                              (Eval0H (x  xs)) 
      0r · x + eval (Variable n νR k) xs              ≡⟨ cong  u  u + eval (Variable n νR k) xs)
                                                              (0LeftAnnihilates _) 
      0r + eval (Variable n νR k) xs                  ≡⟨ +IdL _ 
      eval (Variable n νR k) xs                       ≡⟨ isEqualToNormalform ( k) xs 
        (suc k)  (x  xs) 

  isEqualToNormalform (-' e) [] =
    eval (-ₕ (normalize e)) []  ≡⟨ -EvalDist (normalize e) [] 
    - eval (normalize e) []    ≡⟨ cong -_ (isEqualToNormalform e [] ) 
    -  e  [] 
  isEqualToNormalform (-' e) (x  xs) =
    eval (-ₕ (normalize e)) (x  xs) ≡⟨ -EvalDist (normalize e) (x  xs) 
    - eval (normalize e) (x  xs)    ≡⟨ cong -_ (isEqualToNormalform e (x  xs) ) 
    -  e  (x  xs) 

  isEqualToNormalform (e +' e₁) [] =
        eval (normalize e +ₕ normalize e₁) []
      ≡⟨ +Homeval (normalize e) _ [] 
        eval (normalize e) []
        + eval (normalize e₁) []
      ≡⟨ cong  u  u + eval (normalize e₁) [])
              (isEqualToNormalform e []) 
         e  []
        + eval (normalize e₁) []
      ≡⟨ cong  u   e  [] + u) (isEqualToNormalform e₁ []) 
         e  [] +  e₁  [] 
  isEqualToNormalform (e +' e₁) (x  xs) =
        eval (normalize e +ₕ normalize e₁) (x  xs)
      ≡⟨ +Homeval (normalize e) _ (x  xs) 
        eval (normalize e) (x  xs) + eval (normalize e₁) (x  xs)
      ≡⟨ cong  u  u + eval (normalize e₁) (x  xs))
              (isEqualToNormalform e (x  xs)) 
         e  (x  xs) + eval (normalize e₁) (x  xs)
      ≡⟨ cong  u   e  (x  xs) + u) (isEqualToNormalform e₁ (x  xs)) 
         e  (x  xs) +  e₁  (x  xs) 

  isEqualToNormalform (e ·' e₁) [] =
        eval (normalize e ·ₕ normalize e₁) []
      ≡⟨ ·Homeval (normalize e) _ [] 
        eval (normalize e) [] · eval (normalize e₁) []
      ≡⟨ cong  u  u · eval (normalize e₁) [])
              (isEqualToNormalform e []) 
         e  [] · eval (normalize e₁) []
      ≡⟨ cong  u   e  [] · u) (isEqualToNormalform e₁ []) 
         e  [] ·  e₁  [] 

  isEqualToNormalform (e ·' e₁) (x  xs) =
        eval (normalize e ·ₕ normalize e₁) (x  xs)
      ≡⟨ ·Homeval (normalize e) _ (x  xs) 
        eval (normalize e) (x  xs) · eval (normalize e₁) (x  xs)
      ≡⟨ cong  u  u · eval (normalize e₁) (x  xs))
              (isEqualToNormalform e (x  xs)) 
         e  (x  xs) · eval (normalize e₁) (x  xs)
      ≡⟨ cong  u   e  (x  xs) · u) (isEqualToNormalform e₁ (x  xs)) 
         e  (x  xs) ·  e₁  (x  xs) 

  solve :
    {n : } (e₁ e₂ : ℤExpr n) (xs : Vec (fst R) n)
    (p : eval (normalize e₁) xs  eval (normalize e₂) xs)
      e₁  xs   e₂  xs
  solve e₁ e₂ xs p =
     e₁  xs                  ≡⟨ sym (isEqualToNormalform e₁ xs) 
    eval (normalize e₁) xs ≡⟨ p 
    eval (normalize e₂) xs ≡⟨ isEqualToNormalform e₂ xs 
     e₂  xs 

ℤExpr : (R : CommRing ) (n : )
         _
ℤExpr R n = EqualityToNormalform.ℤExpr R n

solve : (R : CommRing )
        {n : } (e₁ e₂ : ℤExpr R n) (xs : Vec (fst R) n)
        (p : eval (EqualityToNormalform.normalize R e₁) xs  eval (EqualityToNormalform.normalize R e₂) xs)
         _
solve R = EqualityToNormalform.solve R