Library Top.logic_tricks

This file is part of the Elfic 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.

Require Import Decidable.
Require Import Arith.

Intuitionistic tricks for decidability

Section LT.

Lemma logic_not_not : Q, False ((Q ¬Q) False).

Lemma logic_notex_forall (T : Type) :
   (P : T Prop) (x : T),
 ( x, P x) (¬ x, ¬ P x).

Lemma logic_dec_notnot (T : Type) :
   P : T Prop, x : T,
    (decidable (P x)) (P x ~~ P x).

Lemma decidable_ext: P Q, decidable P (P Q) decidable Q.

Lemma decidable_ext_aux: (T : Type), P1 P2 Q,
  decidable ( w:T, P1 w Q w)
    ( x, P1 x P2 x)
      decidable ( w, P2 w Q w).

Lemma decidable_and: (T : Type), P1 P2 (w : T),
   decidable (P1 w) decidable (P2 w) decidable (P1 w P2 w).

Strong induction

Theorem strong_induction:
  P : nat Prop,
    ( n : nat, ( k : nat, ((k < n)%nat P k)) P n)
        n : nat, P n.

Equivalent definition for existence + uniqueness

Lemma unique_existence1: (A : Type) (P : A Prop),
     ( x : A, P x) uniqueness P ( ! x : A, P x).

End LT.