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}