(** * The fan theorem *)

From HoTT Require Import Basics Types. 
Require Import Truncations.Core.
Require Import Spaces.Nat.Core.
Require Import Misc.UStructures BarInduction. 
Require Import Spaces.NatSeq.Core Spaces.NatSeq.UStructure.
Require Import Spaces.List.Core Spaces.List.Theory.

Local Open Scope nat_scope.
Local Open Scope type_scope.
Local Open Scope list_scope.

Definition DecidableFanTheorem (A : Type) :=
  forall (B : list A -> Type)
  (dec : forall l : list A, Decidable (B l))
  (bar : IsBar B),
  IsUniformBar B.

Definition MonotoneFanTheorem (A : Type) :=
  forall (B : list A -> Type)
  (mon : IsMonotone B)
  (bar : IsBar B),
  IsUniformBar B.

Definition FanTheorem (A : Type) :=
  forall (B : list A -> Type)
  (bar : IsBar B),
  IsUniformBar B.

Definition fantheorem_empty : FanTheorem Empty.
FanTheorem Empty
Proof.
FanTheorem Empty
  intros B bB.
B: list Empty -> Type
bB: IsBar B
IsUniformBar B
  exists 0.
B: list Empty -> Type
bB: IsBar B
forall s : nat -> Empty, {n : nat & (n <= 0) * B (list_restrict s n)}
  intro s.
B: list Empty -> Type
bB: IsBar B
s: nat -> Empty
{n : nat & (n <= 0) * B (list_restrict s n)}
  contradiction (s 0).
Defined.

