# Why Coq does not allow the containment relationship between types

**URL:** <https://discourse.rocq-prover.org/t/why-coq-does-not-allow-the-containment-relationship-between-types/962>\
**Category:** Using Rocq\
**Created:** [July 23, 2020, 5:15am UTC](https://discourse.rocq-prover.org/t/why-coq-does-not-allow-the-containment-relationship-between-types/962 "2020-07-23T05:15:05Z")\
**Posts on this page:** 1\
**Showing post:** 5

<div class="post-metadata">

**Author:** ![Lys](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/lys/32/48_2.png) [@Lys](https://discourse.rocq-prover.org/u/Lys)\
**Post date:** [July 23, 2020, 7:47am UTC](https://discourse.rocq-prover.org/t/why-coq-does-not-allow-the-containment-relationship-between-types/962/5 "2020-07-23T07:47:39Z")

</div>

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

```coq
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:

> [@如何定义“类型包含”？](https://discourse.rocq-prover.org/t/topic/961):
>
> 我想定义“整数类型”。但是遇到了障碍 虽然，正数、负数和零并不是同一类型， 但是，正整数、负整数和零都是整数。 但是Coq似乎不允许类型之间的包含关系。 如何定义“整数”？有这样的功能吗？

---

_[View the full topic](https://discourse.rocq-prover.org/t/why-coq-does-not-allow-the-containment-relationship-between-types/962)._