Skip to content

Instantly share code, notes, and snippets.

# Rotsor/problem1.agda

Created May 14, 2017 14:50
Show Gist options
• Save Rotsor/ae5b86a944f0fb5b4666d2f01c8c7759 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 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
to join this conversation on GitHub. Already have an account? Sign in to comment