In Agda, is it possible to define a data type that has equations?
I want to describe integers:
data Integer : Set where
Z : Integer
Succ : Integer -> Integer
Pred : Integer -> Integer
?? what else
The above does not define integers. We need Succ (Pred x) = x and Pred (Succ x) = x. However
spReduce : (m : Integer) -> Succ (Pred m) = m
psReduce : (m : Integer) -> Pred (Succ m) = m
Cannot be added to data type. Better definition of integers by far
data Integers : Set where
Pos : Nat -> Integers
Neg : Nat -> Integers
But I'm curious if there is a way to add equations to the datatype.
source to share
It seems that you need to define a type Integers
as the type of an equivalence relation that identifies Succ (Pred m)
with m
, etc. Agda no longer supports this - there was an experimental library that tried to do this (forcing all functions on top of a categorical type to be defined with a helper function that requires proof of representative invariance), but then someone discovered that the implementation was not waterproof enough and could lead to (mainly by accessing one of their postulates, which should have been inaccessible from the outside), for details you can see this message :
We weren't sure if this hack was sound or not. Now, thanks to Dan Doel, I know it isn't.
[...]
Given these observations, it is easy to prove that the postulate above is unfounded:
I think your best bet at the moment (if you want / need to stick to a fluent equivalence representation in order to tighten it) needs to be defined Setoid
for your type.
source to share
I would think about this by specifying record
:
record Integer (A : Set) : Set where
constructor integer
field
z : A
succ : A -> A
pred : A -> A
spInv : (x : A) -> succ (pred x) == x
psInv : (x : A) -> pred (succ x) == x
This entry can be used as proof that a particular type A
is behaving like Integer
should.
source to share