Library Logic.logic_tricks

This file is part of the Coq Numerical Analysis library
Copyright (C) Boldo, Clément, Faissole, Martin, Mayero
This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation; either version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the COPYING file for more details.


From Coq Require Import Decidable.

Intuitionistic tricks for decidability

Section LT.

Lemma logic_dec_notnot (T : Type) :
   (P : T Prop), (x : T), (decidable (P x)) (P x ~~ P x).
Proof.
  intros P x HdP; split.
  - intros HP HnP; exact (HnP HP).
  - intros HnnP; destruct HdP as [HP | HnP]; [exact HP | exfalso].
    exact (HnnP HnP).
Qed.

End LT.