Intro to induction in Agda

ind-def.agda

module ind-def where

----------------------------------------------------------------------
-- unicode symbols on this file
----------------------------------------------------------------------
-- ℕ  U+2115  DOUBLE-STRUCK CAPITAL N (\bN)
-- →  U+2192  RIGHTWARDS ARROW (\to, \r, \->)
-- ∸  U+2238  DOT MINUS (\.-)
-- ≡  U+2261  IDENTICAL TO (\==)
-- ⟨  U+27E8  MATHEMATICAL LEFT ANGLE BRACKET (\<)
-- ⟩  U+27E9  MATHEMATICAL RIGHT ANGLE BRACKET (\>)
-- ∎  U+220E  END OF PROOF (\qed)

----------------------------------------------------------------------
-- types
----------------------------------------------------------------------

-- type = domain of discourse = sort
-- type signature = type annotation expressed by _:_
-- given a function denoted by its name
-- defines its inputs and outputs

----------------------------------------------------------------------
-- inductive process
----------------------------------------------------------------------
-- HOW start with a finite set
-- HOW apply rules that convert one finite set into another finite set
-- GOAL build up a potentially infinite set

----------------------------------------------------------------------
-- inductive definition
----------------------------------------------------------------------

-- keyword DATA tells this is an inductive definition
-- inductive definition = new datatype with constructors
-- ℕ is the NAME chosen to denote the datatype
-- ℕ : Set is the datatype declaration
-- keyword WHERE separates datatype declaration from constructors declaration
data ℕ : Set where

----------------------------------------------------------------------
-- inference rules = type formation rules = constructors
-- declare each CONSTRUCTOR in a separate line
-- indentation to assign constructors to datatype ℕ
----------------------------------------------------------------------

-- inference rule #1 BASE CASE
-- introduces a member without knowing other members
-- no judgements in hypotheses
-- 1 judgement in conclusions asserts zero is natural
-- zero is the name chosen for the constructor
  zero : ℕ

  -- inference rule #2 INDUCTIVE CASE
  -- introduces other members when we know some
  -- 1 judgement in hypotheses assumes m is natural
  -- 1 judgement in conclusions asserts suc m is natural
  suc  : ℕ → ℕ

  ----------------------------------------------------------------------
  -- pragmas
  ----------------------------------------------------------------------

