Merge pull request #2138 from Alizter/ps/rr/reduce_universes_in_finnat

cleanup in FinNat
HoTT · Nov 17, 2024 · 0200dde · 0200dde
2 parents 6647f3a + 7567113
commit 0200dde
Show file tree

Hide file tree

Showing 4 changed files with 86 additions and 129 deletions.
diff --git a/theories/Algebra/Universal/Operation.v b/theories/Algebra/Universal/Operation.v
@@ -157,10 +157,10 @@ Proof.
   intro i.
   induction i using fin_ind; intros ss N a.
   - unfold cons_dom'.
-    rewrite compute_fin_ind_fin_zero.
+    rewrite fin_ind_beta_zero.
     reflexivity.
   - unfold cons_dom'.
-    by rewrite compute_fin_ind_fsucc.
+    by rewrite fin_ind_beta_fsucc.
 Qed.
 
 Lemma expand_cons_dom `{Funext} {σ} (A : Carriers σ)
@@ -196,10 +196,10 @@ Proof.
   funext a'.
   simpl.
   unfold cons_dom, cons_dom'.
-  rewrite compute_fin_ind_fin_zero.
+  rewrite fin_ind_beta_zero.
   refine (ap (operation_uncurry A (fstail ss) t (a x)) _).
   funext i'.
-  by rewrite compute_fin_ind_fsucc.
+  by rewrite fin_ind_beta_fsucc.
 Qed.
 
 Global Instance isequiv_operation_curry `{Funext} {σ} (A : Carriers σ)

diff --git a/theories/Spaces/Finite/FinInduction.v b/theories/Spaces/Finite/FinInduction.v
@@ -22,7 +22,7 @@ Proof.
     by apply s.
 Defined.
 
-Lemma compute_fin_ind_fin_zero (P : forall n : nat, Fin n -> Type)
+Lemma fin_ind_beta_zero (P : forall n : nat, Fin n -> Type)
   (z : forall n : nat, P n.+1 fin_zero)
   (s : forall (n : nat) (k : Fin n), P n k -> P n.+1 (fsucc k)) (n : nat)
   : fin_ind P z s fin_zero = z n.
@@ -33,10 +33,10 @@ Proof.
   intro p.
   destruct (hset_path2 1 p).
   lhs nrapply transport_1.
-  nrapply compute_finnat_ind_zero.
+  nrapply finnat_ind_beta_zero.
 Defined.
 
-Lemma compute_fin_ind_fsucc (P : forall n : nat, Fin n -> Type)
+Lemma fin_ind_beta_fsucc (P : forall n : nat, Fin n -> Type)
   (z : forall n : nat, P n.+1 fin_zero)
   (s : forall (n : nat) (k : Fin n), P n k -> P n.+1 (fsucc k))
   {n : nat} (k : Fin n)
@@ -46,7 +46,7 @@ Proof.
   generalize (path_fin_to_finnat_to_fin (fsucc k)).
   induction (path_fin_to_finnat_fsucc k)^.
   intro p.
-  refine (ap (transport (P n.+1) p) (compute_finnat_ind_succ _ _ _ _) @ _).
+  refine (ap (transport (P n.+1) p) (finnat_ind_beta_succ _ _ _ _) @ _).
   generalize dependent p.
   induction (path_fin_to_finnat_to_fin k).
   induction (path_fin_to_finnat_to_fin k)^.
@@ -60,20 +60,20 @@ Definition fin_rec (B : nat -> Type)
     forall {n : nat}, Fin n -> B n
   := fin_ind (fun n _ => B n).
 
-Lemma compute_fin_rec_fin_zero (B : nat -> Type)
+Lemma fin_rec_beta_zero (B : nat -> Type)
   (z : forall n : nat, B n.+1)
   (s : forall (n : nat) (k : Fin n), B n -> B n.+1) (n : nat)
   : fin_rec B z s fin_zero = z n.
 Proof.
-  apply (compute_fin_ind_fin_zero (fun n _ => B n)).
+  apply (fin_ind_beta_zero (fun n _ => B n)).
 Defined.
 
