Subject: A new tactic that generalizes "pattern"

Hi coq-users,

I introduce a new tactic called "hpattern" that generalizes the tactic
"pattern".  It was developed last year. Its core part is written in ML
and integrated into Coq8.3. However, in order to use it perperly, you need
"hpattern.v", which is *not* included in Coq8.3.  It is now available
at the following address:
  
   http://www.mpi-sws.org/~gil/Hpattern/

You might have experienced that 'pattern tm' fails but something
like 'pattern tm at 2 4 5' works.  In such cases, "hpattern"
automatically finds those occurrences '2 4 5' for you. "hpattern"
is a sound and complete algorithm, so if it fails, there is no way
to abstract the term 'tm'.

Here is a simple example.

==================================================
Require Import hpattern.

Variable F: nat -> Type.
Variable G: forall {a b c d}, F a -> F b -> F c -> F d -> Type.
Variable P: Type -> Prop.
Variable a b : nat.
Variable x : F a.
Variable y : F b.

Lemma foo: a = b -> 
  (P (forall z w : F a, G x z y w) <-> P (forall z w : F b, G x z y w)).
Proof.
intro Hab.
==================================================

Try to prove the above lemma 'foo'.
'rewrite Hab' will fail.
'pattern a' and 'pattern b' will also fail.

If you carefully analyze the expression, you will find that 

'pattern a at 1 4', 'pattern a at 2 5' and 'pattern a at 1 2 4 5' 

succeed because the 1st and 4th occurrences of 'a' are connected, and 
so are the 2nd and 5th ones.

But, finding such occurrences is quite painful because you have to
even search all implicit arguments after doing something like 
"Set Printing All".

If you don't enjoy such a tedious job, you can use 'hpattern' instead. 

'hpattern a at 1' does 'pattern a at 1 4' 
because the 4th occurrence is related to the 1st one.

'hapttern a at 4' does 'pattern a at 1 4'
because the 1st occurrence is realted to the 4th one.

Similarly, 
'hpattern a at 2' does 'pattern a at 2 5' and
'hpattern a at 5' does 'pattern a at 2 5'.

However, 'hpattern a at 3' fails because there is no way to abstract
the 3rd occurrence of 'a'.

Also, you can simply do 

'hpattern a', which does 'pattern a at 1 4'

because it tries 

'hpattern a at 1', 'hpattern a at 2', ...

until it succeeds or it reaches the last occurrence of 'a'.

So the above lemma can be proved as follows.
===============================
do 2 (hpattern a; rewrite Hab).
split; auto.
Qed.
===============================

Or, more simply:
===============================
do 2 hrewrite Hab.
split; auto.
Qed.
===============================

I hope you find this useful.

Best,
Gil