    ------------------------------------------------------------------------
    -- 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