Skip to Content.
Sympa Menu

coq-club - [Coq-Club] using a hypothesis

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] using a hypothesis


Chronological Thread 
  • From: Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>
  • To: "coq-club AT inria.fr" <coq-club AT inria.fr>
  • Subject: [Coq-Club] using a hypothesis
  • Date: Tue, 8 Jan 2019 06: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-SY3-obe.outbound.protection.outlook.com
  • Ironport-phdr: 9a23:je98dxyobtafwd/XCy+O+j09IxM/srCxBDY+r6Qd2+0UIJqq85mqBkHD//Il1AaPAd2Lraocw8Pt8InYEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzHcBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze+/94HQbglSmDaxfa55IQmrownWqsQYm5ZpJLwryhvOrHtIeuBWyn1tKFmOgRvy5dq+8YB6/ShItP0v68BPUaPhf6QlVrNYFygpM3o05MLwqxbOSxaE62YGXWUXlhpIBBXF7A3/U5zsvCb2qvZx1S+HNsDwULs6Wymt771zRRHolikJKiI5/m/UhMxxkK1Vrx2uqgdjw4HPeoyZKOZycr/fcN4cWGFPXtxRVytEAo6ka4UAEfABMvhdr4j9ulAAowGxBAe3BOPozD9Dm3j706kk3OQ7Dw7G2QwhE8gAvnvOotT1L6ASUeauwabSyzXDcula1ing54jVaBwuu+yMUKt2fMHMykcvDxvIg1qMpYD/Ij+ZyuYAv3KG4+duV++jkXMrpx1trjS328shipXFipgLxlzY+yh12pg5KcCkREJhfNKpHp9duzmUN4RoQc4uX2RltSM5x7EavZO2fi0HxZspxxHCdvCKdpSH7xDsWeuVJDp3mnJodK6jiBu07EOu0PfzVtOu31ZPtidFksfDtnQK1xHL9sWIROZz8lu81TqWyg7c6O9JLVkzlaXANZEt2LkwlocPsUvYGS/2hUP2g7KMekU84Oio7Pjnbav6qZ+ANo90jQf+Pr4pmsyiHeQ4Ng8OX2+Y+eimyLLj+kj5TK1Ljv0wjKbZrIjXKMsHqqKjHgNZzoQu5wyiAzqo0tkUh2QLIE5ZdB6fiojmIVDOIPT2DfelhFSslS9myfTYMb37HJrNK3jCnK3vc7ln5U9c0w0zzdZE6p1ODLEBPej/VVHsu9zFFBM2KRG0z/79CNphzoMeRX6PAqiBPazOtl+I//sjLPWIZI8IoznwMOMl5v7rjX8hg1ARZ6ip3Z0NaHC5BPtqOUuZYWC/yusGRC0BuRN7R+j3gnWDVyRSbjC8Reh0sjo8EcetCZrJboGrmr2ImimhSM54fGdDX3KBC3rtZs2oUugXbyTadu1siDEBRP6NQpA60heGvQnnjbdrM6zd53tL5trYyNFp6riLxlkJ/jtuApHFijDffyRPhmoNAgQO8uV6qE15xE2E1PEi0fVeCJpe6+4PWxpobMeAndw/MMj7X0f6RvnMUEyvG4/0CDcsCN893pkHfhQlQojwvlX4xyOvRoQtufmLCZgzrv2O9kXKf5848Eedka4rgh8hX9dFMnCgiuhn7Q/PCoXVkkKf0aG3aaAb2y2L/2CGnzOD
  • Spamdiagnosticmetadata: NSPM
  • Spamdiagnosticoutput: 1:99

Hi coq-club,

two questions:

(1) given a hypothesis, such as
H : forall x : A x -> B x

how do I get it into the form
A ?x -> B ?x
where ?x is to be instantiated later

(2) given a hypothesis, such as
H : A -> B
how do I get this to two subgoals, one with B as a hypothesis,
and the other with A as the conclusion
(where either A and B are too long to type in, or where I want to do
this inside an Ltac tactic, where A and B may vary)

Thanks

Jeremy

Archive powered by MHonArc 2.6.18.

Top of Page