coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] how to stop Coq from unfolding defined constants

From: Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] how to stop Coq from unfolding defined constants
Date: Thu, 6 Aug 2020 12:59:10 +1000
Arc-authentication-results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=anu.edu.au; dmarc=pass action=none header.from=anu.edu.au; dkim=pass header.d=anu.edu.au; arc=none
Arc-message-signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck; bh=c+DNVQfoNY27mxVOvkke7O5wYqcMq1yCufSAGmAHG48=; b=ZDfU+Fcd07t6oEsHWXc8S7OPpcsJP5BRefw7w4yGi8Jdl5a2WKD3OQujog1TtqyjLxm1tD0YacEyvljebTYQO7ArhaAzzfopdm3QweAeRA2sJDdZbRfs4r9UpBoTCY0mfOCYURQiN4+Lvz96OyJMGjA75/8OvQbEBzmppsrWLLpxRJdDeWwKCBO3BMxQRl7LHzZ7GPyUqczx81xiUPSPlcNZoU0mB+0hl/ank8meud7S/OKhd5p5S8BEsDBjpAtb6oeFR36MkVF4tADbB1FcMLcEqXSM6/kYXBOqxIN0HUC7tLJoeER+W1lzVnwLIDnm2vUvNnsFOPx6GknZ96Jt+g==
Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=a7Tfp7QgJDJgWtFUzHUXYXkozMf2J1j+WEw9DgXzdbvGcR7ZIND7KRU9auommAeCrLzlT5UDCUx0G9HDkalNV5N/mAUVVA6OOggmd78RJYiOg0G2HCB+yoV2OkXqlpsX3FbjMv/TFjG2imxNdn1xPUFdDGandZ3Q1tvGHcv0XiidNLzec7IONSx3p+jda/Drl9u0SlsvplD4HJcIeHuYV/OxHm/0WrN0iwLukDv1ko7PufEVV1E/unJoL4u2dLKcxuNdBS84Vqi6NajikbbRqYoWuVHB16ecDnoQiHxPHgiCaIhhOz1+oSWnWHAZvYcsc6yWO7WRhJZcOxjGiGjy4w==
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.mailfrom=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.helo=postmaster AT AUS01-ME1-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:8vS0JxOrg9bevCkfgPol6mtUPXoX/o7sNwtQ0KIMzox0IvX8rarrMEGX3/hxlliBBdydt6sazbWH+P6+EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCe8bL9oLhi7qQrdu8gXjIB/Nqs/1xzFr2dSde9L321oP1WTnxj95se04pFu9jlbtuwi+cBdT6j0Zrw0QrNEAjsoNWA1/9DrugLYTQST/HscU34ZnQRODgPY8Rz1RJbxsi/9tupgxCmXOND9QL4oVTi+6apgVRnlgzoFOTEk6mHaktF+grxVoByhpBJxzYDbb4OJO/RxcazdfMgXRXZCU8tLSyBNHo2xYokJAuEcPehYtY79p14WoBW6GwasHv3gyjpIh3Tr06M1yeogERrB3AwmAtkDt3Dao8vvNKgMVOC0zLPEwzvZYPJYwjf9747Ifws7rvGKQLJ8a9TexlQyFw/flFqQtJXoMjWI3esCr2aV9fBvVf6zi2E5sQFxpCCiy8gjhITVhowZ103I+Ct3zYg7JtC2R1N2bMKrHZdNtiyXM4V4T8EsTmxqpCs21KMKtJq5cSUK1Jkpxx7SZv+IfoWO/xntV/6RLC93iX55Yr6zmgq+/Eq6xuHhWMS50UxGojdLn9XQrnwA2Bje5tKaRvZ+40utwyuD2g/O5u1ePEw5lqrWJpg8ybAqjJUTq17MHirulUX2kqCWckIk9/C05uvpf7vquoKQO5ZzhA/xL6gig8u/Dv8mPQQUWGib5Pi826bk/U3kRrVFk+c6krHDsJDdOcQUuLK2AxNU0oYk7RazFTCm0MkEnXkDK1JFfxGHg5L1NFHJJfD0Ffa/g1Kynzd33/3LMaHtDo/QInTfkrrtZ6tx5kBdxQYp0NxS6Y5YBqkEIP3pW0/xsNLYDgU+Mwyx2+vpDMty1pkAVmKKAq6VKq3cvkWG5+I0JOmMYpQYtyz7K/g4/fLhk2I2mUIHcaazwJsbcGq4Eeh+I0WFfXrshc8MHnsNvgonVeDllFmCUSNIaHupRKI95jQ7CJq8AovZR4CthqaB3CahEZFMaGBGEAPELXC9fIKdHvwIdSi6I8l7kzVCW6LyZZUm0ESMuRX3zqsvAuPL4Soe/cbB2cJ44vyVuRgt7jtyJ82bzieAQ3wyl35eFGx+57x2vUEokgTL6qN/mfENTYUOtcMMaR8zMNvn98I/C932XV6eLP60cw7/B/CLWHQ2RN93xMISaUFgHdnklgrEwyehH74SkfqMGYAw9aXfmXP2IpQkkieU5Owal1AjB/B3Gyijj697+RLUAteTwUyfiuCnebla1TOfrT7fn1rLh1lRVUtLaYuARWoWPxGEpNLkoE7OUvmnFOZ/Pw==

Thanks Pierre!

On 5/8/20 8:18 pm, Matthieu Sozeau wrote:

Le 9 juil. 2020 à 15:46, Jeremy Dawson <Jeremy.Dawson AT anu.edu.au> a écrit :

Hi,

I have a goal

swapped ((single a ++ qs) ++ vs) ((qs ++ vs) ++ single a)

where single is defined by

Definition single X (a : X) := [a].

When I try

rewrite - !app_comm_cons.

it unfolds one of the occurrences of single x

(which stops my carefully written Ltac function from working and took ages to
pinpoint what was happening).

How do I stop this from happening?

Hi,

I think you have to refine the syntactic pattern to `rewrite - [(_ :: _) ++
_]!app_comm_cons`, otherwise
the inferred syntactic pattern of the rule just considers the top-level
symbol, e.g. `[_ ++ _]`
and then uses unification up-to-reduction for the subterms, which succeeds
here.

Best,
— Matthieu

Re: [Coq-Club] how to stop Coq from unfolding defined constants, Matthieu Sozeau, 08/05/2020
- Re: [Coq-Club] how to stop Coq from unfolding defined constants, Jeremy Dawson, 08/06/2020