Why is my definition not allowed because of strict positivity?

Question

Unfortunately, there’s nothing super deep about this example. As you noted Agda accepts it, and what trips Coq is the lack of uniformity in the parameters. For example, it accepts this:

Inductive SwitchNSPA (A : Type) : Type :=
| switchNSPA : SwitchNSPA A -> SwitchNSPA A.

Inductive UseSwitchNSPA :=
| useSwitchNSPA : SwitchNSPA UseSwitchNSPA -> UseSwitchNSPA.

Positivity criteria like the one used by Coq are not complete, so they will reject harmless types; the problem with supporting more types is that it often makes the positivity checker more complex, and that’s already one of the most complex pieces of the kernel.

As for the concrete details of why it rejects it, well, I’m not 100% sure. Going by the rules in the manual, I think it should be accepted?

EDIT: The manual is being updated.

Specifically, using the following shorter names to simplify the following:

Inductive Inner (A : Type) : Type := inner : Inner bool -> Inner A.
Inductive Outer := outer : Inner Outer -> Outer.

Correctness rules
Positivity condition

Here,
```
X = Outer
T = forall x: Inner X, X
```
So we’re in the second case with
```
U = Inner X
V = X
```
1. V is easy, so let’s do that first:
  V = (X) falls in the first case, with no t_i, hence is positive for X
2. For U: is U = Inner X strictly positive wrt X?
  
  Here,
```
T = Inner X
```
  Hence we’re in the last case: T converts to (I a1) (no t_i) with
```
I = Inner
a1 = X
```
  and X does not occur in the t_i, since there are no t_i.
  Do the instantiated types of the constructors satisfy the nested positivity condition?
  There is only one constructor:
  1. inner : Inner bool -> Inner X.
    Does this satisfy the nested positivity condition?
    Here,
```
T = forall x: Inner bool, Inner X.
```
    So we’re in the second case with
```
U = Inner bool
V = Inner X
```
    1. X does not occur in U, so X is strictly positive in U.
    2. Does V satisfy the nested positivity condition for X?
      Here,
```
T = Inner X
```
      Hence we’re in the first case: T converts to (I b1) (no u_i) with
```
I = Inner
b1 = X
```
      There are no u_i, so V satisfies the nested positivity condition.

I have opened a bug report. The manual is being fixed.

Two more small things:

I can’t resist pointing that your type is empty:

Theorem Inner_empty: forall A, Inner A -> False.
Proof. induction 1; assumption. Qed.

You wrote:

if Coq allows non-strictly positivity data type definitions, I could construct non-terminating functions without using fix (which is pretty bad).

That’s almost correct, but not exactly: if Coq didn’t enforce strict positivity, you could construct non-terminating functions period, which is bad. It doesn’t matter whether they use fix or not: having non-termination in the logic basically makes it unsound (and hence Coq prevents you from writing fixpoints that do not terminate by lazy reduction).

Leave a Comment Cancel reply