« back to all changes in this revision
Viewing changes to src/Algebra/RingSolver.agda
- browse files at revision 11
- compare with another revision
- download diff
- download tarball
- view history from revision 11
- Committer: Package Import Robot
- Author(s): Iain Lane
- Date: 2013-04-10 10:30:20 UTC
- mfrom: (2.1.7 experimental)
- Revision ID: package-import@ubuntu.com-20130410103020-bcspfz3whyy5iafu
Tags: 0.7-1
* [6d52289] Imported Upstream version 0.7
* [54104d0] Update Depends and Build-Depends for this version, compatible
with Agda 2.3.2
* [b3ddce4] No need for the .install file to be executable (thanks lintian)
* [a9a6cb7] Standards-Version → 3.9.4, no changes required
* [54104d0] Update Depends and Build-Depends for this version, compatible
with Agda 2.3.2
* [b3ddce4] No need for the .install file to be executable (thanks lintian)
* [a9a6cb7] Standards-Version → 3.9.4, no changes required
- files added:
- .pc
- src/Category/Monad/Partiality
- files modified:
- Everything.agda
- debian/agda-stdlib.install *
added
removed
src/Algebra/RingSolver.agda
6
6
7
7
-- Uses ideas from the Coq ring tactic. See "Proving Equalities in a
8
8
-- Commutative Ring Done Right in Coq" by Grégoire and Mahboubi. The
9
-- code below is not optimised like theirs, though (in particular, our
10
-- Horner normal forms are not sparse).
9
11
10
12
open import Algebra
11
13
open import Algebra.RingSolver.AlmostCommutativeRing
12
14
15
open import Relation.Binary
16
13
17
module Algebra.RingSolver
14
18
{r₁ r₂ r₃}
15
19
(Coeff : RawRing r₁) -- Coefficient "ring".
16
20
(R : AlmostCommutativeRing r₂ r₃) -- Main "ring".
17
21
(morphism : Coeff -Raw-AlmostCommutative⟶ R)
22
(_coeff≟_ : Decidable (Induced-equivalence morphism))
18
23
where
19
24
20
25
import Algebra.RingSolver.Lemmas as L; open L Coeff R morphism
21
26
private module C = RawRing Coeff
22
open AlmostCommutativeRing R hiding (zero)
27
open AlmostCommutativeRing R renaming (zero to zero*)
23
28
import Algebra.FunctionProperties as P; open P _≈_
24
29
open import Algebra.Morphism
25
open _-Raw-AlmostCommutative⟶_ morphism renaming (⟦_⟧ to ⟦_⟧')
30
open _-Raw-AlmostCommutative⟶_ morphism renaming (⟦_⟧ to ⟦_⟧′)
26
31
import Algebra.Operations as Ops; open Ops semiring
27
32
28
33
open import Relation.Binary
34
open import Relation.Nullary.Core
35
import Relation.Binary.EqReasoning as EqR; open EqR setoid
29
36
import Relation.Binary.PropositionalEquality as PropEq
30
37
import Relation.Binary.Reflection as Reflection
31
38
32
open import Data.Nat using (ℕ; suc; zero) renaming (_+_ to _ℕ-+_)
39
open import Data.Empty
40
open import Data.Product
41
open import Data.Nat as Nat using (ℕ; suc; zero)
33
42
open import Data.Fin as Fin using (Fin; zero; suc)
34
43
open import Data.Vec
35
open import Function hiding (type-signature)
44
open import Function
36
45
open import Level using (_⊔_)
37
46
38
infix 9 _↑ :-_ -‿NF_
39
infixr 9 _:^_ _^-NF_ _:↑_
40
infix 8 _*x _*x+_
41
infixl 8 _:*_ _*-NF_ _↑-*-NF_
42
infixl 7 _:+_ _+-NF_ _:-_
43
infixl 0 _∶_
47
infix 9 :-_ -H_ -N_
48
infixr 9 _:^_ _^N_
49
infix 8 _*x+_ _*x+HN_ _*x+H_
50
infixl 8 _:*_ _*N_ _*H_ _*NH_ _*HN_
51
infixl 7 _:+_ _:-_ _+H_ _+N_
52
infix 4 _≈H_ _≈N_
44
53
45
54
------------------------------------------------------------------------
46
55
-- Polynomials
50
58
[+] : Op
51
59
[*] : Op
52
60
61
-- The polynomials are indexed by the number of variables.
53
62
54
63
data Polynomial (m : ℕ) : Set r₁ where
55
64
op : (o : Op) (p₁ : Polynomial m) (p₂ : Polynomial m) → Polynomial m
78
86
79
87
⟦_⟧ : ∀ {n} → Polynomial n → Vec Carrier n → Carrier
80
88
⟦ op o p₁ p₂ ⟧ ρ = ⟦ p₁ ⟧ ρ ⟨ sem o ⟩ ⟦ p₂ ⟧ ρ
81
⟦ con c ⟧ ρ = ⟦ c ⟧'
82
⟦ var x ⟧ ρ = lookup x ρ
83
⟦ p :^ n ⟧ ρ = ⟦ p ⟧ ρ ^ n
84
⟦ :- p ⟧ ρ = - ⟦ p ⟧ ρ
85
86
87
_≛_ : ∀ {n} → Polynomial n → Polynomial n → Set _
88
p₁ ≛ p₂ = ∀ {ρ} → ⟦ p₁ ⟧ ρ ≈ ⟦ p₂ ⟧ ρ
89
90
private
91
92
-- Reindexing.
93
94
_:↑_ : ∀ {n} → Polynomial n → (m : ℕ) → Polynomial (m ℕ-+ n)
95
op o p₁ p₂ :↑ m = op o (p₁ :↑ m) (p₂ :↑ m)
96
con c :↑ m = con c
97
var x :↑ m = var (Fin.raise m x)
98
(p :^ n) :↑ m = (p :↑ m) :^ n
99
(:- p) :↑ m = :- (p :↑ m)
89
⟦ con c ⟧ ρ = ⟦ c ⟧′
90
⟦ var x ⟧ ρ = lookup x ρ
91
⟦ p :^ n ⟧ ρ = ⟦ p ⟧ ρ ^ n
92
⟦ :- p ⟧ ρ = - ⟦ p ⟧ ρ
100
93
101
94
------------------------------------------------------------------------
102
95
-- Normal forms of polynomials
103
96
104
105
data Normal : (n : ℕ) → Polynomial n → Set (r₁ ⊔ r₂ ⊔ r₃) where
106
con : (c : C.Carrier) → Normal 0 (con c)
107
_↑ : ∀ {n p'} (p : Normal n p') → Normal (suc n) (p' :↑ 1)
108
_*x+_ : ∀ {n p' c'} (p : Normal (suc n) p') (c : Normal n c') →
109
Normal (suc n) (p' :* var zero :+ c' :↑ 1)
110
_∶_ : ∀ {n p₁ p₂} (p : Normal n p₁) (eq : p₁ ≛ p₂) → Normal n p₂
111
112
⟦_⟧-Normal : ∀ {n p} → Normal n p → Vec Carrier n → Carrier
113
⟦ p ∶ _ ⟧-Normal ρ = ⟦ p ⟧-Normal ρ
114
⟦ con c ⟧-Normal ρ = ⟦ c ⟧'
115
⟦ p ↑ ⟧-Normal (x ∷ ρ) = ⟦ p ⟧-Normal ρ
116
⟦ p *x+ c ⟧-Normal (x ∷ ρ) = (⟦ p ⟧-Normal (x ∷ ρ) * x) + ⟦ c ⟧-Normal ρ
97
-- A univariate polynomial of degree d,
98
--
99
-- p = a_d x^d + a_{d-1}x^{d-1} + … + a_0,
100
--
101
-- is represented in Horner normal form by
102
--
103
-- p = ((a_d x + a_{d-1})x + …)x + a_0.
104
--
105
-- Note that Horner normal forms can be represented as lists, with the
106
-- empty list standing for the zero polynomial of degree "-1".
107
--
108
-- Given this representation of univariate polynomials over an
109
-- arbitrary ring, polynomials in any number of variables over the
110
-- ring C can be represented via the isomorphisms
111
--
112
-- C[] ≅ C
113
--
114
-- and
115
--
116
-- C[X_0,...X_{n+1}] ≅ C[X_0,...,X_n][X_{n+1}].
117
118
mutual
119
120
-- The polynomial representations are indexed by the polynomial's
121
-- degree.
122
123
data HNF : ℕ → Set r₁ where
124
∅ : ∀ {n} → HNF (suc n)
125
_*x+_ : ∀ {n} → HNF (suc n) → Normal n → HNF (suc n)
126
127
data Normal : ℕ → Set r₁ where
128
con : C.Carrier → Normal zero
129
poly : ∀ {n} → HNF (suc n) → Normal (suc n)
130
131
-- Note that the data types above do /not/ ensure uniqueness of
132
-- normal forms: the zero polynomial of degree one can be
133
-- represented using both ∅ and ∅ *x+ con C.0#.
134
135
mutual
136
137
-- Semantics.
138
139
⟦_⟧H : ∀ {n} → HNF (suc n) → Vec Carrier (suc n) → Carrier
140
⟦ ∅ ⟧H _ = 0#
141
⟦ p *x+ c ⟧H (x ∷ ρ) = ⟦ p ⟧H (x ∷ ρ) * x + ⟦ c ⟧N ρ
142
143
⟦_⟧N : ∀ {n} → Normal n → Vec Carrier n → Carrier
144
⟦ con c ⟧N _ = ⟦ c ⟧′
145
⟦ poly p ⟧N ρ = ⟦ p ⟧H ρ
146
147
------------------------------------------------------------------------
148
-- Equality and decidability
149
150
mutual
151
152
-- Equality.
153
154
data _≈H_ : ∀ {n} → HNF n → HNF n → Set (r₁ ⊔ r₃) where
155
∅ : ∀ {n} → _≈H_ {suc n} ∅ ∅
156
_*x+_ : ∀ {n} {p₁ p₂ : HNF (suc n)} {c₁ c₂ : Normal n} →
157
p₁ ≈H p₂ → c₁ ≈N c₂ → (p₁ *x+ c₁) ≈H (p₂ *x+ c₂)
158
159
data _≈N_ : ∀ {n} → Normal n → Normal n → Set (r₁ ⊔ r₃) where
160
con : ∀ {c₁ c₂} → ⟦ c₁ ⟧′ ≈ ⟦ c₂ ⟧′ → con c₁ ≈N con c₂
161
poly : ∀ {n} {p₁ p₂ : HNF (suc n)} → p₁ ≈H p₂ → poly p₁ ≈N poly p₂
162
163
mutual
164
165
-- Equality is decidable.
166
167
_≟H_ : ∀ {n} → Decidable (_≈H_ {n = n})
168
∅ ≟H ∅ = yes ∅
169
∅ ≟H (_ *x+ _) = no λ()
170
(_ *x+ _) ≟H ∅ = no λ()
171
(p₁ *x+ c₁) ≟H (p₂ *x+ c₂) with p₁ ≟H p₂ | c₁ ≟N c₂
172
... | yes p₁≈p₂ | yes c₁≈c₂ = yes (p₁≈p₂ *x+ c₁≈c₂)
173
... | _ | no c₁≉c₂ = no λ { (_ *x+ c₁≈c₂) → c₁≉c₂ c₁≈c₂ }
174
... | no p₁≉p₂ | _ = no λ { (p₁≈p₂ *x+ _) → p₁≉p₂ p₁≈p₂ }
175
176
_≟N_ : ∀ {n} → Decidable (_≈N_ {n = n})
177
con c₁ ≟N con c₂ with c₁ coeff≟ c₂
178
... | yes c₁≈c₂ = yes (con c₁≈c₂)
179
... | no c₁≉c₂ = no λ { (con c₁≈c₂) → c₁≉c₂ c₁≈c₂}
180
poly p₁ ≟N poly p₂ with p₁ ≟H p₂
181
... | yes p₁≈p₂ = yes (poly p₁≈p₂)
182
... | no p₁≉p₂ = no λ { (poly p₁≈p₂) → p₁≉p₂ p₁≈p₂ }
183
184
mutual
185
186
-- The semantics respect the equality relations defined above.
187
188
⟦_⟧H-cong : ∀ {n} {p₁ p₂ : HNF (suc n)} →
189
p₁ ≈H p₂ → ∀ ρ → ⟦ p₁ ⟧H ρ ≈ ⟦ p₂ ⟧H ρ
190
⟦ ∅ ⟧H-cong _ = refl
191
⟦ p₁≈p₂ *x+ c₁≈c₂ ⟧H-cong (x ∷ ρ) =
192
(⟦ p₁≈p₂ ⟧H-cong (x ∷ ρ) ⟨ *-cong ⟩ refl)
193
⟨ +-cong ⟩
194
⟦ c₁≈c₂ ⟧N-cong ρ
195
196
⟦_⟧N-cong :
197
∀ {n} {p₁ p₂ : Normal n} →
198
p₁ ≈N p₂ → ∀ ρ → ⟦ p₁ ⟧N ρ ≈ ⟦ p₂ ⟧N ρ
199
⟦ con c₁≈c₂ ⟧N-cong _ = c₁≈c₂
200
⟦ poly p₁≈p₂ ⟧N-cong ρ = ⟦ p₁≈p₂ ⟧H-cong ρ
201
202
------------------------------------------------------------------------
203
-- Ring operations on Horner normal forms
204
205
-- Zero.
206
207
0H : ∀ {n} → HNF (suc n)
208
0H = ∅
209
210
0N : ∀ {n} → Normal n
211
0N {zero} = con C.0#
212
0N {suc n} = poly 0H
213
214
mutual
215
216
-- One.
217
218
1H : ∀ {n} → HNF (suc n)
219
1H {n} = ∅ *x+ 1N {n}
220
221
1N : ∀ {n} → Normal n
222
1N {zero} = con C.1#
223
1N {suc n} = poly 1H
224
225
-- A simplifying variant of _*x+_.
226
227
_*x+HN_ : ∀ {n} → HNF (suc n) → Normal n → HNF (suc n)
228
(p *x+ c′) *x+HN c = (p *x+ c′) *x+ c
229
∅ *x+HN c with c ≟N 0N
230
... | yes c≈0 = ∅
231
... | no c≉0 = ∅ *x+ c
232
233
mutual
234
235
-- Addition.
236
237
_+H_ : ∀ {n} → HNF (suc n) → HNF (suc n) → HNF (suc n)
238
∅ +H p = p
239
p +H ∅ = p
240
(p₁ *x+ c₁) +H (p₂ *x+ c₂) = (p₁ +H p₂) *x+HN (c₁ +N c₂)
241
242
_+N_ : ∀ {n} → Normal n → Normal n → Normal n
243
con c₁ +N con c₂ = con (c₁ C.+ c₂)
244
poly p₁ +N poly p₂ = poly (p₁ +H p₂)
245
246
-- Multiplication.
247
248
_*x+H_ : ∀ {n} → HNF (suc n) → HNF (suc n) → HNF (suc n)
249
p₁ *x+H (p₂ *x+ c) = (p₁ +H p₂) *x+HN c
250
∅ *x+H ∅ = ∅
251
(p₁ *x+ c) *x+H ∅ = (p₁ *x+ c) *x+ 0N
252
253
mutual
254
255
_*NH_ : ∀ {n} → Normal n → HNF (suc n) → HNF (suc n)
256
c *NH ∅ = ∅
257
c *NH (p *x+ c′) with c ≟N 0N
258
... | yes c≈0 = ∅
259
... | no c≉0 = (c *NH p) *x+ (c *N c′)
260
261
_*HN_ : ∀ {n} → HNF (suc n) → Normal n → HNF (suc n)
262
∅ *HN c = ∅
263
(p *x+ c′) *HN c with c ≟N 0N
264
... | yes c≈0 = ∅
265
... | no c≉0 = (p *HN c) *x+ (c′ *N c)
266
267
_*H_ : ∀ {n} → HNF (suc n) → HNF (suc n) → HNF (suc n)
268
∅ *H _ = ∅
269
(_ *x+ _) *H ∅ = ∅
270
(p₁ *x+ c₁) *H (p₂ *x+ c₂) =
271
((p₁ *H p₂) *x+H (p₁ *HN c₂ +H c₁ *NH p₂)) *x+HN (c₁ *N c₂)
272
273
_*N_ : ∀ {n} → Normal n → Normal n → Normal n
274
con c₁ *N con c₂ = con (c₁ C.* c₂)
275
poly p₁ *N poly p₂ = poly (p₁ *H p₂)
276
277
-- Exponentiation.
278
279
_^N_ : ∀ {n} → Normal n → ℕ → Normal n
280
p ^N zero = 1N
281
p ^N suc n = p *N (p ^N n)
282
283
mutual
284
285
-- Negation.
286
287
-H_ : ∀ {n} → HNF (suc n) → HNF (suc n)
288
-H p = (-N 1N) *NH p
289
290
-N_ : ∀ {n} → Normal n → Normal n
291
-N con c = con (C.- c)
292
-N poly p = poly (-H p)
117
293
118
294
------------------------------------------------------------------------
119
295
-- Normalisation
120
296
121
private
122
123
con-NF : ∀ {n} → (c : C.Carrier) → Normal n (con c)
124
con-NF {zero} c = con c
125
con-NF {suc _} c = con-NF c ↑
126
127
_+-NF_ : ∀ {n p₁ p₂} → Normal n p₁ → Normal n p₂ → Normal n (p₁ :+ p₂)
128
(p₁ ∶ eq₁) +-NF (p₂ ∶ eq₂) = p₁ +-NF p₂ ∶ eq₁ ⟨ +-cong ⟩ eq₂
129
(p₁ ∶ eq) +-NF p₂ = p₁ +-NF p₂ ∶ eq ⟨ +-cong ⟩ refl
130
p₁ +-NF (p₂ ∶ eq) = p₁ +-NF p₂ ∶ refl ⟨ +-cong ⟩ eq
131
con c₁ +-NF con c₂ = con (C._+_ c₁ c₂) ∶ +-homo _ _
132
p₁ ↑ +-NF p₂ ↑ = (p₁ +-NF p₂) ↑ ∶ refl
133
p₁ *x+ c₁ +-NF p₂ ↑ = p₁ *x+ (c₁ +-NF p₂) ∶ sym (+-assoc _ _ _)
134
p₁ *x+ c₁ +-NF p₂ *x+ c₂ = (p₁ +-NF p₂) *x+ (c₁ +-NF c₂) ∶ lemma₁ _ _ _ _ _
135
p₁ ↑ +-NF p₂ *x+ c₂ = p₂ *x+ (p₁ +-NF c₂) ∶ lemma₂ _ _ _
136
137
_*x : ∀ {n p} → Normal (suc n) p → Normal (suc n) (p :* var zero)
138
p *x = p *x+ con-NF C.0# ∶ lemma₀ _
139
140
mutual
141
142
-- The first function is just a variant of _*-NF_ which I used to
143
-- make the termination checker believe that the code is
144
-- terminating.
145
146
_↑-*-NF_ : ∀ {n p₁ p₂} →
147
Normal n p₁ → Normal (suc n) p₂ →
148
Normal (suc n) (p₁ :↑ 1 :* p₂)
149
p₁ ↑-*-NF (p₂ ∶ eq) = p₁ ↑-*-NF p₂ ∶ refl ⟨ *-cong ⟩ eq
150
p₁ ↑-*-NF p₂ ↑ = (p₁ *-NF p₂) ↑ ∶ refl
151
p₁ ↑-*-NF (p₂ *x+ c₂) = (p₁ ↑-*-NF p₂) *x+ (p₁ *-NF c₂) ∶ lemma₄ _ _ _ _
152
153
_*-NF_ : ∀ {n p₁ p₂} →
154
Normal n p₁ → Normal n p₂ → Normal n (p₁ :* p₂)
155
(p₁ ∶ eq₁) *-NF (p₂ ∶ eq₂) = p₁ *-NF p₂ ∶ eq₁ ⟨ *-cong ⟩ eq₂
156
(p₁ ∶ eq) *-NF p₂ = p₁ *-NF p₂ ∶ eq ⟨ *-cong ⟩ refl
157
p₁ *-NF (p₂ ∶ eq) = p₁ *-NF p₂ ∶ refl ⟨ *-cong ⟩ eq
158
con c₁ *-NF con c₂ = con (C._*_ c₁ c₂) ∶ *-homo _ _
159
p₁ ↑ *-NF p₂ ↑ = (p₁ *-NF p₂) ↑ ∶ refl
160
(p₁ *x+ c₁) *-NF p₂ ↑ = (p₁ *-NF p₂ ↑) *x+ (c₁ *-NF p₂) ∶ lemma₃ _ _ _ _
161
p₁ ↑ *-NF (p₂ *x+ c₂) = (p₁ ↑ *-NF p₂) *x+ (p₁ *-NF c₂) ∶ lemma₄ _ _ _ _
162
(p₁ *x+ c₁) *-NF (p₂ *x+ c₂) =
163
(p₁ *-NF p₂) *x *x +-NF
164
(p₁ *-NF c₂ ↑ +-NF c₁ ↑-*-NF p₂) *x+ (c₁ *-NF c₂) ∶ lemma₅ _ _ _ _ _
165
166
-‿NF_ : ∀ {n p} → Normal n p → Normal n (:- p)
167
-‿NF (p ∶ eq) = -‿NF p ∶ -‿cong eq
168
-‿NF con c = con (C.-_ c) ∶ -‿homo _
169
-‿NF (p ↑) = (-‿NF p) ↑
170
-‿NF (p *x+ c) = -‿NF p *x+ -‿NF c ∶ lemma₆ _ _ _
171
172
var-NF : ∀ {n} → (i : Fin n) → Normal n (var i)
173
var-NF zero = con-NF C.1# *x+ con-NF C.0# ∶ lemma₇ _
174
var-NF (suc i) = var-NF i ↑
175
176
_^-NF_ : ∀ {n p} → Normal n p → (i : ℕ) → Normal n (p :^ i)
177
p ^-NF zero = con-NF C.1# ∶ 1-homo
178
p ^-NF suc n = p *-NF p ^-NF n ∶ refl
179
180
normaliseOp : ∀ (o : Op) {n p₁ p₂} →
181
Normal n p₁ → Normal n p₂ → Normal n (p₁ ⟨ op o ⟩ p₂)
182
normaliseOp [+] = _+-NF_
183
normaliseOp [*] = _*-NF_
184
185
normalise : ∀ {n} (p : Polynomial n) → Normal n p
186
normalise (op o p₁ p₂) = normalise p₁ ⟨ normaliseOp o ⟩ normalise p₂
187
normalise (con c) = con-NF c
188
normalise (var i) = var-NF i
189
normalise (p :^ n) = normalise p ^-NF n
190
normalise (:- p) = -‿NF normalise p
297
normalise-con : ∀ {n} → C.Carrier → Normal n
298
normalise-con {zero} c = con c
299
normalise-con {suc n} c = poly (∅ *x+HN normalise-con c)
300
301
normalise-var : ∀ {n} → Fin n → Normal n
302
normalise-var zero = poly ((∅ *x+ 1N) *x+ 0N)
303
normalise-var (suc i) = poly (∅ *x+HN normalise-var i)
304
305
normalise : ∀ {n} → Polynomial n → Normal n
306
normalise (op [+] t₁ t₂) = normalise t₁ +N normalise t₂
307
normalise (op [*] t₁ t₂) = normalise t₁ *N normalise t₂
308
normalise (con c) = normalise-con c
309
normalise (var i) = normalise-var i
310
normalise (t :^ k) = normalise t ^N k
311
normalise (:- t) = -N normalise t
312
313
-- Evaluation after normalisation.
191
314
192
315
⟦_⟧↓ : ∀ {n} → Polynomial n → Vec Carrier n → Carrier
193
⟦ p ⟧↓ ρ = ⟦ normalise p ⟧-Normal ρ
316
⟦ p ⟧↓ ρ = ⟦ normalise p ⟧N ρ
317
318
------------------------------------------------------------------------
319
-- Homomorphism lemmas
320
321
0N-homo : ∀ {n} ρ → ⟦ 0N {n} ⟧N ρ ≈ 0#
322
0N-homo [] = 0-homo
323
0N-homo (x ∷ ρ) = refl
324
325
-- If c is equal to 0N, then c is semantically equal to 0#.
326
327
0≈⟦0⟧ : ∀ {n} {c : Normal n} → c ≈N 0N → ∀ ρ → 0# ≈ ⟦ c ⟧N ρ
328
0≈⟦0⟧ {c = c} c≈0 ρ = sym (begin
329
⟦ c ⟧N ρ ≈⟨ ⟦ c≈0 ⟧N-cong ρ ⟩
330
⟦ 0N ⟧N ρ ≈⟨ 0N-homo ρ ⟩
331
0# ∎)
332
333
1N-homo : ∀ {n} ρ → ⟦ 1N {n} ⟧N ρ ≈ 1#
334
1N-homo [] = 1-homo
335
1N-homo (x ∷ ρ) = begin
336
0# * x + ⟦ 1N ⟧N ρ ≈⟨ refl ⟨ +-cong ⟩ 1N-homo ρ ⟩
337
0# * x + 1# ≈⟨ lemma₆ _ _ ⟩
338
1# ∎
339
340
-- _*x+HN_ is equal to _*x+_.
341
342
*x+HN≈*x+ : ∀ {n} (p : HNF (suc n)) (c : Normal n) →
343
∀ ρ → ⟦ p *x+HN c ⟧H ρ ≈ ⟦ p *x+ c ⟧H ρ
344
*x+HN≈*x+ (p *x+ c′) c ρ = refl
345
*x+HN≈*x+ ∅ c (x ∷ ρ) with c ≟N 0N
346
... | yes c≈0 = begin
347
0# ≈⟨ 0≈⟦0⟧ c≈0 ρ ⟩
348
⟦ c ⟧N ρ ≈⟨ sym $ lemma₆ _ _ ⟩
349
0# * x + ⟦ c ⟧N ρ ∎
350
... | no c≉0 = refl
351
352
∅*x+HN-homo : ∀ {n} (c : Normal n) x ρ →
353
⟦ ∅ *x+HN c ⟧H (x ∷ ρ) ≈ ⟦ c ⟧N ρ
354
∅*x+HN-homo c x ρ with c ≟N 0N
355
... | yes c≈0 = 0≈⟦0⟧ c≈0 ρ
356
... | no c≉0 = lemma₆ _ _
357
358
mutual
359
360
+H-homo : ∀ {n} (p₁ p₂ : HNF (suc n)) →
361
∀ ρ → ⟦ p₁ +H p₂ ⟧H ρ ≈ ⟦ p₁ ⟧H ρ + ⟦ p₂ ⟧H ρ
362
+H-homo ∅ p₂ ρ = sym (proj₁ +-identity _)
363
+H-homo (p₁ *x+ x₁) ∅ ρ = sym (proj₂ +-identity _)
364
+H-homo (p₁ *x+ c₁) (p₂ *x+ c₂) (x ∷ ρ) = begin
365
⟦ (p₁ +H p₂) *x+HN (c₁ +N c₂) ⟧H (x ∷ ρ) ≈⟨ *x+HN≈*x+ (p₁ +H p₂) (c₁ +N c₂) (x ∷ ρ) ⟩
366
367
⟦ p₁ +H p₂ ⟧H (x ∷ ρ) * x + ⟦ c₁ +N c₂ ⟧N ρ ≈⟨ (+H-homo p₁ p₂ (x ∷ ρ) ⟨ *-cong ⟩ refl) ⟨ +-cong ⟩ +N-homo c₁ c₂ ρ ⟩
368
369
(⟦ p₁ ⟧H (x ∷ ρ) + ⟦ p₂ ⟧H (x ∷ ρ)) * x + (⟦ c₁ ⟧N ρ + ⟦ c₂ ⟧N ρ) ≈⟨ lemma₁ _ _ _ _ _ ⟩
370
371
(⟦ p₁ ⟧H (x ∷ ρ) * x + ⟦ c₁ ⟧N ρ) +
372
(⟦ p₂ ⟧H (x ∷ ρ) * x + ⟦ c₂ ⟧N ρ) ∎
373
374
+N-homo : ∀ {n} (p₁ p₂ : Normal n) →
375
∀ ρ → ⟦ p₁ +N p₂ ⟧N ρ ≈ ⟦ p₁ ⟧N ρ + ⟦ p₂ ⟧N ρ
376
+N-homo (con c₁) (con c₂) _ = +-homo _ _
377
+N-homo (poly p₁) (poly p₂) ρ = +H-homo p₁ p₂ ρ
378
379
*x+H-homo :
380
∀ {n} (p₁ p₂ : HNF (suc n)) x ρ →
381
⟦ p₁ *x+H p₂ ⟧H (x ∷ ρ) ≈
382
⟦ p₁ ⟧H (x ∷ ρ) * x + ⟦ p₂ ⟧H (x ∷ ρ)
383
*x+H-homo ∅ ∅ _ _ = sym $ lemma₆ _ _
384
*x+H-homo (p *x+ c) ∅ x ρ = begin
385
⟦ p *x+ c ⟧H (x ∷ ρ) * x + ⟦ 0N ⟧N ρ ≈⟨ refl ⟨ +-cong ⟩ 0N-homo ρ ⟩
386
⟦ p *x+ c ⟧H (x ∷ ρ) * x + 0# ∎
387
*x+H-homo p₁ (p₂ *x+ c₂) x ρ = begin
388
⟦ (p₁ +H p₂) *x+HN c₂ ⟧H (x ∷ ρ) ≈⟨ *x+HN≈*x+ (p₁ +H p₂) c₂ (x ∷ ρ) ⟩
389
⟦ p₁ +H p₂ ⟧H (x ∷ ρ) * x + ⟦ c₂ ⟧N ρ ≈⟨ (+H-homo p₁ p₂ (x ∷ ρ) ⟨ *-cong ⟩ refl) ⟨ +-cong ⟩ refl ⟩
390
(⟦ p₁ ⟧H (x ∷ ρ) + ⟦ p₂ ⟧H (x ∷ ρ)) * x + ⟦ c₂ ⟧N ρ ≈⟨ lemma₀ _ _ _ _ ⟩
391
⟦ p₁ ⟧H (x ∷ ρ) * x + (⟦ p₂ ⟧H (x ∷ ρ) * x + ⟦ c₂ ⟧N ρ) ∎
392
393
mutual
394
395
*NH-homo :
396
∀ {n} (c : Normal n) (p : HNF (suc n)) x ρ →
397
⟦ c *NH p ⟧H (x ∷ ρ) ≈ ⟦ c ⟧N ρ * ⟦ p ⟧H (x ∷ ρ)
398
*NH-homo c ∅ x ρ = sym (proj₂ zero* _)
399
*NH-homo c (p *x+ c′) x ρ with c ≟N 0N
400
... | yes c≈0 = begin
401
0# ≈⟨ sym (proj₁ zero* _) ⟩
402
0# * (⟦ p ⟧H (x ∷ ρ) * x + ⟦ c′ ⟧N ρ) ≈⟨ 0≈⟦0⟧ c≈0 ρ ⟨ *-cong ⟩ refl ⟩
403
⟦ c ⟧N ρ * (⟦ p ⟧H (x ∷ ρ) * x + ⟦ c′ ⟧N ρ) ∎
404
... | no c≉0 = begin
405
⟦ c *NH p ⟧H (x ∷ ρ) * x + ⟦ c *N c′ ⟧N ρ ≈⟨ (*NH-homo c p x ρ ⟨ *-cong ⟩ refl) ⟨ +-cong ⟩ *N-homo c c′ ρ ⟩
406
(⟦ c ⟧N ρ * ⟦ p ⟧H (x ∷ ρ)) * x + (⟦ c ⟧N ρ * ⟦ c′ ⟧N ρ) ≈⟨ lemma₃ _ _ _ _ ⟩
407
⟦ c ⟧N ρ * (⟦ p ⟧H (x ∷ ρ) * x + ⟦ c′ ⟧N ρ) ∎
408
409
*HN-homo :
410
∀ {n} (p : HNF (suc n)) (c : Normal n) x ρ →
411
⟦ p *HN c ⟧H (x ∷ ρ) ≈ ⟦ p ⟧H (x ∷ ρ) * ⟦ c ⟧N ρ
412
*HN-homo ∅ c x ρ = sym (proj₁ zero* _)
413
*HN-homo (p *x+ c′) c x ρ with c ≟N 0N
414
... | yes c≈0 = begin
415
0# ≈⟨ sym (proj₂ zero* _) ⟩
416
(⟦ p ⟧H (x ∷ ρ) * x + ⟦ c′ ⟧N ρ) * 0# ≈⟨ refl ⟨ *-cong ⟩ 0≈⟦0⟧ c≈0 ρ ⟩
417
(⟦ p ⟧H (x ∷ ρ) * x + ⟦ c′ ⟧N ρ) * ⟦ c ⟧N ρ ∎
418
... | no c≉0 = begin
419
⟦ p *HN c ⟧H (x ∷ ρ) * x + ⟦ c′ *N c ⟧N ρ ≈⟨ (*HN-homo p c x ρ ⟨ *-cong ⟩ refl) ⟨ +-cong ⟩ *N-homo c′ c ρ ⟩
420
(⟦ p ⟧H (x ∷ ρ) * ⟦ c ⟧N ρ) * x + (⟦ c′ ⟧N ρ * ⟦ c ⟧N ρ) ≈⟨ lemma₂ _ _ _ _ ⟩
421
(⟦ p ⟧H (x ∷ ρ) * x + ⟦ c′ ⟧N ρ) * ⟦ c ⟧N ρ ∎
422
423
*H-homo : ∀ {n} (p₁ p₂ : HNF (suc n)) →
424
∀ ρ → ⟦ p₁ *H p₂ ⟧H ρ ≈ ⟦ p₁ ⟧H ρ * ⟦ p₂ ⟧H ρ
425
*H-homo ∅ p₂ ρ = sym $ proj₁ zero* _
426
*H-homo (p₁ *x+ c₁) ∅ ρ = sym $ proj₂ zero* _
427
*H-homo (p₁ *x+ c₁) (p₂ *x+ c₂) (x ∷ ρ) = begin
428
⟦ ((p₁ *H p₂) *x+H ((p₁ *HN c₂) +H (c₁ *NH p₂))) *x+HN
429
(c₁ *N c₂) ⟧H (x ∷ ρ) ≈⟨ *x+HN≈*x+ ((p₁ *H p₂) *x+H ((p₁ *HN c₂) +H (c₁ *NH p₂)))
430
(c₁ *N c₂) (x ∷ ρ) ⟩
431
⟦ (p₁ *H p₂) *x+H
432
((p₁ *HN c₂) +H (c₁ *NH p₂)) ⟧H (x ∷ ρ) * x +
433
⟦ c₁ *N c₂ ⟧N ρ ≈⟨ (*x+H-homo (p₁ *H p₂) ((p₁ *HN c₂) +H (c₁ *NH p₂)) x ρ
434
⟨ *-cong ⟩
435
refl)
436
⟨ +-cong ⟩
437
*N-homo c₁ c₂ ρ ⟩
438
(⟦ p₁ *H p₂ ⟧H (x ∷ ρ) * x +
439
⟦ (p₁ *HN c₂) +H (c₁ *NH p₂) ⟧H (x ∷ ρ)) * x +
440
⟦ c₁ ⟧N ρ * ⟦ c₂ ⟧N ρ ≈⟨ (((*H-homo p₁ p₂ (x ∷ ρ) ⟨ *-cong ⟩ refl)
441
⟨ +-cong ⟩
442
(+H-homo (p₁ *HN c₂) (c₁ *NH p₂) (x ∷ ρ)))
443
⟨ *-cong ⟩
444
refl)
445
⟨ +-cong ⟩
446
refl ⟩
447
(⟦ p₁ ⟧H (x ∷ ρ) * ⟦ p₂ ⟧H (x ∷ ρ) * x +
448
(⟦ p₁ *HN c₂ ⟧H (x ∷ ρ) + ⟦ c₁ *NH p₂ ⟧H (x ∷ ρ))) * x +
449
⟦ c₁ ⟧N ρ * ⟦ c₂ ⟧N ρ ≈⟨ ((refl ⟨ +-cong ⟩ (*HN-homo p₁ c₂ x ρ ⟨ +-cong ⟩ *NH-homo c₁ p₂ x ρ))
450
⟨ *-cong ⟩
451
refl)
452
⟨ +-cong ⟩
453
refl ⟩
454
(⟦ p₁ ⟧H (x ∷ ρ) * ⟦ p₂ ⟧H (x ∷ ρ) * x +
455
(⟦ p₁ ⟧H (x ∷ ρ) * ⟦ c₂ ⟧N ρ + ⟦ c₁ ⟧N ρ * ⟦ p₂ ⟧H (x ∷ ρ))) * x +
456
(⟦ c₁ ⟧N ρ * ⟦ c₂ ⟧N ρ) ≈⟨ lemma₄ _ _ _ _ _ ⟩
457
458
(⟦ p₁ ⟧H (x ∷ ρ) * x + ⟦ c₁ ⟧N ρ) *
459
(⟦ p₂ ⟧H (x ∷ ρ) * x + ⟦ c₂ ⟧N ρ) ∎
460
461
*N-homo : ∀ {n} (p₁ p₂ : Normal n) →
462
∀ ρ → ⟦ p₁ *N p₂ ⟧N ρ ≈ ⟦ p₁ ⟧N ρ * ⟦ p₂ ⟧N ρ
463
*N-homo (con c₁) (con c₂) _ = *-homo _ _
464
*N-homo (poly p₁) (poly p₂) ρ = *H-homo p₁ p₂ ρ
465
466
^N-homo : ∀ {n} (p : Normal n) (k : ℕ) →
467
∀ ρ → ⟦ p ^N k ⟧N ρ ≈ ⟦ p ⟧N ρ ^ k
468
^N-homo p zero ρ = 1N-homo ρ
469
^N-homo p (suc k) ρ = begin
470
⟦ p *N (p ^N k) ⟧N ρ ≈⟨ *N-homo p (p ^N k) ρ ⟩
471
⟦ p ⟧N ρ * ⟦ p ^N k ⟧N ρ ≈⟨ refl ⟨ *-cong ⟩ ^N-homo p k ρ ⟩
472
⟦ p ⟧N ρ * (⟦ p ⟧N ρ ^ k) ∎
473
474
mutual
475
476
-H‿-homo : ∀ {n} (p : HNF (suc n)) →
477
∀ ρ → ⟦ -H p ⟧H ρ ≈ - ⟦ p ⟧H ρ
478
-H‿-homo p (x ∷ ρ) = begin
479
⟦ (-N 1N) *NH p ⟧H (x ∷ ρ) ≈⟨ *NH-homo (-N 1N) p x ρ ⟩
480
⟦ -N 1N ⟧N ρ * ⟦ p ⟧H (x ∷ ρ) ≈⟨ trans (-N‿-homo 1N ρ) (-‿cong (1N-homo ρ)) ⟨ *-cong ⟩ refl ⟩
481
- 1# * ⟦ p ⟧H (x ∷ ρ) ≈⟨ lemma₇ _ ⟩
482
- ⟦ p ⟧H (x ∷ ρ) ∎
483
484
-N‿-homo : ∀ {n} (p : Normal n) →
485
∀ ρ → ⟦ -N p ⟧N ρ ≈ - ⟦ p ⟧N ρ
486
-N‿-homo (con c) _ = -‿homo _
487
-N‿-homo (poly p) ρ = -H‿-homo p ρ
194
488
195
489
------------------------------------------------------------------------
196
490
-- Correctness
197
491
198
private
199
sem-cong : ∀ op → sem op Preserves₂ _≈_ ⟶ _≈_ ⟶ _≈_
200
sem-cong [+] = +-cong
201
sem-cong [*] = *-cong
202
203
raise-sem : ∀ {n x} (p : Polynomial n) ρ →
204
⟦ p :↑ 1 ⟧ (x ∷ ρ) ≈ ⟦ p ⟧ ρ
205
raise-sem (op o p₁ p₂) ρ = raise-sem p₁ ρ ⟨ sem-cong o ⟩
206
raise-sem p₂ ρ
207
raise-sem (con c) ρ = refl
208
raise-sem (var x) ρ = refl
209
raise-sem (p :^ n) ρ = raise-sem p ρ ⟨ ^-cong ⟩
210
PropEq.refl {x = n}
211
raise-sem (:- p) ρ = -‿cong (raise-sem p ρ)
212
213
nf-sound : ∀ {n p} (nf : Normal n p) ρ →
214
⟦ nf ⟧-Normal ρ ≈ ⟦ p ⟧ ρ
215
nf-sound (nf ∶ eq) ρ = nf-sound nf ρ ⟨ trans ⟩ eq
216
nf-sound (con c) ρ = refl
217
nf-sound (_↑ {p' = p'} nf) (x ∷ ρ) =
218
nf-sound nf ρ ⟨ trans ⟩ sym (raise-sem p' ρ)
219
nf-sound (_*x+_ {c' = c'} nf₁ nf₂) (x ∷ ρ) =
220
(nf-sound nf₁ (x ∷ ρ) ⟨ *-cong ⟩ refl)
221
⟨ +-cong ⟩
222
(nf-sound nf₂ ρ ⟨ trans ⟩ sym (raise-sem c' ρ))
223
492
correct-con : ∀ {n} (c : C.Carrier) (ρ : Vec Carrier n) →
493
⟦ normalise-con c ⟧N ρ ≈ ⟦ c ⟧′
494
correct-con c [] = refl
495
correct-con c (x ∷ ρ) = begin
496
⟦ ∅ *x+HN normalise-con c ⟧H (x ∷ ρ) ≈⟨ ∅*x+HN-homo (normalise-con c) x ρ ⟩
497
⟦ normalise-con c ⟧N ρ ≈⟨ correct-con c ρ ⟩
498
⟦ c ⟧′ ∎
499
500
correct-var : ∀ {n} (i : Fin n) →
501
∀ ρ → ⟦ normalise-var i ⟧N ρ ≈ lookup i ρ
502
correct-var () []
503
correct-var (suc i) (x ∷ ρ) = begin
504
⟦ ∅ *x+HN normalise-var i ⟧H (x ∷ ρ) ≈⟨ ∅*x+HN-homo (normalise-var i) x ρ ⟩
505
⟦ normalise-var i ⟧N ρ ≈⟨ correct-var i ρ ⟩
506
lookup i ρ ∎
507
correct-var zero (x ∷ ρ) = begin
508
(0# * x + ⟦ 1N ⟧N ρ) * x + ⟦ 0N ⟧N ρ ≈⟨ ((refl ⟨ +-cong ⟩ 1N-homo ρ) ⟨ *-cong ⟩ refl) ⟨ +-cong ⟩ 0N-homo ρ ⟩
509
(0# * x + 1#) * x + 0# ≈⟨ lemma₅ _ ⟩
510
x ∎
511
512
correct : ∀ {n} (p : Polynomial n) → ∀ ρ → ⟦ p ⟧↓ ρ ≈ ⟦ p ⟧ ρ
513
correct (op [+] p₁ p₂) ρ = begin
514
⟦ normalise p₁ +N normalise p₂ ⟧N ρ ≈⟨ +N-homo (normalise p₁) (normalise p₂) ρ ⟩
515
⟦ p₁ ⟧↓ ρ + ⟦ p₂ ⟧↓ ρ ≈⟨ correct p₁ ρ ⟨ +-cong ⟩ correct p₂ ρ ⟩
516
⟦ p₁ ⟧ ρ + ⟦ p₂ ⟧ ρ ∎
517
correct (op [*] p₁ p₂) ρ = begin
518
⟦ normalise p₁ *N normalise p₂ ⟧N ρ ≈⟨ *N-homo (normalise p₁) (normalise p₂) ρ ⟩
519
⟦ p₁ ⟧↓ ρ * ⟦ p₂ ⟧↓ ρ ≈⟨ correct p₁ ρ ⟨ *-cong ⟩ correct p₂ ρ ⟩
520
⟦ p₁ ⟧ ρ * ⟦ p₂ ⟧ ρ ∎
521
correct (con c) ρ = correct-con c ρ
522
correct (var i) ρ = correct-var i ρ
523
correct (p :^ k) ρ = begin
524
⟦ normalise p ^N k ⟧N ρ ≈⟨ ^N-homo (normalise p) k ρ ⟩
525
⟦ p ⟧↓ ρ ^ k ≈⟨ correct p ρ ⟨ ^-cong ⟩ PropEq.refl {x = k} ⟩
526
⟦ p ⟧ ρ ^ k ∎
527
correct (:- p) ρ = begin
528
⟦ -N normalise p ⟧N ρ ≈⟨ -N‿-homo (normalise p) ρ ⟩
529
- ⟦ p ⟧↓ ρ ≈⟨ -‿cong (correct p ρ) ⟩
530
- ⟦ p ⟧ ρ ∎
224
531
225
532
------------------------------------------------------------------------
226
533
-- "Tactics"
227
534
228
open Reflection setoid var ⟦_⟧ ⟦_⟧↓ (nf-sound ∘ normalise)
229
public using (prove; solve) renaming (_⊜_ to _:=_)
535
open Reflection setoid var ⟦_⟧ ⟦_⟧↓ correct public
536
using (prove; solve) renaming (_⊜_ to _:=_)
230
537
231
538
-- For examples of how solve and _:=_ can be used to
232
539
-- semi-automatically prove ring equalities, see, for instance,
Loggerhead is a web-based interface for Breezy
Version: 2.0.1