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
pos
itive 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
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)