Why Coq does not allow the containment relationship between types

Using Rocq
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: