Apply and apply with COQ

Question

Sorry for the ambiguous question but I'm having hard time understanding the difference between apply and apply with.

Suppose I have a goal, when should I use apply and when should I use apply with? my goal is of the form: P a b. And the lemma I'm trying to apply to has forall a b. If I'm using apply, it just makes the a b constants. If I'm using apply with it generalizes the a and b.

Answer 1

When you look at a theorem statement, you can check whether the universally quantified variables appear in the final conclusion of the statement. I all of them do appear, you can use apply. If one of them does not, then it is often more practical to use apply ... with ....

Here are two examples.

Require Import Arith.
Check le_trans.
(* This says : 
  Nat.le_trans
   : forall n m p : nat, n <= m -> m <= p -> n <= p. *)
Check le_S.
(* This says :
 le_S
  : forall n m : nat, n <= m -> n <= S m *)
Check le_n.
(* This says :
 le_n
  : forall n: nat, n <= n *)m -> n <= S m

I am taking examples from the already existing Arith library. The two Check commands make it possible to verify that we are on the same page. The first one, about le_trans shows that in this theorem there is one variable, named y in my example, which does not appear in the final statement. So, when performing an apply command, this y will not be guessable by comparison with the goal at hand. For this reason, this theorem is a good candidate for apply ... with ....

Here is an example proof:

Lemma test_drive : forall x, x <= S (S x).
Proof.
intros x.
apply le_trans with (S x).
apply le_S.
apply le_n.
apply le_S.
apply le_n.
end.

When applying the theorem le_trans, the Coq system can guess which value will be used for instanciating variables named n and p, by simply comparing with the goal at the time: n should should be x and p should be S (S x). For m, a value should be given, and apply expects the user to give it, this is where we use the with clause. In this case, we can simply give the value (the order in which variables appear is being used). We choose to give S x. As a result, we obtain two goals, one with statement x <= S x and one with statement S x <= S (S x). Both goals are instances of the final statement of le_S. In turn, this lemma has the property that both universally quantified variables appear in the final statement, so apply without the with clause can be used.

The same happens later when we want to use the lemma le_n.