------------------------------------------------------------------------
-- 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 --without-K #-}

module README.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₁ = + 

-- The -_ function negates an integer.

ex₂ : ℤ
ex₂ = - + 

-- Some binary operators are also defined, including addition,
-- subtraction and multiplication.

ex₃ : ℤ
ex₃ = +   +  +  * - +   -  + 

-- Propositional equality and some related properties can be found
-- in Relation.Binary.PropositionalEquality.

open import Relation.Binary.PropositionalEquality as P using (_≡_)

ex₄ : ex₃ ≡ - + 
ex₄ = P.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 P.≡-Reasoning
open import Data.Product

ex₆ : ∀ i j → i * (j + + ) ≡ j * i
ex₆ i j = begin
  i * (j + + )  ≡⟨ P.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 ≡ - +  * i * j
ex₇ = solve  (λ i j → i :* :- j :- j :* i  :=  :- con (+ ) :* i :* j)
              P.refl