The Coq mailing list

[Nikhil Swamy <nswamy AT microsoft.com>]

Thanks Stefan. In this case, it does seem closely related to uniqueness of 
identity proofs.

However, forbidding indexes (and non-uniformly recursive parameters) from 
mentioning the inductive being defined seems to impose a broader class of 
restrictions that I don't know how to interpret.

For instance, in this context of basic definitions:

Inductive Eq (A:Type) (x:A) : A -> Type :=
  | Refl : Eq A x x.

Inductive Opt (A:Type) :=
  | None : Opt A
  | Some : A -> Opt A.

Inductive Sigma (A:Type) (B: A -> Type) : Type :=
  | Sig : forall (x:A), B x -> Sigma A B.

Here is something that is accepted:

Definition n (A:Type) := Sigma A (fun (v:A) => Eq A v v).

Inductive N :=
  | MkN : n N -> N.

But, here's a small variant where the inductive definition M is rejected.

Definition IsSome (A:Type) (x:Opt A) : bool :=
  match x with
  | Some _ _ => true
  | _ => false
  end.

Definition m (A:Type) := Sigma (Opt A) (fun (v:Opt A) => Eq bool (IsSome A v) 
true).

Inductive M :=
  | MkM : m M -> M.

I think the only difference that I can see is that in the case of n N​, the 
type N​ appears only as a parameter of both Sigma​ and Eq​ and so it is 
accepted.
Whereas in the second case, the type A​ appears free in the index of the 
constructed type of the Refl constructor (after instantiation with the 
parameters bool and (IsSome A v​)).

Interestingly, although Agda also rejects my first example with I1 and I2, it 
accepts an adaption of this second example.

data Bool : Set where
 true : Bool
 false : Bool
 
data Eq (A : Set) (x : A) : A -> Set where
 refl : Eq A x x

data Opt (A : Set) : Set where
 some : A -> Opt A
 none : Opt A

isSome : (A : Set) -> Opt A -> Bool
isSome A (some _) = true
isSome A none = false

data Sigma (A : Set) (B : A -> Set) : Set where
 sig : (x : A) -> B x -> Sigma A B

n : Set -> Set
n A = Sigma A (\x -> Eq A x x)

data N : Set where
 MkN : n N -> N

m : Set -> Set
m A = Sigma (Opt A) (\x -> Eq Bool (isSome A x) true)

Is there something fundamental here or is it just a quirk of the syntactic 
nested positivity condition?

Thanks for any insights!

-Nik


From: Stefan Monnier <monnier AT iro.umontreal.ca>
Sent: Tuesday, February 7, 2023 3:36 PM
To: Nikhil Swamy <nswamy AT microsoft.com>
Cc: coq-club AT inria.fr <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Nested positivity 
 
> Coq rejects the definition of I2 below saying "Non strictly positive
> occurrence of "I2" in "I1 I2 I2 -> I2".".
>
> Inductive I1 (A:Type) : Type -> Type :=
>   | MkI1 : I1 A A.
>
> Inductive I2 :=
>   | MkI2 : I1 I2 I2 -> I2.
>
> I think this is due to a violation of the Nested Positivity condition, 
> described here:
> https://coq.inria.fr/refman/language/core/inductive.html#nested-positivity
>
> However, I couldn't find a description in the manual for why nested 
> positivity is important.
>
> In particular, if one were to accept a definition in which the type being
> defined (I2 in this case) appears as an index of some other inductive type
> (e.g., I1), do things become inconsistent?

Coq's positivity requirements are stricter than mere positivity
(because of impredicativity), but even for "mere" positivity I think
your above I2 type is only positive if you assume uniqueness of
I1 proofs (i.e. axiom K):

   I1   ≃ Eq
   MkI1 ≃ eq_refl
   I2   ≃ μx . (I1 x x) = μF

I can define

    fmap : (α → β) → F α → F β
    fmap f _ = eq_refl

but then for `fmap id = id` to be true I need axiom K.

I'd be curious to know if admitting such definitions is more or less
soundness-threatening than axiom K.


        Stefan