The Coq mailing list

[Chung-Kil Hur <gil AT mpi-sws.org>]

Hi Gyesik,

Indeed, the algorithm is very simple and cool !
It is only 60 lines of ML code, which can be found in 
"tactics/extratactics.ml4"
(line 541 - 603).

I explained the algorithm in my paper presented at the last year's Coq
workshop (see Section 7).

http://www.mpi-sws.org/~gil/publications/heq.pdf

Best,
Gil



On Thu, Apr 7, 2011 at 5:14 PM, Gyesik Lee 
<gslee AT hknu.ac.kr>
 wrote:
> 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
>>
>