{-# OPTIONS --safe #-}
open import Level
open import Data.Nat hiding (_⊔_)
open import Data.Product
open import Function.Base
open import Data.Unit
open import Data.Empty
open import Data.Nat.Properties
open import Agda.Builtin.Equality
open import Data.List
open import Data.List.Properties
import Data.List.Relation.Binary.Pointwise as List
open import Relation.Binary
open import Relation.Binary.PropositionalEquality.Core
open import Relation.Binary.PropositionalEquality.Properties
open import Data.List.Relation.Binary.Prefix.Heterogeneous using (Prefix)
import Data.List.Relation.Binary.Prefix.Heterogeneous as Pref
import Data.List.Relation.Binary.Prefix.Heterogeneous.Properties as Pref
open import Relation.Unary as Unary
open import Relation.Nullary
module ListBisect {a : Level} {A : Set a} where
_⊑_ : REL (List A) (List A) a
_⊑_ = Pref.Prefix _≡_
Prefix-Closed : {p : Level} (P : List A → Set p) → Set _
Prefix-Closed P = ∀ {w} → P w → ∀ {v} → v ⊑ w → P v
record PrefixWith {p : Level} (P : List A → Set p) (w : List A) : Set (p ⊔ a) where
field
v : List A
is-prefix : v ⊑ w
has-prop : P v
suffix : Σ[ s ∈ List A ] v ++ s ≡ w
suffix = case (Pref.toView is-prefix) of λ
{ (v∼cs Pref.++ u) →
u , cong (λ - → - ++ u) (List.Pointwise-≡⇒≡ v∼cs)
}
record LongestPrefixWith {p : Level} (P : List A → Set p) (w : List A) : Set (p ⊔ a) where
field
is-prefix-with : PrefixWith P w
open PrefixWith is-prefix-with public
field
is-longest : ∀ (other : PrefixWith P w) → (PrefixWith.v other) ⊑ v
bound-LongestPrefixWith : {p : Level} {P : List A → Set p} { x : A } {w : List A}
→ Prefix-Closed P
→ ¬ (P [ x ])
→ (pref : PrefixWith P (x ∷ w))
→ (PrefixWith.v pref) ⊑ []
bound-LongestPrefixWith {x = x} {w = w} pref-closed ¬P[x]
record { v = [] ; is-prefix = Prefix.[] ; has-prop = _ } = Prefix.[]
bound-LongestPrefixWith {x = x} {w = w} pref-closed ¬P[x]
record { v = (.x ∷ v) ; is-prefix = (refl Prefix.∷ v⊑w) ; has-prop = has-prop } =
⊥-elim (¬P[x] (pref-closed {x ∷ v} has-prop (refl Prefix.∷ Prefix.[])))
find-LongestPrefixWith : {p : Level} {P : List A → Set p}
→ P []
→ Prefix-Closed P
→ Unary.Decidable P
→ (w : List A) → LongestPrefixWith P w
find-LongestPrefixWith P[] pref-closed dec [] =
record
{ is-prefix-with = record
{ v = []
; is-prefix = Prefix.[]
; has-prop = P[]
}
; is-longest = λ { record { v = [] ; is-prefix = Prefix.[] ; has-prop = _ } → Prefix.[] }
}
find-LongestPrefixWith {p} {P} P[] pref-closed dec (x List.∷ w) with (dec [ x ])
... | (no ¬P[x]) = record
{ is-prefix-with = record { v = [] ; is-prefix = Prefix.[] ; has-prop = P[] }
; is-longest = bound-LongestPrefixWith pref-closed ¬P[x] }
... | (yes P[x]) = record
{ is-prefix-with = record
{ v = x ∷ lp.v
; is-prefix = refl Prefix.∷ lp.is-prefix
; has-prop = lp.has-prop }
; is-longest = λ
{ record
{ v = []
; is-prefix = _
; has-prop = _
} → Prefix.[]
; record
{ v = (.x ∷ v)
; is-prefix = (refl Prefix.∷ v⊑w)
; has-prop = Pxv
} → refl Prefix.∷ (lp.is-longest (record { v = v ; is-prefix = v⊑w ; has-prop = Pxv }))
}
}
where
Px : List A → Set p
Px suffix = P (x ∷ suffix)
Px-pref-closed : Prefix-Closed Px
Px-pref-closed {w} Pxw {v} v⊑w = pref-closed {x ∷ w} Pxw (refl Prefix.∷ v⊑w)
dec-Px : Unary.Decidable Px
dec-Px v = (dec (x ∷ v))
lp : LongestPrefixWith Px w
lp = find-LongestPrefixWith P[x] Px-pref-closed dec-Px w
module lp = LongestPrefixWith lp
record List≤2^ (n : ℕ) : Set a where
field
toList : List A
len≤2^ : length toList ≤ 2 ^ n
2^n+1 : ∀ n → 2 ^ (1 + n) ≡ 2 ^ n + 2 ^ n
2^n+1 n = begin
2 ^ (ℕ.suc n) ≡⟨⟩
2 * (2 ^ n) ≡⟨⟩
2 ^ n + (2 ^ n + 0) ≡⟨ cong (λ - → 2 ^ n + -) (+-identityʳ _) ⟩
2 ^ n + 2 ^ n
∎
where open ≡-Reasoning
IsNonEmpty : List A → Set 0ℓ
IsNonEmpty [] = ⊥
IsNonEmpty (_ ∷ _) = ⊤
record Bisected (n : ℕ) (l : List≤2^ (1 + n)) : Set a where
field
first : List≤2^ n
second : List≤2^ n
module l = List≤2^ l
module first = List≤2^ first
module second = List≤2^ second
field
concatted : l.toList ≡ first.toList ++ second.toList
non-empty : IsNonEmpty l.toList → IsNonEmpty first.toList
n⊓m≤n : ∀ m n → n ⊓ m ≤ n
n⊓m≤n ℕ.zero ℕ.zero = z≤n
n⊓m≤n (ℕ.suc _) ℕ.zero = z≤n
n⊓m≤n ℕ.zero (ℕ.suc _) = z≤n
n⊓m≤n (ℕ.suc n) (ℕ.suc m) = s≤s (n⊓m≤n n m)
2^n≥1 : ∀ n → ∃[ m ] (2 ^ n ≡ 1 + m)
2^n≥1 ℕ.zero = 0 , refl
2^n≥1 (ℕ.suc n) rewrite (2^n+1 n) =
let m , 2^n≡1+m = 2^n≥1 n in
(m + 2 ^ n) , (begin
2 ^ n + 2 ^ n ≡⟨ cong (λ - → 2 ^ n + -) 2^n≡1+m ⟩
2 ^ n + (1 + m) ≡⟨ +-comm (2 ^ n) (1 + m) ⟩
1 + m + 2 ^ n ≡⟨ +-assoc 1 m (2 ^ n) ⟩
ℕ.suc (m + 2 ^ n)
∎)
where
open ≡-Reasoning
cut-in-halves : ∀ n (l : List≤2^ (1 + n)) → Bisected n l
cut-in-halves n l = record
{ first = record
{ toList = first
; len≤2^ =
let open ≤-Reasoning in
begin
length first ≡⟨ length-take 2^n l.toList ⟩
2 ^ n ⊓ length l.toList ≤⟨ n⊓m≤n _ _ ⟩
2 ^ n
∎
}
; second = record
{ toList = drop 2^n l.toList
; len≤2^ =
let open ≤-Reasoning in
begin
length (drop 2^n l.toList) ≡⟨ length-drop 2^n _ ⟩
length l.toList ∸ 2^n ≤⟨ ∸-monoˡ-≤ 2^n l.len≤2^ ⟩
2 ^ (1 + n) ∸ 2^n ≡⟨ cong (λ - → - ∸ 2 ^ n) (2^n+1 n) ⟩
2 ^ n + 2 ^ n ∸ (2 ^ n) ≡⟨ m+n∸n≡m 2^n 2^n ⟩
2 ^ n
∎
}
; concatted = sym (take++drop≡id (2 ^ n) _)
; non-empty = non-empty
}
where
module l = List≤2^ l
2^n = 2 ^ n
first = take 2^n l.toList
non-empty : IsNonEmpty l.toList → IsNonEmpty first
non-empty x with l.toList
non-empty _ | _ ∷ _ rewrite (proj₂ (2^n≥1 n)) = tt