Fibonacci function

Description

Define a Fibonacci function and prove FibFunc predicate for your function.

Definitions (download)

module Definitions where

open import Data.Nat

data Fib : ℕ → ℕ → Set where
  Fib0 : Fib 0 1
  Fib1 : Fib 1 1
  FibN : ∀ {n x y} → Fib (suc n) x → Fib n y → Fib (suc (suc n)) (x + y)

FibFunc : (ℕ → ℕ) → Set
FibFunc f = ∀ n → Fib n (f n)

Theorem (download)

module Theorem where

open import Data.Nat
open import Definitions

postulate
  fib : ℕ → ℕ

  fib-is-FibFunc : FibFunc fib

Verifier

module Verifier where

open import Definitions
open import Theorem

verify : FibFunc fib
verify = fib-is-FibFunc

Proofs

Rank Prover Size Date
1 strout 164 2014-01-06 11:18:46 JST
2 chiguri 233 2013-05-29 17:22:40 JST
3 phi16_ 239 2017-11-14 15:42:49 JST
4 trigott 239 2014-04-15 23:54:00 JST
5 kiritex 239 2014-04-04 16:20:10 JST
6 nrolland 244 2014-12-26 00:46:32 JST
7 kdxu 244 2014-03-16 16:40:54 JST
8 Rotsor 250 2013-12-28 23:35:45 JST
9 masahiro_sakai 261 2014-11-25 00:24:31 JST
10 Lost_dog_ 283 2013-06-14 00:48:54 JST
11 ikegami__ 753 2013-10-19 08:39:02 JST
12 notogawa 1185 2013-05-29 20:49:06 JST