CODEWITHSUNDEEP
coq
Marcus
Marcus

Reputation: 469

How to create a new hypothesis from apply?

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.

Upvotes: 0

Views: 1234

Answers (2)

Vinz
Vinz

Reputation: 6057

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.

Upvotes: 1

Daniel Ricketts
Daniel Ricketts

Reputation: 447

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.

Upvotes: 0

Related Questions