From 2af716f4bbaaef7ac73d688aeb0d671f512c6c06 Mon Sep 17 00:00:00 2001 From: Pierre Rousselin Date: Thu, 15 Feb 2024 21:17:52 +0100 Subject: [PATCH] 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 #18628) is provided. --- .../success/strong_and_binary_induction.v | 55 +++++++++++++++++++ theories/Arith/PeanoNat.v | 9 +++ theories/NArith/BinNat.v | 3 + theories/Numbers/Natural/Abstract/NBits.v | 13 +++-- theories/Numbers/Natural/Abstract/NOrder.v | 6 +- 5 files changed, 80 insertions(+), 6 deletions(-) create mode 100644 test-suite/success/strong_and_binary_induction.v diff --git a/test-suite/success/strong_and_binary_induction.v b/test-suite/success/strong_and_binary_induction.v new file mode 100644 index 0000000000000..eda2b78d8ab56 --- /dev/null +++ b/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. diff --git a/theories/Arith/PeanoNat.v b/theories/Arith/PeanoNat.v index 64664916fb2b8..11317e6b2118e 100644 --- a/theories/Arith/PeanoNat.v +++ b/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. diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v index 8229255f1461f..b7db6753aad15 100644 --- a/theories/NArith/BinNat.v +++ b/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] *) diff --git a/theories/Numbers/Natural/Abstract/NBits.v b/theories/Numbers/Natural/Abstract/NBits.v index df2a9371d6bb1..c225435ef7dac 100644 --- a/theories/Numbers/Natural/Abstract/NBits.v +++ b/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 _). diff --git a/theories/Numbers/Natural/Abstract/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v index ce294d4c48caa..7df03bca502ec 100644 --- a/theories/Numbers/Natural/Abstract/NOrder.v +++ b/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.