Why Coq does not allow the containment relationship between types

Using Coq
1

English is not my native language

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”?

Coq 8.11.2

2

Thank you for reposting this question in your preferred language! I’ve added my thoughts there:

I’m so happy that this multilingual forum is helping people to learn Coq more efficiently.

4

image

5

In the code you’ve shown:

  • O has type zero.
  • K takes a neg as argument to construct a neg.
  • O is not a neg.
  • Therefore, K O is not a valid expression.
  • 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”:

Inductive pos :=
| One
| S (n : pos).

Variant Z' :=
| Z0'              (* zero         *)
| Zpos' (n : pos)  (* positive [n] *)
| Zneg' (n : pos). (* negative [n] *)

If you prefer asking (and responded) in Chinese, please feel free to post under the other thread you created: