problem1.agda

module problem1 where

-- solution to https://coq-math-problems.github.io/Problem1/
-- 
-- sadly mine is the longest one
-- see https://www.reddit.com/r/Coq/comments/6amhkb/starting_a_problemoftheweek_blog_for_coq/

open import Data.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

Decreasing : (f : ℕ → ℕ) → Set
Decreasing f = ∀ n → f (suc n) ≤ f n

Valley : ℕ → (ℕ → ℕ) → Set
Valley w f = ∃ λ m → ∃ λ l → ∀ k → k ≤ w → f (m + k) ≡ l

Induction : (P : ℕ → Set) → P zero → (∀ n → P n → P (suc n)) → ∀ n → P n
Induction P z s zero = z
Induction P z s (suc n) = Induction (λ z₁ → P (suc z₁)) (s zero z) (λ n₁ → s (suc n₁)) n

leq-and-neq-give-less : ∀ x y → x ≤ y → ¬ (x ≡ y) → x < y
leq-and-neq-give-less .0 zero z≤n neq = ⊥-elim (neq refl)
leq-and-neq-give-less .0 (suc y) z≤n neq = s≤s z≤n
leq-and-neq-give-less .(suc _) .(suc _) (s≤s leq) neq =
   s≤s (leq-and-neq-give-less _ _ leq (λ { refl → neq refl }))

zero-right-identity : ∀ (m : ℕ) → m + 0 ≡ m
zero-right-identity zero = refl
zero-right-identity (suc m) = cong suc (zero-right-identity m)

helper1 : ∀ (f : ℕ → ℕ) → (m : ℕ) → (l : ℕ) → f m ≡ l → f (m + 0) ≡ l
helper1 f m .(f m) refl = cong f (zero-right-identity m)

move-succ : ∀ (m k : ℕ) → m + suc k ≡ suc (m + k)
move-succ zero k = refl
move-succ (suc m) k = cong suc (move-succ m k)

leq-remove-succ : ∀ k w → suc k ≤ suc w → k ≤ w
leq-remove-succ k w (s≤s leq) = leq

checkValley : 
  (f : ℕ → ℕ) → Decreasing f
  → (width : ℕ)
  → (level : ℕ)
  → (m : ℕ)
  → f m ≡ level
  → (∀ k → k ≤ width → f (m + k) ≡ level) ⊎ (∃ λ m' → f m' < level)
checkValley f d zero l m eq = inj₁ (λ k → λ { z≤n →  helper1 f m l eq})
checkValley f d (suc w) l m eq with f (suc m) ≟ l
checkValley f d (suc w) l m eq | Dec.yes p with checkValley f d w l (suc m) p
checkValley f d (suc w) l m eq | yes p | (inj₁ rest-flat) =
  inj₁ (λ {
    zero → λ x₁ → helper1 f m l eq
  ; (suc k) → λ in-range →
    trans (cong f (move-succ m k)) (rest-flat k (leq-remove-succ k w in-range))})
checkValley f d (suc w) l m eq | yes p | (inj₂ y) = inj₂ y
checkValley f d (suc w) l m eq | Dec.no ¬p =
 inj₂ ((suc m) , leq-and-neq-give-less (f (suc m)) l (subst (λ q → f (suc m) ≤ q) eq (d m)) ¬p)

findValley :
  (f : ℕ → ℕ) → Decreasing f
  → (width : ℕ)
  → (level : ℕ)
  → (∀ level' → level' < level → (n : ℕ) → f n ≡ level' → Valley width f)
  → (n : ℕ) → f n ≡ level → Valley width f
findValley f d w l rec n eq with checkValley f d w l n eq
findValley f d w l rec n eq | inj₁ x = n , l , x
findValley f d w 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 → ∀ w → Valley w f
theorem f decreasing w = Induction'' _ (findValley f decreasing w) (f 0) 0 refl