Merge pull request #1772 from jdchristensen/nat_iter

Use nat_iter for iteration

theories/Algebra/Groups/Group.v

@@ -4,6 +4,7 @@ Require Export Classes.interfaces.abstract_algebra.
 Require Export Classes.theory.groups.
 Require Import Pointed.Core.
 Require Import WildCat.
+Require Import Spaces.Nat.Core.
 
 Local Set Polymorphic Inductive Cumulativity.
 
@@ -463,11 +464,7 @@ End GroupMovement.
 
 (** Power operation *)
 
-Fixpoint grp_pow {G : Group} (g : G) (n : nat) : G :=
-  match n with
-  | 0%nat => mon_unit
-  | m.+1%nat => g * grp_pow g m
-  end.
+Definition grp_pow {G : Group} (g : G) (n : nat) : G := nat_iter n (g *.) mon_unit.
 
 (** Any homomorphism respects [grp_pow]. *)
 Lemma grp_pow_homo {G H : Group} (f : GroupHomomorphism G H)

theories/Algebra/Rings/CRing.v

@@ -1,5 +1,5 @@
 Require Import WildCat.
-Require Import Spaces.Nat.
+Require Import Spaces.Nat.Core.
 Require Export Classes.interfaces.abstract_algebra.
 Require Import Algebra.AbGroups.
 Require Export Classes.theory.rings.
@@ -405,23 +405,16 @@ Defined.
 (** *** More Ring laws *)
 
 (** Powers of ring elements *)
-Fixpoint rng_power {R : CRing} (x : R) (n : nat) : R :=
-  match n with
-  | 0%nat => cring_one
-  | n.+1%nat => x * rng_power x n
-  end.
+Definition rng_power {R : CRing} (x : R) (n : nat) : R := nat_iter n (x *.) cring_one.
 
 (** Power laws *)
 Lemma rng_power_mult_law {R : CRing} (x : R) (n m : nat)
   : (rng_power x n) * (rng_power x m) = rng_power x (n + m).
 Proof.
-  revert m.
-  induction n.
-  { intros m.
-    apply rng_mult_one_l. }
-  intros m; cbn.
+  induction n as [|n IHn].
+  1: apply rng_mult_one_l.
   refine ((rng_mult_assoc _ _ _)^ @ _).
-  f_ap.
+  exact (ap (x *.) IHn).
 Defined.
 
 (** Powers commute with multiplication *)
@@ -430,7 +423,7 @@ Lemma rng_power_mult {R : CRing} (x y : R) (n : nat)
 Proof.
   induction n.
   1: symmetry; apply rng_mult_one_l.
-  cbn.
+  simpl.
   rewrite rng_mult_assoc.
   rewrite <- (rng_mult_assoc x _ y).
   rewrite (rng_mult_comm (rng_power x n) y).

theories/Homotopy/Join/Core.v

@@ -5,6 +5,7 @@ Require Import Colimits.Pushout.
 Require Import Truncations.Core Truncations.Connectedness.
 Require Import Pointed.Core.
 Require Import WildCat.
+Require Import Spaces.Nat.Core.
 
 Local Open Scope pointed_scope.
 Local Open Scope path_scope.
@@ -799,24 +800,18 @@ End JoinEmpty.
 (** Iterated Join powers of a type. *)
 Section JoinPower.
 
-  (** The join of [n.+1] copies of a type. This is convenient because it produces [A] definitionally when [n] is [0]. *)
-  Fixpoint Join_power (A : Type) (n : nat) : Type :=
-    match n with
-    | 0%nat => A
-    | m.+1%nat => Join A (Join_power A m)
-    end.
+  (** The join of [n.+1] copies of a type. This is convenient because it produces [A] definitionally when [n] is [0]. We annotate the universes to reduce universe variables. *)
+  Definition iterated_join (A : Type@{u}) (n : nat) : Type@{u}
+    := nat_iter n (Join A) A.
 
   (** The join of [n] copies of a type. This is sometimes convenient for proofs by induction as it gives a trivial base case. *)
-  Fixpoint Join_power' (A : Type) (n : nat) : Type :=
-    match n with
-    | 0%nat => Empty
-    | m.+1%nat => Join A (Join_power' A m)
-    end.
+  Definition join_power (A : Type@{u}) (n : nat) : Type@{u}
+    := nat_iter n (Join A) (Empty : Type@{u}).
 
-  Definition equiv_join_powers (A : Type) (n : nat) : Join_power A n <~> Join_power' A n.+1.
+  Definition equiv_join_powers (A : Type) (n : nat) : join_power A n.+1 <~> iterated_join A n.
   Proof.
-    induction n as [|n IHn].
-    - symmetry; apply equiv_join_empty.
+    induction n as [|n IHn]; simpl.
+    - exact (equiv_join_empty A).
     - exact (equiv_functor_join equiv_idmap IHn).
   Defined.
 

theories/Homotopy/Join/JoinAssoc.v

@@ -150,7 +150,7 @@ Defined.
 
 (** As a consequence, we get associativity of powers. *)
 Corollary join_join_power A n m
-  : Join (Join_power' A n) (Join_power' A m) <~> Join_power' A (n + m)%nat.
+  : Join (join_power A n) (join_power A m) <~> join_power A (n + m)%nat.
 Proof.
   induction n as [|n IHn].
   1: exact (equiv_join_empty' _).

theories/Homotopy/Join/JoinSusp.v

@@ -53,7 +53,7 @@ Definition equiv_join_susp (A : Type) : Join Bool A <~> Susp A
   := Build_Equiv _ _ (join_to_susp A) _.
 
 (** It follows that the iterated join of [Bool] gives a sphere. *)
-Definition equiv_join_power_bool_sphere (n : nat): Join_power' Bool n <~> Sphere (n.-1).
+Definition equiv_join_power_bool_sphere (n : nat): join_power Bool n <~> Sphere (n.-1).
 Proof.
   induction n as [|n IHn].
   - reflexivity.

theories/Metatheory/PropTrunc.v

@@ -13,7 +13,7 @@ Local Open Scope nat_scope.
 Definition Join_seq (A : Type) : Sequence.
 Proof.
   srapply Build_Sequence.
-  1: exact (Join_power A).
+  1: exact (iterated_join A).
   intros n.
   exact joinr.
 Defined.

theories/Pointed/Loops.v

@@ -2,6 +2,7 @@ Require Import HoTT.Basics HoTT.Types.
 Require Import HFiber Factorization Truncations.Core Truncations.Connectedness HProp.
 Require Import Pointed.Core Pointed.pEquiv.
 Require Import WildCat.
+Require Import Spaces.Nat.Core.
 
 Local Open Scope pointed_scope.
 Local Open Scope path_scope.
@@ -14,22 +15,13 @@ Global Instance ispointed_loops A (a : A) : IsPointed (a = a) := 1.
 Definition loops (A : pType) : pType
   := [point A = point A, 1].
 
-Fixpoint iterated_loops (n : nat) (A : pType) : pType
-  := match n with
-       | O => A
-       | S p => loops (iterated_loops p A)
-     end.
+Definition iterated_loops (n : nat) (A : pType) : pType
+  := nat_iter n loops A.
 
 (* Inner unfolding for iterated loops *)
-Lemma unfold_iterated_loops (n : nat) (X : pType)
-  : iterated_loops n.+1 X = iterated_loops n (loops X).
-Proof.
-  induction n.
-  1: reflexivity.
-  change (iterated_loops n.+2 X)
-    with (loops (iterated_loops n.+1 X)).
-  by refine (ap loops IHn @ _).
-Defined.
+Definition unfold_iterated_loops (n : nat) (X : pType)
+  : iterated_loops n.+1 X = iterated_loops n (loops X)
+  := nat_iter_succ_r _ _ _.
 
 (** The loop space decreases the truncation level by one.  We don't bother making this an instance because it is automatically found by typeclass search, but we record it here in case anyone is looking for it. *)
 Definition istrunc_loops {n} (A : pType) `{IsTrunc n.+1 A}

theories/Sets/Powers.v

@@ -1,21 +1,18 @@
-From HoTT Require Import TruncType abstract_algebra.
+From HoTT Require Import Basics Types TruncType.
 From HoTT Require Import PropResizing.PropResizing.
-From HoTT Require Import Spaces.Card.
-
+From HoTT Require Import Spaces.Card Spaces.Nat.Core.
 
 (** * Definition of Power types *)
 
-(* The definition is only used in Hartogs.v to allow defining a coercion,
-   everywhere else we prefer to write out the definition for clarity. *)
-
-Definition power_type (A : Type) : Type :=
-  A -> HProp.
+(* The definition is only used in Hartogs.v to allow defining a coercion, and one place below.  Everywhere else we prefer to write out the definition for clarity. *)
 
+Definition power_type (A : Type) : Type
+  := A -> HProp.
 
 (** * Iterated powers *)
 
-Lemma Injection_power {PR : PropResizing} X :
-  IsHSet X -> Injection X (X -> HProp).
+Lemma Injection_power {PR : PropResizing} X
+  : IsHSet X -> Injection X (X -> HProp).
 Proof.
   intros HX.
   set (f (x : X) := fun y => Build_HProp (resize_hprop (x = y))).
@@ -24,55 +21,42 @@ Proof.
   rewrite H. cbn. apply equiv_resize_hprop. reflexivity.
 Qed.
 
-Fixpoint power_iterated X n :=
-  match n with
-  | O => X 
-  | S n => power_iterated X n -> HProp
-  end.
+Definition power_iterated X n := nat_iter n power_type X.
 
-Lemma power_iterated_shift X n :
-  power_iterated (X -> HProp) n = (power_iterated X n -> HProp).
-Proof.
-  induction n in X |- *; cbn.
-  - reflexivity.
-  - rewrite IHn. reflexivity.
-Qed.
+Definition power_iterated_shift X n
+  : power_iterated (X -> HProp) n = (power_iterated X n -> HProp)
+  := (nat_iter_succ_r _ _ _)^.
 
-Global Instance hset_power {UA : Univalence} (X : HSet) :
-  IsHSet (X -> HProp).
+Global Instance hset_power {UA : Univalence} (X : HSet)
+  : IsHSet (X -> HProp).
 Proof.
   intros p q. apply hprop_allpath. intros H H'.
   destruct (equiv_path_arrow p q) as [f [g Hfg Hgf _]].
   rewrite <- (Hfg H), <- (Hfg H'). apply ap. apply path_forall.
   intros x. apply isset_HProp.
 Qed.
 
-Global Instance hset_power_iterated {UA : Univalence} (X : HSet) n :
-  IsHSet (power_iterated X n).
-Proof.
-  induction n; cbn.
-  - apply X.
-  - apply (@hset_power UA (Build_HSet (power_iterated X n))).
-Qed.
+Global Instance hset_power_iterated {UA : Univalence} (X : HSet) n
+  : IsHSet (power_iterated X n)
+  := nat_iter_invariant _ _ _ _ _ _.
 
-Lemma Injection_power_iterated {UA : Univalence} {PR : PropResizing} (X : HSet) n :
-  Injection X (power_iterated X n).
+Lemma Injection_power_iterated {UA : Univalence} {PR : PropResizing} (X : HSet) n
+  : Injection X (power_iterated X n).
 Proof.
-  induction n.
+  induction n as [|n IHn].
   - reflexivity.
   - eapply Injection_trans; try apply IHn.
     apply Injection_power. exact _.
 Qed.
 
-Lemma infinite_inject X Y :
-  infinite X -> Injection X Y -> infinite Y.
+Lemma infinite_inject X Y
+  : infinite X -> Injection X Y -> infinite Y.
 Proof.
   apply Injection_trans.
 Qed.
 
-Lemma infinite_power_iterated {UA : Univalence} {PR : PropResizing} (X : HSet) n :
-  infinite X -> infinite (power_iterated X n).
+Lemma infinite_power_iterated {UA : Univalence} {PR : PropResizing} (X : HSet) n
+  : infinite X -> infinite (power_iterated X n).
 Proof.
   intros H. eapply infinite_inject; try apply H. apply Injection_power_iterated.
 Qed.
-

theories/Spaces/Nat/Core.v

@@ -198,11 +198,6 @@ Fixpoint log2_iter k p q r : nat :=
 
 Definition log2 n : nat := log2_iter (pred n) 0 1 0.
 
-(** ** Iterator on natural numbers *)
-
-Definition iter (n : nat) {A} (f : A -> A) (x : A) : A :=
-  nat_rec A x (fun _ => f) n.
-
 Local Definition ap_S := @ap _ _ S.
 Local Definition ap_nat := @ap nat.
 #[export] Hint Resolve ap_S : core.
@@ -632,53 +627,52 @@ Proof.
   intros; rewrite min_comm; by apply min_l.
 Defined.
 
-(** [n]th iteration of the function [f] *)
-
-Fixpoint nat_iter (n:nat) {A} (f:A->A) (x:A) : A :=
-  match n with
-    | O => x
-    | S n' => f (nat_iter n' f x)
-  end.
+(** [n]th iteration of the function [f : A -> A].  We have definitional equalities [nat_iter 0 f x = x] and [nat_iter n.+1 f x = f (nat_iter n f x).  We make this a notation, so it doesn't add a universe variable for the universe containing [A]. *)
+Notation nat_iter n f x
+  := ((fix F (m : nat)
+      := match m with
+        | 0 => x
+        | m'.+1 => f (F m')
+        end) n).
 
-Lemma nat_iter_succ_r n {A} (f:A->A) (x:A) :
-  nat_iter (S n) f x = nat_iter n f (f x).
+Lemma nat_iter_succ_r n {A} (f : A -> A) (x : A)
+  : nat_iter (S n) f x = nat_iter n f (f x).
 Proof.
-  induction n; intros; simpl; rewrite <- ?IHn; trivial.
+  induction n as [|n IHn]; simpl; trivial.
+  exact (ap f IHn).
 Defined.
 
-Theorem nat_iter_add :
-  forall (n m:nat) {A} (f:A -> A) (x:A),
-    nat_iter (n + m) f x = nat_iter n f (nat_iter m f x).
+Theorem nat_iter_add (n m : nat) {A} (f : A -> A) (x : A)
+  : nat_iter (n + m) f x = nat_iter n f (nat_iter m f x).
 Proof.
-  induction n; intros; simpl; rewrite ?IHn; trivial.
+  induction n as [|n IHn]; simpl; trivial.
+  exact (ap f IHn).
 Defined.
 
-(** Preservation of invariants : if [f : A -> A] preserves the invariant [Inv], then the iterates of [f] also preserve it. *)
-
+(** Preservation of invariants : if [f : A -> A] preserves the invariant [P], then the iterates of [f] also preserve it. *)
 Theorem nat_iter_invariant (n : nat) {A} (f : A -> A) (P : A -> Type)
   : (forall x, P x -> P (f x)) -> forall x, P x -> P (nat_iter n f x).
 Proof.
-  revert n A f P.
-  induction n; simpl; trivial.
-  intros A f P Hf x Hx.
+  induction n as [|n IHn]; simpl; trivial.
+  intros Hf x Hx.
   apply Hf, IHn; trivial.
 Defined.
 
 (** ** Arithmetic *)
 
-Lemma nat_add_n_Sm : forall n m:nat, (n + m).+1 = n + m.+1.
+Lemma nat_add_n_Sm (n m : nat) : (n + m).+1 = n + m.+1.
 Proof.
-  intros n m; induction n; simpl.
+  induction n; simpl.
   - reflexivity.
   - apply ap; assumption.
 Defined.
 
 Definition nat_add_comm (n m : nat) : n + m = m + n.
 Proof.
-  revert m; induction n as [|n IH]; intros m; simpl.
-  - refine (add_n_O m).
+  induction n as [|n IHn]; simpl.
+  - exact (add_n_O m).
   - transitivity (m + n).+1.
-    + apply ap, IH.
+    + apply ap, IHn.
     + apply nat_add_n_Sm.
 Defined.