coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Jean-Francois Monin <jean-francois.monin AT univ-grenoble-alpes.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] How to construct this simple proof term with tactics?
Date: Mon, 16 Apr 2018 14:19:23 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=monin AT imag.fr; spf=Neutral smtp.mailfrom=monin AT imag.fr; spf=None smtp.helo=postmaster AT zm-mta-out-2.u-ga.fr
Ironport-phdr: 9a23:rc96YRMMrlLVByErTzAl6mtUPXoX/o7sNwtQ0KIMzox0Iv79rarrMEGX3/hxlliBBdydt6ofzbKO+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxlGiTanfb9+MAi9oBnMuMURnYZsMLs6xAHTontPdeRWxGdoKkyWkh3h+Mq+/4Nt/jpJtf45+MFOTav1f6IjTbxFFzsmKHw65NfqtRbYUwSC4GYXX3gMnRpJBwjF6wz6Xov0vyDnuOdxxDWWMMvrRr0yRD+s7bpkSAXwhSkJNzA37nzZhM9+jK1UvB2uuhNxzIzab4GOL/d+YqDQcMkGSWZdRMtcVSpMCZ68YYsVCOoBOP5VoY3jqFQUqxuyHAmiBPn1xT9OmnD22qw60/88Gg/B2wwgGdMOsHLJp9jyNqcdT/q6zK/RwTXNdfNZwzH955TPchAguvGAR7dwcc3XyUkuEQPIlUiQqYrkPzOLz+gNvHKb4PRmVeKokGEnrx9+riG1yccokonGmJkVxkrK9SVj2Ys4I8CzRkB8Yd6hCpRQtieaOpN3QsMkX2FnpiI6xqcbtpGleiUB1ZcpxwbHZvCac4WE/AjvWeSTLDtimn5pZK6ziwyy/EWi0uHwS9e43VJQoidGkdTArH8A2wLJ5sWDTPZ2412v1iyV1w/J7+FJOUA0mrTfK54m2rMxl58TvV3GHi/qgkr6laiWdlg4+uSx9ejreKjmqoaTN4BukA3+PL4ultS+AeQ+LAcOQ3CW9fm82bH950H0QrdHguconqXFrJzWP8QWq6yhDw9QyIkj6hK/Dzm80NQfmHkKNFdFeBWBj4joPVHDO/H4DfKljFSjijtryerGMqX7AprRNnjDjKvhfbFl5kFAzwoz1MlT6I5QCrEcO/3+QVTxtdzdDh8hKQO42efnCNNn1oMfQ22DGKGZMLmB+WOPs+koOqyHYJIfkDf7MfksofD03lEjnlpIX6Sg2945cnm+FfNnOA28ZnzthJ9VE2oDuE8wVuXsg1qDSnhWYHCzWYoh4DAlTY28AIHETISgxbWFxCqgWJNMMDMVQmuQGGvlIt3XE8wHbzifd5c4w240EIO5Qopk7imA8Qrzyr5pNO3Rq38ZsJvsktZvtbeKyUMCsAdsBsHY6FmjCnlulzJaRjo/0+Zxux4lkwrR4e1Dm/VdUOdrybZJXwM9b8SO3ek/Dsz7HwXcYpLTDkvjTdzgDytjFt8=

Hi,

apply H. right. intro Pw. apply H. left. apply Pw.

Best regards,
JF

On Mon, Apr 16, 2018 at 12:12:23PM +0000, Soegtrop, Michael wrote:
> 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

[Coq-Club] How to construct this simple proof term with tactics?, Soegtrop, Michael, 04/16/2018
- Re: [Coq-Club] How to construct this simple proof term with tactics?, Jean-Francois Monin, 04/16/2018
  - RE: [Coq-Club] How to construct this simple proof term with tactics?, Soegtrop, Michael, 04/16/2018
- Re: [Coq-Club] How to construct this simple proof term with tactics?, Laurent Thery, 04/16/2018
- Re: [Coq-Club] How to construct this simple proof term with tactics?, Gaëtan Gilbert, 04/16/2018