2
2
-- Solver for commutative ring or semiring equalities
3
3
------------------------------------------------------------------------
5
{-# OPTIONS --universe-polymorphism #-}
5
7
-- Uses ideas from the Coq ring tactic. See "Proving Equalities in a
6
8
-- Commutative Ring Done Right in Coq" by Grégoire and Mahboubi. The
7
9
-- code below is not optimised like theirs, though.
10
12
open import Algebra.RingSolver.AlmostCommutativeRing
12
14
module Algebra.RingSolver
13
(coeff : RawRing) -- Coefficient "ring".
14
(r : AlmostCommutativeRing) -- Main "ring".
15
(morphism : coeff -Raw-AlmostCommutative⟶ r)
16
(Coeff : RawRing r₁) -- Coefficient "ring".
17
(R : AlmostCommutativeRing r₂ r₃) -- Main "ring".
18
(morphism : Coeff -Raw-AlmostCommutative⟶ R)
18
import Algebra.RingSolver.Lemmas as L; open L coeff r morphism
19
private module C = RawRing coeff
20
open AlmostCommutativeRing r hiding (zero)
21
import Algebra.RingSolver.Lemmas as L; open L Coeff R morphism
22
private module C = RawRing Coeff
23
open AlmostCommutativeRing R hiding (zero)
21
24
import Algebra.FunctionProperties as P; open P _≈_
22
25
open import Algebra.Morphism
23
26
open _-Raw-AlmostCommutative⟶_ morphism renaming (⟦_⟧ to ⟦_⟧')
30
33
open import Data.Nat using (ℕ; suc; zero) renaming (_+_ to _ℕ-+_)
31
34
open import Data.Fin as Fin using (Fin; zero; suc)
32
35
open import Data.Vec
33
open import Data.Function hiding (_∶_)
36
open import Function hiding (type-signature)
35
39
infix 9 _↑ :-_ -‿NF_
36
40
infixr 9 _:^_ _^-NF_ _:↑_
49
53
-- The polynomials are indexed over the number of variables.
51
data Polynomial (m : ℕ) : Set where
55
data Polynomial (m : ℕ) : Set r₁ where
52
56
op : (o : Op) (p₁ : Polynomial m) (p₂ : Polynomial m) → Polynomial m
53
57
con : (c : C.Carrier) → Polynomial m
54
58
var : (x : Fin m) → Polynomial m
79
83
⟦ p :^ n ⟧ ρ = ⟦ p ⟧ ρ ^ n
80
84
⟦ :- p ⟧ ρ = - ⟦ p ⟧ ρ
88
_≛_ : ∀ {n} → Polynomial n → Polynomial n → Set _
89
p₁ ≛ p₂ = ∀ {ρ} → ⟦ p₁ ⟧ ρ ≈ ⟦ p₂ ⟧ ρ
86
_≛_ : ∀ {n} → Polynomial n → Polynomial n → Set
87
p₁ ≛ p₂ = ∀ {ρ} → ⟦ p₁ ⟧ ρ ≈ ⟦ p₂ ⟧ ρ
91
95
_:↑_ : ∀ {n} → Polynomial n → (m : ℕ) → Polynomial (m ℕ-+ n)
98
102
------------------------------------------------------------------------
99
103
-- Normal forms of polynomials
103
-- The normal forms (Horner forms) are indexed over
104
-- * the number of variables in the polynomial, and
105
-- * an equivalent polynomial.
107
data Normal : (n : ℕ) → Polynomial n → Set where
108
con : (c : C.Carrier) → Normal 0 (con c)
109
_↑ : ∀ {n p'} (p : Normal n p') → Normal (suc n) (p' :↑ 1)
110
_*x+_ : ∀ {n p' c'} (p : Normal (suc n) p') (c : Normal n c') →
111
Normal (suc n) (p' :* var zero :+ c' :↑ 1)
112
_∶_ : ∀ {n p₁ p₂} (p : Normal n p₁) (eq : p₁ ≛ p₂) → Normal n p₂
114
⟦_⟧-NF : ∀ {n p} → Normal n p → Vec Carrier n → Carrier
115
⟦ p ∶ _ ⟧-NF ρ = ⟦ p ⟧-NF ρ
116
⟦ con c ⟧-NF ρ = ⟦ c ⟧'
117
⟦ p ↑ ⟧-NF (x ∷ ρ) = ⟦ p ⟧-NF ρ
118
⟦ p *x+ c ⟧-NF (x ∷ ρ) = (⟦ p ⟧-NF (x ∷ ρ) * x) + ⟦ c ⟧-NF ρ
105
-- The normal forms (Horner forms) are indexed over
106
-- * the number of variables in the polynomial, and
107
-- * an equivalent polynomial.
109
data Normal : (n : ℕ) → Polynomial n → Set (r₁ ⊔ r₂ ⊔ r₃) where
110
con : (c : C.Carrier) → Normal 0 (con c)
111
_↑ : ∀ {n p'} (p : Normal n p') → Normal (suc n) (p' :↑ 1)
112
_*x+_ : ∀ {n p' c'} (p : Normal (suc n) p') (c : Normal n c') →
113
Normal (suc n) (p' :* var zero :+ c' :↑ 1)
114
_∶_ : ∀ {n p₁ p₂} (p : Normal n p₁) (eq : p₁ ≛ p₂) → Normal n p₂
116
⟦_⟧-Normal : ∀ {n p} → Normal n p → Vec Carrier n → Carrier
117
⟦ p ∶ _ ⟧-Normal ρ = ⟦ p ⟧-Normal ρ
118
⟦ con c ⟧-Normal ρ = ⟦ c ⟧'
119
⟦ p ↑ ⟧-Normal (x ∷ ρ) = ⟦ p ⟧-Normal ρ
120
⟦ p *x+ c ⟧-Normal (x ∷ ρ) = (⟦ p ⟧-Normal (x ∷ ρ) * x) + ⟦ c ⟧-Normal ρ
120
122
------------------------------------------------------------------------
184
186
normaliseOp [+] = _+-NF_
185
187
normaliseOp [*] = _*-NF_
187
normalise : ∀ {n} (p : Polynomial n) → Normal n p
188
normalise (op o p₁ p₂) = normalise p₁ ⟨ normaliseOp o ⟩ normalise p₂
189
normalise (con c) = con-NF c
190
normalise (var i) = var-NF i
191
normalise (p :^ n) = normalise p ^-NF n
192
normalise (:- p) = -‿NF normalise p
189
normalise : ∀ {n} (p : Polynomial n) → Normal n p
190
normalise (op o p₁ p₂) = normalise p₁ ⟨ normaliseOp o ⟩ normalise p₂
191
normalise (con c) = con-NF c
192
normalise (var i) = var-NF i
193
normalise (p :^ n) = normalise p ^-NF n
194
normalise (:- p) = -‿NF normalise p
194
196
⟦_⟧↓ : ∀ {n} → Polynomial n → Vec Carrier n → Carrier
195
⟦ p ⟧↓ ρ = ⟦ normalise p ⟧-NF ρ
197
⟦ p ⟧↓ ρ = ⟦ normalise p ⟧-Normal ρ
197
199
------------------------------------------------------------------------
213
215
raise-sem (:- p) ρ = -‿cong (raise-sem p ρ)
215
217
nf-sound : ∀ {n p} (nf : Normal n p) ρ →
216
⟦ nf ⟧-NF ρ ≈ ⟦ p ⟧ ρ
218
⟦ nf ⟧-Normal ρ ≈ ⟦ p ⟧ ρ
217
219
nf-sound (nf ∶ eq) ρ = nf-sound nf ρ ⟨ trans ⟩ eq
218
220
nf-sound (con c) ρ = refl
219
221
nf-sound (_↑ {p' = p'} nf) (x ∷ ρ) =
added
removed
src/Algebra/RingSolver.agda
