Sorry, if it's probably been asked many times.

I'm trying to use conveniently a new induction principle on, say, `nat`

.

```
From Coq Require Import Arith.PeanoNat.
Lemma binary_induction (A : nat -> Prop) : A 0 ->
(forall n : nat, A n -> A (2 * n) /\ A (2 * n + 1)) -> forall n : nat, A n.
Proof. Admitted.
Lemma land_even_even :
forall a b : nat, Nat.land (2 * a) (2 * b) = 2 * Nat.land a b.
Proof.
Fail induction a using binary_induction.
(* Cannot recognize the branches of an induction scheme. *)
Admitted.
Lemma land_even_even' :
forall a b : nat, Nat.land (2 * a) (2 * b) = 2 * Nat.land a b.
Proof.
intros a; apply binary_induction.
- admit.
- intros n H.
(* fail : H is not universally quantified. *)
Admitted.
Lemma land_even_even'_2 :
forall a b : nat, Nat.land (2 * a) (2 * b) = 2 * Nat.land a b.
Proof.
apply binary_induction.
- (* no progress at all, this is the statement of the lemma *)
admit.
- (* silly goal with [nat ->] in front *) intros n H; split; exact H.
- (* silly goal [nat] *) exact 0.
Admitted.
Lemma land_even_even'' :
forall a b : nat, Nat.land (2 * a) (2 * b) = 2 * Nat.land a b.
Proof.
apply (binary_induction
(fun a => forall b, Nat.land (2 * a) (2 * b) = 2 * Nat.land a b)).
- admit.
- intros a IH; split; intros b.
(* good! but writing the predicate by hand is unpleasant *)
Admitted.
Require Import ssreflect.
Lemma land_even_even''' :
forall a b : nat, Nat.land (2 * a) (2 * b) = 2 * Nat.land a b.
Proof.
elim/binary_induction.
- admit.
- intros a IH; split; intros b. (* great *)
Admitted.
```

to sum up, I don't know how to make vanilla Coq:

- accept
`binary_induction`

in`induction ... using ...`

- infer a nice predicate with
`apply`

Forgot to say, this is on `master (8.20alpha)`

and `8.17`

(so I guess in the other versions in between).

It looks like induction expect at most one conclusion per branch (induction has no understanding of `/\`

), e.g.:

```
From Coq Require Import Arith.PeanoNat.
Lemma binary_induction (A : nat -> Prop) : A 0 ->
(forall n : nat, A n -> A (2 * n)) -> (forall n : nat, A n -> A (2 * n + 1)) -> forall n : nat, A n.
Proof. Admitted.
Lemma land_even_even :
forall a b : nat, Nat.land (2 * a) (2 * b) = 2 * Nat.land a b.
Proof.
induction a using binary_induction.
- admit.
- intros b. admit.
- intros b. admit.
Admitted.
```

Thanks! This is even better to use with your modification.

(I'm still curious about why there is a problem with `/\`

though)

The documentation of`induction`

is not really specific about what it accept as an induction principle and I would guess that it has a rather rigid view of induction principles akind of

`forall Parameters Predicates/Motives, Methods -> forall object, Predicate evaluated on object`

where each `Method`

is itself of shape `forall Parameters Arguments, InductiveHypotheses -> Predicate evaluated on an element`

.

Pierre Rousselin said:

`Lemma land_even_even' : forall a b : nat, Nat.land (2 * a) (2 * b) = 2 * Nat.land a b. Proof. intros a; apply binary_induction.`

This is due to `apply`

mechanics: it cannot guess `A`

correctly. Here doing `intros a; apply binary_induction with (n:=a)`

is enough to hint it correctly. In general you should specify `A`

itself or make it appear explicitly in the goal.

This is a usual way of doing it:

```
Lemma land_even_even' :
forall a b : nat, Nat.land (2 * a) (2 * b) = 2 * Nat.land a b.
Proof.
intro a.
pattern a.
apply binary_induction.
```

This is what `induction`

does at its core, but it does other things (goodies like reverting things before applying the induction scheme, renaming hypothesis afterward, etc) .

The documentation of induction is not really specific about what it accept as an induction principle and I would guess that it has a rather rigid view of induction principles akind of

forall Parameters Predicates/Motives, Methods -> forall object, Predicate evaluated on object

That is pretty accurate.

```
where each Method is itself of shape forall Parameters Arguments, InductiveHypotheses -> Predicate evaluated on an element.
```

I think it can be any product finishing with an application of the predicate under consideration (or one of the same inductive family).

This constraints are not strictly necessary from the logical point of view (pattern + apply don't need this for instance) but I think it makes possible some of the goodies of `induction`

possible. The `elim`

tactic from ssreflect is much more permissive in this regard AFAIK.

Thank you for the detailed answer. I will work on it. For the moment, changing `binary_induction`

as suggested by @Kenji Maillard should be enough. This is for Coq/Coq#18628.

Last updated: Jun 23 2024 at 04:03 UTC