Skip to content

Instantly share code, notes, and snippets.

@mildsunrise
Last active April 13, 2024 20:54
Show Gist options
  • Save mildsunrise/d78f4dd77ca6eed72616c30a307a9d46 to your computer and use it in GitHub Desktop.
Save mildsunrise/d78f4dd77ca6eed72616c30a307a9d46 to your computer and use it in GitHub Desktop.
polynomial algebra over a ring
open import Level using (suc; _⊔_)
open import Function using (id; _∘_)
open import Data.List as List using (
List; []; _∷_; [_]; map; reverse; align; alignWith; foldr; head; last; drop; length
)
import Data.List.Properties as List
import Data.List.Relation.Unary.All as All
import Data.List.Relation.Binary.Pointwise as PW
open import Data.Sum as Sum using (_⊎_; inj₁; inj₂)
open import Data.Product as Product using (_×_; _,_)
open import Data.Maybe as Maybe using (Maybe; fromMaybe)
import Data.Maybe.Relation.Unary.All as Maybe
import Data.These as These
import Data.These.Properties as These
open import Data.Nat as ℕ using (ℕ)
import Data.Nat.Properties as ℕ
open import Algebra.Bundles using (CommutativeRing)
open import Relation.Nullary as Dec using (¬_; Dec)
open import Relation.Binary using (Setoid)
open import Relation.Binary.PropositionalEquality as PropEq using (_≡_) renaming (refl to ≡-refl)
import Relation.Binary.Reasoning.Setoid as Reasoning
-- two crucial choices have to be made regarding definition of polynomials
-- 1. whether to make it normalized or not
-- if normalized:
-- degree is known
-- equality is list equality
-- if not:
-- no need to prove normalization
-- 2. whether to make it LE or BE
-- if LE:
-- basic polynomial operations (_+_, _*_, _∣_, _≈_) are simple
-- if BE:
-- complex operations (degree, division, normalized proofs for product) are simple
--
-- and a third one, which is whether to allow 0-length coefficients or always force non-empty list
module polynomials {c} {ℓ} (ring : CommutativeRing c ℓ) where
private
module R where
open CommutativeRing ring public
open CommutativeRing ring renaming (Carrier to Rₛ) using ()
-- Carrier to R; _≈_ to _≈R_; _+_ to _+R_; _*_ to _*R_; ) using ()
Polynomial = List Rₛ
-- coefficients, with least significant being head
0# : Polynomial
0# = []
-- scalars can be embedded as polynomials
scalar : Rₛ → Polynomial
scalar = [_]
1# : Polynomial
1# = scalar R.1#
-- evaluation, N-th coefficient
private
evalStep = λ x k res → k R.+ x R.* res
_∣_ : Polynomial → Rₛ → Rₛ
P ∣ x = foldr (evalStep x) R.0# P
_⟨_⟩ : List Rₛ → ℕ → Rₛ
[] ⟨ k ⟩ = R.0#
(x ∷ P) ⟨ ℕ.zero ⟩ = x
(x ∷ P) ⟨ ℕ.suc k ⟩ = P ⟨ k ⟩
-- polynomials are an R-module
infix 6 -_
infixl 6 _+_ _-_
infixl 7 _*_ _*S_
_*S_ : Rₛ → Polynomial → Polynomial
k *S P = map (k R.*_) P
-_ : Polynomial → Polynomial
-_ = map (R.-_)
_+_ : Polynomial → Polynomial → Polynomial
_+_ = alignWith (These.fold id id R._+_)
_-_ : Polynomial → Polynomial → Polynomial
P - Q = P + (- Q)
-- polynomials are an R-algebra
private
*-step = λ K res → K ⟨ 0 ⟩ ∷ (drop 1 K + res)
_*_ : Polynomial → Polynomial → Polynomial
P * Q = foldr *-step 0# (map (_*S Q) P)
-- degree predicates
private
pred : ℕ → Maybe ℕ
pred 0 = Maybe.nothing
pred (ℕ.suc n) = Maybe.just n
-- Norm≤ : ℕ → Polynomial → Set ℓ
-- Norm≤ n P = drop n P ≈ 0#
-- Norm≡ : ℕ → Polynomial → Set ℓ
-- Norm≡ n P = IsBelowDegree n P × Maybe.All ((R._≉ R.0#) ∘ P ⟨_⟩) (pred n)
IsBelowDegree : ℕ → Polynomial → Set ℓ
IsBelowDegree n P = ∀ {k} → n ℕ.≤ k → P ⟨ k ⟩ R.≈ R.0#
FitsDegree : ℕ → Polynomial → Set ℓ
FitsDegree = IsBelowDegree ∘ ℕ.suc
IsDegree : ℕ → Polynomial → Set ℓ
-- IsDegree n P = FitsDegree n P × (P ⟨ n ⟩ R.≉ R.0# ⊎ n ≡ 0)
IsDegree 0 P = FitsDegree 0 P
IsDegree n P = FitsDegree n P × P ⟨ n ⟩ R.≉ R.0#
IsDegree⇒FitsDegree : ∀ {n P} → IsDegree n P → FitsDegree n P
IsDegree⇒FitsDegree {0} deg = deg
IsDegree⇒FitsDegree {ℕ.suc n} (deg , _) = deg
FitsDegree∧NonZero⇒IsDegree : ∀ {n P} → FitsDegree n P → P ⟨ n ⟩ R.≉ R.0# → IsDegree n P
FitsDegree∧NonZero⇒IsDegree {0} deg _ = deg
FitsDegree∧NonZero⇒IsDegree {ℕ.suc n} deg nz = deg , nz
-- special polynomials
root : Rₛ → Polynomial
root r = (R.- r) ∷ 1#
identity = root R.0#
-- equality
infix 4 _≈_ _≉_
data _≈_ (P Q : Polynomial) : Set ℓ where
mk≈ : (∀ k → P ⟨ k ⟩ R.≈ Q ⟨ k ⟩) → P ≈ Q
≈⟨⟩ : ∀ {P Q} → P ≈ Q → ∀ k → P ⟨ k ⟩ R.≈ Q ⟨ k ⟩
≈⟨⟩ (mk≈ f) = f
_≉_ : Polynomial → Polynomial → Set ℓ
P ≉ Q = ¬ (P ≈ Q)
-- lower / raise degree
lower : ℕ → Polynomial → Polynomial
lower = drop
raise : ℕ → Polynomial → Polynomial
raise ℕ.zero P = P
raise (ℕ.suc k) P = R.0# ∷ P
-- normalization
IsNormalized : Polynomial → Set (c ⊔ ℓ)
IsNormalized P = Maybe.All (R._≉ R.0#) (last P)
0#normal : IsNormalized 0#
0#normal = Maybe.nothing
-- properties of _≈_
refl : ∀ {P} → P ≈ P
refl = mk≈ λ k → R.refl
sym : ∀ {P Q} → P ≈ Q → Q ≈ P
sym P≈Q = mk≈ λ k → R.sym (≈⟨⟩ P≈Q k)
trans : ∀ {P Q R} → P ≈ Q → Q ≈ R → P ≈ R
trans P≈Q Q≈R = mk≈ λ k → R.trans (≈⟨⟩ P≈Q k) (≈⟨⟩ Q≈R k)
setoid : Setoid c ℓ
setoid = record {
Carrier = Polynomial; _≈_ = _≈_;
isEquivalence = record { refl = refl; sym = sym; trans = trans } }
-- properties of fromList, raise, drop
⟨⟩-lower : ∀ n P k → (lower n P) ⟨ k ⟩ ≡ P ⟨ n ℕ.+ k ⟩
⟨⟩-lower ℕ.zero P k = PropEq.refl
⟨⟩-lower (ℕ.suc n) [] k = PropEq.refl
⟨⟩-lower (ℕ.suc n) (x ∷ P) k = ⟨⟩-lower n P k
lower-≈ : ∀ n {P Q} → P ≈ Q → lower n P ≈ lower n Q
lower-≈ n {P} {Q} P≈Q = mk≈ helper
where
helper : ∀ k → (lower n P) ⟨ k ⟩ R.≈ (lower n Q) ⟨ k ⟩
helper k
rewrite ⟨⟩-lower n P k
rewrite ⟨⟩-lower n Q k
= ≈⟨⟩ P≈Q (n ℕ.+ k)
head-≈ : ∀ {P Q} → P ≈ Q → P ⟨ 0 ⟩ R.≈ Q ⟨ 0 ⟩
head-≈ P = ≈⟨⟩ P 0
tail-≈ = lower-≈ 1
uncons-≈ : ∀ {P Q} → P ≈ Q → (P ⟨ 0 ⟩ R.≈ Q ⟨ 0 ⟩) × (lower 1 P ≈ lower 1 Q)
uncons-≈ P≈Q = head-≈ P≈Q , tail-≈ P≈Q
∷-≈ : ∀ {k l P Q} → k R.≈ l → P ≈ Q → k ∷ P ≈ l ∷ Q
∷-≈ k≈l P≈Q = mk≈ λ where
0 → k≈l
(ℕ.suc k) → ≈⟨⟩ P≈Q k
zero≈0 : scalar R.0# ≈ 0#
zero≈0 = mk≈ λ where
0 → R.refl
(ℕ.suc k) → R.refl
scalar-≈ : ∀ {k l} → k R.≈ l → scalar k ≈ scalar l
scalar-≈ k≈l = mk≈ λ where
0 → k≈l
(ℕ.suc k) → R.refl
-- normalization
-- -- -- module _ (≈?0 : ∀ k → Dec (k R.≈ R.0#)) where
-- -- -- normalized : Polynomial → Polynomial
-- -- -- normalized P = {! !}
-- -- -- normalized-≈ : ∀ P → normalized P ≈ P
-- -- -- normalized-≈ P = {! !}
-- -- -- normalized-idempotent : ∀ P → normalized (normalized P) ≡ normalized P
-- -- -- normalized-idempotent P = ?
-- (stronger) list equality
open import Data.List.Relation.Binary.Equality.Setoid R.setoid
as ListEq using (_≋_)
-- ≋⇒≈ : ∀ {P Q} → P ≋ Q → P ≈ Q
-- ≋⇒≈ P≋Q k = {! !}
-- ≈⇒≋ : ∀ {P Q} → P ≈ Q → length P ≡ length Q → P ≋ Q
-- ≈⇒≋ P≈Q leneq = {! !}
-- properties of _+_
+-⟨⟩ : ∀ P Q k → P ⟨ k ⟩ R.+ Q ⟨ k ⟩ R.≈ (P + Q) ⟨ k ⟩
+-⟨⟩ [] [] 0 = R.+-identityˡ R.0#
+-⟨⟩ [] (x ∷ Q) 0 = R.+-identityˡ x
+-⟨⟩ (x ∷ P) [] 0 = R.+-identityʳ x
+-⟨⟩ (x ∷ P) (y ∷ Q) 0 = R.refl
+-⟨⟩ [] [] (ℕ.suc k) = R.+-identityˡ R.0#
+-⟨⟩ [] (x ∷ Q) (ℕ.suc k) rewrite List.map-id Q = R.+-identityˡ (Q ⟨ k ⟩)
+-⟨⟩ (x ∷ P) [] (ℕ.suc k) rewrite List.map-id P = R.+-identityʳ (P ⟨ k ⟩)
+-⟨⟩ (x ∷ P) (y ∷ Q) (ℕ.suc k) = +-⟨⟩ P Q k
+-comm : ∀ P Q → P + Q ≈ Q + P
+-comm P Q = mk≈ λ k → let _ₖ = _⟨ k ⟩ in begin
(P + Q) ₖ ≈⟨ R.sym (+-⟨⟩ P Q k) ⟩
P ₖ R.+ Q ₖ ≈⟨ R.+-comm (P ₖ) (Q ₖ) ⟩
Q ₖ R.+ P ₖ ≈⟨ +-⟨⟩ Q P k ⟩
(Q + P) ₖ ∎
where open Reasoning R.setoid
+-assoc : ∀ P Q R → (P + Q) + R ≈ P + (Q + R)
+-assoc P Q R = mk≈ λ k → let _ₖ = _⟨ k ⟩ in begin
((P + Q) + R) ₖ ≈⟨ R.sym (+-⟨⟩ (P + Q) R k) ⟩
(P + Q) ₖ R.+ R ₖ ≈⟨ R.sym (R.+-congʳ (+-⟨⟩ P Q k)) ⟩
(P ₖ R.+ Q ₖ) R.+ R ₖ ≈⟨ R.+-assoc (P ₖ) (Q ₖ) (R ₖ) ⟩
P ₖ R.+ (Q ₖ R.+ R ₖ) ≈⟨ R.+-congˡ (+-⟨⟩ Q R k) ⟩
P ₖ R.+ (Q + R) ₖ ≈⟨ +-⟨⟩ P (Q + R) k ⟩
(P + (Q + R)) ₖ ∎
where open Reasoning R.setoid
+-cong : ∀ {P Q R S} → P ≈ Q → R ≈ S → P + R ≈ Q + S
+-cong {P} {Q} {R} {S} P≈Q R≈S = mk≈ λ k → let _ₖ = _⟨ k ⟩ in begin
(P + R) ₖ ≈⟨ R.sym (+-⟨⟩ P R k) ⟩
P ₖ R.+ R ₖ ≈⟨ R.+-cong (≈⟨⟩ P≈Q k) (≈⟨⟩ R≈S k) ⟩
Q ₖ R.+ S ₖ ≈⟨ +-⟨⟩ Q S k ⟩
(Q + S) ₖ ∎
where open Reasoning R.setoid
-- properties of _*S_
*S-⟨⟩ : ∀ l P k → (l *S P) ⟨ k ⟩ R.≈ l R.* P ⟨ k ⟩
*S-⟨⟩ l [] ℕ.zero = R.sym (R.zeroʳ l)
*S-⟨⟩ l [] (ℕ.suc k) = R.sym (R.zeroʳ l)
*S-⟨⟩ l (x ∷ P) ℕ.zero = R.refl
*S-⟨⟩ l (x ∷ P) (ℕ.suc k) = *S-⟨⟩ l P k
*S-idˡ : ∀ P → R.1# *S P ≈ P
*S-idˡ P = mk≈ λ k → let _ₖ = _⟨ k ⟩ in
R.trans (*S-⟨⟩ R.1# P k) (R.*-identityˡ (P ₖ))
*S-zeroˡ : ∀ P → R.0# *S P ≈ 0#
*S-zeroˡ P = mk≈ λ k → let _ₖ = _⟨ k ⟩ in
R.trans (*S-⟨⟩ R.0# P k) (R.zeroˡ (P ₖ))
*S-cong : ∀ {l m P Q} → l R.≈ m → P ≈ Q → l *S P ≈ m *S Q
*S-cong {l} {m} {P} {Q} l≈m P≈Q = mk≈ λ k → let _ₖ = _⟨ k ⟩ in begin
(l *S P) ₖ ≈⟨ *S-⟨⟩ l P k ⟩
l R.* P ₖ ≈⟨ R.*-cong l≈m (≈⟨⟩ P≈Q k) ⟩
m R.* Q ₖ ≈⟨ R.sym (*S-⟨⟩ m Q k) ⟩
(m *S Q) ₖ ∎
where open Reasoning R.setoid
*S-distrˡ : ∀ l P Q → l *S (P + Q) ≈ l *S P + l *S Q
*S-distrˡ l P Q = mk≈ λ k → let _ₖ = _⟨ k ⟩ in begin
(l *S (P + Q)) ₖ ≈⟨ *S-⟨⟩ l (P + Q) k ⟩
l R.* (P + Q) ₖ ≈⟨ R.sym (R.*-congˡ (+-⟨⟩ P Q k)) ⟩
l R.* (P ₖ R.+ Q ₖ) ≈⟨ R.distribˡ l (P ₖ) (Q ₖ) ⟩
l R.* P ₖ R.+ l R.* Q ₖ ≈⟨ R.sym (R.+-cong (*S-⟨⟩ l P k) (*S-⟨⟩ l Q k)) ⟩
(l *S P) ₖ R.+ (l *S Q) ₖ ≈⟨ +-⟨⟩ (l *S P) (l *S Q) k ⟩
(l *S P + l *S Q) ₖ ∎
where open Reasoning R.setoid
*S-distrʳ : ∀ l m P → (l R.+ m) *S P ≈ l *S P + m *S P
*S-distrʳ l m P = mk≈ λ k → let _ₖ = _⟨ k ⟩ in begin
((l R.+ m) *S P) ₖ ≈⟨ *S-⟨⟩ (l R.+ m) P k ⟩
(l R.+ m) R.* P ₖ ≈⟨ R.distribʳ (P ₖ) l m ⟩
l R.* P ₖ R.+ m R.* P ₖ ≈⟨ R.sym (R.+-cong (*S-⟨⟩ l P k) (*S-⟨⟩ m P k)) ⟩
(l *S P) ₖ R.+ (m *S P) ₖ ≈⟨ +-⟨⟩ (l *S P) (m *S P) k ⟩
(l *S P + m *S P) ₖ ∎
where open Reasoning R.setoid
*S-compat : ∀ l m P → (l R.* m) *S P ≈ l *S (m *S P)
*S-compat l m P = mk≈ λ k → let _ₖ = _⟨ k ⟩ in begin
((l R.* m) *S P) ₖ ≈⟨ *S-⟨⟩ (l R.* m) P k ⟩
(l R.* m) R.* P ₖ ≈⟨ R.*-assoc l m (P ₖ) ⟩
l R.* (m R.* P ₖ) ≈⟨ R.sym (R.*-congˡ (*S-⟨⟩ m P k)) ⟩
l R.* (m *S P) ₖ ≈⟨ R.sym (*S-⟨⟩ l (m *S P) k) ⟩
(l *S (m *S P)) ₖ ∎
where open Reasoning R.setoid
-- properties of _*_
private
*-step-cong : ∀ {P Q R S} → P ≈ Q → R ≈ S → *-step P R ≈ *-step Q S
*-step-cong {P} {Q} P≈Q R≈S with p≈q , P≈Q ← uncons-≈ P≈Q =
∷-≈ p≈q (+-cong P≈Q R≈S)
*-step-zero : ∀ {P Q} → P ≈ 0# → Q ≈ 0# → *-step P Q ≈ 0#
*-step-zero P≈0 Q≈0 = trans (*-step-cong P≈0 Q≈0) zero≈0
*-cong : ∀ {P Q R S} → P ≈ Q → R ≈ S → P * R ≈ Q * S
*-cong {[]} {[]} {R} {S} P≈Q R≈S = refl
*-cong {[]} {q ∷ Q} {R} {S} P≈Q R≈S with p≈q , P≈Q ← uncons-≈ P≈Q with ih ← *-cong P≈Q R≈S = sym (*-step-zero (trans (*S-cong (R.sym p≈q) refl) (*S-zeroˡ S)) (sym ih))
*-cong {p ∷ P} {[]} {R} {S} P≈Q R≈S with p≈q , P≈Q ← uncons-≈ P≈Q with ih ← *-cong P≈Q R≈S = *-step-zero (trans (*S-cong p≈q refl) (*S-zeroˡ R)) ih
*-cong {p ∷ P} {q ∷ Q} {R} {S} P≈Q R≈S with p≈q , P≈Q ← uncons-≈ P≈Q with ih ← *-cong P≈Q R≈S = *-step-cong (*S-cong p≈q R≈S) ih
-- properties of _∣_
private
-0≈0 : R.- R.0# R.≈ R.0#
-0≈0 = R.trans (R.sym (R.+-identityˡ _)) (R.-‿inverseʳ R.0#)
x-0≈x : ∀ x → x R.- R.0# R.≈ x
x-0≈x x = R.trans (R.+-congˡ -0≈0) (R.+-identityʳ x)
x+y0≈x : ∀ x y → x R.+ y R.* R.0# R.≈ x
x+y0≈x x y = R.trans (R.+-congˡ (R.zeroʳ y)) (R.+-identityʳ x)
x+0y≈x : ∀ x y → x R.+ R.0# R.* y R.≈ x
x+0y≈x x y = R.trans (R.+-congˡ (R.zeroˡ y)) (R.+-identityʳ x)
scalar-∣ : ∀ x k → (scalar k ∣ x) R.≈ k
scalar-∣ x k = x+y0≈x k x
root-∣ : ∀ r x → (root r ∣ x) R.≈ x R.- r
root-∣ r x = begin
(R.- r) R.+ x R.* (R.1# R.+ x R.* R.0#) ≈⟨ R.+-comm _ _ ⟩
x R.* (R.1# R.+ x R.* R.0#) R.- r ≈⟨ R.+-congʳ (R.*-congˡ (x+y0≈x R.1# x)) ⟩
x R.* R.1# R.- r ≈⟨ R.+-congʳ (R.*-identityʳ x) ⟩
x R.- r ∎
where open Reasoning R.setoid
identity-∣ : ∀ x → (identity ∣ x) R.≈ x
identity-∣ x = R.trans (root-∣ R.0# x) (x-0≈x x)
private
evalStep-cong : ∀ {x y} → x R.≈ y
→ ∀ {k l a b} → k R.≈ l → a R.≈ b
→ evalStep x k a R.≈ evalStep y l b
evalStep-cong x≈y k≈l a≈b = R.+-cong k≈l (R.*-cong x≈y a≈b)
evalStep-zeroʳ : ∀ {x k a} → a R.≈ R.0# → evalStep x k a R.≈ k
evalStep-zeroʳ {x} {k} {a} a≈0 = R.trans (R.+-congˡ lemma) (R.+-identityʳ k)
where
lemma = R.trans (R.*-congˡ a≈0) (R.zeroʳ x)
evalStep-+ : ∀ x pk qk pa qa →
evalStep x (pk R.+ qk) (pa R.+ qa) R.≈
evalStep x pk pa R.+ evalStep x qk qa
evalStep-+ x pk qk pa qa = begin
(pk R.+ qk) R.+ x R.* (pa R.+ qa) ≈⟨ R.+-congˡ (R.distribˡ x pa qa) ⟩
(pk R.+ qk) R.+ (x R.* pa R.+ x R.* qa) ≈⟨ transpose-sum pk qk _ _ ⟩
(pk R.+ x R.* pa) R.+ (qk R.+ x R.* qa) ∎
where
open Reasoning R.setoid
_∙_ = R._+_ -- FIXME: move this out to a lemma file
transpose-sum : ∀ a b c d → _
transpose-sum a b c d = begin
(a ∙ b) ∙ (c ∙ d) ≈⟨ R.+-assoc a b (c ∙ d) ⟩
a ∙ (b ∙ (c ∙ d)) ≈⟨ R.+-congˡ (R.sym (R.+-assoc b c d)) ⟩
a ∙ ((b ∙ c) ∙ d) ≈⟨ R.+-congˡ (R.+-congʳ (R.+-comm b c)) ⟩
a ∙ ((c ∙ b) ∙ d) ≈⟨ R.+-congˡ (R.+-assoc c b d) ⟩
a ∙ (c ∙ (b ∙ d)) ≈⟨ R.sym (R.+-assoc a c (b ∙ d)) ⟩
(a ∙ c) ∙ (b ∙ d) ∎
evalStep-*S : ∀ k x l a → k R.* (evalStep x l a) R.≈ evalStep x (k R.* l) (k R.* a)
evalStep-*S k x l a = R.trans (R.distribˡ k l _) (R.+-congˡ lemma)
where
open Reasoning R.setoid
lemma = begin -- FIXME: move this out to a lemma file
k R.* (x R.* a) ≈⟨ R.sym (R.*-assoc k x a) ⟩
(k R.* x) R.* a ≈⟨ R.*-congʳ (R.*-comm k x) ⟩
(x R.* k) R.* a ≈⟨ R.*-assoc x k a ⟩
x R.* (k R.* a) ∎
∣-zeroʳ : ∀ P → P ∣ R.0# R.≈ P ⟨ 0 ⟩
∣-zeroʳ [] = R.refl
∣-zeroʳ (x ∷ P) = R.trans (R.+-congˡ (R.zeroˡ _)) (R.+-identityʳ _)
∣-cong : ∀ {P Q x y} → P ≈ Q → x R.≈ y → P ∣ x R.≈ Q ∣ y
∣-cong {[]} {[]} P≈Q x≈y = head-≈ P≈Q
∣-cong {p ∷ P} {[]} P≈Q x≈y with p≈q , P≈Q ← uncons-≈ P≈Q with ih ← ∣-cong P≈Q x≈y = R.trans (evalStep-zeroʳ ih) p≈q
∣-cong {[]} {q ∷ Q} P≈Q x≈y with p≈q , P≈Q ← uncons-≈ P≈Q with ih ← ∣-cong P≈Q x≈y = R.trans p≈q (R.sym (evalStep-zeroʳ (R.sym ih)))
∣-cong {p ∷ P} {q ∷ Q} P≈Q x≈y with p≈q , P≈Q ← uncons-≈ P≈Q with ih ← ∣-cong P≈Q x≈y = evalStep-cong x≈y p≈q ih
*S-∣ : ∀ k P x → k R.* (P ∣ x) R.≈ (k *S P) ∣ x
*S-∣ k [] x = R.zeroʳ k
*S-∣ k (p ∷ P) x = R.trans
(evalStep-*S k x p (P ∣ x))
(evalStep-cong R.refl R.refl (*S-∣ k P x))
+-∣ : ∀ P Q x → P ∣ x R.+ Q ∣ x R.≈ (P + Q) ∣ x
+-∣ [] [] x = R.+-identityˡ R.0#
+-∣ (p ∷ P) [] x rewrite List.map-id P = R.+-identityʳ _
+-∣ [] (q ∷ Q) x rewrite List.map-id Q = R.+-identityˡ _
+-∣ (p ∷ P) (q ∷ Q) x = R.trans
(R.sym (evalStep-+ x p q (P ∣ x) (Q ∣ x)))
(evalStep-cong R.refl R.refl (+-∣ P Q x))
-- basic degree proof manipulation
degree<length : ∀ P → IsBelowDegree (length P) P
degree<length [] {k = ℕ.zero} _ = R.refl
degree<length [] {k = ℕ.suc k} _ = R.refl
degree<length (x ∷ l) (ℕ.s≤s k≥l) = degree<length l k≥l
degree-inj : ∀ {P n m}
→ IsBelowDegree n P
→ n ℕ.≤ m
→ IsBelowDegree m P
degree-inj degn n≤m m≤k = degn (ℕ.≤-trans n≤m m≤k)
degree<⊓ : ∀ {P m n}
→ IsBelowDegree m P
→ IsBelowDegree n P
→ IsBelowDegree (m ℕ.⊓ n) P
degree<⊓ {P} {m} {n} mdeg ndeg with ℕ.≤-total m n
... | inj₁ m≤n rewrite ℕ.m≤n⇒m⊓n≡m m≤n = mdeg
... | inj₂ n≤m rewrite ℕ.m≥n⇒m⊓n≡n n≤m = ndeg
-- operations preserve degree in some way
≈-degree : ∀ {P Q n}
→ IsBelowDegree n P
→ P ≈ Q
→ IsBelowDegree n Q
≈-degree deg P≈Q {k} n≤k = R.trans (R.sym (≈⟨⟩ P≈Q k)) (deg n≤k)
*S-degree : ∀ {k P n}
→ IsBelowDegree n P
→ IsBelowDegree n (k *S P)
*S-degree {l} {P} deg {k} n≤k = begin
(l *S P)ₖ ≈⟨ *S-⟨⟩ l P k ⟩
l R.* P ₖ ≈⟨ R.*-congˡ (deg n≤k) ⟩
l R.* R.0# ≈⟨ R.zeroʳ l ⟩
R.0# ∎
where
open Reasoning R.setoid
_ₖ = _⟨ k ⟩
-- -- -- +-degree : ∀ {P Q n m}
-- -- -- → IsBelowDegree n P
-- -- -- → IsBelowDegree m Q
-- -- -- → IsBelowDegree (n ℕ.⊓ m) (P + Q)
-- -- -- +-degree Pdeg Qdeg k = {! !}
-- -- -- *-degree : ∀ {P Q n m}
-- -- -- → FitsDegree n P
-- -- -- → FitsDegree m Q
-- -- -- → FitsDegree (n ℕ.+ m) (P * Q)
-- -- -- *-degree Pdeg Qdeg k = {! !}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment