Apply partially instantiated lemma

2
votes

Let us assume that we want to prove the following (totally contrived) lemma.

Lemma lem : (forall n0 : nat, 0 <= n0 -> 0 <= S n0) -> forall n, le 0 n.

We want to apply nat_ind to prove it. Here is a possible proof:

Proof.
  intros H n. apply nat_ind. constructor. exact H.
Qed.

But why not directly using H in the apply tactic, using something like apply (nat_ind _ _ H) or eapply (nat_ind _ _ H) ? But the first one fails, and the second one hides the remaining goal in an existential variable.

Is it possible in apply or its derivatives to skip hypotheses in order to specify the other arguments while keeping them as classic goals in the remainder of the proof ?

3
coq
A typo: intros n H. should be intros H n. – Anton Trunov
Looks like Coq doesn't infer a proof term for P 0 a.k.a. 0 <= 0, since this works: apply (nat_ind _ (le_n _) H). – Anton Trunov
@AntonTrunov corrected, thanks. – eponier
@AntonTrunov I do not expect Coq to guess the missing proof (here it is not difficult, but more complex cases can be found). I would like Coq to leave me with one goal: 0 <= 0. – eponier

3 Answers

2
votes

If you do 

intros. refine (nat_ind _ _ H _).

then you only have 

0 <= 0

left. Is that useful in your case?

1
votes

Another approach (more universal than in my other answer) would be using the apply ... with ... construct, like this:

intros H n.
apply nat_ind with (2 := H).

Here, 2 is referring to the inductive step parameter of nat_ind (see the Coq v8.5 reference manual, 8.1.3):

In a bindings list of the form (ref_1 := term_1) ... (ref_n := term_n), ref is either an ident or a num. ... If ref_i is some number n, this number denotes the n-th non dependent premise of the term, as determined by the type of term.

0
votes

This partial proof

intros H n.
apply nat_ind, H.

will give you 0 <= 0 as the only subgoal left.

This approach uses the apply tactic, but does not answer the question in its generality, since it will work only if you want to instantiate the last parameter (which is the case for the example in the question). Here is quote from the Coq reference manual:

apply term_1 , ... , term_n

This is a shortcut for apply term_1 ; [ .. | ... ; [ .. | apply term_n ]... ], i.e. for the successive applications of term_(i+1) on the last subgoal generated by apply term_i, starting from the application of term_1.

Also, since it's just syntactic sugar, the solution may be considered cheating (and, I guess, abuse of the original intent of the Coq tactics developers) in the context of the question.