coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] rewriting of universally quantified goal

From: Christian Doczkal <christian.doczkal AT ens-lyon.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] rewriting of universally quantified goal
Date: Tue, 8 Jan 2019 09:41:23 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=christian.doczkal AT ens-lyon.fr; spf=Pass smtp.mailfrom=christian.doczkal AT ens-lyon.fr; spf=None smtp.helo=postmaster AT labbe.ens-lyon.fr
Autocrypt: addr=christian.doczkal AT ens-lyon.fr; prefer-encrypt=mutual; keydata= mQINBFIuNbYBEADAiZlQsnkRrXHOkaZ2mZIVNxzcBha3+HhZ8IhtxF4t5QXRNWFLtdwBuE8u D0GMB/Lacm/LujwcI756cPM/7PhrUFAyn1IrYHYsK4/O5gBEgbSBRjD0X8mJ0V3oIm/PtjMC YiXBJwzOMNXOeWp+HcyCR0eh2sQD94gbF9SUOKDoamNB3DbLEHKjYPJ9O3zQw/Xai624OXB0 Wk5yIW77I1mGWhwbWxeHOJ/NmhHEU38YfbxXSzCLeMv98bNTej4oA+cPtMZ94AZOSy/oroMh rsr6wA9PL7NS+B1kRbgv6a5KL9latAI7zPeXcVsYw076rL850PLez/SXDuIr9mud4v8Zvcp9 65vTK4lTAD4C4vneNRGt4iwCOIgGsAN6BgqEgr7EwLX8dAX57OXPKZj0/0TdCbu+qsoSrQ3u +Ul6k374jFeIndqg/e9NiJbHjYAuug3cZZ6mH24SXWtTd4hGWi6f26tQQcRyGiduZkw5Wn26 g0UVgps7o2zHwlp9LJVjL3pCw7a9tKOfZaH+h7dV5JsA/Oq+7F3PhTbyNagi4A9igw+0qU+n Ws/nZDVMRiUv+1HY4PG8q6iEGSfHHjwW8InYS+Ah3stTddJ0sLc+0AGutx8ueTE2Ks14c4c8 aNW5y9bNFI/6/UQmOOwGmBeYC/kjZhjhsC3dTJ9uX4pXlMhpLQARAQABtDFDaHJpc3RpYW4g RG9jemthbCA8Y2hyaXN0aWFuLmRvY3prYWxAZW5zLWx5b24uZnI+iQJUBBMBCAA+AhsDBQsJ CAcCBhUKCQgLAgQWAgMBAh4BAheAFiEE6jiiZvHNwp19meaCj7B3SJxkuY0FAluX/3QFCQtK /T4ACgkQj7B3SJxkuY24UQ/+L9DFIx/Z8+SGhA6h8+JvfM/N3l2IT9fsDfPTLVLoyYk6j0CR T/DTGOzmh9fCCcYJbxeNeR63vwo13B0nCKfJE1sudpJCqM/6xMMeq4IcQo4Sump24iP3V9Dg iicyXowcaMTAonwadhRyGoykdXWkaHTLLbFtuF10oO0geoyM0gy/quVmONvDZVDX6WRk0DHN vx/fRCnr3pHFm1TDp5XatQbxwDH7MqX7zS5P9onkro3lqIJiekXyPeeUVZn1OWI4Ai8RgUTZ w5RNgoj/iPtCdu0yVrL5EwEikSRrrPwqp/VLNw+hslgrdI9rtv6bf2x4AshjBoi/S4MUt3s5 3hTiLhkxMeD6iPFv70SKYdYqkhN1Y7owb0L4u9/gdODvCOofo97mv0UCTvY0hpDpiyYDM/tr 6fwSVGObSYLmjzVjrwWB1gQaDsn+ghSwwGutGEHSPdwHIy4e5qCYDaUPRWSdfxfGx3ZOO9f4 s28ufT9tJbvZK2/DPpxhGEcVQE+vMoopWJma8NoZW4IbQzqg/8vFd4w9MsMDqDsbhgOlKtpv 3GEixafUMF5wJDHEpYQaWKWf1lLg7u8FIefCaJC9E/0Wl7XhmhYx0wPQ71fOhEGmf7P1DUdy OTrZtS+O3RcM54zQjlK9lweIOPYpwW8BvgNI4+E/ev1Fv31duTniNbxSeku5Ag0EUi41tgEQ ALKCkrZVjm7Jr6wZkeYMPs+OCtICbILfcRODKsM/JxEdcxbr99UA5GGi94OXGxvkQf5yLQxG hCzrLJVbrpBvl+stg72/8DrYGCCSl72gxLTTInfFxEvH3xGpBP/oMXdGjk+jxWA48opzsaar Bd9PxvFNZoWjB9jdgzBPpNMa/ykw4ATVC2fzC5xuo4fwUsl1Wu8DFLbMVwSHGXCqmV6QYUXf 0i3EKnNkKRH3a3rd7JsrC0/6lBL8sLoT54K3J6NGii6dzalhOycsSI4R8czclof3RIy5Mh/Z /rqv4d0OgY2b7QOYnGrITVtyC5UqzGMZx0dnQr5Bm7YOHaCML/LjMoYj2ovFh2zjaU6I/smx 3stVkMRpmqB7/cYPktkpGV8K9S0l6Cgiepn9pymU0/NCBFKXrPuoorKz0+X6j6YsSy7PJ1KC EIh2nSPdhB7/4ezw3DB/COfTE8EY+xbPpTF4DfI+4ARrbP953C4Z2JC7xHUGqH+D/TQ2qYiT mfHdZTrzvWYHCERApZKq1Erdpl7mHfFnwyoDB8OqS9QWfwz3Ql8TeoFPP5LdS4PHkEqog2vH j6njJnLDLUcU5OGKVrGiu8qdMGyIJNeyY6eGcl+4RR+iNJaCVSwLDB+otbxCg2cemGAfvTI4 GGpwxXuf8/r8JL9l9Jgr/zw2WroiZwOJDhPpABEBAAGJAjwEGAECACYCGwwWIQTqOKJm8c3C nX2Z5oKPsHdInGS5jQUCW5f/dAUJC0r9PgAKCRCPsHdInGS5jbhiEACnBN29HGmlJLqLyh3H /lbZDKXWQg1KzlTiMcL/EUwrUhYLK0Lm9tsHNggQfqtnAJTW+0g/Q9wGsLDAyTaHtgPUym8j FWtPv45YfHElSwdUSzy80ZKxcw5WsD4ofpvKite4j7ehzegJF0nJ1JlPFGwRDaRoVig+cQDq jtK3fCOflsTgIcqt4gB/44x79zWSfdqag64RLMmthVWq+eRCQzFNaOH6nSUcpmXe/OTMRYx3 weqsmtLAm4kcHRdGR6bmlmOcng5gleT2TImwiW3KbRzDGFIzj/gcx6XvsonEdKGv/VgUWYvq xSnktd9/YWVUQaj+XN+C7S2p8VThkwzTxbG30jU8rgjCgci3dObipm5wkvXdI2Ojrk5wz2yD tQS1DHjE4GeC0fP2XinC3IeH8uXl1ggCxH7emzETZgM+hiM1Ijt4M80nhjbMB989q8CheOhl T/6R0G7BWKAoFo/nx+KqzWNoRX2tWPaNrbxiPdTwe3l6imJ0LYqMoNGG52+WCE98JsihXE5x 62m2vEFztbJ/CyyyIAgcdQdnVeh9N2Bhx99LdKWmxb1DLGi4nsBdtlOr4nGHbO36PbBvPp0U hMGMe8UQs41NBGp2u4avbPdQYcMBdURHHgcVPMUTQIN7D1zGPNKw/31f11BY4o3BdbLXAggJ 3dGbm2ZAnj3OQRK3Sg==
Ironport-phdr: 9a23:ODze/RShPcROW0rsIIe+5jHoPNpsv+yvbD5Q0YIujvd0So/mwa6yZxeN2/xhgRfzUJnB7Loc0qyK6/CmATRIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfbB/IA+qoQnNq8IbnZZsJqEtxxXTv3BGYf5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ7NYCi8mM30u683wqRbDVwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4qF2QxHqlSgHLSY0/n/ZisJwkaxVoxyvqBJwzIHWfI6YL/V+cr/HcN0dWWZMUMZcWipcCY28dYsPCO8BMP5Goon9vVsOrAC+BRWtBOz1zD9Dm3H43aom3OUgEgHJxgggFM8JvXvIrNX1LqYSUfupzKnJ1zrDaela1ir66IfUcxEhouuDXbZrfMXPz0kvDBrJjlGQqIziOTOZzOoNs3KC4udmSOmhhWknqwRrrTiuwMchkojJhoQPylDF7yp12og1JcegRE50YN6kDJtQtzyBOIdsXswiRGRotSAnwbMFoZ62ZDUGxZs7yxLFafGKcZKE7g/iWeuTOzt0mmxpdKynixux70Ss0PPwW8mp3FpQsCZJj9rBumoQ2xDN6cWKTOZ28F271jaVzQ/T7/lJIUAqmqrfLJ4s2rowmYAIvkvYACD6glv5jKmNdkk9/uip6+PnYrP8qp+SLY94kgD+MqIwlcyjGek0LwcDU3SB9em+1rDv51D1TbRIg/EsjKXVro7WKdwepqGjAg9V1ogj6wy4DzejyNkXgXkHLEhEeBKck4jpOkvBIPbiAfiihFSjjDZqx/PcMb3lGZjCMH7DkKz4cbZ5609czwwzwcpR55JOEr0BOu78WlfttNzECR80KxC7w+H+CNlkyoweXX+PDbSCPaPJsV6I4/ovLPOWaI8Uvjb9Mfkl6OT0gX83g19ONZWuiJAQcTWzGulsC0Sfe3vlxNkbQkkQuQ9rZ+zwiUaeUDdVL1q1VLA/7zVzXImmF4bYWoGkhvqN2yypHZRSTm1AERWIAHDuMYueDaRfIBmOK9Nsx2RXHYOqTJUsgEn35V3KjoF/J++RwRU28Jfq1dx7/erWzEpg+DpvSsCM1GfLQXsmxzpUFQ9z57h2pAlG8nnGybJx2qcKGNpIovdYVQF8O4SOl7UnWeC3YRrIe5KycHjjQtiiBmhgHNY4ydUDJUt7AJCmnxfFmSSwUecY
Openpgp: preference=signencrypt

