The Coq mailing list

[Venanzio Capretta <Venanzio.Capretta AT sophia.inria.fr>]

Lionel Elie Mamane wrote:
> 
> Hi,
> 
> Does Coq permit me to do pattern matching on a type while defining
> this same type?
> 
> What I'm trying to do (with version 7.2) is something like:
> 
> Inductive Example : Type :=
>    Example1: nat -> Example
>  | Example2:
>   let check = [e:Example]
>     Cases e of
>      (Example1 n) => (lt (S (S O)) n)
>     |(Example2 e p) => false
>     end
>   in
>  (e:Example) (check e)-> Example.
> 


This kind of definitions is not permitted in Coq, but it is allowed in
systems that admits simultaneous induction-recursion like ALF.
simultaneous induction recursion allows you to define an inductive type
and a recursive function over it simultaneously. In your case you would
define

Example : Type
  ex1: nat -> Example
  ex2: (e:Example)(check e)->Example
check : Example -> Prop
  check (ex1 n) = (lt (2) n)
  check (ex2 e h) = False

Simultaneous induction-recursion was introduced by Peter Dybjer and has
been proved to be meaningful and consistent at least in Martin-Lof type
theory.
In general there doesn't seem to be a uniform way to untangle such a
definition to define it in Coq. Of course, in your example it is easy
because check is always false on the second constructor, but you can
think of more complex ones like the following variation:

Example : Type
  ex1: nat -> Example
  ex2: (e:Example)(check e)->Example
check : Example -> Prop
  check (ex1 n) = (lt (2) n)
  check (ex2 e h) = not (check e)

It is hard to think how to translate this definition in Coq. In Alf you
would have no problem with it.


See, P.Dybjer, A general formulation of simultaneous inductive-recursive
definitions in type theory, Journal of Symbolic Logic, Volume 65, Number
2, June 2000. 

Venanzio