Martin Escardo, 20-21 December 2012.

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

\begin{code}

{-# OPTIONS --without-K --exact-split --safe #-}

module LexicographicSearch where

open import SpartanMLTT
open import Two
open import LexicographicOrder
open import InfSearchable

sums-preserve-inf-searchability : {X : U} {Y : X  U}
   (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 =
 (x₀ , y₀) , (putative-root-lemma , (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 x)  ((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 = pr₁(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 = pr₂(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 : X)  p(x , next x)    R m x)  R m x₀)
  lemma-first = ε x  p(x , next x))

  x₀ : X
  x₀ = pr₁ 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)  ((x : X)  p(x , next x)    R m x)  R m x₀)
  first-correctness = pr₂ 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) = pr₁ first-correctness (x , pr₁(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 = R-lemma , S-lemma
   where
    φ : {x x' : X}  x  x'  Y x  Y x'
    φ = transport Y
    f : p(x , next x)    R x₀ x 
    f = pr₁(pr₂ first-correctness) x
    R-lemma : R x₀ x 
    R-lemma = f(pr₁(next-correctness x)(y , r))
    g : S x (next x) y
    g = pr₁(pr₂(next-correctness x)) y r
    j : {x₀ x : X} (r : x₀  x) {y : Y x} 
       S x (next x) y  S x₀ (next x₀) (φ (sym r) y)
    j = J  x₀ x r  {y : Y x}  S x (next x) y  S x₀ (next x₀) (φ (sym r) y))  r  id) 
    S-lemma : (r : x₀  x)  S x₀ y₀ (φ (sym r) y)
    S-lemma r = j r g

  uborlb-lemma : (n : Σ \(x : X)  Y x)  ((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 = R-lemma , S-lemma
   where
    φ : {x x' : X}  x  x'  Y x  Y x'
    φ = transport Y
    f : ((x' : X)  p(x' , next x')    R x x')  R x x₀
    f = pr₂(pr₂ first-correctness) x
    R-lower-bounder : (x' : X)(y' : Y x')  p(x' , y')    R x x'
    R-lower-bounder x' y' r' = pr₁(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 = pr₂(pr₂(next-correctness x)) y
    S-lower-bounder : (x' : X)(y' : Y x')  p(x' , y')    (r : x  x')  S x y (transport Y (sym r) y')
    S-lower-bounder x' y' r' = pr₂(lower-bounder ((x' , y')) r')
    j : {x x₀ : X}  (r : x  x₀)  {y : Y x} 
       S x y (next x)  S x y (φ (sym r) (next x₀))
    j = J  x x₀ r  {y : Y x}  S x y (next x)  S x y (φ (sym r) (next x₀)))  r  id) 
    S-lemma : (r : x  x₀)  S x y (φ (sym r) y₀)
    S-lemma r = j r (g y' r  S-lower-bounder x y' r refl))
    
\end{code}