From 926cf8cc5cd103b6daa072f9f45f2e479e2c9fce Mon Sep 17 00:00:00 2001 From: thchatzidiamantis Date: Fri, 31 Jan 2025 16:10:26 -0500 Subject: [PATCH 1/3] Uniform structures --- theories/Misc/UStructures.v | 81 +++++++++++++++++++++++++++++++++++++ 1 file changed, 81 insertions(+) create mode 100644 theories/Misc/UStructures.v diff --git a/theories/Misc/UStructures.v b/theories/Misc/UStructures.v new file mode 100644 index 0000000000..e0f026a394 --- /dev/null +++ b/theories/Misc/UStructures.v @@ -0,0 +1,81 @@ +(** * Uniform Structures *) + +Require Import Basics Types. +Require Import Truncations.Core. +Require Import Spaces.Nat.Core. + +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). + +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). From c557c79a5f42a2e0205b804583b2b6bf7465ecbc Mon Sep 17 00:00:00 2001 From: thchatzidiamantis Date: Fri, 31 Jan 2025 16:10:34 -0500 Subject: [PATCH 2/3] Sequences --- theories/Spaces/List/Theory.v | 10 ++-- theories/Spaces/NatSeq/Core.v | 75 ++++++++++++++++++++++++++ theories/Spaces/NatSeq/UStructure.v | 81 +++++++++++++++++++++++++++++ 3 files changed, 161 insertions(+), 5 deletions(-) create mode 100644 theories/Spaces/NatSeq/Core.v create mode 100644 theories/Spaces/NatSeq/UStructure.v diff --git a/theories/Spaces/List/Theory.v b/theories/Spaces/List/Theory.v index 37495255f8..8a334dbb99 100644 --- a/theories/Spaces/List/Theory.v +++ b/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. diff --git a/theories/Spaces/NatSeq/Core.v b/theories/Spaces/NatSeq/Core.v new file mode 100644 index 0000000000..1b9c15a2ed --- /dev/null +++ b/theories/Spaces/NatSeq/Core.v @@ -0,0 +1,75 @@ +(** * Types of Sequences [nat -> X] *) + +Require Import Basics Types. +Require Import Spaces.Nat.Core. + +Open Scope nat_scope. +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). diff --git a/theories/Spaces/NatSeq/UStructure.v b/theories/Spaces/NatSeq/UStructure.v new file mode 100644 index 0000000000..f3631c3921 --- /dev/null +++ b/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. + +Open Scope nat_scope. +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. From e5faee1be4e41b75f10e71c4ea7d0bf2c8bd6a5a Mon Sep 17 00:00:00 2001 From: thchatzidiamantis Date: Sat, 1 Feb 2025 11:55:51 -0500 Subject: [PATCH 3/3] Fix scope, notation --- theories/Misc/UStructures.v | 5 +++-- theories/Spaces/NatSeq/Core.v | 4 ++-- theories/Spaces/NatSeq/UStructure.v | 4 ++-- 3 files changed, 7 insertions(+), 6 deletions(-) diff --git a/theories/Misc/UStructures.v b/theories/Misc/UStructures.v index e0f026a394..f7b6ccd962 100644 --- a/theories/Misc/UStructures.v +++ b/theories/Misc/UStructures.v @@ -4,7 +4,7 @@ Require Import Basics Types. Require Import Truncations.Core. Require Import Spaces.Nat.Core. -Open Scope nat_scope. +Local Open Scope nat_scope. (** ** [nat]-graded uniform structures *) @@ -19,7 +19,8 @@ Class UStructure (us_type : Type) := { Existing Instances us_reflexive us_symmetric us_transitive. -Notation "u =[ n ] v" := (us_rel n u v) (at level 70). +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) diff --git a/theories/Spaces/NatSeq/Core.v b/theories/Spaces/NatSeq/Core.v index 1b9c15a2ed..35ce42e1ae 100644 --- a/theories/Spaces/NatSeq/Core.v +++ b/theories/Spaces/NatSeq/Core.v @@ -3,8 +3,8 @@ Require Import Basics Types. Require Import Spaces.Nat.Core. -Open Scope nat_scope. -Open Scope type_scope. +Local Open Scope nat_scope. +Local Open Scope type_scope. (** ** Operations on sequences *) diff --git a/theories/Spaces/NatSeq/UStructure.v b/theories/Spaces/NatSeq/UStructure.v index f3631c3921..0305c3c0ef 100644 --- a/theories/Spaces/NatSeq/UStructure.v +++ b/theories/Spaces/NatSeq/UStructure.v @@ -6,8 +6,8 @@ Require Import Misc.UStructures. Require Import List.Core List.Theory. Require Import Spaces.NatSeq.Core. -Open Scope nat_scope. -Open Scope type_scope. +Local Open Scope nat_scope. +Local Open Scope type_scope. (** ** [UStructure] defined by [seq_agree_lt] *)