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

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

    open import Tactic.RingSolver.Core.Polynomial.Parameters

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

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

    open Homomorphism homo hiding (_^_)

    open import Tactic.RingSolver.Core.Polynomial.Homomorphism.Lemmas homo
    open import Tactic.RingSolver.Core.Polynomial.Homomorphism.Addition 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.Definitions.RawSemiring rawSemiring
      using () renaming (_^′_ to _^_)

    reassoc : ∀ {y} x z → x * (y * z) ≈ y * (x * z)
    reassoc {y} x z = sym (*-assoc x y z) ⟨ trans ⟩ ((≪* *-comm x y) ⟨ trans ⟩ *-assoc y x z)

    mutual
      ⊠-step′-hom : ∀ {n} → (a : Acc _<′_ n) → (xs ys : Poly n) → ∀ ρ → ⟦ ⊠-step′ a xs ys ⟧ ρ ≈ ⟦ xs ⟧ ρ * ⟦ ys ⟧ ρ
      ⊠-step′-hom a (x ⊐ p) = ⊠-step-hom a x p

      ⊠-step-hom : ∀ {i n}
                 → (a : Acc _<′_ n)
                 → (xs : FlatPoly i)
                 → (i≤n : i ≤′ n)
                 → (ys : Poly n)
                 → ∀ ρ → ⟦ ⊠-step a xs i≤n ys ⟧ ρ ≈ ⟦ xs ⊐ i≤n ⟧ ρ * ⟦ ys ⟧ ρ
      ⊠-step-hom a (Κ x) i≤n = ⊠-Κ-hom a x
      ⊠-step-hom a (⅀ xs) i≤n = ⊠-⅀-hom a xs i≤n

      ⊠-Κ-hom : ∀ {n}
              → (a : Acc _<′_ n)
              → ∀ x
              → (ys : Poly n)
              → ∀ ρ
              → ⟦ ⊠-Κ a x ys ⟧ ρ ≈ ⟦ x ⟧ᵣ * ⟦ ys ⟧ ρ
      ⊠-Κ-hom (acc _)  x (Κ y  ⊐ i≤n) ρ = *-homo x y
      ⊠-Κ-hom (acc wf) x (⅀ xs ⊐ i≤n) ρ =
        begin
          ⟦ ⊠-Κ-inj (wf i≤n) x xs ⊐↓ i≤n ⟧ ρ
        ≈⟨ ⊐↓-hom (⊠-Κ-inj (wf i≤n) x xs) i≤n ρ ⟩
          ⅀?⟦ ⊠-Κ-inj (wf i≤n) x xs ⟧ (drop-1 i≤n ρ)
        ≈⟨ ⊠-Κ-inj-hom (wf i≤n) x xs (drop-1 i≤n ρ) ⟩
          ⟦ x ⟧ᵣ * ⅀⟦ xs ⟧ (drop-1 i≤n ρ)
        ∎

      ⊠-Κ-inj-hom : ∀ {n}
                  → (a : Acc _<′_ n)
                  → (x : Raw.Carrier)
                  → (xs : Coeff n +)
                  → ∀ ρ
                  → ⅀?⟦ ⊠-Κ-inj a x xs ⟧ ρ ≈ ⟦ x ⟧ᵣ * ⅀⟦ xs ⟧ ρ
      ⊠-Κ-inj-hom {n} a x xs (ρ , Ρ) =
        poly-mapR
          ρ
          Ρ
          (⊠-Κ a x)
          (⟦ x ⟧ᵣ *_)
          (*-cong refl)
          reassoc
          (distribˡ ⟦ x ⟧ᵣ)
          (λ ys → ⊠-Κ-hom a x ys Ρ)
          (zeroʳ _)
          xs

      ⊠-⅀-hom : ∀ {i n}
              → (a : Acc _<′_ n)
              → (xs : Coeff i +)
              → (i<n : i <′ n)
              → (ys : Poly n)
              → ∀ ρ
              → ⟦ ⊠-⅀ a xs i<n ys ⟧ ρ ≈ ⅀⟦ xs ⟧ (drop-1 i<n ρ) * ⟦ ys ⟧ ρ
      ⊠-⅀-hom (acc wf) xs i<n (⅀ ys ⊐ j≤n) = ⊠-match-hom (acc wf) (inj-compare i<n j≤n) xs ys
      ⊠-⅀-hom (acc wf) xs i<n (Κ y  ⊐ _) ρ =
        begin
          ⟦ ⊠-Κ-inj (wf i<n) y xs ⊐↓ i<n ⟧ ρ
        ≈⟨ ⊐↓-hom (⊠-Κ-inj (wf i<n) y xs) i<n ρ ⟩
          ⅀?⟦ ⊠-Κ-inj (wf i<n) y xs ⟧ (drop-1 i<n ρ)
        ≈⟨ ⊠-Κ-inj-hom (wf i<n) y xs (drop-1 i<n ρ) ⟩
          ⟦ y ⟧ᵣ * ⅀⟦ xs ⟧ (drop-1 i<n ρ)
        ≈⟨ *-comm _ _ ⟩
          ⅀⟦ xs ⟧ (drop-1 i<n ρ) * ⟦ y ⟧ᵣ
        ∎

      ⊠-⅀-inj-hom : ∀ {i k}
                  → (a : Acc _<′_ k)
                  → (i<k : i <′ k)
                  → (xs : Coeff i +)
                  → (ys : Poly k)
                  → ∀ ρ
                  → ⟦ ⊠-⅀-inj a i<k xs ys ⟧ ρ ≈ ⅀⟦ xs ⟧ (drop-1 i<k ρ) * ⟦ ys ⟧ ρ
      ⊠-⅀-inj-hom (acc wf) i<k x (⅀ ys ⊐ j≤k) = ⊠-match-hom (acc wf) (inj-compare i<k j≤k) x ys
      ⊠-⅀-inj-hom (acc wf) i<k x (Κ y ⊐ j≤k) ρ =
        begin
          ⟦ ⊠-Κ-inj (wf i<k) y x ⊐↓ i<k ⟧ ρ
        ≈⟨ ⊐↓-hom (⊠-Κ-inj (wf i<k) y x) i<k ρ ⟩
          ⅀?⟦ ⊠-Κ-inj (wf i<k) y x ⟧ (drop-1 i<k ρ)
        ≈⟨ ⊠-Κ-inj-hom (wf i<k) y x (drop-1 i<k ρ) ⟩
          ⟦ y ⟧ᵣ * ⅀⟦ x ⟧ (drop-1 i<k ρ)
        ≈⟨ *-comm _ _ ⟩
          ⅀⟦ x ⟧ (drop-1 i<k ρ) * ⟦ y ⟧ᵣ
        ∎

      ⊠-match-hom : ∀ {i j n}
                  → (a : Acc _<′_ n)
                  → {i<n : i <′ n}
                  → {j<n : j <′ n}
                  → (ord : InjectionOrdering i<n j<n)
                  → (xs : Coeff i +)
                  → (ys : Coeff j +)
                  → (Ρ : Vec Carrier n)
                  → ⟦ ⊠-match a ord xs ys ⟧ Ρ
                  ≈ ⅀⟦ xs ⟧ (drop-1 i<n Ρ) * ⅀⟦ ys ⟧ (drop-1 j<n Ρ)
      ⊠-match-hom {j = j} (acc wf) (inj-lt i≤j-1 j≤n) xs ys Ρ′ =
        let (ρ , Ρ) = drop-1 j≤n Ρ′
            xs′ = ⅀⟦ xs ⟧ (drop-1 (≤′-trans (≤′-step i≤j-1) j≤n) Ρ′)
        in
        begin
          ⟦ poly-map ( (⊠-⅀-inj (wf j≤n) i≤j-1 xs)) ys ⊐↓ j≤n ⟧ Ρ′
        ≈⟨ ⊐↓-hom (poly-map ( (⊠-⅀-inj (wf j≤n) i≤j-1 xs)) ys) j≤n Ρ′ ⟩
          ⅀?⟦ poly-map ( (⊠-⅀-inj (wf j≤n) i≤j-1 xs)) ys ⟧ (ρ , Ρ)
        ≈⟨ poly-mapR ρ Ρ (⊠-⅀-inj (wf j≤n) i≤j-1 xs)
                         (_ *_)
                         (*-cong refl)
                         reassoc
                         (distribˡ _)
                         (λ y → ⊠-⅀-inj-hom (wf j≤n) i≤j-1 xs y _)
                         (zeroʳ _) ys ⟩
           ⅀⟦ xs ⟧ (drop-1 i≤j-1 Ρ) * ⅀⟦ ys ⟧ (ρ , Ρ)
        ≈⟨ ≪* trans-join-coeffs-hom i≤j-1 j≤n xs Ρ′ ⟩
          xs′ * ⅀⟦ ys ⟧ (ρ , Ρ)
        ∎
      ⊠-match-hom (acc wf) (inj-gt i≤n j≤i-1) xs ys Ρ′ =
        let (ρ , Ρ) = drop-1 i≤n Ρ′
            ys′ = ⅀⟦ ys ⟧ (drop-1 (≤′-step j≤i-1 ⟨ ≤′-trans ⟩ i≤n) Ρ′)
        in
        begin
          ⟦ poly-map ( (⊠-⅀-inj (wf i≤n) j≤i-1 ys)) xs ⊐↓ i≤n ⟧ Ρ′
        ≈⟨ ⊐↓-hom (poly-map ( (⊠-⅀-inj (wf i≤n) j≤i-1 ys)) xs) i≤n Ρ′ ⟩
          ⅀?⟦ poly-map ( (⊠-⅀-inj (wf i≤n) j≤i-1 ys)) xs ⟧ (ρ , Ρ)
        ≈⟨ poly-mapR ρ Ρ (⊠-⅀-inj (wf i≤n) j≤i-1 ys)
                         (_ *_)
                         (*-cong refl)
                         reassoc
                         (distribˡ _)
                         (λ x → ⊠-⅀-inj-hom (wf i≤n) j≤i-1 ys x _)
                         (zeroʳ _) xs ⟩
          ⅀⟦ ys ⟧ (drop-1 j≤i-1 Ρ) * ⅀⟦ xs ⟧ (ρ , Ρ)
        ≈⟨ ≪* trans-join-coeffs-hom j≤i-1 i≤n ys Ρ′ ⟩
          ys′ * ⅀⟦ xs ⟧ (ρ , Ρ)
        ≈⟨ *-comm ys′ _ ⟩
          ⅀⟦ xs ⟧ (ρ , Ρ) * ys′
        ∎
      ⊠-match-hom (acc wf) (inj-eq ij≤n) xs ys Ρ =
        begin
          ⟦ ⊠-coeffs (wf ij≤n) xs ys ⊐↓ ij≤n ⟧ Ρ
        ≈⟨ ⊐↓-hom (⊠-coeffs (wf ij≤n) xs ys) ij≤n Ρ ⟩
          ⅀?⟦ ⊠-coeffs (wf ij≤n) xs ys ⟧ (drop-1 ij≤n Ρ)
        ≈⟨ ⊠-coeffs-hom (wf ij≤n) xs ys (drop-1 ij≤n Ρ) ⟩
          ⅀⟦ xs ⟧ (drop-1 ij≤n Ρ) * ⅀⟦ ys ⟧ (drop-1 ij≤n Ρ)
        ∎

      ⊠-coeffs-hom : ∀ {n}
                   → (a : Acc _<′_ n)
                   → (xs ys : Coeff n +)
                   → ∀ ρ → ⅀?⟦ ⊠-coeffs a xs ys ⟧ ρ ≈ ⅀⟦ xs ⟧ ρ * ⅀⟦ ys ⟧ ρ
      ⊠-coeffs-hom a xs (y ≠0 Δ j & []) (ρ , Ρ) =
        begin
          ⅀?⟦ poly-map (⊠-step′ a y) xs ⍓* j ⟧ (ρ , Ρ)
        ≈⟨ sym (pow′-hom j (poly-map (⊠-step′ a y) xs) ρ Ρ) ⟩
          ⅀?⟦ poly-map (⊠-step′ a y) xs ⟧ (ρ , Ρ) *⟨ ρ ⟩^ j
        ≈⟨ pow-mul-cong (poly-mapR ρ Ρ (⊠-step′ a y) (⟦ y ⟧ Ρ *_) (*-cong refl) reassoc (distribˡ _) (λ z → ⊠-step′-hom a y z Ρ) (zeroʳ _) xs) ρ j ⟩
          (⟦ y ⟧ Ρ * ⅀⟦ xs ⟧ (ρ , Ρ)) *⟨ ρ ⟩^ j
        ≈⟨ pow-opt _ ρ j ⟩
          (ρ ^ j) * (⟦ y ⟧ Ρ * ⅀⟦ xs ⟧ (ρ , Ρ))
        ≈⟨ sym (*-assoc _ _ _) ⟩
          (ρ ^ j) * ⟦ y ⟧ Ρ * ⅀⟦ xs ⟧ (ρ , Ρ)
        ≈⟨ *-comm _ _ ⟩
          ⅀⟦ xs ⟧ (ρ , Ρ) * ((ρ ^ j) * ⟦ y ⟧ Ρ)
        ≈⟨ *≫ sym (pow-opt _ ρ j) ⟩
          ⅀⟦ xs ⟧ (ρ , Ρ) * (⟦ y ⟧ Ρ *⟨ ρ ⟩^ j)
        ∎
      ⊠-coeffs-hom a xs (y ≠0 Δ j & ∹ ys) (ρ , Ρ) =
        let xs′ = ⅀⟦ xs ⟧ (ρ , Ρ)
            y′  = ⟦ y ⟧ Ρ
            ys′ = ⅀⟦ ys ⟧ (ρ , Ρ)
        in
        begin
          ⅀?⟦ para (⊠-cons a y ys) xs ⍓* j ⟧ (ρ , Ρ)
        ≈⟨ sym (pow′-hom j (para (⊠-cons a y ys) xs) ρ Ρ) ⟨ trans ⟩ pow-opt _ ρ j ⟩
          ρ ^ j * ⅀?⟦ para (⊠-cons a y ys) xs ⟧ (ρ , Ρ)
        ≈⟨ *≫ ⊠-cons-hom a y ys xs ρ Ρ ⟩
         ρ ^ j * (xs′ * (ρ * ys′ + y′))
        ≈⟨ sym (*-assoc _ _ _) ⟨ trans ⟩ (≪* *-comm _ _) ⟨ trans ⟩ *-assoc _ _ _ ⟨ trans ⟩ (*≫ sym (pow-opt _ ρ j))⟩
          xs′ * ((ρ * ys′ + y′) *⟨ ρ ⟩^ j)
        ∎

      ⊠-cons-hom : ∀ {n}
                 → (a : Acc _<′_ n)
                 → (y : Poly n)
                 → (ys xs : Coeff n +)
                 → (ρ : Carrier)
                 → (Ρ : Vec Carrier n)
                 → ⅀?⟦ para (⊠-cons a y ys) xs ⟧ (ρ , Ρ)
                 ≈ ⅀⟦ xs ⟧ (ρ , Ρ) * (ρ * ⅀⟦ ys ⟧ (ρ , Ρ) + ⟦ y ⟧ Ρ)
      -- ⊠-cons-hom a y [] xs ρ Ρ = {!!}
      ⊠-cons-hom a y ys xs ρ Ρ = poly-foldR ρ Ρ (⊠-cons a y ys) (flip _*_ (ρ * ⅀⟦ ys ⟧ (ρ , Ρ) + ⟦ y ⟧ Ρ)) (flip *-cong refl) (λ x y → sym (*-assoc x y _)) step (zeroˡ _) xs
        where
        step = λ { (z ⊐ j≤n) {ys₁} zs ys≋zs →
          let x′  = ⟦ z ⊐ j≤n ⟧ Ρ
              xs′ = ⅀?⟦ zs ⟧ (ρ , Ρ)
              y′  = ⟦ y ⟧ Ρ
              ys′ = ⅀⟦ ys ⟧ (ρ , Ρ)
              step = λ y → ⊠-step-hom a z j≤n y Ρ
          in
          begin
            ρ * ⅀?⟦ ⊞-coeffs (poly-map ( (⊠-step a z j≤n)) ys) ys₁ ⟧ (ρ , Ρ) + ⟦ ⊠-step a z j≤n y ⟧ Ρ
          ≈⟨ (*≫ ⊞-coeffs-hom (poly-map (⊠-step a z j≤n) ys) _ (ρ , Ρ)) ⟨ +-cong ⟩ ⊠-step-hom a z j≤n y Ρ ⟩
            ρ * (⅀?⟦ poly-map (⊠-step a z j≤n) ys ⟧ (ρ , Ρ) + ⅀?⟦ ys₁ ⟧ (ρ , Ρ)) + x′ * y′
          ≈⟨ ≪+ *≫ (poly-mapR ρ Ρ (⊠-step a z j≤n) (x′ *_) (*-cong refl) reassoc (distribˡ _) step (zeroʳ _) ys ⟨ +-cong ⟩ ys≋zs) ⟩
            ρ * (x′ * ys′ + xs′ * (ρ * ys′ + y′)) + (x′ * y′)
          ≈⟨ ≪+ distribˡ _ _ _ ⟩
            ρ * (x′ * ys′) + ρ * (xs′ * (ρ * ys′ + y′)) + (x′ * y′)
          ≈⟨ (≪+ +-comm _ _) ⟨ trans ⟩ +-assoc _ _ _ ⟩
            ρ * (xs′ * (ρ * ys′ + y′)) + (ρ * (x′ * ys′) + (x′ * y′))
          ≈⟨ sym (*-assoc _ _ _) ⟨ +-cong ⟩ ((≪+ (sym (*-assoc _ _ _) ⟨ trans ⟩ (≪* *-comm _ _) ⟨ trans ⟩ *-assoc _ _ _)) ⟨ trans ⟩ sym (distribˡ _ _ _)) ⟩
            ρ * xs′ * (ρ * ys′ + y′) + x′ * (ρ * ys′ + y′)
          ≈⟨ sym (distribʳ _ _ _) ⟩
            (ρ * xs′ + x′) * (ρ * ys′ + y′)
          ∎ }

    ⊠-hom : ∀ {n} (xs ys : Poly n) →
            ∀ ρ → ⟦ xs ⊠ ys ⟧ ρ ≈ ⟦ xs ⟧ ρ * ⟦ ys ⟧ ρ
    ⊠-hom (xs ⊐ i≤n) = ⊠-step-hom (<′-wellFounded _) xs i≤n