10
10
module Algebra.Operations {s₁ s₂} (S : Semiring s₁ s₂) where
12
open Semiring S hiding (zero)
13
open import Data.Nat using (zero; suc; ℕ)
12
open Semiring S renaming (zero to *-zero)
14
using (zero; suc; ℕ) renaming (_+_ to _ℕ+_; _*_ to _ℕ*_)
15
open import Data.Product using (module Σ)
14
16
open import Function
15
17
open import Relation.Binary
16
18
open import Relation.Binary.PropositionalEquality as PropEq using (_≡_)
39
49
------------------------------------------------------------------------
52
-- Unfolding lemma for _×′_.
54
1+×′ : ∀ n x → suc n ×′ x ≈ x + n ×′ x
56
x ≈⟨ sym $ Σ.proj₂ +-identity x ⟩
58
1+×′ (suc n) x = begin
62
-- _×_ and _×′_ are extensionally equal (up to the setoid
65
×≈×′ : ∀ n x → n × x ≈ n ×′ x
67
×≈×′ (suc n) x = begin
68
x + n × x ≈⟨ +-cong refl (×≈×′ n x) ⟩
69
x + n ×′ x ≈⟨ sym $ 1+×′ n x ⟩
72
-- _×_ is homomorphic with respect to _ℕ+_/_+_.
74
×-homo-+ : ∀ c m n → (m ℕ+ n) × c ≈ m × c + n × c
75
×-homo-+ c 0 n = begin
76
n × c ≈⟨ sym $ Σ.proj₁ +-identity (n × c) ⟩
78
×-homo-+ c (suc m) n = begin
79
c + (m ℕ+ n) × c ≈⟨ +-cong refl (×-homo-+ c m n) ⟩
80
c + (m × c + n × c) ≈⟨ sym $ +-assoc c (m × c) (n × c) ⟩
83
-- _×′_ is homomorphic with respect to _ℕ+_/_+_.
85
×′-homo-+ : ∀ c m n → (m ℕ+ n) ×′ c ≈ m ×′ c + n ×′ c
86
×′-homo-+ c m n = begin
87
(m ℕ+ n) ×′ c ≈⟨ sym $ ×≈×′ (m ℕ+ n) c ⟩
88
(m ℕ+ n) × c ≈⟨ ×-homo-+ c m n ⟩
89
m × c + n × c ≈⟨ +-cong (×≈×′ m c) (×≈×′ n c) ⟩
92
-- _× 1# is homomorphic with respect to _ℕ*_/_*_.
94
×1-homo-* : ∀ m n → (m ℕ* n) × 1# ≈ (m × 1#) * (n × 1#)
96
0# ≈⟨ sym $ Σ.proj₁ *-zero (n × 1#) ⟩
98
×1-homo-* (suc m) n = begin
99
(n ℕ+ m ℕ* n) × 1# ≈⟨ ×-homo-+ 1# n (m ℕ* n) ⟩
100
n × 1# + (m ℕ* n) × 1# ≈⟨ +-cong refl (×1-homo-* m n) ⟩
101
n × 1# + (m × 1#) * (n × 1#) ≈⟨ sym $ +-cong (Σ.proj₁ *-identity (n × 1#)) refl ⟩
102
1# * (n × 1#) + (m × 1#) * (n × 1#) ≈⟨ sym $ Σ.proj₂ distrib (n × 1#) 1# (m × 1#) ⟩
103
(1# + m × 1#) * (n × 1#) ∎
105
-- _×′ 1# is homomorphic with respect to _ℕ*_/_*_.
107
×′1-homo-* : ∀ m n → (m ℕ* n) ×′ 1# ≈ (m ×′ 1#) * (n ×′ 1#)
108
×′1-homo-* m n = begin
109
(m ℕ* n) ×′ 1# ≈⟨ sym $ ×≈×′ (m ℕ* n) 1# ⟩
110
(m ℕ* n) × 1# ≈⟨ ×1-homo-* m n ⟩
111
(m × 1#) * (n × 1#) ≈⟨ *-cong (×≈×′ m 1#) (×≈×′ n 1#) ⟩
112
(m ×′ 1#) * (n ×′ 1#) ∎
114
-- _×_ preserves equality.
42
116
×-cong : _×_ Preserves₂ _≡_ ⟶ _≈_ ⟶ _≈_
43
×-cong {n} {n'} {x} {x'} n≡n' x≈x' = begin
44
n × x ≈⟨ reflexive $ PropEq.cong (λ n → n × x) n≡n' ⟩
45
n' × x ≈⟨ ×-congʳ n' x≈x' ⟩
117
×-cong {n} {n′} {x} {x′} n≡n′ x≈x′ = begin
118
n × x ≈⟨ reflexive $ PropEq.cong (λ n → n × x) n≡n′ ⟩
119
n′ × x ≈⟨ ×-congʳ n′ x≈x′ ⟩
48
122
×-congʳ : ∀ n → (_×_ n) Preserves _≈_ ⟶ _≈_
49
×-congʳ zero x≈x' = refl
50
×-congʳ (suc n) x≈x' = x≈x' ⟨ +-cong ⟩ ×-congʳ n x≈x'
123
×-congʳ 0 x≈x′ = refl
124
×-congʳ (suc n) x≈x′ = x≈x′ ⟨ +-cong ⟩ ×-congʳ n x≈x′
126
-- _×′_ preserves equality.
128
×′-cong : _×′_ Preserves₂ _≡_ ⟶ _≈_ ⟶ _≈_
129
×′-cong {n} {n′} {x} {x′} n≡n′ x≈x′ = begin
130
n ×′ x ≈⟨ sym $ ×≈×′ n x ⟩
131
n × x ≈⟨ ×-cong n≡n′ x≈x′ ⟩
132
n′ × x′ ≈⟨ ×≈×′ n′ x′ ⟩
135
-- _^_ preserves equality.
52
137
^-cong : _^_ Preserves₂ _≈_ ⟶ _≡_ ⟶ _≈_
53
138
^-cong {x} {x'} {n} {n'} x≈x' n≡n' = begin
added
removed
src/Algebra/Operations.agda
