------------------------------------------------------------------------
-- An example: A function that, given a stream, tries to find an
-- element satisfying a predicate
------------------------------------------------------------------------

{-# OPTIONS --without-K #-}

module Search where

open import Equality.Propositional
open import Interval using (⟨ext⟩)
open import Prelude hiding ()

open import Univalence-axiom equality-with-J

open import Partiality-algebra.Monotone

-- Streams.

infixr 5 _∷_

record Stream {a} (A : Set a) : Set a where
coinductive
constructor _∷_
field
tail : Stream A

open Stream

-- A direct implementation of the function.

module Direct {a} {A : Set a} (q : A  Bool) where

Φ : Trans (Stream A)  _  A)
Φ f xs = if q (head xs) then return (head xs) else f (tail xs)

Φ-monotone :
{f₁ f₂}  (∀ xs  f₁ xs  f₂ xs)   xs  Φ f₁ xs  Φ f₂ xs
Φ-monotone f₁⊑f₂ xs with q (head xs)
... | true  = return (head xs)
... | false = f₁⊑f₂ (tail xs)

Φ-⊑ : Trans-⊑ (Stream A)  _  A)
Φ-⊑ = record { function = Φ; monotone = Φ-monotone }

search : Stream A  A
search = fix→ Φ-⊑

search-least :
f  (∀ xs  Φ f xs  f xs)
xs  search xs  f xs
search-least = fix→-is-least Φ-⊑

Φ-ω-continuous :
(s :  λ (f :   Stream A  A )
n xs  f n xs  f (suc n) xs)
Φ (  at s)    at [ Φ-⊑ \$ s ]-inc
Φ-ω-continuous s = ⟨ext⟩ helper
where
helper :  xs  Φ (  at s) xs   (at [ Φ-⊑ \$ s ]-inc xs)
helper xs with q (head xs)
... | true  = return (head xs)               ≡⟨ sym ⨆-const ⟩∎
... | false =  (at s (tail xs))

Φ-ω : Trans-ω (Stream A)  _  A)
Φ-ω = record
{ monotone-function = Φ-⊑
; ω-continuous      = Φ-ω-continuous
}

search-fixpoint : search  Φ search
search-fixpoint = fix→-is-fixpoint-combinator Φ-ω

-- An arguably more convenient implementation, with the potential
-- drawback that one of the lemmas depends on propositional
-- extensionality.

module Indirect {a} {A : Set a} (q : A  Bool) where

ΦP : Stream A  Partial (Stream A)  _  A) A
ΦP xs =
else
rec (tail xs)

Φ : Trans (Stream A)  _  A)
Φ = Trans-⊑.function (transformer ΦP)

search : Stream A  A
search = fixP ΦP

search-least :
f  (∀ xs  Φ f xs  f xs)
xs  search xs  f xs
search-least = fixP-is-least ΦP

search-fixpoint :
Propositional-extensionality a
search  Φ search
search-fixpoint prop-ext = fixP-is-fixpoint-combinator prop-ext ΦP