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
61
62
63
64
65
66
67
68
69
70
|
------------------------------------------------------------------------
-- The Agda standard library
--
-- Some examples showing where the integers and some related
-- operations and properties are defined, and how they can be used
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible #-}
module README.Data.Integer where
-- The integers and various arithmetic operations are defined in
-- Data.Integer.
open import Data.Integer
-- The +_ function converts natural numbers into integers.
ex₁ : ℤ
ex₁ = + 2
-- The -_ function negates an integer.
ex₂ : ℤ
ex₂ = - + 4
-- Some binary operators are also defined, including addition,
-- subtraction and multiplication.
ex₃ : ℤ
ex₃ = + 1 + + 3 * - + 2 - + 4
-- Propositional equality and some related properties can be found
-- in Relation.Binary.PropositionalEquality.
open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
ex₄ : ex₃ ≡ - + 9
ex₄ = ≡.refl
-- Data.Integer.Properties contains a number of properties related to
-- integers. Algebra defines what a commutative ring is, among other
-- things.
import Data.Integer.Properties as ℤ
ex₅ : ∀ i j → i * j ≡ j * i
ex₅ i j = ℤ.*-comm i j
-- The module ≡-Reasoning in Relation.Binary.PropositionalEquality
-- provides some combinators for equational reasoning.
open ≡.≡-Reasoning
ex₆ : ∀ i j → i * (j + + 0) ≡ j * i
ex₆ i j = begin
i * (j + + 0) ≡⟨ ≡.cong (i *_) (ℤ.+-identityʳ j) ⟩
i * j ≡⟨ ℤ.*-comm i j ⟩
j * i ∎
-- The module RingSolver in Data.Integer.Solver contains a solver
-- for integer equalities involving variables, constants, _+_, _*_, -_
-- and _-_.
open import Data.Integer.Solver using (module +-*-Solver)
open +-*-Solver
ex₇ : ∀ i j → i * - j - j * i ≡ - + 2 * i * j
ex₇ = solve 2 (λ i j → i :* :- j :- j :* i := :- con (+ 2) :* i :* j)
≡.refl
|
