Chuangjie Xu, 2013

This corresponds to part of Section 4.2 of the paper
http://www.cs.bham.ac.uk/~mhe/papers/kleene-kreisel.pdf

The behaviour of the Fan functional is expressed in T by the
following skolemization of UC:

    f : (Ⓝ ⇨ ②) ⇨ Ⓝ , α : Ⓝ ⇨ ② , β : Ⓝ ⇨ ②
    ⊢
    α ≣[ FAN f ] β →→ f α == f β

\begin{code}

module Validation-of-fan where

open import MiniLibrary
open import Sequence
open import Space
open import Space-product
open import Space-exponential
open import Space-discrete
open import not-not
open import Inequality
open import UniformContinuity
open import Fan
open import T
open import C-interpretation-of-T

\end{code}

The interpretation of T formulas:

\begin{code}

〔_〕 : {n : ℕ}{Γ : Cxt n} → Fml Γ → U 〖 Γ 〗 → Set
〔 M == N 〕 ρ = π₀ ⟦ M ⟧ ρ ≡ π₀ ⟦ N ⟧ ρ
〔 φ ∧∧ ψ 〕 ρ = (〔 φ 〕 ρ) × (〔 ψ 〕 ρ)
〔 φ →→ ψ 〕 ρ = (〔 φ 〕 ρ) → (〔 ψ 〕 ρ)

\end{code}

The "agree with" function in T is defined as a ②-valued function, using the
recursor and the following two auxiliary functions, EQ and MIN.

EQ returns ⊤ iff the two input booleans are equal. And eq is the set
interpretation of EQ

\begin{code}

EQ : {n : ℕ}{Γ : Cxt n} → Tm Γ ② → Tm Γ ② → Tm Γ ②
EQ B₀ B₁ = IF ∙ (IF ∙ ⊤ ∙ ⊥ ∙ B₁) ∙ B₁ ∙ B₀

eq : ₂ → ₂ → ₂
eq b₀ b₁ = if (if ₁ ₀ b₁) b₁ b₀

Lemma[eq] : (b₀ b₁ : ₂) → eq b₀ b₁ ≡ ₁ → b₀ ≡ b₁
Lemma[eq] ₀ ₀ refl = refl
Lemma[eq] ₀ ₁ ()
Lemma[eq] ₁ ₀ ()
Lemma[eq] ₁ ₁ refl = refl

\end{code}

MIN returns the minimal one of the two input booleans. And min is the set
interpretation of MIN.

\begin{code}

MIN : {n : ℕ}{Γ : Cxt n} → Tm Γ ② → Tm Γ ② → Tm Γ ②
MIN B₀ B₁ = IF ∙ ⊥ ∙ B₁ ∙ B₀

min : ₂ → ₂ → ₂
min b₀ b₁ = if ₀ b₁ b₀

Lemma[min] : (b₀ b₁ : ₂) → min b₀ b₁ ≡ ₁ → b₀ ≡ ₁ ∧ b₁ ≡ ₁
Lemma[min] ₀ ₀ ()
Lemma[min] ₀ ₁ ()
Lemma[min] ₁ ₀ ()
Lemma[min] ₁ ₁ refl = ∧-intro refl refl

\end{code}

Instead of arbitrary sequences, we define "agree with" function only for the two
sequences (variables) A and B in the context

  Γ  ≡  F : (Ⓝ ⇨ ②) ⇨ Ⓝ , A : Ⓝ ⇨ ② , B : Ⓝ ⇨ ②.

\begin{code}

ν₀ : {n : ℕ}{Γ : Cxt (succ n)} →
     Tm Γ (Γ ₍ zero ₎)
ν₀ = VAR zero
ν₁ : {n : ℕ}{Γ : Cxt (succ (succ n))} →
     Tm Γ (Γ ₍ succ zero ₎)
ν₁ = VAR (succ zero)
ν₂ : {n : ℕ}{Γ : Cxt (succ (succ (succ n)))} →
     Tm Γ (Γ ₍ succ (succ zero) ₎)
ν₂ = VAR (succ (succ zero))
ν₃ : {n : ℕ}{Γ : Cxt (succ (succ (succ (succ n))))} →
     Tm Γ (Γ ₍ succ (succ (succ zero)) ₎)
ν₃ = VAR (succ (succ (succ zero)))

Γ : Cxt 
Γ = ε ₊ ((Ⓝ ⇨ ②) ⇨ Ⓝ) ₊ (Ⓝ ⇨ ②) ₊ (Ⓝ ⇨ ②)

F : Tm Γ ((Ⓝ ⇨ ②) ⇨ Ⓝ)
F = ν₂

N : Tm Γ Ⓝ
N = FAN ∙ F

A B : Tm Γ (Ⓝ ⇨ ②)
A = ν₁
B = ν₀

\end{code}

A' and B' are the weakening of sequences A and B.

\begin{code}

A' B' : Tm (Γ ₊ Ⓝ ₊ ②) (Ⓝ ⇨ ②)
A' = ν₃
B' = ν₂

\end{code}

The "agree with" function for the two sequences A and B.
If they are equal up to the first N positions, then A≣[N]B is ⊤.

\begin{code}

A≣[N]B : Tm Γ ②
A≣[N]B = REC ∙ ⊤ ∙ (LAM (LAM (MIN (EQ (A' ∙ ν₁) (B' ∙ ν₁)) ν₀))) ∙ N

\end{code}

C-spaces validate the theorem that if the sequences A and B are equal up to the
first N positions, then the applications F A and F B are equal.

\begin{code}

Theorem : ∀(ρ : U 〖 Γ 〗) → 〔 (A≣[N]B == ⊤) →→ (F ∙ A == F ∙ B) 〕 ρ
Theorem ρ EN = fan-behaviour f α β en
 where
  f : Map (ℕSpace ⇒ ₂Space) ℕSpace
  f = π₀ ⟦ F ⟧ ρ
  α β : Map ℕSpace ₂Space
  α = π₀ ⟦ A ⟧ ρ
  β = π₀ ⟦ B ⟧ ρ

  g : ℕ → ₂ → ₂
  g n b = π₀ (π₀ (π₀ ⟦ LAM (LAM (MIN (EQ (A' ∙ ν₁) (B' ∙ ν₁)) ν₀)) ⟧ ρ) n) b

  lemma : (k : ℕ) → rec ₁ g k ≡ ₁ → π₀ α ≣[ k ] π₀ β
  lemma         refl = ≣[zero]
  lemma (succ k) esk  = ≣[succ] IH claim₁
   where
    ek : rec ₁ g k ≡ ₁
    ek = ∧-elim₁ (Lemma[min] (eq (π₀ α k) (π₀ β k)) (rec ₁ g k)  esk)
    IH : π₀ α ≣[ k ] π₀ β
    IH = lemma k ek
    claim₀ : eq (π₀ α k) (π₀ β k) ≡ ₁
    claim₀ = ∧-elim₀ (Lemma[min] (eq (π₀ α k) (π₀ β k)) (rec ₁ g k) esk)
    claim₁ : π₀ α k ≡ π₀ β k
    claim₁ = Lemma[eq] (π₀ α k) (π₀ β k) claim₀

  -- By the above lemma and the assumption that 〔 A≣[N]B == ⊤ 〕 ρ ≡ ₁,
  -- the interpretations of the two sequences are equal up to the first ⟦ N ⟧ position.
  en : π₀ (π₀ ⟦ A ⟧ ρ) ≣[ π₀ ⟦ N ⟧ ρ ] π₀ (π₀ ⟦ B ⟧ ρ)
  en = lemma (π₀ ⟦ N ⟧ ρ) EN

\end{code}