{-# OPTIONS --cubical-compatible --safe #-}
open import Tactic.RingSolver.Core.Polynomial.Parameters
module Tactic.RingSolver.Core.Polynomial.Homomorphism.Lemmas
{r₁ r₂ r₃ r₄}
(homo : Homomorphism r₁ r₂ r₃ r₄)
where
open import Data.Bool using (Bool;true;false)
open import Data.Nat.Base as ℕ using (ℕ; suc; zero; compare; _≤′_; ≤′-step; ≤′-refl)
open import Data.Nat.Properties as ℕ using (≤′-trans)
open import Data.Vec.Base as Vec using (Vec; _∷_)
open import Data.Fin using (Fin; zero; suc)
open import Data.List.Base using (_∷_; [])
open import Data.Unit using (tt)
open import Data.List.Kleene
open import Data.Product.Base using (_,_; proj₁; proj₂; map₁; _×_)
open import Data.Maybe using (nothing; just)
open import Function.Base using (_⟨_⟩_)
open import Level using (lift)
open import Relation.Nullary using (Dec; yes; no)
open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
open Homomorphism homo hiding (_^_)
open import Tactic.RingSolver.Core.Polynomial.Reasoning to
open import Tactic.RingSolver.Core.Polynomial.Base from
open import Tactic.RingSolver.Core.Polynomial.Semantics homo
open import Algebra.Properties.Semiring.Exp.TCOptimised semiring
pow-opt : ∀ x ρ i → x *⟨ ρ ⟩^ i ≈ ρ ^ i * x
pow-opt x ρ zero = sym (*-identityˡ x)
pow-opt x ρ (suc i) = refl
pow-add : ∀ x y i j → y ^ (suc j) * x *⟨ y ⟩^ i ≈ x *⟨ y ⟩^ (i ℕ.+ suc j)
pow-add x y zero j = refl
pow-add x y (suc i) j = go x y i j
where
go : ∀ x y i j → (y ^ suc j) * ((y ^ suc i) * x) ≈ y ^ suc (i ℕ.+ suc j) * x
go x y zero j = sym (*-assoc _ _ _)
go x y (suc i) j = begin
(y ^ suc j) * (y ^ (suc i) * y * x) ≈⟨ *≫ *-assoc _ y x ⟩
(y ^ suc j) * (y ^ (suc i) * (y * x)) ≈⟨ go (y * x) y i j ⟩
y ^ suc (i ℕ.+ suc j) * (y * x) ≈⟨ sym (*-assoc _ y x) ⟩
y ^ suc (suc i ℕ.+ suc j) * x ∎
pow-hom : ∀ {n} i
→ (xs : Coeff n +)
→ ∀ ρ ρs
→ ⅀⟦ xs ⟧ (ρ , ρs) *⟨ ρ ⟩^ i ≈ ⅀⟦ xs ⍓+ i ⟧ (ρ , ρs)
pow-hom zero (x Δ j & xs) ρ ρs rewrite ℕ.+-identityʳ j = refl
pow-hom (suc i) (x ≠0 Δ j & xs) ρ ρs =
begin
ρ ^ (suc i) * (((x , xs) ⟦∷⟧ (ρ , ρs)) *⟨ ρ ⟩^ j)
≈⟨ pow-add _ ρ j i ⟩
(((x , xs) ⟦∷⟧ (ρ , ρs)) *⟨ ρ ⟩^ (j ℕ.+ suc i))
∎
pow-mul-cong : ∀ {x y} → x ≈ y → ∀ ρ i → x *⟨ ρ ⟩^ i ≈ y *⟨ ρ ⟩^ i
pow-mul-cong x≈y ρ zero = x≈y
pow-mul-cong x≈y ρ (suc i) = *≫ x≈y
zero-hom : ∀ {n} (p : Poly n) → Zero p → (ρs : Vec Carrier n) → 0# ≈ ⟦ p ⟧ ρs
zero-hom (Κ x ⊐ i≤n) p≡0 ρs = Zero-C⟶Zero-R x p≡0
pow-suc : ∀ x i → x ^ suc i ≈ x * x ^ i
pow-suc x zero = sym (*-identityʳ _)
pow-suc x (suc i) = *-comm _ _
pow-sucʳ : ∀ x i → x ^ suc i ≈ x ^ i * x
pow-sucʳ x zero = sym (*-identityˡ _)
pow-sucʳ x (suc i) = refl
⅀?⟦_⟧ : ∀ {n} (xs : Coeff n *) → Carrier × Vec Carrier n → Carrier
⅀?⟦ [] ⟧ _ = 0#
⅀?⟦ ∹ x ⟧ = ⅀⟦ x ⟧
_⟦∷⟧?_ : ∀ {n} (x : Poly n × Coeff n *) → Carrier × Vec Carrier n → Carrier
(x , xs) ⟦∷⟧? (ρ , ρs) = ρ * ⅀?⟦ xs ⟧ (ρ , ρs) + ⟦ x ⟧ ρs
⅀?-hom : ∀ {n} (xs : Coeff n +) → ∀ ρ → ⅀?⟦ ∹ xs ⟧ ρ ≈ ⅀⟦ xs ⟧ ρ
⅀?-hom _ _ = refl
⟦∷⟧?-hom : ∀ {n} (x : Poly n) → ∀ xs ρ ρs → (x , xs) ⟦∷⟧? (ρ , ρs) ≈ (x , xs) ⟦∷⟧ (ρ , ρs)
⟦∷⟧?-hom x (∹ xs ) ρ ρs = refl
⟦∷⟧?-hom x [] ρ ρs = (≪+ zeroʳ _) ⟨ trans ⟩ +-identityˡ _
pow′-hom : ∀ {n} i (xs : Coeff n *) → ∀ ρ ρs → ((⅀?⟦ xs ⟧ (ρ , ρs)) *⟨ ρ ⟩^ i) ≈ (⅀?⟦ xs ⍓* i ⟧ (ρ , ρs))
pow′-hom i (∹ xs ) ρ ρs = pow-hom i xs ρ ρs
pow′-hom zero [] ρ ρs = refl
pow′-hom (suc i) [] ρ ρs = zeroʳ _
∷↓-hom-0 : ∀ {n} (x : Poly n) → ∀ xs ρ ρs → ⅀?⟦ x Δ 0 ∷↓ xs ⟧ (ρ , ρs) ≈ (x , xs) ⟦∷⟧ (ρ , ρs)
∷↓-hom-0 x xs ρ ρs with zero? x
∷↓-hom-0 x xs ρ ρs | no ¬p = refl
∷↓-hom-0 x [] ρ ρs | yes p = zero-hom x p ρs
∷↓-hom-0 x (∹ xs ) ρ ρs | yes p =
begin
⅀⟦ xs ⍓+ 1 ⟧ (ρ , ρs)
≈⟨ sym (pow-hom 1 xs ρ ρs) ⟩
ρ * ⅀⟦ xs ⟧ (ρ , ρs)
≈⟨ sym (+-identityʳ _) ⟨ trans ⟩ (+≫ zero-hom x p ρs) ⟩
ρ * ⅀⟦ xs ⟧ (ρ , ρs) + ⟦ x ⟧ ρs
∎
∷↓-hom-s : ∀ {n} (x : Poly n) → ∀ i xs ρ ρs → ⅀?⟦ x Δ suc i ∷↓ xs ⟧ (ρ , ρs) ≈ (ρ ^ suc i) * (x , xs) ⟦∷⟧ (ρ , ρs)
∷↓-hom-s x i xs ρ ρs with zero? x
∷↓-hom-s x i xs ρ ρs | no ¬p = refl
∷↓-hom-s x i [] ρ ρs | yes p = sym ((*≫ sym (zero-hom x p ρs)) ⟨ trans ⟩ zeroʳ _)
∷↓-hom-s x i (∹ xs ) ρ ρs | yes p =
begin
⅀⟦ xs ⍓+ (suc (suc i)) ⟧ (ρ , ρs)
≈⟨ sym (pow-hom (suc (suc i)) xs ρ ρs) ⟩
(ρ ^ suc (suc i)) * ⅀⟦ xs ⟧ (ρ , ρs)
≈⟨ *-assoc _ _ _ ⟩
(ρ ^ suc i) * (ρ * ⅀⟦ xs ⟧ (ρ , ρs))
≈⟨ *≫ (sym (+-identityʳ _) ⟨ trans ⟩ (+≫ zero-hom x p ρs)) ⟩
(ρ ^ suc i) * (ρ * ⅀⟦ xs ⟧ (ρ , ρs) + ⟦ x ⟧ ρs)
∎
∷↓-hom : ∀ {n}
→ (x : Poly n)
→ ∀ i xs ρ ρs
→ ⅀?⟦ x Δ i ∷↓ xs ⟧ (ρ , ρs) ≈ ρ ^ i * ((x , xs) ⟦∷⟧ (ρ , ρs))
∷↓-hom x zero xs ρ ρs = ∷↓-hom-0 x xs ρ ρs ⟨ trans ⟩ sym (*-identityˡ _)
∷↓-hom x (suc i) xs ρ ρs = ∷↓-hom-s x i xs ρ ρs
⟦∷⟧-hom : ∀ {n}
→ (x : Poly n)
→ (xs : Coeff n *)
→ ∀ ρ ρs → (x , xs) ⟦∷⟧ (ρ , ρs) ≈ ρ * ⅀?⟦ xs ⟧ (ρ , ρs) + ⟦ x ⟧ ρs
⟦∷⟧-hom x [] ρ ρs = sym ((≪+ zeroʳ _) ⟨ trans ⟩ +-identityˡ _)
⟦∷⟧-hom x (∹ xs) ρ ρs = refl
⅀-⊐↑-hom : ∀ {i n m}
→ (xs : Coeff i +)
→ (si≤n : suc i ≤′ n)
→ (sn≤m : suc n ≤′ m)
→ ∀ ρ
→ ⅀⟦ xs ⟧ (drop-1 (≤′-step si≤n ⟨ ≤′-trans ⟩ sn≤m) ρ)
≈ ⅀⟦ xs ⟧ (drop-1 si≤n (proj₂ (drop-1 sn≤m ρ)))
⅀-⊐↑-hom xs si≤n ≤′-refl (_ ∷ _) = refl
⅀-⊐↑-hom xs si≤n (≤′-step sn≤m) (_ ∷ ρ) = ⅀-⊐↑-hom xs si≤n sn≤m ρ
⊐↑-hom : ∀ {n m}
→ (x : Poly n)
→ (sn≤m : suc n ≤′ m)
→ ∀ ρ
→ ⟦ x ⊐↑ sn≤m ⟧ ρ ≈ ⟦ x ⟧ (proj₂ (drop-1 sn≤m ρ))
⊐↑-hom (Κ x ⊐ i≤sn) _ _ = refl
⊐↑-hom (⅀ xs ⊐ i≤sn) = ⅀-⊐↑-hom xs i≤sn
trans-join-coeffs-hom : ∀ {i j-1 n}
→ (i≤j-1 : suc i ≤′ j-1)
→ (j≤n : suc j-1 ≤′ n)
→ (xs : Coeff i +)
→ ∀ ρ
→ ⅀⟦ xs ⟧ (drop-1 i≤j-1 (proj₂ (drop-1 j≤n ρ))) ≈ ⅀⟦ xs ⟧ (drop-1 (≤′-step i≤j-1 ⟨ ≤′-trans ⟩ j≤n) ρ)
trans-join-coeffs-hom i<j-1 ≤′-refl xs (_ ∷ _) = refl
trans-join-coeffs-hom i<j-1 (≤′-step j<n) xs (_ ∷ ρ) = trans-join-coeffs-hom i<j-1 j<n xs ρ
trans-join-hom : ∀ {i j-1 n}
→ (i≤j-1 : i ≤′ j-1)
→ (j≤n : suc j-1 ≤′ n)
→ (x : FlatPoly i)
→ ∀ ρ
→ ⟦ x ⊐ i≤j-1 ⟧ (proj₂ (drop-1 j≤n ρ)) ≈ ⟦ x ⊐ (≤′-step i≤j-1 ⟨ ≤′-trans ⟩ j≤n) ⟧ ρ
trans-join-hom i≤j-1 j≤n (Κ x) _ = refl
trans-join-hom i≤j-1 j≤n (⅀ x) = trans-join-coeffs-hom i≤j-1 j≤n x
⊐↓-hom : ∀ {n m}
→ (xs : Coeff n *)
→ (sn≤m : suc n ≤′ m)
→ ∀ ρ
→ ⟦ xs ⊐↓ sn≤m ⟧ ρ ≈ ⅀?⟦ xs ⟧ (drop-1 sn≤m ρ)
⊐↓-hom [] sn≤m _ = 0-homo
⊐↓-hom (∹ x₁ Δ zero & ∹ xs) sn≤m _ = refl
⊐↓-hom (∹ x Δ suc j & xs ) sn≤m _ = refl
⊐↓-hom (∹ _≠0 x {x≠0} Δ zero & []) sn≤m ρs =
let (ρ , ρs′) = drop-1 sn≤m ρs
in
begin
⟦ x ⊐↑ sn≤m ⟧ ρs
≈⟨ ⊐↑-hom x sn≤m ρs ⟩
⟦ x ⟧ ρs′
∎
drop-1⇒lookup : ∀ {n} (i : Fin n) (ρs : Vec Carrier n) →
proj₁ (drop-1 (space≤′n i) ρs) ≡ Vec.lookup ρs i
drop-1⇒lookup zero (ρ ∷ ρs) = ≡.refl
drop-1⇒lookup (suc i) (ρ ∷ ρs) = drop-1⇒lookup i ρs
poly-foldR : ∀ {n} ρ ρs
→ ([f] : Fold n)
→ (f : Carrier → Carrier)
→ (∀ {x y} → x ≈ y → f x ≈ f y)
→ (∀ x y → x * f y ≈ f (x * y))
→ (∀ y {ys} zs → ⅀?⟦ ys ⟧ (ρ , ρs) ≈ f (⅀?⟦ zs ⟧ (ρ , ρs)) → [f] (y , ys) ⟦∷⟧? (ρ , ρs) ≈ f ((y , zs) ⟦∷⟧? (ρ , ρs)) )
→ (f 0# ≈ 0#)
→ ∀ xs
→ ⅀?⟦ para [f] xs ⟧ (ρ , ρs) ≈ f (⅀⟦ xs ⟧ (ρ , ρs))
poly-foldR ρ ρs f e cng dist step base (x ≠0 Δ suc i & []) =
let y,ys = f (x , [])
y = proj₁ y,ys
ys = proj₂ y,ys
in
begin
⅀?⟦ y Δ suc i ∷↓ ys ⟧ (ρ , ρs)
≈⟨ ∷↓-hom-s y i ys ρ ρs ⟩
(ρ ^ suc i) * ((y , ys) ⟦∷⟧ (ρ , ρs))
≈⟨ *≫ ⟦∷⟧?-hom y ys ρ ρs ⟨
(ρ ^ suc i) * ((y , ys) ⟦∷⟧? (ρ , ρs))
≈⟨ *≫ step x [] (sym base) ⟩
(ρ ^ suc i) * e ((x , []) ⟦∷⟧? (ρ , ρs))
≈⟨ *≫ cng (⟦∷⟧?-hom x [] ρ ρs) ⟩
(ρ ^ suc i) * e ((x , []) ⟦∷⟧ (ρ , ρs))
≈⟨ dist _ _ ⟩
e ((ρ ^ suc i) * ((x , []) ⟦∷⟧ (ρ , ρs)))
∎
poly-foldR ρ ρs f e cng dist step base (x ≠0 Δ suc i & ∹ xs) =
let ys = para f xs
y,zs = f (x , ys)
y = proj₁ y,zs
zs = proj₂ y,zs
in
begin
⅀?⟦ y Δ suc i ∷↓ zs ⟧ (ρ , ρs)
≈⟨ ∷↓-hom-s y i zs ρ ρs ⟩
(ρ ^ suc i) * ((y , zs) ⟦∷⟧ (ρ , ρs))
≈⟨ *≫ ⟦∷⟧?-hom y zs ρ ρs ⟨
(ρ ^ suc i) * ((y , zs) ⟦∷⟧? (ρ , ρs))
≈⟨ *≫ step x (∹ xs) (poly-foldR ρ ρs f e cng dist step base xs) ⟩
(ρ ^ suc i) * e ((x , (∹ xs )) ⟦∷⟧? (ρ , ρs))
≈⟨ *≫ cng (⟦∷⟧?-hom x (∹ xs ) ρ ρs) ⟩
(ρ ^ suc i) * e ((x , (∹ xs )) ⟦∷⟧ (ρ , ρs))
≈⟨ dist _ _ ⟩
e (ρ ^ suc i * ((x , (∹ xs )) ⟦∷⟧ (ρ , ρs)))
∎
poly-foldR ρ ρs f e cng dist step base (x ≠0 Δ ℕ.zero & []) =
let y,zs = f (x , [])
y = proj₁ y,zs
zs = proj₂ y,zs
in
begin
⅀?⟦ y Δ ℕ.zero ∷↓ zs ⟧ (ρ , ρs)
≈⟨ ∷↓-hom-0 y zs ρ ρs ⟩
((y , zs) ⟦∷⟧ (ρ , ρs))
≈⟨ ⟦∷⟧?-hom y zs ρ ρs ⟨
((y , zs) ⟦∷⟧? (ρ , ρs))
≈⟨ step x [] (sym base) ⟩
e ((x , []) ⟦∷⟧? (ρ , ρs))
≈⟨ cng (⟦∷⟧?-hom x [] ρ ρs) ⟩
e ((x , []) ⟦∷⟧ (ρ , ρs))
∎
poly-foldR ρ ρs f e cng dist step base (x ≠0 Δ ℕ.zero & (∹ xs )) =
let ys = para f xs
y,zs = f (x , ys)
y = proj₁ y,zs
zs = proj₂ y,zs
in
begin
⅀?⟦ y Δ ℕ.zero ∷↓ zs ⟧ (ρ , ρs)
≈⟨ ∷↓-hom-0 y zs ρ ρs ⟩
((y , zs) ⟦∷⟧ (ρ , ρs))
≈⟨ ⟦∷⟧?-hom y zs ρ ρs ⟨
((y , zs) ⟦∷⟧? (ρ , ρs))
≈⟨ step x (∹ xs ) (poly-foldR ρ ρs f e cng dist step base xs) ⟩
e ((x , (∹ xs )) ⟦∷⟧ (ρ , ρs))
≈⟨ cng (⟦∷⟧?-hom x (∹ xs ) ρ ρs) ⟩
e ((x , (∹ xs )) ⟦∷⟧ (ρ , ρs))
∎
poly-mapR : ∀ {n} ρ ρs
→ ([f] : Poly n → Poly n)
→ (f : Carrier → Carrier)
→ (∀ {x y} → x ≈ y → f x ≈ f y)
→ (∀ x y → x * f y ≈ f (x * y))
→ (∀ x y → f (x + y) ≈ f x + f y)
→ (∀ y → ⟦ [f] y ⟧ ρs ≈ f (⟦ y ⟧ ρs) )
→ (f 0# ≈ 0#)
→ ∀ xs
→ ⅀?⟦ poly-map [f] xs ⟧ (ρ , ρs) ≈ f (⅀⟦ xs ⟧ (ρ , ρs))
poly-mapR ρ ρs [f] f cng *-dist +-dist step′ base xs = poly-foldR ρ ρs (map₁ [f]) f cng *-dist step base xs
where
step : ∀ y {ys} zs → ⅀?⟦ ys ⟧ (ρ , ρs) ≈ f (⅀?⟦ zs ⟧ (ρ , ρs)) →(map₁ [f] (y , ys) ⟦∷⟧? (ρ , ρs)) ≈ f ((y , zs) ⟦∷⟧? (ρ , ρs))
step y {ys} zs ys≋zs =
begin
map₁ [f] (y , ys) ⟦∷⟧? (ρ , ρs)
≡⟨⟩
ρ * ⅀?⟦ ys ⟧ (ρ , ρs) + ⟦ [f] y ⟧ ρs
≈⟨ ((*≫ ys≋zs) ⟨ trans ⟩ *-dist ρ _) ⟨ +-cong ⟩ step′ y ⟩
f (ρ * ⅀?⟦ zs ⟧ (ρ , ρs)) + f (⟦ y ⟧ ρs)
≈⟨ sym (+-dist _ _) ⟩
f ((y , zs) ⟦∷⟧? (ρ , ρs))
∎