coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] ltac error?

From: Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] ltac error?
Date: Sun, 7 Apr 2019 15:24:02 +0000
Accept-language: en-CA, en-US
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=fdhzs2010 AT hotmail.com; spf=Pass smtp.mailfrom=fdhzs2010 AT hotmail.com; spf=Pass smtp.helo=postmaster AT NAM02-BL2-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:Xo5WiRbXR8vMPyKx6icXI2//LSx+4OfEezUN459isYplN5qZrsm8bnLW6fgltlLVR4KTs6sC17OP9fm5EjxcqdbZ6TZeKcQKD0dEwewt3CUYSPafDkP6KPO4JwcbJ+9lEGFfwnegLEJOE9z/bVCB6le77DoVBwmtfVEtfre9FYHdldm42P6v8JPPfQpImCC9YbRvJxmqsAndrMYbjZZ/Jqor1xfFv3REdudZyGh1IV6fgwvw6t2/8ZJ+7yhcoe4t+9JFXa7nY6k2ULtUASg8PWso/sPrrx7DTQWO5nsYTGoblwdDDhbG4h/nQJr/qzP2ueVh1iaUO832Vq00Vi+576h3Uh/oiTwIOCA//WrKl8F/lqNboBampxxi347ZZZyeOfRicq/Be94RWG1OUNtMVyxaGoOzcZcAD/YPM+ZfqonyvVoOrR2jDgWoC+7izjpEi3nr1qM4zushCxnL0gw+EdwTrHTaotb7NKkQXu+pw6bF1i/MY+9K1Trn9ITEbg4trPeRVrxwa8rRzkwvGhvBgFqKsozlODWV3fkUv2eY7+pgUuSvi2E6oA9sojig2MEsiobQiokIyF7E6DhyzYE7JdKlSE56YMWkHIVMuy2HK4d7WcMiQ2Z0uCY/0LIGuJq7cDIWx5Qgwh7ScvqKeJWG7BLkUeaeOzZ4hHR9dbKwhhay7UigyvDnWcWu0VZKqSxImcTPuHAVzxHe5dSLRuF580u/wzqC2Rrf5+NALEwsm6rUNZ0szqI1m5cWrEjPAiH2l1nzgaKWa0kp+uql5uH8bbr6qJKTKop5hhzjPqktnsGyB/kzPBIUUGiB4+u80aXu/U3nT7VOif07irHXvYzdK8gHuKK1GhJY3IA95xqmCDepy8oXkWMALFJYZBKIlI/pO0zIIP/lF/u/m06skDB3x//YIrLhHpTNLn/FkLv7erZ99lJcyA40zdBY5JJYEK0OIPX2WkPptdzYCAE2MxCszuvoFNlxzIcTVXyVDqKXKq/fs1uF6voqI+aWZY8VvDj9K+Ii5/7rlXI5l0ISfamo3JsMdny0AulqL1mCbHrshdcBDWIKsRA/TOzuklGNTTlTZ3OqU6Im+j47EJ6mDZvERo21nLOB2z67EoRKaWBCF1CDCmzld56EWvcJcCKdONVtkj0CVbi7So8uzwuitAHgy+kvEu2BsCYfrNfo0MV/z+zVjxA7szJuRYzJ2GaUCmpwg2kgRjks3ak5r1YrmXmZ1q0tofVDEtobosFJVQE1faXcwup1TpjSR0qVcNuJWk38Goz+KTE2Utc4wttIaEF4TYbxxivf1janVudG34eAA4Y5p/6NhimjF4NG03/DkZIZoRwjS8pLO3ehg/ckpQjUG4vAkkHfnKGvJ/1FgHz9sVybxG/Lh3l2FRZqWPyeD3AYek7frNC/7UTHHef3VOYXdzBZwMvHEZNkL93kiVIaG6XFEfGGOSebvz31AhyFgLSRcIDtZmMRmj3HD1QJmBwS+nDAMhUiAiCmoCTVCzk8TF8=

did you try

ltac:(rewrite app_assoc)

my wild guess is Ltac is parsing the arguments as Gallina terms because your terms look like term applications.

Thanks,

Jason Hu

https://hustmphrrr.github.io/

From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>
Sent: April 7, 2019 11:17 AM
To: coq-club AT inria.fr
Subject: [Coq-Club] ltac error?

Hi,

I have an Ltac "program" as follows:

Ltac nsgen drs nsr rs c sppc q qin acm inps0 at1 at2 :=
...
at1 ;
...
at2 ;
...

Calling it as follows failed:
nsgen drs nsr rs pp sppc q qin acm inps0 (rewrite app_assoc)
(rewrite app_assoc).
with the message Error: The reference rewrite was not found
in the current environment.
but it succeeded, after defining
Ltac rwapas := rewrite app_assoc.
as follows
nsgen drs nsr rs pp sppc q qin acm inps0 rwapas rwapas.

Then I tried
Ltac rw3 pp1 := rewrite app_assoc ; rewrite (app_assoc _ pp1).
and calling it as
nsgen drs nsr rs c sppc q qin acm inps0 (rw3 pp1) rwmb.
failed with the message
Error: The reference rw3 was not found in the current environment.

What am I doing wrong here?

Thanks

Jeremy

[Coq-Club] ltac error?, Jeremy Dawson, 04/07/2019
- Re: [Coq-Club] ltac error?, Jason -Zhong Sheng- Hu, 04/07/2019