coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Merlin Göttlinger <megoettlinger AT gmail.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] Mutual inductive types with a predicate
Date: Wed, 15 Nov 2017 09:22:52 +0000
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=megoettlinger AT gmail.com; spf=Pass smtp.mailfrom=megoettlinger AT gmail.com; spf=None smtp.helo=postmaster AT mail-it0-f53.google.com
Ironport-phdr: 9a23:mcyj8BC5yFJiUI1UlQf7UyQJP3N1i/DPJgcQr6AfoPdwSP3zocbcNUDSrc9gkEXOFd2Crakb26yL6+jJYi8p39WoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6i760TlHUB74LE9+Ivn/Mo/UlcW+ke6osdWHaAJRwTG5fLlaLROsrAyXuNNA0qV4LaNk7xbTpnpOTMvI2X9sJFSckgy0ssK985lu7zhUuvQu+tRoXqDzfqB+RrtdWmd1e1sp7dHm4EGQBTCE4WERBz0b

Hi,

what I want to implement is a more complicated version of this:

Inductive A :=

| a1 : nat -> A

| a2 : nat -> A

| a3 : B -> A -> A

with B :=

| b1 : nat -> B

| b2 : { ae : A | P ae} -> B

with P : A -> Prop :=

| pa3 : forall b a, P a -> P (a3 b a)

| pa1 : forall n, P (a1 n).

However that is rejected by coq (8.6.1) with the error The reference A was not found in the current environment. at the Type of P.

Why is that the case?

One way I found to avoid this is to "bake the predicate into the type":

Inductive A : bool -> Set :=

| a1 : nat -> A true

| a2 : nat -> A false

| a3 {b} : B -> A b -> A b

with B : Set :=

| b1 : nat -> B

| b2 : A true -> B.

But this forces you to wrap and unwrap A everywhere where you do not care about the predicate.

Is there a better way?

Cheers,

Merlin

[Coq-Club] Mutual inductive types with a predicate, Merlin Göttlinger, 11/15/2017
- Re: [Coq-Club] Mutual inductive types with a predicate, Matthieu Sozeau, 11/15/2017
  - Re: [Coq-Club] Mutual inductive types with a predicate, Thorsten Altenkirch, 11/15/2017
    - Re: [Coq-Club] Mutual inductive types with a predicate, Bas Spitters, 11/16/2017