CODEWITHSUNDEEP
coq
SDR
SDR

Reputation: 69

Unable to find an instance for the variable x, even with explicit instantiation

I'm currently working through the Logical Foundations book and I'm stuck on the last part of Exercise: 4 stars, advanced (subsequence) (subseq_trans).

Here is my definition for subseq:

Inductive subseq { X : Type } : list X -> list X -> Prop :=
  | s1 : forall l, subseq [] l
  | s2 : forall (x : X) (l l': list X), subseq l l' -> subseq l (x :: l')
  | s3 : forall (x : X) (l l' : list X), subseq l l' -> subseq (x :: l) (x :: l').

And here is my proof for subseq_trans:

Theorem subseq_trans : forall (X : Type) (l1 l2 l3 : list X),
   subseq l1 l2 -> subseq l2 l3 -> subseq l1 l3.
Proof.
  intros X l1 l2 l3 H H'.
  generalize dependent H.
  generalize dependent l1.
  induction H'.
  { intros l1 H. inversion H. apply s1. }
  { intros l1 H. apply s2. apply IHH'. apply H. }
  { intros l1 H. apply s2. apply IHH'. apply s2 in H. (* Unable to find an instance for the variable x. *) }

Here is the proof context before the failed apply:

1 subgoal
X : Type
x : X
l, l' : list X
H' : subseq l l'
IHH' : forall l1 : list X, subseq l1 l -> subseq l1 l'
l1 : list X
H : subseq l1 (x :: l)
______________________________________(1/1)
subseq l1 l

I have tried explicitly instantiating x like this:

apply s2 with (x:=x) in H

But that gives me:

No such bound variable x (possible names are: x0, l0 and l'0).

Thanks in advance.

Upvotes: 1

Views: 712

Answers (2)

eponier
eponier

Reputation: 3122

As diagnosed by @tbrk, this is a renaming done by Coq in the presence of maximal implicit arguments (see this issue). This is due to the declaration of {X : Type} in the definition of subsequence.

One solution is to use @ to turn all implicit arguments to non-implicit and avoid this renaming issue. This would give:

apply @s2 with (x:=x) in H.

Upvotes: 2

tbrk
tbrk

Reputation: 1299

You may find the eapply tactic useful to see what is going on.

...
{ intros l1 H. apply s2. apply IHH'. eapply s2 in H.

gives subseq l1 (?1 :: x :: l), where you can instantiate the ?1 with whatever you want, but, as you can now see, applying s2 forward from that assumption doesn't advance the proof.

Another possibility is to apply s2 to x and then to the assumption H:

apply (s2 x) in H.

I also find it strange that apply s2 with (x:=x) does not work. Coq seems to be doing some renaming behind the scenes, probably to avoid confusion with the x in the proof context. The following sequence applies without error:

rename x into y. apply s2 with (x:=y) in H.

Upvotes: 1

Related Questions