Skip to Content.
Sympa Menu

coq-club - [Coq-Club] How to construct this simple proof term with tactics?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] How to construct this simple proof term with tactics?


Chronological Thread 
  • From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
  • To: "coq-club AT inria.fr" <coq-club AT inria.fr>
  • Subject: [Coq-Club] How to construct this simple proof term with tactics?
  • Date: Mon, 16 Apr 2018 12:12:23 +0000
  • Accept-language: de-DE, en-US
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=michael.soegtrop AT intel.com; spf=Pass smtp.mailfrom=michael.soegtrop AT intel.com; spf=None smtp.helo=postmaster AT mga14.intel.com
  • Ironport-phdr: 9a23:98Xg3xwlsQbfor7XCy+O+j09IxM/srCxBDY+r6Qd2+4UIJqq85mqBkHD//Il1AaPAd2Araocw8Pt8InYEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzHcBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze+/94HdbglSmDaxfa55IQmrownWqsQYm5ZpJLwryhvOrHtIeuBWyn1tKFmOgRvy5dq+8YB6/ShItP0v68BPUaPhf6QlVrNYFygpM3o05MLwqxbOSxaE62YGXWUXlhpIBBXF7A3/U5zsvCb2qvZx1S+HNsDwULs6Wymt771zRRHolikJKiI5/m/UhMxxkK1UrwmsqAZjz4PQeoyZKOZycr3bcNgHRWRBRMFRVylZD4+ycoUPCPQOPelEr4nnoFsOtQOyDhSrCuPu1jBIhmX50rM+0+gvDArL2wkgH9MSv3TUttr6KqMSXfquzKnP0zrDYO9W2S366IjQaR0hoPeMXa5ufsrV00UgCwTFjlCJpIHjIjib2OMNs22B4OphU+Kik28nqwdtojexwscgkJTGiZwTx1vZ9it52J44KcC8RUJle9KpEJtduzuaOodoWM8uXnxktSYixrEbuJO2cjIGxZopyhLFdfCKfYyF7gj+WOuSPzt0nG9pdbO7ihqo70StyuLxWtOq3FpQsyZIk9bBu3YQ3BLJ8MeHUOFy/kK51DaPyQ/T7uZELFgxlarUMZEt37E9moASsUTFAi/5hkH2gLWKeUUj/+ik8+XnYrP4qZ+AL4J4lwXzPro0lsG/Aek0KAgDU3aB9eihybHu/VX1QLBQgf03lqnZvoraJcMepqOhBg9V05os6xalADi41NQUh2IHLFVbdxKIk4jpIVbOIOjjAPe+hVSsjClkx/TcMrL9BZXNK2DPkK39crZl905c1A0zwMhD6JJTE7ENOe78WkvstNPDFRI5KAy1w+P/CNpnzI8eWGSPArWYMKzIq1OI6PgvcKGwY9pfszHkbvMh+vTGjHkjmFZbc7Pjlc8cb2n9FfB7KW2YZ2Dti5EPCzFZkBA5Sbmgs1qPXiJJYG72F4c97TEyBYbsRdPGR4utibGFmjy8E5JKfGdeIlGKDXrsMY6DXqFfO2qpPsZ9n2lcBvCaQIg72ET27V6o+/9cNuPRvxYgm9fm3dlx6ffUkEhrpz1yE8mZlWqKSjMtxz9ad3oNxKl65HdF5BKby6Eh2q5ZE8Be47VCVQJobceBndw/MMj7X0f6RvnMSFuiRYz5UzQ+R4tthd4If0t5Xd6li0Kb0g==

Dear Coq Users,

 

doing some exercises I want to proof:

 

1 subgoal

P : Prop

H : P \/ ~ P -> False

______________________________________(1/1)

False

 

It is easy to see that this can be done with

 

destruct (H (or_intror (fun Pw : P => H (or_introl Pw)))).

 

The function argument to or_intror is (P->False) which is the ~P needed by or_intror to construct a (P \/ ~P) as argument for H. H applied to this gives False and that’s it.

 

But what I am looking for is a more conventional tactics based way to do this (except tauto – no cheating in exercises ;-). I guess I am missing something obvious …

 

Best regards,

 

Michael

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928


Archive powered by MHonArc 2.6.18.

Top of Page