Definition fantheorem_contr (A : Type) `{Contr A} : FanTheorem A.
A: Type
Contr0: Contr A
FanTheorem A
Proof.
A: Type
Contr0: Contr A
FanTheorem A
  intros B bB.
A: Type
Contr0: Contr A
B: list A -> Type
bB: IsBar B
IsUniformBar B
  pose (c := fun (_ : nat) => center A).
A: Type
Contr0: Contr A
B: list A -> Type
bB: IsBar B
c:= fun _ : nat => center A: nat -> A
IsUniformBar B
  exists (bB c).1.
A: Type
Contr0: Contr A
B: list A -> Type
bB: IsBar B
c:= fun _ : nat => center A: nat -> A
forall s : nat -> A, {n : nat & (n <= (bB c).1) * B (list_restrict s n)}
  intro s.
A: Type
Contr0: Contr A
B: list A -> Type
bB: IsBar B
c:= fun _ : nat => center A: nat -> A
s: nat -> A
{n : nat & (n <= (bB c).1) * B (list_restrict s n)}
  assert (p : forall n : nat, list_restrict s n = list_restrict c n).
A: Type
Contr0: Contr A
B: list A -> Type
bB: IsBar B
c:= fun _ : nat => center A: nat -> A
s: nat -> A
forall n : nat, list_restrict s n = list_restrict c n
A: Type
Contr0: Contr A
B: list A -> Type
bB: IsBar B
c:= fun _ : nat => center A: nat -> A
s: nat -> A
p: forall n : nat, list_restrict s n = list_restrict c n
{n : nat & (n <= (bB c).1) * B (list_restrict s n)}
  {
A: Type
Contr0: Contr A
B: list A -> Type
bB: IsBar B
c:= fun _ : nat => center A: nat -> A
s: nat -> A
forall n : nat, list_restrict s n = list_restrict c n intro n.
A: Type
Contr0: Contr A
B: list A -> Type
bB: IsBar B
c:= fun _ : nat => center A: nat -> A
s: nat -> A
n: nat
list_restrict s n = list_restrict c n
    srapply path_list_nth'.
A: Type
Contr0: Contr A
B: list A -> Type
bB: IsBar B
c:= fun _ : nat => center A: nat -> A
s: nat -> A
n: nat
length (list_restrict s n) = length (list_restrict c n)
A: Type
Contr0: Contr A
B: list A -> Type
bB: IsBar B
c:= fun _ : nat => center A: nat -> A
s: nat -> A
n: nat
forall (n0 : nat) (H : n0 < length (list_restrict s n)),
nth' (list_restrict s n) n0 H =
nth' (list_restrict c n) n0 (transport (lt n0) ?p H)
    1: by rewrite !length_list_restrict.
A: Type
Contr0: Contr A
B: list A -> Type
bB: IsBar B
c:= fun _ : nat => center A: nat -> A
s: nat -> A
n: nat
forall (n0 : nat) (H : n0 < length (list_restrict s n)),
nth' (list_restrict s n) n0 H =
nth' (list_restrict c n) n0
  (transport (lt n0)
     (internal_paths_rew_r (fun n1 : nat => n1 = length (list_restrict c n))
        (internal_paths_rew_r (fun n1 : nat => n = n1) 1
           (length_list_restrict c n))
        (length_list_restrict s n))
     H)
    intros m h.
A: Type
Contr0: Contr A
B: list A -> Type
bB: IsBar B
c:= fun _ : nat => center A: nat -> A
s: nat -> A
n, m: nat
h: m < length (list_restrict s n)
nth' (list_restrict s n) m h =
nth' (list_restrict c n) m
  (transport (lt m)
     (internal_paths_rew_r (fun n0 : nat => n0 = length (list_restrict c n))
        (internal_paths_rew_r (fun n0 : nat => n = n0) 1
           (length_list_restrict c n))
        (length_list_restrict s n))
     h)
    by apply path_contr. }
A: Type
Contr0: Contr A
B: list A -> Type
bB: IsBar B
c:= fun _ : nat => center A: nat -> A
s: nat -> A
p: forall n : nat, list_restrict s n = list_restrict c n
{n : nat & (n <= (bB c).1) * B (list_restrict s n)}
  exists (bB c).1; split.
A: Type
Contr0: Contr A
B: list A -> Type
bB: IsBar B
c:= fun _ : nat => center A: nat -> A
s: nat -> A
p: forall n : nat, list_restrict s n = list_restrict c n
(bB c).1 <= (bB c).1
A: Type
Contr0: Contr A
B: list A -> Type
bB: IsBar B
c:= fun _ : nat => center A: nat -> A
s: nat -> A
p: forall n : nat, list_restrict s n = list_restrict c n
B (list_restrict s (bB c).1)
  -
A: Type
Contr0: Contr A
B: list A -> Type
bB: IsBar B
c:= fun _ : nat => center A: nat -> A
s: nat -> A
p: forall n : nat, list_restrict s n = list_restrict c n
(bB c).1 <= (bB c).1 reflexivity.
  -
A: Type
Contr0: Contr A
B: list A -> Type
bB: IsBar B
c:= fun _ : nat => center A: nat -> A
s: nat -> A
p: forall n : nat, list_restrict s n = list_restrict c n
B (list_restrict s (bB c).1) rewrite p.
A: Type
Contr0: Contr A
B: list A -> Type
bB: IsBar B
c:= fun _ : nat => center A: nat -> A
s: nat -> A
p: forall n : nat, list_restrict s n = list_restrict c n
B (list_restrict c (bB c).1)
    exact (bB c).2.
Defined.

(** The family we use when applying the fan theorem in our proof that continuity implies uniform continuity. *)
Definition uc_theorem_family {A : Type} (p : (nat -> A) -> Bool)
  : list A -> Type
  := fun l =>
      forall (u v : nat -> A) (h : list_restrict u (length l) = l)
        (h' : list_restrict v (length l) = l), p u = p v.

Definition is_bar_uc_theorem_family {A : Type}
  (p : (nat -> A) -> Bool) (cont : IsContinuous p)
  : IsBar (uc_theorem_family p).
A: Type
p: (nat -> A) -> Bool
cont: IsContinuous p
IsBar (uc_theorem_family p)
Proof.
A: Type
p: (nat -> A) -> Bool
cont: IsContinuous p
IsBar (uc_theorem_family p)
  intro s.
A: Type
p: (nat -> A) -> Bool
cont: IsContinuous p
s: nat -> A
{n : nat & uc_theorem_family p (list_restrict s n)}
  specialize (cont s 0) as [n H].
A: Type
p: (nat -> A) -> Bool
s: nat -> A
n: nat
H: forall v : nat -> A, s =[n] v -> p s =[0] p v
{n0 : nat & uc_theorem_family p (list_restrict s n0)}
  exists n.
A: Type
p: (nat -> A) -> Bool
s: nat -> A
n: nat
H: forall v : nat -> A, s =[n] v -> p s =[0] p v
uc_theorem_family p (list_restrict s n)
  intros u v h t.
A: Type
p: (nat -> A) -> Bool
s: nat -> A
n: nat
H: forall v0 : nat -> A, s =[n] v0 -> p s =[0] p v0
u, v: nat -> A
h: list_restrict u (length (list_restrict s n)) = list_restrict s n
t: list_restrict v (length (list_restrict s n)) = list_restrict s n
p u = p v
  symmetry in h,t.
A: Type
p: (nat -> A) -> Bool
s: nat -> A
n: nat
H: forall v0 : nat -> A, s =[n] v0 -> p s =[0] p v0
u, v: nat -> A
h: list_restrict s n = list_restrict u (length (list_restrict s n))
t: list_restrict s n = list_restrict v (length (list_restrict s n))
p u = p v
  rewrite length_list_restrict in h, t.
A: Type
p: (nat -> A) -> Bool
s: nat -> A
n: nat
H: forall v0 : nat -> A, s =[n] v0 -> p s =[0] p v0
u, v: nat -> A
h: list_restrict s n = list_restrict u n
t: list_restrict s n = list_restrict v n
p u = p v
  apply list_restrict_eq_iff_seq_agree_lt in h, t.
A: Type
p: (nat -> A) -> Bool
s: nat -> A
n: nat
H: forall v0 : nat -> A, s =[n] v0 -> p s =[0] p v0
u, v: nat -> A
h: s =[n] u
t: s =[n] v
p u = p v
  exact ((H _ h)^ @ (H _ t)).
Defined.

(** The fan theorem implies that every continuous function is uniformly continuous. The current proof uses the full fan theorem. Less powerful versions might be enough. *)

Definition uniform_continuity_fantheorem {A : Type} (fan : FanTheorem A)
  (p : (nat -> A) -> Bool) (c : IsContinuous p)
  : uniformly_continuous p.
A: Type
fan: FanTheorem A
p: (nat -> A) -> Bool
c: IsContinuous p
uniformly_continuous p
Proof.
A: Type
fan: FanTheorem A
p: (nat -> A) -> Bool
c: IsContinuous p
uniformly_continuous p
  pose proof (fan' := fan (uc_theorem_family p) (is_bar_uc_theorem_family p c)).
A: Type
fan: FanTheorem A
p: (nat -> A) -> Bool
c: IsContinuous p
fan': IsUniformBar (uc_theorem_family p)
uniformly_continuous p
  destruct fan' as [n ub].
A: Type
fan: FanTheorem A
p: (nat -> A) -> Bool
c: IsContinuous p
n: nat
ub: forall s : nat -> A,
{n0 : nat & (n0 <= n) * uc_theorem_family p (list_restrict s n0)}
uniformly_continuous p
  intro m.
A: Type
fan: FanTheorem A
p: (nat -> A) -> Bool
c: IsContinuous p
n: nat
ub: forall s : nat -> A,
{n0 : nat & (n0 <= n) * uc_theorem_family p (list_restrict s n0)}
m: nat
{n0 : nat & forall u v : nat -> A, u =[n0] v -> p u =[m] p v}
  exists n.
A: Type
fan: FanTheorem A
p: (nat -> A) -> Bool
c: IsContinuous p
n: nat
ub: forall s : nat -> A,
{n0 : nat & (n0 <= n) * uc_theorem_family p (list_restrict s n0)}
m: nat
forall u v : nat -> A, u =[n] v -> p u =[m] p v
  intros u v h.
A: Type
fan: FanTheorem A
p: (nat -> A) -> Bool
c: IsContinuous p
n: nat
ub: forall s : nat -> A,
{n0 : nat & (n0 <= n) * uc_theorem_family p (list_restrict s n0)}
m: nat
u, v: nat -> A
h: u =[n] v
p u =[m] p v
  specialize (ub v) as [k [bound uctf]].
A: Type
fan: FanTheorem A
p: (nat -> A) -> Bool
c: IsContinuous p
n, m: nat
u, v: nat -> A
h: u =[n] v
k: nat
bound: k <= n
uctf: uc_theorem_family p (list_restrict v k)
p u =[m] p v
  apply uctf.
A: Type
fan: FanTheorem A
p: (nat -> A) -> Bool
c: IsContinuous p
n, m: nat
u, v: nat -> A
h: u =[n] v
k: nat
bound: k <= n
uctf: uc_theorem_family p (list_restrict v k)
list_restrict u (length (list_restrict v k)) = list_restrict v k
A: Type
fan: FanTheorem A
p: (nat -> A) -> Bool
c: IsContinuous p
n, m: nat
u, v: nat -> A
h: u =[n] v
k: nat
bound: k <= n
uctf: uc_theorem_family p (list_restrict v k)
list_restrict v (length (list_restrict v k)) = list_restrict v k
  -
A: Type
fan: FanTheorem A
p: (nat -> A) -> Bool
c: IsContinuous p
n, m: nat
u, v: nat -> A
h: u =[n] v
k: nat
bound: k <= n
uctf: uc_theorem_family p (list_restrict v k)
list_restrict u (length (list_restrict v k)) = list_restrict v k rewrite length_list_restrict.
A: Type
fan: FanTheorem A
p: (nat -> A) -> Bool
c: IsContinuous p
n, m: nat
u, v: nat -> A
h: u =[n] v
k: nat
bound: k <= n
uctf: uc_theorem_family p (list_restrict v k)
list_restrict u k = list_restrict v k
    apply (snd list_restrict_eq_iff_seq_agree_lt).
A: Type
fan: FanTheorem A
p: (nat -> A) -> Bool
c: IsContinuous p
n, m: nat
u, v: nat -> A
h: u =[n] v
k: nat
bound: k <= n
uctf: uc_theorem_family p (list_restrict v k)
u =[k] v
    apply (us_rel_leq bound h).
  -
A: Type
fan: FanTheorem A
p: (nat -> A) -> Bool
c: IsContinuous p
n, m: nat
u, v: nat -> A
h: u =[n] v
k: nat
bound: k <= n
uctf: uc_theorem_family p (list_restrict v k)
list_restrict v (length (list_restrict v k)) = list_restrict v k exact (ap _ (length_list_restrict _ _)).
Defined.