Skip to content

Instantly share code, notes, and snippets.

@UlfNorell
Created March 29, 2016 08:16
Show Gist options
  • Save UlfNorell/f2d8674b1d6b98172827 to your computer and use it in GitHub Desktop.
Save UlfNorell/f2d8674b1d6b98172827 to your computer and use it in GitHub Desktop.
Fast search
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment