coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] rewriting of universally quantified goal

From: Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] rewriting of universally quantified goal
Date: Tue, 8 Jan 2019 06:51:17 +0000
Accept-language: en-US
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:wrjN8xy71nUcCO3XCy+O+j09IxM/srCxBDY+r6Qd2+0UIJqq85mqBkHD//Il1AaPAd2Lraocw8Pt8InYEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzHcBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze+/94HQbglSmDaxfa55IQmrownWqsQYm5ZpJLwryhvOrHtIeuBWyn1tKFmOgRvy5dq+8YB6/ShItP0v68BPUaPhf6QlVrNYFygpM3o05MLwqxbOSxaE62YGXWUXlhpIBBXF7A3/U5zsvCb2qvZx1S+HNsDwULs6Wymt771zRRHolikJKiI5/m/UhMxxkK1Vrx2uqgdjw4HPeoyZKOZycr/fcN4cWGFPXtxRVytEAo6ka4UAEfABMvhdr4j9ulAAowGxBAe3BOPozD9Dm3j706kk3OQ7Dw7G2QwhE8gAvnvOotT1L6ASUeauwabSyzXDcula1ing54jVaBwuu+yMUKt2fMHMykcvDxvIg1qMpYD/Ij+ZyuYAv3KG4+duVO+jkXMrpg91rzS328shipXFipgLxlzY+yh12pg5KcCkREJhfNKpHp9duzmUN4RoQc4uX2RltSM5x7EavZO2fi0HxZspxxHCdvCKdpSH7xDsWeuVJDp3mnJodK6jiBu07EOu0PfzVtOu31ZPtidFksfDtnQK1xHL9sWIROZz8lu81TqW0A7d5fxILVkzlaXANZEt2LkwlocPsUvYGS/2hUP2g7KMekU84Oio7Pjnbav6qZ+ANo90jQf+Pr4pmsyiHeQ4Ng8OX2+Y+eimyLLj+kj5TK1Ljv0wjKbZrIjXKMsHqqKjHgNZzoQu5wyiAzqo0dkUh2QLIVxBdR6fiojmIVDOIPT2DfelhFSslS9myfTYMb37HJrNK3jCnK3vc7ln5U9c0w0zzdZE6p1ODLEBPej/VVHsu9zFFBM2KRG0z/79CNphzoMeRX6PAqiBPazOtl+I//sjLPWIZI8IoznwMOMl5v7rjX8hg1ARZ6ip3Z0NaHC5BPtqOUuZYWC/yusGRC0BuRN7R+j3gnWDVyRSbjC8Reh0sjo8EcetCZrJboGrmr2ImimhSM54fGdDX3KBC3rtZs2oUugXbyTadu1siDEBRP6NQpA60heGvQnnjbdrM6zd53tL5trYyNFp6riLxlkJ/jtuApHFijDffyRPhmoNAgQO8uV6qE15xE2E1PEi0fVeCJpe6+4PWxpobMeAndw/MMj7X0f6RvnMUEyvG4/0CDcsCN893pkHfhQlQojwvlX4xyOvRoQtufmLCZgzrv2O9kXKf5847lufka4rgh8hX9dFMnCgiuhn7Q/PCoXVkkKf0aG3aaAb2y2L/2CGnzOD
Spamdiagnosticmetadata: NSPM
Spamdiagnosticoutput: 1:99

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