------------------------------------------------------------------------
-- The Agda standard library
--
-- Some examples showing where the natural numbers and some related
-- operations and properties are defined, and how they can be used
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible #-}

module README.Data.Nat where

-- The natural numbers and various arithmetic operations are defined
-- in Data.Nat.

open import Data.Nat using (ℕ; _+_; _*_)

-- _*_ has precedence 7 over precedence 6 of _+_
-- precedence of both defined in module Agda.Builtin.Nat
ex₁ : ℕ
ex₁ =  +  * 

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

open import Relation.Binary.PropositionalEquality using (_≡_; refl)

ex₂ :  +  ≡  * 
ex₂ = refl

-- Data.Nat.Properties contains a number of properties about natural
-- numbers.

open import Data.Nat.Properties using (*-comm; +-identityʳ)

ex₃ : ∀ m n → m * n ≡ n * m
ex₃ m n = *-comm m n

-- The module ≡-Reasoning in Relation.Binary.PropositionalEquality
-- provides some combinators for equational reasoning.

open Relation.Binary.PropositionalEquality using (cong; module ≡-Reasoning)

ex₄ : ∀ m n → m * (n + ) ≡ n * m
ex₄ m n = begin
  m * (n + )  ≡⟨ cong (_*_ m) (+-identityʳ n) ⟩
  m * n        ≡⟨ *-comm m n ⟩
  n * m        ∎
  where open ≡-Reasoning

-- The module SemiringSolver in Data.Nat.Solver contains a solver
-- for natural number equalities involving variables, constants, _+_
-- and _*_.

open import Data.Nat.Solver using (module +-*-Solver)
open +-*-Solver using (solve; _:*_; _:+_; con; _:=_)

ex₅ : ∀ m n → m * (n + ) ≡ n * m
ex₅ = solve  (λ m n → m :* (n :+ con )  :=  n :* m) refl