The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

> Date: Sun, 03 Jul 2005 15:38:42 +0800
> From: xiang sen 
> <xiangsen AT ustc.edu>
> To: 
> coq-club AT pauillac.inria.fr
> Subject: [Coq-Club] How to determine the parameters order in "apply" tactic
> 
> Hi, all :
> 
> When I apply a lemma on the current goal , there are many parameters
> required to be specified.
> But their order seems puzzling. What 's the mechanism of order
> determination in coq. Thanks!
> 
> All the best!
> Xiang Sen
> 
> 

The first argument to apply is the theorem or function that one
wants to apply,  then you can add the keyword "with" and then you may add
extra arguments.  There are two styles:

- in the first style, you give the arguments by name or rank with
respect to the theorem or function type and the order does not matter.
Here are a few examples.

Axiom ex1 : forall a b c d, a <= b -> b <= c -> c <= d -> a <= d.

Theorem ex2 : forall x y z t u, x <= y -> y <= z -> z <= t -> t <= u -> x <= 
u.
intros x y z t u H H0 H1 H2.
(* the goal is 
  x : nat
  y : nat
  z : nat
  t : nat
  u : nat
  H : x <= y
  H0 : y <= z
  H1 : z <= t
  H2 : x <= t
  ============================
   x <= u
*)
apply ex1 with (b := y) (c:=z).
Undo.
apply ex1 with (c:=z)(b:=y).
Undo.
apply ex1 with (2:=H0).
Undo.
apply ex1 with (1:=H)(c:=z).
Undo.
apply ex1 with (1:=H)(2:=H0).
Undo.

Please note that ex1 has a functional type: this theorem is a function
that takes 7 arguments, the first 4 arguments are dependent and they
are given a name in the theorem statement.  When you use apply, the tactic
needs to know what is the value for the 2 variables that do not appear
in the theorem's conclusion "a <= d", these variables are b and c.  The
values for the variables can be given directly (the first two examples),
or they can be given by specifying the instantiations of some non-dependent
arguments of the theorem, which appear as premises of implications.

- In the second style, you don't give the arguments by name or rank, but
directly by position.  In this case, only the dependent arguments (or
universally quantified parameters of the theorem) that
do not appear in the theorem's conclusion need to be given, and in the
same order as they appear in the universal quantifications.
Here you must give the value for b and c, in this order.  Here is the example:

apply ex1 with y z.

It is sometimes difficult to infer what are the missing arguments, especially
if there are implicit arguments that are present in the theorem's conclusion
but not visible on the screen, on the other hand the order is always clear.
Anyway, I suggest you use the first style, which is more explicit.

Yves

  Yves