Sequences, uniform structures

theories/Misc/UStructures.v

@@ -0,0 +1,82 @@
+(** * Uniform Structures *)
+
+Require Import Basics Types.
+Require Import Truncations.Core.
+Require Import Spaces.Nat.Core.
+
+Local Open Scope nat_scope.
+
+(** ** [nat]-graded uniform structures *)
+
+(** A uniform structure on a type consists of an equivalence relation for every natural number, each one being stronger than its predecessor. *)
+Class UStructure (us_type : Type) := {
+  us_rel : nat -> Relation us_type;
+  us_reflexive : forall n : nat, Reflexive (us_rel n);
+  us_symmetric : forall n : nat, Symmetric (us_rel n);
+  us_transitive : forall n : nat, Transitive (us_rel n);
+  us_pred : forall (n : nat) (x y : us_type), us_rel n.+1 x y -> us_rel n x y
+}.
+
+Existing Instances us_reflexive us_symmetric us_transitive.
+
+Notation "u =[ n ] v" := (us_rel n u v)
+  (at level 70, format "u  =[ n ]  v").
+
+Definition us_rel_leq {X : Type} {struct : UStructure X}
+  {m n : nat} (hm : m <= n) {u v : X} (h : u =[n] v)
+  : u =[m] v.
+Proof.
+  induction hm.
+  - assumption.
+  - apply IHhm.
+    by apply us_pred.
+Defined.
+
+(** Every type admits the trivial uniform structure with the standard identity type on every level. *)
+Global Instance trivial_us {X : Type} : UStructure X | 100.
+Proof.
+  srapply (Build_UStructure _ (fun n x y => (x = y))).
+  exact (fun _ _ _ => idmap).
+Defined.
+
+(** Example of a uniform structures based on truncations, with the relation being the [n-2]-truncation of the identity type. *)
+Definition trunc_us {X : Type} : UStructure X.
+Proof.
+  srapply (Build_UStructure X
+            (fun n x y => Tr (trunc_index_inc (-2) n) (x = y))).
+  - intros n x. exact (tr idpath).
+  - intros n x y h; strip_truncations.
+    exact (tr h^).
+  - intros n x y z h1 h2; strip_truncations.
+    exact (tr (h1 @ h2)).
+  - intros n x y h; strip_truncations.
+    exact (tr h).
+Defined.
+
+(** ** Continuity *)
+
+(** Definition of a continuous function depending on two uniform structures. *)
+Definition IsContinuous
+  {X Y : Type} {usX : UStructure X} {usY : UStructure Y} (p : X -> Y)
+  := forall (u : X) (m : nat),
+      {n : nat & forall v : X, u =[n] v -> p u =[m] p v}.
+
+Definition uniformly_continuous {X Y : Type}
+  {usX : UStructure X} {usY : UStructure Y} (p : X -> Y)
+  := forall (m : nat),
+      {n : nat & forall u v : X, u =[n] v -> p u =[m] p v}.
+
+(** In the case that the target has the trivial uniform structure, it is useful to state uniform continuity by providing the specific modulus, which now only depends on the function. *)
+Definition is_modulus_of_uniform_continuity {X Y : Type} {usX : UStructure X}
+  (n : nat) (p : X -> Y)
+  := forall u v : X, u =[n] v -> p u = p v.
+
+Definition uniformly_continuous_has_modulus {X Y :Type} {usX : UStructure X}
+  {p : X -> Y} {n : nat} (c : is_modulus_of_uniform_continuity n p)
+  : uniformly_continuous p
+  := fun m => (n; c).
+
+Definition iscontinuous_uniformly_continuous {X Y : Type}
+  {usX : UStructure X} {usY : UStructure Y} (p : X -> Y)
+  : uniformly_continuous p -> IsContinuous p
+  := fun uc u m => ((uc m).1 ; fun v => (uc m).2 u v).

theories/Spaces/List/Theory.v

