2012-08-22 68 views
1

我想定義一個提供身份和組成的類。除了其他有用的實例(List with nil and concatenation;與關係,好,身份和組合;-)),我想有一個函數實例。在Coq中有( - >)的顯式類型構造函數嗎?

鑑於

Class Cat (C0 : Type) (C1 : C0 -> C0 -> Type) := 
    { identity : forall a, C1 a a 
    ; compose : forall {a b c : C0}, C1 b c -> C1 a b -> C1 a c 
    (* snip: some laws *) 
    }. 

我希望能夠定義像

Instance Cat (->) := { ... }. 

但在勒柯克運營商不一樣,一起想。首先我假設->是一個符號,但Locate "_ -> _".聲稱這是一個Unknown notation。使用fun a b => a -> b有點作品,但類型看起來很有趣。

> Check (identity nat). 
identity nat 
    : (fun a b : Type => a -> b) nat nat 

(同去的Eval compute in,看來它並沒有簡化的類型。)我寧願更具可讀性identity nat : nat -> nat。 (目前,這些類型對於我正在做的事情來說變得不可讀)

有沒有辦法讓'原始'->或至少說服Coq給我更好的類型?


附註:我建立了很多代表評價語義Inductive,那是我的目標是「正常」的編程語言的子集映射到勒柯克和背部,傳輸安全約束和做魔術。我不得不一遍又一遍地用不同的構造函數來證明相同的東西,並希望這能讓我證明一次又一次的東西。我認爲類別是抽象的正確方法。我在這裏包括這個筆記,以防萬一我錯了,也許有更好的方法來避免整個->問題。

回答

2

我只能回答部分問題。 ->不是像+exists{ ... | ... }這樣的標記,它是內置在解析器中的,如forall。語法a -> b相當於forall x:a, bxb(我不知道,如果它在任何情況下都等同,可能會有用途,其中x不能b發生,你必須使用->)免費。

原因是函數抽象和應用,並執行它們的類型,是Coq的基礎,它們不是從更原始的概念派生的。您不能直接使用fun,應用程序->forall,因爲它們不是一流的對象。

這就是說,類型類是一種專門用於應用程序的方法。我不熟悉他們,所以我不知道是否有辦法做你想做的事情。

+4

實際上,[Logic.v](https://gforge.inria.fr/scm/viewvc.php/trunk/theories/Init/Logic.v?view=markup&revision=15929&root=coq)定義了「符號」A - > B「:=(forall(_:A),B):type_scope。」 – minopret

相關問題