Nat: direct proof of Dec Paths; move equiv_path_nat to Nat/Paths.v

contrib/HoTTBook.v

@@ -58,7 +58,7 @@
 *)
 
 From HoTT Require Import Basics Truncations.
-From HoTT Require Idempotents Spaces.Spheres Spaces.No.
+From HoTT Require Idempotents Spaces.Spheres Spaces.No Spaces.Nat.
 From HoTT Require HIT.V HIT.Flattening Homotopy.WhiteheadsPrinciple Homotopy.Hopf.
 From HoTT Require Categories.
 From HoTT Require Metatheory.IntervalImpliesFunext Metatheory.UnivalenceImpliesFunext.
@@ -309,7 +309,7 @@ Definition Book_2_12_5 := @HoTT.Types.Sum.equiv_path_sum.
 (* ================================================== thm:path-nat *)
 (** Theorem 2.13.1 *)
 
-Definition Book_2_13_1 := @HoTT.Spaces.Nat.Core.equiv_path_nat.
+Definition Book_2_13_1 := @HoTT.Spaces.Nat.Paths.equiv_path_nat.
 
 (* ================================================== thm:prod-ump *)
 (** Theorem 2.15.2 *)

theories/Classes/implementations/binary_naturals.v

@@ -1,5 +1,5 @@
 Require Import
-        HoTT.Spaces.Nat.
+        HoTT.Spaces.Nat.Core.
 Require Import
         HoTT.Tactics.
 Require Import

theories/Classes/implementations/ne_list.v

@@ -2,7 +2,7 @@ Require Import
   HoTT.Utf8Minimal
   HoTT.Classes.implementations.list
   HoTT.Basics.Overture
-  HoTT.Spaces.Nat.
+  HoTT.Spaces.Nat.Core.
 
 Local Open Scope nat_scope.
 Local Open Scope type_scope.

theories/Spaces/Finite/Fin.v

