История изменений
Исправление quasimoto, (текущая версия) :
вернись к первому посту, и продемонстрируй
Определения:
open import Data.Nat
fib₁-rec : ℕ → ℕ → ℕ → ℕ
fib₁-rec a b zero = a
fib₁-rec a b (suc n) = fib₁-rec b (a + b) n
fib₁ : ℕ → ℕ
fib₁ = fib₁-rec 0 1
fib₂ : ℕ → ℕ
fib₂ (suc (suc n)) = fib₂ n + fib₂ (suc n)
fib₂ n = n
доказательство эквивалентности:
open import Data.Nat.Properties -- un'private'ized
open import Relation.Binary.PropositionalEquality
fib₁≡fib₂ : ∀ n → fib₁ n ≡ fib₂ n
fib₁≡fib₂ = go 0 where
go : ∀ m n → fib₁-rec (fib₂ m) (fib₂ (suc m)) n ≡ fib₂ (m + n)
go m zero = cong fib₂ (sym (n+0≡n m))
go m (suc n) = trans (go (suc m) n) (cong fib₂ (sym (m+1+n≡1+m+n m n)))
Две строчки, фактически.
Откуда следует, что ∀ n → fib₁ n ≡ fib₂ n и его отрицание не являются независимыми, то есть если начать перечислять все доказательства и опровержения, то за конечное время найдётся доказательство эквивалентности — для не независимых утверждений такая проблема разрешима (вообще — http://en.wikipedia.org/wiki/Entscheidungsproblem с исключениями вроде http://en.wikipedia.org/wiki/Presburger_arithmetic или http://en.wikipedia.org/wiki/Tarski's_axioms — consistent + complete + decidable).
На практике «за конечное время» может быть «за нереально долгое время», так что проще найти доказательство в ручном или полуручном режиме. Agda или Coq это пруф ассистенты (http://en.wikipedia.org/wiki/Proof_assistant), так что они предполагают ручные и полуручные доказательства, но есть и автоматические пруверы (http://en.wikipedia.org/wiki/Automated_theorem_proving), которые вполне способны доказывать такого рода вещи полностью автоматически (решая полуразрешимую проблему, то есть с зависаниями — нужно ставить таймауты).
Исходная версия quasimoto, :
вернись к первому посту, и продемонстрируй
Определения:
open import Data.Nat
fib₁-rec : ℕ → ℕ → ℕ → ℕ
fib₁-rec a b zero = a
fib₁-rec a b (suc n) = fib₁-rec b (a + b) n
fib₁ : ℕ → ℕ
fib₁ = fib₁-rec 0 1
fib₂ : ℕ → ℕ
fib₂ (suc (suc n)) = fib₂ n + fib₂ (suc n)
fib₂ n = n
доказательство эквивалентности:
open import Data.Nat.Properties -- un'private'ized
open import Relation.Binary.PropositionalEquality
fib₁≡fib₂ : ∀ n → fib₁ n ≡ fib₂ n
fib₁≡fib₂ = go 0 where
go : ∀ m n → fib₁-rec (fib₂ m) (fib₂ (suc m)) n ≡ fib₂ (m + n)
go m zero = cong fib₂ (sym (n+0≡n m))
go m (suc n) = trans (go (suc m) n) (cong fib₂ (sym (m+1+n≡1+m+n m n)))
Три строчки, фактически.
Откуда следует, что ∀ n → fib₁ n ≡ fib₂ n и его отрицание не являются независимыми, то есть если начать перечислять все доказательства и опровержения, то за конечное время найдётся доказательство эквивалентности — для не независимых утверждений такая проблема разрешима (вообще — http://en.wikipedia.org/wiki/Entscheidungsproblem с исключениями вроде http://en.wikipedia.org/wiki/Presburger_arithmetic или http://en.wikipedia.org/wiki/Tarski's_axioms — consistent + complete + decidable).
На практике «за конечное время» может быть «за нереально долгое время», так что проще найти доказательство в ручном или полуручном режиме. Agda или Coq это пруф ассистенты (http://en.wikipedia.org/wiki/Proof_assistant), так что они предполагают ручные и полуручные доказательства, но есть и автоматические пруверы (http://en.wikipedia.org/wiki/Automated_theorem_proving), которые вполне способны доказывать такого рода вещи полностью автоматически (решая полуразрешимую проблему, то есть с зависаниями — нужно ставить таймауты).