-- declare that out type ℕ
-- corresponds to the built in type NATURAL
-- allows to eval normal forms of expressions
-- that include numbers, not combinations of constructors
{-# BUILTIN NATURAL ℕ #-}
----------------------------------------------------------------------
-- imports from Agda standard library
----------------------------------------------------------------------

-- import keyword brings into scope PropositionalEquality module
-- standard library module that defines equality
-- as keyword denotes it with the name Eq
import Relation.Binary.PropositionalEquality as Eq

-- open Eq module
-- using clause adds the names specified into the current scope
-- _≡_ equality operator
-- refl sole constructor of _≡_
open Eq using (_≡_ ; refl)

-- open Eq.≡-Reasoning submodule
-- begin_ prefix operator
-- _≡⟨⟩_ infix operator
-- _∎ postfix operator
open Eq.≡-Reasoning using (begin_ ; _≡⟨⟩_ ; _∎)

----------------------------------------------------------------------
-- operation _+_ ADDITION
----------------------------------------------------------------------

-- type signature or annotation for operator _+_
-- infix notation n + m is a shorthand for _+_ n m
_+_ : ℕ → ℕ → ℕ

-- Patern matching on first operand
-- only via constructors
zero + n = n
(suc m) + n = suc (m + n)

-- EXAMPLE DERIVATIONS
-- use the dummy name _
-- _ can be reused and is good for examples
-- names other than _ must be used only once in a module
-- type signature says that _ is of type 2 + 3 ≡ 5
_ : 2 + 3 ≡ 5
_ =      -- binding gives a term of the type given
  begin  -- start chain of equations
    2 + 3
  ≡⟨⟩    -- because of pragma is shorthand for
    (suc (suc zero)) + (suc (suc (suc zero)))
  ≡⟨⟩    -- inductive case _+_
    suc ((suc zero) + (suc (suc (suc zero))))
  ≡⟨⟩    -- inductive case _+_
    suc (suc (zero + (suc (suc (suc zero)))))
  ≡⟨⟩    -- base case _+_
    suc (suc (suc (suc (suc zero))))
  ≡⟨⟩    -- because of pragma is longhand for
    5
  ∎      -- qed or tombstone

-- agda knows how to compute with constructors
_ : 2 + 3 ≡ 5
_ = refl

----------------------------------------------------------------------
-- operation _*_ MULTIPLICATION
----------------------------------------------------------------------

_*_ : ℕ → ℕ → ℕ
zero    * n  =  zero
(suc m) * n  =  n + (m * n)

-- EXAMPLE 2 * 3
_ =
  begin 2 * 3
  ≡⟨⟩ (suc (suc zero)) * (suc (suc (suc zero)))
  ≡⟨⟩ (suc (suc (suc zero))) + ((suc zero) * (suc (suc (suc zero))))
  ≡⟨⟩ (suc (suc (suc zero))) + ((suc (suc (suc zero))) + (zero * (suc (suc (suc zero)))))
  ≡⟨⟩ (suc (suc (suc zero))) + ((suc (suc (suc zero))) + zero)
  ≡⟨⟩ (suc (suc (suc zero))) + (suc (suc (suc zero)))
  ≡⟨⟩ suc (suc ((suc zero)) + (suc (suc (suc zero))))
  ≡⟨⟩ suc (suc (suc zero + (suc (suc (suc zero)))))
  ≡⟨⟩ suc (suc (suc (suc (suc (suc zero)))))
  ≡⟨⟩ 6
  ∎

_ : 2 * 3 ≡ 6
_ = refl

----------------------------------------------------------------------
-- operation _^_ EXPONENTIATION
----------------------------------------------------------------------

-- pattern matching on second argument
_^_ : ℕ → ℕ → ℕ
m ^ zero = suc zero
m ^ (suc n) = (m ^ n) * m

-- EXAMPLE 3 ^ 4
_ = begin 3 ^ 4
  ≡⟨⟩ (3 ^ 3) * 3
  ≡⟨⟩ (3 ^ 2) * (3 * 3)
  ≡⟨⟩ (3 ^ 1) * (3 * 9)
  ≡⟨⟩ 3 * 27
  ≡⟨⟩ 81
  ∎

----------------------------------------------------------------------
-- operation _∸_ MONUS substraction on naturals
----------------------------------------------------------------------

_∸_ : ℕ → ℕ → ℕ
m     ∸ zero   =  m
zero  ∸ suc n  =  zero
suc m ∸ suc n  =  m ∸ n

_ : 3 ∸ 2 ≡ 1
_ = refl

_ = begin 4 ∸ 3 ≡⟨⟩ 3 ∸ 2 ≡⟨⟩ 2 ∸ 1 ≡⟨⟩ 1 ∎

----------------------------------------------------------------------
-- syntax
----------------------------------------------------------------------

-- Application binds more tightly than
-- (has precedence over) any operator
-- higher levels have higher precedence
infixl 6  _+_  _∸_
infixl 7  _*_

----------------------------------------------------------------------
-- representation of naturals in a binary system
----------------------------------------------------------------------

data Bin : Set where
  nil : Bin
  x0_ : Bin → Bin
  x1_ : Bin → Bin

inc : Bin → Bin
inc nil = x1 nil
inc (x0 n) = x1 n
inc (x1 n) = x0 inc n

to   : ℕ → Bin
to zero = x0 nil
to (suc n) = inc (to n)

-- compute normal form for
-- to 92

from : Bin → ℕ
from nil = zero
from (x0 n) = zero + ((from n) * suc(suc zero))
from (x1 n) = suc zero + ((from n) * suc(suc zero))

-- compute normal form for
-- from (x0 x0 x1 x1 x1 x0 x1 nil)

----------------------------------------------------------------------
-- representation of naturals in a ternary system
----------------------------------------------------------------------

data Ter : Set where
  nil : Ter
  x0_ : Ter → Ter
  x1_ : Ter → Ter
  x2_ : Ter → Ter

inc2 : Ter → Ter
inc2 nil = x1 nil
inc2 (x0 n) = x1 n
inc2 (x1 n) = x2 n
inc2 (x2 n) = x0 inc2 n

to2  : ℕ → Ter
to2 zero = x0 nil
to2 (suc n) = inc2 (to2 n)

----------------------------------------------------------------------
-- representation of naturals in a decimal system
----------------------------------------------------------------------

data Dec : Set where
  nil : Dec
  x0_ : Dec → Dec
  x1_ : Dec → Dec
  x2_ : Dec → Dec
  x3_ : Dec → Dec
  x4_ : Dec → Dec
  x5_ : Dec → Dec
  x6_ : Dec → Dec
  x7_ : Dec → Dec
  x8_ : Dec → Dec
  x9_ : Dec → Dec

incDec : Dec → Dec
incDec nil = x1 nil
incDec (x0 n) = x1 n
incDec (x1 n) = x2 n
incDec (x2 n) = x3 n
incDec (x3 n) = x4 n
incDec (x4 n) = x5 n
incDec (x5 n) = x6 n
incDec (x6 n) = x7 n
incDec (x7 n) = x8 n
incDec (x8 n) = x9 n
incDec (x9 n) = x0 incDec n

toDec  : ℕ → Dec
toDec zero = x0 nil
toDec (suc n) = incDec (toDec n)