@@ -423,7 +423,8 @@ Fixpoint fin_nat {n : nat} (m : nat) : Fin n.+1
 
 (** The 1-dimensional version of Sperner's lemma says that given any finite sequence of decidable hProps, where the sequence starts with true and ends with false, we can find a point in the sequence where the sequence changes from true to false. This is like a discrete intermediate value theorem. *)
 Fixpoint sperners_lemma_1d {n} :
-  forall (f : Fin (n.+2) -> DHProp)
+  forall (f : Fin (n.+2) -> Type)
+         {dprop : forall i, Decidable (f i)}
          (left_true : f fin_zero)
          (right_false : ~ f fin_last),
     {k : Fin n.+1 & f (fin_incl k) /\ ~ f (fsucc k)}.
@@ -433,7 +434,7 @@ Proof.
   - exists fin_zero. split; assumption.
   - destruct (dec (f (fin_incl fin_last))) as [prev_true|prev_false].
     + exists fin_last. split; assumption.
-    + destruct (sperners_lemma_1d _ (f o fin_incl) left_true prev_false) as [k' [fleft fright]].
+    + destruct (sperners_lemma_1d _ (f o fin_incl) _ left_true prev_false) as [k' [fleft fright]].
       exists (fin_incl k').
       split; assumption.
 Defined.

theories/Spaces/Nat.v

@@ -1,2 +1,5 @@
+(** Nat.Paths has many dependencies, so if you do not need it, it is better to explicitly require only those files that you need. *)
+
 Require Export Nat.Core.
 Require Export Nat.Arithmetic.
+Require Export Nat.Paths.

theories/Spaces/Nat/Arithmetic.v

@@ -209,6 +209,13 @@ Proof.
   destruct (nat_add_comm m n). exact (add_n_sub_n_eq m n).
 Defined.
 
+Lemma summand_is_sub k m n (p : k + n = m) : k = m - n.
+Proof.
+  destruct p.
+  symmetry.
+  apply add_n_sub_n_eq.
+Defined.
+
 Proposition n_lt_m_n_leq_m { n m : nat } : n < m -> n <= m.
 Proof.
   intro H. apply leq_S, leq_S_n in H; exact H.
@@ -349,6 +356,24 @@ Defined.
 #[export] Hint Rewrite -> natminuspluseq : nat.
 #[export] Hint Rewrite -> natminuspluseq' : nat.
 
+Lemma equiv_leq_add n m
+  : leq n m <~> exists k, k + n = m.
+Proof.
+  srapply equiv_iff_hprop.
+  - apply hprop_allpath.
+    intros [x p] [y q].
+    pose (r := summand_is_sub x _ _ p @ (summand_is_sub y _ _ q)^).
+    destruct r.
+    apply ap.
+    apply path_ishprop.
+  - intros p.
+    exists (m - n).
+    apply natminuspluseq, p.
+  - intros [k p].
+    destruct p.
+    apply leq_add.
+Defined.
+
 #[export] Hint Resolve leq_S_n' : nat.
 
 Ltac leq_S_n_in_hypotheses :=

theories/Spaces/Nat/Core.v

@@ -1,7 +1,6 @@
 (* -*- mode: coq; mode: visual-line -*- *)
-Require Import Basics Types.
+Require Import Basics.
 Require Export Basics.Nat.
-Require Export HoTT.DProp.
 
 Local Set Universe Minimization ToSet.
 
@@ -297,47 +296,19 @@ Notation mul_succ_r_reverse := mul_n_Sm (only parsing).
 
 (** *** Boolean equality and its properties *)
 
-Fixpoint code_nat (m n : nat) {struct m} : DHProp@{Set} :=
-  match m, n with
-  | 0, 0 => True
-  | m'.+1, n'.+1 => code_nat m' n'
-  | _, _ => False
-  end.
-
-Infix "=n" := code_nat : nat_scope.
-
-Fixpoint idcode_nat {n} : (n =n n) :=
-  match n as n return (n =n n) with
-  | 0 => tt
-  | S n' => @idcode_nat n'
-  end.
-
-Fixpoint path_nat {n m} : (n =n m) -> (n = m) :=
-  match m as m, n as n return (n =n m) -> (n = m) with
-  | 0, 0 => fun _ => idpath
-  | m'.+1, n'.+1 => fun H : (n' =n m') => ap S (path_nat H)
-  | _, _ => fun H => match H with end
-  end.
-
-Global Instance isequiv_path_nat {n m} : IsEquiv (@path_nat n m).
+(** [nat] has decidable paths *)
+Global Instance decidable_paths_nat : DecidablePaths nat.
 Proof.
-  refine (isequiv_adjointify
-            (@path_nat n m)
-            (fun H => transport (fun m' => (n =n m')) H idcode_nat)
-            _ _).
-  { intros []; simpl.
-    induction n; simpl; trivial.
-    by destruct (IHn^)%path. }
-  { intro. apply path_ishprop. }
+  intros n; induction n as [|n IHn];
+  intros m; destruct m.
+  - exact (inl idpath).
+  - exact (inr (not_eq_O_S m)).
+  - exact (inr (fun p => not_eq_O_S n p^)).
+  - destruct (IHn m) as [p|q].
+    + exact (inl (ap S p)).
+    + exact (inr (fun p => q (path_nat_S _ _ p))).
 Defined.
 
-Definition equiv_path_nat {n m} : (n =n m) <~> (n = m)
-  := Build_Equiv _ _ (@path_nat n m) _.
-
-(** Thus [nat] has decidable paths *)
-Global Instance decidable_paths_nat : DecidablePaths nat
-  := fun n m => decidable_equiv _ (@path_nat n m) _.
-
 (** And is therefore a HSet *)
 Global Instance hset_nat : IsHSet nat := _.
 
@@ -481,36 +452,6 @@ Proof.
   apply leq_S, leq_add.
 Defined.
 
-Lemma equiv_leq_add n m
-  : leq n m <~> exists k, k + n = m.
-Proof.
-  srapply equiv_iff_hprop.
-  { apply hprop_allpath.
-    intros [x p] [y q].
-    apply path_sigma_hprop.
-    simpl.
-    revert m p q.
-    induction n.
-    { intros m p q.
-      rewrite <- add_n_O in p,q.
-      exact (p @ q^). }
-    intros m p q.
-    rewrite <- add_n_Sm in p,q.
-    destruct m.
-    { inversion p. }
-    apply path_nat_S in p, q.
-    by apply (IHn m). }
-  { intros p.
-    induction p.
-    + exists 0.
-      reflexivity.
-    + exists IHp.1.+1.
-      apply ap_S, IHp.2. }
-  intros [k p].
-  destruct p.
-  apply leq_add.
-Defined.
-
 (** We define the less-than relation [lt] in terms of [leq] *)
 Definition lt n m : Type0 := leq (S n) m.
 

theories/Spaces/Nat/Paths.v

@@ -0,0 +1,49 @@
+Require Import Basics.
+Require Export Basics.Nat.
+Require Export HoTT.DProp.
+
+(** * Characterization of the path types of [nat] *)
+
+(** We characterize the path types of [nat].  We put this in its own file because it uses DProp, which has a lot of dependencies. *)
+
+Local Set Universe Minimization ToSet.
+
+Local Close Scope trunc_scope.
+Local Open Scope nat_scope.
+
+Fixpoint code_nat (m n : nat) {struct m} : DHProp@{Set} :=
+  match m, n with
+  | 0, 0 => True
+  | m'.+1, n'.+1 => code_nat m' n'
+  | _, _ => False
+  end.
+
+Infix "=n" := code_nat : nat_scope.
+
+Fixpoint idcode_nat {n} : (n =n n) :=
+  match n as n return (n =n n) with
+  | 0 => tt
+  | S n' => @idcode_nat n'
+  end.
+
+Fixpoint path_nat {n m} : (n =n m) -> (n = m) :=
+  match m as m, n as n return (n =n m) -> (n = m) with
+  | 0, 0 => fun _ => idpath
+  | m'.+1, n'.+1 => fun H : (n' =n m') => ap S (path_nat H)
+  | _, _ => fun H => match H with end
+  end.
+
+Global Instance isequiv_path_nat {n m} : IsEquiv (@path_nat n m).
+Proof.
+  refine (isequiv_adjointify
+            (@path_nat n m)
+            (fun H => transport (fun m' => (n =n m')) H idcode_nat)
+            _ _).
+  { intros []; simpl.
+    induction n; simpl; trivial.
+    by destruct (IHn^)%path. }
+  { intro. apply path_ishprop. }
+Defined.
+
+Definition equiv_path_nat {n m} : (n =n m) <~> (n = m)
+  := Build_Equiv _ _ (@path_nat n m) _.