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