我使用AGDA試圖證明一些引理，並且這樣做算術prroofs，我需要證明關於自然數的事實，如：形式化使用阿格達
我不知道從哪裏開始證明這些事實。我不確定Agda是否有任何預定義的定義可以幫助完成該任務。
任何幫助高度讚賞。
Agda的標準庫很小，很難瀏覽。
您可能需要考慮查看Data/Nat.agda和Data/Nat/*.agda以瞭解與自然數算術相關的事情。
您可能不得不定義even和odd謂詞，例如，grepping它們什麼也沒有。你可能想要通過自然數來歸納地定義它們，或者重用在我提到的文件中找到的更整體可分性的概念。
你可能會發現它很有用看一看如何坡口（X - 1）（X^+ 1）= X^3 - 1採用環形公理： https://github.com/solomatov/AgdaSandbox/blob/master/Ring.agda
一些進口第一。
open import Relation.Binary.PropositionalEquality
open import Data.Nat
open import Data.Product
open import Data.Empty
open import Relation.Nullary
open ≡-Reasoning
open import Function
open import Algebra
open import Data.Nat.Properties
open CommutativeSemiring commutativeSemiring hiding (zero; _+_; _*_; sym; refl)
您可以表達平度作爲函數或作爲歸納類型。 區別在這裏解釋：http://oxij.org/note/BrutalDepTypes/ 它的介紹，所以你真的應該閱讀它，以及如其他介紹， 如果你想使用agda。有不少這樣的文字。 下面是偶的定義：
data Even : ℕ -> Set where
ezero : Even 0
esuc : {n : ℕ} -> Even n -> Even (suc (suc n))
然後，你需要定義冪。
infixr 8 _^_
_^_ : ℕ -> ℕ -> ℕ
n^0 = 1
n^(suc m) = n * n^m
n^2但是減小到n * (n * 1)，這是unconvenient。因此，我將使用這個來代替：
_^2 : ℕ -> ℕ
n ^2 = n * n
輔助引理
m+1+n≡1+m+n : ∀ m n → m + suc n ≡ suc (m + n)
m+1+n≡1+m+n zero n = refl
m+1+n≡1+m+n (suc m) n = cong suc (m+1+n≡1+m+n m n)
下一頁聲明說，正如你的第一個事實。
as-2*k : {n : ℕ} -> Even n -> ∃ λ k -> n ≡ 2 * k
as-2*k ezero = 0 , refl
as-2*k (esuc en) with as-2*k en
... | n , refl = {!!}
孔的類型是Σ ℕ (λ k → suc (suc (n + (n + 0))) ≡ k + (k + 0))。 這是∃ (λ k → suc (suc (n + (n + 0))) ≡ k + (k + 0))的縮小版本。 顯然k應該等於suc n。
as-2*k : {n : ℕ} -> Even n -> ∃ λ k -> n ≡ 2 * k
as-2*k ezero = 0 , refl
as-2*k (esuc en) with as-2*k en
... | n , refl = suc n , {!!}
現在洞的類型是suc (suc (n + (n + 0))) ≡ suc (n + suc (n + 0))。 所以你需要跳過suc s cong，並用先前定義的引理重新排列表達式的其餘部分。
cong : ∀ {a b} {A : Set a} {B : Set b}
(f : A → B) {x y} → x ≡ y → f x ≡ f y
cong f refl = refl
as-2*k : {n : ℕ} -> Even n -> ∃ λ k -> n ≡ 2 * k
as-2*k ezero = 0 , refl
as-2*k (esuc en) with as-2*k en
... | n , refl = suc n , cong suc (sym (m+1+n≡1+m+n n (n + 0)))
sym使得從x ≡ yy ≡ x。
另一個輔助引理：
remove-*2 : (n : ℕ) -> {m : ℕ} -> Even (n + n + m) -> Even m
remove-*2 0 e = e
remove-*2 (suc n) {m} e
with subst (λ n' -> Even (suc (n' + m))) (+-comm n (suc n)) e
... | esuc e1 = remove-*2 n e1
和第二個事實，而骯髒的證明。首先你需要證明一些基本情況。
even-sqrt : {n : ℕ} -> Even (n ^2) -> Even n
even-sqrt {0} ezero = ezero
even-sqrt {1} ()
even-sqrt {suc (suc n)} (esuc e) = {!!}
如果n是1然後n ^2不是Even的居民，這樣你就可以通過()排除這種情況。上下文現在看起來是這樣的：
Goal: Even (suc (suc n))
————————————————————————————————————————————————————————————
e : Even (n + suc (suc (n + n * suc (suc n))))
n : ℕ
證明是很長，所以我給你一個鏈接到整個代碼：http://lpaste.net/101722 沒有爲第三個事實也證明。 第四個事實是最簡單的一個：
0<n^2 : {n : ℕ} -> 0 < n -> 0 < n ^2
0<n^2 (s≤s le) = s≤s z≤n