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 to .
_β-_ : Nat β Nat β Int x β- zero = pos x zero β- suc y = negsuc y suc x β- suc y = x β- y
We can decide equality of two Int'
s by comparing
their underlying naturals when the constructors match (i.e.Β pos/pos or negsuc/negsuc):
Discrete-Int : Discrete Int Discrete-Int (pos x) (pos y) with Discrete-Nat x y ... | yes p = yes (ap pos p) ... | no Β¬p = no Ξ» path β Β¬p (ap (Ξ» { (pos x) β x ; (negsuc _) β zero }) path) Discrete-Int (negsuc x) (negsuc y) with Discrete-Nat x y ... | yes p = yes (ap negsuc p) ... | no Β¬p = no Ξ» path β Β¬p (ap (Ξ» { (negsuc x) β x ; (pos _) β zero }) path)
And in case the constructors are mismatched, there can be no path between them:
Discrete-Int (pos x) (negsuc y) = no Ξ» path β subst (Ξ» { (pos x) β β€ ; (negsuc _) β β₯ }) path tt Discrete-Int (negsuc x) (pos y) = no Ξ» path β subst (Ξ» { (pos x) β β₯ ; (negsuc _) β β€ }) path tt
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)