open import 1Lab.Equiv
open import 1Lab.Path
open import 1Lab.Type

open import Data.Dec.Base
open import Data.Nat.Base

module Data.Int.Inductive where

Inductive integersπŸ”—

The inductive integers (or built-in integers) are the type generated by the two constructors pos and negsuc, as below. This type is important to have around because it is the type of integers that Agda privileges as a built-in.

data Int : Type where
  pos    : Nat β†’ Int
  negsuc : Nat β†’ Int
{-# BUILTIN INTEGER       Int    #-}
{-# BUILTIN INTEGERPOS    pos    #-}
{-# BUILTIN INTEGERNEGSUC negsuc #-}

As the names indicate, these constructors are meant to represent a positive integer, and the negation of a successor of a natural number, i.e.Β negsuc is the map taking nn to βˆ’(n+1)-(n + 1).

_β„•-_ : Nat β†’ Nat β†’ Int
x     β„•- zero  = pos x
zero  β„•- suc y = negsuc y
suc x β„•- suc y = x β„•- y

pos-injective : βˆ€ {x y} β†’ pos x ≑ pos y β†’ x ≑ y
pos-injective = ap (case_of Ξ» { (pos x) β†’ x ; (negsuc _) β†’ zero })

negsuc-injective : βˆ€ {x y} β†’ negsuc x ≑ negsuc y β†’ x ≑ y
negsuc-injective = ap (case_of Ξ» { (pos x) β†’ 0 ; (negsuc x) β†’ x })

_ = Discrete-Nat

We can decide equality of two Int's by comparing their underlying naturals when the constructors match (i.e.Β pos/pos or negsuc/negsuc):

instance
  Discrete-Int : Discrete Int
  Discrete-Int {pos x} {pos y} with x ≑? y
  ... | yes p = yes (ap pos p)
  ... | no Β¬p = no Ξ» path β†’ Β¬p (pos-injective path)

  Discrete-Int {negsuc x} {negsuc y} with x ≑? y
  ... | yes p = yes (ap negsuc p)
  ... | no Β¬p = no Ξ» path β†’ Β¬p (negsuc-injective path)

And in case the constructors are mismatched, there can be no path between them:

  Discrete-Int {pos x} {negsuc y} =
    let
      posβ‰ ns : pos x ≑ negsuc y β†’ βŠ₯
      posβ‰ ns p = subst (Ξ» { (pos x) β†’ ⊀ ; (negsuc _) β†’ βŠ₯ }) p tt
    in no pos≠ns
  Discrete-Int {negsuc x} {pos y} =
    let
      nsβ‰ pos : negsuc x ≑ pos y β†’ βŠ₯
      nsβ‰ pos p = subst (Ξ» { (pos x) β†’ βŠ₯ ; (negsuc _) β†’ ⊀ }) p tt
    in no ns≠pos

The integers are characterised as being the free type with an equivalence. This equivalence is the successor function:

suc-int : Int β†’ Int
suc-int (pos n)          = pos (suc n)
suc-int (negsuc zero)    = pos zero
suc-int (negsuc (suc n)) = negsuc n

pred-int : Int β†’ Int
pred-int (pos zero)    = negsuc zero
pred-int (pos (suc n)) = pos n
pred-int (negsuc n)    = negsuc (suc n)

suc-pred : (x : Int) β†’ suc-int (pred-int x) ≑ x
suc-pred (pos zero)    = refl
suc-pred (pos (suc x)) = refl
suc-pred (negsuc x)    = refl

pred-suc : (x : Int) β†’ pred-int (suc-int x) ≑ x
pred-suc (pos x) = refl
pred-suc (negsuc zero) = refl
pred-suc (negsuc (suc x)) = refl

suc-equiv : Int ≃ Int
suc-equiv = Iso→Equiv (suc-int , iso pred-int suc-pred pred-suc)