```------------------------------------------------------------------------
-- 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 Monad equality-with-J
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 ⟩∎
⨆ (constˢ (return (head xs)))  ∎
... | 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 =
if q (head xs) then
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
```