The Coq mailing list

[Christine Paulin <Christine.Paulin AT lri.fr>]

The tactic Prolog takes a set of lemmas as input and try to Apply
these theorems in turn until it solves the goal.
Actually it uses the tact EApply 
The difference between Apply and EApply appears when trying to use a
theorem like a transitivity lemma :
  trans : (x,y,z:A)(R x y)->(R y z)->(R x z)
Apply trans will fail because the argument y which appears in the
hypothesis cannot be infer from the goal

The tactic EApply trans will generate to subgoal (R a ?) and (R ? b)
sharing an existential variable to be instantiated later.

The EAuto tactics is based on the Auto tactic which uses a data base
of tactics to be tried in turn.

If we try to introduce the theorem trans for subsequent use by the
Auto tactic (Hints Resolve trans) there is a warning mentioning that
trans will only be used by the EAuto tactic.

So the behavior of EAuto is try to solve the goal with the current
Hints database using also the tactics EApply thm which appears in the
database. 

Prolog thm1 ... thmn is consequentely equivalent to 
Hints Resolve thm1 ... thmn : local_prolog
followed by EAuto with local_prolog

The EAuto tactics accepts also extra arguments for choosing between
depth-first and breadth-first search and limiting the size of the
search-tree. 

Christine Paulin


Robert R. Schneck writes:
 
 > Also, can someone explain to me the differences between the tactics
 > EAuto and Prolog?  Such as goals which one can prove but not the other?
 > 
 > Many thanks,
 > Robert
 > 

-- 
  Christine Paulin-Mohring             mailto : 
Christine.Paulin AT lri.fr
  LRI, UMR 8623 CNRS, Bat 490, Université Paris Sud,   91405 ORSAY Cedex 
  LRI   tel : (+33) (0)1 69 15 66 35       fax : (+33) (0)1 69 15 65 86
  INRIA tel : (+33) (0)1 39 63 54 60       fax : (+33) (0)1 39 63 56 84