Classical_Pred

Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

(* This file is a renaming for V5.10.14b, Oct 1995, of file Classical.v
   introduced in Coq V5.8.3, June 1993 *)

Classical Predicate Logic on Type

Require Import Classical_Prop.

Section Generic.
Variable U : Type.

de Morgan laws for quantifiers

Lemma not_all_not_ex :
 forall P:U -> Prop, ~ (forall n:U, ~ P n) ->  exists n : U, P n.U:Type
forall P : U -> Prop,
~ (forall n : U, ~ P n) -> exists n : U, P n
Proof.U:Type
forall P : U -> Prop,
~ (forall n : U, ~ P n) -> exists n : U, P n
intros P notall.U:Type
P:U -> Prop
notall:~ (forall n : U, ~ P n)
exists n : U, P n
apply NNPP.U:Type
P:U -> Prop
notall:~ (forall n : U, ~ P n)
~ ~ (exists n : U, P n)
intro abs.U:Type
P:U -> Prop
notall:~ (forall n : U, ~ P n)
abs:~ (exists n : U, P n)
False
apply notall.U:Type
P:U -> Prop
notall:~ (forall n : U, ~ P n)
abs:~ (exists n : U, P n)
forall n : U, ~ P n
intros n H.U:Type
P:U -> Prop
notall:~ (forall n0 : U, ~ P n0)
abs:~ (exists n0 : U, P n0)
n:U
H:P n
False
apply abs; exists n; exact H.
Qed.

Lemma not_all_ex_not :
 forall P:U -> Prop, ~ (forall n:U, P n) ->  exists n : U, ~ P n.U:Type
forall P : U -> Prop,
~ (forall n : U, P n) -> exists n : U, ~ P n
Proof.U:Type
forall P : U -> Prop,
~ (forall n : U, P n) -> exists n : U, ~ P n
intros P notall.U:Type
P:U -> Prop
notall:~ (forall n : U, P n)
exists n : U, ~ P n
apply not_all_not_ex with (P:=fun x => ~ P x).U:Type
P:U -> Prop
notall:~ (forall n : U, P n)
~ (forall n : U, ~ ~ P n)
intro all; apply notall.U:Type
P:U -> Prop
notall:~ (forall n : U, P n)
all:forall n : U, ~ ~ P n
forall n : U, P n
intro n; apply NNPP.U:Type
P:U -> Prop
notall:~ (forall n0 : U, P n0)
all:forall n0 : U, ~ ~ P n0
n:U
~ ~ P n
apply all.
Qed.

Lemma not_ex_all_not :
 forall P:U -> Prop, ~ (exists n : U, P n) -> forall n:U, ~ P n.U:Type
forall P : U -> Prop,
~ (exists n : U, P n) -> forall n : U, ~ P n
Proof. (* Intuitionistic *)U:Type
forall P : U -> Prop,
~ (exists n : U, P n) -> forall n : U, ~ P n
unfold not; intros P notex n abs.U:Type
P:U -> Prop
notex:(exists n0 : U, P n0) -> False
n:U
abs:P n
False
apply notex.U:Type
P:U -> Prop
notex:(exists n0 : U, P n0) -> False
n:U
abs:P n
exists n0 : U, P n0
exists n; trivial.
Qed.

Lemma not_ex_not_all :
 forall P:U -> Prop, ~ (exists n : U, ~ P n) -> forall n:U, P n.U:Type
forall P : U -> Prop,
~ (exists n : U, ~ P n) -> forall n : U, P n
Proof.U:Type
forall P : U -> Prop,
~ (exists n : U, ~ P n) -> forall n : U, P n
intros P H n.U:Type
P:U -> Prop
H:~ (exists n0 : U, ~ P n0)
n:U
P n
apply NNPP.U:Type
P:U -> Prop
H:~ (exists n0 : U, ~ P n0)
n:U
~ ~ P n
red; intro K; apply H; exists n; trivial.
Qed.

Lemma ex_not_not_all :
 forall P:U -> Prop, (exists n : U, ~ P n) -> ~ (forall n:U, P n).U:Type
forall P : U -> Prop,
(exists n : U, ~ P n) -> ~ (forall n : U, P n)
Proof. (* Intuitionistic *)U:Type
forall P : U -> Prop,
(exists n : U, ~ P n) -> ~ (forall n : U, P n)
unfold not; intros P exnot allP.U:Type
P:U -> Prop
exnot:exists n : U, P n -> False
allP:forall n : U, P n
False
elim exnot; auto.
Qed.

Lemma all_not_not_ex :
 forall P:U -> Prop, (forall n:U, ~ P n) -> ~ (exists n : U, P n).U:Type
forall P : U -> Prop,
(forall n : U, ~ P n) -> ~ (exists n : U, P n)
Proof. (* Intuitionistic *)U:Type
forall P : U -> Prop,
(forall n : U, ~ P n) -> ~ (exists n : U, P n)
unfold not; intros P allnot exP; elim exP; intros n p.U:Type
P:U -> Prop
allnot:forall n0 : U, P n0 -> False
exP:exists n0 : U, P n0
n:U
p:P n
False
apply allnot with n; auto.
Qed.

End Generic.