{-# OPTIONS --safe --cubical-compatible #-}
open import Tactic.RingSolver.Core.Polynomial.Parameters
module Tactic.RingSolver.Core.Polynomial.Base
{ℓ₁ ℓ₂} (coeffs : RawCoeff ℓ₁ ℓ₂) where
open RawCoeff coeffs
open import Data.Bool.Base using (Bool; true; false; T)
open import Data.Empty using (⊥)
open import Data.Fin.Base as Fin using (Fin; zero; suc)
open import Data.List.Kleene
open import Data.Nat.Base as ℕ using (ℕ; suc; zero; _≤′_; compare; ≤′-refl; ≤′-step; _<′_)
open import Data.Nat.Properties using (z≤′n; ≤′-trans)
open import Data.Nat.Induction
open import Data.Product.Base using (_×_; _,_; map₁; curry; uncurry)
open import Data.Unit.Base using (⊤; tt)
open import Function.Base
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Algebra.Definitions.RawSemiring rawSemiring
using (_^′_)
data InjectionOrdering {n : ℕ} : ∀ {i j} (i≤n : i ≤′ n) (j≤n : j ≤′ n) → Set
where
inj-lt : ∀ {i j-1} (i≤j-1 : i ≤′ j-1) (j≤n : suc j-1 ≤′ n) →
InjectionOrdering (≤′-step i≤j-1 ⟨ ≤′-trans ⟩ j≤n) j≤n
inj-gt : ∀ {i-1 j} (i≤n : suc i-1 ≤′ n) (j≤i-1 : j ≤′ i-1) →
InjectionOrdering i≤n (≤′-step j≤i-1 ⟨ ≤′-trans ⟩ i≤n)
inj-eq : ∀ {i} (i≤n : i ≤′ n) →
InjectionOrdering i≤n i≤n
inj-compare : ∀ {i j n} (x : i ≤′ n) (y : j ≤′ n) → InjectionOrdering x y
inj-compare ≤′-refl ≤′-refl = inj-eq ≤′-refl
inj-compare ≤′-refl (≤′-step y) = inj-gt ≤′-refl y
inj-compare (≤′-step x) ≤′-refl = inj-lt x ≤′-refl
inj-compare (≤′-step x) (≤′-step y) = case inj-compare x y of
λ { (inj-lt i≤j-1 y) → inj-lt i≤j-1 (≤′-step y)
; (inj-gt x j≤i-1) → inj-gt (≤′-step x) j≤i-1
; (inj-eq x) → inj-eq (≤′-step x)
}
space : ∀ {n} → Fin n → ℕ
space f = suc (go f)
where
go : ∀ {n} → Fin n → ℕ
go {suc n} Fin.zero = n
go (Fin.suc x) = go x
space≤′n : ∀ {n} (x : Fin n) → space x ≤′ n
space≤′n zero = ≤′-refl
space≤′n (suc x) = ≤′-step (space≤′n x)
infixl 6 _Δ_
record PowInd {c} (C : Set c) : Set c where
constructor _Δ_
field
coeff : C
pow : ℕ
open PowInd public
record Poly (n : ℕ) : Set ℓ₁
data FlatPoly : ℕ → Set ℓ₁
Coeff : ℕ → Set ℓ₁
record NonZero (i : ℕ) : Set ℓ₁
Zero : ∀ {n} → Poly n → Set
Normalised : ∀ {i} → Coeff i + → Set
infixl 6 _⊐_
record Poly n where
inductive
constructor _⊐_
eta-equality
field
{i} : ℕ
flat : FlatPoly i
i≤n : i ≤′ n
data FlatPoly where
Κ : Carrier → FlatPoly zero
⅀ : ∀ {n} (xs : Coeff n +) {xn : Normalised xs} → FlatPoly (suc n)
Coeff n = PowInd (NonZero n)
infixl 6 _≠0
record NonZero i where
inductive
constructor _≠0
field
poly : Poly i
.{poly≠0} : ¬ Zero poly
Zero (Κ x ⊐ _) = T (isZero x)
Zero (⅀ _ ⊐ _) = ⊥
Normalised (_ Δ zero & []) = ⊥
Normalised (_ Δ zero & ∹ _) = ⊤
Normalised (_ Δ suc _ & _) = ⊤
open NonZero public
open Poly public
zero? : ∀ {n} → (p : Poly n) → Dec (Zero p)
zero? (⅀ _ ⊐ _) = no id
zero? (Κ x ⊐ _) with isZero x
... | true = yes tt
... | false = no id
{-# INLINE zero? #-}
infixr 8 _⍓*_ _⍓+_
_⍓*_ : ∀ {n} → Coeff n * → ℕ → Coeff n *
_⍓+_ : ∀ {n} → Coeff n + → ℕ → Coeff n +
[] ⍓* _ = []
(∹ xs) ⍓* i = ∹ xs ⍓+ i
coeff (head (xs ⍓+ i)) = coeff (head xs)
pow (head (xs ⍓+ i)) = pow (head xs) ℕ.+ i
tail (xs ⍓+ i) = tail xs
infixr 5 _∷↓_
_∷↓_ : ∀ {n} → PowInd (Poly n) → Coeff n * → Coeff n *
x Δ i ∷↓ xs = case zero? x of
λ { (yes p) → xs ⍓* suc i
; (no ¬p) → ∹ _≠0 x {¬p} Δ i & xs
}
{-# INLINE _∷↓_ #-}
_⊐↑_ : ∀ {n m} → Poly n → (suc n ≤′ m) → Poly m
(xs ⊐ i≤n) ⊐↑ n≤m = xs ⊐ (≤′-step i≤n ⟨ ≤′-trans ⟩ n≤m)
{-# INLINE _⊐↑_ #-}
infixr 4 _⊐↓_
_⊐↓_ : ∀ {i n} → Coeff i * → suc i ≤′ n → Poly n
[] ⊐↓ i≤n = Κ 0# ⊐ z≤′n
(∹ (x ≠0 Δ zero & [] )) ⊐↓ i≤n = x ⊐↑ i≤n
(∹ (x Δ zero & ∹ xs)) ⊐↓ i≤n = ⅀ (x Δ zero & ∹ xs) ⊐ i≤n
(∹ (x Δ suc j & xs )) ⊐↓ i≤n = ⅀ (x Δ suc j & xs) ⊐ i≤n
{-# INLINE _⊐↓_ #-}
PolyF : ℕ → Set ℓ₁
PolyF i = Poly i × Coeff i *
Fold : ℕ → Set ℓ₁
Fold i = PolyF i → PolyF i
para : ∀ {i} → Fold i → Coeff i + → Coeff i *
para f (x ≠0 Δ i & []) = case f (x , []) of λ {(y , ys) → y Δ i ∷↓ ys}
para f (x ≠0 Δ i & ∹ xs) = case f (x , para f xs) of λ {(y , ys) → y Δ i ∷↓ ys}
poly-map : ∀ {i} → (Poly i → Poly i) → Coeff i + → Coeff i *
poly-map f = para (map₁ f)
{-# INLINE poly-map #-}
mutual
infixl 6 _⊞_
_⊞_ : ∀ {n} → Poly n → Poly n → Poly n
(xs ⊐ i≤n) ⊞ (ys ⊐ j≤n) = ⊞-match (inj-compare i≤n j≤n) xs ys
⊞-match : ∀ {i j n}
→ {i≤n : i ≤′ n}
→ {j≤n : j ≤′ n}
→ InjectionOrdering i≤n j≤n
→ FlatPoly i
→ FlatPoly j
→ Poly n
⊞-match (inj-eq i&j≤n) (Κ x) (Κ y) = Κ (x + y) ⊐ i&j≤n
⊞-match (inj-eq i&j≤n) (⅀ (x Δ i & xs)) (⅀ (y Δ j & ys)) = ⊞-zip (compare i j) x xs y ys ⊐↓ i&j≤n
⊞-match (inj-lt i≤j-1 j≤n) xs (⅀ ys) = ⊞-inj i≤j-1 xs ys ⊐↓ j≤n
⊞-match (inj-gt i≤n j≤i-1) (⅀ xs) ys = ⊞-inj j≤i-1 ys xs ⊐↓ i≤n
⊞-inj : ∀ {i k}
→ (i ≤′ k)
→ FlatPoly i
→ Coeff k +
→ Coeff k *
⊞-inj i≤k xs (y ⊐ j≤k ≠0 Δ zero & ys) = ⊞-match (inj-compare j≤k i≤k) y xs Δ zero ∷↓ ys
⊞-inj i≤k xs (y Δ suc j & ys) = xs ⊐ i≤k Δ zero ∷↓ ∹ y Δ j & ys
⊞-coeffs : ∀ {n} → Coeff n * → Coeff n * → Coeff n *
⊞-coeffs (∹ x Δ i & xs) ys = ⊞-zip-r x i xs ys
⊞-coeffs [] ys = ys
⊞-zip : ∀ {p q n}
→ ℕ.Ordering p q
→ NonZero n
→ Coeff n *
→ NonZero n
→ Coeff n *
→ Coeff n *
⊞-zip (ℕ.less i k) x xs y ys = ∹ x Δ i & ⊞-zip-r y k ys xs
⊞-zip (ℕ.greater j k) x xs y ys = ∹ y Δ j & ⊞-zip-r x k xs ys
⊞-zip (ℕ.equal i ) x xs y ys = (x .poly ⊞ y .poly) Δ i ∷↓ ⊞-coeffs xs ys
{-# INLINE ⊞-zip #-}
⊞-zip-r : ∀ {n} → NonZero n → ℕ → Coeff n * → Coeff n * → Coeff n *
⊞-zip-r x i xs [] = ∹ x Δ i & xs
⊞-zip-r x i xs (∹ y Δ j & ys) = ⊞-zip (compare i j) x xs y ys
⊟-step : ∀ {n} → Acc _<′_ n → Poly n → Poly n
⊟-step (acc wf) (Κ x ⊐ i≤n) = Κ (- x) ⊐ i≤n
⊟-step (acc wf) (⅀ xs ⊐ i≤n) = poly-map (⊟-step (wf i≤n)) xs ⊐↓ i≤n
⊟_ : ∀ {n} → Poly n → Poly n
⊟_ = ⊟-step (<′-wellFounded _)
{-# INLINE ⊟_ #-}
mutual
⊠-step′ : ∀ {n} → Acc _<′_ n → Poly n → Poly n → Poly n
⊠-step′ a (x ⊐ i≤n) = ⊠-step a x i≤n
⊠-step : ∀ {i n} → Acc _<′_ n → FlatPoly i → i ≤′ n → Poly n → Poly n
⊠-step a (Κ x) _ = ⊠-Κ a x
⊠-step a (⅀ xs) = ⊠-⅀ a xs
⊠-Κ : ∀ {n} → Acc _<′_ n → Carrier → Poly n → Poly n
⊠-Κ (acc _ ) x (Κ y ⊐ i≤n) = Κ (x * y) ⊐ i≤n
⊠-Κ (acc wf) x (⅀ xs ⊐ i≤n) = ⊠-Κ-inj (wf i≤n) x xs ⊐↓ i≤n
{-# INLINE ⊠-Κ #-}
⊠-⅀ : ∀ {i n} → Acc _<′_ n → Coeff i + → i <′ n → Poly n → Poly n
⊠-⅀ (acc wf) xs i≤n (⅀ ys ⊐ j≤n) = ⊠-match (acc wf) (inj-compare i≤n j≤n) xs ys
⊠-⅀ (acc wf) xs i≤n (Κ y ⊐ _) = ⊠-Κ-inj (wf i≤n) y xs ⊐↓ i≤n
⊠-Κ-inj : ∀ {i} → Acc _<′_ i → Carrier → Coeff i + → Coeff i *
⊠-Κ-inj a x xs = poly-map (⊠-Κ a x) (xs)
⊠-⅀-inj : ∀ {i k}
→ Acc _<′_ k
→ i <′ k
→ Coeff i +
→ Poly k
→ Poly k
⊠-⅀-inj (acc wf) i≤k x (⅀ y ⊐ j≤k) = ⊠-match (acc wf) (inj-compare i≤k j≤k) x y
⊠-⅀-inj (acc wf) i≤k x (Κ y ⊐ j≤k) = ⊠-Κ-inj (wf i≤k) y x ⊐↓ i≤k
⊠-match : ∀ {i j n}
→ Acc _<′_ n
→ {i≤n : i <′ n}
→ {j≤n : j <′ n}
→ InjectionOrdering i≤n j≤n
→ Coeff i +
→ Coeff j +
→ Poly n
⊠-match (acc wf) (inj-eq i&j≤n) xs ys = ⊠-coeffs (wf i&j≤n) xs ys ⊐↓ i&j≤n
⊠-match (acc wf) (inj-lt i≤j-1 j≤n) xs ys = poly-map (⊠-⅀-inj (wf j≤n) i≤j-1 xs) (ys) ⊐↓ j≤n
⊠-match (acc wf) (inj-gt i≤n j≤i-1) xs ys = poly-map (⊠-⅀-inj (wf i≤n) j≤i-1 ys) (xs) ⊐↓ i≤n
⊠-coeffs : ∀ {n} → Acc _<′_ n → Coeff n + → Coeff n + → Coeff n *
⊠-coeffs a (xs) (y ≠0 Δ j & []) = poly-map (⊠-step′ a y) (xs) ⍓* j
⊠-coeffs a (xs) (y ≠0 Δ j & ∹ ys) = para (⊠-cons a y ys) (xs) ⍓* j
{-# INLINE ⊠-coeffs #-}
⊠-cons : ∀ {n}
→ Acc _<′_ n
→ Poly n
→ Coeff n +
→ Fold n
⊠-cons a y ys (x ⊐ j≤n , xs) =
⊠-step a x j≤n y , ⊞-coeffs (poly-map (⊠-step a x j≤n) ys) xs
{-# INLINE ⊠-cons #-}
infixl 7 _⊠_
_⊠_ : ∀ {n} → Poly n → Poly n → Poly n
_⊠_ = ⊠-step′ (<′-wellFounded _)
{-# INLINE _⊠_ #-}
κ : ∀ {n} → Carrier → Poly n
κ x = Κ x ⊐ z≤′n
{-# INLINE κ #-}
ι : ∀ {n} → Fin n → Poly n
ι i = (κ 1# Δ 1 ∷↓ []) ⊐↓ space≤′n i
{-# INLINE ι #-}
⊡-mult : ∀ {n} → ℕ → Poly n → Poly n
⊡-mult zero xs = xs
⊡-mult (suc n) xs = ⊡-mult n xs ⊠ xs
_⊡_+1 : ∀ {n} → Poly n → ℕ → Poly n
(Κ x ⊐ i≤n) ⊡ i +1 = Κ (x ^′ suc i) ⊐ i≤n
(⅀ (x Δ j & []) ⊐ i≤n) ⊡ i +1 = x .poly ⊡ i +1 Δ (j ℕ.+ i ℕ.* j) ∷↓ [] ⊐↓ i≤n
xs@(⅀ (_ & ∹ _) ⊐ i≤n) ⊡ i +1 = ⊡-mult i xs
infixr 8 _⊡_
_⊡_ : ∀ {n} → Poly n → ℕ → Poly n
_ ⊡ zero = κ 1#
xs ⊡ suc i = xs ⊡ i +1
{-# INLINE _⊡_ #-}