阿格達定理權力

Question

我試圖證明如下：

1-pow : ∀ {n : ℕ} → 1 pow n ≡ 1 
1-pow {zero} = refl 
1-pow {suc x} = {!!} 

我是全新的，以Adga，甚至不真的知道從哪裏開始。任何建議或指導？顯然很容易在紙上證明，但我不確定告訴Agda。

我定義我的戰俘功能如下：

Answer 1

當1-pow上n你的模式匹配，並找出它是zero，阿格達會看看的_pow_的定義和檢查的一個函數子句匹配。第一個是，所以它將應用該定義並且1 pow zero變成1。 1顯然等於1，所以refl將用於證明。

n是suc x是什麼情況？問題在於：Agda無法承諾第二個子句（因爲x可能是zero），也不是第三個子句（因爲x對於某些y可能是suc y）。所以，你必須走一步，以確保阿格達適用的_pow_定義：

1-pow : ∀ {n : ℕ} → 1 pow n ≡ 1 
1-pow {zero}  = refl 
1-pow {suc zero} = {!!} 
1-pow {suc (suc x)} = {!!} 

讓我們看看什麼是第一孔的類型。 Agda告訴我們這是1 ≡ 1，所以我們可以再次使用refl。最後一個有點棘手，我們應該生產1 * 1 pow (suc x) ≡ 1類型的東西。假設您正在使用_*_的標準定義（即左側參數的遞歸和左側的重複添加，例如標準庫中的那個），則這應該減少到1 pow (suc x) + 0 ≡ 1。歸納假設（即1-pow適用於suc x）告訴我們1 pow (suc x) ≡ 1。所以我們幾乎在那裏，但我們不知道n + 0 ≡ n（這是因爲添加由左參數遞歸定義，所以我們不能簡化這個表達式）。一種選擇是證明這個事實，我將其作爲一個練習。不過，這裏有一個提示：你可能會發現這個功能很有用。

cong : ∀ {a b} {A : Set a} {B : Set b} 
     (f : A → B) {x y} → x ≡ y → f x ≡ f y 
cong f refl = refl 

它已經是Relation.Binary.PropositionalEquality模塊的一部分，所以你不需要自己定義它。

所以，回顧一下：我們知道n + 0 ≡ n和1 pow (suc x) ≡ 1，我們需要1 pow (suc x) + 0 ≡ 1。這兩個事實結合在一起很好地 - 平等是傳遞的，所以我們應該能夠合併1 pow (suc x) + 0 ≡ 1 pow (suc x)和1 pow (suc x) ≡ 1成一個證明，事實上，這樣的話：

1-pow {suc (suc x)} = trans (+0 (1 pow suc x)) (1-pow {suc x}) 

就是這樣！

---

讓我來提一下其他方法。

整個證明也可以使用1 * x ≡ x的證明來完成，雖然這與我們之前所做的幾乎沒有什麼不同。

您可以簡化_pow_到：

_pow_ : ℕ → ℕ → ℕ 
x pow zero = 1 
x pow (suc y) = x * (x pow y) 

這是一起工作稍微更方便。證明會相應地改變（即它不會有原始證明的第二個條款）。

最後，你可以這樣做：

1-pow : ∀ {n : ℕ} → 1 pow n ≡ 1 
1-pow {zero}  = refl 
1-pow {suc zero} = refl 
1-pow {suc (suc x)} = cong (λ x → x + 0) (1-pow {suc x}) 

揣摩爲什麼作品！如果您有任何問題，請在評論中告訴我，我會幫助您。