[Agda] Q: Equational Reasoning

[Nils Anders Danielsson]

On 2009-05-27 02:12, ch wrote:
> I am new to Agda and confused by all the library modules. [...]

The following example code should hopefully answer some of the questions
in this thread:

  module Examples where

  open import Data.Nat

  ex₁ : ℕ
  ex₁ = 1 + 3

  open import Relation.Binary.PropositionalEquality

  ex₂ : 3 + 5 ≡ 2 * 4
  ex₂ = refl

  open import Algebra
  import Data.Nat.Properties as Nat

  ex₃ : ∀ m n → m * n ≡ n * m
  ex₃ m n = *-comm m n
    where open CommutativeSemiring Nat.commutativeSemiring

  open ≡-Reasoning
  open import Data.Product

  ex₄ : ∀ m n → m * (n + 0) ≡ n * m
  ex₄ m n = begin
    m * (n + 0)  ≡⟨ cong (_*_ m) (proj₂ +-identity n) ⟩
    m * n        ≡⟨ *-comm m n ⟩
    n * m        ∎
    where
    open CommutativeSemiring Nat.commutativeSemiring hiding (_+_; _*_)

  open Nat.SemiringSolver

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

To find out where a given identifier is defined, load up the module in
Agda's Emacs mode and click on the identifier using the middle mouse
button.

-- 
/NAD



This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.