@@ -990,12 +990,12 @@ Definition length_list_restrict {A : Type} (s : nat -> A) (n : nat)
   := length_Build_list _ _.
 
 (** [nth'] of the restriction of a sequence is the corresponding term of the sequence.  *)
-Definition nth'_list_restrict {A : Type} (s : nat -> A) (n : nat)
-  {i : nat} (Hi : i < n) (Hi' : i < length (list_restrict s n))
-  : nth' (list_restrict s n) i Hi' = s i.
+Definition nth'_list_restrict {A : Type} (s : nat -> A) {n : nat}
+  {i : nat} (Hi : i < length (list_restrict s n))
+  : nth' (list_restrict s n) i Hi = s i.
 Proof.
-  unshelve lhs snrefine (nth'_list_map _ _ _ (_^ # Hi) _).
-  - nrapply length_seq'.
+  unshelve lhs snrapply nth'_list_map.
+  - exact ((length_list_restrict _ _ @ (length_seq' n)^) # Hi).
   - exact (ap s (nth'_seq' _ _ _)).
 Defined.
 

theories/Spaces/NatSeq/Core.v

@@ -0,0 +1,75 @@
+(** * Types of Sequences [nat -> X] *)
+
+Require Import Basics Types.
+Require Import Spaces.Nat.Core.
+
+Local Open Scope nat_scope.
+Local Open Scope type_scope.
+
+(** ** Operations on sequences *)
+
+(** The first term of a sequence. *)
+Definition head {X : Type} (u : nat -> X) : X := u 0.
+
+(** Shift of a sequence by 1 to the left. *)
+Definition tail {X : Type} (u : nat -> X) : (nat -> X) := u o S.
+
+(** Add a term to the start of a sequence. *)
+Definition cons {X : Type} : X -> (nat -> X) -> (nat -> X).
+Proof.
+  intros x u [|n].
+  - exact x.
+  - exact (u n).
+Defined.
+
+Definition cons_head_tail {X : Type} (u : nat -> X)
+  : cons (head u) (tail u) == u.
+Proof.
+  by intros [|n].
+Defined.
+
+Definition tail_cons {X : Type} (u : nat -> X) {x : X} : tail (cons x u) == u
+  := fun _ => idpath.
+
+(** ** Equivalence relations on sequences.  *)
+
+(** For every [n : nat], we define a relation between two sequences that holds if and only if their first [n] terms are equal. *)
+Definition seq_agree_lt {X : Type} (n : nat) (s t : nat -> X) : Type
+  := forall (m : nat), m < n -> s m = t m.
+
+(** [seq_agree_lt] has an equivalent inductive definition. We don't use this equivalence, but include it in case it is useful in future work. *)
+Definition seq_agree_inductive {X : Type} (n : nat) (s t : nat -> X) : Type.
+Proof.
+  induction n in s, t |-*.
+  - exact Unit.
+  - exact ((head s = head t) * (IHn (tail s) (tail t))).
+Defined.
+
+Definition seq_agree_inductive_seq_agree_lt {X : Type} {n : nat}
+  {s t : nat -> X} (h : seq_agree_lt n s t)
+  : seq_agree_inductive n s t.
+Proof.
+  induction n in s, t, h |- *.
+  - exact tt.
+  - simpl.
+    exact (h 0 _, IHn _ _ (fun m hm => h m.+1 (_ hm))).
+Defined.
+
+Definition seq_agree_lt_seq_agree_inductive {X : Type} {n : nat}
+  {s t : nat -> X} (h : seq_agree_inductive n s t)
+  : seq_agree_lt n s t.
+Proof.
+  intros m hm.
+  induction m in n, s, t, h, hm |- *.
+  - revert n hm h; nrapply gt_zero_ind; intros n h.
+    exact (fst h).
+  - induction n.
+    + contradiction (not_lt_zero_r _ hm).
+    + exact (IHm _ (tail s) (tail t) (snd h) _).
+Defined.
+
+Definition seq_agree_lt_iff_seq_agree_inductive
+  {X : Type} {n : nat} {s t : nat -> X}
+  : seq_agree_lt n s t <-> seq_agree_inductive n s t
+  := (fun h => seq_agree_inductive_seq_agree_lt h,
+      fun h => seq_agree_lt_seq_agree_inductive h).

theories/Spaces/NatSeq/UStructure.v

@@ -0,0 +1,81 @@
+(** * Uniform structure on types of sequences *)
+
+Require Import Basics Types.
+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]. *)
+Global Instance sequence_type_us' {X : Type} : UStructure (nat -> X) | 10.
+Proof.
+  snrapply Build_UStructure.
+  - exact seq_agree_lt.
+  - exact (fun _ _ _ _ => idpath).
+  - exact (fun _ _ _ h _ _ => (h _ _)^).
+  - exact (fun _ _ _ _ h1 h2 _ _ => ((h1 _ _) @ (h2 _ _))).
+  - exact (fun _ _ _ h _ _ => h _ _).
+Defined.
+
+Definition cons_of_eq {X : Type} {n : nat} {s t : nat -> X} {x : X}
+  (h : s =[n] t)
+  : (cons x s) =[n.+1] (cons x t).
+Proof.
+  intros m hm; destruct m.
+  - reflexivity.
+  - 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.
+Proof.
+  constructor.
+  - intros h m hm.
+    lhs_V srapply (nth'_list_restrict s ((length_list_restrict _ _)^ # hm)).
+    rhs_V srapply (nth'_list_restrict t ((length_list_restrict _ _)^ # hm)).
+    exact (nth'_path_list h _ _).
+  - intro h.
+    apply (path_list_nth' _ _
+            (length_list_restrict s n @ (length_list_restrict t n)^)).
+    intros i Hi.
+    lhs snrapply nth'_list_restrict.
+    rhs snrapply nth'_list_restrict.
+    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 cons b).
+Proof.
+  intros u v huv.
+  apply hSn.
+  exact (cons_of_eq huv).
+Defined.