open import Algebra
open import Algebra.RingSolver.AlmostCommutativeRing
module Algebra.RingSolver
(coeff : RawRing)
(r : AlmostCommutativeRing)
(morphism : coeff -Raw-AlmostCommutative⟶ r)
where
import Algebra.RingSolver.Lemmas as L; open L coeff r morphism
private module C = RawRing coeff
open AlmostCommutativeRing r hiding (zero)
import Algebra.FunctionProperties as P; open P setoid
open import Algebra.Morphism
open _-RawRing⟶_ morphism renaming (⟦_⟧ to ⟦_⟧')
import Algebra.Operations as Ops; open Ops semiring
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import Data.Nat using (ℕ; suc; zero) renaming (_+_ to _ℕ-+_)
import Data.Fin as Fin
open Fin using (Fin; zero; suc)
open import Data.Vec
open import Data.Function
infix 9 _↑-NF :-_ --NF_
infixr 9 _:^_ _^-NF_ _:↑_
infix 8 _*x _*x+_
infixl 8 _:*_ _*-NF_ _↑-*-NF_
infixl 7 _:+_ _+-NF_ _:-_
infixl 0 _∷-NF_
data Op : Set where
[+] : Op
[*] : Op
data Polynomial (m : ℕ) : Set where
op : (o : Op) (p₁ : Polynomial m) (p₂ : Polynomial m) → Polynomial m
con : (c : C.carrier) → Polynomial m
var : (x : Fin m) → Polynomial m
_:^_ : (p : Polynomial m) (n : ℕ) → Polynomial m
:-_ : (p : Polynomial m) → Polynomial m
_:+_ : ∀ {n} → Polynomial n → Polynomial n → Polynomial n
_:+_ = op [+]
_:*_ : ∀ {n} → Polynomial n → Polynomial n → Polynomial n
_:*_ = op [*]
_:-_ : ∀ {n} → Polynomial n → Polynomial n → Polynomial n
x :- y = x :+ :- y
sem : Op → Op₂
sem [+] = _+_
sem [*] = _*_
⟦_⟧_ : ∀ {n} → Polynomial n → Vec carrier n → carrier
⟦ op o p₁ p₂ ⟧ ρ = ⟦ p₁ ⟧ ρ ⟨ sem o ⟩ ⟦ p₂ ⟧ ρ
⟦ con c ⟧ ρ = ⟦ c ⟧'
⟦ var x ⟧ ρ = lookup x ρ
⟦ p :^ n ⟧ ρ = ⟦ p ⟧ ρ ^ n
⟦ :- p ⟧ ρ = - ⟦ p ⟧ ρ
private
_≛_ : ∀ {n} → Polynomial n → Polynomial n → Set
p₁ ≛ p₂ = ∀ {ρ} → ⟦ p₁ ⟧ ρ ≈ ⟦ p₂ ⟧ ρ
_:↑_ : ∀ {n} → Polynomial n → (m : ℕ) → Polynomial (m ℕ-+ n)
op o p₁ p₂ :↑ m = op o (p₁ :↑ m) (p₂ :↑ m)
con c :↑ m = con c
var x :↑ m = var (Fin.raise m x)
(p :^ n) :↑ m = (p :↑ m) :^ n
(:- p) :↑ m = :- (p :↑ m)
private
data Normal : (n : ℕ) → Polynomial n → Set where
con-NF : (c : C.carrier) → Normal 0 (con c)
_↑-NF : ∀ {n p'} (p : Normal n p') → Normal (suc n) (p' :↑ 1)
_*x+_ : ∀ {n p' c'} (p : Normal (suc n) p') (c : Normal n c') →
Normal (suc n) (p' :* var zero :+ c' :↑ 1)
_∷-NF_ : ∀ {n p₁ p₂} (p : Normal n p₁) (eq : p₁ ≛ p₂) → Normal n p₂
⟦_⟧-NF_ : ∀ {n p} → Normal n p → Vec carrier n → carrier
⟦ p ∷-NF _ ⟧-NF ρ = ⟦ p ⟧-NF ρ
⟦ con-NF c ⟧-NF ρ = ⟦ c ⟧'
⟦ p ↑-NF ⟧-NF (x ∷ ρ) = ⟦ p ⟧-NF ρ
⟦ p *x+ c ⟧-NF (x ∷ ρ) = (⟦ p ⟧-NF (x ∷ ρ) * x) + ⟦ c ⟧-NF ρ
private
con-NF⋆ : ∀ {n} → (c : C.carrier) → Normal n (con c)
con-NF⋆ {zero} c = con-NF c
con-NF⋆ {suc _} c = con-NF⋆ c ↑-NF
_+-NF_ : ∀ {n p₁ p₂} →
Normal n p₁ → Normal n p₂ → Normal n (p₁ :+ p₂)
(p₁ ∷-NF eq₁) +-NF (p₂ ∷-NF eq₂) = p₁ +-NF p₂ ∷-NF eq₁ ⟨ +-pres-≈ ⟩ eq₂
(p₁ ∷-NF eq) +-NF p₂ = p₁ +-NF p₂ ∷-NF eq ⟨ +-pres-≈ ⟩ refl
p₁ +-NF (p₂ ∷-NF eq) = p₁ +-NF p₂ ∷-NF refl ⟨ +-pres-≈ ⟩ eq
con-NF c₁ +-NF con-NF c₂ = con-NF (C._+_ c₁ c₂) ∷-NF +-homo _ _
p₁ ↑-NF +-NF p₂ ↑-NF = (p₁ +-NF p₂) ↑-NF ∷-NF refl
p₁ *x+ c₁ +-NF p₂ ↑-NF = p₁ *x+ (c₁ +-NF p₂) ∷-NF sym (+-assoc _ _ _)
p₁ *x+ c₁ +-NF p₂ *x+ c₂ = (p₁ +-NF p₂) *x+ (c₁ +-NF c₂) ∷-NF lemma₁ _ _ _ _ _
p₁ ↑-NF +-NF p₂ *x+ c₂ = p₂ *x+ (p₁ +-NF c₂) ∷-NF lemma₂ _ _ _
_*x : ∀ {n p} → Normal (suc n) p → Normal (suc n) (p :* var zero)
p *x = p *x+ con-NF⋆ C.0# ∷-NF lemma₀ _
mutual
_↑-*-NF_ : ∀ {n p₁ p₂} →
Normal n p₁ → Normal (suc n) p₂ →
Normal (suc n) (p₁ :↑ 1 :* p₂)
p₁ ↑-*-NF (p₂ ∷-NF eq) = p₁ ↑-*-NF p₂ ∷-NF refl ⟨ *-pres-≈ ⟩ eq
p₁ ↑-*-NF p₂ ↑-NF = (p₁ *-NF p₂) ↑-NF ∷-NF refl
p₁ ↑-*-NF (p₂ *x+ c₂) = (p₁ ↑-*-NF p₂) *x+ (p₁ *-NF c₂) ∷-NF lemma₄ _ _ _ _
_*-NF_ : ∀ {n p₁ p₂} →
Normal n p₁ → Normal n p₂ → Normal n (p₁ :* p₂)
(p₁ ∷-NF eq₁) *-NF (p₂ ∷-NF eq₂) = p₁ *-NF p₂ ∷-NF eq₁ ⟨ *-pres-≈ ⟩ eq₂
(p₁ ∷-NF eq) *-NF p₂ = p₁ *-NF p₂ ∷-NF eq ⟨ *-pres-≈ ⟩ refl
p₁ *-NF (p₂ ∷-NF eq) = p₁ *-NF p₂ ∷-NF refl ⟨ *-pres-≈ ⟩ eq
con-NF c₁ *-NF con-NF c₂ = con-NF (C._*_ c₁ c₂) ∷-NF *-homo _ _
p₁ ↑-NF *-NF p₂ ↑-NF = (p₁ *-NF p₂) ↑-NF ∷-NF refl
(p₁ *x+ c₁) *-NF p₂ ↑-NF = (p₁ *-NF p₂ ↑-NF) *x+ (c₁ *-NF p₂) ∷-NF lemma₃ _ _ _ _
p₁ ↑-NF *-NF (p₂ *x+ c₂) = (p₁ ↑-NF *-NF p₂) *x+ (p₁ *-NF c₂) ∷-NF lemma₄ _ _ _ _
(p₁ *x+ c₁) *-NF (p₂ *x+ c₂) =
(p₁ *-NF p₂) *x *x +-NF
(p₁ *-NF c₂ ↑-NF +-NF c₁ ↑-*-NF p₂) *x+ (c₁ *-NF c₂) ∷-NF lemma₅ _ _ _ _ _
--NF_ : ∀ {n p} → Normal n p → Normal n (:- p)
--NF_ (p ∷-NF eq) = --NF_ p ∷-NF --pres-≈ eq
--NF_ (con-NF c) = con-NF (C.-_ c) ∷-NF --homo _
--NF_ (p ↑-NF) = --NF_ p ↑-NF
--NF_ (p *x+ c) = --NF_ p *x+ --NF_ c ∷-NF lemma₆ _ _ _
var-NF : ∀ {n} → (i : Fin n) → Normal n (var i)
var-NF zero = con-NF⋆ C.1# *x+ con-NF⋆ C.0# ∷-NF lemma₇ _
var-NF (suc i) = var-NF i ↑-NF
_^-NF_ : ∀ {n p} → Normal n p → (i : ℕ) → Normal n (p :^ i)
p ^-NF zero = con-NF⋆ C.1# ∷-NF 1-homo
p ^-NF suc n = p *-NF p ^-NF n ∷-NF refl
normaliseOp : ∀ (o : Op) {n p₁ p₂} →
Normal n p₁ → Normal n p₂ → Normal n (p₁ ⟨ op o ⟩ p₂)
normaliseOp [+] = _+-NF_
normaliseOp [*] = _*-NF_
normalise : ∀ {n} (p : Polynomial n) → Normal n p
normalise (op o p₁ p₂) = normalise p₁ ⟨ normaliseOp o ⟩ normalise p₂
normalise (con c) = con-NF⋆ c
normalise (var i) = var-NF i
normalise (p :^ n) = normalise p ^-NF n
normalise (:- p) = --NF normalise p
⟦_⟧↓_ : ∀ {n} → Polynomial n → Vec carrier n → carrier
⟦ p ⟧↓ ρ = ⟦ normalise p ⟧-NF ρ
private
sem-pres-≈ : ∀ op → sem op Preserves₂ _≈_ ⟶ _≈_ ⟶ _≈_
sem-pres-≈ [+] = +-pres-≈
sem-pres-≈ [*] = *-pres-≈
raise-sem : ∀ {n x} (p : Polynomial n) ρ →
⟦ p :↑ 1 ⟧ (x ∷ ρ) ≈ ⟦ p ⟧ ρ
raise-sem (op o p₁ p₂) ρ = raise-sem p₁ ρ ⟨ sem-pres-≈ o ⟩
raise-sem p₂ ρ
raise-sem (con c) ρ = refl
raise-sem (var x) ρ = refl
raise-sem (p :^ n) ρ = raise-sem p ρ ⟨ ^-pres-≈ ⟩ ≡-refl {x = n}
raise-sem (:- p) ρ = --pres-≈ (raise-sem p ρ)
nf-sound : ∀ {n p} (nf : Normal n p) ρ →
⟦ nf ⟧-NF ρ ≈ ⟦ p ⟧ ρ
nf-sound (nf ∷-NF eq) ρ = nf-sound nf ρ ⟨ trans ⟩ eq
nf-sound (con-NF c) ρ = refl
nf-sound (_↑-NF {p' = p'} nf) (x ∷ ρ) =
nf-sound nf ρ ⟨ trans ⟩ sym (raise-sem p' ρ)
nf-sound (_*x+_ {c' = c'} nf₁ nf₂) (x ∷ ρ) =
(nf-sound nf₁ (x ∷ ρ) ⟨ *-pres-≈ ⟩ refl)
⟨ +-pres-≈ ⟩
(nf-sound nf₂ ρ ⟨ trans ⟩ sym (raise-sem c' ρ))
prove : ∀ {n} (ρ : Vec carrier n) p₁ p₂ →
⟦ p₁ ⟧↓ ρ ≈ ⟦ p₂ ⟧↓ ρ →
⟦ p₁ ⟧ ρ ≈ ⟦ p₂ ⟧ ρ
prove ρ p₁ p₂ eq =
sym (nf-sound (normalise p₁) ρ)
⟨ trans ⟩
eq
⟨ trans ⟩
nf-sound (normalise p₂) ρ