← Back to branch summary

~ubuntu-branches/ubuntu/precise/agda-stdlib/precise

« back to all changes in this revision

Viewing changes to src/Algebra/Operations.agda

  • Committer: Bazaar Package Importer
  • Author(s): Iain Lane
  • Date: 2010-01-08 23:35:09 UTC
  • Revision ID: james.westby@ubuntu.com-20100108233509-l6ejt9xji64xysfb
Import upstream version 0.3

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Algebra/Operations.agda
 
1
------------------------------------------------------------------------
 
2
-- Some defined operations (multiplication by natural number and
 
3
-- exponentiation)
 
4
------------------------------------------------------------------------
 
5
 
 
6
open import Algebra
 
7
 
 
8
module Algebra.Operations (s : Semiring) where
 
9
 
 
10
open Semiring s hiding (zero)
 
11
open import Data.Nat using (zero; suc; ℕ)
 
12
open import Data.Function
 
13
open import Relation.Binary
 
14
open import Relation.Binary.PropositionalEquality as PropEq using (_≡_)
 
15
import Relation.Binary.EqReasoning as EqR
 
16
open EqR setoid
 
17
 
 
18
------------------------------------------------------------------------
 
19
-- Operations
 
20
 
 
21
-- Multiplication by natural number.
 
22
 
 
23
infixr 7 _×_
 
24
 
 
25
_×_ : ℕ → Carrier → Carrier
 
26
zero  × x = 0#
 
27
suc n × x = x + n × x
 
28
 
 
29
-- Exponentiation.
 
30
 
 
31
infixr 8 _^_
 
32
 
 
33
_^_ : Carrier → ℕ → Carrier
 
34
x ^ zero  = 1#
 
35
x ^ suc n = x * x ^ n
 
36
 
 
37
------------------------------------------------------------------------
 
38
-- Some properties
 
39
 
 
40
×-cong : _×_ Preserves₂ _≡_ ⟶ _≈_ ⟶ _≈_
 
41
×-cong {n} {n'} {x} {x'} n≡n' x≈x' = begin
 
42
  n  × x   ≈⟨ reflexive $ PropEq.cong (λ n → n × x) n≡n' ⟩
 
43
  n' × x   ≈⟨ ×-congʳ n' x≈x' ⟩
 
44
  n' × x'  ∎
 
45
  where
 
46
  ×-congʳ : ∀ n → (_×_ n) Preserves _≈_ ⟶ _≈_
 
47
  ×-congʳ zero    x≈x' = refl
 
48
  ×-congʳ (suc n) x≈x' = x≈x' ⟨ +-cong ⟩ ×-congʳ n x≈x'
 
49
 
 
50
^-cong : _^_ Preserves₂ _≈_ ⟶ _≡_ ⟶ _≈_
 
51
^-cong {x} {x'} {n} {n'} x≈x' n≡n' = begin
 
52
  x  ^ n   ≈⟨ reflexive $ PropEq.cong (_^_ x) n≡n' ⟩
 
53
  x  ^ n'  ≈⟨ ^-congˡ n' x≈x' ⟩
 
54
  x' ^ n'  ∎
 
55
  where
 
56
  ^-congˡ : ∀ n → (λ x → x ^ n) Preserves _≈_ ⟶ _≈_
 
57
  ^-congˡ zero    x≈x' = refl
 
58
  ^-congˡ (suc n) x≈x' = x≈x' ⟨ *-cong ⟩ ^-congˡ n x≈x'