Specialize new induction lemmas in implementations

The lemmas `strong_induction_le` and `binary_induction` in
`Numbers.Natural` are now marked as `Private_` and hidden from the
documentation.

Specialized versions (not hidden) are provided for `PeanoNat` and (only
`strong_induction`) for `BinNat`.

A new test file for these induction lemmas (and other additions in coq#18628)
is provided.

test-suite/success/strong_and_binary_induction.v

@@ -0,0 +1,55 @@
+(** This file is meant to test that the induction lemmas introduced in
+    #18628:
+    - [binary_induction] and [strong_induction_le] in PeanoNat
+    - [strong_induction_le] in BinNat
+    work with the [induction] tactic. *)
+
+From Coq.Arith Require Import PeanoNat.
+From Coq.NArith Require Import BinNat.
+
+Open Scope nat_scope.
+
+Lemma land_diag_binary_induction_test n : Nat.land n n = n.
+Proof.
+  induction n as [| n IH | n IH] using Nat.binary_induction.
+  - rewrite Nat.land_0_l; reflexivity.
+  - rewrite Nat.land_even_l, Nat.div2_even, IH; reflexivity.
+  - rewrite Nat.land_odd_l, Nat.odd_odd, Nat.div2_odd', IH; reflexivity.
+Qed.
+
+Lemma land_diag_strong_induction_test n : Nat.land n n = n.
+Proof.
+  induction n as [| n IH] using Nat.strong_induction_le.
+  - rewrite Nat.land_0_l; reflexivity.
+  - destruct (Nat.Even_or_Odd n) as [[k ->] | [k ->]].
+    + rewrite <-Nat.add_1_r, Nat.land_odd_l, Nat.div2_odd', IH, Nat.odd_odd;
+        [reflexivity |].
+      apply Nat.le_mul_l; discriminate.
+    + replace (S (2 * k + 1)) with (2 * (k + 1)); cycle 1. {
+        rewrite Nat.mul_add_distr_l, <-Nat.add_succ_r, Nat.mul_1_r; reflexivity.
+      }
+      rewrite Nat.land_even_l, Nat.div2_even, IH; [reflexivity |].
+      apply Nat.add_le_mono; [| exact (Nat.le_refl _)].
+      apply Nat.le_mul_l; discriminate.
+Qed.
+
+Close Scope nat_scope.
+Open Scope N_scope.
+
+(* Of course, this example is articifial in N. However, this shows that the
+   previous proof with almost no modifications. *)
+Lemma land_diag_strong_induction_test_N n : N.land n n = n.
+Proof.
+  induction n as [| n IH] using N.strong_induction_le.
+  - rewrite N.land_0_l; reflexivity.
+  - destruct (N.Even_or_Odd n) as [[k ->] | [k ->]].
+    + rewrite <-N.add_1_r, N.land_odd_l, N.div2_odd', IH, N.odd_odd;
+        [reflexivity |].
+      apply N.le_mul_l; discriminate.
+    + replace (N.succ (2 * k + 1)) with (2 * (k + 1)); cycle 1. {
+        rewrite N.mul_add_distr_l, <-N.add_succ_r, N.mul_1_r; reflexivity.
+      }
+      rewrite N.land_even_l, N.div2_even, IH; [reflexivity |].
+      apply N.add_le_mono; [| exact (N.le_refl _)].
+      apply N.le_mul_l; discriminate.
+Qed.

theories/Arith/PeanoNat.v

@@ -257,6 +257,10 @@ Include BoolOrderFacts.
 
 Include NBasicProp <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.
 
+Lemma strong_induction_le (A : nat -> Prop) :
+  A 0 -> (forall n, (forall m, m <= n -> A m) -> A (S n)) -> forall n, A n.
+Proof. apply Private_strong_induction_le; intros x y ->; reflexivity. Qed.
+
 (** ** Power *)
 
 Lemma pow_neg_r a b : b<0 -> a^b = 0.
@@ -914,6 +918,11 @@ Proof. reflexivity. Qed.
 
 Include NExtraPreProp <+ NExtraProp0.
 
+Lemma binary_induction (A : nat -> Prop) :
+  A 0 -> (forall n, A n -> A (2 * n)) -> (forall n, A n -> A (2 * n + 1))
+  -> forall n, A n.
+Proof. apply Private_binary_induction; intros x y ->; reflexivity. Qed.
+
 (** Properties of tail-recursive addition and multiplication *)
 
 Lemma tail_add_spec n m : tail_add n m = n + m.

theories/NArith/BinNat.v

@@ -370,6 +370,9 @@ Qed.
 
 Include NBasicProp <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.
 
+Lemma strong_induction_le (A : N -> Prop) :
+  A 0 -> (forall n, (forall m, m <= n -> A m) -> A (succ n)) -> forall n, A n.
+Proof. apply Private_strong_induction_le; intros x y ->; reflexivity. Qed.
 
 (** Properties of [double] and [succ_double] *)
 

theories/Numbers/Natural/Abstract/NBits.v

@@ -64,13 +64,15 @@ Proof.
  - exists a'. exists true. now simpl.
 Qed.
 
-(** A useful induction lemma to reason on bits *)
-Lemma binary_induction (A : t -> Prop) :
+(* This is kept private in order to drop the `Proper` condition in
+   implementations. *)
+(* begin hide *)
+Lemma Private_binary_induction (A : t -> Prop) :
   (Proper (eq ==> iff) A) -> A 0 -> (forall n, A n -> A (2 * n)) ->
   (forall n, A n -> A (2 * n + 1)) -> (forall n, A n).
 Proof.
   intros H H0 I J.
-  apply strong_induction_le; [exact H | exact H0 |]; intros n Hm.
+  apply Private_strong_induction_le; [exact H | exact H0 |]; intros n Hm.
   pose proof (exists_div2 (S n)) as [m [[|] Hmb]]; simpl in Hmb; rewrite Hmb.
   - apply J, Hm.
     rewrite add_1_r in Hmb; apply succ_inj in Hmb; rewrite Hmb, two_succ.
@@ -80,6 +82,7 @@ Proof.
     apply add_le_mono_l, neq_0_le_1; intros C; rewrite C, mul_0_r in Hmb.
     exact (neq_succ_0 _ Hmb).
 Qed.
+(* end hide *)
 
 (** We can compact [testbit_odd_0] [testbit_even_0]
     [testbit_even_succ] [testbit_odd_succ] in only two lemmas. *)
@@ -858,7 +861,7 @@ Proof. intros a b; rewrite land_odd_l, div2_odd', odd_odd; reflexivity. Qed.
 Lemma land_le_l :
   forall a b, land a b <= a.
 Proof.
-  apply (binary_induction (fun a => forall b, _)); [| | intros a H b..].
+  apply (Private_binary_induction (fun a => forall b, _)); [| | intros a H b..].
   - intros x y eq; split; intros H b; [rewrite <-eq | rewrite eq]; now apply H.
   - intros b; rewrite land_0_l; exact (le_refl _).
   - rewrite land_even_l; apply mul_le_mono_l; exact (H _).
@@ -943,7 +946,7 @@ Proof. intros a b; rewrite ldiff_odd_r, div2_odd'; reflexivity. Qed.
 Lemma ldiff_le_l :
   forall a b, ldiff a b <= a.
 Proof.
-  apply (binary_induction (fun a => forall b, _)); [| | intros a H b..].
+  apply (Private_binary_induction (fun a => forall b, _)); [| | intros a H b..].
   - intros x y eq; split; intros H b; [rewrite <-eq | rewrite eq]; now apply H.
   - intros b; rewrite ldiff_0_l; exact (le_0_l _).
   - rewrite ldiff_even_l; apply mul_le_mono_l; exact (H _).

theories/Numbers/Natural/Abstract/NOrder.v

@@ -272,7 +272,10 @@ Proof.
   intros y _ IH'. apply IH. intros. apply IH'. now split; [apply le_0_l|].
 Defined.
 
-Theorem strong_induction_le {A : t -> Prop} :
+(* This is kept private in order to drop the [Proper] condition in
+   implementations. *)
+(* begin hide *)
+Theorem Private_strong_induction_le {A : t -> Prop} :
   Proper (eq ==> iff) A ->
   A 0 -> (forall n, ((forall m, m <= n -> A m) -> A (S n))) -> (forall n, A n).
 Proof.
@@ -286,5 +289,6 @@ Proof.
     + exact Hk.
     + apply sIH; exact I.
 Qed.
+(* end hide *)
 
 End NOrderProp.