From e16ad63844fc5c51db37d8330a2b47b3961c4282 Mon Sep 17 00:00:00 2001
From: Ali Caglayan <alizter@gmail.com>
Date: Sun, 14 Apr 2024 18:55:09 +0100
Subject: [PATCH] more list functions + truncation level of lists

Signed-off-by: Ali Caglayan <alizter@gmail.com>

<!-- ps-id: be8baae8-7652-48c2-b90d-d5e4f6748147 -->
---
 theories/Spaces/List.v | 122 ++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 120 insertions(+), 2 deletions(-)

diff --git a/theories/Spaces/List.v b/theories/Spaces/List.v
index b6df01f77ac..5d20dc648ee 100644
--- a/theories/Spaces/List.v
+++ b/theories/Spaces/List.v
@@ -1,8 +1,52 @@
-Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids.
-Require Import Classes.implementations.list.
+Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc.
+Require Import Classes.implementations.list Types.Unit Types.Empty Types.Prod.
+Require Import Modalities.ReflectiveSubuniverse Truncations.Core.
 
 Local Open Scope list_scope.
 
+(** Tail-recursive list reversal. *)
+Fixpoint reverse_acc {A} (acc : list A) (l : list A) : list A :=
+  match l with
+  | nil => acc
+  | x :: l => reverse_acc (x :: acc) l
+  end.
+
+(** Reversing the order of a list. *)
+Definition reverse {A} (l : list A) : list A := reverse_acc nil l.
+
+(** The last element of a list. *)
+Fixpoint last {A} (default : A) (l : list A) : A :=
+  match l with
+  | nil => default
+  | _ :: l => last default l
+  end.
+
+(** The [n]-th element of a list. *)
+Fixpoint nth {A} (l : list A) (n : nat) (default : A) : A :=
+  match n, l with
+  | O, x :: _ => x
+  | S n, _ :: l => nth l n default
+  | _, _ => default
+  end.
+
+(** Remove the last element of a list and do nothing if empty. *)
+Fixpoint remove_last {A} (l : list A) : list A :=
+  match l with
+  | nil => nil
+  | _ :: nil => nil
+  | x :: l => x :: remove_last l
+  end.
+
+(** Descending sequence of natural numbers starting from [n.-1]. *)
+Fixpoint seq_rev (n : nat) : list nat :=
+    match n with
+    | O => nil
+    | S n => n :: seq_rev n
+    end.
+
+(** Ascending sequence of natural numbers [< n]. *)
+Definition seq (n : nat) : list nat := reverse (seq_rev n).
+
 (** ** Lemmas about lists *)
 
 (** Note that [list] is currently defined in Basics.Datatypes. *)
@@ -69,3 +113,77 @@ Proof.
     lhs_V nrapply ap_compose.
     nrapply (ap_compose (fun l => l ++ z)).
 Defined.
+
+(** ** Path spaces of lists *)
+
+(** This proof was adapted from a proof givaen in agda/cubical by Evan Cavallo. *)
+
+Section PathList.
+  Context {A : Type}.
+  
+  (** This type is equivalent to the path space of lists. We don't actually show that it is equivalent to the type of paths but rather that it is a retract of it. This is sufficient to determine the h-level of the type of lists. *)
+  Fixpoint ListEq (l l' : list A) : Type :=
+    match l, l' with
+      | nil, nil => Unit
+      | cons x xs, cons x' xs' => (x = x') * ListEq xs xs'
+      | _, _ => Empty
+    end.
+
+  Global Instance reflexive_listeq : Reflexive ListEq. 
+  Proof.
+    intros l.
+    induction l as [| a l IHl].
+    - exact tt.
+    - by split.
+  Defined.
+
+  Local Definition encode {l1 l2} (p : l1 = l2) : ListEq l1 l2.
+  Proof.
+    by destruct p.
+  Defined.
+
+  Local Definition decode {l1 l2} (q : ListEq l1 l2) : l1 = l2.
+  Proof.
+    induction l1 as [| a l1 IHl1 ] in l2, q |- *.
+    1: by destruct l2.
+    destruct l2.
+    1: contradiction.
+    destruct q as [p q].
+    exact (ap011 (cons (A:=_)) p (IHl1 _ q)).
+  Defined.
+
+  Local Definition decode_refl {l} : decode (reflexivity l) = idpath.
+  Proof.
+    induction l.
+    1: reflexivity.
+    exact (ap02 (cons a) IHl).
+  Defined.
+
+  Local Definition decode_encode {l1 l2} (p : l1 = l2)
+    : decode (encode p) = p.
+  Proof.
+    destruct p.
+    apply decode_refl.
+  Defined.
+
+  (** By case analysis on both lists, it's easy to show that [ListEq] is n.+1-truncated if [A] is n.+2-truncated. *)
+  Global Instance istrunc_listeq n {l1 l2} {H : IsTrunc n.+2 A}
+    : IsTrunc n.+1 (ListEq l1 l2).
+  Proof.
+    induction l1 in l2 |- *.
+    - destruct l2.
+      1,2: exact _.
+    - destruct l2.
+      1: exact _.
+      rapply istrunc_prod.
+  Defined.
+
+  (** Since [ListEq] is a retract of the path space of lists, the latter is n.+1-truncated hence [list A] is n.+2-truncated. *)
+  Global Instance istrunc_list n {H : IsTrunc n.+2 A} : IsTrunc n.+2 (list A).
+  Proof.
+    apply istrunc_S.
+    intros x y.
+    rapply (inO_retract_inO n.+1 _ _ encode decode decode_encode).
+  Defined.
+
+End PathList.