勒柯克符號的多類型列表

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

下面是勒柯克的文檔提取約lists

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

我會堅持使用;而不是,因爲後者是在勒柯克的語法經常使用，它可能會非常棘手正確地得到符號的優先級。

最佳，

五

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機制勒柯克的不走類型的子表達式的考慮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".