Is there a solution for the problematic induction hypotheses generated using eqn:H?

Using Coq
1

Hello!

The following is a severely stripped down piece extracted from a larger development. The proof (at least in the real development) appears to require the use of the eqn:... construct:

Require Import Coq.Strings.String.
Require Import Coq.Strings.Ascii.
Require Import Coq.Arith.PeanoNat.
Require Import Coq.Lists.List.

Inductive identifier := {
  id_number : nat;
  id_name   : string
}.

Definition distinct_names
  (ids : list identifier)
: list string :=
  nodup string_dec (map id_name ids).

Theorem distinct_names_forall : forall xs,
  Forall (fun name => exists k, In k xs -> id_name k = name) (distinct_names xs).
Proof.
  intros xs.
  induction (distinct_names xs) as [|y ys] eqn:H. {
    constructor.
  } {
    (* Induction hypothesis is bad *)
  }
Qed.

The proof context at the comment looks like this:

1 goal
xs : list identifier
y : string
ys : list string
H : (distinct_names xs) = (y :: ys)
IHys : ((distinct_names xs) = ys) ->
       Forall (fun name : string => exists k : identifier, ((In k xs) -> (id_name k) = name)) ys
______________________________________(1/1)
Forall (fun name : string => exists k : identifier, ((In k xs) -> (id_name k) = name)) (y :: ys)

Note that there’s a ((distinct_names xs) = ys) parameter to the induction hypothesis that effectively prevents being able to apply the hypothesis.

Removing the eqn:... also makes the proof grind to a halt, because several properties about the original list are effectively thrown away.

There’s a comment about this here from three years ago:

It essentially ended with the comment:

I believe the answer to question in the comment is yes, because the elim tactic from the ssreflectpackage does it better. But the extra equality that added in the process is more artificial than for the eqn:Evariant of destruct. I believe an wish for improvement should be posted to the Coq developers.

I believe in my case (at least in the real development), I do need to use eqn:. Is this still considered a bug? Is it fixed? Is there some other way instead?

2

You never “need” to use some specific tactic. Either there exists a proof term and you can provide it directly, or there is not and the theorem is not provable anyway. Tactics are just some way to generate a proof term for you, and if they fail to do so, just do not use them. In your case, you can start your proof as follows:

  intros xs.
  remember (distinct_names xs) as ys.
  revert xs Heqys.
  induction ys as [|y ys].
3

You never “need” to use some specific tactic. Either there exists a proof term and you can provide it directly, or there is not and the theorem is not provable anyway.

Well, yes, “need” is a relative term. I decided the least painful way to prove this theorem was through the induction tactic, so I thought I “needed” the eqn: feature in to avoid getting stuck. I’ll try out your suggestion. :+1:

4

Those tactics seem to have the same problem.

Require Import Coq.Strings.String.
Require Import Coq.Strings.Ascii.
Require Import Coq.Arith.PeanoNat.
Require Import Coq.Lists.List.

Inductive identifier := {
  id_number : nat;
  id_name   : string
}.

Definition distinct_names
  (ids : list identifier)
: list string :=
  nodup string_dec (map id_name ids).

Theorem distinct_names_forall : forall xs,
  Forall (fun name => exists k, In k xs -> id_name k = name) (distinct_names xs).
Proof.
  intros xs.
  remember (distinct_names xs) as ys.
  revert xs Heqys.
  induction ys as [|y ys]. {
    intros. constructor.
  } {
    (* Induction hypothesis is bad *)
    intros xs Heq.
  }
Qed.

Yields this proof context:

1 goal
y : string
ys : list string
IHys : forall xs : list identifier,
       (ys = (distinct_names xs)) ->
       Forall (fun name : string => exists k : identifier, ((In k xs) -> (id_name k) = name)) ys
xs : list identifier
Heq : (y :: ys) = (distinct_names xs)
______________________________________(1/1)
Forall (fun name : string => exists k : identifier, ((In k xs) -> (id_name k) = name)) (y :: ys)
5

I’m not sure what you expect from using eqn with induction. With destruct the resulting goals are still about the destructed value, but with induction they are about any subterm of it so how can the equation make sense? (except when the inductive has no recursion such that induction and destruct are basically the same)

6

No, it does not. Notice how the induction hypothesis IHys is now universally quantified over xs. So, it is now possible to instantiate it, while it was impossible before.

I guess the question is: Why does Coq provide a tactic that always makes the goal unprovable (unless it was provable without an induction anyway).

(SSReflect’s own implementation of induction eqn does not suffer from this issue.)

1 Like
7

No, it does not. Notice how the induction hypothesis IHys is now universally quantified over xs. So, it is now possible to instantiate it, while it was impossible before.

:man_facepalming:

Sorry, bit of tunnel vision there. I’ve been staring at this development for quite a while.

Thanks! I’ll give it another go…

8

As is probably no surprise to anyone, it was provable without induction (at least with the introduction of an intermediary lemma):

Require Import Coq.Strings.String.
Require Import Coq.Strings.Ascii.
Require Import Coq.Arith.PeanoNat.
Require Import Coq.Lists.List.
Require Import Coq.Logic.FinFun.

Inductive identifier := {
  id_number : nat;
  id_name   : string
}.

Definition names
  (ids : list identifier)
: list string :=
  map id_name ids.

Theorem names_forall : forall (xs : list identifier),
  Forall (fun name => exists i, id_name i = name /\ In i xs) (names xs).
Proof.
  intros xs.
  unfold names.
  rewrite Forall_map.
  induction xs as [|y ys]. {
    constructor.
  } {
    constructor. {
      exists y.
      apply conj. reflexivity. left; reflexivity.
    }
    rewrite Forall_forall in *.
    intros x Hxin.
    pose proof (IHys _ Hxin) as [k [Hk0 Hk1]].
    exists k.
    apply conj.
    exact Hk0.
    apply in_cons.
    exact Hk1.
  }
Qed.

Definition distinct_names
  (ids : list identifier)
: list string :=
  nodup string_dec (names ids).

Theorem distinct_names_forall : forall xs,
  Forall (fun name => exists i, id_name i = name /\ In i xs) (distinct_names xs).
Proof.
  unfold distinct_names.
  intros xs.
  pose proof (names_forall xs) as H_nfa.
  rewrite Forall_forall in *.
  intros x H_in_nodup.
  rewrite nodup_In in H_in_nodup.
  apply (H_nfa x H_in_nodup).
Qed.
9

alternatively


Lemma Forall_nodup A dec P (l:list A) :
  Forall P (nodup dec l) <-> Forall P l.
Proof.
  rewrite 2!Forall_forall.
  setoid_rewrite nodup_In. (* we need to say setoid explicitly to rewrite under binders *)
  reflexivity.
Qed.

Theorem distinct_names_forall : forall xs,
  Forall (fun name => exists i, id_name i = name /\ In i xs) (distinct_names xs).
Proof.
  unfold distinct_names.
  intros xs.
  apply Forall_nodup, Forall_map.
  apply Forall_forall.
  eauto.
Qed.
1 Like
10

I have run into this in another form, but can’t really show it without dragging in huge parts of a development. It looks like there’s a ticket filed:

11

Yours is much nicer, but here’s my attempt on the original using just induction (excuse the lack of proper name introduction):

Definition distinct_names
  (ids : list identifier)
: list string :=
  nodup string_dec (map id_name ids).

Theorem distinct_names_forall : forall xs,
  Forall (fun name => exists i, id_name i = name /\ In i xs) (distinct_names xs).
Proof.
  unfold distinct_names.
  induction xs; [ constructor | ].
  simpl.
  rewrite Forall_forall in *.
  destruct (in_dec string_dec (id_name a) (map id_name xs)); intros.
  - specialize (IHxs x H) as (k & Hkn & Hki); eauto.
  - destruct H.
    * eauto. (* by H *)
    * specialize (IHxs x H) as (k & Hkn & Hki); eauto.
Qed.

With the setoid_rewrite trick:

Definition distinct_names
  (ids : list identifier)
: list string :=
  nodup string_dec (map id_name ids).

Theorem distinct_names_forall : forall xs,
  Forall (fun name => exists i, id_name i = name /\ In i xs) (distinct_names xs).
Proof.
  unfold distinct_names.
  induction xs; [ constructor | ].
  rewrite Forall_forall in *.
  setoid_rewrite nodup_In.
  setoid_rewrite nodup_In in IHxs.
  simpl.
  intros x []; eauto.
  specialize (IHxs x H) as (k & Hkn & Hki); eauto.
Qed.
1 Like