-Lemma compute_fin_rec_fsucc (B : nat -> Type)
+Lemma fin_rec_beta_fsucc (B : nat -> Type)
   (z : forall n : nat, B n.+1)
   (s : forall (n : nat) (k : Fin n), B n -> B n.+1)
   {n : nat} (k : Fin n)
   : fin_rec B z s (fsucc k) = s n k (fin_rec B z s k).
 Proof.
-  apply (compute_fin_ind_fsucc (fun n _ => B n)).
+  apply (fin_ind_beta_fsucc (fun n _ => B n)).
 Defined.
 
diff --git a/theories/Spaces/Finite/FinNat.v b/theories/Spaces/Finite/FinNat.v
@@ -1,108 +1,84 @@
-Require Import
-  HoTT.Basics
-  HoTT.Types
-  HoTT.Universes.HSet
-  HoTT.Spaces.Nat.Core
-  HoTT.Spaces.Finite.Fin.
+Require Import Basics.Overture Basics.Tactics Basics.Trunc Basics.PathGroupoids
+  Basics.Equivalences Basics.Decidable Basics.Classes.
+Require Import Types.Empty Types.Sigma Types.Sum Types.Prod Types.Equiv.
+Require Import Spaces.Nat.Core.
+Require Import Finite.Fin.
 
 Local Open Scope nat_scope.
 
-Definition FinNat (n : nat) : Type0 := {x : nat | x < n}.
+Set Universe Minimization ToSet.
 
-Definition zero_finnat (n : nat) : FinNat n.+1
-  := (0; _ : 0 < n.+1).
+Definition FinNat@{} (n : nat) : Type0 := {x : nat | x < n}.
 
-Lemma path_zero_finnat (n : nat) (h : 0 < n.+1) : zero_finnat n = (0; h).
-Proof.
-  by apply path_sigma_hprop.
-Defined.
+Definition zero_finnat@{} (n : nat) : FinNat n.+1
+  := (0; _ : 0 < n.+1).
 
-Definition succ_finnat {n : nat} (u : FinNat n) : FinNat n.+1
+Definition succ_finnat@{} {n : nat} (u : FinNat n) : FinNat n.+1
   := (u.1.+1; leq_succ u.2).
 
