類型中使用的agda命題 - 它是什麼意思？

Question

我從「Agda的殘酷介紹」中獲取此信息http://oxij.org/note/BrutalDepTypes/

假設我們想要在偶數上定義除以二的數。我們可以做到這一點爲：

div : (n : N) -> even n -> N 
div zero p = zero 
div (succ (succ n)) p= succ (div n p) 
div (succ zero)() 

N是自然數，甚至是下面的 「命題」

even : N -> Set 
even zero = \top 
even (succ zero) = \bot 
even (succ (succ n)) = even n 
data \bot : Set where 
record \top : Set where 

當你計算表達式 DIV（SUCC（SUCC零）） 你得到 \ p - > succ zero 這是您所期望的。但是，我不明白的是如何解釋\ p。我也不明白什麼代碼 f = \ bot - > N f = div（succ zero） 的意思。我明白\ bot暗示A表示任何A ...，因此該類型是有效的。我想我認爲依賴型打字會允許我以這樣的方式編寫div，div（succ zero）會更明確地失敗類型檢查。

任何人都可以提出一個建議，如何使用和查看agda中的謂詞？

Answer 1

在你的例子中的p是證明你分開的號碼（n）確實是even。當你想使用你的div函數來劃分一個數字時，僅給出數字是不夠的！阿格達代表給你回的另一個功能 - 這消耗了證明2 even並還給功能1.

讓我們寫了一些測試，看看它是如何工作的：

test₁ : ℕ 
test₁ = div 4 ? 

的類型在這種情況下，這個洞是不可冒犯的，⊤。 even 4減少了⊤兩個步驟，這樣你就可以很容易地在空記錄填寫或只給一個下劃線 - 只有一個可能值，阿格達可以填補在：

test₁ = div 4 _ 

時，在另一方面，你給它一個奇數，例如：

test₂ : ℕ 
test₂ = div 3 ? 

的類型的孔減小到⊥。 ⊥是空的類型;給出這種類型的數值來證明你的邏輯矛盾。所以我們被困在這裏 - 這正是我們想要的。現在

---

，你想使它感覺多一點...隱，也許引進一個編譯錯誤，當我們試圖給它一個奇數。

Agda只能通過統一來填充隱含的東西。雖然統一可以做一些複雜的事情，但有一些問題無法解決;猜測證據就是其中之一。如果我們想保持隱含的證明，我們必須保持簡單。 even就是一個很好的例子：我們可以從我們分割的數字中完整地計算它，它返回⊤（可以簡單填充）或⊥（這意味着有錯誤）。

div-implicit : (n : ℕ) {p : even n} → ℕ 
div-implicit n {p} = div n p 

即使數字是罰款：

test₃ : ℕ 
test₃ = div-implicit 4 

奇數給出一個編譯錯誤，請參閱我的previous answer在這個問題上。我們得到明亮的黃色和I-鴕鳥政策知道什麼對填充錯誤：

___10 : ⊥ [ at D:\Agda\SO6.agda:27,9-23 ] 

---

這裏有一個關於如何通過阿格達做出猜測的瑣碎的證明義務食譜：

首先，我們需要一個確定參數是否正確的函數。通常，這是返回Bool或Dec的函數。

check : ℕ → Bool 

接下來，我們改造Bool成一個命題：

-- The Bool is true. 
True : Bool → Set 
True true = ⊤ 
True false = ⊥ 

-- The Bool is false. 
False : Bool → Set 
False true = ⊥ 
False false = ⊤ 

最後，我們可以有一個隱含的說法，阿格達將填補，如果參數是正確的，或者給回亮黃色：

f : (n : ℕ) {p : True (check n)} → ℕ 

---

阿格達允許你省略函數方程如果右邊你會發現其中一個論點沒有意義，可以這麼說。更具體地說，當你寫下()作爲一種模式時，你斷言任何人都不可能提供這種類型的參數 - 如果沒有人能用這些參數實際調用函數，爲什麼還要寫一個右手邊？考慮一個例子：

f : (m n : ℕ) → m ≡ n → ℕ 
f zero (suc zero) p = ? 
f _ _ _ = ? 

p是什麼類型的？這是一個證明0 ≡ 1 - 這顯然是一個廢話，沒有人可以打電話f 0 1，並給出一個證明0 ≡ 1。我們有理由用()更換p並離開了右邊：

f zero (suc zero)() 

將這一對div例如：

div (suc zero) p = ? 

現在，p類型是⊥。任何人都無法給出⊥類型的值。因此，我們再次告知阿格達這種情況下是不可能的：

div (suc zero)() 

---

現在，那些是什麼問號？關於agda-mode的好處是，它可以幫助您以合作的方式構建您的程序。當你在某個地方寫上?時，你告訴agda-mode「我不知道這裏發生了什麼，讓我們一起找出來」。

當您再檢查文件通過C-c C-l阿格達需要那些? S和把他們變成孔（這些是{ }0你看到的）。程序中可以有多個孔，這說明了背後的數字。

現在，我說這些允許你以合作的方式建立程序，合作的地方在哪裏？你可以用一個洞來做很多事情。例如，你可以問它的類型（通過C-c C-,）：

div : (n : ℕ) → even n → ℕ 
div zero   p = zero 
div (suc (suc n)) p = { }0 
div (suc zero) () 

-- Agda information buffer 
Goal: ℕ 
———————————————————————————————————————————————————————————— 
p : even n 
n : ℕ 

這三行告訴你，你最終還是要寫下ℕ類型（目標）的expreesion和範圍你有even n型p和n類型ℕ。

你甚至可以寫東西的孔內，並詢問什麼是目前你寫什麼類型（通過C-c C-.）：

div (suc (suc n)) p = {n }0 

-- Agda information buffer 
Goal: ℕ 
Have: ℕ 
———————————————————————————————————————————————————————————— 
p : even n 
n : ℕ 

當你滿意，你可以用任何你更換洞」已經寫入（通過，只要它typechecks）通過C-c C-space。

如果你不關心實現（例如，你正在寫一個證明，任何事情都會做），你也可以告訴Agda嘗試通過C-c C-a來猜測它。當你有很多微不足道的情況時，這是非常有用的。

然後有案例分裂。當你編寫一個函數時，你通常必須進行模式匹配以更多地瞭解參數。 Agda允許您節省手動編寫所有這些函數方程式的一些痛苦。

_+_ : (m n : ℕ) → ℕ 
m + n = { }0 

我們寫上，我們要做的孔內的情況下分裂一個變量：

_+_ : (m n : ℕ) → ℕ 
m + n = {m }0 

而且按神奇C-c C-c瞧：

_+_ : (m n : ℕ) → ℕ 
zero + n = { }0 
suc m + n = { }1