coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] weird rewriting results

From: Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] weird rewriting results
Date: Tue, 22 Jan 2019 05:17:33 +0000
Accept-language: en-US
Authentication-results: mail2-smtp-roc.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:OlOrChD9FrxgGtHXvxZEUyQJP3N1i/DPJgcQr6AfoPdwSPT8pcbcNUDSrc9gkEXOFd2Cra4c26yO6+jJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglUhzexe69+IAmrpgjNq8cahpdvJLwswRXTuHtIfOpWxWJsJV2Nmhv3+9m98p1+/SlOovwt78FPX7n0cKQ+VrxYES8pM3sp683xtBnMVhWA630BWWgLiBVIAgzF7BbnXpfttybxq+Rw1DWGMcDwULs5Xymp4aV2Rx/ykCoJNyA3/nzLisJ+j6xbrhCupx1jzIDbb46YL+Z+cbjHcN8GWWZNQsRcWipcCY28dYsPCO8BMP5coYbjvVsBsx6+BAmxD+3h0DBJiGT23ao80+88FgzI2BIvH8gQv3TRrNT5LqkcXvq7zanTyjXDaehb1i376IjVaBwuv+yDXa9qfcXL1EkiDgXIhUiTp4z9Jz6Y2fgBv3KG4+Z8V++jkXMrpg9wrzS1wsoglJHFip8Vx1zY7yl13po5KNOiREJlfNKoDIFcuzyUOoZyWs8iTX9ntSUmxrADvJO2cjQGxZUjyhPad/OKcpaH7QnmWeafITp1imxpdbeliBa8/0itzuvxXdSu3llQtCpKiNzMu2gN1xPN7siHTeNw81uv1jiSywzf9/hIL0c7m6bGMpIhxaU/mYQJvUTEAy/2hF75jKiLdkUi5+ek8fznYq/hpp+AKYB7lh3+MqUpmsy5G+g4NRUOX3Sf+eS7073j/lf1T6lNjv0ziqXZsZbaKtoHpqOhDAJZzpwv5wujAzqkytgUgHcKIVNfdB+DkYTlI1TOL+r5Dfe7jVSsijBrx/XeM7PlHJrNNGbMkLLhfLpn5UBT0gQyzctY55JSEbwOOvTzWlLruNPGExA5Lha4zPz6CNllzIMRRXqPArOFMKPVqVKH+uUvI/CVaIAJvDb9NuMq6uX1jX45nF8dZbOm0YEWaHC+BPRmIl+WbWDigtcbQi82uV90R+vzzVaGTDR7ZnCoXqt66CtxQNatCp6GTYSwipSA2j26F9tYfDYVJEqLFCLKep+JXuZERCuNOchn2mgmWKKsTp5n+Rixrwj847NhM6zZ9jBevI+1h4s93PHaiRxnrW88NM+ayWzYFzglzFNNfCc/2eVEmWI4z16C1aZihPkBT45a4e4PXwsnc5fBnbUjV4LCHznZd9LMc26IB828CGhrHNs33pkDb1s7Esjw1kmejRrvOKcckvmwPLJx8q/Y2CSude9A8C6fkYwM1hwhSMYJMnC6jKli8QSVH5TOj0iSi6etc+IbwTLJ82CAi2GJuRMBXQ==
Spamdiagnosticmetadata: NSPM
Spamdiagnosticoutput: 1:99

thanks Laurent,

Is there any way of stopping it doing this?

(For "repeat tac" to work, tac has to fail when expected)

thanks

Jeremy

On 15/1/19 7:30 pm, Laurent Thery wrote:
> Hi,
>
> ir is just that your goal
>
> Γ1 ++ Γ2 ++ (Q :: sel3)
>
> does not match exactly your rewriting pattern
>
> l ++ m ++ x :: xs
>
> so in order to make it work Coq has performed some evaluation in
> particular in your case it has unfolded some definition of cat.
>
>
> you can either refold it back afterward
>
> rewrite app_assoc_cons.
> rewrite -[_ sel3 _]/(_ ++ _).
>
> or you can first perform some computation on your goal
>
> rewrite /=.
>
> and then
>
> rewrite app_assoc_cons.
>
> --
> Laurent
>

[Coq-Club] weird rewriting results, Jeremy Dawson, 01/15/2019
- Re: [Coq-Club] weird rewriting results, Laurent Thery, 01/15/2019
  - Re: [Coq-Club] weird rewriting results, Jeremy Dawson, 01/22/2019
    - Re: [Coq-Club] weird rewriting results, Laurent Thery, 01/22/2019