Agda中的可判斷謂詞

Question

我是Agda的新手，需要幫助瞭解Decidable函數和Dec類型。

我想定義一個一階邏輯謂詞，我想用證明編碼某種布爾值。我發現這樣做的方法是使用Dec類型..

現在，據我所知，能夠做到這一點，我必須重新定義所有邏輯運算符的類型是可判定的，而不是類型集。這樣做，我有點嵌入成新的類型，這是我這樣做是爲了和運營商：

data _∧_ (A B : Set) : Set where 
    _&_ : A → B → A ∧ B 

Dec∧ : {A B : Set} → A ∧ B → Dec (A ∧ B) 
Dec∧ A∧B = yes (A∧B) 

是它做的方式，或者是有另一種方式？

然後，我想用這個操作定義在納特值的關係，所以我做了這樣的事情：

_◆_ : ℕ → ℕ → Dec∧ (Rel ℕ lzero) (ℕ → Set) 
x ◆ y = (0 < x) ∧ (x ² ≡ 2 * y ²) 

但是這給人一種類型的錯誤..

我不知道如何與Dec合作，我將不勝感激，如果任何人可以指導我的教程或例子使用它來證明邏輯陳述..

Answer 1

基本上可判斷的謂詞是一個謂詞，我們有一個算法，在有限的時間內終止並返回要麼是一起證明它是真實的，要麼沒有一起證明它是否定的。例如，對於每兩個自然數，我們可以證明它們是相等的或者它們不相等。

你寫的東西沒有輸入檢查。你的函數應該返回Dec（Relℕlero）（ℕ→Set），第一個參數是正確的，但第二個參數是不正確的。它應該是一個函數，例如\ x - > 2 * x。

P.S.對我來說，這個功能毫無意義。你想用它來完成什麼？