problem2.agda

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