The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

Notice that the destruct is not needed:
P, H |- (H (or_intror (fun Pw : P => H (or_introl Pw)))) : False

Then you can unfold that into a string of applications to get JF Monin's 
proof.

Gaëtan Gilbert

On 16/04/2018 14:12, 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