Skip to content

Instantly share code, notes, and snippets.

@cutsea110

cutsea110/fib.agda

Created December 29, 2017 22:16
Show Gist options
  • Save cutsea110/765160316a01cbdb7acea45a0cdf6464 to your computer and use it in GitHub Desktop.
Save cutsea110/765160316a01cbdb7acea45a0cdf6464 to your computer and use it in GitHub Desktop.
Download ZIP
proof for momoko's hypothesis 1 on http://www.rimse.or.jp/research/pdf/5th/work10.pdf
Raw
fib.agda
module fib where
open import Data.Bool
open import Data.Empty
open import Data.Unit
open import Data.Fin renaming (zero to fzero; suc to fsuc) hiding (_+_)
open import Data.Nat
open import Data.Nat.Properties
open import Data.Nat.DivMod
open import Function
import Relation.Binary.PropositionalEquality as PropEq
open PropEq using (_≡_; refl; subst; cong; sym)
open import Relation.Nullary
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)
fib : ℕ → ℕ
fib (suc (suc n)) = fib (suc n) + fib n
fib n = 1
-- To prove fib is FibFunc
fib-is-FibFunc : FibFunc fib
fib-is-FibFunc zero = Fib0
fib-is-FibFunc (suc zero) = Fib1
fib-is-FibFunc (suc (suc n)) = FibN (fib-is-FibFunc (suc n)) (fib-is-FibFunc n)
toFib : (n : ℕ) → Fib n (fib n)
toFib zero = Fib0
toFib (suc zero) = Fib1
toFib (suc (suc n)) = FibN (toFib (suc n)) (toFib n)
data Parity : ℕ → Set where
even : (k : ℕ) → Parity (k * 2)
odd : (k : ℕ) → Parity (1 + k * 2)
parity : (n : ℕ) → Parity n
parity zero = even zero
parity (suc zero) = odd zero
parity (suc (suc n)) with parity n
... | even k = even (suc k)
... | odd k = odd (suc k)
half : ℕ → ℕ
half n with parity n
half .(k * 2) | even k = k
half .(1 + k * 2) | odd k = k
even? : ℕ → Bool
even? n with parity n
even? .(k * 2) | even k = true
even? .(1 + k * 2) | odd k = false
odd? : ℕ → Bool
odd? n with parity n
odd? .(k * 2) | even k = false
odd? .(1 + k * 2) | odd k = true
isTrue : Bool → Set
isTrue false = ⊥
isTrue true = ⊤
isFalse : Bool → Set
isFalse false = ⊥
isFalse true = ⊤
IsEven : ℕ → Set
IsEven = isTrue ∘ even?
IsOdd : ℕ → Set
IsOdd = isTrue ∘ odd?
even→¬odd : ∀ n → IsEven n → ¬ IsOdd n
even→¬odd n p with parity n
even→¬odd .(k * 2) p | even k = id
even→¬odd .(1 + k * 2) p | odd k = const p
odd→¬even : ∀ n → IsOdd n → ¬ IsEven n
odd→¬even n p with parity n
odd→¬even .(k * 2) p | even k = const p
odd→¬even .(1 + k * 2) p | odd k = id
lemma : {m n : ℕ} → (P : ℕ → Set) → m ≡ n → P m → P n
lemma P refl q = q
data Inspect {A : Set}(x : A) : Set where
_with-≡_ : (y : A) → x ≡ y → Inspect x
inspect : {A : Set}(x : A) → Inspect x
inspect x = x with-≡ refl
step-even : ∀ n → IsEven n → IsEven (suc (suc n))
step-even n p with parity n
step-even .(k * 2) tt | even k = tt
step-even .(suc (k * 2)) () | odd k
pets-even : ∀ n → IsEven (suc (suc n)) → IsEven n
pets-even n p with parity n
pets-even .(k * 2) p | even k = tt
pets-even .(suc (k * 2)) () | odd k
step-odd : ∀ n → IsOdd n → IsOdd (suc (suc n))
step-odd n p with parity n
step-odd .(k * 2) () | even k
step-odd .(suc (k * 2)) tt | odd k = tt
pets-odd : ∀ n → IsOdd (suc (suc n)) → IsOdd n
pets-odd n p with parity n
pets-odd .(k * 2) () | even k
pets-odd .(suc (k * 2)) tt | odd k = tt
trivEven : ∀ k → IsEven (k * 2)
trivEven zero = tt
trivEven (suc zero) = tt
trivEven (suc (suc k)) = step-even (suc (suc (k * 2))) (trivEven (suc k))
trivOdd : ∀ k → IsOdd (1 + k * 2)
trivOdd zero = tt
trivOdd (suc zero) = tt
trivOdd (suc (suc k)) = step-odd (suc (suc (suc (k * 2)))) (trivOdd (suc k))
triv¬Even : ∀ k → ¬ IsEven (1 + k * 2)
triv¬Even zero = id
triv¬Even (suc k) = odd→¬even (suc (suc (suc (k * 2)))) (step-odd (suc (k * 2)) (trivOdd k))
triv¬Odd : ∀ k → ¬ IsOdd (k * 2)
triv¬Odd zero = id
triv¬Odd (suc k) = even→¬odd (suc (suc (k * 2))) (step-even (k * 2) (trivEven k))
next-even-is-odd : ∀ n → IsEven n → IsOdd (suc n)
next-even-is-odd n p with parity n
next-even-is-odd .(k * 2) tt | even k = trivOdd k
next-even-is-odd .(suc (k * 2)) () | odd k
prev-even-is-odd : ∀ n → IsEven (suc n) → IsOdd n
prev-even-is-odd n p with parity n
prev-even-is-odd .(k * 2) p | even k = triv¬Even k p
prev-even-is-odd .(suc (k * 2)) p | odd k = tt
next-odd-is-even : ∀ n → IsOdd n → IsEven (suc n)
next-odd-is-even n p with parity n
next-odd-is-even .(k * 2) () | even k
next-odd-is-even .(suc (k * 2)) tt | odd k = step-even (k * 2) (trivEven k)
even-comm : ∀ m n → IsEven (m + n) → IsEven (n + m)
even-comm m n p = lemma IsEven (+-comm m n) p
odd-comm : ∀ m n → IsOdd (m + n) → IsOdd (n + m)
odd-comm m n p = lemma IsOdd (+-comm m n) p
even+even=even : ∀ m n → IsEven m → IsEven n → IsEven (m + n)
even+even=even zero zero p q = tt
even+even=even zero (suc n) p q = q
even+even=even (suc m) zero p tt = lemma IsEven (cong suc (+-comm zero m)) p
even+even=even (suc zero) (suc zero) p q = tt
even+even=even (suc zero) (suc (suc n)) () q
even+even=even (suc (suc m)) (suc zero) p ()
even+even=even (suc (suc m)) (suc (suc n)) p q
= step-even (m + suc (suc n)) (even+even=even m (suc (suc n)) (pets-even m p) q)
odd+odd=even : ∀ m n → IsOdd m → IsOdd n → IsEven (m + n)
odd+odd=even zero zero () q
odd+odd=even zero (suc n) () q
odd+odd=even (suc m) zero p ()
odd+odd=even (suc zero) (suc zero) tt tt = tt
odd+odd=even (suc zero) (suc (suc n)) tt q = next-odd-is-even (suc (suc n)) q
odd+odd=even (suc (suc m)) (suc zero) p tt
= next-odd-is-even (suc (m + 1)) (lemma IsOdd (cong suc (+-comm 1 m)) p)
odd+odd=even (suc (suc m)) (suc (suc n)) p q
= step-even (m + suc (suc n)) (odd+odd=even m (suc (suc n)) (pets-odd m p) q)
odd+even=odd : ∀ m n → IsOdd m → IsEven n → IsOdd (m + n)
odd+even=odd zero zero () q
odd+even=odd zero (suc n) () q
odd+even=odd (suc m) zero p tt = lemma IsOdd (cong suc (+-comm zero m)) p
odd+even=odd (suc zero) (suc zero) p ()
odd+even=odd (suc zero) (suc (suc n)) tt q = next-even-is-odd (suc (suc n)) q
odd+even=odd (suc (suc m)) (suc zero) p ()
odd+even=odd (suc (suc m)) (suc (suc n)) p q
= step-odd (m + suc (suc n)) (odd+even=odd m (suc (suc n)) (pets-odd m p) q)
even+odd=odd : ∀ m n → IsEven m → IsOdd n → IsOdd (m + n)
even+odd=odd m n p q = odd-comm n m (odd+even=odd n m q p)
-- Momoko's Hypothesis 1
momoko-lemma0 : ∀ k → IsOdd (fib (k * 3))
momoko-lemma1 : ∀ k → IsOdd (fib (1 + k * 3))
momoko-lemma2 : ∀ k → IsEven (fib (2 + k * 3))
momoko-lemma0 zero = tt
momoko-lemma0 (suc n)
= even+odd=odd (fib (suc (n * 3)) + fib (n * 3))
(fib (suc (n * 3)))
(odd+odd=even (fib (suc (n * 3)))
(fib (n * 3))
(momoko-lemma1 n)
(momoko-lemma0 n))
(momoko-lemma1 n)
momoko-lemma1 zero = tt
momoko-lemma1 (suc n)
= odd+even=odd (fib (suc (n * 3)) + fib (n * 3) + fib (suc (n * 3)))
(fib (suc (n * 3)) + fib (n * 3))
(even+odd=odd (fib (suc (n * 3)) + fib (n * 3))
(fib (suc (n * 3)))
(odd+odd=even (fib (suc (n * 3)))
(fib (n * 3))
(momoko-lemma1 n)
(momoko-lemma0 n))
(momoko-lemma1 n))
(odd+odd=even (fib (suc (n * 3)))
(fib (n * 3))
(momoko-lemma1 n)
(momoko-lemma0 n))
momoko-lemma2 n = odd+odd=even (fib (suc (n * 3)))
(fib (n * 3))
(momoko-lemma1 n)
(momoko-lemma0 n)
momoko-hypothesis-1 : ∀ k → IsEven (fib (2 + k * 3))
momoko-hypothesis-1 = momoko-lemma2
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment