Merge pull request #11880 from Lysxia/iter

NArith, PArith: Add facts about iter

3 files changed, 84 insertions, 3 deletions

diff --git a/doc/changelog/10-standard-library/11880-iter.rst b/doc/changelog/10-standard-library/11880-iter.rst
new file mode 100644
index 0000000000..be4e44ce4c
--- /dev/null
+++ b/doc/changelog/10-standard-library/11880-iter.rst
@@ -0,0 +1,8 @@
+- **Added:**
+  Facts about ``N.iter`` and ``Pos.iter``:
+
+    - ``N.iter_swap_gen``, ``N.iter_swap``, ``N.iter_succ``, ``N.iter_succ_r``, ``N.iter_add``, ``N.iter_ind``, ``N.iter_invariant``;
+    - ``Pos.iter_succ_r``, ``Pos.iter_ind``.
+
+  (`#11880 <https://github.com/coq/coq/pull/11880>`_,
+  by Lysxia).
diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v
index f0011fe147..d68c32b371 100644
--- a/theories/NArith/BinNat.v
+++ b/theories/NArith/BinNat.v
@@ -943,6 +943,64 @@ Proof.
  destruct p; simpl; trivial.
 Qed.
 
+(** ** Properties of [iter] *)
+
+Lemma iter_swap_gen : forall A B (f:A -> B) (g:A -> A) (h:B -> B),
+ (forall a, f (g a) = h (f a)) -> forall n a,
+ f (iter n g a) = iter n h (f a).
+Proof.
+ destruct n; simpl; intros; rewrite ?H; trivial.
+ now apply Pos.iter_swap_gen.
+Qed.
+
+Theorem iter_swap :
+  forall n (A:Type) (f:A -> A) (x:A),
+    iter n f (f x) = f (iter n f x).
+Proof.
+ intros. symmetry. now apply iter_swap_gen.
+Qed.
+
+Theorem iter_succ :
+  forall n (A:Type) (f:A -> A) (x:A),
+    iter (succ n) f x = f (iter n f x).
+Proof.
+ destruct n; intros; simpl; trivial.
+ now apply Pos.iter_succ.
+Qed.
+
+Theorem iter_succ_r :
+  forall n (A:Type) (f:A -> A) (x:A),
+    iter (succ n) f x = iter n f (f x).
+Proof.
+ intros; now rewrite iter_succ, iter_swap.
+Qed.
+
+Theorem iter_add :
+  forall p q (A:Type) (f:A -> A) (x:A),
+    iter (p+q) f x = iter p f (iter q f x).
+Proof.
+ induction p using peano_ind; intros; trivial.
+ now rewrite add_succ_l, !iter_succ, IHp.
+Qed.
+
+Theorem iter_ind :
+  forall (A:Type) (f:A -> A) (a:A) (P:N -> A -> Prop),
+    P 0 a ->
+    (forall n a', P n a' -> P (succ n) (f a')) ->
+    forall n, P n (iter n f a).
+Proof.
+ induction n using peano_ind; trivial.
+ rewrite iter_succ; auto.
+Qed.
+
+Theorem iter_invariant :
+  forall (n:N) (A:Type) (f:A -> A) (Inv:A -> Prop),
+    (forall x:A, Inv x -> Inv (f x)) ->
+    forall x:A, Inv x -> Inv (iter n f x).
+Proof.
+ intros; apply iter_ind with (P := fun _ => Inv); trivial.
+Qed.
+
 End N.
 
 Bind Scope N_scope with N.t N.
diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v
index 99e77fd596..387ab75362 100644
--- a/theories/PArith/BinPos.v
+++ b/theories/PArith/BinPos.v
@@ -597,6 +597,13 @@ Proof.
  now rewrite !IHp, iter_swap.
 Qed.
 
+Theorem iter_succ_r :
+  forall p (A:Type) (f:A -> A) (x:A),
+    iter f x (succ p) = iter f (f x) p.
+Proof.
+ intros; now rewrite iter_succ, iter_swap.
+Qed.
+
 Theorem iter_add :
   forall p q (A:Type) (f:A -> A) (x:A),
     iter f x (p+q) = iter f (iter f x q) p.
@@ -606,14 +613,22 @@ Proof.
  now rewrite add_succ_l, !iter_succ, IHp.
 Qed.
 
+Theorem iter_ind :
+  forall (A:Type) (f:A -> A) (a:A) (P:positive -> A -> Prop),
+    P 1 (f a) ->
+    (forall p a', P p a' -> P (succ p) (f a')) ->
+    forall p, P p (iter f a p).
+Proof.
+ induction p using peano_ind; trivial.
+ rewrite iter_succ; auto.
+Qed.
+
 Theorem iter_invariant :
   forall (p:positive) (A:Type) (f:A -> A) (Inv:A -> Prop),
     (forall x:A, Inv x -> Inv (f x)) ->
     forall x:A, Inv x -> Inv (iter f x p).
 Proof.
- induction p as [p IHp|p IHp|]; simpl; trivial.
- intros A f Inv H x H0. apply H, IHp, IHp; trivial.
- intros A f Inv H x H0. apply IHp, IHp; trivial.
+ intros; apply iter_ind with (P := fun _ => Inv); auto.
 Qed.
 
 (** ** Properties of power *)