Coq中的受限感應類型定義

我想以某種方式限制允許在歸納定義中使用哪種輸入構造函數。說我想說的定義二進制數如下：Coq中的受限感應類型定義

Inductive bin : Type := 
    | O : bin 
    | D : bin -> bin 
    | S : bin -> bin.

這裏的想法是，d通過在結尾處增加一個零雙打非零數字和S接受一個數字與零作爲最後一個數字並開啓最後一位數字變成一位。這意味着，以下是合法的數字：

S 0 
D (S 0) 
D (D (S 0))

而下面不會是：

S (S 0) 
D 0

有沒有辦法在一個乾淨的方式強制執行的歸納定義這些限制嗎？

來源

2012-12-23 pki

您可以定義bin與謂詞合法的含義，然後爲符合該謂詞的子集bin指定名稱。然後你用Program Definition和Program Fixpoint而不是Definition和Fixpoint編寫函數。對於遞歸函數，您還需要一個度量來證明函數的參數減小，因爲函數不再是結構遞歸。

Require Import Coq.Program.Program. 

Fixpoint Legal (b1 : bin) : Prop := 
    match b1 with 
    | O  => True 
    | D O  => False 
    | D b2 => Legal b2 
    | S (S _) => False 
    | S b2 => Legal b2 
    end. 

Definition lbin : Type := {b1 : bin | Legal b1}. 

Fixpoint to_un (b1 : bin) : nat := 
    match b1 with 
    | O => 0 
    | D b2 => to_un b2 + to_un b2 
    | S b2 => Coq.Init.Datatypes.S (to_un b2) 
    end. 

Program Definition zer (b1 : lbin) := O. 

Program Fixpoint succ (b1 : lbin) {measure (to_un b1)} : lbin :=

但是this簡單的方法可能會更容易。

來源

2012-12-23 23:28:56

這似乎比其他答案更合理。我懶得寫一個。你可以把一個謂詞作爲額外的參數，但是然後寫數字很煩人。在需要時你可能不會關心和規範化。 – Ptival

這可以通過歸納遞歸定義完成 - 但不幸的是Coq不支持這些定義。

從一個面向對象的程序設計的角度來看，O，D和S是bin亞型，它們的構造類型然後不訴諸邏輯謂詞定義，但Coq的不支持面向對象編程本身任一。

但是，Coq確實有類型類。所以我可能要做的是讓bin成爲一個類型類型，並使每個構造函數成爲一個單獨的歸納類型，其中每個類型都有一個類型類型的實例bin。我不確定類型類的方法是什麼。

來源

2012-12-23 10:12:07

Coq中的受限感應類型定義

回答

相關問題