The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

I am trying to understand the various ways there are in Coq to get a 
hole (implicit arg subgoal, or "_" in a term) to have a proof attempted 
on it automatically, without the need to explicitly supply a term or 
call a tactic.

AFAICT, there are 4 varieties of ways:

- typeclasses

- canonical structures

- Declare Implicit Tactic

- Program with Obligation Tactic

Are there any I left out?

Below is my attempt at rough descriptions of what these do - but not 
being an expert, I would greatly appreciate any corrections:

I think the most restrictive is Program/Obligation Tactic - which 
requires that one starts the definition in Program mode, and only solves 
holes generated from that top-level Program definition - hence it cannot 
be used in the middle of a proof or non-Program definition.  But, it has 
no restriction on the type (conclusion) of the holes it can try to solve.

Typeclasses automatically attempt to solve holes generated at any point, 
but only if the initial hole is an exact match (modulo intros) for a 
type declared in the appropriate way as a class. Once typeclass 
resolution is started in the initial hole, any subsequent subgoal holes 
generated from there can be solved using hints or classes (the search 
done by typeclasses eauto).  The Existing Class command can extend the 
initial hole types to previously defined non-class types.  However, the 
match for the initial hole still has to be exact.

I am not as familiar with canonical structures as typeclasses. I think 
with canonical structures there is a further restriction that the hole 
be a hole in a projection term - not a hole in an arbitrary term.  
However, canonical structures will do reduction on the type of the hole 
to find a match - which among other things makes overlapping matches 
possible.  But, AFAIK, unlike typeclasses, there is no way to declare 
matches for some pre-existing type (for example, eq) because there is no 
way to declare post-hoc projections for pre-existing types.  In other 
words, there is nothing like the typeclass Existing Class declaration.  
Is that right?

Declare Implicit Tactic is a bit of a backwater in Coq - apparently 
little used since its introduction in 8.1, and it seems to have suffered 
some amount of bit-rot since then.  However, it apparently would have 
the least restrictions - any hole of any type produced at any time would 
fire the tactic so declared.  But, I think the tactic must solve all 
goals it attempts, unless this can be subverted via the shelve tactic 
(as in Declare Implicit Tactic (try mytac; shelve).)


Suppose one were to describe what happens starting with the formation of 
an arbitrary hole.  How do these competing hole-fillers interact?

-- Jonathan