Coq：通過模式匹配定義函數的參數

我想定義一個函數，其行爲取決於它的參數是否（至少）是n位函數。一個基本的（失敗）的嘗試是Coq：通過模式匹配定義函數的參數

Definition rT {y:Type}(x:y) := ltac: (match y with 
| _ -> _ -> _ => exact True 
| _ => exact False end). 

Check prod: Type -> Type -> Type. 
Compute rT prod. (*= False: Prop*) 
Print rT. (*rT = fun (y : Type) (_ : y) => False: forall y : Type, y -> Prop*)

正如你看到的，rT映射一切False。爲什麼？如果我在匹配條款中替換y w/type of x

來源

2017-04-22 jaam

您希望的函數不能以您期望的類型存在於Gallina中。

你的功能被接受，但如果你打印出來，你可以看到它的身體是：

rT = fun (y : Type) (_ : y) => False

利納沒有辦法的match -ing上Type。有多種方法可以處理n元函數，這樣可以檢查其元數，但是它涉及依賴類型來靜態捕獲元數。例如，對於均勻n元功能：

https://coq.inria.fr/library/Coq.Numbers.NaryFunctions.html

來源

2017-04-22 21:06:51 Ptival

是這背後的原因，勒柯克的模式匹配被設計爲僅在感應式的構造工作？ – jaam

模式匹配有兩個級別。「Gallina」模式匹配確實只適用於歸納和合作類型。您的代碼使用的「Ltac」模式更符合句法，因此它所做的不能表達爲Gallina術語（通常）。 – Ptival

Coq：通過模式匹配定義函數的參數

回答

相關問題