0

When I run the Coq script below (a simplification of the original one):

Inductive w (g: nat): nat -> Prop:=
 | z: w g 0.

Lemma x:
  forall (i j: nat), w i j -> (forall k: nat, k <= k).
Proof.
Admitted.

Lemma y:
  forall (m n: nat),
  w m n -> w m n.
Proof.
  intros m n H. 
  apply x in H.

I get the following error message on the last line:

Error: Unable to find an instance for the variable k.

Can anybody explain to me why this happens and what I have to do in order to have forall k: nat, k <= k as a new hypothesis in the context?

Thanks in advance, Marcus.

2 Answers 2

1

Since your lemma x contains an inner universal quantification (the forall k part at the end), Coq does not manage to guess which natural number you want to use. By applying xto H, you only provide i and j. You have two solutions:

  1. provide the relevant k by hand using the apply x with (k := foo) in H syntax

  2. ask Coq to introduce a "meta-variable" (think of it as a typed hole that you will fill later) using the eapply tactic

Hope it helps, V.

2
  • Thanks a lot for the answer. However, I still don´t understand why Coq simply does not return (forall k: nat, k <= k) as the new hypothesis, once I have supplied H. I would appreciate if you could clarify that for me. Best Regards.
    – Marcus
    Jun 25, 2014 at 10:01
  • I honestly don't know. You should ask the devs on the Coq-club mailing list.
    – Vinz
    Jun 25, 2014 at 10:48
0

Rather than apply x in H, you can use pose proof (x _ _ H). This will give you the hypothesis you're looking for.

From the Coq tactic manual,

apply term in ident tries to match the conclusion of the type of ident against a non-dependent premise of the type of term, trying them from right to left.

I think the key point to note here is that apply only works for non-dependent premises, while the premise you want it to match, i=j, is dependent. However, the particular error message returned by Coq is confusing.

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.