Induction hypotheses, again

Using Coq
1

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).

2

A concrete example from a real development (thousands of lines, so I won’t post it here):

  Lemma initialStateBarrierNeverExecuting : stateBarrierNeverExecuting initialState.
  Proof.
    unfold stateBarrierNeverExecuting.
    unfold initialState.
    unfold initialStateElements.
    unfold statusOf.

    pose proof P.elementsAreFinite as Hf.
    pose proof P.elementsUnique as Hu.

At this point, the context is:

1 goal
Hf : forall e : P.element, List.In e P.elements
Hu : List.NoDup P.elements
______________________________________(1/1)
forall (e : P.element) (a : P.agent) (n : nat),
P.elementIsBarrier e -> EExecuting a n <> EMaps.get (initialStateElementsF (EMaps.init initialStateElement) P.elements) e

Solving the proof involves induction on P.elements. The base case is easy:

    elim : P.elements => [e0|e0 es].
    - move => a n Hb.
      simpl.
      rewrite EMaps.initGet.
      elim : (initialStateElementChoice e0);
        move => Heq;
        rewrite <- Heq; discriminate.

Then:

    - move => Hbase e1 a m Hb.

At this point, I need to show that NoDup es. This would be trivial because es is a subterm of P.elements, and I have NoDup P.elements. However, the association between the two has been lost in the context (in other words, nothing in the context says that es is a subterm of P.elements in any way):

1 goal
Hf : forall e : P.element, List.In e P.elements
Hu : List.NoDup P.elements
e0 : P.element
es : list P.element
Hbase : forall (e : P.element) (a : P.agent) (n : nat),
        P.elementIsBarrier e -> EExecuting a n <> EMaps.get (initialStateElementsF (EMaps.init initialStateElement) es) e
e1 : P.element
a : P.agent
m : nat
Hb : P.elementIsBarrier e1
______________________________________(1/1)
EExecuting a m <> EMaps.get (initialStateElementsF (EMaps.init initialStateElement) (e0 :: es)) e1

Trying to use eqn or remember just runs into the issue described in the GitHub issue.

3

It seems you have simplified your problem too much, as there is a trivial proof:

Lemma px : forall (x : A), Q x.
Proof. intros x. now apply PQ, elementsHold, elementsIn. Qed.
4

It seems you have simplified your problem too much, as there is a trivial proof:

Probably. It is difficult to come up with an example where this problem turns up without also including way too much of an existing development. As I said, I’m not interested in solving that particular example proof, there are various ways to solve it, it’s just that it shows what happens when the induction tactic doesn’t work properly.

5

induction element is for proving forall elements, something about element. I don’t know if this is due to over-simplification but the fact that element is specific and not any list makes inducting on it pointless. Any induction hypothesis will be about another list than elements. eqn:H won’t save you this time.