The Coq mailing list

[Gyesik Lee <gslee AT ropas.snu.ac.kr>]

Hi Chung-Kil,

indeed using the original tactic "pattern" and tactics which are based
on it such as "rewrite" gets sometimes  really tricky as you
demonstrated. In that sense, "hpattern" would relieve the burdon of
taking care of implicit or dependent arguments. Many thanks for the
introduction.

I am just wondering about its way of inner working.
Could you give some explanations how you implemented it?
Is it possible to make the original "pattern" tactic behave like your
"hpattern" tactic?
If not, why?

Best,

Gyesik

2011/4/7 Chung-Kil Hur 
<gil.hur AT gmail.com>:
> 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 included in 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
>