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

Question

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

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

Answer 1

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

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

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

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

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