Hi,

I understand that limiting rewriting under binders to setoid_rewrite is a
choice made for reasons of backwards compatibility, but I still feel that
there should be an option to allow the standard rewrite to also consider
subterms under binders.

I opened an issue on GitHub for this (https://github.com/coq/coq/issues/8872)
two months ago, but it has so far not received any attention.

Best,
Christian

On 1/8/19 9:04 AM, Pierre Courtieu wrote:
> Hi this is described in the following section of the ref manual:
> https://coq.inria.fr/refman/addendum/generalized-rewriting.html
>
> In short: you need to declare morphisms for the “all” combinator and it
> will only work with setoid_rewrite.
> Hope this helps
> Pierre
>
> Pierre
>
> ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
> *De :*
> coq-club-request AT inria.fr
> de la part de Jeremy Dawson
> <jeremy.dawson AT anu.edu.au>
> *Envoyé :* mardi, janvier 8, 2019 7:51 AM
> *À :*
> coq-club AT inria.fr
> *Objet :* [Coq-Club] rewriting of universally quantified goal
>
>
> Hi,
>
> I find that sometimes a goal like
>
> forall x : T, ....
>
> rewriting with some equality theorem fails (where I would expect the
> body of the goal to be rewritten), but when I do intros to eliminate the
> forall x : T quantifier, then the rewriting succeeds.
>
> I can't figure out when rewriting in this situation works and when not.
>
> can anyone explain this, and is there a way around the problem?
>
> thanks
>
> Jeremy

Attachment: signature.asc
Description: OpenPGP digital signature

[Coq-Club] rewriting of universally quantified goal, Jeremy Dawson, 01/08/2019
- Re: [Coq-Club] rewriting of universally quantified goal, Pierre Courtieu, 01/08/2019
  - Re: [Coq-Club] rewriting of universally quantified goal, Christian Doczkal, 01/08/2019