I want to define “integer type”. But encounter obstacles
Although the types of positive integers, negative integers and zero are not exactly the same,
However, positive integers, negative integers and zero are all integers,
But Coq does not seem to allow containment relationships between types.
How to define “integer”?
Moreover, you can’t write any instance of pos or neg, because both inductive definitions lack a base case. A positive number must be “either one, or some positive number plus one”; Similarly, a negative number must be “either negative one, or some negative number minus one”.
You can define integers as “zero, positive, or negative”: