Here is a contrived multi type list:
Inductive Apple : Set :=.
Inductive Pear : Set :=.
Inductive FruitList : Set :=
| Empty
| Cons_apple (a : Apple) (p : FruitList)
| Cons_pear (p : Pear) (p: FruitList).
Variable a : Apple.
Variable p : Pear.
Definition a_fruitList := Cons_apple a (Cons_pear p Empty).
Is there a way to define a list notation for this so that, for example, a_fruitList could have been defined by [p,a] instead?
The problem is that your list has two cons constructors, whereas the usual notation mechanism for recursive notations requires you to use always the same constructors. Coercions can help you overcome part of this problem:
Section ApplesAndPears.
Variable Apple Pear : Set.
Inductive FruitList : Set :=
| Nil
| ConsApple (a : Apple) (l : FruitList)
| ConsPear (p : Pear) (l : FruitList).
Inductive Fruit : Set :=
| IsApple (a : Apple)
| IsPear (p : Pear).
Coercion IsApple : Apple >-> Fruit.
Coercion IsPear : Pear >-> Fruit.
Definition ConsFruit (f : Fruit) (l : FruitList) : FruitList :=
match f with
| IsApple a => ConsApple a l
| IsPear p => ConsPear p l
end.
Notation "[ ]" := (Nil) (at level 0).
Notation "[ x ; .. ; y ]" := (ConsFruit x .. (ConsFruit y Nil) ..) (at level 0).
Variable a : Apple.
Variable p : Pear.
Definition a_fruitList := [ a ; p ].
End ApplesAndPears.
(By the way, I'm assuming that you really meant to write [ a ; p ], and not [ p ; a ]. If you did mean to write [ p ; a ], then you just have to use a SnocFruit function instead, that adds the element to the end of the list. However, this would make the problems explained later even worse.)
Now, we've defined a new function to replace the constructors, and can use that function instead, by declaring the constructors of Fruit to be coercions.
This solution is not entirely satisfactory, of course, because the term your notation produces makes reference to ConsFruit, while ideally it would be nice to have something that picks ConsApple or ConsFruit depending on the argument you give. I suspect there isn't a way of doing this with the notation mechanism, but I could be wrong.
This is one of the reasons why I would recommend you to use just the list type and declare another type such as Fruit to hold Apple and Pear instead of using two cons constructors, unless you have a very good reason not to.
As mentioned by Arthur Azevedo De Amorim, the issue is that the Notation mechanism of Coq does not take the types of the sub-expressions into account to discriminate between Cons_apple and Cons_pear. However, you can use Type Classes to do that:
Class Cons_fruit(A:Set) := {
CONS: A -> FruitList -> FruitList }.
Instance Cons_fruit_apple: Cons_fruit Apple:= { CONS := Cons_apple }.
Instance Cons_fruit_pear: Cons_fruit Pear := { CONS := Cons_pear }.
Notation " [ x ; .. ; y ] " := (CONS x .. (CONS y Empty) .. ).
Definition test := [a; p; p; a ].
We define here a type class Cons_fruit containing a single function, and two instances, one for consing apples and one for consing pears. We can then use the templated CONS function in the notation, and Coq will select the appropriate instance when needed.
Note that this may result in less understandable error messages. For instance, with
Definition bad:= [ 0; p ].
You will get
Error: Cannot infer the implicit parameter Cons_fruit of CONS.
Could not find an instance for "Cons_fruit nat".
Here is an extract from Coq's documentation about lists
Notation " [ ] " := nil : list_scope.
Notation " [ x ] " := (cons x nil) : list_scope.
Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) : list_scope.
I would stick to using ; and not , since the latter is often use in Coq's syntax, it might be tricky to get the notation priority correctly.
Best,
V.
Inductive Apple: Set :=.definesAppleas an empty set. Thus, when you declareVariable a: Apple, you introduce an inconsistency in your development. You should useParameter Apple: Setinstead. - Virgile