不動點函數類型類實例

我試圖在一個類型的類實例的上下文中使用固定點式的功能，但它似乎並沒有工作。有什麼額外的工作要做嗎？暫時我用移動式類外的函數，並明確聲明它不動點的黑客攻擊。然而，這看起來很糟糕。不動點函數類型類實例

下面是簡單的例子：

Inductive cexp : Type := 
| CAnd : cexp -> cexp -> cexp 
| COr : cexp -> cexp -> cexp 
| CProp : bool -> cexp. 

Class Propable (A : Type) := { compile : A -> Prop }. 

Instance: Propable cexp := 
    { compile c := 
     match c with 
     | CAnd x y => (compile x) /\ (compile y) 
     | COr x y => (compile x) \/ (compile y) 
     | CProp _ => False 
     end 
    }.

這種失敗：

Error: Unable to satisfy the following constraints: 
In environment: 
c, x, y : cexp 

?Propable : "Propable cexp"

什麼是一個必須做的，使這項工作？

來源

2017-06-19 jsinglet

您可以使用fix做到這一點：

Instance: Propable cexp := 
    { compile := fix compile c := 
     match c with 
     | CAnd x y => (compile x) /\ (compile y) 
     | COr x y => (compile x) \/ (compile y) 
     | CProp _ => False 
     end 
    }.

讓我說明，如何能夠拿出它。讓我們以下面的一段代碼：

Fixpoint silly n := 
    match n with 
    | 0 => 0 
    | S n => silly n 
    end.

Fixpoint這裏是一個白話命令這使得定義的眼睛更容易一點點，但它掩蓋了什麼是怎麼回事。事實證明，什麼勒柯克實際上做的是這樣的：

Definition silly' := 
    fix self n := 
    match n with 
    | 0 => 0 
    | S n => self n 
    end.

您可以通過定義後使用Print silly.驗證。

來源

2017-06-19 06:09:01

這個作品，但我注意到，當我套用「簡體」戰術，我得到了巨大的不守規矩的定位點定義，而不是隻是一個簡單的公式與標識符。有沒有辦法告訴Coq製作更好看的標識符，而不是將整個函數內聯打印？ – jsinglet

這是一個常見問題。這些問題可能會提供一些見解：[1]（https://stackoverflow.com/q/39355817/2747511），[2]（https://stackoverflow.com/q/28432187/2747511），[3]（HTTPS ：//stackoverflow.com/q/41404337/2747511）。 'fold'可以幫助（但很少做），也許你需要在減少發生，其中一個更好的控制。如果這些都無濟於事，請給我一個鏈接到實際的代碼 - 我會試着去查看它。 –

不動點函數類型類實例

回答

相關問題