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?
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].
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.
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)
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.)
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.
Sorry, bit of tunnel vision there. I’ve been staring at this development for quite a while.
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.
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:
