Coq：如何從可判斷的Prop創建一個bool？

我想將我的程序構建爲抽象模塊，並編寫使用抽象類型的函數。但是我不能使用match來破壞抽象類型，所以我將不得不創建某種反轉引理，但我也不能在其上使用match。我試圖把我的問題歸結爲：Coq：如何從可判斷的Prop創建一個bool？

首先創建一個Module Type，可以使用decidable類型。

Require Import Decidable. 

Module Type decType. 
    Parameter T : Type. 
    Axiom decT : forall (a b:T), decidable (a=b). 
End decType.

這裏是一個例子：nat是可判定的。但其目的是編寫plus等，只針對抽象類型。（我已經刪除了參數zero，Succ和他們的要求，使這裏的例子最小）。

Require Peano_dec. 

Module nat_dec <: decType. 
    Definition T := nat. 
    Definition decT := Peano_dec.dec_eq_nat. 
End nat_dec.

現在我的問題：我想寫參數化的decType模塊上有一個返回true如果a=b和false否則功能的模塊。由於a和b是decType這應該是可判定的（因此可以計算或？），但是如何編寫beq？

Module decBool (M: decType). 
    Import M. 
    Definition beq (a b:T) : bool := 
    ??? 
    . 

End decBool.

我的想法到目前爲止是，我有一個布爾函數添加到decType模塊類型，像這樣：

Module Type decType. 
    Parameter T : Type. 
    Axiom decT : forall (a b:T), decidable (a=b). 
    Parameter decB : forall (a b:T), {a=b}+{a<>b}. 
End decType.

然後定義nat_dec模塊decB以上。

這是一個必須做的事情（即定義函數decB）？是否不可能使用抽象的事實，即類型是可判定的，而不通過返回布爾的函數？

來源

2015-10-02 larsr

由於Coq中命題和計算對象的分離（例如參見this answer），您無法編寫此函數。，將您decB參數到你的模塊

通知使得decidable公理不必要的，因爲你可以使用{P} + {Q}派生P \/ Q。

我想添加一些相關的註釋。首先，我會避免使用Coq模塊系統來執行除命名空間和寫入不透明定義之外的任何操作。如果你想編寫參數定義，你可能最好使用依賴記錄，例如

Record eqType := { 
    sort :> Type; 
    eqb : sort -> sort -> bool; 
    eqbP : forall x y, eqb x y = true <-> x = y 
}.

這主要是由Ssreflect採取的做法。您可以使用規範結構（如Ssreflect）或鍵入類來更容易地使用這些相關記錄。

其次，您可以編寫明確的消除器函數以避免不得不求助於match。例如，nat_rect功能允許你寫遞歸函數上nat與高階參數：

nat_rect : forall (T : nat -> Type), 
      (* value for 0 *) 
      T 0 -> 
      (* body for recursive call *) 
      (forall n, T n -> T (S n)) -> 
      forall n, T n.

這些功能對每個感應數據類型自動定義。它們涉及依賴類型，但您也可以使用它們來進行非依賴類型遞歸。雖然這可能會有點低效，但也可以通過傳遞函數來忽略遞歸調用的值（在上面的示例中爲第二個函數參數的T n參數），將它們用於模式匹配。

來源

2015-10-02 17:07:08

Coq：如何從可判斷的Prop創建一個bool？

回答

相關問題