The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

Could a type of automation hint be added to Coq that helps with forward 
chaining?

Of course, (e)auto Extern hints are general enough to be used to do 
forward chaining.  One can write something like this:

Hint Extern 10 => match goal with H : T |- _=> pose proof (Lem H) end.

so that during (e)auto, whenever a hypothesis of type T is present, the 
automation will add a new hypothesis based on lemma Lem. However, this 
slows automation significantly, because nothing stops it from adding 
duplicates of that new hypothesis, with these duplicates needlessly 
adding to the backtracking strain.  Also, this only produces one 
parameterization of Lem, not all of them.

It's possible to do this instead:

Hint Extern 10 => repeat match goal with H : T |- _=> let H':=fresh in 
pose proof (Lem H) as H'; fail_if_redundant H' end.

where fail_if_redundant (see below) checks to see if another hyp with 
the same type as H' already exists, and fails if one does. This produces 
all parameterizations of Lem without duplicates, but slows automation a 
lot due to repeated useless attempts at firing this hint, and the 
internal backtracking for duplicate prevention. Also, if some further 
(e)auto processing of the goal purposefully removed one such new 
hypothesis (by some elimination - like destruct), this hint would make 
it re-materialize, perhaps causing even more costly needless proof 
searching to get triggered.

The problem is that there is currently no way to trigger an action to 
occur only when a new hypothesis of a certain type is added to a goal.  
But suppose there was such a mechanism.  The interface might look like this:

Hint FChain (H : T) =>  pose proof (Lem H).

The semantics would be - during (e)auto, if a new hypothesis H with a 
type matching the type pattern T is added to the goal, then trigger the 
rhs tactic of each applicable FChain hint immediately after the 
completion of the hint that added H.  The same hint wouldn't get 
triggered twice for the same hypothesis.  It might make sense to add a 
cost to each FChain hint, which would delay the triggering of that 
FChain hint until just before other non-FChain hints of similar cost - 
so that the general form would be:

Hint FChain <cost> <hyp pattern> => <tactic> : <dbs>.

For hypotheses that already exist in the goal at the time the (e)auto 
tactic is started, they are all considered new, and so all will trigger 
any applicable FChain hints.  One could also have a tactic [autofchain 
with dbs] that, like autounfold and autorewrite, used the hints outside 
the context of (e)auto.

Does a feature like this sound useful?

Maybe typeclasses might be able to do things similar to this, but I'm no 
typeclass expert.  Do any typeclass experts know if (and how) it can?

-- Jonathan


Note:

Ltac fail_if_redundant H :=
  let T:=type of H in
  try (clear H; lazymatch goal with _: T |- _ => fail 1 | _ => fail end).