diff --git a/src/Algebra/Polynomial/Base.agda b/src/Algebra/Polynomial/Base.agda new file mode 100644 index 0000000000..84ae5763e0 --- /dev/null +++ b/src/Algebra/Polynomial/Base.agda @@ -0,0 +1,78 @@ +open import Algebra.Bundles using (Semiring) +open import Data.Nat.Base as ℕ using (ℕ; _⊔_; suc; pred) +open import Data.Product.Base using (_,_) +open import Data.Vec.Base as Vec using ([]; _∷_) +import Level as L + +module Algebra.Polynomial.Base + {ℓ₁ ℓ₂} (SR : Semiring ℓ₁ ℓ₂) + where + +open import Algebra.Polynomial.Poly.Base SR as Poly + using (Poly; zeros) + +open Semiring SR + using (0#; 1#) + renaming (Carrier to A) + +private + variable + m n k : ℕ + p : Poly m + q : Poly n + r : Poly k + +--------------------------------------------------- +-- Types + +record Polynomial : Set ℓ₁ where + constructor _,_ + field + degree : ℕ + polynomial : Poly degree + +private + variable + P Q R : Polynomial + +-- Equivalence relation for representations of polynomials +infix 4 _≈_ +_≈_ : Polynomial → Polynomial → Set (ℓ₁ L.⊔ ℓ₂) +(m , p) ≈ (n , q) = p Poly.≈ q + +refl : P ≈ P +refl = Poly.refl + +sym : P ≈ Q → Q ≈ P +sym = Poly.sym + +trans : P ≈ Q → Q ≈ R → P ≈ R +trans = Poly.trans + +-------------------------------------------------- +-- Constants + +zero : Polynomial +zero = (0 , []) + +one : Polynomial +one = (1 , (1# ∷ [])) + +--------------------------------------------------- +-- Operations + +-- Multiply the polynomial by a factor of x +shift : Polynomial → Polynomial +shift (m , p) = (suc m , Poly.shift p) + +-- Scaling +_·_ : A → Polynomial → Polynomial +a · (m , p) = (m , a Poly.· p) + +-- Addition +_+_ : Polynomial → Polynomial → Polynomial +(m , p) + (n , q) = (m ⊔ n , p Poly.+ q) + +-- Multiplication +_*_ : Polynomial → Polynomial → Polynomial +(m , p) * (n , q) = (pred (m ℕ.+ n) , p Poly.* q) diff --git a/src/Algebra/Polynomial/Base1.agda b/src/Algebra/Polynomial/Base1.agda new file mode 100644 index 0000000000..bc68980ffd --- /dev/null +++ b/src/Algebra/Polynomial/Base1.agda @@ -0,0 +1,82 @@ +open import Algebra.Bundles using (Ring) +open import Data.Nat.Base as ℕ using (ℕ; _⊔_; suc; pred) +open import Data.Product.Base using (_,_) +open import Data.Vec.Base as Vec using ([]; _∷_) +import Level as L + +module Algebra.Polynomial.Base1 + {ℓ₁ ℓ₂} (R : Ring ℓ₁ ℓ₂) + where + +open import Algebra.Polynomial.Poly.Base1 R as Poly + using (Poly; zeros) + +open Ring R + using (0#; 1#) + renaming (Carrier to A) + +private + variable + m n k : ℕ + p : Poly m + q : Poly n + r : Poly k + +--------------------------------------------------- +-- Types + +record Polynomial : Set ℓ₁ where + constructor _,_ + field + degree : ℕ + polynomial : Poly degree + +private + variable + P Q W : Polynomial + +-- Equivalence relation for representations of polynomials +infix 4 _≈_ +_≈_ : Polynomial → Polynomial → Set (ℓ₁ L.⊔ ℓ₂) +(m , p) ≈ (n , q) = p Poly.≈ q + +refl : P ≈ P +refl = Poly.refl + +sym : P ≈ Q → Q ≈ P +sym = Poly.sym + +trans : P ≈ Q → Q ≈ W → P ≈ W +trans = Poly.trans + +-------------------------------------------------- +-- Constants + +zero : Polynomial +zero = (0 , []) + +one : Polynomial +one = (1 , (1# ∷ [])) + +--------------------------------------------------- +-- Operations + +-- Multiply the polynomial by a factor of x +shift : Polynomial → Polynomial +shift (m , p) = (suc m , Poly.shift p) + +-- Negation +-_ : Polynomial → Polynomial +- (m , p) = (m , Poly.- p) + +-- Scaling +_·_ : A → Polynomial → Polynomial +a · (m , p) = (m , a Poly.· p) + +-- Addition +_+_ : Polynomial → Polynomial → Polynomial +(m , p) + (n , q) = (m ⊔ n , p Poly.+ q) + +-- Multiplication +_*_ : Polynomial → Polynomial → Polynomial +(m , p) * (n , q) = (pred (m ℕ.+ n) , p Poly.* q) diff --git a/src/Algebra/Polynomial/Base2.agda b/src/Algebra/Polynomial/Base2.agda new file mode 100644 index 0000000000..a4316f82f8 --- /dev/null +++ b/src/Algebra/Polynomial/Base2.agda @@ -0,0 +1,82 @@ +open import Algebra.Bundles using (CommutativeRing) +open import Data.Nat.Base as ℕ using (ℕ; _⊔_; suc; pred) +open import Data.Product.Base using (_,_) +open import Data.Vec.Base as Vec using ([]; _∷_) +import Level as L + +module Algebra.Polynomial.Base2 + {ℓ₁ ℓ₂} (CR : CommutativeRing ℓ₁ ℓ₂) + where + +open import Algebra.Polynomial.Poly.Base2 CR as Poly + using (Poly; zeros) + +open CommutativeRing CR + using (0#; 1#) + renaming (Carrier to A) + +private + variable + m n k : ℕ + p : Poly m + q : Poly n + r : Poly k + +--------------------------------------------------- +-- Types + +record Polynomial : Set ℓ₁ where + constructor _,_ + field + degree : ℕ + polynomial : Poly degree + +private + variable + P Q R : Polynomial + +-- Equivalence relation for representations of polynomials +infix 4 _≈_ +_≈_ : Polynomial → Polynomial → Set (ℓ₁ L.⊔ ℓ₂) +(m , p) ≈ (n , q) = p Poly.≈ q + +refl : P ≈ P +refl = Poly.refl + +sym : P ≈ Q → Q ≈ P +sym = Poly.sym + +trans : P ≈ Q → Q ≈ R → P ≈ R +trans = Poly.trans + +-------------------------------------------------- +-- Constants + +zero : Polynomial +zero = (0 , []) + +one : Polynomial +one = (1 , (1# ∷ [])) + +--------------------------------------------------- +-- Operations + +-- Multiply the polynomial by a factor of x +shift : Polynomial → Polynomial +shift (m , p) = (suc m , Poly.shift p) + +-- Negation +-_ : Polynomial → Polynomial +- (m , p) = (m , Poly.- p) + +-- Scaling +_·_ : A → Polynomial → Polynomial +a · (m , p) = (m , a Poly.· p) + +-- Addition +_+_ : Polynomial → Polynomial → Polynomial +(m , p) + (n , q) = (m ⊔ n , p Poly.+ q) + +-- Multiplication +_*_ : Polynomial → Polynomial → Polynomial +(m , p) * (n , q) = (pred (m ℕ.+ n) , p Poly.* q) diff --git a/src/Algebra/Polynomial/Morphism/Morphism.agda b/src/Algebra/Polynomial/Morphism/Morphism.agda new file mode 100644 index 0000000000..05020c0b93 --- /dev/null +++ b/src/Algebra/Polynomial/Morphism/Morphism.agda @@ -0,0 +1,510 @@ +-- Polynomial Morphisms +open import Algebra.Bundles + using (CommutativeRing ; CommutativeSemiring; Ring; + SemiringWithoutAnnihilatingZero; Semiring) + +module ALgebra.Polynomial.Morphism.Morphism + {ℓ₁ ℓ₂} + (R : CommutativeRing ℓ₁ ℓ₂) + where + +open import Algebra.Bundles.Raw using (RawRing) +open import Algebra.Morphism.Bundles + using (RingHomomorphism ; MagmaHomomorphism ; MonoidHomomorphism) +open import Algebra.Morphism.Structures + using (IsRingHomomorphism ; IsMagmaHomomorphism ; IsSemiringHomomorphism; + IsNearSemiringHomomorphism ; IsMonoidHomomorphism) +open import Algebra.Polynomial.Poly.Base2 R + using (Poly; []≈ ; ≈[]; cons ; cast-lem ; consˡ ; consʳ) + renaming ( sym to P-sym ; _·_ to _·P_ + ; _+_ to _+P_ ; _*_ to _*P_; _≈_ to _≈P_; -_ to -P_) +open import Algebra.Polynomial.Poly.Properties2 R + using (cast-p≈p; IsZero⇒≈0; ≈0⇒IsZero; a·p≈a∷[]*p ; *-distrib-shift) + renaming (+-identityˡ to +-P-identityˡ ; +-identityʳ to +-P-identityʳ + ; zeroˡ to P-zeroˡ; zeroʳ to P-zeroʳ ; *-comm to *-P-comm ) +open import Algebra.Polynomial.Base2 R +open import Algebra.Polynomial.Properties2 R as P + using (+-identityˡ; +-identityʳ; +-*-commutativeRing; *-zeroˡ ; *-zeroʳ) + +import Algebra.Definitions.RawSemiring as Def +import Algebra.Definitions as D +open import Algebra.Properties.Group +open import Algebra.Properties.Ring +open import Data.Nat.Base as ℕ using (ℕ; suc; pred; _⊔_) +open import Data.Vec.Base as Vec using (Vec; []; _∷_) +open import Data.Vec.Relation.Unary.All +open import Data.Product.Base using (proj₁ ; proj₂) +import Level as L +import Relation.Binary.Morphism.Structures as S + using (IsRelHomomorphism) +open import Relation.Binary.PropositionalEquality.Core using (cong) + +module R = CommutativeRing R +open R + hiding (distrib) + renaming + ( Carrier to A + ; _≈_ to _≈A_ + ; _+_ to _+A_ + ; _*_ to _*A_ + ; -_ to -A_ + ; 0# to A0# + ; 1# to A1#) + +private + variable + m n k l : ℕ + a b c d : A + p : Poly m + q : Poly n + P : Polynomial + Q : Polynomial + +module PolynomialRingMorphism + {ℓ₃ ℓ₄} + (B : CommutativeRing ℓ₃ ℓ₄) + (β : CommutativeRing.Carrier B) + + (f : RingHomomorphism {ℓ₁} {ℓ₂} + (CommutativeRing.rawRing R) (CommutativeRing.rawRing B) ) + where + + module B = CommutativeRing B + open B + using (semiringWithoutOne ; isSemiringWithoutOne ; distrib) + renaming + (_≈_ to _≈B_ + ; _+_ to _+B_ + ; _*_ to _*B_ + ; -_ to -B_ + ; setoid to B-Set) + using (0#; 1#) + + open import Relation.Binary.Reasoning.Setoid B-Set + + open RingHomomorphism f using (⟦_⟧) + open D {A = B.Carrier} (_≈B_) + using (_MiddleFourExchange_; _DistributesOverˡ_) + + eval-p : Poly m → CommutativeRing.Carrier B + eval-p [] = 0# + eval-p (a ∷ p) = ⟦ a ⟧ +B (β *B eval-p p ) + + + eval : Polynomial → CommutativeRing.Carrier B + eval (ℕ.zero , []) = 0# + eval (suc n , (a ∷ p)) = ⟦ a ⟧ +B (β *B eval (n , p) ) + + + + eval-equiv : (p : Poly m) → eval-p p ≈B (eval (m , p)) + eval-equiv {ℕ.zero} [] = B.refl + eval-equiv {suc m} (a ∷ p) = begin + ⟦ a ⟧ +B β *B eval-p p + ≈⟨ B.+-congˡ (B.*-congˡ (eval-equiv p) ) ⟩ + ⟦ a ⟧ +B β *B eval (m , p) + ∎ + + + eval-p-cong : ∀ {p : Poly m} → ∀ {q : Poly n} → p ≈P q → (eval-p p) ≈B (eval-p q) + eval-p-cong {p = []} {[]} P≈Q = B.refl + eval-p-cong {p = []} {b ∷ q} p≈q = begin + eval-p [] + ≈⟨ B.zeroʳ β ⟨ + β *B 0# + ≈⟨ B.+-identityˡ (β *B eval-p []) ⟨ + 0# +B β *B eval-p [] + ≈⟨ B.+-congʳ (MonoidHomomorphism.ε-homo + (RingHomomorphism.+-monoidHomomorphism f)) ⟨ + ⟦ A0# ⟧ +B β *B eval-p [] + ≈⟨ B.+-congˡ (B.*-congˡ (eval-p-cong {p = []} {q = q} + (P-sym (IsZero⇒≈0 (tail (≈0⇒IsZero (P-sym p≈q))))))) ⟩ + ⟦ A0# ⟧ +B β *B eval-p q + ≈⟨ B.+-congʳ (S.IsRelHomomorphism.cong + (RingHomomorphism.isRelHomomorphism f) (head (≈0⇒IsZero (P-sym p≈q)))) ⟨ + eval-p (b ∷ q) + ∎ + eval-p-cong {p = a ∷ p} {[]} p≈q = begin + eval-p (a ∷ p) + ≈⟨ B.+-congʳ (S.IsRelHomomorphism.cong + (RingHomomorphism.isRelHomomorphism f) (head (≈0⇒IsZero p≈q))) ⟩ + ⟦ A0# ⟧ +B β *B eval-p p + ≈⟨ B.+-congˡ (B.*-congˡ (eval-p-cong {p = p} {q = []} + (IsZero⇒≈0 (tail (≈0⇒IsZero p≈q))))) ⟩ + ⟦ A0# ⟧ +B β *B eval-p [] + ≈⟨ B.+-congʳ (MonoidHomomorphism.ε-homo + (RingHomomorphism.+-monoidHomomorphism f)) ⟩ + 0# +B β *B eval-p [] + ≈⟨ B.+-congˡ (B.zeroʳ β) ⟩ + 0# +B 0# + ≈⟨ B.+-identityʳ 0# ⟩ + eval-p [] + ∎ + eval-p-cong {p = a ∷ p} {b ∷ q} (cons a≈b p≈q) + = B.+-cong (S.IsRelHomomorphism.cong (RingHomomorphism.isRelHomomorphism f) a≈b) + (B.*-congˡ (eval-p-cong p≈q)) + + + eval-cong : P ≈ Q → eval P ≈B eval Q + eval-cong {P = (m , p)} {Q = (n , q)} P≈Q = begin + eval (m , p) + ≈⟨ eval-equiv p ⟨ + eval-p p + ≈⟨ eval-p-cong P≈Q ⟩ + eval-p q + ≈⟨ eval-equiv q ⟩ + eval (n , q) + ∎ + + + + eval-p-+-homomorphic : (p : Poly m) → (q : Poly n) → eval-p (p +P q) ≈B eval-p p +B eval-p q + eval-p-+-homomorphic [] q = begin + eval-p ([] +P q) + ≈⟨ eval-p-cong (+-P-identityˡ {m = 0} q) ⟩ + eval-p q + ≈⟨ B.+-identityˡ (eval-p q) ⟨ + eval-p [] +B eval-p q + ∎ + eval-p-+-homomorphic (a ∷ p) [] = B.sym (B.+-identityʳ (eval-p (a ∷ p))) + eval-p-+-homomorphic (a ∷ p) (b ∷ q) = begin + eval-p ((a ∷ p) +P (b ∷ q)) + ≈⟨ B.+-congˡ (B.*-congˡ (eval-p-+-homomorphic p q)) ⟩ + ⟦ a +A b ⟧ +B (β *B (eval-p p +B eval-p q)) + ≈⟨ B.+-congˡ (proj₁ distrib β (eval-p p) (eval-p q)) ⟩ + ⟦ a +A b ⟧ +B (β *B eval-p p +B β *B eval-p q) + ≈⟨ B.+-congʳ (IsMagmaHomomorphism.homo (RingHomomorphism.+-isMagmaHomomorphism f) a b) ⟩ + ⟦ a ⟧ +B ⟦ b ⟧ +B (β *B eval-p p +B β *B eval-p q) + ≈⟨ B.+-assoc (⟦ a ⟧ +B ⟦ b ⟧) (β *B eval-p p) (β *B eval-p q) ⟨ + ⟦ a ⟧ +B ⟦ b ⟧ +B β *B eval-p p +B β *B eval-p q + ≈⟨ B.+-congʳ (B.+-assoc ⟦ a ⟧ ⟦ b ⟧ (β *B eval-p p)) ⟩ + ⟦ a ⟧ +B (⟦ b ⟧ +B β *B eval-p p) +B β *B eval-p q + ≈⟨ B.+-assoc (⟦ a ⟧) (⟦ b ⟧ +B β *B eval-p p) (β *B eval-p q) ⟩ + ⟦ a ⟧ +B ( ⟦ b ⟧ +B β *B eval-p p +B (β *B eval-p q)) + ≈⟨ B.+-congˡ (B.+-congʳ ((B.+-comm (β *B eval-p p) ⟦ b ⟧))) ⟨ + ⟦ a ⟧ +B ((β *B eval-p p) +B ⟦ b ⟧ +B (β *B eval-p q)) + ≈⟨ B.+-congˡ (B.+-assoc (β *B eval-p p) ⟦ b ⟧ (β *B eval-p q)) ⟩ + ⟦ a ⟧ +B (β *B eval-p p +B eval-p (b ∷ q)) + ≈⟨ B.+-assoc ⟦ a ⟧ (β *B eval-p p) (eval-p (b ∷ q)) ⟨ + ⟦ a ⟧ +B β *B eval-p p +B eval-p (b ∷ q) + ∎ + + + + eval-+-homomorphic : (P : Polynomial) → (Q : Polynomial) → eval (P + Q) ≈B eval P +B eval Q + eval-+-homomorphic (m , p) (n , q) = begin + eval ((m , p) + (n , q)) + ≈⟨ eval-equiv (p +P q) ⟨ + eval-p (p +P q) + ≈⟨ eval-p-+-homomorphic p q ⟩ + eval-p p +B eval-p q + ≈⟨ B.+-cong (eval-equiv p) (eval-equiv q) ⟩ + eval (m , p) +B eval (n , q) + ∎ + + eval-p-1#-homomorphic : eval-p (A1# ∷ []) ≈B 1# + eval-p-1#-homomorphic = begin + eval-p (A1# ∷ []) + ≈⟨ B.+-cong (RingHomomorphism.1#-homo f) (B.zeroʳ β) ⟩ + 1# +B 0# + ≈⟨ B.+-identityʳ 1# ⟩ + 1# + ∎ + + eval-1#-homomorphic : eval one ≈B 1# + eval-1#-homomorphic = begin + eval (1 , (A1# ∷ [])) + ≈⟨ eval-equiv (A1# ∷ []) ⟨ + eval-p (A1# ∷ []) + ≈⟨ eval-p-1#-homomorphic ⟩ + 1# + ∎ + + + eval-p-scale : (a : A) → (p : Poly m) → eval-p (a ·P p) ≈B eval-p (a ∷ []) *B (eval-p p) + eval-p-scale a [] = begin + 0# + ≈⟨ B.zeroʳ (⟦ a ⟧ +B β *B 0#) ⟨ + (⟦ a ⟧ +B β *B 0#) *B 0# + ∎ + eval-p-scale a (b ∷ p) = begin + ⟦ a *A b ⟧ +B β *B eval-p (a ·P p) + ≈⟨ B.+-congʳ (IsMagmaHomomorphism.homo (RingHomomorphism.*-isMagmaHomomorphism f) a b) ⟩ + (⟦ a ⟧ *B ⟦ b ⟧) +B β *B eval-p (a ·P p) + ≈⟨ B.+-congˡ (B.*-congˡ (eval-p-scale a p)) ⟩ + (⟦ a ⟧ *B ⟦ b ⟧) +B β *B (eval-p (a ∷ []) *B (eval-p p)) + ≈⟨ B.+-congˡ (B.*-congˡ (B.*-congʳ (B.+-congˡ (B.zeroʳ β)))) ⟩ + (⟦ a ⟧ *B ⟦ b ⟧) +B β *B ((⟦ a ⟧ +B 0#) *B (eval-p p)) + ≈⟨ B.+-congˡ (B.*-congˡ (B.*-congʳ (B.+-identityʳ ⟦ a ⟧))) ⟩ + ⟦ a ⟧ *B ⟦ b ⟧ +B β *B ((⟦ a ⟧ *B eval-p p)) + ≈⟨ B.+-congˡ (B.*-assoc β ⟦ a ⟧ (eval-p p)) ⟨ + ⟦ a ⟧ *B ⟦ b ⟧ +B (β *B (⟦ a ⟧) *B (eval-p p)) + ≈⟨ B.+-congˡ (B.*-congʳ (B.*-comm β ⟦ a ⟧)) ⟩ + (⟦ a ⟧ *B ⟦ b ⟧) +B (⟦ a ⟧ *B β) *B eval-p p + ≈⟨ B.+-congˡ (B.*-assoc ⟦ a ⟧ β (eval-p p)) ⟩ + (⟦ a ⟧ *B ⟦ b ⟧) +B ⟦ a ⟧ *B (β *B eval-p p) + ≈⟨ proj₁ distrib ⟦ a ⟧ ⟦ b ⟧ ( β *B eval-p p) ⟨ + (⟦ a ⟧) *B (⟦ b ⟧ +B β *B eval-p p) + ≈⟨ B.*-congʳ (B.+-identityʳ ⟦ a ⟧) ⟨ + (⟦ a ⟧ +B 0#) *B (⟦ b ⟧ +B β *B eval-p p) + ≈⟨ B.*-congʳ (B.+-congˡ (B.zeroʳ β)) ⟨ + (⟦ a ⟧ +B β *B 0#) *B (⟦ b ⟧ +B β *B eval-p p) + ∎ + + eval-p-shift : (p : Poly m) → eval-p (A0# ∷ p) ≈B β *B eval-p p + eval-p-shift p = begin + ⟦ A0# ⟧ +B β *B eval-p p + ≈⟨ B.+-congʳ (MonoidHomomorphism.ε-homo + (RingHomomorphism.+-monoidHomomorphism f)) ⟩ + 0# +B β *B eval-p p + ≈⟨ B.+-identityˡ (β *B eval-p p) ⟩ + β *B eval-p p + ∎ + + + eval-p-*-homomorphic : (p : Poly m) → (q : Poly n) → eval-p (p *P q) ≈B eval-p p *B eval-p q + eval-p-*-homomorphic [] q = begin + eval-p ([] *P q) + ≈⟨ eval-p-cong (P-zeroˡ q) ⟩ + eval-p [] + ≈⟨ B.zeroˡ (eval-p q) ⟨ + eval-p [] *B eval-p q + ∎ + eval-p-*-homomorphic (a ∷ p) [] = begin + eval-p ((a ∷ p) *P []) + ≈⟨ eval-p-cong (P-zeroʳ (a ∷ p)) ⟩ + eval-p [] + ≈⟨ B.zeroʳ (eval-p (a ∷ p)) ⟨ + eval-p (a ∷ p) *B eval-p [] + ∎ + eval-p-*-homomorphic {suc m} {suc n} (a ∷ p) (b ∷ q) = begin + eval-p ((a ∷ p) *P (b ∷ q)) + ≈⟨ eval-p-cong (cast-p≈p (cast-lem (suc n) (m))) ⟩ + eval-p (a ·P (b ∷ q) +P p *P (A0# ∷ b ∷ q)) + ≈⟨ eval-p-+-homomorphic (a ·P (b ∷ q)) (p *P (A0# ∷ b ∷ q)) ⟩ + eval-p (a ·P (b ∷ q)) +B eval-p (p *P (A0# ∷ b ∷ q)) + ≈⟨ B.+-congʳ (eval-p-scale a (b ∷ q)) ⟩ + (eval-p (a ∷ []) *B eval-p (b ∷ q)) +B eval-p (p *P (A0# ∷ b ∷ q)) + ≈⟨ B.+-congˡ (eval-p-*-homomorphic p (A0# ∷ b ∷ q)) ⟩ + (eval-p (a ∷ []) *B eval-p (b ∷ q)) +B (eval-p p) *B eval-p (A0# ∷ b ∷ q) + ≈⟨ B.+-congˡ (B.*-congˡ (eval-p-shift (b ∷ q))) ⟩ + (eval-p (a ∷ []) *B eval-p (b ∷ q)) +B (eval-p p) *B (β *B eval-p (b ∷ q)) + ≈⟨ B.+-congʳ (B.*-congʳ (B.+-congˡ (B.zeroʳ β))) ⟩ + (⟦ a ⟧ +B 0#) *B (⟦ b ⟧ +B β *B eval-p q) +B eval-p p *B (β *B (⟦ b ⟧ +B β *B eval-p q)) + ≈⟨ B.+-congʳ (B.*-congʳ (B.+-identityʳ ⟦ a ⟧)) ⟩ + (⟦ a ⟧ *B (⟦ b ⟧ +B β *B eval-p q) +B eval-p p *B (β *B (⟦ b ⟧ +B β *B eval-p q))) + ≈⟨ B.+-congˡ (B.*-assoc (eval-p p) β (⟦ b ⟧ +B β *B eval-p q)) ⟨ + (⟦ a ⟧ *B (⟦ b ⟧ +B β *B eval-p q) +B (eval-p p *B β) *B (⟦ b ⟧ +B β *B eval-p q)) + ≈⟨ B.+-congˡ (B.*-congʳ (B.*-comm (eval-p p) β)) ⟩ + (⟦ a ⟧ *B (⟦ b ⟧ +B β *B eval-p q) +B (β *B eval-p p) *B (⟦ b ⟧ +B β *B eval-p q)) + ≈⟨ proj₂ distrib (⟦ b ⟧ +B β *B eval-p q) ⟦ a ⟧ (β *B eval-p p) ⟨ + (⟦ a ⟧ +B β *B eval-p p) *B (⟦ b ⟧ +B β *B eval-p q) + ∎ + + eval-*-homomorphic : (P : Polynomial) → (Q : Polynomial) → eval (P * Q) ≈B eval P *B eval Q + eval-*-homomorphic (m , p) (n , q) = begin + eval ((m , p) * (n , q)) + ≈⟨ eval-equiv ((p *P q)) ⟨ + eval-p (p *P q) + ≈⟨ eval-p-*-homomorphic p q ⟩ + (eval-p p *B eval-p q) + ≈⟨ B.*-cong (eval-equiv p) (eval-equiv q) ⟩ + eval (m , p) *B eval (n , q) + ∎ + + eval-p-inverse-homomorphic : (p : Poly m) → eval-p (-P p) ≈B -B (eval-p p) + eval-p-inverse-homomorphic [] = B.sym (ε⁻¹≈ε B.+-group) + eval-p-inverse-homomorphic (a ∷ p) = begin + eval-p (-P (a ∷ p)) + ≈⟨ B.+-congˡ (B.*-congˡ (eval-p-inverse-homomorphic p)) ⟩ + ⟦ -A a ⟧ +B β *B (-B (eval-p p)) + ≈⟨ B.+-congˡ step1 ⟩ + ⟦ -A a ⟧ +B -B (β *B eval-p p) + ≈⟨ B.+-congʳ (RingHomomorphism.-‿homo f a) ⟩ + -B ⟦ a ⟧ +B -B (β *B eval-p p) + ≈⟨ B.+-comm (-B (β *B eval-p p)) (-B ⟦ a ⟧) ⟨ + -B (β *B eval-p p) +B -B ⟦ a ⟧ + ≈⟨ ⁻¹-anti-homo-∙ B.+-group ⟦ a ⟧ (β *B eval-p p) ⟨ + -B eval-p (a ∷ p) + ∎ + where + step1 = begin + β *B -B eval-p p + ≈⟨ B.*-congˡ (-1*x≈-x B.ring (eval-p p)) ⟨ + β *B (-B 1# *B eval-p p) + ≈⟨ B.*-assoc β (-B 1#) (eval-p p) ⟨ + (β *B -B 1#) *B eval-p p + ≈⟨ B.*-congʳ (B.*-comm (-B 1#) β) ⟨ + (-B 1# *B β) *B eval-p p + ≈⟨ B.*-assoc (-B 1#) β (eval-p p) ⟩ + (-B 1#) *B (β *B eval-p p) + ≈⟨ -1*x≈-x B.ring (β *B eval-p p) ⟩ + -B (β *B eval-p p) + ∎ + + + + + eval-inverse-homomorphic : (P : Polynomial) → eval (- P) ≈B -B (eval P) + eval-inverse-homomorphic (m , p) = begin + eval (- (m , p)) + ≈⟨ eval-equiv (-P p) ⟨ + eval-p (-P p) + ≈⟨ eval-p-inverse-homomorphic p ⟩ + -B eval-p p + ≈⟨ B.-‿cong (eval-equiv p) ⟩ + -B eval (m , p) + ∎ + + eval-+-isMagmaHomomorphism : IsMagmaHomomorphism (CommutativeRing.+-rawMagma +-*-commutativeRing) + (CommutativeRing.+-rawMagma B) eval + eval-+-isMagmaHomomorphism = record + { isRelHomomorphism = record { cong = eval-cong } + ; homo = eval-+-homomorphic + } + + eval-+-isMonoidHomomorphism : IsMonoidHomomorphism (CommutativeRing.+-rawMonoid +-*-commutativeRing) + (CommutativeRing.+-rawMonoid B) eval + eval-+-isMonoidHomomorphism = record + { isMagmaHomomorphism = eval-+-isMagmaHomomorphism + ; ε-homo = B.refl + } + + eval-isNearSemiringHomomorphism : IsNearSemiringHomomorphism (SemiringWithoutAnnihilatingZero.rawNearSemiring + (Semiring.semiringWithoutAnnihilatingZero (CommutativeRing.semiring +-*-commutativeRing))) + (SemiringWithoutAnnihilatingZero.rawNearSemiring + (Semiring.semiringWithoutAnnihilatingZero (CommutativeRing.semiring B))) eval + eval-isNearSemiringHomomorphism = record + { +-isMonoidHomomorphism = eval-+-isMonoidHomomorphism + ; *-homo = eval-*-homomorphic } + + eval-isSemiringHomomorphism : IsSemiringHomomorphism (CommutativeSemiring.rawSemiring + (CommutativeRing.commutativeSemiring +-*-commutativeRing)) + (CommutativeSemiring.rawSemiring (CommutativeRing.commutativeSemiring B)) eval + eval-isSemiringHomomorphism = record + { isNearSemiringHomomorphism = eval-isNearSemiringHomomorphism + ; 1#-homo = eval-1#-homomorphic } + + eval-isRingHomomorphism : IsRingHomomorphism (CommutativeRing.rawRing +-*-commutativeRing) (CommutativeRing.rawRing B) eval + eval-isRingHomomorphism = record + { isSemiringHomomorphism = eval-isSemiringHomomorphism + ; -‿homo = eval-inverse-homomorphic + } + + + + +{- + eval-cong : P ≈ Q → eval P ≈B eval Q + eval-cong {P = 0 , []} {Q = ℕ.zero , []} P≈Q = B.refl + eval-cong {P = suc n , (a ∷ p)} {Q = ℕ.zero , []} P≈Q = begin + eval (suc n , (a ∷ p)) + ≈⟨ B.+-congʳ (S.IsRelHomomorphism.cong + (RingHomomorphism.isRelHomomorphism f) (head (≈0⇒IsZero P≈Q))) ⟩ + ⟦ A0# ⟧ +B β *B eval (n , p) + ≈⟨ B.+-congˡ (B.*-congˡ (eval-cong {P = n , p} {Q = ℕ.zero , []} + (IsZero⇒≈0 (tail (≈0⇒IsZero P≈Q))))) ⟩ + ⟦ A0# ⟧ +B β *B eval(ℕ.zero , []) + ≈⟨ B.+-congʳ (MonoidHomomorphism.ε-homo + (RingHomomorphism.+-monoidHomomorphism f)) ⟩ + (0# +B β *B eval(ℕ.zero , [])) + ≈⟨ B.+-congˡ (B.zeroʳ β) ⟩ + (0# +B 0#) + ≈⟨ B.+-identityʳ 0# ⟩ + eval (ℕ.zero , []) + ∎ + eval-cong {P = ℕ.zero , []} {Q = suc n , (a ∷ q)} P≈Q = begin + eval (ℕ.zero , []) + ≈⟨ B.zeroʳ β ⟨ + β *B eval (ℕ.zero , []) + ≈⟨ B.+-identityˡ (β *B eval (ℕ.zero , [])) ⟨ + 0# +B β *B eval (ℕ.zero , []) + ≈⟨ B.+-congʳ ( (MonoidHomomorphism.ε-homo + (RingHomomorphism.+-monoidHomomorphism f))) ⟨ + ⟦ A0# ⟧ +B β *B eval (ℕ.zero , []) + ≈⟨ B.+-congˡ (B.*-congˡ (eval-cong {P = 0 , []} {Q = n , q} + (P-sym (IsZero⇒≈0 (tail (≈0⇒IsZero (P-sym P≈Q))))))) ⟩ + ⟦ A0# ⟧ +B β *B eval (n , q) + ≈⟨ B.+-congʳ ((S.IsRelHomomorphism.cong (RingHomomorphism.isRelHomomorphism f) + (head (≈0⇒IsZero (P-sym P≈Q))))) ⟨ + eval (suc n , (a ∷ q)) + ∎ + eval-cong {P = suc m , (a ∷ p)} {Q = suc n , (b ∷ q)} (cons a≈b p≈q) + = B.+-cong (S.IsRelHomomorphism.cong (RingHomomorphism.isRelHomomorphism f) a≈b) + (B.*-congˡ (eval-cong p≈q)) + -} + + +{-eval-+-homomorphic (0 , []) (n , q) = begin + eval ((ℕ.zero , []) + (n , q)) + ≈⟨ eval-cong (P.+-identityˡ ((n , q))) ⟩ + eval (n , q) + ≈⟨ B.+-identityˡ (eval (n , q)) ⟨ + eval (ℕ.zero , []) +B eval (n , q) + ∎ + eval-+-homomorphic (suc m , (a ∷ p)) (0 , []) = B.sym (B.+-identityʳ (eval (suc m , (a ∷ p)))) + eval-+-homomorphic (suc m , (a ∷ p)) (suc n , (b ∷ q)) = begin + eval ((suc m , (a ∷ p)) + (suc n , (b ∷ q))) + ≈⟨ B.+-congˡ (B.*-congˡ (eval-+-homomorphic (m , p) (n , q))) ⟩ + ⟦ a +A b ⟧ +B (β *B (eval (m , p) +B eval (n , q))) + ≈⟨ B.+-congˡ (proj₁ distrib β (eval (m , p)) (eval (n , q))) ⟩ + ⟦ a +A b ⟧ +B (β *B eval (m , p) +B β *B eval (n , q)) + ≈⟨ B.+-congʳ (IsMagmaHomomorphism.homo (RingHomomorphism.+-isMagmaHomomorphism f) a b) ⟩ + ⟦ a ⟧ +B ⟦ b ⟧ +B (β *B eval (m , p) +B β *B eval (n , q)) + ≈⟨ B.+-assoc ( ⟦ a ⟧ +B ⟦ b ⟧) (β *B eval (m , p)) (β *B eval (n , q)) ⟨ + ⟦ a ⟧ +B ⟦ b ⟧ +B β *B eval (m , p) +B β *B eval (n , q) + ≈⟨ B.+-congʳ (B.+-assoc ⟦ a ⟧ ⟦ b ⟧ (β *B eval (m , p))) ⟩ + ⟦ a ⟧ +B (⟦ b ⟧ +B β *B eval (m , p)) +B β *B eval (n , q) + ≈⟨ (B.+-assoc (⟦ a ⟧) (⟦ b ⟧ +B β *B eval (m , p)) (β *B eval (n , q))) ⟩ + ⟦ a ⟧ +B ( ⟦ b ⟧ +B β *B eval (m , p) +B (β *B eval (n , q))) + ≈⟨ B.+-congˡ (B.+-congʳ ((B.+-comm (β *B eval (m , p)) ⟦ b ⟧))) ⟨ + ⟦ a ⟧ +B ((β *B eval (m , p)) +B ⟦ b ⟧ +B (β *B eval (n , q))) + ≈⟨ B.+-congˡ (B.+-assoc (β *B eval (m , p)) ⟦ b ⟧ (β *B eval (n , q))) ⟩ + ⟦ a ⟧ +B (β *B eval (m , p) +B eval (suc n , (b ∷ q))) + ≈⟨ B.+-assoc ⟦ a ⟧ (β *B eval (m , p)) (eval (suc n , (b ∷ q))) ⟨ + eval (suc m , (a ∷ p)) +B eval (suc n , (b ∷ q)) + ∎ + -} + + + +{- eval-1#-homomorphic = begin + eval (1 , (A1# ∷ [])) + ≈⟨ B.+-cong (RingHomomorphism.1#-homo f) (B.zeroʳ β) ⟩ + 1# +B 0# + ≈⟨ B.+-identityʳ (1#) ⟩ + 1# + ∎ + +-} + + +{-eval-inverse-homomorphic (0 , []) = B.sym (ε⁻¹≈ε B.+-group) + eval-inverse-homomorphic (suc m , (a ∷ p)) = begin + eval (- (suc m , (a ∷ p))) + ≈⟨ B.+-congˡ (B.*-congˡ (eval-inverse-homomorphic (m , p))) ⟩ + ⟦ -A a ⟧ +B β *B (-B (eval (m , p))) + ≈⟨ B.+-congˡ step1 ⟩ + ⟦ -A a ⟧ +B -B (β *B eval (m , p)) + ≈⟨ B.+-congʳ (RingHomomorphism.-‿homo f a) ⟩ + -B ⟦ a ⟧ +B -B (β *B eval (m , p)) + ≈⟨ B.+-comm (-B (β *B eval (m , p))) (-B ⟦ a ⟧) ⟨ + -B (β *B eval (m , p)) +B (-B ⟦ a ⟧) + ≈⟨ ⁻¹-anti-homo-∙ B.+-group ⟦ a ⟧ (β *B eval (m , p)) ⟨ + (-B eval (suc m , (a ∷ p))) + ∎ + where + step1 = begin + β *B (-B (eval (m , p))) + ≈⟨ B.*-congˡ (-1*x≈-x B.ring (eval (m , p))) ⟨ + β *B (-B 1# *B eval (m , p)) + ≈⟨ B.*-assoc β (-B 1#) (eval (m , p)) ⟨ + (β *B -B 1#) *B eval (m , p) + ≈⟨ B.*-congʳ (B.*-comm (-B 1#) β) ⟨ + (-B 1# *B β) *B eval (m , p) + ≈⟨ B.*-assoc (-B 1#) β (eval (m , p)) ⟩ + (-B 1#) *B (β *B eval (m , p)) + ≈⟨ -1*x≈-x B.ring (β *B eval (m , p)) ⟩ + -B (β *B eval (m , p)) + ∎ + -} diff --git a/src/Algebra/Polynomial/Poly/Base.agda b/src/Algebra/Polynomial/Poly/Base.agda new file mode 100644 index 0000000000..b150951622 --- /dev/null +++ b/src/Algebra/Polynomial/Poly/Base.agda @@ -0,0 +1,142 @@ +open import Algebra.Bundles using (Semiring) + +module Algebra.Polynomial.Poly.Base + {ℓ₁ ℓ₂} (SR : Semiring ℓ₁ ℓ₂) + where + +open import Data.Nat.Base as ℕ using (ℕ; suc; pred; _⊔_) +import Data.Nat.Properties as ℕ +open import Data.Vec.Base as Vec using (Vec; []; _∷_) +open import Data.Vec.Relation.Unary.All using (All ; []; _∷_) +import Level as L +open import Relation.Binary.PropositionalEquality.Core using (cong) +open import Relation.Binary.PropositionalEquality + using (_≡_; cong; module ≡-Reasoning) + +module SR = Semiring SR +open SR + renaming + ( Carrier to A + ; _≈_ to _≈A_ + ; _+_ to _+A_ + ; _*_ to _*A_ + ) + using (0#; 1#) + +infixl 7 _*_ +infix 7 _·_ +infixl 6 _+_ +infix 4 _≈_ + +private + variable + m n k l : ℕ + a b c d : A + +-- Polynomial of degree most n is represented as a vector of length n + 1 +-- a₀ ∷ a₁ ∷ ⋯ ∷ aₙ ∷ [] represents the polynomial a₀ + a₁x + ⋯ + aₙxⁿ + +Poly : ℕ → Set ℓ₁ +Poly n = Vec A n + +private + variable + p : Poly m + q : Poly n + r : Poly k + s : Poly l + +zeros : (n : ℕ) → Poly n +zeros n = Vec.replicate n (0#) + +-- Scaling a polynomial by a +_·_ : A → Poly n → Poly n +a · p = Vec.map (a *A_) p + +-- Multiply a polynomial by a factor of x +shift : Poly n → Poly (suc n) +shift p = 0# ∷ p + +IsZero : Poly n → Set (ℓ₁ L.⊔ ℓ₂) +IsZero = All (_≈A 0#) + +-- The representation of a polynomial is not unique +-- because we allow coefficients to be zero +-- We define an equivalence relation which takes this into account + +data _≈_ : (Poly m) → (Poly n) → Set (ℓ₁ L.⊔ ℓ₂) where + []≈ : (q : Poly n) → IsZero q → [] ≈ q + ≈[] : (p : Poly m) → IsZero p → p ≈ [] + cons : (a ≈A b) → (p ≈ q) → (a ∷ p) ≈ (b ∷ q) + +-- Properties of Polynomial Equality + +zeros-unique : IsZero p → IsZero q → p ≈ q +zeros-unique [] [] = []≈ [] [] +zeros-unique [] (a≈0 ∷ p≈0) = []≈ (_ ∷ _) (a≈0 ∷ p≈0) +zeros-unique (a≈0 ∷ p≈0) [] = ≈[] (_ ∷ _) (a≈0 ∷ p≈0) +zeros-unique (a≈0 ∷ p≈0) (b≈0 ∷ q≈0) + = cons (SR.trans a≈0 (SR.sym b≈0)) (zeros-unique p≈0 q≈0) + +IsZero-cong : IsZero p → p ≈ q → IsZero q +IsZero-cong [] ([]≈ q q≈0) = q≈0 +IsZero-cong [] (≈[] p p≈0) = p≈0 +IsZero-cong (a≈0 ∷ p≈0) (≈[] a∷p a∷p≈0) = [] +IsZero-cong (a≈0 ∷ p≈0) (cons a≈b p≈q) + = (SR.trans (SR.sym a≈b) a≈0) ∷ IsZero-cong p≈0 p≈q + +-- _≈_ is an equivalence relation + +refl : p ≈ p +refl {p = []} = []≈ [] [] +refl {p = a ∷ p} = cons SR.refl refl + +sym : p ≈ q → q ≈ p +sym ([]≈ q q≈0) = ≈[] q q≈0 +sym (≈[] p p≈0) = []≈ p p≈0 +sym (cons a≈b p≈q) = cons (SR.sym a≈b) (sym p≈q) + +trans : p ≈ q → q ≈ r → p ≈ r +trans {r = r} ([]≈ q q≈0) q≈r = []≈ r (IsZero-cong q≈0 q≈r) +trans (≈[] p p≈0) q≈r = zeros-unique p≈0 (IsZero-cong [] q≈r) +trans (cons a≈b p≈q) (≈[] q q≈0) + = ≈[] _ (IsZero-cong q≈0 (sym (cons a≈b p≈q))) +trans (cons a≈b p≈q) (cons b≈c q≈r) + = cons (SR.trans a≈b b≈c) (trans p≈q q≈r) + +consˡ : (a ≈A b) → (a ∷ p) ≈ (b ∷ p) +consˡ a≈b = cons a≈b refl + +consʳ : p ≈ q → (a ∷ p) ≈ (a ∷ q) +consʳ = cons SR.refl + +---------------------------------------------------------------- +-- Operations + +-- Addition +_+_ : Poly m → Poly n → Poly (m ⊔ n) +[] + [] = [] +[] + (a ∷ p) = a ∷ p +(a ∷ p) + [] = a ∷ p +(a ∷ p) + (b ∷ q) = (a +A b) ∷ (p + q) + +private + pred[n+sucm]≡n+m : ∀ n → ∀ m → pred (n ℕ.+ suc m) ≡ n ℕ.+ m + pred[n+sucm]≡n+m n m = begin + pred (n ℕ.+ suc m) ≡⟨ cong pred (ℕ.+-comm n (suc m)) ⟩ + pred (suc m ℕ.+ n) ≡⟨ ℕ.+-comm m n ⟩ + n ℕ.+ m ∎ + where open ≡-Reasoning + +cast-lem : ∀ m → ∀ n → m ⊔ pred (n ℕ.+ suc m) ≡ (n ℕ.+ m) +cast-lem m n = begin + m ⊔ pred (n ℕ.+ suc m) ≡⟨ cong (m ⊔_) (pred[n+sucm]≡n+m n m) ⟩ + m ⊔ (n ℕ.+ m) ≡⟨ ℕ.m≤n⇒m⊔n≡n (ℕ.m≤n+m m n) ⟩ + n ℕ.+ m ∎ + where open ≡-Reasoning + +-- Multiplication +_*_ : Poly n → Poly m → Poly (pred (n ℕ.+ m)) +_*_ {m = m} [] p = zeros (pred m) +_*_ {suc n} {m} (a ∷ p) q = Vec.cast (cast-lem m n) ((a · q) + (p * (0# ∷ q))) + diff --git a/src/Algebra/Polynomial/Poly/Base1.agda b/src/Algebra/Polynomial/Poly/Base1.agda new file mode 100644 index 0000000000..814f134482 --- /dev/null +++ b/src/Algebra/Polynomial/Poly/Base1.agda @@ -0,0 +1,148 @@ +open import Algebra.Bundles using (Ring) + +module Algebra.Polynomial.Poly.Base1 + {ℓ₁ ℓ₂} (R : Ring ℓ₁ ℓ₂) + where + +open import Data.Nat.Base as ℕ using (ℕ; suc; pred; _⊔_) +import Data.Nat.Properties as ℕ +open import Data.Vec.Base as Vec using (Vec; []; _∷_) +open import Data.Vec.Relation.Unary.All using (All ; []; _∷_) +import Level as L +open import Relation.Binary.PropositionalEquality.Core using (cong) +open import Relation.Binary.PropositionalEquality + using (_≡_; cong; module ≡-Reasoning) + +module R = Ring R +open R + renaming + ( Carrier to A + ; _≈_ to _≈A_ + ; _+_ to _+A_ + ; _*_ to _*A_ + ; -_ to -A_) + using (0#; 1#) + +infix 8 -_ +infixl 7 _*_ +infix 7 _·_ +infixl 6 _+_ +infix 4 _≈_ + +private + variable + m n k l : ℕ + a b c d : A + +-- Polynomial of degree most n is represented as a vector of length n + 1 +-- a₀ ∷ a₁ ∷ ⋯ ∷ aₙ ∷ [] represents the polynomial a₀ + a₁x + ⋯ + aₙxⁿ + +Poly : ℕ → Set ℓ₁ +Poly n = Vec A n + +private + variable + p : Poly m + q : Poly n + r : Poly k + s : Poly l + +zeros : (n : ℕ) → Poly n +zeros n = Vec.replicate n (0#) + +-- Scaling a polynomial by a +_·_ : A → Poly n → Poly n +a · p = Vec.map (a *A_) p + +-- Multiply a polynomial by a factor of x +shift : Poly n → Poly (suc n) +shift p = 0# ∷ p + +IsZero : Poly n → Set (ℓ₁ L.⊔ ℓ₂) +IsZero = All (_≈A 0#) + + +-- The additive inverse +-_ : Poly n → Poly n +- p = Vec.map -A_ p + +-- The representation of a polynomial is not unique +-- because we allow coefficients to be zero +-- We define an equivalence relation which takes this into account + +data _≈_ : (Poly m) → (Poly n) → Set (ℓ₁ L.⊔ ℓ₂) where + []≈ : (q : Poly n) → IsZero q → [] ≈ q + ≈[] : (p : Poly m) → IsZero p → p ≈ [] + cons : (a ≈A b) → (p ≈ q) → (a ∷ p) ≈ (b ∷ q) + +-- Properties of Polynomial Equality + +zeros-unique : IsZero p → IsZero q → p ≈ q +zeros-unique [] [] = []≈ [] [] +zeros-unique [] (a≈0 ∷ p≈0) = []≈ (_ ∷ _) (a≈0 ∷ p≈0) +zeros-unique (a≈0 ∷ p≈0) [] = ≈[] (_ ∷ _) (a≈0 ∷ p≈0) +zeros-unique (a≈0 ∷ p≈0) (b≈0 ∷ q≈0) + = cons (R.trans a≈0 (R.sym b≈0)) (zeros-unique p≈0 q≈0) + +IsZero-cong : IsZero p → p ≈ q → IsZero q +IsZero-cong [] ([]≈ q q≈0) = q≈0 +IsZero-cong [] (≈[] p p≈0) = p≈0 +IsZero-cong (a≈0 ∷ p≈0) (≈[] a∷p a∷p≈0) = [] +IsZero-cong (a≈0 ∷ p≈0) (cons a≈b p≈q) + = (R.trans (R.sym a≈b) a≈0) ∷ IsZero-cong p≈0 p≈q + +-- _≈_ is an equivalence relation + +refl : p ≈ p +refl {p = []} = []≈ [] [] +refl {p = a ∷ p} = cons R.refl refl + +sym : p ≈ q → q ≈ p +sym ([]≈ q q≈0) = ≈[] q q≈0 +sym (≈[] p p≈0) = []≈ p p≈0 +sym (cons a≈b p≈q) = cons (R.sym a≈b) (sym p≈q) + +trans : p ≈ q → q ≈ r → p ≈ r +trans {r = r} ([]≈ q q≈0) q≈r = []≈ r (IsZero-cong q≈0 q≈r) +trans (≈[] p p≈0) q≈r = zeros-unique p≈0 (IsZero-cong [] q≈r) +trans (cons a≈b p≈q) (≈[] q q≈0) + = ≈[] _ (IsZero-cong q≈0 (sym (cons a≈b p≈q))) +trans (cons a≈b p≈q) (cons b≈c q≈r) + = cons (R.trans a≈b b≈c) (trans p≈q q≈r) + +consˡ : (a ≈A b) → (a ∷ p) ≈ (b ∷ p) +consˡ a≈b = cons a≈b refl + +consʳ : p ≈ q → (a ∷ p) ≈ (a ∷ q) +consʳ = cons R.refl + +---------------------------------------------------------------- +-- Operations + +-- Addition +_+_ : Poly m → Poly n → Poly (m ⊔ n) +[] + [] = [] +[] + (a ∷ p) = a ∷ p +(a ∷ p) + [] = a ∷ p +(a ∷ p) + (b ∷ q) = (a +A b) ∷ (p + q) + +private + pred[n+sucm]≡n+m : ∀ n → ∀ m → pred (n ℕ.+ suc m) ≡ n ℕ.+ m + pred[n+sucm]≡n+m n m = begin + pred (n ℕ.+ suc m) ≡⟨ cong pred (ℕ.+-comm n (suc m)) ⟩ + pred (suc m ℕ.+ n) ≡⟨ ℕ.+-comm m n ⟩ + n ℕ.+ m ∎ + where open ≡-Reasoning + +cast-lem : ∀ m → ∀ n → m ⊔ pred (n ℕ.+ suc m) ≡ (n ℕ.+ m) +cast-lem m n = begin + m ⊔ pred (n ℕ.+ suc m) ≡⟨ cong (m ⊔_) (pred[n+sucm]≡n+m n m) ⟩ + m ⊔ (n ℕ.+ m) ≡⟨ ℕ.m≤n⇒m⊔n≡n (ℕ.m≤n+m m n) ⟩ + n ℕ.+ m ∎ + where open ≡-Reasoning + +-- Multiplication +_*_ : Poly n → Poly m → Poly (pred (n ℕ.+ m)) +_*_ {m = m} [] p = zeros (pred m) +_*_ {suc n} {m} (a ∷ p) q = Vec.cast (cast-lem m n) ((a · q) + (p * (0# ∷ q))) + diff --git a/src/Algebra/Polynomial/Poly/Base2.agda b/src/Algebra/Polynomial/Poly/Base2.agda new file mode 100644 index 0000000000..aac53f2489 --- /dev/null +++ b/src/Algebra/Polynomial/Poly/Base2.agda @@ -0,0 +1,149 @@ +open import Algebra.Bundles using (CommutativeRing) + +module Algebra.Polynomial.Poly.Base2 + {ℓ₁ ℓ₂} (R : CommutativeRing ℓ₁ ℓ₂) + where + +open import Data.Nat.Base as ℕ using (ℕ; suc; pred; _⊔_) +import Data.Nat.Properties as ℕ +open import Data.Vec.Base as Vec using (Vec; []; _∷_) +open import Data.Vec.Relation.Unary.All using (All ; []; _∷_) +import Level as L +open import Relation.Binary.PropositionalEquality.Core using (cong) +open import Relation.Binary.PropositionalEquality + using (_≡_; cong; module ≡-Reasoning) + +infix 8 -_ +infixl 7 _*_ +infix 7 _·_ +infixl 6 _+_ +infix 4 _≈_ + +module CR = CommutativeRing R +open CR + renaming + ( Carrier to A + ; _≈_ to _≈A_ + ; _+_ to _+A_ + ; _*_ to _*A_ + ; -_ to -A_) + using (0#; 1#) + +private + variable + m n k l : ℕ + a b c d : A + +-- Polynomial of degree most n is represented as a vector of length n + 1 +-- a₀ ∷ a₁ ∷ ⋯ ∷ aₙ ∷ [] represents the polynomial a₀ + a₁x + ⋯ + aₙxⁿ + +Poly : ℕ → Set ℓ₁ +Poly n = Vec A n + +private + variable + p : Poly m + q : Poly n + r : Poly k + s : Poly l + +zeros : (n : ℕ) → Poly n +zeros n = Vec.replicate n (0#) + +-- Scaling a polynomial by a +_·_ : A → Poly n → Poly n +a · p = Vec.map (a *A_) p + +-- Multiply a polynomial by a factor of x +shift : Poly n → Poly (suc n) +shift p = 0# ∷ p + +IsZero : Poly n → Set (ℓ₁ L.⊔ ℓ₂) +IsZero = All (_≈A 0#) + +-- The additive inverse +-_ : Poly n → Poly n +- p = Vec.map -A_ p + +------------------------------------------------------------------ +-- The representation of a polynomial is not unique +-- because we allow coefficients to be zero +-- We define an equivalence relation which takes this into account + +data _≈_ : (Poly m) → (Poly n) → Set (ℓ₁ L.⊔ ℓ₂) where + []≈ : (q : Poly n) → IsZero q → [] ≈ q + ≈[] : (p : Poly m) → IsZero p → p ≈ [] + cons : (a ≈A b) → (p ≈ q) → (a ∷ p) ≈ (b ∷ q) + +------------------------------------------------------------------ +-- Properties of Polynomial Equality + +zeros-unique : IsZero p → IsZero q → p ≈ q +zeros-unique [] [] = []≈ [] [] +zeros-unique [] (a≈0 ∷ p≈0) = []≈ (_ ∷ _) (a≈0 ∷ p≈0) +zeros-unique (a≈0 ∷ p≈0) [] = ≈[] (_ ∷ _) (a≈0 ∷ p≈0) +zeros-unique (a≈0 ∷ p≈0) (b≈0 ∷ q≈0) + = cons (CR.trans a≈0 (CR.sym b≈0)) (zeros-unique p≈0 q≈0) + +IsZero-cong : IsZero p → p ≈ q → IsZero q +IsZero-cong [] ([]≈ q q≈0) = q≈0 +IsZero-cong [] (≈[] p p≈0) = p≈0 +IsZero-cong (a≈0 ∷ p≈0) (≈[] a∷p a∷p≈0) = [] +IsZero-cong (a≈0 ∷ p≈0) (cons a≈b p≈q) + = (CR.trans (CR.sym a≈b) a≈0) ∷ IsZero-cong p≈0 p≈q + +------------------------------------------------------------------ +-- _≈_ is an equivalence relation + +refl : p ≈ p +refl {p = []} = []≈ [] [] +refl {p = a ∷ p} = cons CR.refl refl + +sym : p ≈ q → q ≈ p +sym ([]≈ q q≈0) = ≈[] q q≈0 +sym (≈[] p p≈0) = []≈ p p≈0 +sym (cons a≈b p≈q) = cons (CR.sym a≈b) (sym p≈q) + +trans : p ≈ q → q ≈ r → p ≈ r +trans {r = r} ([]≈ q q≈0) q≈r = []≈ r (IsZero-cong q≈0 q≈r) +trans (≈[] p p≈0) q≈r = zeros-unique p≈0 (IsZero-cong [] q≈r) +trans (cons a≈b p≈q) (≈[] q q≈0) + = ≈[] _ (IsZero-cong q≈0 (sym (cons a≈b p≈q))) +trans (cons a≈b p≈q) (cons b≈c q≈r) + = cons (CR.trans a≈b b≈c) (trans p≈q q≈r) + +consˡ : (a ≈A b) → (a ∷ p) ≈ (b ∷ p) +consˡ a≈b = cons a≈b refl + +consʳ : p ≈ q → (a ∷ p) ≈ (a ∷ q) +consʳ = cons CR.refl + +---------------------------------------------------------------- +-- Operations + +-- Addition +_+_ : Poly m → Poly n → Poly (m ⊔ n) +[] + [] = [] +[] + (a ∷ p) = a ∷ p +(a ∷ p) + [] = a ∷ p +(a ∷ p) + (b ∷ q) = (a +A b) ∷ (p + q) + +private + pred[n+sucm]≡n+m : ∀ n → ∀ m → pred (n ℕ.+ suc m) ≡ n ℕ.+ m + pred[n+sucm]≡n+m n m = begin + pred (n ℕ.+ suc m) ≡⟨ cong pred (ℕ.+-comm n (suc m)) ⟩ + pred (suc m ℕ.+ n) ≡⟨ ℕ.+-comm m n ⟩ + n ℕ.+ m ∎ + where open ≡-Reasoning + +cast-lem : ∀ m → ∀ n → m ⊔ pred (n ℕ.+ suc m) ≡ (n ℕ.+ m) +cast-lem m n = begin + m ⊔ pred (n ℕ.+ suc m) ≡⟨ cong (m ⊔_) (pred[n+sucm]≡n+m n m) ⟩ + m ⊔ (n ℕ.+ m) ≡⟨ ℕ.m≤n⇒m⊔n≡n (ℕ.m≤n+m m n) ⟩ + n ℕ.+ m ∎ + where open ≡-Reasoning + +-- Multiplication +_*_ : Poly n → Poly m → Poly (pred (n ℕ.+ m)) +_*_ {m = m} [] p = zeros (pred m) +_*_ {suc n} {m} (a ∷ p) q = Vec.cast (cast-lem m n) ((a · q) + (p * (0# ∷ q))) diff --git a/src/Algebra/Polynomial/Poly/Properties.agda b/src/Algebra/Polynomial/Poly/Properties.agda new file mode 100644 index 0000000000..ff614789c9 --- /dev/null +++ b/src/Algebra/Polynomial/Poly/Properties.agda @@ -0,0 +1,609 @@ +open import Algebra.Bundles using (Semiring) + +module Algebra.Polynomial.Poly.Properties + {ℓ₁ ℓ₂} (SR : Semiring ℓ₁ ℓ₂) + where + +open import Algebra.Polynomial.Poly.Base SR as P + using ( Poly; _+_ ; _*_ ; _·_ ; shift; _≈_; refl; trans; sym; zeros + ; IsZero; []≈ ; ≈[]; cons; zeros-unique; consˡ; consʳ; cast-lem) +open import Data.Nat.Base as ℕ using (ℕ; suc; pred; _⊔_) +import Data.Nat.Properties as ℕ +open import Data.Vec.Base as Vec using (Vec; []; _∷_) +open import Data.Vec.Relation.Unary.All using (All ; []; _∷_; head; tail) +import Level as L +open import Relation.Binary +open import Relation.Binary.PropositionalEquality as Eq + using (_≡_; module ≡-Reasoning) +open import Relation.Binary.PropositionalEquality.Core using (cong) + +module SR = Semiring SR +open SR + renaming + ( Carrier to A + ; _≈_ to _≈A_ + ; _+_ to _+A_ + ; _*_ to _*A_ + ) + using (0#; 1#) + +private + variable + m n k l : ℕ + a b c d : A + p : Poly m + q : Poly n + r : Poly k + s : Poly l + +--------------------------------------------------------------------- +-- Equational reasoning for Poly n and Poly m +-- where m is not necesarily the same as n +private + + infix 4 _IsRelatedTo_ + + data _IsRelatedTo_ (p : Poly m) (q : Poly n) : Set (ℓ₁ L.⊔ ℓ₂) where + relTo : (p≈q : p ≈ q) → p IsRelatedTo q + + start : _IsRelatedTo_ {m} {n} ⇒ _≈_ + start (relTo p≈q) = p≈q + + ∼-go : Trans (_≈_) (_IsRelatedTo_ {n} {k}) (_IsRelatedTo_ {m} {k}) + ∼-go p≈q (relTo q≈r) = relTo (trans p≈q q≈r) + + stop : Reflexive (_IsRelatedTo_ {m} {m}) + stop = relTo refl + + forward : (p : Poly m) → q IsRelatedTo r → p ≈ q → p IsRelatedTo r + forward p qRr p≈q = ∼-go p≈q qRr + + backward : (p : Poly m) → q IsRelatedTo r → q ≈ p → p IsRelatedTo r + backward p qRr q≈p = ∼-go (sym q≈p) qRr + + infix 1 begin_ + begin_ : p IsRelatedTo q → p ≈ q + begin_ = start + + infixr 2 step-∼-⟩ + step-∼-⟩ = forward + syntax step-∼-⟩ p qRr p≈q = p ≈⟨ p≈q ⟩ qRr + + infixr 2 step-∼-⟨ + step-∼-⟨ = backward + syntax step-∼-⟨ p qRr q≈p = p ≈⟨ q≈p ⟨ qRr + + infix 3 _∎ + _∎ : (p : Poly m) → p IsRelatedTo p + p ∎ = stop + +-- Properties of zero polynomial + +zerosIsZero : (n : ℕ) → IsZero (zeros n) +zerosIsZero 0 = [] +zerosIsZero (suc n) = SR.refl ∷ (zerosIsZero n) + +zerosm≈zerosn : zeros m ≈ zeros n +zerosm≈zerosn {m} {n} = zeros-unique (zerosIsZero m) (zerosIsZero n) + +≈0⇒IsZero : p ≈ zeros m → IsZero p +≈0⇒IsZero ([]≈ zeros zeros≈0) = [] +≈0⇒IsZero (≈[] p p≈0) = p≈0 +≈0⇒IsZero (cons a≈0 p≈0) = a≈0 ∷ ≈0⇒IsZero p≈0 + +IsZero⇒≈0 : IsZero p → p ≈ zeros m +IsZero⇒≈0 {m = m} p≈0 = zeros-unique p≈0 (zerosIsZero m) + +All-p≈0∧q≈0⇒p+q≈0 : IsZero p → IsZero q → IsZero (p + q) +All-p≈0∧q≈0⇒p+q≈0 {p = _} {q = _} [] [] = [] +All-p≈0∧q≈0⇒p+q≈0 {p = _} {q = _} [] (b≈0 ∷ q≈0) = b≈0 ∷ q≈0 +All-p≈0∧q≈0⇒p+q≈0 {p = _} {q = _} (a≈0 ∷ p≈0) [] = a≈0 ∷ p≈0 +All-p≈0∧q≈0⇒p+q≈0 {p = a ∷ p} {q = b ∷ q} (a≈0 ∷ p≈0) (b≈0 ∷ q≈0) + = SR.trans (SR.+-cong a≈0 b≈0) (SR.+-identityˡ 0#) ∷ All-p≈0∧q≈0⇒p+q≈0 p≈0 q≈0 + +----------------------------------------------------- +-- Properties of polynomial addition + ++-comm : (p : Poly m) → (q : Poly n) → p + q ≈ q + p ++-comm [] [] = refl ++-comm [] (a ∷ p) = refl ++-comm (a ∷ p) [] = refl ++-comm (a ∷ p) (b ∷ q) = cons (SR.+-comm a b) (+-comm p q) + ++-idʳ : (p : Poly n) → (q : Poly m) → IsZero q → p + q ≈ p ++-idʳ [] q [] = refl ++-idʳ (a ∷ p) q [] = refl ++-idʳ [] (a ∷ q) (a≈0 ∷ q≈0) = ≈[] (a ∷ q) (a≈0 ∷ q≈0) ++-idʳ (a ∷ p) (b ∷ q) (b≈0 ∷ q≈0) + = cons (SR.trans (SR.+-congˡ b≈0) (SR.+-identityʳ a)) (+-idʳ p q q≈0) + ++-idˡ : (p : Poly n) → (q : Poly m) → IsZero p → p + q ≈ q ++-idˡ p q p≈0 = begin + p + q ≈⟨ +-comm p q ⟩ + q + p ≈⟨ +-idʳ q p p≈0 ⟩ + q ∎ + ++-identityʳ : (p : Poly n) → p + (zeros m) ≈ p ++-identityʳ {m = m} p = +-idʳ p (zeros m) (zerosIsZero m) + ++-identityˡ : (p : Poly n) → (zeros m) + p ≈ p ++-identityˡ {m = m} p = +-idˡ (zeros m) p (zerosIsZero m) + ++-cong : p ≈ q → r ≈ s → p + r ≈ q + s ++-cong {p = _} {q = _} {r = r} {s = s} ([]≈ q q≈0) r≈s = begin + [] + r ≈⟨ +-identityˡ r ⟩ + r ≈⟨ r≈s ⟩ + s ≈⟨ +-idˡ q s q≈0 ⟨ + q + s ∎ ++-cong {p = _} {q = _} {r = r} {s = s} (≈[] p p≈0) r≈s = begin + p + r ≈⟨ +-idˡ p r p≈0 ⟩ + r ≈⟨ r≈s ⟩ + s ≈⟨ +-identityˡ s ⟨ + [] + s ∎ ++-cong {p = a ∷ p} {q = b ∷ q} {r = _} {s = s} (cons a≈b p≈q) ([]≈ s s≈0) = begin + a ∷ p ≈⟨ cons a≈b p≈q ⟩ + b ∷ q ≈⟨ +-idʳ (b ∷ q) s s≈0 ⟨ + (b ∷ q) + s ∎ ++-cong {p = a ∷ p} {q = b ∷ q} {r = r} {s = _} (cons a≈b p≈q) (≈[] r r≈0) = begin + (a ∷ p) + r ≈⟨ +-idʳ (a ∷ p) r r≈0 ⟩ + a ∷ p ≈⟨ cons a≈b p≈q ⟩ + b ∷ q ∎ ++-cong (cons a≈b p≈q) (cons c≈d r≈s) + = cons (SR.+-cong a≈b c≈d) (+-cong p≈q r≈s) + ++-congˡ : p ≈ q → p + r ≈ q + r ++-congˡ p≈q = +-cong p≈q refl + ++-congʳ : q ≈ r → p + q ≈ p + r ++-congʳ q≈r = +-cong refl q≈r + ++-assoc : (p : Poly m) → (q : Poly n) → (r : Poly k) → + (p + q) + r ≈ p + (q + r) ++-assoc [] q r = begin + ([] + q) + r ≈⟨ +-congˡ (+-identityˡ q) ⟩ + q + r ≈⟨ +-identityˡ (q + r) ⟨ + [] + (q + r) ∎ ++-assoc (a ∷ p) [] r = +-congʳ (sym (+-identityˡ r)) ++-assoc (a ∷ p) (b ∷ q) [] = refl ++-assoc (a ∷ p) (b ∷ q) (c ∷ r) + = cons (SR.+-assoc a b c) (+-assoc p q r) + +middleFour : (p : Poly m) → (q : Poly n) → (r : Poly k) → (w : Poly l) → + (p + q) + (r + w) ≈ (p + r) + (q + w) +middleFour p q r w = begin + (p + q) + (r + w) ≈⟨ +-assoc (p + q) r w ⟨ + (p + q + r) + w ≈⟨ +-congˡ (+-assoc p q r) ⟩ + (p + (q + r)) + w ≈⟨ +-congˡ (+-congʳ (+-comm q r)) ⟩ + (p + (r + q)) + w ≈⟨ +-congˡ (+-assoc p r q) ⟨ + (p + r + q) + w ≈⟨ +-assoc (p + r) q w ⟩ + (p + r) + (q + w) ∎ + +------------------------------------------------------------------ +-- Vector casting lemmas + +private + n+1≡sucn+0 : (n ℕ.+ 1) ≡ suc (n ℕ.+ 0) + n+1≡sucn+0 {0} = Eq.refl + n+1≡sucn+0 {suc n} = cong suc n+1≡sucn+0 + + cast-p≈0⇒p≈0 : (m≡n : m ≡ n) → All (_≈A 0#) p → + All (_≈A 0#) (Vec.cast m≡n p) + cast-p≈0⇒p≈0 {n = 0} {[]} m≡n [] = [] + cast-p≈0⇒p≈0 {n = suc n} {a ∷ p} m≡n (a≈0 ∷ p≈0) + = a≈0 ∷ cast-p≈0⇒p≈0 (cong pred m≡n) p≈0 + + cast-p≈p : (m≡n : m ≡ n) → Vec.cast m≡n p ≈ p + cast-p≈p {n = 0} {[]} Eq.refl = refl + cast-p≈p {n = suc n} {a ∷ p} m≡n = consʳ (cast-p≈p (cong pred m≡n)) + + +------------------------------------------------------------------ +-- Properties of polynomial shifting + +*-distrib-shift : (p : Poly m) → (q : Poly n) → + p * (shift q) ≈ shift (p * q) +*-distrib-shift {_} {_} [] qs = zerosm≈zerosn +*-distrib-shift {suc m} {n} (a ∷ p) q = begin + (a ∷ p) * (0# ∷ q) + ≈⟨ cast-p≈p (cast-lem (suc n) m) ⟩ + a · (0# ∷ q) + p * (0# ∷ 0# ∷ q) + ≈⟨ +-congˡ (consˡ (SR.zeroʳ a)) ⟩ + (0# ∷ a · q) + p * (0# ∷ 0# ∷ q) + ≈⟨ +-congʳ (*-distrib-shift p (0# ∷ q)) ⟩ + (0# ∷ a · q) + (0# ∷ (p * (0# ∷ q))) + ≈⟨ consˡ (SR.+-identityˡ 0#) ⟩ + 0# ∷ (a · q + p * (0# ∷ q)) + ≈⟨ consʳ (cast-p≈p (cast-lem n m)) ⟨ + 0# ∷ ((a ∷ p) * q) + ∎ + +·-distrib-shift : (a : A) → (p : Poly m) → a · (shift p) ≈ shift (a · p) +·-distrib-shift a [] = cons (SR.zeroʳ a) (refl) +·-distrib-shift a (b ∷ p) = consˡ (SR.zeroʳ a) + +---------------------------------------------------------------- +-- Properties of polynomial scaling + +a·p≈a∷[]*p : (a : A) → (p : Poly n) → a · p ≈ (a ∷ []) * p +a·p≈a∷[]*p {_} a [] = refl +a·p≈a∷[]*p {suc n} a (b ∷ p) = begin + a · (b ∷ p) + ≈⟨ cons (SR.+-identityʳ (a *A b)) (+-identityʳ (a · p)) ⟨ + a *A b +A 0# ∷ (a · p + zeros n) + ≈⟨ consʳ (cast-p≈p (ℕ.⊔-idem n)) ⟨ + (a ∷ []) * (b ∷ p) ∎ + +1·p≈p : (p : Poly n) → 1# · p ≈ p +1·p≈p [] = refl +1·p≈p (a ∷ p) = cons (SR.*-identityˡ a) (1·p≈p p) + + +pIsZero⇒a·pIsZero : (a : A) → (p : Poly n) → IsZero p → IsZero (a · p) +pIsZero⇒a·pIsZero a p [] = [] +pIsZero⇒a·pIsZero a (b ∷ p) (b≈0 ∷ p≈0) + = (SR.trans (SR.*-congˡ b≈0) (SR.zeroʳ a)) ∷ pIsZero⇒a·pIsZero a p p≈0 + +a≈0⇒a·pIsZero : (a : A) → (p : Poly n) → a ≈A 0# → IsZero (a · p) +a≈0⇒a·pIsZero a [] a≈0 = [] +a≈0⇒a·pIsZero a (b ∷ p) a≈0 + = SR.trans (SR.*-congʳ a≈0) (SR.zeroˡ b) ∷ (a≈0⇒a·pIsZero a p a≈0) + +·-cong : a ≈A b → p ≈ q → a · p ≈ b · q +·-cong {a = _} {b = b} _ ([]≈ q q≈0) + = sym (IsZero⇒≈0 (pIsZero⇒a·pIsZero b q q≈0)) +·-cong {a = a} {b = _} _ (≈[] p p≈0) + = IsZero⇒≈0 (pIsZero⇒a·pIsZero a p p≈0) +·-cong {a = _} {b = _} c≈d (cons a≈b p≈q) + = cons (SR.*-cong c≈d a≈b) (·-cong c≈d p≈q) + +·-congˡ : a ≈A b → a · p ≈ b · p +·-congˡ a≈b = ·-cong a≈b refl + +·-congʳ : p ≈ q → a · p ≈ a · q +·-congʳ = ·-cong SR.refl + +·-dist : a · (p + q) ≈ (a · p) + (a · q) +·-dist {p = []} {q = []} = refl +·-dist {p = []} {q = b ∷ q} = refl +·-dist {p = b ∷ p} {q = []} = refl +·-dist {a = a} {p = b ∷ p} {q = c ∷ q} = cons (SR.distribˡ a b c) ·-dist + +·-assoc : a · (b · p) ≈ (a *A b) · p +·-assoc {p = []} = refl +·-assoc {a} {b} {p = c ∷ p} = cons (SR.sym (SR.*-assoc a b c)) ·-assoc + +a·-cong : p ≈ q → a · p ≈ a · q +a·-cong = ·-cong SR.refl + +·-distrib-+A : (a b : A) → (p : Poly m) → (a +A b) · p ≈ a · p + b · p +·-distrib-+A a b [] = refl +·-distrib-+A a b (c ∷ p) = cons (SR.distribʳ c a b) (·-distrib-+A a b p) + +----------------------------------------------------------------- +-- Properties of polynomial multiplication + +zeroˡ : (p : Poly m) → [] * p ≈ [] +zeroˡ p = zerosm≈zerosn + +zeroʳ : (p : Poly m) → p * [] ≈ [] +zeroʳ [] = refl +zeroʳ {m} (a ∷ p) = begin + (a ∷ p) * [] ≈⟨ cast-p≈p (cong pred n+1≡sucn+0) ⟩ + (a · []) + p * (0# ∷ []) ≈⟨ +-identityˡ (p * (0# ∷ [])) ⟩ + p * (0# ∷ []) ≈⟨ *-distrib-shift p [] ⟩ + 0# ∷ (p * []) ≈⟨ consʳ (zeroʳ p) ⟩ + 0# ∷ [] ≈⟨ zerosm≈zerosn ⟩ + [] ∎ + +pIsZero⇒p*qIsZero : (q : Poly n) → IsZero p → IsZero (p * q) +pIsZero⇒p*qIsZero {n} {p = []} q [] = zerosIsZero (pred n) +pIsZero⇒p*qIsZero {n} {suc m} {p = a ∷ p} q (a≈0 ∷ p≈0) + = cast-p≈0⇒p≈0 (cast-lem n m) + (All-p≈0∧q≈0⇒p+q≈0 (a≈0⇒a·pIsZero a q a≈0) (pIsZero⇒p*qIsZero (0# ∷ q) p≈0)) + +p≈[]⇒p*q≈[] : (q : Poly n) → p ≈ [] → p * q ≈ [] +p≈[]⇒p*q≈[] q p≈0 = IsZero⇒≈0 (pIsZero⇒p*qIsZero q (≈0⇒IsZero p≈0)) + +*-cong : {p : Poly m} → {q : Poly n} → {r : Poly k} → {s : Poly l} → + p ≈ q → r ≈ s → p * r ≈ q * s +*-cong {k = k} {q = q} {r} {s} ([]≈ q q≈0) r≈s = begin + [] * r ≈⟨ p≈[]⇒p*q≈[] r refl ⟩ + [] ≈⟨ p≈[]⇒p*q≈[] s (IsZero⇒≈0 q≈0) ⟨ + q * s ∎ +*-cong {k = k} {q = q} {r} {s} (≈[] p p≈0) r≈s = begin + p * r ≈⟨ p≈[]⇒p*q≈[] r (IsZero⇒≈0 p≈0) ⟩ + [] ≈⟨ zerosm≈zerosn ⟩ + [] * s ∎ +*-cong {n = suc n} {l = l} {a ∷ p} {b ∷ q} (cons a≈b p≈q) ([]≈ s s≈0) = begin + (a ∷ p) * [] + ≈⟨ cast-p≈p (cong pred n+1≡sucn+0) ⟩ + [] + p * (0# ∷ []) + ≈⟨ +-congʳ (*-cong (sym p≈q) (consʳ (IsZero⇒≈0 s≈0))) ⟨ + [] + q * (0# ∷ s) + ≈⟨ +-congˡ (zerosm≈zerosn) ⟩ + zeros l + q * (0# ∷ s) + ≈⟨ +-congˡ (IsZero⇒≈0 (pIsZero⇒a·pIsZero b s s≈0)) ⟨ + (b · s) + q * (0# ∷ s) + ≈⟨ cast-p≈p (cast-lem l n) ⟨ + (b ∷ q) * s + ∎ +*-cong {suc m} {k = k} {p = a ∷ p} {b ∷ q} (cons a≈b p≈q) (≈[] r s≈0) = begin + (a ∷ p) * r + ≈⟨ cast-p≈p (cast-lem k m) ⟩ + (a · r) + p * (0# ∷ r) + ≈⟨ +-congʳ (*-cong (sym p≈q) (consʳ ([]≈ r s≈0))) ⟨ + (a · r) + q * (0# ∷ []) + ≈⟨ +-congˡ (IsZero⇒≈0 (pIsZero⇒a·pIsZero a r s≈0)) ⟩ + zeros k + q * (0# ∷ []) + ≈⟨ +-congˡ zerosm≈zerosn ⟩ + (b · []) + q * (0# ∷ []) + ≈⟨ cast-p≈p (cong pred n+1≡sucn+0) ⟨ + (b ∷ q) * [] + ∎ +*-cong {suc m} {suc n} {suc k} {suc l} {a ∷ p} {b ∷ q} {c ∷ r} {d ∷ s} (cons a≈b p≈q) (cons c≈d r≈s) = begin + (a ∷ p) * (c ∷ r) + ≈⟨ cast-p≈p (cast-lem (suc k) m)⟩ + (a *A c ∷ a · r) + p * (0# ∷ c ∷ r) + ≈⟨ +-congˡ (consˡ (SR.*-cong a≈b c≈d)) ⟩ + (b *A d ∷ a · r) + p * (0# ∷ c ∷ r) + ≈⟨ +-congˡ (consʳ (·-cong a≈b r≈s)) ⟩ + (b *A d ∷ b · s) + p * (0# ∷ c ∷ r) + ≈⟨ +-congʳ (*-cong p≈q (consʳ (cons c≈d r≈s))) ⟩ + (b *A d ∷ b · s) + q * (0# ∷ d ∷ s) + ≈⟨ cast-p≈p (cast-lem (suc l) n) ⟨ + (b ∷ q) * (d ∷ s) + ∎ + +*-congʳ : q ≈ r → p * q ≈ p * r +*-congʳ {p = p} q≈r = *-cong {p = p} refl q≈r + +*-congˡ : p ≈ q → p * r ≈ q * r +*-congˡ p≈q = *-cong p≈q refl + +qIsZero⇒p*qIsZero : (p : Poly m) → IsZero q → IsZero (p * q) +qIsZero⇒p*qIsZero {m} {q = []} p [] = ≈0⇒IsZero (zeroʳ p) +qIsZero⇒p*qIsZero {m} {suc n} {q = b ∷ q} p (b≈0 ∷ q≈0) + = ≈0⇒IsZero ( + begin + p * (b ∷ q) ≈⟨ *-congʳ {p = p} (consˡ b≈0) ⟩ + p * (0# ∷ q) ≈⟨ *-distrib-shift p q ⟩ + 0# ∷ (p * q) ≈⟨ consʳ (IsZero⇒≈0 (qIsZero⇒p*qIsZero p q≈0)) ⟩ + 0# ∷ (zeros m) ≈⟨ zerosm≈zerosn ⟩ + zeros m ∎ + ) + +q≈[]→p*q≈[] : (p : Poly n) → q ≈ [] → p * q ≈ [] +q≈[]→p*q≈[] p q≈0 = IsZero⇒≈0 (qIsZero⇒p*qIsZero p (≈0⇒IsZero q≈0)) + +shift-distrib-+ : (p : Poly m) → (q : Poly n) → + shift (p + q) ≈ (shift p) + (shift q) +shift-distrib-+ p q = cons (SR.sym (SR.+-identityʳ 0#)) refl + +*-identityʳ : (p : Poly n) → p * (1# ∷ []) ≈ p +*-identityʳ {0} [] = zerosm≈zerosn +*-identityʳ {suc n} (a ∷ p) = begin + (a ∷ p) * (1# ∷ []) + ≈⟨ cast-p≈p (cast-lem 1 n) ⟩ + (a *A 1# ∷ []) + (p * (0# ∷ 1# ∷ [])) + ≈⟨ +-congˡ (consˡ (SR.*-identityʳ a)) ⟩ + (a ∷ []) + (p * (0# ∷ 1# ∷ [])) + ≈⟨ +-congʳ (*-distrib-shift p (1# ∷ [])) ⟩ + (a ∷ []) + (0# ∷ (p * (1# ∷ []))) + ≈⟨ cons (SR.+-identityʳ a) (+-identityˡ (p * (1# ∷ []))) ⟩ + a ∷ (p * (1# ∷ [])) + ≈⟨ consʳ (*-identityʳ p) ⟩ + a ∷ p ∎ + +*-identityˡ : (p : Poly n) → (1# ∷ []) * p ≈ p +*-identityˡ [] = refl +*-identityˡ {suc n} (a ∷ p) = begin + (1# ∷ []) * (a ∷ p) + ≈⟨ consʳ (cast-p≈p (ℕ.⊔-idem n)) ⟩ + 1# · (a ∷ p) + [] * (0# ∷ a ∷ p) + ≈⟨ +-identityʳ {m = pred (suc (suc n))} (1# · (a ∷ p) + []) ⟩ + 1# · (a ∷ p) + [] + ≈⟨ +-identityʳ {m = 0} (1# · (a ∷ p)) ⟩ + 1# · (a ∷ p) + ≈⟨ cons (SR.*-identityˡ a) (1·p≈p p) ⟩ + a ∷ p ∎ + +-- (0# ∷ 1# ∷ []) is the center of a polynomial ring +shiftp≈p*x : (p : Poly n) → shift p ≈ p * (0# ∷ 1# ∷ []) +shiftp≈p*x [] = refl +shiftp≈p*x {suc n} (a ∷ p) = begin + 0# ∷ a ∷ p + ≈⟨ cons (SR.+-identityˡ 0#) (cons (SR.+-identityʳ a) (+-identityˡ p)) ⟨ + (0# ∷ a ∷ []) + shift (shift p) + ≈⟨ consʳ (consʳ (+-congʳ (*-identityʳ p))) ⟨ + (0# ∷ a ∷ []) + (shift (shift (p * (1# ∷ [])))) + ≈⟨ +-congʳ {p = 0# ∷ a ∷ []} (consʳ (*-distrib-shift p (1# ∷ []))) ⟨ + (0# ∷ a ∷ []) + shift (p * shift (1# ∷ [])) + ≈⟨ +-congʳ {p = 0# ∷ a ∷ []} (*-distrib-shift p (0# ∷ 1# ∷ [])) ⟨ + (0# ∷ a ∷ []) + p * shift (shift (1# ∷ [])) + ≈⟨ +-congˡ (cons (SR.zeroʳ a) (consˡ (SR.*-identityʳ a))) ⟨ + a · (0# ∷ 1# ∷ []) + p * (0# ∷ 0# ∷ 1# ∷ []) + ≈⟨ cast-p≈p (cast-lem 2 n) ⟨ + (a ∷ p) * (0# ∷ 1# ∷ []) ∎ + +shiftp≈x*p : (p : Poly n) → shift p ≈ (0# ∷ 1# ∷ []) * p +shiftp≈x*p [] + = consˡ (SR.sym (SR.trans (SR.+-identityʳ (1# *A 0#)) (SR.zeroʳ 1#))) +shiftp≈x*p {suc n} (a ∷ p) = begin + 0# ∷ a ∷ p + ≈⟨ *-identityˡ (0# ∷ a ∷ p) ⟨ + (1# ∷ []) * (0# ∷ a ∷ p) + ≈⟨ +-identityˡ {m = 0} ((1# ∷ []) * (0# ∷ a ∷ p)) ⟨ + [] + (1# ∷ []) * (0# ∷ a ∷ p) + ≈⟨ +-identityˡ {m = 0} ((1# ∷ []) * (0# ∷ a ∷ p)) ⟩ + (1# ∷ []) * (0# ∷ a ∷ p) + ≈⟨ +-idˡ (0# *A a ∷ 0# · p) ((1# ∷ []) * (0# ∷ a ∷ p)) + ((SR.zeroˡ a) ∷ a≈0⇒a·pIsZero 0# p SR.refl) ⟨ + 0# · (a ∷ p) + (1# ∷ []) * (0# ∷ a ∷ p) + ≈⟨ consʳ (cast-p≈p (ℕ.m≤n⇒m⊔n≡n (ℕ.n≤1+n n))) ⟨ + (0# ∷ 1# ∷ []) * (a ∷ p) ∎ + +·-distrib-* : (p : Poly m) → (q : Poly n) → (a : A) → + a · (p * q) ≈ (a · p) * q +·-distrib-* {_} {n} [] q a = begin + a · ([] * q) ≈⟨ ·-congʳ zerosm≈zerosn ⟩ + a · [] ≈⟨ zerosm≈zerosn ⟨ + (a · []) * q ∎ +·-distrib-* {suc m} {_} (b ∷ p) [] a = begin + a · ((b ∷ p) * []) + ≈⟨ a·-cong (cast-p≈p (cong pred n+1≡sucn+0)) ⟩ + a · ((b · []) + (p * (0# ∷ []))) + ≈⟨ a·-cong (+-identityˡ (p * (0# ∷ []))) ⟩ + a · (p * (0# ∷ [])) + ≈⟨ a·-cong (q≈[]→p*q≈[] p zerosm≈zerosn) ⟩ + [] + ≈⟨ q≈[]→p*q≈[] ((a · p)) zerosm≈zerosn ⟨ + (a · p) * (0# ∷ []) + ≈⟨ +-identityˡ ((a · p) * (0# ∷ [])) ⟨ + ((a *A b) · []) + ((a · p) * (0# ∷ [])) + ≈⟨ cast-p≈p (cong pred n+1≡sucn+0) ⟨ + (a · (b ∷ p)) * [] + ∎ +·-distrib-* {suc m} {suc n} (b ∷ p) (c ∷ q) a = begin + a · ((b ∷ p) * (c ∷ q)) + ≈⟨ a·-cong (cast-p≈p (cast-lem (suc n) m)) ⟩ + a · ((b · (c ∷ q)) + (p * (0# ∷ c ∷ q))) + ≈⟨ ·-dist ⟩ + a · (b *A c ∷ (b · q)) + a · (p * (0# ∷ c ∷ q)) + ≈⟨ +-congˡ (cons (SR.sym (SR.*-assoc a b c)) ·-assoc) ⟩ + (a *A b *A c ∷ ((a *A b) · q)) + a · (p * (0# ∷ c ∷ q)) + ≈⟨ +-congʳ (·-distrib-* p (0# ∷ c ∷ q) a) ⟩ + (a *A b) · (c ∷ q) + (a · p) * (0# ∷ c ∷ q) + ≈⟨ cast-p≈p (cast-lem (suc n) m) ⟨ + (a · (b ∷ p)) * (c ∷ q) + ∎ + +0∷[p*q]≈[0∷p]*q : (p : Poly m) → (q : Poly n) → + shift (p * q) ≈ (shift p) * q +0∷[p*q]≈[0∷p]*q {n = n} [] q = begin + shift ([] * q) + ≈⟨ consʳ zerosm≈zerosn ⟩ + shift [] + ≈⟨ IsZero⇒≈0 (All-p≈0∧q≈0⇒p+q≈0 (a≈0⇒a·pIsZero 0# q SR.refl) + (≈0⇒IsZero {m = n} zerosm≈zerosn)) ⟨ + 0# · q + zeros (pred (suc n)) + ≈⟨ cast-p≈p (ℕ.⊔-idem (pred (1 ℕ.+ n))) ⟨ + shift [] * q ∎ +0∷[p*q]≈[0∷p]*q {m = suc m} {n = n} (a ∷ p) (q) = begin + shift ((a ∷ p) * q) + ≈⟨ *-distrib-shift (a ∷ p) q ⟨ + (a ∷ p) * shift q + ≈⟨ cast-p≈p (cast-lem (suc n) m) ⟩ + a · shift q + p * (0# ∷ shift q) + ≈⟨ +-idˡ (0# · q) (a · (0# ∷ q) + p * (0# ∷ 0# ∷ q)) + (a≈0⇒a·pIsZero 0# q SR.refl) ⟨ + 0# · q + (a · (0# ∷ q) + p * (0# ∷ 0# ∷ q)) + ≈⟨ +-congʳ (cast-p≈p (cast-lem (suc n) m)) ⟨ + 0# · q + (a ∷ p) * (0# ∷ q) + ≈⟨ cast-p≈p (cast-lem n (suc m)) ⟨ + shift (a ∷ p) * q ∎ + +*-distribˡ-+ : (p : Poly m) → (q : Poly n) → (r : Poly k) → + p * (q + r) ≈ p * q + p * r +*-distribˡ-+ [] q r = begin + [] * (q + r) + ≈⟨ zerosm≈zerosn ⟩ + [] + ≈⟨ IsZero⇒≈0 (All-p≈0∧q≈0⇒p+q≈0 (≈0⇒IsZero refl) (≈0⇒IsZero refl)) ⟨ + [] * q + [] * r ∎ +*-distribˡ-+ {m = suc m} {n = n} {k = k} (a ∷ p) q r = begin + (a ∷ p) * (q + r) + ≈⟨ cast-p≈p (cast-lem (n ⊔ k) m) ⟩ + a · (q + r) + p * (0# ∷ q + r) + ≈⟨ +-cong ·-dist (*-distrib-shift p (q + r)) ⟩ + (a · q + a · r) + (0# ∷ (p * (q + r))) + ≈⟨ +-congʳ (consʳ (*-distribˡ-+ p q r)) ⟩ + (a · q + a · r) + (0# ∷ (p * q + p * r)) + ≈⟨ +-congʳ (consˡ (SR.+-identityʳ 0#)) ⟨ + (a · q + a · r) + ((0# ∷ (p * q)) + (0# ∷ (p * r))) + ≈⟨ middleFour (a · q) (a · r) (0# ∷ p * q) (0# ∷ p * r) ⟩ + ((a · q) + (0# ∷ (p * q))) + ((a · r) + (0# ∷ (p * r))) + ≈⟨ +-cong (+-congʳ (*-distrib-shift p q)) (+-congʳ (*-distrib-shift p r)) ⟨ + (a · q + p * (0# ∷ q)) + (a · r + p * (0# ∷ r)) + ≈⟨ +-cong (cast-p≈p (cast-lem n m)) (cast-p≈p (cast-lem k m)) ⟨ + (a ∷ p) * q + (a ∷ p) * r + ∎ + +*-distribʳ-+ : (p : Poly m) → (q : Poly n) → (r : Poly k) → + (q + r) * p ≈ (q * p) + (r * p) +*-distribʳ-+ {m = m} p [] [] = sym (+-identityʳ (zeros (m ℕ.∸ 1))) +*-distribʳ-+ {m = m} {k = suc k} p [] (c ∷ r) = begin + ([] + (c ∷ r)) * p + ≈⟨ cast-p≈p (cast-lem m k) ⟩ + c · p + r * (0# ∷ p) + ≈⟨ cast-p≈p (cast-lem m k) ⟨ + (c ∷ r) * p + ≈⟨ +-identityˡ ((c ∷ r) * p) ⟨ + [] * p + (c ∷ r) * p + ∎ +*-distribʳ-+ {m = m} {n = suc n} p (b ∷ q) [] = begin + ((b ∷ q) + []) * p + ≈⟨ cast-p≈p (cast-lem m n) ⟩ + b · p + q * (0# ∷ p) + ≈⟨ cast-p≈p (cast-lem m n) ⟨ + (b ∷ q) * p + ≈⟨ +-identityʳ ((b ∷ q) * p) ⟨ + (b ∷ q) * p + [] * p + ∎ +*-distribʳ-+ {m} {suc n} {suc k} p (b ∷ q) (c ∷ r) = begin + ((b ∷ q) + (c ∷ r)) * p + ≈⟨ cast-p≈p (cast-lem m (n ⊔ k)) ⟩ + (b +A c) · p + (q + r) * (0# ∷ p) + ≈⟨ +-cong (·-distrib-+A b c p) (*-distribʳ-+ (0# ∷ p) q r) ⟩ + ((b · p) + (c · p)) + (q * (0# ∷ p) + r * (0# ∷ p)) + ≈⟨ middleFour (b · p) (c · p) (q * (0# ∷ p)) (r * (0# ∷ p)) ⟩ + (b · p + q * (0# ∷ p)) + (c · p + r * (0# ∷ p)) + ≈⟨ +-cong (cast-p≈p (cast-lem m n)) (cast-p≈p (cast-lem m k)) ⟨ + (b ∷ q) * p + (c ∷ r) * p + ∎ + +*-assoc : (p : Poly m) → (q : Poly n) → (r : Poly k) → + (p * q) * r ≈ p * (q * r) +*-assoc {n = n} {k} [] q r = begin + zeros (n ℕ.∸ 1) * r + ≈⟨ p≈[]⇒p*q≈[] r (IsZero⇒≈0 (zerosIsZero (n ℕ.∸ 1))) ⟩ + [] + ≈⟨ zerosm≈zerosn ⟩ + zeros (pred (0 ℕ.+ pred (n ℕ.+ k))) + ∎ +*-assoc {suc m} {n} {k} (a ∷ p) q r = begin + ((a ∷ p) * q) * r + ≈⟨ *-congˡ (cast-p≈p (cast-lem n m)) ⟩ + ((a · q) + (p * (0# ∷ q))) * r + ≈⟨ *-congˡ (+-congʳ {p = a · q} (*-distrib-shift p q)) ⟩ + ((a · q) + (0# ∷ (p * q))) * r + ≈⟨ *-distribʳ-+ r (a · q) (0# ∷ p * q) ⟩ + ((a · q) * r) + ((0# ∷ (p * q)) * r) + ≈⟨ +-congʳ step1 ⟨ + ((a · q) * r) + (0# ∷ (p * (q * r))) + ≈⟨ +-congˡ (·-distrib-* q r a) ⟨ + (a · (q * r)) + (0# ∷ (p * (q * r))) + ≈⟨ +-congʳ (*-distrib-shift p (q * r)) ⟨ + (a · (q * r)) + (p * (0# ∷ (q * r))) + ≈⟨ cast-p≈p (cast-lem (pred (n ℕ.+ k)) m) ⟨ + (a ∷ p) * (q * r) + ∎ + where + step1 = begin + 0# ∷ (p * (q * r)) + ≈⟨ consʳ (*-assoc p q r) ⟨ + 0# ∷ ((p * q) * r) + ≈⟨ 0∷[p*q]≈[0∷p]*q (p * q) r ⟩ + (0# ∷ (p * q)) * r + ≈⟨ cast-p≈p (cast-lem k (m ℕ.+ n ℕ.∸ 1)) ⟩ + (0# · r) + ((p * q) * (0# ∷ r)) + ≈⟨ +-congˡ (IsZero⇒≈0 (a≈0⇒a·pIsZero 0# r SR.refl) ) ⟩ + zeros k + ((p * q) * (0# ∷ r)) + ≈⟨ +-congʳ (*-distrib-shift (p * q) r) ⟩ + zeros k + (0# ∷ ((p * q) * r)) + ≈⟨ +-congʳ (0∷[p*q]≈[0∷p]*q (p * q) r) ⟩ + zeros k + ((0# ∷ (p * q)) * r) + ≈⟨ +-identityˡ ((0# ∷ (p * q)) * r) ⟩ + (0# ∷ (p * q)) * r + ∎ + + diff --git a/src/Algebra/Polynomial/Poly/Properties1.agda b/src/Algebra/Polynomial/Poly/Properties1.agda new file mode 100644 index 0000000000..de8401c194 --- /dev/null +++ b/src/Algebra/Polynomial/Poly/Properties1.agda @@ -0,0 +1,646 @@ +open import Algebra.Bundles using (Ring) + +module Algebra.Polynomial.Poly.Properties1 + {ℓ₁ ℓ₂} (R : Ring ℓ₁ ℓ₂) + where + +open import Algebra.Polynomial.Poly.Base1 R as P + using ( Poly; _+_ ; _*_ ; _·_ ; -_; shift; _≈_; refl; trans; sym; zeros + ; IsZero; []≈ ; ≈[]; cons; zeros-unique; consˡ; consʳ; cast-lem) +open import Algebra.Properties.Ring +open import Data.Nat.Base as ℕ using (ℕ; suc; pred; _⊔_) +import Data.Nat.Properties as ℕ +open import Data.Vec.Base as Vec using (Vec; []; _∷_) +open import Data.Vec.Relation.Unary.All using (All ; []; _∷_; head; tail) +import Level as L +open import Relation.Binary +open import Relation.Binary.PropositionalEquality as Eq + using (_≡_; module ≡-Reasoning) +open import Relation.Binary.PropositionalEquality.Core using (cong) + +module R = Ring R +open R + renaming + ( Carrier to A + ; _≈_ to _≈A_ + ; _+_ to _+A_ + ; _*_ to _*A_ + ; -_ to -A_) + using (0#; 1#) + +private + variable + m n k l : ℕ + a b c d : A + p : Poly m + q : Poly n + r : Poly k + s : Poly l + +--------------------------------------------------------------------- +-- Equational reasoning for Poly n and Poly m +-- where m is not necesarily the same as n +private + + infix 4 _IsRelatedTo_ + + data _IsRelatedTo_ (p : Poly m) (q : Poly n) : Set (ℓ₁ L.⊔ ℓ₂) where + relTo : (p≈q : p ≈ q) → p IsRelatedTo q + + start : _IsRelatedTo_ {m} {n} ⇒ _≈_ + start (relTo p≈q) = p≈q + + ∼-go : Trans (_≈_) (_IsRelatedTo_ {n} {k}) (_IsRelatedTo_ {m} {k}) + ∼-go p≈q (relTo q≈r) = relTo (trans p≈q q≈r) + + stop : Reflexive (_IsRelatedTo_ {m} {m}) + stop = relTo refl + + forward : (p : Poly m) → q IsRelatedTo r → p ≈ q → p IsRelatedTo r + forward p qRr p≈q = ∼-go p≈q qRr + + backward : (p : Poly m) → q IsRelatedTo r → q ≈ p → p IsRelatedTo r + backward p qRr q≈p = ∼-go (sym q≈p) qRr + + infix 1 begin_ + begin_ : p IsRelatedTo q → p ≈ q + begin_ = start + + infixr 2 step-∼-⟩ + step-∼-⟩ = forward + syntax step-∼-⟩ p qRr p≈q = p ≈⟨ p≈q ⟩ qRr + + infixr 2 step-∼-⟨ + step-∼-⟨ = backward + syntax step-∼-⟨ p qRr q≈p = p ≈⟨ q≈p ⟨ qRr + + infix 3 _∎ + _∎ : (p : Poly m) → p IsRelatedTo p + p ∎ = stop + +-- Properties of zero polynomial + +zerosIsZero : (n : ℕ) → IsZero (zeros n) +zerosIsZero 0 = [] +zerosIsZero (suc n) = R.refl ∷ (zerosIsZero n) + +zerosm≈zerosn : zeros m ≈ zeros n +zerosm≈zerosn {m} {n} = zeros-unique (zerosIsZero m) (zerosIsZero n) + +≈0⇒IsZero : p ≈ zeros m → IsZero p +≈0⇒IsZero ([]≈ zeros zeros≈0) = [] +≈0⇒IsZero (≈[] p p≈0) = p≈0 +≈0⇒IsZero (cons a≈0 p≈0) = a≈0 ∷ ≈0⇒IsZero p≈0 + +IsZero⇒≈0 : IsZero p → p ≈ zeros m +IsZero⇒≈0 {m = m} p≈0 = zeros-unique p≈0 (zerosIsZero m) + +All-p≈0∧q≈0⇒p+q≈0 : IsZero p → IsZero q → IsZero (p + q) +All-p≈0∧q≈0⇒p+q≈0 {p = _} {q = _} [] [] = [] +All-p≈0∧q≈0⇒p+q≈0 {p = _} {q = _} [] (b≈0 ∷ q≈0) = b≈0 ∷ q≈0 +All-p≈0∧q≈0⇒p+q≈0 {p = _} {q = _} (a≈0 ∷ p≈0) [] = a≈0 ∷ p≈0 +All-p≈0∧q≈0⇒p+q≈0 {p = a ∷ p} {q = b ∷ q} (a≈0 ∷ p≈0) (b≈0 ∷ q≈0) + = R.trans (R.+-cong a≈0 b≈0) (R.+-identityˡ 0#) ∷ All-p≈0∧q≈0⇒p+q≈0 p≈0 q≈0 + +------------------------------------------------------ +-- Additive inverse + +[-p]+pIsZero : {p : Poly m} → IsZero ((- p) + p) +[-p]+pIsZero {p = []} = [] +[-p]+pIsZero {p = a ∷ p} = R.-‿inverseˡ a ∷ [-p]+pIsZero + +p+[-p]IsZero : {p : Poly m} → IsZero (p + (- p)) +p+[-p]IsZero {p = []} = [] +p+[-p]IsZero {p = a ∷ p} = R.-‿inverseʳ a ∷ p+[-p]IsZero + ++-inverseˡ : (p : Poly m) → (- p) + p ≈ [] ++-inverseˡ [] = refl ++-inverseˡ (a ∷ p) + = ≈[] ((- (a ∷ p)) + (a ∷ p)) (R.-‿inverseˡ a ∷ [-p]+pIsZero) + ++-inverseʳ : (p : Poly m) → p + (- p) ≈ [] ++-inverseʳ [] = refl ++-inverseʳ (a ∷ p) + = ≈[] ((a ∷ p) + (- (a ∷ p))) ((R.-‿inverseʳ a) ∷ p+[-p]IsZero) + +------------------------------------------------------- +-- Negation is congruent + +-⁺ : IsZero p → IsZero (- p) +-⁺ [] = [] +-⁺ (a≈0 ∷ p≈0) = x≈ε⇒x⁻¹≈ε R a≈0 ∷ (-⁺ p≈0) + +-⁻ : IsZero (- p) → IsZero p +-⁻ {p = []} -p≈0 = -p≈0 +-⁻ {p = a ∷ p} (-a≈0 ∷ -p≈0) = x⁻¹≈ε⇒x≈ε R -a≈0 ∷ (-⁻ -p≈0) + +-‿cong : p ≈ q → - p ≈ - q +-‿cong ([]≈ q q≈0) = []≈ (- q) (-⁺ q≈0) +-‿cong (≈[] p p≈0) = ≈[] (- p) (-⁺ p≈0) +-‿cong (cons a≈b p≈q) = cons (R.-‿cong a≈b) (-‿cong p≈q) + +----------------------------------------------------- +-- Properties of polynomial addition + ++-comm : (p : Poly m) → (q : Poly n) → p + q ≈ q + p ++-comm [] [] = refl ++-comm [] (a ∷ p) = refl ++-comm (a ∷ p) [] = refl ++-comm (a ∷ p) (b ∷ q) = cons (R.+-comm a b) (+-comm p q) + ++-idʳ : (p : Poly n) → (q : Poly m) → IsZero q → p + q ≈ p ++-idʳ [] q [] = refl ++-idʳ (a ∷ p) q [] = refl ++-idʳ [] (a ∷ q) (a≈0 ∷ q≈0) = ≈[] (a ∷ q) (a≈0 ∷ q≈0) ++-idʳ (a ∷ p) (b ∷ q) (b≈0 ∷ q≈0) + = cons (R.trans (R.+-congˡ b≈0) (R.+-identityʳ a)) (+-idʳ p q q≈0) + ++-idˡ : (p : Poly n) → (q : Poly m) → IsZero p → p + q ≈ q ++-idˡ p q p≈0 = begin + p + q ≈⟨ +-comm p q ⟩ + q + p ≈⟨ +-idʳ q p p≈0 ⟩ + q ∎ + ++-identityʳ : (p : Poly n) → p + (zeros m) ≈ p ++-identityʳ {m = m} p = +-idʳ p (zeros m) (zerosIsZero m) + ++-identityˡ : (p : Poly n) → (zeros m) + p ≈ p ++-identityˡ {m = m} p = +-idˡ (zeros m) p (zerosIsZero m) + ++-cong : p ≈ q → r ≈ s → p + r ≈ q + s ++-cong {p = _} {q = _} {r = r} {s = s} ([]≈ q q≈0) r≈s = begin + [] + r ≈⟨ +-identityˡ r ⟩ + r ≈⟨ r≈s ⟩ + s ≈⟨ +-idˡ q s q≈0 ⟨ + q + s ∎ ++-cong {p = _} {q = _} {r = r} {s = s} (≈[] p p≈0) r≈s = begin + p + r ≈⟨ +-idˡ p r p≈0 ⟩ + r ≈⟨ r≈s ⟩ + s ≈⟨ +-identityˡ s ⟨ + [] + s ∎ ++-cong {p = a ∷ p} {q = b ∷ q} {r = _} {s = s} (cons a≈b p≈q) ([]≈ s s≈0) = begin + a ∷ p ≈⟨ cons a≈b p≈q ⟩ + b ∷ q ≈⟨ +-idʳ (b ∷ q) s s≈0 ⟨ + (b ∷ q) + s ∎ ++-cong {p = a ∷ p} {q = b ∷ q} {r = r} {s = _} (cons a≈b p≈q) (≈[] r r≈0) = begin + (a ∷ p) + r ≈⟨ +-idʳ (a ∷ p) r r≈0 ⟩ + a ∷ p ≈⟨ cons a≈b p≈q ⟩ + b ∷ q ∎ ++-cong (cons a≈b p≈q) (cons c≈d r≈s) + = cons (R.+-cong a≈b c≈d) (+-cong p≈q r≈s) + ++-congˡ : p ≈ q → p + r ≈ q + r ++-congˡ p≈q = +-cong p≈q refl + ++-congʳ : q ≈ r → p + q ≈ p + r ++-congʳ q≈r = +-cong refl q≈r + ++-assoc : (p : Poly m) → (q : Poly n) → (r : Poly k) → + (p + q) + r ≈ p + (q + r) ++-assoc [] q r = begin + ([] + q) + r ≈⟨ +-congˡ (+-identityˡ q) ⟩ + q + r ≈⟨ +-identityˡ (q + r) ⟨ + [] + (q + r) ∎ ++-assoc (a ∷ p) [] r = +-congʳ (sym (+-identityˡ r)) ++-assoc (a ∷ p) (b ∷ q) [] = refl ++-assoc (a ∷ p) (b ∷ q) (c ∷ r) + = cons (R.+-assoc a b c) (+-assoc p q r) + +middleFour : (p : Poly m) → (q : Poly n) → (r : Poly k) → (w : Poly l) → + (p + q) + (r + w) ≈ (p + r) + (q + w) +middleFour p q r w = begin + (p + q) + (r + w) ≈⟨ +-assoc (p + q) r w ⟨ + (p + q + r) + w ≈⟨ +-congˡ (+-assoc p q r) ⟩ + (p + (q + r)) + w ≈⟨ +-congˡ (+-congʳ (+-comm q r)) ⟩ + (p + (r + q)) + w ≈⟨ +-congˡ (+-assoc p r q) ⟨ + (p + r + q) + w ≈⟨ +-assoc (p + r) q w ⟩ + (p + r) + (q + w) ∎ + +------------------------------------------------------------------ +-- Vector casting lemmas + +private + n+1≡sucn+0 : (n ℕ.+ 1) ≡ suc (n ℕ.+ 0) + n+1≡sucn+0 {0} = Eq.refl + n+1≡sucn+0 {suc n} = cong suc n+1≡sucn+0 + + cast-p≈0⇒p≈0 : (m≡n : m ≡ n) → All (_≈A 0#) p → + All (_≈A 0#) (Vec.cast m≡n p) + cast-p≈0⇒p≈0 {n = 0} {[]} m≡n [] = [] + cast-p≈0⇒p≈0 {n = suc n} {a ∷ p} m≡n (a≈0 ∷ p≈0) + = a≈0 ∷ cast-p≈0⇒p≈0 (cong pred m≡n) p≈0 + + cast-p≈p : (m≡n : m ≡ n) → Vec.cast m≡n p ≈ p + cast-p≈p {n = 0} {[]} Eq.refl = refl + cast-p≈p {n = suc n} {a ∷ p} m≡n = consʳ (cast-p≈p (cong pred m≡n)) + + +------------------------------------------------------------------ +-- Properties of polynomial shifting + +*-distrib-shift : (p : Poly m) → (q : Poly n) → + p * (shift q) ≈ shift (p * q) +*-distrib-shift {_} {_} [] qs = zerosm≈zerosn +*-distrib-shift {suc m} {n} (a ∷ p) q = begin + (a ∷ p) * (0# ∷ q) + ≈⟨ cast-p≈p (cast-lem (suc n) m) ⟩ + a · (0# ∷ q) + p * (0# ∷ 0# ∷ q) + ≈⟨ +-congˡ (consˡ (R.zeroʳ a)) ⟩ + (0# ∷ a · q) + p * (0# ∷ 0# ∷ q) + ≈⟨ +-congʳ (*-distrib-shift p (0# ∷ q)) ⟩ + (0# ∷ a · q) + (0# ∷ (p * (0# ∷ q))) + ≈⟨ consˡ (R.+-identityˡ 0#) ⟩ + 0# ∷ (a · q + p * (0# ∷ q)) + ≈⟨ consʳ (cast-p≈p (cast-lem n m)) ⟨ + 0# ∷ ((a ∷ p) * q) + ∎ + +·-distrib-shift : (a : A) → (p : Poly m) → a · (shift p) ≈ shift (a · p) +·-distrib-shift a [] = cons (R.zeroʳ a) (refl) +·-distrib-shift a (b ∷ p) = consˡ (R.zeroʳ a) + +---------------------------------------------------------------- +-- Properties of polynomial scaling + +a·p≈a∷[]*p : (a : A) → (p : Poly n) → a · p ≈ (a ∷ []) * p +a·p≈a∷[]*p {_} a [] = refl +a·p≈a∷[]*p {suc n} a (b ∷ p) = begin + a · (b ∷ p) + ≈⟨ cons (R.+-identityʳ (a *A b)) (+-identityʳ (a · p)) ⟨ + a *A b +A 0# ∷ (a · p + zeros n) + ≈⟨ consʳ (cast-p≈p (ℕ.⊔-idem n)) ⟨ + (a ∷ []) * (b ∷ p) ∎ + +1·p≈p : (p : Poly n) → 1# · p ≈ p +1·p≈p [] = refl +1·p≈p (a ∷ p) = cons (R.*-identityˡ a) (1·p≈p p) + + +pIsZero⇒a·pIsZero : (a : A) → (p : Poly n) → IsZero p → IsZero (a · p) +pIsZero⇒a·pIsZero a p [] = [] +pIsZero⇒a·pIsZero a (b ∷ p) (b≈0 ∷ p≈0) + = (R.trans (R.*-congˡ b≈0) (R.zeroʳ a)) ∷ pIsZero⇒a·pIsZero a p p≈0 + +a≈0⇒a·pIsZero : (a : A) → (p : Poly n) → a ≈A 0# → IsZero (a · p) +a≈0⇒a·pIsZero a [] a≈0 = [] +a≈0⇒a·pIsZero a (b ∷ p) a≈0 + = R.trans (R.*-congʳ a≈0) (R.zeroˡ b) ∷ (a≈0⇒a·pIsZero a p a≈0) + +·-cong : a ≈A b → p ≈ q → a · p ≈ b · q +·-cong {a = _} {b = b} _ ([]≈ q q≈0) + = sym (IsZero⇒≈0 (pIsZero⇒a·pIsZero b q q≈0)) +·-cong {a = a} {b = _} _ (≈[] p p≈0) + = IsZero⇒≈0 (pIsZero⇒a·pIsZero a p p≈0) +·-cong {a = _} {b = _} c≈d (cons a≈b p≈q) + = cons (R.*-cong c≈d a≈b) (·-cong c≈d p≈q) + +·-congˡ : a ≈A b → a · p ≈ b · p +·-congˡ a≈b = ·-cong a≈b refl + +·-congʳ : p ≈ q → a · p ≈ a · q +·-congʳ = ·-cong R.refl + +·-dist : a · (p + q) ≈ (a · p) + (a · q) +·-dist {p = []} {q = []} = refl +·-dist {p = []} {q = b ∷ q} = refl +·-dist {p = b ∷ p} {q = []} = refl +·-dist {a = a} {p = b ∷ p} {q = c ∷ q} = cons (R.distribˡ a b c) ·-dist + +·-assoc : a · (b · p) ≈ (a *A b) · p +·-assoc {p = []} = refl +·-assoc {a} {b} {p = c ∷ p} = cons (R.sym (R.*-assoc a b c)) ·-assoc + +a·-cong : p ≈ q → a · p ≈ a · q +a·-cong = ·-cong R.refl + +·-distrib-+A : (a b : A) → (p : Poly m) → (a +A b) · p ≈ a · p + b · p +·-distrib-+A a b [] = refl +·-distrib-+A a b (c ∷ p) = cons (R.distribʳ c a b) (·-distrib-+A a b p) + +----------------------------------------------------------------- +-- Properties of polynomial multiplication + +zeroˡ : (p : Poly m) → [] * p ≈ [] +zeroˡ p = zerosm≈zerosn + +zeroʳ : (p : Poly m) → p * [] ≈ [] +zeroʳ [] = refl +zeroʳ {m} (a ∷ p) = begin + (a ∷ p) * [] ≈⟨ cast-p≈p (cong pred n+1≡sucn+0) ⟩ + (a · []) + p * (0# ∷ []) ≈⟨ +-identityˡ (p * (0# ∷ [])) ⟩ + p * (0# ∷ []) ≈⟨ *-distrib-shift p [] ⟩ + 0# ∷ (p * []) ≈⟨ consʳ (zeroʳ p) ⟩ + 0# ∷ [] ≈⟨ zerosm≈zerosn ⟩ + [] ∎ + +pIsZero⇒p*qIsZero : (q : Poly n) → IsZero p → IsZero (p * q) +pIsZero⇒p*qIsZero {n} {p = []} q [] = zerosIsZero (pred n) +pIsZero⇒p*qIsZero {n} {suc m} {p = a ∷ p} q (a≈0 ∷ p≈0) + = cast-p≈0⇒p≈0 (cast-lem n m) + (All-p≈0∧q≈0⇒p+q≈0 (a≈0⇒a·pIsZero a q a≈0) (pIsZero⇒p*qIsZero (0# ∷ q) p≈0)) + +p≈[]⇒p*q≈[] : (q : Poly n) → p ≈ [] → p * q ≈ [] +p≈[]⇒p*q≈[] q p≈0 = IsZero⇒≈0 (pIsZero⇒p*qIsZero q (≈0⇒IsZero p≈0)) + +*-cong : {p : Poly m} → {q : Poly n} → {r : Poly k} → {s : Poly l} → + p ≈ q → r ≈ s → p * r ≈ q * s +*-cong {k = k} {q = q} {r} {s} ([]≈ q q≈0) r≈s = begin + [] * r ≈⟨ p≈[]⇒p*q≈[] r refl ⟩ + [] ≈⟨ p≈[]⇒p*q≈[] s (IsZero⇒≈0 q≈0) ⟨ + q * s ∎ +*-cong {k = k} {q = q} {r} {s} (≈[] p p≈0) r≈s = begin + p * r ≈⟨ p≈[]⇒p*q≈[] r (IsZero⇒≈0 p≈0) ⟩ + [] ≈⟨ zerosm≈zerosn ⟩ + [] * s ∎ +*-cong {n = suc n} {l = l} {a ∷ p} {b ∷ q} (cons a≈b p≈q) ([]≈ s s≈0) = begin + (a ∷ p) * [] + ≈⟨ cast-p≈p (cong pred n+1≡sucn+0) ⟩ + [] + p * (0# ∷ []) + ≈⟨ +-congʳ (*-cong (sym p≈q) (consʳ (IsZero⇒≈0 s≈0))) ⟨ + [] + q * (0# ∷ s) + ≈⟨ +-congˡ (zerosm≈zerosn) ⟩ + zeros l + q * (0# ∷ s) + ≈⟨ +-congˡ (IsZero⇒≈0 (pIsZero⇒a·pIsZero b s s≈0)) ⟨ + (b · s) + q * (0# ∷ s) + ≈⟨ cast-p≈p (cast-lem l n) ⟨ + (b ∷ q) * s + ∎ +*-cong {suc m} {k = k} {p = a ∷ p} {b ∷ q} (cons a≈b p≈q) (≈[] r s≈0) = begin + (a ∷ p) * r + ≈⟨ cast-p≈p (cast-lem k m) ⟩ + (a · r) + p * (0# ∷ r) + ≈⟨ +-congʳ (*-cong (sym p≈q) (consʳ ([]≈ r s≈0))) ⟨ + (a · r) + q * (0# ∷ []) + ≈⟨ +-congˡ (IsZero⇒≈0 (pIsZero⇒a·pIsZero a r s≈0)) ⟩ + zeros k + q * (0# ∷ []) + ≈⟨ +-congˡ zerosm≈zerosn ⟩ + (b · []) + q * (0# ∷ []) + ≈⟨ cast-p≈p (cong pred n+1≡sucn+0) ⟨ + (b ∷ q) * [] + ∎ +*-cong {suc m} {suc n} {suc k} {suc l} {a ∷ p} {b ∷ q} {c ∷ r} {d ∷ s} (cons a≈b p≈q) (cons c≈d r≈s) = begin + (a ∷ p) * (c ∷ r) + ≈⟨ cast-p≈p (cast-lem (suc k) m)⟩ + (a *A c ∷ a · r) + p * (0# ∷ c ∷ r) + ≈⟨ +-congˡ (consˡ (R.*-cong a≈b c≈d)) ⟩ + (b *A d ∷ a · r) + p * (0# ∷ c ∷ r) + ≈⟨ +-congˡ (consʳ (·-cong a≈b r≈s)) ⟩ + (b *A d ∷ b · s) + p * (0# ∷ c ∷ r) + ≈⟨ +-congʳ (*-cong p≈q (consʳ (cons c≈d r≈s))) ⟩ + (b *A d ∷ b · s) + q * (0# ∷ d ∷ s) + ≈⟨ cast-p≈p (cast-lem (suc l) n) ⟨ + (b ∷ q) * (d ∷ s) + ∎ + +*-congʳ : q ≈ r → p * q ≈ p * r +*-congʳ {p = p} q≈r = *-cong {p = p} refl q≈r + +*-congˡ : p ≈ q → p * r ≈ q * r +*-congˡ p≈q = *-cong p≈q refl + +qIsZero⇒p*qIsZero : (p : Poly m) → IsZero q → IsZero (p * q) +qIsZero⇒p*qIsZero {m} {q = []} p [] = ≈0⇒IsZero (zeroʳ p) +qIsZero⇒p*qIsZero {m} {suc n} {q = b ∷ q} p (b≈0 ∷ q≈0) + = ≈0⇒IsZero ( + begin + p * (b ∷ q) ≈⟨ *-congʳ {p = p} (consˡ b≈0) ⟩ + p * (0# ∷ q) ≈⟨ *-distrib-shift p q ⟩ + 0# ∷ (p * q) ≈⟨ consʳ (IsZero⇒≈0 (qIsZero⇒p*qIsZero p q≈0)) ⟩ + 0# ∷ (zeros m) ≈⟨ zerosm≈zerosn ⟩ + zeros m ∎ + ) + +q≈[]→p*q≈[] : (p : Poly n) → q ≈ [] → p * q ≈ [] +q≈[]→p*q≈[] p q≈0 = IsZero⇒≈0 (qIsZero⇒p*qIsZero p (≈0⇒IsZero q≈0)) + +shift-distrib-+ : (p : Poly m) → (q : Poly n) → + shift (p + q) ≈ (shift p) + (shift q) +shift-distrib-+ p q = cons (R.sym (R.+-identityʳ 0#)) refl + +*-identityʳ : (p : Poly n) → p * (1# ∷ []) ≈ p +*-identityʳ {0} [] = zerosm≈zerosn +*-identityʳ {suc n} (a ∷ p) = begin + (a ∷ p) * (1# ∷ []) + ≈⟨ cast-p≈p (cast-lem 1 n) ⟩ + (a *A 1# ∷ []) + (p * (0# ∷ 1# ∷ [])) + ≈⟨ +-congˡ (consˡ (R.*-identityʳ a)) ⟩ + (a ∷ []) + (p * (0# ∷ 1# ∷ [])) + ≈⟨ +-congʳ (*-distrib-shift p (1# ∷ [])) ⟩ + (a ∷ []) + (0# ∷ (p * (1# ∷ []))) + ≈⟨ cons (R.+-identityʳ a) (+-identityˡ (p * (1# ∷ []))) ⟩ + a ∷ (p * (1# ∷ [])) + ≈⟨ consʳ (*-identityʳ p) ⟩ + a ∷ p ∎ + +*-identityˡ : (p : Poly n) → (1# ∷ []) * p ≈ p +*-identityˡ [] = refl +*-identityˡ {suc n} (a ∷ p) = begin + (1# ∷ []) * (a ∷ p) + ≈⟨ consʳ (cast-p≈p (ℕ.⊔-idem n)) ⟩ + 1# · (a ∷ p) + [] * (0# ∷ a ∷ p) + ≈⟨ +-identityʳ {m = pred (suc (suc n))} (1# · (a ∷ p) + []) ⟩ + 1# · (a ∷ p) + [] + ≈⟨ +-identityʳ {m = 0} (1# · (a ∷ p)) ⟩ + 1# · (a ∷ p) + ≈⟨ cons (R.*-identityˡ a) (1·p≈p p) ⟩ + a ∷ p ∎ + +-- (0# ∷ 1# ∷ []) is the center of a polynomial ring +shiftp≈p*x : (p : Poly n) → shift p ≈ p * (0# ∷ 1# ∷ []) +shiftp≈p*x [] = refl +shiftp≈p*x {suc n} (a ∷ p) = begin + 0# ∷ a ∷ p + ≈⟨ cons (R.+-identityˡ 0#) (cons (R.+-identityʳ a) (+-identityˡ p)) ⟨ + (0# ∷ a ∷ []) + shift (shift p) + ≈⟨ consʳ (consʳ (+-congʳ (*-identityʳ p))) ⟨ + (0# ∷ a ∷ []) + (shift (shift (p * (1# ∷ [])))) + ≈⟨ +-congʳ {p = 0# ∷ a ∷ []} (consʳ (*-distrib-shift p (1# ∷ []))) ⟨ + (0# ∷ a ∷ []) + shift (p * shift (1# ∷ [])) + ≈⟨ +-congʳ {p = 0# ∷ a ∷ []} (*-distrib-shift p (0# ∷ 1# ∷ [])) ⟨ + (0# ∷ a ∷ []) + p * shift (shift (1# ∷ [])) + ≈⟨ +-congˡ (cons (R.zeroʳ a) (consˡ (R.*-identityʳ a))) ⟨ + a · (0# ∷ 1# ∷ []) + p * (0# ∷ 0# ∷ 1# ∷ []) + ≈⟨ cast-p≈p (cast-lem 2 n) ⟨ + (a ∷ p) * (0# ∷ 1# ∷ []) ∎ + +shiftp≈x*p : (p : Poly n) → shift p ≈ (0# ∷ 1# ∷ []) * p +shiftp≈x*p [] = consˡ (R.sym (R.trans (R.+-identityʳ (1# *A 0#)) (R.zeroʳ 1#))) +shiftp≈x*p {suc n} (a ∷ p) = begin + 0# ∷ a ∷ p + ≈⟨ *-identityˡ (0# ∷ a ∷ p) ⟨ + (1# ∷ []) * (0# ∷ a ∷ p) + ≈⟨ +-identityˡ {m = 0} ((1# ∷ []) * (0# ∷ a ∷ p)) ⟨ + [] + (1# ∷ []) * (0# ∷ a ∷ p) + ≈⟨ +-identityˡ {m = 0} ((1# ∷ []) * (0# ∷ a ∷ p)) ⟩ + (1# ∷ []) * (0# ∷ a ∷ p) + ≈⟨ +-idˡ (0# *A a ∷ 0# · p) ((1# ∷ []) * (0# ∷ a ∷ p)) + ((R.zeroˡ a) ∷ a≈0⇒a·pIsZero 0# p R.refl) ⟨ + 0# · (a ∷ p) + (1# ∷ []) * (0# ∷ a ∷ p) + ≈⟨ consʳ (cast-p≈p (ℕ.m≤n⇒m⊔n≡n (ℕ.n≤1+n n))) ⟨ + (0# ∷ 1# ∷ []) * (a ∷ p) ∎ + +·-distrib-* : (p : Poly m) → (q : Poly n) → (a : A) → + a · (p * q) ≈ (a · p) * q +·-distrib-* {_} {n} [] q a = begin + a · ([] * q) ≈⟨ ·-congʳ zerosm≈zerosn ⟩ + a · [] ≈⟨ zerosm≈zerosn ⟨ + (a · []) * q ∎ +·-distrib-* {suc m} {_} (b ∷ p) [] a = begin + a · ((b ∷ p) * []) + ≈⟨ a·-cong (cast-p≈p (cong pred n+1≡sucn+0)) ⟩ + a · ((b · []) + (p * (0# ∷ []))) + ≈⟨ a·-cong (+-identityˡ (p * (0# ∷ []))) ⟩ + a · (p * (0# ∷ [])) + ≈⟨ a·-cong (q≈[]→p*q≈[] p zerosm≈zerosn) ⟩ + [] + ≈⟨ q≈[]→p*q≈[] ((a · p)) zerosm≈zerosn ⟨ + (a · p) * (0# ∷ []) + ≈⟨ +-identityˡ ((a · p) * (0# ∷ [])) ⟨ + ((a *A b) · []) + ((a · p) * (0# ∷ [])) + ≈⟨ cast-p≈p (cong pred n+1≡sucn+0) ⟨ + (a · (b ∷ p)) * [] + ∎ +·-distrib-* {suc m} {suc n} (b ∷ p) (c ∷ q) a = begin + a · ((b ∷ p) * (c ∷ q)) + ≈⟨ a·-cong (cast-p≈p (cast-lem (suc n) m)) ⟩ + a · ((b · (c ∷ q)) + (p * (0# ∷ c ∷ q))) + ≈⟨ ·-dist ⟩ + a · (b *A c ∷ (b · q)) + a · (p * (0# ∷ c ∷ q)) + ≈⟨ +-congˡ (cons (R.sym (R.*-assoc a b c)) ·-assoc) ⟩ + (a *A b *A c ∷ ((a *A b) · q)) + a · (p * (0# ∷ c ∷ q)) + ≈⟨ +-congʳ (·-distrib-* p (0# ∷ c ∷ q) a) ⟩ + (a *A b) · (c ∷ q) + (a · p) * (0# ∷ c ∷ q) + ≈⟨ cast-p≈p (cast-lem (suc n) m) ⟨ + (a · (b ∷ p)) * (c ∷ q) + ∎ + +0∷[p*q]≈[0∷p]*q : (p : Poly m) → (q : Poly n) → + shift (p * q) ≈ (shift p) * q +0∷[p*q]≈[0∷p]*q {n = n} [] q = begin + shift ([] * q) + ≈⟨ consʳ zerosm≈zerosn ⟩ + shift [] + ≈⟨ IsZero⇒≈0 (All-p≈0∧q≈0⇒p+q≈0 (a≈0⇒a·pIsZero 0# q R.refl) + (≈0⇒IsZero {m = n} zerosm≈zerosn)) ⟨ + 0# · q + zeros (pred (suc n)) + ≈⟨ cast-p≈p (ℕ.⊔-idem (pred (1 ℕ.+ n))) ⟨ + shift [] * q ∎ +0∷[p*q]≈[0∷p]*q {m = suc m} {n = n} (a ∷ p) (q) = begin + shift ((a ∷ p) * q) + ≈⟨ *-distrib-shift (a ∷ p) q ⟨ + (a ∷ p) * shift q + ≈⟨ cast-p≈p (cast-lem (suc n) m) ⟩ + a · shift q + p * (0# ∷ shift q) + ≈⟨ +-idˡ (0# · q) (a · (0# ∷ q) + p * (0# ∷ 0# ∷ q)) + (a≈0⇒a·pIsZero 0# q R.refl) ⟨ + 0# · q + (a · (0# ∷ q) + p * (0# ∷ 0# ∷ q)) + ≈⟨ +-congʳ (cast-p≈p (cast-lem (suc n) m)) ⟨ + 0# · q + (a ∷ p) * (0# ∷ q) + ≈⟨ cast-p≈p (cast-lem n (suc m)) ⟨ + shift (a ∷ p) * q ∎ + +*-distribˡ-+ : (p : Poly m) → (q : Poly n) → (r : Poly k) → + p * (q + r) ≈ p * q + p * r +*-distribˡ-+ [] q r = begin + [] * (q + r) + ≈⟨ zerosm≈zerosn ⟩ + [] + ≈⟨ IsZero⇒≈0 (All-p≈0∧q≈0⇒p+q≈0 (≈0⇒IsZero refl) (≈0⇒IsZero refl)) ⟨ + [] * q + [] * r ∎ +*-distribˡ-+ {m = suc m} {n = n} {k = k} (a ∷ p) q r = begin + (a ∷ p) * (q + r) + ≈⟨ cast-p≈p (cast-lem (n ⊔ k) m) ⟩ + a · (q + r) + p * (0# ∷ q + r) + ≈⟨ +-cong ·-dist (*-distrib-shift p (q + r)) ⟩ + (a · q + a · r) + (0# ∷ (p * (q + r))) + ≈⟨ +-congʳ (consʳ (*-distribˡ-+ p q r)) ⟩ + (a · q + a · r) + (0# ∷ (p * q + p * r)) + ≈⟨ +-congʳ (consˡ (R.+-identityʳ 0#)) ⟨ + (a · q + a · r) + ((0# ∷ (p * q)) + (0# ∷ (p * r))) + ≈⟨ middleFour (a · q) (a · r) (0# ∷ p * q) (0# ∷ p * r) ⟩ + ((a · q) + (0# ∷ (p * q))) + ((a · r) + (0# ∷ (p * r))) + ≈⟨ +-cong (+-congʳ (*-distrib-shift p q)) (+-congʳ (*-distrib-shift p r)) ⟨ + (a · q + p * (0# ∷ q)) + (a · r + p * (0# ∷ r)) + ≈⟨ +-cong (cast-p≈p (cast-lem n m)) (cast-p≈p (cast-lem k m)) ⟨ + (a ∷ p) * q + (a ∷ p) * r + ∎ + +*-distribʳ-+ : (p : Poly m) → (q : Poly n) → (r : Poly k) → + (q + r) * p ≈ (q * p) + (r * p) +*-distribʳ-+ {m = m} p [] [] = sym (+-identityʳ (zeros (m ℕ.∸ 1))) +*-distribʳ-+ {m = m} {k = suc k} p [] (c ∷ r) = begin + ([] + (c ∷ r)) * p + ≈⟨ cast-p≈p (cast-lem m k) ⟩ + c · p + r * (0# ∷ p) + ≈⟨ cast-p≈p (cast-lem m k) ⟨ + (c ∷ r) * p + ≈⟨ +-identityˡ ((c ∷ r) * p) ⟨ + [] * p + (c ∷ r) * p + ∎ +*-distribʳ-+ {m = m} {n = suc n} p (b ∷ q) [] = begin + ((b ∷ q) + []) * p + ≈⟨ cast-p≈p (cast-lem m n) ⟩ + b · p + q * (0# ∷ p) + ≈⟨ cast-p≈p (cast-lem m n) ⟨ + (b ∷ q) * p + ≈⟨ +-identityʳ ((b ∷ q) * p) ⟨ + (b ∷ q) * p + [] * p + ∎ +*-distribʳ-+ {m} {suc n} {suc k} p (b ∷ q) (c ∷ r) = begin + ((b ∷ q) + (c ∷ r)) * p + ≈⟨ cast-p≈p (cast-lem m (n ⊔ k)) ⟩ + (b +A c) · p + (q + r) * (0# ∷ p) + ≈⟨ +-cong (·-distrib-+A b c p) (*-distribʳ-+ (0# ∷ p) q r) ⟩ + ((b · p) + (c · p)) + (q * (0# ∷ p) + r * (0# ∷ p)) + ≈⟨ middleFour (b · p) (c · p) (q * (0# ∷ p)) (r * (0# ∷ p)) ⟩ + (b · p + q * (0# ∷ p)) + (c · p + r * (0# ∷ p)) + ≈⟨ +-cong (cast-p≈p (cast-lem m n)) (cast-p≈p (cast-lem m k)) ⟨ + (b ∷ q) * p + (c ∷ r) * p + ∎ + +*-assoc : (p : Poly m) → (q : Poly n) → (r : Poly k) → + (p * q) * r ≈ p * (q * r) +*-assoc {n = n} {k} [] q r = begin + zeros (n ℕ.∸ 1) * r + ≈⟨ p≈[]⇒p*q≈[] r (IsZero⇒≈0 (zerosIsZero (n ℕ.∸ 1))) ⟩ + [] + ≈⟨ zerosm≈zerosn ⟩ + zeros (pred (0 ℕ.+ pred (n ℕ.+ k))) + ∎ +*-assoc {suc m} {n} {k} (a ∷ p) q r = begin + ((a ∷ p) * q) * r + ≈⟨ *-congˡ (cast-p≈p (cast-lem n m)) ⟩ + ((a · q) + (p * (0# ∷ q))) * r + ≈⟨ *-congˡ (+-congʳ {p = a · q} (*-distrib-shift p q)) ⟩ + ((a · q) + (0# ∷ (p * q))) * r + ≈⟨ *-distribʳ-+ r (a · q) (0# ∷ p * q) ⟩ + ((a · q) * r) + ((0# ∷ (p * q)) * r) + ≈⟨ +-congʳ step1 ⟨ + ((a · q) * r) + (0# ∷ (p * (q * r))) + ≈⟨ +-congˡ (·-distrib-* q r a) ⟨ + (a · (q * r)) + (0# ∷ (p * (q * r))) + ≈⟨ +-congʳ (*-distrib-shift p (q * r)) ⟨ + (a · (q * r)) + (p * (0# ∷ (q * r))) + ≈⟨ cast-p≈p (cast-lem (pred (n ℕ.+ k)) m) ⟨ + (a ∷ p) * (q * r) + ∎ + where + step1 = begin + 0# ∷ (p * (q * r)) + ≈⟨ consʳ (*-assoc p q r) ⟨ + 0# ∷ ((p * q) * r) + ≈⟨ 0∷[p*q]≈[0∷p]*q (p * q) r ⟩ + (0# ∷ (p * q)) * r + ≈⟨ cast-p≈p (cast-lem k (m ℕ.+ n ℕ.∸ 1)) ⟩ + (0# · r) + ((p * q) * (0# ∷ r)) + ≈⟨ +-congˡ (IsZero⇒≈0 (a≈0⇒a·pIsZero 0# r R.refl) ) ⟩ + zeros k + ((p * q) * (0# ∷ r)) + ≈⟨ +-congʳ (*-distrib-shift (p * q) r) ⟩ + zeros k + (0# ∷ ((p * q) * r)) + ≈⟨ +-congʳ (0∷[p*q]≈[0∷p]*q (p * q) r) ⟩ + zeros k + ((0# ∷ (p * q)) * r) + ≈⟨ +-identityˡ ((0# ∷ (p * q)) * r) ⟩ + (0# ∷ (p * q)) * r + ∎ + + diff --git a/src/Algebra/Polynomial/Poly/Properties2.agda b/src/Algebra/Polynomial/Poly/Properties2.agda new file mode 100644 index 0000000000..56c7f0612c --- /dev/null +++ b/src/Algebra/Polynomial/Poly/Properties2.agda @@ -0,0 +1,663 @@ +open import Algebra.Bundles using (CommutativeRing) + +module Algebra.Polynomial.Poly.Properties2 + {ℓ₁ ℓ₂} (R : CommutativeRing ℓ₁ ℓ₂) + where + +open import Algebra.Polynomial.Poly.Base2 R as P + using ( Poly; _+_ ; _*_ ; _·_ ; -_; shift; _≈_; refl; trans; sym; zeros + ; IsZero; []≈ ; ≈[]; cons; zeros-unique; consˡ; consʳ; cast-lem) +open import Algebra.Properties.Ring +open import Data.Nat.Base as ℕ using (ℕ; suc; pred; _⊔_) +import Data.Nat.Properties as ℕ +open import Data.Vec.Base as Vec using (Vec; []; _∷_) +open import Data.Vec.Relation.Unary.All using (All ; []; _∷_; head; tail) +import Level as L +open import Relation.Binary +open import Relation.Binary.PropositionalEquality as Eq + using (_≡_; module ≡-Reasoning) +open import Relation.Binary.PropositionalEquality.Core using (cong) + +module CR = CommutativeRing R +open CR + renaming + ( Carrier to A + ; _≈_ to _≈A_ + ; _+_ to _+A_ + ; _*_ to _*A_ + ; -_ to -A_) + using (0#; 1#) + +private + variable + m n k l : ℕ + a b c d : A + p : Poly m + q : Poly n + r : Poly k + s : Poly l + +--------------------------------------------------------------------- +-- Equational reasoning for Poly n and Poly m +-- where m is not necesarily the same as n +private + + infix 4 _IsRelatedTo_ + + data _IsRelatedTo_ (p : Poly m) (q : Poly n) : Set (ℓ₁ L.⊔ ℓ₂) where + relTo : (p≈q : p ≈ q) → p IsRelatedTo q + + start : _IsRelatedTo_ {m} {n} ⇒ _≈_ + start (relTo p≈q) = p≈q + + ∼-go : Trans (_≈_) (_IsRelatedTo_ {n} {k}) (_IsRelatedTo_ {m} {k}) + ∼-go p≈q (relTo q≈r) = relTo (trans p≈q q≈r) + + stop : Reflexive (_IsRelatedTo_ {m} {m}) + stop = relTo refl + + forward : (p : Poly m) → q IsRelatedTo r → p ≈ q → p IsRelatedTo r + forward p qRr p≈q = ∼-go p≈q qRr + + backward : (p : Poly m) → q IsRelatedTo r → q ≈ p → p IsRelatedTo r + backward p qRr q≈p = ∼-go (sym q≈p) qRr + + infix 1 begin_ + begin_ : p IsRelatedTo q → p ≈ q + begin_ = start + + infixr 2 step-∼-⟩ + step-∼-⟩ = forward + syntax step-∼-⟩ p qRr p≈q = p ≈⟨ p≈q ⟩ qRr + + infixr 2 step-∼-⟨ + step-∼-⟨ = backward + syntax step-∼-⟨ p qRr q≈p = p ≈⟨ q≈p ⟨ qRr + + infix 3 _∎ + _∎ : (p : Poly m) → p IsRelatedTo p + p ∎ = stop + +----------------------------------------------------------------- +-- Properties of zero polynomial + +zerosIsZero : (n : ℕ) → IsZero (zeros n) +zerosIsZero 0 = [] +zerosIsZero (suc n) = CR.refl ∷ (zerosIsZero n) + +zerosm≈zerosn : zeros m ≈ zeros n +zerosm≈zerosn {m} {n} = zeros-unique (zerosIsZero m) (zerosIsZero n) + +≈0⇒IsZero : p ≈ zeros m → IsZero p +≈0⇒IsZero ([]≈ zeros zeros≈0) = [] +≈0⇒IsZero (≈[] p p≈0) = p≈0 +≈0⇒IsZero (cons a≈0 p≈0) = a≈0 ∷ ≈0⇒IsZero p≈0 + +IsZero⇒≈0 : IsZero p → p ≈ zeros m +IsZero⇒≈0 {m = m} p≈0 = zeros-unique p≈0 (zerosIsZero m) + +All-p≈0∧q≈0⇒p+q≈0 : All (_≈A 0#) p → All (_≈A 0#) q → All (_≈A 0#) (p + q) +All-p≈0∧q≈0⇒p+q≈0 {p = _} {q = _} [] [] = [] +All-p≈0∧q≈0⇒p+q≈0 {p = _} {q = _} [] (b≈0 ∷ q≈0) = b≈0 ∷ q≈0 +All-p≈0∧q≈0⇒p+q≈0 {p = _} {q = _} (a≈0 ∷ p≈0) [] = a≈0 ∷ p≈0 +All-p≈0∧q≈0⇒p+q≈0 {p = a ∷ p} {q = b ∷ q} (a≈0 ∷ p≈0) (b≈0 ∷ q≈0) + = CR.trans (CR.+-cong a≈0 b≈0) (CR.+-identityˡ 0#) ∷ All-p≈0∧q≈0⇒p+q≈0 p≈0 q≈0 + +------------------------------------------------------ +-- Additive inverse + +[-p]+pIsZero : {p : Poly m} → IsZero ((- p) + p) +[-p]+pIsZero {p = []} = [] +[-p]+pIsZero {p = a ∷ p} = CR.-‿inverseˡ a ∷ [-p]+pIsZero + +p+[-p]IsZero : {p : Poly m} → IsZero (p + (- p)) +p+[-p]IsZero {p = []} = [] +p+[-p]IsZero {p = a ∷ p} = CR.-‿inverseʳ a ∷ p+[-p]IsZero + ++-inverseˡ : (p : Poly m) → (- p) + p ≈ [] ++-inverseˡ [] = refl ++-inverseˡ (a ∷ p) + = ≈[] ((- (a ∷ p)) + (a ∷ p)) (CR.-‿inverseˡ a ∷ [-p]+pIsZero) + ++-inverseʳ : (p : Poly m) → p + (- p) ≈ [] ++-inverseʳ [] = refl ++-inverseʳ (a ∷ p) + = ≈[] ((a ∷ p) + (- (a ∷ p))) ((CR.-‿inverseʳ a) ∷ p+[-p]IsZero) + +------------------------------------------------------- +-- Negation is congruent + +-⁺ : IsZero p → IsZero (- p) +-⁺ [] = [] +-⁺ (a≈0 ∷ p≈0) = x≈ε⇒x⁻¹≈ε CR.ring a≈0 ∷ (-⁺ p≈0) + +-⁻ : IsZero (- p) → IsZero p +-⁻ {p = []} -p≈0 = -p≈0 +-⁻ {p = a ∷ p} (-a≈0 ∷ -p≈0) = x⁻¹≈ε⇒x≈ε CR.ring -a≈0 ∷ (-⁻ -p≈0) + +-‿cong : p ≈ q → - p ≈ - q +-‿cong ([]≈ q q≈0) = []≈ (- q) (-⁺ q≈0) +-‿cong (≈[] p p≈0) = ≈[] (- p) (-⁺ p≈0) +-‿cong (cons a≈b p≈q) = cons (CR.-‿cong a≈b) (-‿cong p≈q) + +----------------------------------------------------- +-- Properties of polynomial addition + ++-comm : (p : Poly m) → (q : Poly n) → p + q ≈ q + p ++-comm [] [] = refl ++-comm [] (a ∷ p) = refl ++-comm (a ∷ p) [] = refl ++-comm (a ∷ p) (b ∷ q) = cons (CR.+-comm a b) (+-comm p q) + ++-idʳ : (p : Poly n) → (q : Poly m) → IsZero q → p + q ≈ p ++-idʳ [] q [] = refl ++-idʳ (a ∷ p) q [] = refl ++-idʳ [] (a ∷ q) (a≈0 ∷ q≈0) = ≈[] (a ∷ q) (a≈0 ∷ q≈0) ++-idʳ (a ∷ p) (b ∷ q) (b≈0 ∷ q≈0) + = cons (CR.trans (CR.+-congˡ b≈0) (CR.+-identityʳ a)) (+-idʳ p q q≈0) + ++-idˡ : (p : Poly n) → (q : Poly m) → IsZero p → p + q ≈ q ++-idˡ p q p≈0 = begin + p + q ≈⟨ +-comm p q ⟩ + q + p ≈⟨ +-idʳ q p p≈0 ⟩ + q ∎ + ++-identityʳ : (p : Poly n) → p + (zeros m) ≈ p ++-identityʳ {m = m} p = +-idʳ p (zeros m) (zerosIsZero m) + ++-identityˡ : (p : Poly n) → (zeros m) + p ≈ p ++-identityˡ {m = m} p = +-idˡ (zeros m) p (zerosIsZero m) + ++-cong : p ≈ q → r ≈ s → p + r ≈ q + s ++-cong {p = _} {q = _} {r = r} {s = s} ([]≈ q q≈0) r≈s = begin + [] + r ≈⟨ +-identityˡ r ⟩ + r ≈⟨ r≈s ⟩ + s ≈⟨ +-idˡ q s q≈0 ⟨ + q + s ∎ ++-cong {p = _} {q = _} {r = r} {s = s} (≈[] p p≈0) r≈s = begin + p + r ≈⟨ +-idˡ p r p≈0 ⟩ + r ≈⟨ r≈s ⟩ + s ≈⟨ +-identityˡ s ⟨ + [] + s ∎ ++-cong {p = a ∷ p} {q = b ∷ q} {r = _} {s = s} (cons a≈b p≈q) ([]≈ s s≈0) = begin + a ∷ p ≈⟨ cons a≈b p≈q ⟩ + b ∷ q ≈⟨ +-idʳ (b ∷ q) s s≈0 ⟨ + (b ∷ q) + s ∎ ++-cong {p = a ∷ p} {q = b ∷ q} {r = r} {s = _} (cons a≈b p≈q) (≈[] r r≈0) = begin + (a ∷ p) + r ≈⟨ +-idʳ (a ∷ p) r r≈0 ⟩ + a ∷ p ≈⟨ cons a≈b p≈q ⟩ + b ∷ q ∎ ++-cong (cons a≈b p≈q) (cons c≈d r≈s) + = cons (CR.+-cong a≈b c≈d) (+-cong p≈q r≈s) + ++-congˡ : p ≈ q → p + r ≈ q + r ++-congˡ p≈q = +-cong p≈q refl + ++-congʳ : q ≈ r → p + q ≈ p + r ++-congʳ q≈r = +-cong refl q≈r + ++-assoc : (p : Poly m) → (q : Poly n) → (r : Poly k) → + (p + q) + r ≈ p + (q + r) ++-assoc [] q r = begin + ([] + q) + r ≈⟨ +-congˡ (+-identityˡ q) ⟩ + q + r ≈⟨ +-identityˡ (q + r) ⟨ + [] + (q + r) ∎ ++-assoc (a ∷ p) [] r = +-congʳ (sym (+-identityˡ r)) ++-assoc (a ∷ p) (b ∷ q) [] = refl ++-assoc (a ∷ p) (b ∷ q) (c ∷ r) + = cons (CR.+-assoc a b c) (+-assoc p q r) + +middleFour : (p : Poly m) → (q : Poly n) → (r : Poly k) → (w : Poly l) → + (p + q) + (r + w) ≈ (p + r) + (q + w) +middleFour p q r w = begin + (p + q) + (r + w) ≈⟨ +-assoc (p + q) r w ⟨ + (p + q + r) + w ≈⟨ +-congˡ (+-assoc p q r) ⟩ + (p + (q + r)) + w ≈⟨ +-congˡ (+-congʳ (+-comm q r)) ⟩ + (p + (r + q)) + w ≈⟨ +-congˡ (+-assoc p r q) ⟨ + (p + r + q) + w ≈⟨ +-assoc (p + r) q w ⟩ + (p + r) + (q + w) ∎ + +------------------------------------------------------------------ +-- Vector casting lemmas + +private + n+1≡sucn+0 : (n ℕ.+ 1) ≡ suc (n ℕ.+ 0) + n+1≡sucn+0 {0} = Eq.refl + n+1≡sucn+0 {suc n} = cong suc n+1≡sucn+0 + + cast-p≈0⇒p≈0 : (m≡n : m ≡ n) → All (_≈A 0#) p → + All (_≈A 0#) (Vec.cast m≡n p) + cast-p≈0⇒p≈0 {n = 0} {[]} m≡n [] = [] + cast-p≈0⇒p≈0 {n = suc n} {a ∷ p} m≡n (a≈0 ∷ p≈0) + = a≈0 ∷ cast-p≈0⇒p≈0 (cong pred m≡n) p≈0 + +cast-p≈p : (m≡n : m ≡ n) → Vec.cast m≡n p ≈ p +cast-p≈p {n = 0} {[]} Eq.refl = refl +cast-p≈p {n = suc n} {a ∷ p} m≡n = consʳ (cast-p≈p (cong pred m≡n)) + +------------------------------------------------------------------ +-- Properties of polynomial shifting + +*-distrib-shift : (p : Poly m) → (q : Poly n) → + p * (shift q) ≈ shift (p * q) +*-distrib-shift {_} {_} [] qs = zerosm≈zerosn +*-distrib-shift {suc m} {n} (a ∷ p) q = begin + (a ∷ p) * (0# ∷ q) + ≈⟨ cast-p≈p (cast-lem (suc n) m) ⟩ + a · (0# ∷ q) + p * (0# ∷ 0# ∷ q) + ≈⟨ +-congˡ (consˡ (CR.zeroʳ a)) ⟩ + (0# ∷ a · q) + p * (0# ∷ 0# ∷ q) + ≈⟨ +-congʳ (*-distrib-shift p (0# ∷ q)) ⟩ + (0# ∷ a · q) + (0# ∷ (p * (0# ∷ q))) + ≈⟨ consˡ (CR.+-identityˡ 0#) ⟩ + 0# ∷ (a · q + p * (0# ∷ q)) + ≈⟨ consʳ (cast-p≈p (cast-lem n m)) ⟨ + 0# ∷ ((a ∷ p) * q) + ∎ + +·-distrib-shift : (a : A) → (p : Poly m) → a · (shift p) ≈ shift (a · p) +·-distrib-shift a [] = cons (CR.zeroʳ a) (refl) +·-distrib-shift a (b ∷ p) = consˡ (CR.zeroʳ a) + +---------------------------------------------------------------- +-- Properties of polynomial scaling + +a·p≈a∷[]*p : (a : A) → (p : Poly n) → a · p ≈ (a ∷ []) * p +a·p≈a∷[]*p {_} a [] = refl +a·p≈a∷[]*p {suc n} a (b ∷ p) = begin + a · (b ∷ p) + ≈⟨ cons (CR.+-identityʳ (a *A b)) (+-identityʳ (a · p)) ⟨ + a *A b +A 0# ∷ (a · p + zeros n) + ≈⟨ consʳ (cast-p≈p (ℕ.⊔-idem n)) ⟨ + (a ∷ []) * (b ∷ p) ∎ + +pIsZero⇒a·pIsZero : (a : A) → (p : Poly n) → IsZero p → IsZero (a · p) +pIsZero⇒a·pIsZero a p [] = [] +pIsZero⇒a·pIsZero a (b ∷ p) (b≈0 ∷ p≈0) + = (CR.trans (CR.*-congˡ b≈0) (CR.zeroʳ a)) ∷ pIsZero⇒a·pIsZero a p p≈0 + +a≈0⇒a·pIsZero : (a : A) → (p : Poly n) → a ≈A 0# → IsZero (a · p) +a≈0⇒a·pIsZero a [] a≈0 = [] +a≈0⇒a·pIsZero a (b ∷ p) a≈0 + = CR.trans (CR.*-congʳ a≈0) (CR.zeroˡ b) ∷ (a≈0⇒a·pIsZero a p a≈0) + +·-cong : a ≈A b → p ≈ q → a · p ≈ b · q +·-cong {a = _} {b = b} _ ([]≈ q q≈0) + = sym (IsZero⇒≈0 (pIsZero⇒a·pIsZero b q q≈0)) +·-cong {a = a} {b = _} _ (≈[] p p≈0) + = IsZero⇒≈0 (pIsZero⇒a·pIsZero a p p≈0) +·-cong {a = _} {b = _} c≈d (cons a≈b p≈q) + = cons (CR.*-cong c≈d a≈b) (·-cong c≈d p≈q) + +·-congˡ : a ≈A b → a · p ≈ b · p +·-congˡ a≈b = ·-cong a≈b refl + +·-congʳ : p ≈ q → a · p ≈ a · q +·-congʳ = ·-cong CR.refl + +·-dist : a · (p + q) ≈ (a · p) + (a · q) +·-dist {a = _} {p = []} {q = []} = refl +·-dist {a = _} {p = []} {q = b ∷ q} = refl +·-dist {a = _} {p = b ∷ p} {q = []} = refl +·-dist {a = a} {p = b ∷ p} {q = c ∷ q} = cons (CR.distribˡ a b c) ·-dist + +·-assoc : a · (b · p) ≈ (a *A b) · p +·-assoc {_} {_} {p = []} = refl +·-assoc {a} {b} {p = c ∷ p} = cons (CR.sym (CR.*-assoc a b c)) ·-assoc + +a·-cong : p ≈ q → a · p ≈ a · q +a·-cong = ·-cong CR.refl + +----------------------------------------------------------------- +-- Properties of polynomial multiplication + +zeroˡ : (p : Poly m) → [] * p ≈ [] +zeroˡ p = zerosm≈zerosn + +zeroʳ : (p : Poly m) → p * [] ≈ [] +zeroʳ {_} [] = refl +zeroʳ {m} (a ∷ p) = begin + (a ∷ p) * [] ≈⟨ cast-p≈p (cong pred n+1≡sucn+0) ⟩ + (a · []) + p * (0# ∷ []) ≈⟨ +-identityˡ (p * (0# ∷ [])) ⟩ + p * (0# ∷ []) ≈⟨ *-distrib-shift p [] ⟩ + 0# ∷ (p * []) ≈⟨ consʳ (zeroʳ p) ⟩ + 0# ∷ [] ≈⟨ zerosm≈zerosn ⟩ + [] ∎ + +pIsZero⇒p*qIsZero : (q : Poly n) → IsZero p → IsZero (p * q) +pIsZero⇒p*qIsZero {n} {_} {p = []} q [] = zerosIsZero (pred n) +pIsZero⇒p*qIsZero {n} {suc m} {p = a ∷ p} q (a≈0 ∷ p≈0) + = cast-p≈0⇒p≈0 (cast-lem n m) + (All-p≈0∧q≈0⇒p+q≈0 (a≈0⇒a·pIsZero a q a≈0) (pIsZero⇒p*qIsZero (0# ∷ q) p≈0)) + +p≈[]⇒p*q≈[] : (q : Poly n) → p ≈ [] → p * q ≈ [] +p≈[]⇒p*q≈[] q p≈0 = IsZero⇒≈0 (pIsZero⇒p*qIsZero q (≈0⇒IsZero p≈0)) + +*-cong : {p : Poly m} → {q : Poly n} → {r : Poly k} → {s : Poly l} → + p ≈ q → r ≈ s → p * r ≈ q * s +*-cong {k = k} {q = q} {r} {s} ([]≈ q q≈0) r≈s = begin + [] * r ≈⟨ p≈[]⇒p*q≈[] r refl ⟩ + [] ≈⟨ p≈[]⇒p*q≈[] s (IsZero⇒≈0 q≈0) ⟨ + q * s ∎ +*-cong {k = k} {q = q} {r} {s} (≈[] p p≈0) r≈s = begin + p * r ≈⟨ p≈[]⇒p*q≈[] r (IsZero⇒≈0 p≈0) ⟩ + [] ≈⟨ zerosm≈zerosn ⟩ + [] * s ∎ +*-cong {n = suc n} {l = l} {a ∷ p} {b ∷ q} (cons a≈b p≈q) ([]≈ s s≈0) = begin + (a ∷ p) * [] + ≈⟨ cast-p≈p (cong pred n+1≡sucn+0) ⟩ + [] + p * (0# ∷ []) + ≈⟨ +-congʳ (*-cong (sym p≈q) (consʳ (IsZero⇒≈0 s≈0))) ⟨ + [] + q * (0# ∷ s) + ≈⟨ +-congˡ (zerosm≈zerosn) ⟩ + zeros l + q * (0# ∷ s) + ≈⟨ +-congˡ (IsZero⇒≈0 (pIsZero⇒a·pIsZero b s s≈0)) ⟨ + (b · s) + q * (0# ∷ s) + ≈⟨ cast-p≈p (cast-lem l n) ⟨ + (b ∷ q) * s + ∎ +*-cong {suc m} {k = k} {p = a ∷ p} {b ∷ q} (cons a≈b p≈q) (≈[] r s≈0) = begin + (a ∷ p) * r + ≈⟨ cast-p≈p (cast-lem k m) ⟩ + (a · r) + p * (0# ∷ r) + ≈⟨ +-congʳ (*-cong (sym p≈q) (consʳ ([]≈ r s≈0))) ⟨ + (a · r) + q * (0# ∷ []) + ≈⟨ +-congˡ (IsZero⇒≈0 (pIsZero⇒a·pIsZero a r s≈0)) ⟩ + zeros k + q * (0# ∷ []) + ≈⟨ +-congˡ zerosm≈zerosn ⟩ + (b · []) + q * (0# ∷ []) + ≈⟨ cast-p≈p (cong pred n+1≡sucn+0) ⟨ + (b ∷ q) * [] + ∎ +*-cong {suc m} {suc n} {suc k} {suc l} {a ∷ p} {b ∷ q} {c ∷ r} {d ∷ s} (cons a≈b p≈q) (cons c≈d r≈s) = begin + (a ∷ p) * (c ∷ r) + ≈⟨ cast-p≈p (cast-lem (suc k) m)⟩ + (a *A c ∷ a · r) + p * (0# ∷ c ∷ r) + ≈⟨ +-congˡ (consˡ (CR.*-cong (CR.sym a≈b) (CR.sym c≈d))) ⟨ + (b *A d ∷ a · r) + p * (0# ∷ c ∷ r) + ≈⟨ +-congˡ (consʳ ((·-cong (CR.sym a≈b) (sym r≈s)))) ⟨ + (b *A d ∷ b · s) + p * (0# ∷ c ∷ r) + ≈⟨ +-congʳ (*-cong p≈q (consʳ (cons c≈d r≈s))) ⟩ + (b *A d ∷ b · s) + q * (0# ∷ d ∷ s) + ≈⟨ cast-p≈p (cast-lem (suc l) n) ⟨ + (b ∷ q) * (d ∷ s) + ∎ + +*-congʳ : q ≈ r → p * q ≈ p * r +*-congʳ {p = p} q≈r = *-cong {p = p} refl q≈r + +*-congˡ : p ≈ q → p * r ≈ q * r +*-congˡ p≈q = *-cong p≈q refl + +qIsZero⇒p*qIsZero : (p : Poly m) → IsZero q → IsZero (p * q) +qIsZero⇒p*qIsZero {m} {_} {q = []} p [] = ≈0⇒IsZero (zeroʳ p) +qIsZero⇒p*qIsZero {m} {suc n} {q = b ∷ q} p (b≈0 ∷ q≈0) + = ≈0⇒IsZero ( + begin + p * (b ∷ q) ≈⟨ *-congʳ {p = p} (consˡ b≈0) ⟩ + p * (0# ∷ q) ≈⟨ *-distrib-shift p q ⟩ + 0# ∷ (p * q) ≈⟨ consʳ (IsZero⇒≈0 (qIsZero⇒p*qIsZero p q≈0)) ⟩ + 0# ∷ (zeros m) ≈⟨ zerosm≈zerosn ⟩ + zeros m ∎ + ) + +q≈[]→p*q≈[] : (p : Poly n) → q ≈ [] → p * q ≈ [] +q≈[]→p*q≈[] p q≈0 = IsZero⇒≈0 (qIsZero⇒p*qIsZero p (≈0⇒IsZero q≈0)) + +*-comm : (p : Poly m) → (q : Poly n) → p * q ≈ q * p +*-comm {_} {_} [] [] = refl +*-comm {_} {suc n} [] (b ∷ q) = sym ( begin + (b ∷ q) * [] + ≈⟨ cast-p≈p (cong pred n+1≡sucn+0) ⟩ + [] + (q * (0# ∷ [])) + ≈⟨ +-congʳ (q≈[]→p*q≈[] q zerosm≈zerosn) ⟩ + [] + [] + ≈⟨ zerosm≈zerosn ⟩ + zeros (pred (0 ℕ.+ suc n)) + ∎) +*-comm {suc m} {_} (a ∷ p) [] = begin + (a ∷ p) * [] + ≈⟨(cast-p≈p (cong pred n+1≡sucn+0))⟩ + [] + p * (0# ∷ []) + ≈⟨ +-congʳ (q≈[]→p*q≈[] p zerosm≈zerosn) ⟩ + [] + [] + ≈⟨ zerosm≈zerosn ⟩ + zeros (pred (0 ℕ.+ suc m)) + ∎ +*-comm {suc m} {suc n} (a ∷ p) (b ∷ q) = begin + (a ∷ p) * (b ∷ q) + ≈⟨ cast-p≈p (cast-lem (suc n) m) ⟩ + a · (b ∷ q) + p * (0# ∷ b ∷ q) + ≈⟨ +-congˡ (*-comm-lem (a *A b) a) ⟩ + (a *A b ∷ []) + a · (0# ∷ q) + p * (0# ∷ b ∷ q) + ≈⟨ +-congˡ (consˡ (CR.+-congʳ (CR.*-comm a b))) ⟩ + (b *A a ∷ []) + a · (0# ∷ q) + p * (0# ∷ b ∷ q) + ≈⟨ +-congʳ step1 ⟩ + (b *A a ∷ []) + (a · (0# ∷ q)) + ((b · (0# ∷ p)) + (0# ∷ 0# ∷ p * q)) + ≈⟨ step2 ⟩ + ((b *A a ∷ []) + b · (0# ∷ p)) + (a · (0# ∷ q) + (0# ∷ 0# ∷ p * q)) + ≈⟨ step3 ⟩ + (b · (a ∷ p)) + (a · (0# ∷ q) + (0# ∷ 0# ∷ (p * q))) + ≈⟨ +-congʳ step4 ⟨ + (b · (a ∷ p) + q * (0# ∷ a ∷ p)) + ≈⟨ cast-p≈p (cast-lem (suc m) n) ⟨ + (b ∷ q) * (a ∷ p) + ∎ + where + *-comm-lem : ∀ {m} → {p : Poly m} → (a b : A) → + a ∷ (b · p) ≈ (a ∷ []) + (b · (0# ∷ p)) + *-comm-lem {p = []} a b + = consˡ (CR.sym (CR.trans (CR.+-congˡ (CR.zeroʳ b)) (CR.+-identityʳ a))) + *-comm-lem {p = a ∷ p} b c + = consˡ (CR.sym (CR.trans (CR.+-congˡ (CR.zeroʳ c)) (CR.+-identityʳ b))) + + step1 = begin + p * (0# ∷ b ∷ q) + ≈⟨ *-distrib-shift p (b ∷ q) ⟩ + 0# ∷ (p * (b ∷ q)) + ≈⟨ consʳ (*-comm p (b ∷ q)) ⟩ + 0# ∷ ((b ∷ q) * p) + ≈⟨ consʳ (cast-p≈p (cast-lem m n)) ⟩ + 0# ∷ (b · p + q * (0# ∷ p)) + ≈⟨ consˡ (CR.sym (CR.+-identityʳ 0#)) ⟩ + (0# ∷ (b · p)) + (0# ∷ (q * (0# ∷ p))) + ≈⟨ +-congˡ {r = (0# ∷ (q * (0# ∷ p)))} (·-distrib-shift b p) ⟨ + (b · (0# ∷ p)) + (0# ∷ (q * (0# ∷ p))) + ≈⟨ +-congʳ {p = b · (0# ∷ p)} (consʳ (*-distrib-shift q p)) ⟩ + b · (0# ∷ p) + (0# ∷ 0# ∷ (q * p)) + ≈⟨ +-congʳ {p = b · (0# ∷ p)} (consʳ (consʳ (*-comm q p))) ⟩ + b · (0# ∷ p) + (0# ∷ 0# ∷ (p * q)) + ∎ + + step2 + = middleFour (b *A a ∷ []) (a · (0# ∷ q)) + (b · (0# ∷ p)) (0# ∷ 0# ∷ (p * q)) + + step3 + = +-congˡ {r = a · (0# ∷ q) + (0# ∷ 0# ∷ (p * q))} + (sym (*-comm-lem {p = p} (b *A a) b)) + + step4 = begin + q * (0# ∷ a ∷ p) + ≈⟨ *-distrib-shift q (a ∷ p) ⟩ + 0# ∷ (q * (a ∷ p)) + ≈⟨ consʳ (*-comm q (a ∷ p)) ⟩ + 0# ∷ ((a ∷ p) * q) + ≈⟨ consʳ (cast-p≈p (cast-lem n m)) ⟩ + 0# ∷ (a · q + p * (0# ∷ q)) + ≈⟨ consˡ (CR.sym (CR.+-identityʳ 0#)) ⟩ + (0# ∷ (a · q)) + (0# ∷ (p * (0# ∷ q))) + ≈⟨ +-congˡ {r = (0# ∷ (p * (0# ∷ q)))} (·-distrib-shift a q) ⟨ + a · (0# ∷ q) + (0# ∷ (p * (0# ∷ q))) + ≈⟨ +-congʳ {p = a · (0# ∷ q)} (consʳ (*-distrib-shift p q))⟩ + a · (0# ∷ q) + (0# ∷ 0# ∷ (p * q)) + ∎ + +shift-distrib-+ : (p : Poly m) → (q : Poly n) → + shift (p + q) ≈ (shift p) + (shift q) +shift-distrib-+ p q = cons (CR.sym (CR.+-identityʳ 0#)) refl + +0∷[p*q]≈[0∷p]*q : (p : Poly m) → (q : Poly n) → shift (p * q) ≈ (shift p) * q +0∷[p*q]≈[0∷p]*q p q = begin + 0# ∷ (p * q) ≈⟨ consʳ (*-comm p q) ⟩ + 0# ∷ (q * p) ≈⟨ *-distrib-shift q p ⟨ + q * (0# ∷ p) ≈⟨ *-comm q (0# ∷ p) ⟩ + (0# ∷ p) * q ∎ + +0∷[p*q]≈q*[0∷p] : (p : Poly m) → (q : Poly n) → shift (p * q) ≈ q * (shift p) +0∷[p*q]≈q*[0∷p] p q = begin + 0# ∷ (p * q) ≈⟨ 0∷[p*q]≈[0∷p]*q p q ⟩ + (0# ∷ p) * q ≈⟨ *-comm (0# ∷ p) q ⟩ + q * (0# ∷ p) ∎ + +*-distribʳ-+ : (p : Poly m) → (q : Poly n) → (r : Poly k) → + (q + r) * p ≈ (q * p) + (r * p) +*-distribʳ-+ {_} {_} {_} [] q r = begin + (q + r) * [] + ≈⟨ q≈[]→p*q≈[] (q + r) refl ⟩ + [] + [] + ≈⟨ +-cong (zeroʳ q) (zeroʳ r)⟨ + (q * []) + (r * []) + ∎ +*-distribʳ-+ {suc m} {n} {k} (a ∷ p) q r = begin + ((q + r) * (a ∷ p)) + ≈⟨ *-comm (q + r) (a ∷ p) ⟩ + ((a ∷ p) * (q + r)) + ≈⟨ cast-p≈p (cast-lem (n ⊔ k) m) ⟩ + (a · (q + r)) + (p * (0# ∷ (q + r))) + ≈⟨ +-cong ·-dist (*-distrib-shift p (q + r)) ⟩ + (a · q + a · r) + (0# ∷ (p * (q + r))) + ≈⟨ +-congʳ step5 ⟩ + (a · q + a · r) + ((0# ∷ (q * p)) + (0# ∷ (r * p))) + ≈⟨ middleFour (a · q) (a · r) (0# ∷ (q * p)) (0# ∷ (r * p)) ⟩ + (a · q + (0# ∷ (q * p))) + (a · r + (0# ∷ (r * p))) + ≈⟨ +-congˡ step6 ⟩ + q * (a ∷ p) + (a · r + (0# ∷ r * p)) + ≈⟨ +-congʳ step7 ⟩ + (q * (a ∷ p) + r * (a ∷ p)) + ∎ + where + step5 = begin + 0# ∷ p * (q + r) + ≈⟨ consʳ (*-comm p (q + r)) ⟩ + 0# ∷ ((q + r) * p) + ≈⟨ consʳ (*-distribʳ-+ p q r) ⟩ + 0# ∷ q * p + r * p + ≈⟨ shift-distrib-+ (q * p) (r * p) ⟩ + (0# ∷ q * p) + (0# ∷ r * p) ∎ + + step6 = begin + a · q + (0# ∷ q * p) + ≈⟨ +-congʳ (0∷[p*q]≈q*[0∷p] q p) ⟩ + a · q + p * (0# ∷ q) + ≈⟨ cast-p≈p (cast-lem n m) ⟨ + (a ∷ p) * q + ≈⟨ *-comm (a ∷ p) q ⟩ + q * (a ∷ p) ∎ + + step7 = begin + a · r + (0# ∷ r * p) + ≈⟨ +-congʳ (0∷[p*q]≈q*[0∷p] r p) ⟩ + a · r + p * (0# ∷ r) + ≈⟨ cast-p≈p (cast-lem k m) ⟨ + (a ∷ p) * r + ≈⟨ *-comm (a ∷ p) r ⟩ + r * (a ∷ p) ∎ + +·-distrib-* : (p : Poly m) → (q : Poly n) → (a : A) → + a · (p * q) ≈ (a · p) * q +·-distrib-* {_} {n} [] q a = begin + a · ([] * q) ≈⟨ ·-congʳ zerosm≈zerosn ⟩ + a · [] ≈⟨ zerosm≈zerosn ⟨ + (a · []) * q ∎ +·-distrib-* {suc m} {_} (b ∷ p) [] a = begin + a · ((b ∷ p) * []) + ≈⟨ a·-cong (cast-p≈p (cong pred n+1≡sucn+0)) ⟩ + a · ((b · []) + (p * (0# ∷ []))) + ≈⟨ a·-cong (+-identityˡ (p * (0# ∷ []))) ⟩ + a · (p * (0# ∷ [])) + ≈⟨ a·-cong (q≈[]→p*q≈[] p zerosm≈zerosn) ⟩ + [] + ≈⟨ q≈[]→p*q≈[] ((a · p)) zerosm≈zerosn ⟨ + (a · p) * (0# ∷ []) + ≈⟨ +-identityˡ ((a · p) * (0# ∷ [])) ⟨ + ((a *A b) · []) + ((a · p) * (0# ∷ [])) + ≈⟨ cast-p≈p (cong pred n+1≡sucn+0) ⟨ + (a · (b ∷ p)) * [] + ∎ +·-distrib-* {suc m} {suc n} (b ∷ p) (c ∷ q) a = begin + a · ((b ∷ p) * (c ∷ q)) + ≈⟨ a·-cong (cast-p≈p (cast-lem (suc n) m)) ⟩ + a · ((b · (c ∷ q)) + (p * (0# ∷ c ∷ q))) + ≈⟨ ·-dist ⟩ + a · (b *A c ∷ (b · q)) + a · (p * (0# ∷ c ∷ q)) + ≈⟨ +-congˡ (cons (CR.sym (CR.*-assoc a b c)) ·-assoc) ⟩ + (a *A b *A c ∷ ((a *A b) · q)) + a · (p * (0# ∷ c ∷ q)) + ≈⟨ +-congʳ (·-distrib-* p (0# ∷ c ∷ q) a) ⟩ + (a *A b) · (c ∷ q) + (a · p) * (0# ∷ c ∷ q) + ≈⟨ cast-p≈p (cast-lem (suc n) m) ⟨ + (a · (b ∷ p)) * (c ∷ q) + ∎ + +*-assoc : (p : Poly m) → (q : Poly n) → (r : Poly k) → + (p * q) * r ≈ p * (q * r) +*-assoc {_} {n} {k} [] q r = begin + zeros (n ℕ.∸ 1) * r + ≈⟨ p≈[]⇒p*q≈[] r (IsZero⇒≈0 (zerosIsZero (n ℕ.∸ 1))) ⟩ + [] + ≈⟨ zerosm≈zerosn ⟩ + zeros (pred (0 ℕ.+ pred (n ℕ.+ k))) + ∎ +*-assoc {suc m} {n} {k} (a ∷ p) q r = begin + ((a ∷ p) * q) * r + ≈⟨ *-congˡ (cast-p≈p (cast-lem n m)) ⟩ + ((a · q) + (p * (0# ∷ q))) * r + ≈⟨ *-congˡ (+-congʳ {p = a · q} (*-distrib-shift p q)) ⟩ + ((a · q) + (0# ∷ (p * q))) * r + ≈⟨ *-distribʳ-+ r (a · q) (0# ∷ p * q) ⟩ + ((a · q) * r) + ((0# ∷ (p * q)) * r) + ≈⟨ +-congʳ step8 ⟨ + ((a · q) * r) + (0# ∷ (p * (q * r))) + ≈⟨ +-congˡ (·-distrib-* q r a) ⟨ + (a · (q * r)) + (0# ∷ (p * (q * r))) + ≈⟨ +-congʳ (*-distrib-shift p (q * r)) ⟨ + (a · (q * r)) + (p * (0# ∷ (q * r))) + ≈⟨ cast-p≈p (cast-lem (pred (n ℕ.+ k)) m) ⟨ + (a ∷ p) * (q * r) + ∎ + where + step8 = begin + 0# ∷ (p * (q * r)) + ≈⟨ consʳ (*-assoc p q r) ⟨ + 0# ∷ ((p * q) * r) + ≈⟨ 0∷[p*q]≈[0∷p]*q (p * q) r ⟩ + (0# ∷ (p * q)) * r + ≈⟨ cast-p≈p (cast-lem k (m ℕ.+ n ℕ.∸ 1)) ⟩ + (0# · r) + ((p * q) * (0# ∷ r)) + ≈⟨ +-congˡ (IsZero⇒≈0 (a≈0⇒a·pIsZero 0# r CR.refl) ) ⟩ + zeros k + ((p * q) * (0# ∷ r)) + ≈⟨ +-congʳ (*-distrib-shift (p * q) r) ⟩ + zeros k + (0# ∷ ((p * q) * r)) + ≈⟨ +-congʳ (0∷[p*q]≈[0∷p]*q (p * q) r) ⟩ + zeros k + ((0# ∷ (p * q)) * r) + ≈⟨ +-identityˡ ((0# ∷ (p * q)) * r) ⟩ + (0# ∷ (p * q)) * r + ∎ + +--------------------------------------------------------------------- +-- Multiplicative identity + +*-identityʳ : (p : Poly n) → p * (1# ∷ []) ≈ p +*-identityʳ {0} [] = zerosm≈zerosn +*-identityʳ {suc n} (a ∷ p) = begin + (a ∷ p) * (1# ∷ []) + ≈⟨ cast-p≈p (cast-lem 1 n) ⟩ + (a *A 1# ∷ []) + (p * (0# ∷ 1# ∷ [])) + ≈⟨ +-congˡ (consˡ (CR.*-identityʳ a)) ⟩ + (a ∷ []) + (p * (0# ∷ 1# ∷ [])) + ≈⟨ +-congʳ (*-distrib-shift p (1# ∷ [])) ⟩ + (a ∷ []) + (0# ∷ (p * (1# ∷ []))) + ≈⟨ cons (CR.+-identityʳ a) (+-identityˡ (p * (1# ∷ []))) ⟩ + a ∷ (p * (1# ∷ [])) + ≈⟨ consʳ (*-identityʳ p) ⟩ + a ∷ p ∎ diff --git a/src/Algebra/Polynomial/Properties.agda b/src/Algebra/Polynomial/Properties.agda new file mode 100644 index 0000000000..3b84fe5220 --- /dev/null +++ b/src/Algebra/Polynomial/Properties.agda @@ -0,0 +1,234 @@ +open import Algebra.Bundles using (Magma; Semiring) + +module Algebra.Polynomial.Properties + {ℓ₁ ℓ₂} + (SR : Semiring ℓ₁ ℓ₂) + where + +open import Algebra.Bundles.Raw +import Algebra.Definitions as Def +import Algebra.Polynomial.Poly.Properties SR as Poly +open import Algebra.Polynomial.Base SR + using ( Polynomial; _,_; _≈_; shift; _+_; _*_; _·_ + ; zero; one; refl; sym; trans) +open import Algebra.Structures + using ( IsMagma; IsSemigroup; IsCommutativeSemigroup; IsMonoid + ; IsSemiring; IsCommutativeMonoid + ) +open import Data.Nat.Base as ℕ using (ℕ; _⊔_; suc; pred) +open import Data.Product.Base using (_,_) +open import Data.Vec.Base as Vec using ([]; _∷_) +open import Relation.Binary using (IsEquivalence) + +open Polynomial + +open Semiring SR + using (0#; 1#) + renaming (Carrier to A) + +open Def _≈_ + +private + variable + P Q R : Polynomial + +-------------------------------------------------------------- +-- Algebraic properties of addition + ++-identityˡ : LeftIdentity zero _+_ ++-identityˡ P = Poly.+-identityˡ (polynomial P) + ++-identityʳ : RightIdentity zero _+_ ++-identityʳ P = Poly.+-identityʳ (polynomial P) + ++-identity : Identity zero _+_ ++-identity = +-identityˡ , +-identityʳ + ++-comm : Commutative _+_ ++-comm P Q = Poly.+-comm (polynomial P) (polynomial Q) + ++-assoc : Associative _+_ ++-assoc P Q R + = Poly.+-assoc (polynomial P) (polynomial Q) (polynomial R) + +--------------------------------------------------------------- +-- Additive structures + +isEquivalence : IsEquivalence _≈_ +isEquivalence = record + { refl = refl + ; sym = sym + ; trans = trans + } + ++-isMagma : IsMagma _≈_ _+_ ++-isMagma = record + { isEquivalence = isEquivalence + ; ∙-cong = Poly.+-cong + } + ++-isSemigroup : IsSemigroup _≈_ _+_ ++-isSemigroup = record + { isMagma = +-isMagma + ; assoc = +-assoc + } + ++-isCommutativeSemigroup : IsCommutativeSemigroup _≈_ _+_ ++-isCommutativeSemigroup = record + { isSemigroup = +-isSemigroup + ; comm = +-comm + } + ++-isMonoid : IsMonoid _≈_ _+_ zero ++-isMonoid = record + { isSemigroup = +-isSemigroup + ; identity = +-identity + } + ++-isCommutativeMonoid : IsCommutativeMonoid _≈_ _+_ zero ++-isCommutativeMonoid = record + { isMonoid = +-isMonoid + ; comm = +-comm + } + +--------------------------------------------------------------- +-- Additive raw bundles ++-rawMagma : Algebra.Bundles.Raw.RawMagma _ _ ++-rawMagma = record + { Carrier = Polynomial + ; _≈_ = _≈_ + ; _∙_ = _+_ + } + ++-rawSemiring : Algebra.Bundles.Raw.RawSemiring _ _ ++-rawSemiring = record + { Carrier = Polynomial + ; _≈_ = _≈_ + ; _+_ = _+_ + ; _*_ = _*_ + ; 0# = zero + ; 1# = one + } + + +-- Additive bundles + ++-magma : Algebra.Bundles.Magma _ _ ++-magma = record + { isMagma = +-isMagma + } + ++-semigroup : Algebra.Bundles.Semigroup _ _ ++-semigroup = record + { isSemigroup = +-isSemigroup + } + ++-commutativeSemigroup : Algebra.Bundles.CommutativeSemigroup _ _ ++-commutativeSemigroup = record + { isCommutativeSemigroup = +-isCommutativeSemigroup + } + ++-monoid : Algebra.Bundles.Monoid _ _ ++-monoid = record + { isMonoid = +-isMonoid + } + ++-commutativeMonoid : Algebra.Bundles.CommutativeMonoid _ _ ++-commutativeMonoid = record + { isCommutativeMonoid = +-isCommutativeMonoid + } + +----------------------------------------------------------------- +-- Algebraic properties of multiplication + +a·p≈a∷[]*p : (a : A) → (P : Polynomial) → a · P ≈ (1 , (a ∷ [])) * P +a·p≈a∷[]*p a P = Poly.a·p≈a∷[]*p a (polynomial P) + +*-identityʳ : RightIdentity one _*_ +*-identityʳ P = Poly.*-identityʳ (polynomial P) + +*-identityˡ : LeftIdentity one _*_ +*-identityˡ P = Poly.*-identityˡ (polynomial P) + +*-identity : Identity one _*_ +*-identity = *-identityˡ , *-identityʳ + +*-zeroˡ : LeftZero zero _*_ +*-zeroˡ P = Poly.zeroˡ (polynomial P) + +*-zeroʳ : RightZero zero _*_ +*-zeroʳ P = Poly.zeroʳ (polynomial P) + +*-zero : Zero zero _*_ +*-zero = *-zeroˡ , *-zeroʳ + +*-assoc : Associative _*_ +*-assoc P Q R + = Poly.*-assoc (polynomial P) (polynomial Q) (polynomial R) + +*-distribʳ-+ : _*_ DistributesOverʳ _+_ +*-distribʳ-+ P Q R + = Poly.*-distribʳ-+ (polynomial P) (polynomial Q) (polynomial R) + +*-distribˡ-+ : _*_ DistributesOverˡ _+_ +*-distribˡ-+ P Q R + = Poly.*-distribˡ-+ (polynomial P) (polynomial Q) (polynomial R) + +*-distrib-+ : _*_ DistributesOver _+_ +*-distrib-+ = *-distribˡ-+ , *-distribʳ-+ + +------------------------------------------------------------------ +-- Multiplicative structure + +*-isMagma : IsMagma _≈_ _*_ +*-isMagma = record + { isEquivalence = isEquivalence + ; ∙-cong = Poly.*-cong + } + +*-isSemigroup : IsSemigroup _≈_ _*_ +*-isSemigroup = record + { isMagma = *-isMagma + ; assoc = *-assoc + } + +*-isMonoid : IsMonoid _≈_ _*_ one +*-isMonoid = record + { isSemigroup = *-isSemigroup + ; identity = *-identity + } + ++-*-isSemiring : IsSemiring _≈_ _+_ _*_ zero one ++-*-isSemiring = record + { isSemiringWithoutAnnihilatingZero = record + { +-isCommutativeMonoid = +-isCommutativeMonoid + ; *-cong = Poly.*-cong + ; *-assoc = *-assoc + ; *-identity = *-identity + ; distrib = *-distrib-+ + } + ; zero = *-zero + } + +--------------------------------------------------------------- +-- Multiplicative bundles + +*-magma : Algebra.Bundles.Magma _ _ +*-magma = record + { isMagma = *-isMagma + } + +*-semigroup : Algebra.Bundles.Semigroup _ _ +*-semigroup = record + { isSemigroup = *-isSemigroup + } + +*-monoid : Algebra.Bundles.Monoid _ _ +*-monoid = record + { isMonoid = *-isMonoid + } + ++-*-semiring : Semiring _ _ ++-*-semiring = record + { isSemiring = +-*-isSemiring + } diff --git a/src/Algebra/Polynomial/Properties1.agda b/src/Algebra/Polynomial/Properties1.agda new file mode 100644 index 0000000000..c0d139b15d --- /dev/null +++ b/src/Algebra/Polynomial/Properties1.agda @@ -0,0 +1,292 @@ +open import Algebra.Bundles using (Magma; Ring) + +module Algebra.Polynomial.Properties1 + {ℓ₁ ℓ₂} + (R : Ring ℓ₁ ℓ₂) + where + +open import Algebra.Bundles.Raw +import Algebra.Definitions as Def +import Algebra.Polynomial.Poly.Properties1 R as Poly +open import Algebra.Polynomial.Base1 R + using ( Polynomial; _,_; _≈_; shift; _+_; _*_; _·_ + ; zero; one; -_; refl; sym; trans) +open import Algebra.Properties.AbelianGroup +open import Algebra.Properties.Ring +open import Algebra.Structures + using ( IsMagma; IsSemigroup; IsCommutativeSemigroup; IsMonoid + ; IsGroup; IsAbelianGroup; IsSemiring; IsCommutativeMonoid + ; IsRing) +open import Data.Nat.Base as ℕ using (ℕ; _⊔_; suc; pred) +open import Data.Product.Base using (_,_) +open import Data.Vec.Base as Vec using ([]; _∷_) +open import Relation.Binary using (IsEquivalence) + +open Polynomial + +open Ring R + using (0#; 1#) + renaming (Carrier to A) + +open Def _≈_ + +private + variable + P Q W : Polynomial + +-------------------------------------------------------------- +-- Algebraic properties of addition + ++-identityˡ : LeftIdentity zero _+_ ++-identityˡ P = Poly.+-identityˡ (polynomial P) + ++-identityʳ : RightIdentity zero _+_ ++-identityʳ P = Poly.+-identityʳ (polynomial P) + ++-identity : Identity zero _+_ ++-identity = +-identityˡ , +-identityʳ + ++-comm : Commutative _+_ ++-comm P Q = Poly.+-comm (polynomial P) (polynomial Q) + ++-assoc : Associative _+_ ++-assoc P Q W + = Poly.+-assoc (polynomial P) (polynomial Q) (polynomial W) + ++-inverseˡ : LeftInverse zero -_ _+_ ++-inverseˡ P = Poly.+-inverseˡ (polynomial P) + ++-inverseʳ : RightInverse zero -_ _+_ ++-inverseʳ P = Poly.+-inverseʳ (polynomial P) + ++-inverse : Inverse zero -_ _+_ ++-inverse = +-inverseˡ , +-inverseʳ + +-‿cong : P ≈ Q → - P ≈ - Q +-‿cong = Poly.-‿cong + +--------------------------------------------------------------- +-- Additive structures + +isEquivalence : IsEquivalence _≈_ +isEquivalence = record + { refl = refl + ; sym = sym + ; trans = trans + } + ++-isMagma : IsMagma _≈_ _+_ ++-isMagma = record + { isEquivalence = isEquivalence + ; ∙-cong = Poly.+-cong + } + ++-isSemigroup : IsSemigroup _≈_ _+_ ++-isSemigroup = record + { isMagma = +-isMagma + ; assoc = +-assoc + } + ++-isCommutativeSemigroup : IsCommutativeSemigroup _≈_ _+_ ++-isCommutativeSemigroup = record + { isSemigroup = +-isSemigroup + ; comm = +-comm + } + ++-isMonoid : IsMonoid _≈_ _+_ zero ++-isMonoid = record + { isSemigroup = +-isSemigroup + ; identity = +-identity + } + ++-isGroup : IsGroup _≈_ _+_ zero -_ ++-isGroup = record + { isMonoid = +-isMonoid + ; inverse = +-inverse + ; ⁻¹-cong = -‿cong + } + ++-isCommutativeMonoid : IsCommutativeMonoid _≈_ _+_ zero ++-isCommutativeMonoid = record + { isMonoid = +-isMonoid + ; comm = +-comm + } + ++-isAbelianGroup : IsAbelianGroup _≈_ _+_ zero -_ ++-isAbelianGroup = record + { isGroup = +-isGroup + ; comm = +-comm + } + +--------------------------------------------------------------- +-- Additive bundles + ++-rawMagma : Algebra.Bundles.Raw.RawMagma _ _ ++-rawMagma = record + { Carrier = Polynomial + ; _≈_ = _≈_ + ; _∙_ = _+_ + } + +*-rawMagma : Algebra.Bundles.Raw.RawMagma _ _ +*-rawMagma = record + { Carrier = Polynomial + ; _≈_ = _≈_ + ; _∙_ = _*_ + } + +rawSemiring : Algebra.Bundles.Raw.RawSemiring _ _ +rawSemiring = record + { Carrier = Polynomial + ; _≈_ = _≈_ + ; _+_ = _+_ + ; _*_ = _*_ + ; 0# = zero + ; 1# = one + } + +rawRing : Algebra.Bundles.Raw.RawRing _ _ +rawRing = record + { Carrier = Polynomial + ; _≈_ = _≈_ + ; _+_ = _+_ + ; _*_ = _*_ + ; -_ = -_ + ; 0# = zero + ; 1# = one + } + ++-magma : Algebra.Bundles.Magma _ _ ++-magma = record + { isMagma = +-isMagma + } + ++-semigroup : Algebra.Bundles.Semigroup _ _ ++-semigroup = record + { isSemigroup = +-isSemigroup + } + ++-commutativeSemigroup : Algebra.Bundles.CommutativeSemigroup _ _ ++-commutativeSemigroup = record + { isCommutativeSemigroup = +-isCommutativeSemigroup + } + ++-monoid : Algebra.Bundles.Monoid _ _ ++-monoid = record + { isMonoid = +-isMonoid + } + ++-commutativeMonoid : Algebra.Bundles.CommutativeMonoid _ _ ++-commutativeMonoid = record + { isCommutativeMonoid = +-isCommutativeMonoid + } + ++-abelianGroup : Algebra.Bundles.AbelianGroup _ _ ++-abelianGroup = record + { isAbelianGroup = +-isAbelianGroup + } + +----------------------------------------------------------------- +-- Algebraic properties of multiplication + +a·p≈a∷[]*p : (a : A) → (P : Polynomial) → a · P ≈ (1 , (a ∷ [])) * P +a·p≈a∷[]*p a P = Poly.a·p≈a∷[]*p a (polynomial P) + +*-identityʳ : RightIdentity one _*_ +*-identityʳ P = Poly.*-identityʳ (polynomial P) + +*-identityˡ : LeftIdentity one _*_ +*-identityˡ P = Poly.*-identityˡ (polynomial P) + +*-identity : Identity one _*_ +*-identity = *-identityˡ , *-identityʳ + +*-zeroˡ : LeftZero zero _*_ +*-zeroˡ P = Poly.zeroˡ (polynomial P) + +*-zeroʳ : RightZero zero _*_ +*-zeroʳ P = Poly.zeroʳ (polynomial P) + +*-zero : Zero zero _*_ +*-zero = *-zeroˡ , *-zeroʳ + +*-assoc : Associative _*_ +*-assoc P Q R + = Poly.*-assoc (polynomial P) (polynomial Q) (polynomial R) + +*-distribʳ-+ : _*_ DistributesOverʳ _+_ +*-distribʳ-+ P Q R + = Poly.*-distribʳ-+ (polynomial P) (polynomial Q) (polynomial R) + +*-distribˡ-+ : _*_ DistributesOverˡ _+_ +*-distribˡ-+ P Q W + = Poly.*-distribˡ-+ (polynomial P) (polynomial Q) (polynomial W) + +*-distrib-+ : _*_ DistributesOver _+_ +*-distrib-+ = *-distribˡ-+ , *-distribʳ-+ + +------------------------------------------------------------------ +-- Multiplicative structure + +*-isMagma : IsMagma _≈_ _*_ +*-isMagma = record + { isEquivalence = isEquivalence + ; ∙-cong = Poly.*-cong + } + +*-isSemigroup : IsSemigroup _≈_ _*_ +*-isSemigroup = record + { isMagma = *-isMagma + ; assoc = *-assoc + } + +*-isMonoid : IsMonoid _≈_ _*_ one +*-isMonoid = record + { isSemigroup = *-isSemigroup + ; identity = *-identity + } + ++-*-isSemiring : IsSemiring _≈_ _+_ _*_ zero one ++-*-isSemiring = record + { isSemiringWithoutAnnihilatingZero = record + { +-isCommutativeMonoid = +-isCommutativeMonoid + ; *-cong = Poly.*-cong + ; *-assoc = *-assoc + ; *-identity = *-identity + ; distrib = *-distrib-+ + } + ; zero = *-zero + } + ++-*-isRing : IsRing _≈_ _+_ _*_ -_ zero one ++-*-isRing = record + { +-isAbelianGroup = +-isAbelianGroup + ; *-cong = Poly.*-cong + ; *-assoc = *-assoc + ; *-identity = *-identity + ; distrib = *-distrib-+ + } + +--------------------------------------------------------------- +-- Multiplicative bundles + +*-magma : Algebra.Bundles.Magma _ _ +*-magma = record + { isMagma = *-isMagma + } + +*-semigroup : Algebra.Bundles.Semigroup _ _ +*-semigroup = record + { isSemigroup = *-isSemigroup + } + +*-monoid : Algebra.Bundles.Monoid _ _ +*-monoid = record + { isMonoid = *-isMonoid + } + ++-*-ring : Algebra.Bundles.Ring _ _ ++-*-ring = record + { isRing = +-*-isRing + } + diff --git a/src/Algebra/Polynomial/Properties2.agda b/src/Algebra/Polynomial/Properties2.agda new file mode 100644 index 0000000000..c239ab54d4 --- /dev/null +++ b/src/Algebra/Polynomial/Properties2.agda @@ -0,0 +1,352 @@ +open import Algebra.Bundles using (Magma; CommutativeRing) +open import Algebra.Bundles.Raw + +module Algebra.Polynomial.Properties2 + {ℓ₁ ℓ₂} + (CR : CommutativeRing ℓ₁ ℓ₂) + where + +import Algebra.Consequences.Setoid as C + using (comm∧distrʳ⇒distrˡ ; comm∧idʳ⇒idˡ) +import Algebra.Definitions as Def +import Algebra.Polynomial.Poly.Properties2 CR as Poly +open import Algebra.Polynomial.Base2 CR + using ( Polynomial; _,_; _≈_; shift; _+_; _*_; _·_ + ; zero; one; -_; refl; sym; trans) +open import Algebra.Properties.AbelianGroup +open import Algebra.Properties.Ring +open import Algebra.Structures + using ( IsMagma; IsSemigroup; IsCommutativeSemigroup; IsMonoid + ; IsGroup; IsAbelianGroup; IsCommutativeMonoid; IsSemiring + ; IsRing; IsCommutativeSemiring; IsCommutativeRing ) +open import Data.Nat.Base as ℕ using (ℕ; _⊔_; suc; pred) +open import Data.Product.Base using (_,_) +open import Data.Vec.Base as Vec using ([]; _∷_) +open import Relation.Binary using (IsEquivalence) + +open Polynomial + +open CommutativeRing CR + using (0#; 1#) + renaming (Carrier to A) + +open Def _≈_ + +private + variable + P Q R : Polynomial + +-------------------------------------------------------------- +-- Algebraic properties of addition + ++-identityˡ : LeftIdentity zero _+_ ++-identityˡ P = Poly.+-identityˡ (polynomial P) + ++-identityʳ : RightIdentity zero _+_ ++-identityʳ P = Poly.+-identityʳ (polynomial P) + ++-identity : Identity zero _+_ ++-identity = +-identityˡ , +-identityʳ + ++-comm : Commutative _+_ ++-comm P Q = Poly.+-comm (polynomial P) (polynomial Q) + ++-assoc : Associative _+_ ++-assoc P Q R + = Poly.+-assoc (polynomial P) (polynomial Q) (polynomial R) + ++-inverseˡ : LeftInverse zero -_ _+_ ++-inverseˡ P = Poly.+-inverseˡ (polynomial P) + ++-inverseʳ : RightInverse zero -_ _+_ ++-inverseʳ P = Poly.+-inverseʳ (polynomial P) + ++-inverse : Inverse zero -_ _+_ ++-inverse = +-inverseˡ , +-inverseʳ + +-‿cong : P ≈ Q → - P ≈ - Q +-‿cong = Poly.-‿cong + +--------------------------------------------------------------- +-- Additive structures + +isEquivalence : IsEquivalence _≈_ +isEquivalence = record + { refl = refl + ; sym = sym + ; trans = trans + } + ++-isMagma : IsMagma _≈_ _+_ ++-isMagma = record + { isEquivalence = isEquivalence + ; ∙-cong = Poly.+-cong + } + ++-isSemigroup : IsSemigroup _≈_ _+_ ++-isSemigroup = record + { isMagma = +-isMagma + ; assoc = +-assoc + } + ++-isCommutativeSemigroup : IsCommutativeSemigroup _≈_ _+_ ++-isCommutativeSemigroup = record + { isSemigroup = +-isSemigroup + ; comm = +-comm + } + ++-isMonoid : IsMonoid _≈_ _+_ zero ++-isMonoid = record + { isSemigroup = +-isSemigroup + ; identity = +-identity + } + ++-isCommutativeMonoid : IsCommutativeMonoid _≈_ _+_ zero ++-isCommutativeMonoid = record + { isMonoid = +-isMonoid + ; comm = +-comm + } + ++-isGroup : IsGroup _≈_ _+_ zero -_ ++-isGroup = record + { isMonoid = +-isMonoid + ; inverse = +-inverse + ; ⁻¹-cong = -‿cong + } + ++-isAbelianGroup : IsAbelianGroup _≈_ _+_ zero -_ ++-isAbelianGroup = record + { isGroup = +-isGroup + ; comm = +-comm + } + +--------------------------------------------------------------- +-- Additive bundles +-- Additive bundles + ++-rawMagma : Algebra.Bundles.Raw.RawMagma _ _ ++-rawMagma = record + { Carrier = Polynomial + ; _≈_ = _≈_ + ; _∙_ = _+_ + } + +*-rawMagma : Algebra.Bundles.Raw.RawMagma _ _ +*-rawMagma = record + { Carrier = Polynomial + ; _≈_ = _≈_ + ; _∙_ = _*_ + } + +rawNearSemiring : Algebra.Bundles.Raw.RawNearSemiring _ _ +rawNearSemiring = record + { Carrier = Polynomial + ; _≈_ = _≈_ + ; _+_ = _+_ + ; _*_ = _*_ + ; 0# = zero + } + +rawSemiring : Algebra.Bundles.Raw.RawSemiring _ _ +rawSemiring = record + { Carrier = Polynomial + ; _≈_ = _≈_ + ; _+_ = _+_ + ; _*_ = _*_ + ; 0# = zero + ; 1# = one + } + + + +rawRing : Algebra.Bundles.Raw.RawRing _ _ +rawRing = record + { Carrier = Polynomial + ; _≈_ = _≈_ + ; _+_ = _+_ + ; _*_ = _*_ + ; -_ = -_ + ; 0# = zero + ; 1# = one + } + ++-magma : Algebra.Bundles.Magma _ _ ++-magma = record + { isMagma = +-isMagma + } + ++-semigroup : Algebra.Bundles.Semigroup _ _ ++-semigroup = record + { isSemigroup = +-isSemigroup + } + ++-commutativeSemigroup : Algebra.Bundles.CommutativeSemigroup _ _ ++-commutativeSemigroup = record + { isCommutativeSemigroup = +-isCommutativeSemigroup + } + ++-monoid : Algebra.Bundles.Monoid _ _ ++-monoid = record + { isMonoid = +-isMonoid + } + ++-commutativeMonoid : Algebra.Bundles.CommutativeMonoid _ _ ++-commutativeMonoid = record + { isCommutativeMonoid = +-isCommutativeMonoid + } + ++-abelianGroup : Algebra.Bundles.AbelianGroup _ _ ++-abelianGroup = record + { isAbelianGroup = +-isAbelianGroup + } + +----------------------------------------------------------------- +-- Algebraic properties of multiplication + +a·p≈a∷[]*p : (a : A) → (P : Polynomial) → a · P ≈ (1 , (a ∷ [])) * P +a·p≈a∷[]*p a P = Poly.a·p≈a∷[]*p a (polynomial P) + +*-comm : Commutative _*_ +*-comm P Q = Poly.*-comm (polynomial P) (polynomial Q) + +*-identityʳ : RightIdentity one _*_ +*-identityʳ P = Poly.*-identityʳ (polynomial P) + +*-identityˡ : LeftIdentity one _*_ +*-identityˡ = C.comm∧idʳ⇒idˡ (Magma.setoid +-magma) *-comm *-identityʳ + +*-identity : Identity one _*_ +*-identity = *-identityˡ , *-identityʳ + +*-zeroˡ : LeftZero zero _*_ +*-zeroˡ P = Poly.zeroˡ (polynomial P) + +*-zeroʳ : RightZero zero _*_ +*-zeroʳ P = Poly.zeroʳ (polynomial P) + +*-zero : Zero zero _*_ +*-zero = *-zeroˡ , *-zeroʳ + +*-assoc : Associative _*_ +*-assoc P Q R + = Poly.*-assoc (polynomial P) (polynomial Q) (polynomial R) + +*-distribʳ-+ : _*_ DistributesOverʳ _+_ +*-distribʳ-+ P Q R + = Poly.*-distribʳ-+ (polynomial P) (polynomial Q) (polynomial R) + +*-distribˡ-+ : _*_ DistributesOverˡ _+_ +*-distribˡ-+ + = C.comm∧distrʳ⇒distrˡ (Magma.setoid +-magma) Poly.+-cong *-comm *-distribʳ-+ + +*-distrib-+ : _*_ DistributesOver _+_ +*-distrib-+ = *-distribˡ-+ , *-distribʳ-+ + +------------------------------------------------------------------ +-- Multiplicative structure + +*-isMagma : IsMagma _≈_ _*_ +*-isMagma = record + { isEquivalence = isEquivalence + ; ∙-cong = Poly.*-cong + } + +*-isSemigroup : IsSemigroup _≈_ _*_ +*-isSemigroup = record + { isMagma = *-isMagma + ; assoc = *-assoc + } + +*-isCommutativeSemigroup : IsCommutativeSemigroup _≈_ _*_ +*-isCommutativeSemigroup = record + { isSemigroup = *-isSemigroup + ; comm = *-comm + } + +*-isMonoid : IsMonoid _≈_ _*_ one +*-isMonoid = record + { isSemigroup = *-isSemigroup + ; identity = *-identity + } + +*-isCommutativeMonoid : IsCommutativeMonoid _≈_ _*_ one +*-isCommutativeMonoid = record + { isMonoid = *-isMonoid + ; comm = *-comm + } + ++-*-isSemiring : IsSemiring _≈_ _+_ _*_ zero one ++-*-isSemiring = record + { isSemiringWithoutAnnihilatingZero = record + { +-isCommutativeMonoid = +-isCommutativeMonoid + ; *-cong = Poly.*-cong + ; *-assoc = *-assoc + ; *-identity = *-identity + ; distrib = *-distrib-+ + } + ; zero = *-zero + } + ++-*-isCommutativeSemiring : IsCommutativeSemiring _≈_ _+_ _*_ zero one ++-*-isCommutativeSemiring = record + { isSemiring = +-*-isSemiring + ; *-comm = *-comm + } + ++-*-isRing : IsRing _≈_ _+_ _*_ -_ zero one ++-*-isRing = record + { +-isAbelianGroup = +-isAbelianGroup + ; *-cong = Poly.*-cong + ; *-assoc = *-assoc + ; *-identity = *-identity + ; distrib = *-distrib-+ + } + ++-*-isCommutativeRing : IsCommutativeRing _≈_ _+_ _*_ -_ zero one ++-*-isCommutativeRing = record + { isRing = +-*-isRing + ; *-comm = *-comm + } + +--------------------------------------------------------------- +-- Multiplicative bundles + +*-magma : Algebra.Bundles.Magma _ _ +*-magma = record + { isMagma = *-isMagma + } + +*-semigroup : Algebra.Bundles.Semigroup _ _ +*-semigroup = record + { isSemigroup = *-isSemigroup + } + +*-commutativeSemigroup : Algebra.Bundles.CommutativeSemigroup _ _ +*-commutativeSemigroup = record + { isCommutativeSemigroup = *-isCommutativeSemigroup + } + +*-monoid : Algebra.Bundles.Monoid _ _ +*-monoid = record + { isMonoid = *-isMonoid + } + +*-commutativeMonoid : Algebra.Bundles.CommutativeMonoid _ _ +*-commutativeMonoid = record + { isCommutativeMonoid = *-isCommutativeMonoid + } + ++-*-commutativeSemiring : Algebra.Bundles.CommutativeSemiring _ _ ++-*-commutativeSemiring = record + { isCommutativeSemiring = +-*-isCommutativeSemiring + } + ++-*-ring : Algebra.Bundles.Ring _ _ ++-*-ring = record + { isRing = +-*-isRing + } + ++-*-commutativeRing : Algebra.Bundles.CommutativeRing _ _ ++-*-commutativeRing = record + { isCommutativeRing = +-*-isCommutativeRing + } diff --git a/src/Algebra/Properties/Group.agda b/src/Algebra/Properties/Group.agda index 8277f4feb7..54c5d469fe 100644 --- a/src/Algebra/Properties/Group.agda +++ b/src/Algebra/Properties/Group.agda @@ -127,6 +127,19 @@ x≈y⇒x∙y⁻¹≈ε {x} {y} x≈y = begin y ∙ y ⁻¹ ≈⟨ inverseʳ y ⟩ ε ∎ +x≈ε⇒x⁻¹≈ε : ∀ {x} → x ≈ ε → x ⁻¹ ≈ ε +x≈ε⇒x⁻¹≈ε {x} x≈ε = begin + x ⁻¹ ≈⟨ ⁻¹-cong x≈ε ⟩ + ε ⁻¹ ≈⟨ ε⁻¹≈ε ⟩ + ε ∎ + +x⁻¹≈ε⇒x≈ε : ∀ {x} → x ⁻¹ ≈ ε → x ≈ ε +x⁻¹≈ε⇒x≈ε {x} x⁻¹≈ε = begin + x ≈⟨ ⁻¹-involutive x ⟨ + x ⁻¹ ⁻¹ ≈⟨ ⁻¹-cong x⁻¹≈ε ⟩ + ε ⁻¹ ≈⟨ ε⁻¹≈ε ⟩ + ε ∎ + ⁻¹-injective : Injective _≈_ _≈_ _⁻¹ ⁻¹-injective = selfInverse⇒injective ⁻¹-selfInverse