Skip to content

Instantly share code, notes, and snippets.

@Rotsor
Created May 21, 2017 17:32
Show Gist options
  • Save Rotsor/09540971f7b0874755526e0e0ce235bc to your computer and use it in GitHub Desktop.
Save Rotsor/09540971f7b0874755526e0e0ce235bc to your computer and use it in GitHub Desktop.
module problem2 where
-- see https://np.reddit.com/r/DailyProver/comments/6brksy/infinite_valleys_and_the_limited_principle_of/
open import Data.Nat as Nat
import Data.Nat.Properties as NatProp
open import Data.Sum
open import Data.Product
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
open import Data.Empty
open import Data.Bool
open import Relation.Binary
open DecTotalOrder Nat.decTotalOrder using () renaming (refl to ≤-refl; trans to ≤-trans)
Decreasing : (f : ℕ → ℕ) → Set
Decreasing f = ∀ n → f (suc n) ≤ f n
LPO = (f : ℕ → Bool) → ∃ (λ x → f x ≡ true) ⊎ ∀ x → f x ≡ false
Infinite-Valley : (ℕ → ℕ) → Set
Infinite-Valley f = ∃ λ m → ∃ λ l → ∀ k → f (m + k) ≡ l
_↔_ : (A B : Set) → Set
A ↔ B = (A → B) × (B → A)
lpo-dec : ∀ {P Q : ℕ → Set} → (∀ n → P n ⊎ Q n) → LPO → (∀ n → P n) ⊎ ∃ (λ n → Q n)
lpo-dec {P} {Q} dec lpo = hoho where
sum-to-bool : ∀ {A B : Set} → A ⊎ B → Bool
sum-to-bool (inj₁ _) = false
sum-to-bool (inj₂ _) = true
p : ℕ → Bool
p n = sum-to-bool (dec n)
extract-inj₂ : ∀ {A B : Set} → (x : A ⊎ B) → sum-to-bool x ≡ true → B
extract-inj₂ (inj₁ x) ()
extract-inj₂ (inj₂ y) eq = y
extract-inj₁ : ∀ {A B : Set} → (x : A ⊎ B) → sum-to-bool x ≡ false → A
extract-inj₁ (inj₂ x) ()
extract-inj₁ (inj₁ y) eq = y
hoho : (∀ n → P n) ⊎ ∃ (λ n → Q n)
hoho with lpo p
hoho | inj₁ (n , is-true) = inj₂ (n , extract-inj₂ (dec n) is-true)
hoho | inj₂ is-false = inj₁ (λ n → extract-inj₁ (dec n) (is-false n))
decreasing-antitone : ∀ a b → a ≤′ b → ∀ f → Decreasing f → f b ≤ f a
decreasing-antitone a .a ≤′-refl f d = ≤-refl
decreasing-antitone a .(suc _) (≤′-step leq) f d = ≤-trans (d _) (decreasing-antitone a _ leq f d)
leq-is-eq-or-less : ∀ x y → x ≤′ y → x ≡ y ⊎ x < y
leq-is-eq-or-less x .x ≤′-refl = inj₁ refl
leq-is-eq-or-less x .(suc _) (≤′-step leq) = inj₂ (s≤s (NatProp.≤′⇒≤ leq))
≤-refl' : ∀ {a b} → a ≡ b → a ≤ b
≤-refl' refl = ≤-refl
lemma0 : ∀ x n → x ≤ x + n
lemma0 zero x = z≤n
lemma0 (suc n) x = s≤s (lemma0 n x)
checkValley :
LPO →
(f : ℕ → ℕ) → Decreasing f
→ (level : ℕ)
→ (m : ℕ)
→ f m ≡ level
→ (∀ k → f (m + k) ≡ level) ⊎ (∃ λ m' → f m' < level)
checkValley lpo f d level m eq with lpo-dec {λ k → f (m + k) ≡ level} {λ k → f (m + k) < level} (λ n → leq-is-eq-or-less (f (m + n)) level (NatProp.≤⇒≤′ (≤-trans (decreasing-antitone m (m + n) (NatProp.≤⇒≤′ (lemma0 _ _)) f d) (≤-refl' eq)))) lpo
... | inj₁ l = inj₁ l
... | inj₂ (m' , ll) = inj₂ (m + m' , ll)
module Copy_pasta (lpo : LPO) where
findValley :
(f : ℕ → ℕ) → Decreasing f
→ (level : ℕ)
→ (∀ level' → level' < level → (n : ℕ) → f n ≡ level' → Infinite-Valley f)
→ (n : ℕ) → f n ≡ level → Infinite-Valley f
findValley f d l rec n eq with checkValley lpo f d l n eq
findValley f d l rec n eq | inj₁ x = n , l , x
findValley f d l rec n eq | inj₂ (n' , smaller) = rec (f n') smaller n' refl
Induction' : (P : ℕ → Set) → (∀ n → (∀ n' → n' <′ n → P n') → P n) → ∀ n → (∀ n' → n' <′ n → P n')
Induction' P f zero = λ n' → λ ()
Induction' P f (suc n) n' lss with Induction' P f n
Induction' P f (suc n) .n ≤′-refl | previous = f n previous
Induction' P f (suc n) n' (≤′-step lss) | previous = previous n' lss
Induction'' : (P : ℕ → Set) → (∀ n → (∀ n' → n' < n → P n') → P n) → ∀ n → P n
Induction'' P f n =
Induction' P (λ n rec → f n (λ n' lss → rec n' (NatProp.≤⇒≤′ lss))) (suc n) n (≤′-refl)
theorem : ∀ (f : ℕ → ℕ) → Decreasing f → Infinite-Valley f
theorem f decreasing = Induction'' _ (findValley f decreasing) (f 0) 0 refl
side1 : LPO → (∀ f → Decreasing f → Infinite-Valley f)
side1 lpo = Copy_pasta.theorem lpo
bool-to-nat : Bool → ℕ
bool-to-nat false = 1
bool-to-nat true = 0
side2 : (∀ f → Decreasing f → Infinite-Valley f) → LPO
side2 infinite-valleys p =
rest (infinite-valleys f f-decreasing)
where
g : ℕ → Bool
g zero = false
g (suc n) = p n ∨ g n
f : ℕ → ℕ
f x = bool-to-nat (g x)
f-decreasing : Decreasing f
f-decreasing n with p n
f-decreasing n | false = ≤-refl
f-decreasing n | true = z≤n
f-suc=1-means-f=1 : ∀ x → f (suc x) ≡ 1 → f x ≡ 1
f-suc=1-means-f=1 x eq with p x
f-suc=1-means-f=1 x eq | false = eq
f-suc=1-means-f=1 x () | true
stuff : ∀ x → f x ≡ 1 → ∀ y → y <′ x → p y ≡ false
stuff .(suc y) eq y ≤′-refl with p y
stuff .(suc y) eq y ≤′-refl | false = refl
stuff .(suc y) () y ≤′-refl | true
stuff .(suc _) eq y (≤′-step {n} y<x) =
stuff _ (f-suc=1-means-f=1 _ eq) y y<x
find-true : ∀ x → f x ≡ 0 → ∃ (λ x → p x ≡ true)
find-true zero ()
find-true (suc x) eq with p x | inspect p x
find-true (suc x) eq | false | _ = find-true x eq
find-true (suc x) eq | true | [ eq2 ] = x , eq2
never-more-than-1 : ∀ x l → f x ≡ suc (suc l) → ⊥
never-more-than-1 x l eq with g x
never-more-than-1 x l () | false
never-more-than-1 x l () | true
lemma : ∀ x n → x <′ n + suc x
lemma x zero = ≤′-refl
lemma x (suc n) = ≤′-step (lemma x n)
rest : Infinite-Valley f → ∃ (λ x → p x ≡ true) ⊎ ((x : ℕ) → p x ≡ false)
rest (n , zero , is-valley) = inj₁ (find-true (n + 0) (is-valley 0))
rest (n , suc zero , is-valley) = inj₂ (λ x → stuff (n + suc x) (is-valley (suc x)) x (lemma x n) )
rest (n , suc (suc level) , is-valley) = ⊥-elim (never-more-than-1 (n + 0) _ (is-valley 0))
theorem : LPO ↔ (∀ f → Decreasing f → Infinite-Valley f)
theorem = side1 , side2
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment