coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Pierre Courtieu <pierre.courtieu AT gmail.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>, "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] rewriting of universally quantified goal
Date: Tue, 8 Jan 2019 08:04:54 +0000
Accept-language: fr-FR, en-US
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=pierre.courtieu AT gmail.com; spf=Pass smtp.mailfrom=pierre.courtieu AT gmail.com; spf=None smtp.helo=postmaster AT mail-wr1-f49.google.com
Ironport-phdr: 9a23:SKjamhR3OZs7PFPVRnJXXTZ9C9psv+yvbD5Q0YIujvd0So/mwa6yYRaN2/xhgRfzUJnB7Loc0qyK6/CmATRIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfbB/IA+qoQnNq8IbnZZsJqEtxxXTv3BGYf5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ7NYCi8mM30u683wqRbDVwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4qF2QxHqlSgHLSY0/mHJhMJtkKJVrhGvpxJ9zIHIb46YL+Bxcr/Sct4AWWZNQsZcWipcCY28dYsPCO8BMP5CoYn8uVQOtwG+ChexD+7xzT9Im2X23bE70+s/DAHNwQstH8oPsHvKttX1LrkdXfqpw6nP0DXDde9W2Tbj54jVaR0hrvSMUqhxccrV00UgCwTFjlCJpIHjIjib2OMNs22B4OphU+Kik28nqwdrojiu3MggkIfJhpgTx1vZ9it52J44KcOkREN/e9KpE5tduzuEO4doX88uWW5ltSIixrAJpZK3ZjUGxIg6yxLFb/GLbpKE7xLtWeuXPDx2nmhqeKiliBa36UWgyvPzVs2z0FtSqypKiNjMtnQU2x3d8MiLV+Jx/kmu1DuLzQzT5eZEIUc7larfNZEt2KI/lp0WsUjbHy/2nlv5jLOOe0k65uSl7/7rb7bmq5OGKYN4lBzyPr4hl8G7Geg4NxIBX2mf+eSyzr3j+kj5Ta1Sjv03jKbZqoraKtoBqqGlBA9Vz5wj6wq+Dzi4zdQVhnYHLFdfdxKGi4jlIU3BIPf9DfunmVSjjC9rx+zaPr3mGpjCMn/DkK74cblh705c1RE8wMtE55NUD7EBOOj8VlXwtNzeFB85Mha7z/zpCNVnhcsiXjfFCaiAdajWrFWg5+Q1IuDKapVf8GL2LOFg7Przh1c4n0UcdO+nx81TIDqzGe0jKEGEa1LthM0AGCEEpEB2GOftkRiJVSNZT3e0RaM1oD8hXtGIF4DGE7isjaab0W+QGYBMemFLFxjYCXblbZ+JHfwLdTiOI8J8ujMBXLmlDYQm0Ef950fB17N7I7+MqWUjvpX52Y0tvryBpVQJ7TVxSv+l/SSIRmBwkHkPQmZvjq96qE15jFyE1Poh2qAKJZlo//pMFzwCG9vE1eUjUoL9XwvAepGCT1P0Goz7UwF0dco4xpo1W2g4G9imiUqejS+jArtQiKbSQZJoo+TT2H/+I8s7wHHDhvEs

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

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

[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