Search code examples
coq

Extra type constructor if parameter matches a pattern

Let's define a type representing sets:

Inductive mySet :=
| funSet   : mySet -> mySet -> mySet
| prod     : mySet -> mySet -> mySet.

We have two type constructors:

  • funSet A B - a set of functions from A to B
  • prod A B - a set of pairs A B.

I would like to define type representing elements of these sets in the following way

Inductive el (X : mySet) :=
  | eval  : forall {Y : mySet}, el (funSet Y X) -> el Y -> el X
  | proj1 : forall {Y : mySet}, el (prod X Y) -> el X
  | proj2 : forall {Y : mySet}, el (prod Y X) -> el X
  | compose : forall {A B C : mySet}, el (funSet A B) -> el (funSet B C) -> el (funSet A C).

Where we have a constructor eval which can evaluate a function, an element of funSet X Y or other constructors proj1 and proj2 which extract corresponding element of a pair.

However, the definition of compose is not valid as it is. I get an error:

Error: Last occurrence of "el" must have "X" as 1st argument in 
 "forall A B C : mySet, el (funSet A B) -> el (funSet B C) -> el (funSet A C)".

Ok, that is understandable, but is there a way to enable the constructor compose when X matches the pattern funSet A C ?

I really want to have compose as a constructor. Later on, I want to do pattern matching on expression composed of eval proj1 proj2 compose.

Solution

  • The solution is simple enough: make X into an index rather than a parameter.

    Inductive mySet :=
| funSet   : mySet -> mySet -> mySet
| prod     : mySet -> mySet -> mySet.

Inductive el: mySet -> Type :=
  | eval  : forall {X Y : mySet}, el (funSet Y X) -> el Y -> el X
  | proj1 : forall {X Y : mySet}, el (prod X Y) -> el X
  | proj2 : forall {X Y : mySet}, el (prod Y X) -> el X
  | compose : forall {A B C : mySet}, el (funSet A B) -> el (funSet B C) -> el (funSet A C).

    Intuitively, the difference is that for some inductive type IndType X, when X is a parameter, each IndType X has essentially the same shape. For example, with list X, regardless of what X is, the elements of the type look like nil, cons a nil, cons a (cons b nil) etc. In contrast, for el X, if X happens to be some funSet A C, it gets some extra constructors of the form compose f g. The actual shape of the inductive type depends on what X is.

    See also: