Stream: Coq users

Topic: binary induction


view this post on Zulip Pierre Rousselin (Feb 07 2024 at 09:56):

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:

Forgot to say, this is on master (8.20alpha) and 8.17 (so I guess in the other versions in between).

view this post on Zulip Kenji Maillard (Feb 07 2024 at 10:25):

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.

view this post on Zulip Pierre Rousselin (Feb 07 2024 at 10:31):

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

view this post on Zulip Pierre Rousselin (Feb 07 2024 at 10:32):

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

view this post on Zulip Kenji Maillard (Feb 07 2024 at 10:50):

The documentation ofinduction 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.

view this post on Zulip Pierre Courtieu (Feb 07 2024 at 17:52):

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.

view this post on Zulip Pierre Rousselin (Feb 07 2024 at 18:02):

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