Martin Escardo, 20-21 December 2012.

This module is mainly for use in the module SearchableOrdinals.lagda.

\begin{code}

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

module LexicographicSearch where

open import Two
open import CurryHoward
open import Equality
open import SetsAndFunctions
open import LexicographicOrder
open import InfSearchable

sums-preserve-inf-searchability : {X : Set} → {Y : X → Set}
→ (R : bin-rel X) → (S : (x : X) → bin-rel(Y x))
→ inf-searchable X R → (∀(x : X) → inf-searchable(Y x)(S x)) → inf-searchable(Σ \(x : X) → Y x)(lex-prod R S)
sums-preserve-inf-searchability {X} {Y} R S ε δ p = ∃-intro (x₀ , y₀) (∧-intro putative-root-lemma
(∧-intro lower-bound-lemma
uborlb-lemma))
where
lemma-next : ∀(x : X) → ∃ \(y₀ : Y x) → ((∃ \(y : Y x) → p(x , y) ≡ ₀) → p (x , y₀) ≡ ₀)
∧ (∀  (y : Y x) → p(x , y) ≡ ₀ → S x y₀ y)
∧ (∀ l → (∀ (y : Y x) → p(x , y) ≡ ₀ → S x l y) → S x l y₀)
lemma-next x = δ x (λ y → p(x , y))

next : (x : X) → Y x
next x = ∃-witness(lemma-next x)

next-correctness : ∀(x : X) → ((∃ \(y : Y x) → p(x , y) ≡ ₀) → p (x , next x) ≡ ₀)
∧ (∀(y : Y x) → p(x , y) ≡ ₀ → S x (next x) y)
∧ (∀(l : Y x) → (∀(y : Y x) → p(x , y) ≡ ₀ → S x l y) → S x l (next x))
next-correctness x = ∃-elim(lemma-next x)

lemma-first : ∃ \(x₀ : X) → ((∃ \(x : X) → p(x , next x) ≡ ₀) → p (x₀ , next x₀) ≡ ₀)
∧ (∀(x : X) → p(x , next x) ≡ ₀ → R x₀ x)
∧ (∀(m : X) → (∀ x → p(x , next x) ≡ ₀ → R m x) → R m x₀)
lemma-first = ε(λ x → p(x , next x))

x₀ : X
x₀ = ∃-witness lemma-first

first-correctness : ((∃ \(x : X) → p(x , next x) ≡ ₀) → p (x₀ , next x₀) ≡ ₀)
∧ (∀(x : X) → p(x , next x) ≡ ₀ → R x₀ x)
∧ (∀ m → (∀ x → p(x , next x) ≡ ₀ → R m x) → R m x₀)
first-correctness = ∃-elim lemma-first

y₀ : Y x₀
y₀ = next x₀

putative-root-lemma : (∃ \(t : (Σ \(x : X) → Y x)) → p t ≡ ₀) → p(x₀ , y₀) ≡ ₀
putative-root-lemma ((x , y) , r) = ∧-elim₀ first-correctness (x , ∧-elim₀(next-correctness x) (y , r))

lower-bound-lemma : ∀(t : (Σ \(x : X) → Y x)) → p t ≡ ₀ → lex-prod R S (x₀ , y₀) t
lower-bound-lemma (x , y) r = ∧-intro R-lemma S-lemma
where
f : p(x , next x) ≡ ₀ → R x₀ x
f = ∧-elim₀(∧-elim₁ first-correctness) x
R-lemma : R x₀ x
R-lemma = f(∧-elim₀(next-correctness x)(y , r))
g : S x (next x) y
g = ∧-elim₀(∧-elim₁(next-correctness x)) y r
j : ∀ {x₀ x : X} → (r : x₀ ≡ x) → ∀{y : Y x}
→ S x (next x) y → S x₀ (next x₀) (subst {X} {Y} (sym r) y)
j = J (λ x₀ x r → ∀{y : Y x} → S x (next x) y → S x₀ (next x₀) (subst {X} {Y} (sym r) y)) (λ r → id)
S-lemma : (r : x₀ ≡ x) → S x₀ y₀ (subst {X} {Y} (sym r) y)
S-lemma r = j r g

uborlb-lemma : ∀ n → (∀(t : (Σ \(x : X) → Y x)) → p t ≡ ₀ → lex-prod R S n t) → lex-prod R S n (x₀ , y₀)
uborlb-lemma (x , y) lower-bounder = ∧-intro R-lemma S-lemma
where
f : (∀ x' → p(x' , next x') ≡ ₀ → R x x') → R x x₀
f = ∧-elim₁(∧-elim₁ first-correctness) x
R-lower-bounder : ∀(x' : X)(y' : Y x') → p(x' , y') ≡ ₀ → R x x'
R-lower-bounder x' y' r' = π₀(lower-bounder ((x' , y')) r')
R-lemma : R x x₀
R-lemma = f(λ x' → R-lower-bounder x' (next x'))
g :  (∀(y' : Y x) → p(x , y') ≡ ₀ → S x y y') → S x y (next x)
g = ∧-elim₁(∧-elim₁(next-correctness x)) y
S-lower-bounder : ∀(x' : X)(y' : Y x') → p(x' , y') ≡ ₀ → ∀(r : x ≡ x') → S x y (subst (sym r) y')
S-lower-bounder x' y' r' = π₁(lower-bounder ((x' , y')) r')
j : ∀ {x x₀ : X} → (r : x ≡ x₀) → ∀{y : Y x}
→ S x y (next x) → S x y (subst {X} {Y} (sym r) (next x₀))
j = J (λ x x₀ r → ∀{y : Y x} → S x y (next x) → S x y (subst {X} {Y} (sym r) (next x₀))) (λ r → id)
S-lemma : ∀(r : x ≡ x₀) → S x y (subst {X} {Y} (sym r) y₀)
S-lemma r = j r (g(λ y' r → S-lower-bounder x y' r refl))

\end{code}