-Lemma path_succ_finnat {n : nat} (u : FinNat n) (h : u.1.+1 < n.+1)
-  : succ_finnat u = (u.1.+1; h).
+Definition path_succ_finnat {n : nat} (x : nat) (h : x.+1 < n.+1)
+  : succ_finnat (x; leq_pred' h) = (x.+1; h).
 Proof.
   by apply path_sigma_hprop.
 Defined.
 
-Definition last_finnat (n : nat) : FinNat n.+1
+Definition last_finnat@{} (n : nat) : FinNat n.+1
   := exist (fun x => x < n.+1) n (leq_refl n.+1).
 
-Lemma path_last_finnat (n : nat) (h : n < n.+1)
-  : last_finnat n = (n; h).
-Proof.
-  by apply path_sigma_hprop.
-Defined.
-
-Definition incl_finnat {n : nat} (u : FinNat n) : FinNat n.+1
+Definition incl_finnat@{} {n : nat} (u : FinNat n) : FinNat n.+1
   := (u.1; leq_trans u.2 (leq_succ_r (leq_refl n))).
 
-Lemma path_incl_finnat (n : nat) (u : FinNat n) (h : u.1 < n.+1)
-  : incl_finnat u = (u.1; h).
-Proof.
-  by apply path_sigma_hprop.
-Defined.
-
-Definition finnat_ind (P : forall n : nat, FinNat n -> Type)
+Definition finnat_ind@{u} (P : forall n : nat, FinNat n -> Type@{u})
   (z : forall n : nat, P n.+1 (zero_finnat n))
   (s : forall (n : nat) (u : FinNat n), P n u -> P n.+1 (succ_finnat u))
   {n : nat} (u : FinNat n)
   : P n u.
 Proof.
-  induction n as [| n IHn].
+  simple_induction n n IHn; intro u.
   - elim (not_lt_zero_r u.1 u.2).
   - destruct u as [x h].
     destruct x as [| x].
-    + exact (transport (P n.+1) (path_zero_finnat _ h) (z _)).
-    + refine (transport (P n.+1) (path_succ_finnat (x; leq_pred' h) _) _).
+    + nrefine (transport (P n.+1) _ (z _)).
+      by apply path_sigma_hprop.
+    + refine (transport (P n.+1) (path_succ_finnat _ _) _).
       apply s. apply IHn.
 Defined.
 
-Lemma compute_finnat_ind_zero (P : forall n : nat, FinNat n -> Type)
+Definition finnat_ind_beta_zero@{u} (P : forall n : nat, FinNat n -> Type@{u})
   (z : forall n : nat, P n.+1 (zero_finnat n))
   (s : forall (n : nat) (u : FinNat n), P n u -> P n.+1 (succ_finnat u))
   (n : nat)
   : finnat_ind P z s (zero_finnat n) = z n.
 Proof.
-  unshelve lhs snrapply transport2.
-  - reflexivity.
-  - rapply hset_path2.
-  - reflexivity.
+  snrapply (transport2 _ (q:=idpath@{Set})).
+  rapply path_ishprop.
 Defined.
 
-Lemma compute_finnat_ind_succ (P : forall n : nat, FinNat n -> Type)
+Definition finnat_ind_beta_succ@{u} (P : forall n : nat, FinNat n -> Type@{u})
   (z : forall n : nat, P n.+1 (zero_finnat n))
   (s : forall (n : nat) (u : FinNat n),
        P n u -> P n.+1 (succ_finnat u))
   {n : nat} (u : FinNat n)
   : finnat_ind P z s (succ_finnat u) = s n u (finnat_ind P z s u).
 Proof.
-  refine
-    (_ @ transport
-          (fun p => transport _ p (s n u _) = s n u (finnat_ind P z s u))
-          (hset_path2 1 (path_succ_finnat u (leq_succ u.2))) 1).
-  destruct u as [u1 u2].
-  assert (u2 = leq_pred' (leq_succ u2)) as p by apply path_ishprop.
-  simpl; by induction p.
+  destruct u as [u1 u2]; simpl; unfold path_succ_finnat.
+  destruct (path_ishprop u2 (leq_pred' (leq_succ u2))).
+  refine (transport2 _ (q:=idpath@{Set}) _ _).
+  rapply path_ishprop.
 Defined.
 
-Monomorphic Definition is_bounded_fin_to_nat {n} (k : Fin n)
+Definition is_bounded_fin_to_nat@{} {n} (k : Fin n)
   : fin_to_nat k < n.
 Proof.
   induction n as [| n IHn].
   - elim k.
-  - destruct k as [k | []].
-    + apply (@leq_trans _ n _).
-      * apply IHn.
-      * by apply leq_succ_r.
-    + apply leq_refl.
+  - destruct k as [k | []]; exact _.
 Defined.
 
-Monomorphic Definition fin_to_finnat {n} (k : Fin n) : FinNat n
+Definition fin_to_finnat {n} (k : Fin n) : FinNat n
   := (fin_to_nat k; is_bounded_fin_to_nat k).
 
-Monomorphic Fixpoint finnat_to_fin {n : nat} : FinNat n -> Fin n
+Fixpoint finnat_to_fin@{} {n : nat} : FinNat n -> Fin n
   := match n with
      | 0 => fun u => Empty_rec (not_lt_zero_r _ u.2)
      | n.+1 => fun u =>
@@ -112,65 +88,47 @@ Monomorphic Fixpoint finnat_to_fin {n : nat} : FinNat n -> Fin n
         end
      end.
 
-Lemma path_fin_to_finnat_fsucc {n : nat} (k : Fin n)
+Definition path_fin_to_finnat_fsucc@{} {n : nat} (k : Fin n)
   : fin_to_finnat (fsucc k) = succ_finnat (fin_to_finnat k).
 Proof.
   apply path_sigma_hprop.
   apply path_nat_fsucc.
 Defined.
 
-Lemma path_fin_to_finnat_fin_zero (n : nat)
+Definition path_fin_to_finnat_fin_zero@{} (n : nat)
   : fin_to_finnat (@fin_zero n) = zero_finnat n.
 Proof.
   apply path_sigma_hprop.
   apply path_nat_fin_zero.
 Defined.
 
-Lemma path_fin_to_finnat_fin_incl {n : nat} (k : Fin n)
-  : fin_to_finnat (fin_incl k) = incl_finnat (fin_to_finnat k).
-Proof.
-  reflexivity.
-Defined.
-
-Lemma path_fin_to_finnat_fin_last (n : nat)
-  : fin_to_finnat (@fin_last n) = last_finnat n.
-Proof.
-  reflexivity.
-Defined.
-
-Lemma path_finnat_to_fin_succ {n : nat} (u : FinNat n)
+Definition path_finnat_to_fin_succ@{} {n : nat} (u : FinNat n)
   : finnat_to_fin (succ_finnat u) = fsucc (finnat_to_fin u).
 Proof.
   cbn. do 2 f_ap. by apply path_sigma_hprop.
 Defined.
 
-Lemma path_finnat_to_fin_zero (n : nat)
-  : finnat_to_fin (zero_finnat n) = fin_zero.
-Proof.
-  reflexivity.
-Defined.
-
-Lemma path_finnat_to_fin_incl {n : nat} (u : FinNat n)
+Definition path_finnat_to_fin_incl@{} {n : nat} (u : FinNat n)
   : finnat_to_fin (incl_finnat u) = fin_incl (finnat_to_fin u).
 Proof.
-  induction n as [| n IHn].
-  - elim (not_lt_zero_r _ u.2).
-  - destruct u as [x h].
-    destruct x as [| x]; [reflexivity|].
-    refine ((ap _ (ap _ (path_succ_finnat (x; leq_pred' h) h)))^ @ _).
-    refine (_ @ ap fsucc (IHn (x; leq_pred' h))).
-    by induction (path_finnat_to_fin_succ (incl_finnat (x; leq_pred' h))).
+  revert n u.
+  snrapply finnat_ind.
+  1: reflexivity.
+  intros n u; cbn beta; intros p.
+  lhs nrapply (path_finnat_to_fin_succ (incl_finnat u)).
+  lhs nrapply (ap fsucc p).
+  exact (ap fin_incl (path_finnat_to_fin_succ _))^.
 Defined.
 
-Lemma path_finnat_to_fin_last (n : nat)
+Definition path_finnat_to_fin_last@{} (n : nat)
   : finnat_to_fin (last_finnat n) = fin_last.
 Proof.
   induction n as [| n IHn].
   - reflexivity.
   - exact (ap fsucc IHn).
 Defined.
 
-Lemma path_finnat_to_fin_to_finnat {n : nat} (u : FinNat n)
+Definition path_finnat_to_fin_to_finnat@{} {n : nat} (u : FinNat n)
   : fin_to_finnat (finnat_to_fin u) = u.
 Proof.
   induction n as [| n IHn].
@@ -183,7 +141,7 @@ Proof.
       exact (ap S (IHn (x; leq_pred' h))..1).
 Defined.
 
-Lemma path_fin_to_finnat_to_fin {n : nat} (k : Fin n)
+Definition path_fin_to_finnat_to_fin@{} {n : nat} (k : Fin n)
   : finnat_to_fin (fin_to_finnat k) = k.
 Proof.
   induction n as [| n IHn].
@@ -195,8 +153,7 @@ Proof.
     + apply path_finnat_to_fin_last.
 Defined.
 
-Definition equiv_fin_finnat (n : nat) : Fin n <~> FinNat n
+Definition equiv_fin_finnat@{} (n : nat) : Fin n <~> FinNat n
   := equiv_adjointify fin_to_finnat finnat_to_fin
       path_finnat_to_fin_to_finnat
       path_fin_to_finnat_to_fin.
-