Skip to content

Instantly share code, notes, and snippets.

@Rotsor
Created May 14, 2017 14:50
Show Gist options
  • Save Rotsor/ae5b86a944f0fb5b4666d2f01c8c7759 to your computer and use it in GitHub Desktop.
Save Rotsor/ae5b86a944f0fb5b4666d2f01c8c7759 to your computer and use it in GitHub Desktop.
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment