Hello!

Revisiting Is there a solution for the problematic induction hypotheses generated using eqn:H? slightly, I’ve run into a similar problem again. To summarize the original post, the behaviour of the induction tactic has a recognized design flaw and there’s a GitHub issue filed for it ("induction ... eqn" creates unusable hypothesis without error · Issue #11784 · coq/coq · GitHub).

In the original thread, the problem I was having ended up being solvable a different way. Additionally, someone offered a workaround to a *specific* case of the induction problem that also allowed it be solved.

However, I’ve run into this same class of problem again, and the specific solution doesn’t appear to be applicable, and I’m looking for other solutions. Here’s the problem, boiled down:

```
Require Coq.Lists.List.
Parameter A : Type.
Parameter elements : list A.
Parameter elementsIn : forall (x : A), List.In x elements.
Parameter P : A -> Prop.
Parameter Q : A -> Prop.
Parameter PQ : forall (x : A), P x -> Q x.
Parameter elementsHold : forall (x : A), List.In x elements -> P x.
```

I now want to prove `forall (x : A), List.In x elements -> Q x.`

. This should be trivial; if there’s an `x`

in `elements`

, then `P x`

. Then, `P x -> Q x`

and therefore all for all `x`

in `elements`

, `Q x`

must hold. Note that the various hypotheses talk about a specific list `elements`

- not just any list of `A`

.

The obvious way to proceed is through induction on `elements`

:

```
Lemma px : forall (x : A),
List.In x elements -> Q x.
Proof.
intros x.
induction elements as [|y ys].
- intros H; inversion H.
- intros H.
(** Association between (y :: ys) is lost. *)
Abort.
```

But, oh dear, the relationship between the subterms `y`

and `ys`

and `elements`

is lost, so there’s nothing in the context that says that `y`

is in `elements`

:

```
x, y : A
ys : list A
IHys : List.In x ys -> Q x
H : List.In x (y :: ys)
______________________________________(1/1)
Q x
```

The obvious answer to this is to use `induction ... eqn:`

to remember the fact that we’re talking about the specific list `elements`

. Unfortunately, this crashes into the GitHub issue where an erroneous equality is inserted into the context:

```
Lemma px : forall (x : A),
List.In x elements -> Q x.
Proof.
intros x.
induction elements as [|y ys] eqn:Heq.
- intros H; inversion H.
- intros H.
(** Relationship Heq : elements = (y :: ys)%list exists. *)
(** However, erroneous elements = ys inserted. *)
(** https://github.com/coq/coq/issues/11784 *)
Abort.
```

```
1 goal
x, y : A
ys : list A
Heq : elements = (y :: ys)%list
IHys : elements = ys -> List.In x ys -> Q x
^^^^^^^^^^^^^
H : List.In x (y :: ys)
______________________________________(1/1)
Q x
```

In the original thread, a workaround was to use a combination of `remember`

and `revert`

in order to ensure that the equality that ended up in the induction hypothesis was universally quantified.

I can’t work out how to apply the same workaround in this example.

Is there a more general solution to this problem? I’ve heard that the `elim`

tactic from ssreflect should be able to handle this, however the documentation on the tactic is almost nonexistent:

https://coq.inria.fr/doc/V8.19.0/refman/proof-engine/ssreflect-proof-language.html#the-elim-tactic

To be clear, I’m not interested in solving this specific proof above. It’s an illustration of a problem I’ve run into several times where I need to perform induction on a specific instance, but I need to remember the fact that I’m working on a subterm of that specific instance (usually because of other hypotheses that refer to the specific instance I’m destructuring and not just any arbitrary instance).