Coq обозначение списка нескольких типов

Question

Вот надуманный мульти список типов:

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). 

Есть ли способ, чтобы определить список обозначений для этого, так что, например, a_fruitList могли быть определены [p,a] вместо этого?

Answer 1

Вот выдержка из документации Coq в о lists

Notation " [ ] " := nil : list_scope. 
Notation " [ x ] " := (cons x nil) : list_scope. 
Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) : list_scope. 

Я бы придерживаться использования ; и не ,, поскольку последний часто используют в синтаксисе Coq, это может быть сложно получить приоритет обозначения правильно.

Бест,

В.

Answer 2

Проблема заключается в том, что список имеет два минусы конструкторов, в то время как обычный механизм обозначения для рекурсивных обозначений требует, чтобы вы всегда использовать одни и те же конструкторы. Приведение может помочь вам преодолеть часть этой проблемы:.

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. 

(Кстати, я предполагаю, что вы на самом деле имел в виду писать [ a ; p ], а не [ p ; a ] Если ты хочешь написать [ p ; a ], то вы просто вместо этого использовать функцию SnocFruit, которая добавит элемент в конец списка. Однако это еще раз ухудшит проблемы, описанные позже.)

Теперь мы определили новую функцию для замены конструкторов и может использовать эту функцию, объявив конструкторы Fruit для принуждения.

Это решение не является полностью удовлетворительным, конечно, потому что термин вашего обозначения производит делает ссылку на ConsFruit, в то время как в идеале было бы неплохо иметь что-то, что улавливает ConsApple или ConsFruit в зависимости от аргумента вы даете. Я подозреваю, что нет способа сделать это с помощью механизма обозначений, но я могу ошибаться.

Это одна из причин, почему я рекомендую вам использовать только list типа и декларирую другой тип, такие как Fruit провести Apple и Pear вместо двух минусов конструкторов, если у вас есть очень веские причины не делать этого.

Answer 3

Как отметил Arthur Azevedo De Amorim, проблема в том, что Notation механизм Coq не принимает типы суб-выражений во внимание, чтобы различать Cons_apple и Cons_pear. Тем не менее, вы можете использовать Type Classes сделать:

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 ]. 

Определим здесь типа класс Cons_fruit, содержащий одну функцию, а также два экземпляра, один для consing яблок и один для consing груши. Затем мы можем использовать шаблонную функцию CONS в обозначении, а Coq выберет соответствующий экземпляр, когда это необходимо.

Обратите внимание, что это может привести к менее понятным сообщениям об ошибках.Например, с

Definition bad:= [ 0; p ]. 

Вы получите

Error: Cannot infer the implicit parameter Cons_fruit of CONS. 
Could not find an instance for "Cons_fruit nat".