Set Implicit Arguments.

(* We define dialogue trees and show that every functional
   that can be represented by a tree is continuous. *)

Inductive D (X Y Z : Type) :=
| η : Z -> D X Y Z
| β : (Y -> D X Y Z) -> X -> D X Y Z.

Fixpoint dialogue X Y Z (d : D X Y Z) (α : X -> Y) :=
  match d with
  | η _ _ z => z
  | β phi x => dialogue (phi (α x)) α
  end.

Definition eloquent (X Y Z : Type) f :=
  { d : D X Y Z | forall α, dialogue d α = f α}.

Definition Baire := nat -> nat.
Definition B := D nat nat.

Inductive peq X : list nat -> (nat -> X) -> (nat -> X) -> Prop :=
| peqN α β : peq nil α β
| peqC α β i L : α i = β i -> peq L α β -> peq (i::L) α β.

Notation "α '=[' L ']' β" := (peq L α β) (at level 50).

Definition continuous X (f : Baire -> X) :=
  forall α, { L | forall β, α =[L] β -> f α = f β }.

Lemma dialogue_continuous X (d : B X) :
  continuous (dialogue d).
Proof.
  induction d; intros α; cbn.
  - now exists nil.
  - destruct (H (α x) α) as [L H1]. exists (cons x L). intros β.
    inversion 1; subst. rewrite <- H4. apply (H1 β H7).
Defined.

Lemma eloquent_continuous X (f : Baire -> X) :
  eloquent f -> continuous f.
Proof.
  intros [d H] α. destruct (dialogue_continuous d α) as [L H1].
  exists L. intros β H2. specialize (H1 β H2). congruence.
Defined.

Lemma cont_ext X (f g : Baire -> X) :
  (forall α, f α = g α) -> continuous f -> continuous g.
Proof.
  intros H1 H2 α. destruct (H2 α) as [L H3].
  exists L. intros β H4. repeat rewrite <- H1. now apply H3.
Defined.

(* We define types and terms of system T and provide set-theoretic semantics.
   An extended version of T including an oracle term is defined similarly. *)

Inductive type : Type :=
| N : type
| imp : type -> type -> type.

Notation "σ ~> τ" := (imp σ τ) (at level 60, right associativity).

Fixpoint sem_ty σ : Type :=
  match σ with
  | N => nat
  | σ ~> τ => (sem_ty σ) -> sem_ty τ
  end.

Require Import Vectors.Fin.

Notation fin := (Fin.t).
Notation env n := (fin n -> type).

Definition cns X (A : X) n (Γ : fin n -> X) : fin (S n) -> X.
  intros ?. inversion H.
  - exact A.
  - subst. apply Γ, H1.
Defined.

Inductive iterm (n : nat) (Γ : env n) : type -> Type :=
| izero : @iterm n Γ N
| isucc : @iterm n Γ (N ~> N)
| ivar (v : fin n) : @iterm n Γ (Γ v)
| irec sigma : @iterm n Γ (sigma ~> (N ~> sigma ~> sigma) ~> N ~> sigma)
| ilambda sigma tau : @iterm (S n) (cns sigma Γ) tau -> @iterm n Γ (sigma ~> tau)
| iapp sigma tau : @iterm n Γ (sigma ~> tau) -> @iterm n Γ sigma -> @iterm n Γ tau.

Definition interp n (Gamma : env n) :=
  forall (x : fin n), sem_ty (Gamma x).

From Equations Require Import Equations.

Definition cns_interp n (Gamma : env n) sigma (a : sem_ty sigma) : interp Gamma -> interp (cns sigma Gamma).
  intros f x. depelim x; subst.
  - exact a.
  - exact (f x).
Defined.

Fixpoint sem_tm n (Gamma : env n) (sigma : type) (t : iterm Gamma sigma) (rho : interp Gamma) : sem_ty sigma :=
  match t with
  | izero _ => O
  | isucc _ => S
  | ivar _ x => rho x
  | irec _ tau => @nat_rect (fun _ => sem_ty tau)
  | ilambda t => fun x => sem_tm t (cns_interp _ x rho)
  | iapp t1 t2 => (sem_tm t1 rho) (sem_tm t2 rho)
  end.

Definition empty_env : fin 0 -> type.
  intros x. depelim x.
Defined.

Definition empty_interp : (forall x : fin 0, sem_ty (empty_env x)).
  intros x. depelim x.
Defined.

Definition definable sigma (f : sem_ty sigma) :=
  { t : iterm empty_env sigma | sem_tm t empty_interp = f}.

