UStructure.v

(** * Uniform structure on types of sequences *)

From HoTT Require Import Basics Types.[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Spaces.Nat.Core.
Require Import Misc.UStructures.
Require Import List.Core List.Theory.
Require Import Spaces.NatSeq.Core.

Local Open Scope nat_scope.
Local Open Scope type_scope.

(** ** [UStructure] defined by [seq_agree_lt] *)

(** Every type of the form [nat -> X] carries a uniform structure defined by the [seq_agree_lt n] relation for every [n : nat]. *)
Instance sequence_type_us {X : Type} : UStructure (nat -> X) | 10.X: Type
UStructure (nat -> X)
Proof.X: Type
UStructure (nat -> X)
  snapply Build_UStructure.X: Type
nat -> Relation (nat -> X)
X: Type
forall n : nat, Reflexive (?us_rel n)
X: Type
forall n : nat, Symmetric (?us_rel n)
X: Type
forall n : nat, Transitive (?us_rel n)
X: Type
forall (n : nat) (x y : nat -> X),
?us_rel n.+1 x y -> ?us_rel n x y
  -X: Type
nat -> Relation (nat -> X) exact seq_agree_lt.
  -X: Type
forall n : nat, Reflexive (seq_agree_lt n) exact (fun _ _ _ _ => idpath).
  -X: Type
forall n : nat, Symmetric (seq_agree_lt n) exact (fun _ _ _ h _ _ => (h _ _)^).
  -X: Type
forall n : nat, Transitive (seq_agree_lt n) exact (fun _ _ _ _ h1 h2 _ _ => ((h1 _ _) @ (h2 _ _))).
  -X: Type
forall (n : nat) (x y : nat -> X),
seq_agree_lt n.+1 x y -> seq_agree_lt n x y exact (fun _ _ _ h _ _ => h _ _).
Defined.

Definition sequence_type_us_zero {X : Type} (s t : nat -> X) : s =[0] t
  := fun n hn => Empty_rec (not_lt_zero_r n hn).

Definition seq_cons_of_eq {X : Type} {n : nat} {s t : nat -> X} {x : X}
  (h : s =[n] t)
  : (seq_cons x s) =[n.+1] (seq_cons x t).X: Type
n: nat
s, t: nat -> X
x: X
h: s =[n] t
seq_cons x s =[n.+1] seq_cons x t
Proof.X: Type
n: nat
s, t: nat -> X
x: X
h: s =[n] t
seq_cons x s =[n.+1] seq_cons x t
  intros m hm; destruct m.X: Type
n: nat
s, t: nat -> X
x: X
h: s =[n] t
hm: 0 < n.+1
seq_cons x s 0 = seq_cons x t 0
X: Type
n: nat
s, t: nat -> X
x: X
h: s =[n] t
m: nat
hm: m.+1 < n.+1
seq_cons x s m.+1 = seq_cons x t m.+1
  -X: Type
n: nat
s, t: nat -> X
x: X
h: s =[n] t
hm: 0 < n.+1
seq_cons x s 0 = seq_cons x t 0 reflexivity.
  -X: Type
n: nat
s, t: nat -> X
x: X
h: s =[n] t
m: nat
hm: m.+1 < n.+1
seq_cons x s m.+1 = seq_cons x t m.+1 exact (h m _).
Defined.

(** We can also rephrase the definition of [seq_agree_lt] using the [list_restrict] function. *)
Definition list_restrict_eq_iff_seq_agree_lt
  {A : Type} {n : nat} {s t : nat -> A}
  : (list_restrict s n = list_restrict t n) <-> s =[n] t.A: Type
n: nat
s, t: nat -> A
list_restrict s n = list_restrict t n <-> s =[n] t
Proof.A: Type
n: nat
s, t: nat -> A
list_restrict s n = list_restrict t n <-> s =[n] t
  constructor.A: Type
n: nat
s, t: nat -> A
list_restrict s n = list_restrict t n -> s =[n] t
A: Type
n: nat
s, t: nat -> A
s =[n] t -> list_restrict s n = list_restrict t n
  -A: Type
n: nat
s, t: nat -> A
list_restrict s n = list_restrict t n -> s =[n] t intros h m hm.A: Type
n: nat
s, t: nat -> A
h: list_restrict s n = list_restrict t n
m: nat
hm: m < n
s m = t m
    lhs_V exact (nth'_list_restrict s ((length_list_restrict _ _)^ # hm)).A: Type
n: nat
s, t: nat -> A
h: list_restrict s n = list_restrict t n
m: nat
hm: m < n
nth' (list_restrict s n) m
  (transport (lt m) (length_list_restrict s n)^ hm) =
t m
    rhs_V exact (nth'_list_restrict t ((length_list_restrict _ _)^ # hm)).A: Type
n: nat
s, t: nat -> A
h: list_restrict s n = list_restrict t n
m: nat
hm: m < n
nth' (list_restrict s n) m
  (transport (lt m) (length_list_restrict s n)^ hm) =
nth' (list_restrict t n) m
  (transport (lt m) (length_list_restrict t n)^ hm)
    exact (nth'_path_list h _ _).
  -A: Type
n: nat
s, t: nat -> A
s =[n] t -> list_restrict s n = list_restrict t n intro h.A: Type
n: nat
s, t: nat -> A
h: s =[n] t
list_restrict s n = list_restrict t n
    apply (path_list_nth' _ _
            (length_list_restrict s n @ (length_list_restrict t n)^)).A: Type
n: nat
s, t: nat -> A
h: s =[n] t
forall (n0 : nat)
(H : n0 < length (list_restrict s n)),
nth' (list_restrict s n) n0 H =
nth' (list_restrict t n) n0
  (transport (lt n0)
     (length_list_restrict s n @
      (length_list_restrict t n)^) H)
    intros i Hi.A: Type
n: nat
s, t: nat -> A
h: s =[n] t
i: nat
Hi: i < length (list_restrict s n)
nth' (list_restrict s n) i Hi =
nth' (list_restrict t n) i
  (transport (lt i)
     (length_list_restrict s n @
      (length_list_restrict t n)^) Hi)
    lhs snapply nth'_list_restrict.A: Type
n: nat
s, t: nat -> A
h: s =[n] t
i: nat
Hi: i < length (list_restrict s n)
s i =
nth' (list_restrict t n) i
  (transport (lt i)
     (length_list_restrict s n @
      (length_list_restrict t n)^) Hi)
    rhs snapply nth'_list_restrict.A: Type
n: nat
s, t: nat -> A
h: s =[n] t
i: nat
Hi: i < length (list_restrict s n)
s i = t i
    exact (h i ((length_list_restrict s n) # Hi)).
Defined.

Definition list_restrict_eq_iff_seq_agree_inductive
  {A : Type} {n : nat} {s t : nat -> A}
  : list_restrict s n = list_restrict t n <-> seq_agree_inductive n s t
  := iff_compose
      list_restrict_eq_iff_seq_agree_lt
      seq_agree_lt_iff_seq_agree_inductive.

(** ** Continuity *)

(** Following https://martinescardo.github.io/TypeTopology/TypeTopology.CantorSearch.html#920.  *)

(** A uniformly continuous function takes homotopic sequences to outputs that are equivalent with respect to the structure on [Y]. *)
Definition uniformly_continuous_extensionality
  {X Y : Type} {usY : UStructure Y} (p : (nat -> X) -> Y) {m : nat}
  (c : uniformly_continuous p)
  {u v : nat -> X} (h : u == v)
  : p u =[m] p v
  := (c m).2 u v (fun m _ => h m).

(** Composing a uniformly continuous function with the [cons] operation decreases the modulus by 1. Maybe this can be done with greater generality for the structure on [Y]. *)
Definition cons_decreases_modulus {X Y : Type}
  (p : (nat -> X) -> Y) (n : nat) (b : X)
  (hSn : is_modulus_of_uniform_continuity n.+1 p)
  : is_modulus_of_uniform_continuity n (p o seq_cons b).X, Y: Type
p: (nat -> X) -> Y
n: nat
b: X
hSn: is_modulus_of_uniform_continuity n.+1 p
is_modulus_of_uniform_continuity n (p o seq_cons b)
Proof.X, Y: Type
p: (nat -> X) -> Y
n: nat
b: X
hSn: is_modulus_of_uniform_continuity n.+1 p
is_modulus_of_uniform_continuity n (p o seq_cons b)
  intros u v huv.X, Y: Type
p: (nat -> X) -> Y
n: nat
b: X
hSn: is_modulus_of_uniform_continuity n.+1 p
u, v: nat -> X
huv: u =[n] v
p (seq_cons b u) = p (seq_cons b v)
  apply hSn.X, Y: Type
p: (nat -> X) -> Y
n: nat
b: X
hSn: is_modulus_of_uniform_continuity n.+1 p
u, v: nat -> X
huv: u =[n] v
seq_cons b u =[n.+1] seq_cons b v
  exact (seq_cons_of_eq huv).
Defined.