------------------------------------------------------------------------
-- The Agda standard library
--
-- Homomorphism proofs for exponentiation over polynomials
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

open import Tactic.RingSolver.Core.Polynomial.Parameters

module Tactic.RingSolver.Core.Polynomial.Homomorphism.Exponentiation
  {r₁ r₂ r₃ r₄}
  (homo : Homomorphism r₁ r₂ r₃ r₄)
  where

open import Function.Base using (_⟨_⟩_)

open import Data.Nat.Base as  using (; suc; zero; compare)
open import Data.Product.Base  using (_,_; _×_; proj₁; proj₂)
open import Data.List.Kleene
open import Data.Vec.Base      using (Vec)

import Data.Nat.Properties as 
import Relation.Binary.PropositionalEquality.Core as 

open Homomorphism homo
open import Tactic.RingSolver.Core.Polynomial.Homomorphism.Lemmas homo
open import Tactic.RingSolver.Core.Polynomial.Base from
open import Tactic.RingSolver.Core.Polynomial.Reasoning to
open import Tactic.RingSolver.Core.Polynomial.Homomorphism.Multiplication homo
open import Tactic.RingSolver.Core.Polynomial.Semantics homo

import Algebra.Properties.CommutativeSemiring.Exp.TCOptimised commutativeSemiring as RawPow
import Algebra.Definitions.RawSemiring (RawCoeff.rawSemiring from) as CoPow

pow-eval-hom :  x i   x CoPow.^′ suc i ⟧ᵣ   x ⟧ᵣ RawPow.^ suc i
pow-eval-hom x zero    = refl
pow-eval-hom x (suc i) = (*-homo _ x)  trans  (≪* pow-eval-hom x i)

⊡-mult-hom :  {n} i (xs : Poly n) ρ   ⊡-mult i xs  ρ   xs  ρ RawPow.^ suc i
⊡-mult-hom zero    xs ρ = refl
⊡-mult-hom (suc i) xs ρ =  ⊠-hom (⊡-mult i xs) xs ρ  trans  (≪* ⊡-mult-hom i xs ρ)

⊡-+1-hom :  {n}  (xs : Poly n)  (i : )   ρ   xs  i +1  ρ   xs  ρ RawPow.^ suc i
⊡-+1-hom (Κ x   i≤n)           i ρ = pow-eval-hom x i
⊡-+1-hom xs@( (_ &  _)  i≤n) i ρ = ⊡-mult-hom i xs ρ
⊡-+1-hom ( (x ≠0 Δ j & [])  i≤n) i ρ =
  begin
     x  i +1 Δ (j ℕ.+ i ℕ.* j) ∷↓ [] ⊐↓ i≤n  ρ
  ≈⟨ ⊐↓-hom (x  i +1 Δ (j ℕ.+ i ℕ.* j) ∷↓ []) i≤n ρ 
    ⅀?⟦ x  i +1 Δ (j ℕ.+ i ℕ.* j) ∷↓ []  (drop-1 i≤n ρ)
  ≈⟨ ∷↓-hom (x  i +1) (j ℕ.+ i ℕ.* j) [] ρ′ Ρ 
    (ρ′ RawPow.^ (j ℕ.+ i ℕ.* j)) * ( x  i +1  Ρ)
  ≈⟨ *≫ (( ⊡-+1-hom x i Ρ) ) 
    (ρ′ RawPow.^ (j ℕ.+ i ℕ.* j)) * ( x  Ρ RawPow.^ suc i)
  ≈⟨ rearrange j 
    ((  x  Ρ) *⟨ ρ′ ⟩^ j) RawPow.^ suc i
  
  where
  ρ′,Ρ = drop-1 i≤n ρ
  ρ′ = proj₁ ρ′,Ρ
  Ρ = proj₂ ρ′,Ρ
  rearrange :  j  (ρ′ RawPow.^ (j ℕ.+ i ℕ.* j)) * ( x  Ρ RawPow.^ suc i) ((  x  Ρ) *⟨ ρ′ ⟩^ j) RawPow.^ suc i
  rearrange zero =
    begin
      (ρ′ RawPow.^ (i ℕ.* 0)) * ( x  Ρ RawPow.^ suc i)
    ≡⟨ ≡.cong  k   (ρ′ RawPow.^ k) * ( x  Ρ RawPow.^ suc i)) (ℕ.*-zeroʳ i) 
      1# * ( x  Ρ RawPow.^ suc i)
    ≈⟨ *-identityˡ _ 
       x  Ρ RawPow.^ suc i
    
  rearrange j@(suc j′) =
    begin
      (ρ′ RawPow.^ (suc i ℕ.* j))           * ( x  Ρ RawPow.^ suc i)
    ≡⟨ ≡.cong  v  (ρ′ RawPow.^ v) * ( x  Ρ RawPow.^ suc i)) (ℕ.*-comm (suc i) j) 
      (ρ′ RawPow.^ (j ℕ.* suc i))           * ( x  Ρ RawPow.^ suc i)
    ≈⟨ ≪* sym (RawPow.^-assocʳ ρ′ j (suc i)) 
      ((ρ′ RawPow.^ suc j′) RawPow.^ suc i) * ( x  Ρ RawPow.^ suc i)
    ≈⟨ sym (RawPow.^-distrib-* _ ( x  Ρ) (suc i)) 
      ((ρ′ RawPow.^ suc j′) *  x  Ρ) RawPow.^ suc i
    

⊡-hom :  {n}  (xs : Poly n)  (i : )   ρ   xs  i  ρ   xs  ρ RawPow.^ i
⊡-hom xs 0       ρ = 1-homo
⊡-hom xs (suc i) ρ = ⊡-+1-hom xs i ρ