Inductive iterm' (n : nat) (Γ : env n) : type -> Type :=
| Omega : @iterm' n Γ (N ~> N)
| izero' : @iterm' n Γ N
| isucc' : @iterm' n Γ (N ~> N)
| ivar' (v : fin n) : @iterm' n Γ (Γ v)
| irec' sigma : @iterm' n Γ (sigma ~> (N ~> sigma ~> sigma) ~> N ~> sigma)
| ilambda' sigma tau : @iterm' (S n) (cns sigma Γ) tau -> @iterm' n Γ (sigma ~> tau)
| iapp' sigma tau : @iterm' n Γ (sigma ~> tau) -> @iterm' n Γ sigma -> @iterm' n Γ tau.

Fixpoint sem_tm' n (Gamma : env n) (sigma : type) (t : iterm' Gamma sigma) (rho : interp Gamma) alpha : sem_ty sigma :=
  match t with
  | Omega _ => alpha
  | izero' _ => O
  | isucc' _ => S
  | ivar' _ x => rho x
  | irec' _ tau => @nat_rect (fun _ => sem_ty tau)
  | ilambda' t => fun x => sem_tm' t (cns_interp _ x rho) alpha
  | iapp' t1 t2 => (sem_tm' t1 rho alpha) (sem_tm' t2 rho alpha)
  end.

Fixpoint embed n (Gamma : env n) σ (t : iterm Gamma σ) : iterm' Gamma σ :=
  match t with
  | izero _ => izero' Gamma
  | isucc _ => isucc' Gamma
  | irec _ σ => irec' Gamma σ
  | ivar _ x => ivar' Gamma x
  | ilambda t => ilambda' (embed t)
  | iapp t1 t2 => iapp' (embed t1) (embed t2)
  end.

Hypothesis FE : forall X Y (f g : X -> Y), (forall x, f x = g x) -> f = g.

Lemma preservation n (Gamma : env n) sigma (t : iterm Gamma sigma) rho α :
  sem_tm t rho = sem_tm' (embed t) rho α.
Proof.
  induction t; cbn; try congruence. apply FE.
  intros a. now rewrite IHt.
Defined.

(* We define the non-standard tree semantics. *)

Fixpoint B_ty (σ : type) :=
  match σ with
  | N => B (sem_ty N)
  | σ ~> τ => B_ty σ -> B_ty τ
  end.

Fixpoint kleisli_ext X Y (f : X -> B Y) (d : B X) : B Y :=
  match d with
  | η _ _ x => f x
  | β ϕ i => β (fun j => kleisli_ext f (ϕ j)) i
  end.

Definition B_func X Y (f : X -> Y) : B X -> B Y :=
  kleisli_ext (fun x => η nat nat (f x)).

Notation decode α d :=
  (dialogue d α).

Lemma decode_natural X Y (g : X -> Y) (d : B X) α :
  g (decode α d) = decode α (B_func g d).
Proof.
  induction d; cbn; trivial.
Defined.

Lemma decode_kleisli X Y (f : X -> B Y) (d : B X) α :
  decode α (f (decode α d)) = decode α (kleisli_ext f d).
Proof.
  induction d; cbn; trivial.
Defined.

Fixpoint kleisli_ext' X σ : (X -> B_ty σ) -> B X -> B_ty σ :=
  match σ with
  | N => kleisli_ext (X:=X) (Y:=nat)
  | σ ~> τ => fun g d s => kleisli_ext' τ (fun x => g x s) d
  end.

Definition generic : B nat -> B nat :=
  kleisli_ext (β (@η nat nat nat)).

Compute (generic (β (fun x : nat => η nat nat 0) 0)).

Lemma generic_diagram α (d : B nat) :
  α (decode α d) = decode α (generic d).
Proof.
  induction d; cbn; trivial.
Defined.

Definition B_ctx n (Gamma : env n) :=
  forall x, B_ty (Gamma x).

Definition swap X Y Z (f : X -> Y -> Z) : Y -> X -> Z :=
  fun y x => f x y.

Eval cbn in (fun sigma => B_ty (sigma ~> (N ~> sigma ~> sigma) ~> N ~> sigma)).

Definition cns_B_ctx n (Gamma : env n) sigma (a : B_ty sigma) : B_ctx Gamma -> B_ctx (cns sigma Gamma).
  intros f x. depelim x; subst.
  - exact a.
  - exact (f x).
Defined.

Fixpoint B_tm n (Gamma : env n) σ (t : iterm' Gamma σ) (Delta : B_ctx Gamma) : B_ty σ :=
  match t with
  | Omega _ => generic
  | izero' _ => η _ _ 0
  | isucc' _ => B_func S
  | irec' _ tau => fun a f => kleisli_ext' tau (@nat_rect (fun _ => B_ty tau) a (fun n => f (η nat nat n)))
  | ivar' _ x => Delta x
  | ilambda' t => fun a => B_tm t (cns_B_ctx _ a Delta)
  | iapp' t1 t2 => B_tm t1 Delta (B_tm t2 Delta)
  end.

(* We define a logical relation R between both semantics for extended terms.
   It follows that R relates the two semantics for any given term. *)

Fixpoint R σ : (Baire -> sem_ty σ) -> B_ty σ -> Prop :=
  match σ with
  | N => fun (n : Baire -> sem_ty N) (n' : B_ty N) => forall α, n α = decode α n'
  | σ ~> τ => fun f f' => forall x x', R σ x x' -> R τ (fun α => f α (x α)) (f' x')
  end.

Lemma R_kleisli σ (g : nat -> Baire -> sem_ty σ) (g' : nat -> B_ty σ) :
  (forall k, R σ (g k) (g' k))
  -> forall (n : Baire -> nat) (n' : B nat), R N n n'
  -> R σ (fun α => g (n α) α) (kleisli_ext' σ g' n').
Proof.
  induction σ as [|σ IHs τ IHt]; cbn.
  - intros H1 n n' H2 α. now rewrite <- decode_kleisli, H1, H2.
  - intros H1 n n' H2 y y' H3. apply (IHt (fun k α => g k α (y α))).
    + intros k. now apply H1.
    + cbn. apply H2.
Defined.

Definition Rs n (Gamma : env n) :=
  fun xs ys => forall i, R (Gamma i) (fun alpha => xs alpha i) (ys i).

Lemma main n (Gamma : env n) σ (t : iterm' Gamma σ) xs ys :
  Rs Gamma xs ys -> R σ (fun alpha => sem_tm' t (xs alpha) alpha) (B_tm t ys).
Proof.
  induction t; cbn; eauto.
  - intros HG x x' H α. now rewrite <- generic_diagram, H.
  - intros HG x x' H α. now rewrite <- decode_natural, H.
  - intros HG f f' H1 x x' H2 l l' H3.
    apply (R_kleisli sigma (fun k α => nat_rect (fun _ => sem_ty sigma) (f α) (x α) k)).
    + intros k. induction k.
      * cbn in *. apply H1.
      * now apply H2, IHk.
    + cbn. apply H3.
  - intros HR x x' H. apply IHt. intros i. depelim i; cbn.
    + apply H.
    + apply HR.
  - intros HR. apply IHt1; trivial. now apply IHt2.
Defined.

(* We translate definable functionals into dialogue trees.
   As the translation preserves all information, definable functionals are continuous. *)

Definition functional :=
  (N ~> N) ~> N.

Definition empty_interpB : (forall x : fin 0, B_ty (empty_env x)).
  intros x. inversion x.
Defined.

Definition ground_iterm :=
  iterm empty_env.

Definition ground_iterm' :=
  iterm' empty_env.

Definition ground_B_tm sigma (t : ground_iterm' sigma) :=
  B_tm t empty_interpB.

Definition dialogue_tree (t : ground_iterm functional) : B nat :=
  ground_B_tm (iapp' (embed t) (Omega _)).

Lemma Rs_empty xs ys :
  Rs empty_env xs ys.
Proof.
  intros i. inversion i.
Defined.

Lemma dialogue_tree_correct (t : ground_iterm functional) (α : Baire) :
  sem_tm t empty_interp α = decode α (dialogue_tree t).
Proof.
  rewrite (preservation t empty_interp α).
  specialize (main (iapp' (embed t) (Omega _))). intros H.
  apply (H (fun _ => empty_interp) empty_interpB (Rs_empty _ _)).
Defined.

Theorem def_eloquent (f : Baire -> nat) :
  definable functional f -> eloquent f.
Proof.
  intros [t H]. exists (dialogue_tree t).
  intros α. now rewrite <- dialogue_tree_correct, H.
Defined.

Corollary def_continuous (f : Baire -> nat) :
  definable functional f -> continuous f.
Proof.
  intros H. now apply eloquent_continuous, def_eloquent.
Defined.

Print Assumptions def_continuous.