The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Wed, 09 May 2012 13:22:36 +0200,
Robbert Krebbers 
<mailinglists AT robbertkrebbers.nl>
 a écrit :

> Hello Coq Club,
> 
> I am wondering why Coq does not allow the following inductive type.
> 
>    Inductive val : Type :=
>      | vnat : nat -> val
>      | varray (l : list val) : length l > 0 -> val.
> 
> It gives the following error
> 
>    Error: Non strictly positive occurrence of "val" in
>     "forall l : list val, length l > 0 -> val".
> 
> However, I do not see why the positivity condition does not hold.
> 
> Am I missing something, is the error message incorrect, or is this a
> bug?
> 
> Robbert
> 

Do you not see why the strict positivity condition does not hold, or do
you not see why the strict positivity condition is not fit to allow what
you wrote and should be refined to allow it ?

For the first point is it rather clear[1]:

Definition (strict positivity according to reference manual)

The constant X occurs strictly positively in T in the following cases:

-X does not occur in T
-T converts to (X t1 …  tn) and X does not occur in any of ti
-T converts to ∀ x:U,V and X does not occur in type U but occurs
strictly positively in type V
-T converts to (I a1 …  am   t1 …  tp)
where I is the name of an inductive declaration of the form
Ind(Γ)[m](I:A:=c1:∀ p1:P1,… ∀ pm:Pm,C1;…;cn:∀ p1:P1,… ∀ pm:Pm,Cn ) (in
particular, it is not mutually defined and it has m parameters) and X
does not occur in any of the ti, and the (instantiated) types of
constructor Ci{pj/aj}j=1… m of I satisfy the nested positivity
condition for X

Now what are the occurences of [val] in the constructor [varray]?
∀ (l : list val(*1*)) (_ : lt (@length val(*2*) l) 0), val(*3*)

the first occurence is strictly positive,
but the second occurence is not:

T=@leq
 (S O) (@length val l)
                      ^^^
- val occurs
- T does not convert to val
- T does not convert to ∀ (x:U), V
- T converts to 
(I:=@leq)
 (a1:=S O) 
(t1:=@length
 val l)
  where @leq is an inductive declaration of the form
  Ind(Γ)[1](@leq : ∀ (_ : nat) (_ : nat), Prop :=
            le_n : ∀ (m : nat), @leq m m;
            le_S : ∀ (m : nat) (n : nat) (_ : @leq m n), @leq m (S n))
  but here, val occurs in t1.

so, you cannot say that the 2nd occurence of [val] is strictly positive.

For the second point, things are less obvious, and I know there are
cases where it could be allowed without breaking consistency.

Of course, you can use:
Inductive val : Type :=
  | vnat : nat → val
  | varray (head : val) (tail : list val) : val
.

Inductive val2 : Type :=
  | vnat2 : nat → val2
  | varray2 (l : list val) : length l > 0 → val2
.

Definition cast1 (v : val) : val2.
  refine (match v with
            | vnat n => vnat2 n
            | varray hd tl => varray2 (cons hd tl) _
          end).
  Proof.
    abstract (unfold gt, lt; simpl; induction (length tl); auto).
  Defined.

Definition cast2 (v : val2) : val :=
  match v with
    | vnat2 n => vnat n
    | varray2 l H => varray (hd (vnat O) l) (tail l)
  end.

Lemma self_reduction : ∀ v, cast2 (cast1 v) = v.
Proof.
  intros []; split.
Qed.

Coercion cast1 : val >-> val2.
Coercion cast2 : val2 >-> val.

But do not expect it to work conveniently.
(Beside that, it is often a bad idea to use "list a" inside the
inductive definition of "a", as the induction principles will mainly be
useless, and you will have to provide your own, and using arithmetic
like in "length l > 0" may also be cumbersome while things like
"match l with [] -> False | _ -> True end" or defining "Inductive
non_empty (A : Type) : list A -> Prop := NE : ∀ hd tl, non_empty A
(hd::tl)" are often more direct and easy to use.)