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

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

open import Tactic.RingSolver.Core.Polynomial.Parameters

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

open import Data.Nat.Base       as ℕ using (ℕ; suc; zero; compare; _≤′_; ≤′-step; ≤′-refl)
open import Data.Nat.Properties as ℕ using (≤′-trans)
open import Data.Product.Base        using (_,_; _×_; proj₂)
open import Data.List.Base           using (_∷_; [])
open import Data.List.Kleene
open import Data.Vec.Base            using (Vec)
open import Function.Base using (_⟨_⟩_; flip)
open import Relation.Unary

import Relation.Binary.PropositionalEquality.Core as ≡

open Homomorphism homo hiding (_^_)
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.Semantics homo
open import Algebra.Properties.Semiring.Exp.TCOptimised semiring

mutual
  ⊞-hom : ∀ {n} (xs ys : Poly n) →
          ∀ ρ → ⟦ xs ⊞ ys ⟧ ρ ≈ ⟦ xs ⟧ ρ + ⟦ ys ⟧ ρ
  ⊞-hom (xs ⊐ i≤n) (ys ⊐ j≤n) = ⊞-match-hom (inj-compare i≤n j≤n) xs ys

  ⊞-match-hom : ∀ {i j n} {i≤n : i ≤′ n} {j≤n : j ≤′ n}
                (i-cmp-j : InjectionOrdering i≤n j≤n)
                (xs : FlatPoly i) (ys : FlatPoly j) →
                ∀ ρ → ⟦ ⊞-match i-cmp-j xs ys ⟧ ρ ≈ ⟦ xs ⊐ i≤n ⟧ ρ + ⟦ ys ⊐ j≤n ⟧ ρ
  ⊞-match-hom (inj-eq ij≤n) (Κ x) (Κ y) Ρ = +-homo x y
  ⊞-match-hom (inj-eq ij≤n) (⅀ (x Δ i & xs)) (⅀ (y Δ j & ys)) Ρ =
    begin
      ⟦ ⊞-zip (compare i j) x xs y ys ⊐↓ ij≤n ⟧ Ρ
    ≈⟨ ⊐↓-hom (⊞-zip (compare i j) x xs y ys) ij≤n Ρ ⟩
      ⅀?⟦ ⊞-zip (compare i j) x xs y ys ⟧ (drop-1 ij≤n Ρ)
    ≈⟨ ⊞-zip-hom (compare i j) x xs y ys (drop-1 ij≤n Ρ) ⟩
      ⅀⟦ x Δ i & xs ⟧ (drop-1 ij≤n Ρ) + ⅀⟦ y Δ j & ys ⟧ (drop-1 ij≤n Ρ)
    ∎
  ⊞-match-hom (inj-gt i≤n j≤i-1) (⅀ xs) ys Ρ =
    let (ρ , Ρ′) = drop-1 i≤n Ρ
    in
    begin
      ⟦ ⊞-inj j≤i-1 ys xs ⊐↓ i≤n ⟧ Ρ
    ≈⟨ ⊐↓-hom (⊞-inj j≤i-1 ys xs) i≤n Ρ ⟩
      ⅀?⟦ ⊞-inj j≤i-1 ys xs ⟧ (drop-1 i≤n Ρ)
    ≈⟨ ⊞-inj-hom j≤i-1 ys xs ρ Ρ′ ⟩
      ⟦ ys ⊐ j≤i-1 ⟧ (proj₂ (drop-1 i≤n Ρ)) + ⅀⟦ xs ⟧ (drop-1 i≤n Ρ)
    ≈⟨ ≪+ trans-join-hom j≤i-1 i≤n ys Ρ ⟩
      ⟦ ys ⊐ (≤′-step j≤i-1 ⟨ ≤′-trans ⟩ i≤n) ⟧ Ρ + ⅀⟦ xs ⟧ (drop-1 i≤n Ρ)
    ≈⟨ +-comm _ _ ⟩
      ⅀⟦ xs ⟧ (drop-1 i≤n Ρ) + ⟦ ys ⊐ (≤′-step j≤i-1 ⟨ ≤′-trans ⟩ i≤n) ⟧ Ρ
    ∎
  ⊞-match-hom (inj-lt i≤j-1 j≤n) xs (⅀ ys) Ρ =
    let (ρ , Ρ′) = drop-1 j≤n Ρ
    in
    begin
      ⟦ ⊞-inj i≤j-1 xs ys ⊐↓ j≤n ⟧ Ρ
    ≈⟨ ⊐↓-hom (⊞-inj i≤j-1 xs ys) j≤n Ρ ⟩
      ⅀?⟦ ⊞-inj i≤j-1 xs ys ⟧ (drop-1 j≤n Ρ)
    ≈⟨ ⊞-inj-hom i≤j-1 xs ys ρ Ρ′ ⟩
      ⟦ xs ⊐ i≤j-1 ⟧ (proj₂ (drop-1 j≤n Ρ)) + ⅀⟦ ys ⟧ (drop-1 j≤n Ρ)
    ≈⟨ ≪+ trans-join-hom i≤j-1 j≤n xs Ρ ⟩
      ⟦ xs ⊐ (≤′-step i≤j-1 ⟨ ≤′-trans ⟩ j≤n) ⟧ Ρ + ⅀⟦ ys ⟧ (drop-1 j≤n Ρ)
    ∎

  ⊞-inj-hom : ∀ {i k}
            → (i≤k : i ≤′ k)
            → (x : FlatPoly i)
            → (ys : Coeff k +)
            → (ρ : Carrier)
            → (Ρ : Vec Carrier k)
            → ⅀?⟦ ⊞-inj i≤k x ys ⟧ (ρ , Ρ) ≈ ⟦ x ⊐ i≤k ⟧ Ρ + ⅀⟦ ys ⟧ (ρ , Ρ)
  ⊞-inj-hom i≤k xs (y ⊐ j≤k ≠0 Δ 0 & []) ρ Ρ =
    begin
      ⅀?⟦ ⊞-match (inj-compare j≤k i≤k) y xs Δ 0 ∷↓ [] ⟧ (ρ , Ρ)
    ≈⟨ ∷↓-hom-0 ((⊞-match (inj-compare j≤k i≤k) y xs)) [] ρ Ρ ⟩
      ⟦ ⊞-match (inj-compare j≤k i≤k) y xs ⟧ Ρ
    ≈⟨ ⊞-match-hom (inj-compare j≤k i≤k) y xs Ρ ⟩
      (⟦ y ⊐ j≤k ⟧ Ρ + ⟦ xs ⊐ i≤k ⟧ Ρ)
    ≈⟨ +-comm _ _ ⟩
      ⟦ xs ⊐ i≤k ⟧ Ρ + ( ⟦ y ⊐ j≤k ⟧ Ρ)
    ∎
  ⊞-inj-hom i≤k xs (y ⊐ j≤k ≠0 Δ 0 & (∹ ys )) ρ Ρ =
    begin
      ⅀?⟦ ⊞-match (inj-compare j≤k i≤k) y xs Δ 0 ∷↓ (∹ ys ) ⟧ (ρ , Ρ)
    ≈⟨ ∷↓-hom-0 ((⊞-match (inj-compare j≤k i≤k) y xs)) (∹ ys ) ρ Ρ ⟩
      ρ * ⅀⟦ ys ⟧ (ρ , Ρ) + ⟦ ⊞-match (inj-compare j≤k i≤k) y xs ⟧ Ρ
    ≈⟨ +≫ ⊞-match-hom (inj-compare j≤k i≤k) y xs Ρ ⟩
      ρ * ⅀⟦ ys ⟧ (ρ , Ρ) + (⟦ y ⊐ j≤k ⟧ Ρ + ⟦ xs ⊐ i≤k ⟧ Ρ)
    ≈⟨ sym (+-assoc _ _ _) ⟨ trans ⟩ +-comm _ _ ⟩
      ⟦ xs ⊐ i≤k ⟧ Ρ + (ρ * ⅀⟦ ys ⟧ (ρ , Ρ) + ⟦ y ⊐ j≤k ⟧ Ρ)
    ∎
  ⊞-inj-hom i≤k xs (y Δ suc j & ys) ρ Ρ =
    begin
      ⅀?⟦ ⊞-inj i≤k xs (y Δ suc j & ys) ⟧ (ρ , Ρ)
    ≡⟨⟩
      ⅀?⟦ xs ⊐ i≤k Δ 0 ∷↓ (∹ y Δ j & ys ) ⟧ (ρ , Ρ)
    ≈⟨ ∷↓-hom-0 (xs ⊐ i≤k) (∹ y Δ j & ys ) ρ Ρ ⟩
      ρ * ⅀⟦ y Δ j & ys ⟧ (ρ , Ρ) + ⟦ xs ⊐ i≤k ⟧ Ρ
    ≈⟨ +-comm _ _ ⟩
      ⟦ xs ⊐ i≤k ⟧ Ρ + ρ * ⅀⟦ y Δ j & ys ⟧ (ρ , Ρ)
    ≈⟨ +≫ (
        begin
          ρ * ⅀⟦ y Δ j & ys ⟧ (ρ , Ρ)
        ≡⟨⟩
          ρ * (((poly y , ys) ⟦∷⟧ (ρ , Ρ)) *⟨ ρ ⟩^ j)
        ≈⟨ *≫ pow-opt _ ρ j ⟩
          ρ * (ρ ^ j * ((poly y , ys) ⟦∷⟧ (ρ , Ρ)))
        ≈⟨ sym (*-assoc ρ _ _) ⟩
          ρ * ρ ^ j * ((poly y , ys) ⟦∷⟧ (ρ , Ρ))
        ≈⟨ ≪* sym (pow-suc ρ j) ⟩
          ⅀⟦ y Δ suc j & ys ⟧ (ρ , Ρ)
        ∎) ⟩
      ⟦ xs ⊐ i≤k ⟧ Ρ + ⅀⟦ y Δ suc j & ys ⟧ (ρ , Ρ)
    ∎

  ⊞-coeffs-hom : ∀ {n} (xs : Coeff n *) (ys : Coeff n *) →
                 ∀ ρ → ⅀?⟦ ⊞-coeffs xs ys ⟧ ρ ≈ ⅀?⟦ xs ⟧ ρ + ⅀?⟦ ys ⟧ ρ
  ⊞-coeffs-hom [] ys Ρ         = sym (+-identityˡ (⅀?⟦ ys ⟧ Ρ))
  ⊞-coeffs-hom (∹ x Δ i & xs ) = ⊞-zip-r-hom i x xs

  ⊞-zip-hom : ∀ {n i j}
           → (c : ℕ.Ordering i j)
           → (x : NonZero n)
           → (xs : Coeff n *)
           → (y : NonZero n)
           → (ys : Coeff n *)
           → ∀ ρ → ⅀?⟦ ⊞-zip c x xs y ys ⟧ ρ ≈ ⅀⟦ x Δ i & xs ⟧ ρ + ⅀⟦ y Δ j & ys ⟧ ρ
  ⊞-zip-hom (ℕ.equal i) (x ≠0) xs (y ≠0) ys (ρ , Ρ) =
    let x′  = ⟦ x ⟧ Ρ
        y′  = ⟦ y ⟧ Ρ
        xs′ = ⅀?⟦ xs ⟧ (ρ , Ρ)
        ys′ = ⅀?⟦ ys ⟧ (ρ , Ρ)
    in
    begin
      ⅀?⟦ x ⊞ y Δ i ∷↓ ⊞-coeffs xs ys ⟧ (ρ , Ρ)
    ≈⟨ ∷↓-hom (x ⊞ y) i (⊞-coeffs xs ys) ρ Ρ ⟩
      ρ ^ i * (((x ⊞ y) , (⊞-coeffs xs ys)) ⟦∷⟧ (ρ , Ρ))
    ≈⟨ *≫ ⟦∷⟧-hom (x ⊞ y) (⊞-coeffs xs ys) ρ Ρ ⟩
      ρ ^ i * (ρ * ⅀?⟦ ⊞-coeffs xs ys ⟧ (ρ , Ρ) + ⟦ x ⊞ y ⟧ Ρ)
    ≈⟨ *≫ begin
           ρ * ⅀?⟦ ⊞-coeffs xs ys ⟧ (ρ , Ρ) + ⟦ x ⊞ y ⟧ Ρ
          ≈⟨ (*≫ ⊞-coeffs-hom xs ys (ρ , Ρ)) ⟨ +-cong ⟩ ⊞-hom x y Ρ  ⟩
            ρ * (xs′ + ys′) + (x′ + y′)
          ≈⟨ ≪+ distribˡ ρ xs′ ys′ ⟩
            ρ * xs′ + ρ * ys′ + (x′ + y′)
          ≈⟨ +-assoc _ _ _ ⟨ trans ⟩ (+≫ (sym (+-assoc _ _ _) ⟨ trans ⟩ (≪+ +-comm _ _))) ⟩
            ρ * xs′ + (x′ + ρ * ys′ + y′)
          ≈⟨ (+≫ +-assoc _ _ _) ⟨ trans ⟩ sym (+-assoc _ _ _) ⟩
            (ρ * xs′ + x′) + (ρ * ys′ + y′)
          ∎ ⟩
     ρ ^ i * ((ρ * xs′ + x′) + (ρ * ys′ + y′))
    ≈⟨ distribˡ (ρ ^ i) _ _ ⟩
      ρ ^ i * (ρ * xs′ + x′) + ρ ^ i * (ρ * ys′ + y′)
    ≈⟨ sym (pow-opt _ ρ i ⟨ +-cong ⟩ pow-opt _ ρ i) ⟩
      (ρ * xs′ + x′) *⟨ ρ ⟩^ i + (ρ * ys′ + y′) *⟨ ρ ⟩^ i
    ≈⟨ pow-mul-cong (sym (⟦∷⟧-hom x xs ρ Ρ)) ρ i ⟨ +-cong ⟩ pow-mul-cong (sym (⟦∷⟧-hom y ys ρ Ρ)) ρ i ⟩
      ((x , xs) ⟦∷⟧ (ρ , Ρ)) *⟨ ρ ⟩^ i + ((y , ys) ⟦∷⟧ (ρ , Ρ)) *⟨ ρ ⟩^ i
    ∎
  ⊞-zip-hom (ℕ.less i k) x xs y ys (ρ , Ρ) = ⊞-zip-r-step-hom i k y ys x xs (ρ , Ρ) ⊙ +-comm _ _
  ⊞-zip-hom (ℕ.greater j k) = ⊞-zip-r-step-hom j k

  ⊞-zip-r-step-hom : ∀ {n} j k
                  → (x : NonZero n)
                  → (xs : Coeff n *)
                  → (y : NonZero n)
                  → (ys : Coeff n *)
                  → ∀ ρ → ⅀⟦ y Δ j & ⊞-zip-r x k xs ys ⟧ ρ ≈ ⅀⟦ x Δ suc (j ℕ.+ k) & xs ⟧ ρ + ⅀⟦ y Δ j & ys ⟧ ρ
  ⊞-zip-r-step-hom j k x xs y ys (ρ , Ρ) =
    let x′  = ⟦ NonZero.poly x ⟧ Ρ
        y′  = ⟦ NonZero.poly y ⟧ Ρ
        xs′ = ⅀?⟦ xs ⟧ (ρ , Ρ)
        ys′ = ⅀?⟦ ys ⟧ (ρ , Ρ)
    in
    begin
      ((poly y , ⊞-zip-r x k xs ys) ⟦∷⟧ (ρ , Ρ)) *⟨ ρ ⟩^ j
    ≈⟨ pow-mul-cong (⟦∷⟧-hom (poly y) (⊞-zip-r x k xs ys) ρ Ρ) ρ j ⟩
      (ρ * ⅀?⟦ ⊞-zip-r x k xs ys ⟧ (ρ , Ρ) + y′) *⟨ ρ ⟩^ j
    ≈⟨ pow-opt _ ρ j ⟩
      ρ ^ j * (ρ * ⅀?⟦ ⊞-zip-r x k xs ys ⟧ (ρ , Ρ) + y′)
    ≈⟨ *≫ ≪+ *≫ (⊞-zip-r-hom k x xs ys (ρ , Ρ) ⟨ trans ⟩ (≪+ pow-mul-cong (⟦∷⟧-hom (poly x) xs ρ Ρ) ρ k)) ⟩
      ρ ^ j * (ρ * ((ρ * xs′ + x′) *⟨ ρ ⟩^ k + ys′) + y′)
    ≈⟨ *≫ ≪+ distribˡ ρ _ _ ⟩
      ρ ^ j * ((ρ * (ρ * xs′ + x′) *⟨ ρ ⟩^ k + ρ * ys′) + y′)
    ≈⟨ *≫ +-assoc _ _ _ ⟩
      ρ ^ j * (ρ * (ρ * xs′ + x′) *⟨ ρ ⟩^ k + (ρ * ys′ + y′))
    ≈⟨ distribˡ _ _ _ ⟩
      ρ ^ j * (ρ * (ρ * xs′ + x′) *⟨ ρ ⟩^ k) + ρ ^ j * (ρ * ys′ + y′)
    ≈⟨ sym (pow-opt _ ρ j) ⟨ flip +-cong ⟩
         (begin
            ρ ^ j * (ρ * ((ρ * ⅀?⟦ xs ⟧ (ρ , Ρ) + ⟦ poly x ⟧ Ρ) *⟨ ρ ⟩^ k))
          ≈⟨ (sym (*-assoc _ _ _) ⟨ trans ⟩ (≪* sym (pow-sucʳ ρ j))) ⟩
            ρ ^ suc j * ((ρ * ⅀?⟦ xs ⟧ (ρ , Ρ) + ⟦ poly x ⟧ Ρ) *⟨ ρ ⟩^ k)
          ≈⟨ pow-add _ _ k j ⟩
            (ρ * ⅀?⟦ xs ⟧ (ρ , Ρ) + ⟦ poly x ⟧ Ρ) *⟨ ρ ⟩^ (k ℕ.+ suc j)
            ≡⟨ ≡.cong (λ i → (ρ * ⅀?⟦ xs ⟧ (ρ , Ρ) + ⟦ poly x ⟧ Ρ) *⟨ ρ ⟩^ i) (ℕ.+-comm k (suc j)) ⟩
            (ρ * ⅀?⟦ xs ⟧ (ρ , Ρ) + ⟦ poly x ⟧ Ρ) *⟨ ρ ⟩^ (suc j ℕ.+ k)
          ∎)
    ⟩
      (ρ * xs′ + x′) *⟨ ρ ⟩^ suc (j ℕ.+ k) + (ρ * ys′ + y′) *⟨ ρ ⟩^ j
    ≈⟨ pow-mul-cong (sym (⟦∷⟧-hom (poly x) xs ρ Ρ)) ρ (suc (j ℕ.+ k)) ⟨ +-cong ⟩ pow-mul-cong (sym (⟦∷⟧-hom (poly y) ys ρ Ρ)) ρ j ⟩
      ((poly x , xs) ⟦∷⟧ (ρ , Ρ)) *⟨ ρ ⟩^ suc (j ℕ.+ k) + ((poly y , ys) ⟦∷⟧ (ρ , Ρ)) *⟨ ρ ⟩^ j
    ∎

  ⊞-zip-r-hom : ∀ {n} i
             → (x : NonZero n)
             → (xs ys : Coeff n *)
             → (Ρ : Carrier × Vec Carrier n)
             → ⅀?⟦ ⊞-zip-r x i xs ys ⟧ (Ρ) ≈ ⅀⟦ x Δ i & xs ⟧ ( Ρ) + ⅀?⟦ ys ⟧ ( Ρ)
  ⊞-zip-r-hom i x xs []                (ρ , Ρ) = sym (+-identityʳ _)
  ⊞-zip-r-hom i x xs (∹ (y Δ j) & ys )         = ⊞-zip-hom (compare i j) x xs y ys