Fast search

Search.agda

module _ where

open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
open import Data.Nat hiding (_<_; _≤_) renaming (_<′_ to _<_; _≤′_ to _≤_)
open import Data.Nat.Properties
open import Data.Nat.Properties.Simple
open import Data.Product
open import Data.Empty
open import Function
open ≡-Reasoning

infix 1 NoBelow
syntax NoBelow (λ z → P) n = No z Below n SuchThat P
NoBelow : ∀ {ℓ} → (ℕ → Set ℓ) → ℕ → Set ℓ
NoBelow P n = ∀ z → z < n → ¬ P z

belowSuc : ∀ {ℓ} (P : ℕ → Set ℓ) n → ¬ P n →
           No z Below n     SuchThat P z →
           No z Below suc n SuchThat P z
belowSuc P n !p below .n ≤′-refl pz = !p pz
belowSuc P n !p below z (≤′-step z<sn) pz = below z z<sn pz

≤-wk : ∀ {a b} → suc a ≤ b → a ≤ b
≤-wk ≤′-refl        = ≤′-step ≤′-refl
≤-wk (≤′-step sa≤b) = ≤′-step (≤-wk sa≤b)

<′-trans : ∀ {a b c} → a < b → b < c → a < c
<′-trans a<b b<c = ≤⇒≤′ (<-trans (≤′⇒≤ a<b) (≤′⇒≤ b<c))

<⇒≤ : ∀ {a b} → a < b → a ≤ b
<⇒≤ ≤′-refl = ≤′-step ≤′-refl
<⇒≤ (≤′-step a<b) = ≤′-step (<⇒≤ a<b)

lem-minus : ∀ a b → a < b → b ∸ a + a ≡ b
lem-minus a b a<b =
  begin
    b ∸ a + a
  ≡⟨ +-comm (b ∸ a) _ ⟩
    a + (b ∸ a)
  ≡⟨ m+n∸m≡n {a} (≤′⇒≤ (<⇒≤ a<b)) ⟩
    b
  ∎

lem-loop : ∀ {a} → a < a → ⊥
lem-loop {zero} ()
lem-loop {suc a} (≤′-step a<a) = lem-loop (≤-wk a<a)

lem-squeeze : ∀ {a b} → a < b → b < suc a → ⊥
lem-squeeze ≤′-refl (≤′-step b<sa) = lem-loop (≤-wk b<sa)
lem-squeeze (≤′-step a<b) b<sa = lem-squeeze a<b (≤-wk b<sa)

<-antisym : ∀ {a b} → a < b → b ≤ a → ⊥
<-antisym a<b b≤a = lem-squeeze a<b (s≤′s b≤a)

module _ {ℓ} (P : ℕ → Set ℓ) (P? : ∀ n → Dec (P n))
         (bound : ∀ n → ∃ λ y → n < y × P y) where

  Goal : ℕ → Set ℓ
  Goal n = ∃ λ y → n < y × P y × (No z Below y SuchThat n < z × P z)

  goSlow : ∀ {lo} c n → lo < n → (y : ℕ) → lo < y × P y → c + n ≡ y →
             No z Below n SuchThat lo < z × P z → Goal lo
  goSlow zero n lo<n _ (_ , py) refl minimal = n , lo<n , py , minimal
  goSlow (suc c) n lo<n y py eq minimal =
    case P? n of λ
    { (yes p) → n , lo<n , p , minimal
    ; (no !p) → goSlow c (suc n) (≤′-step lo<n) y py (trans (+-suc c n) eq)
                        (belowSuc (λ z → _ < z × P z) n (!p ∘ proj₂) minimal) }

  goFast : ℕ → ∀ {lo} n → lo < n → No z Below n SuchThat lo < z × P z → Goal lo
  goFast 0 n lo<n minimal =
    case bound n of λ
    { (y , n<y , py) → goSlow (y ∸ n) n lo<n y (<′-trans lo<n n<y , py)
                               (lem-minus n y n<y) minimal }
  goFast (suc fuel) n lo<n minimal =
    case P? n of λ
    { (yes p) → n , lo<n , p , minimal
    ; (no !p) → goFast fuel (suc n) (≤′-step lo<n)
                        (belowSuc (λ z → _ < z × P z) n (!p ∘ proj₂) minimal) }

  search : (n : ℕ) → Goal n
  search n = goFast 1000000000 (suc n) ≤′-refl λ { z z<n (n<z , _) → <-antisym z<n n<z }

  searchSlow : (n : ℕ) → Goal n
  searchSlow n = case bound (suc n) of λ
    { (y , n<y , py) → goSlow (y ∸ suc n) (suc n) ≤′-refl y (≤-wk n<y , py)
                               (lem-minus (suc n) y n<y)
                               (λ { z z<sn (n<z , _) → lem-squeeze n<z z<sn })
    }

K = 100

P : ℕ → Set
P n = n ≥ K

P? : ∀ n → Dec (P n)
P? n = K ≤? n

slow′ : ℕ → ℕ → ℕ → ℕ
slow′ a zero zero = a
slow′ a zero (suc n) = slow′ (suc a) n n
slow′ a (suc c) n = slow′ (suc a) c n

slow : ℕ → ℕ
slow zero = slow′ 0 500 500
slow n    = slow′ n 500 500

open DecTotalOrder decTotalOrder using (reflexive) renaming (trans to _⟨≤⟩_)

bound : ∀ n → ∃ λ y → n < y × P y
bound n = suc n + (slow n + 100)
        , ≤⇒≤′ (m≤m+n (suc n) (slow n + 100))
        , n≤m+n (suc n + slow n) 100 ⟨≤⟩ reflexive (+-assoc (suc n) _ _)

test : ℕ → ℕ
test n = proj₁ (search P P? bound n)

testSlow : ℕ → ℕ
testSlow n = proj₁ (searchSlow P P? bound n)

-- test 50     :   103ms
-- testSlow 50 : 1,645ms