Library Coq.Logic.Classical_Prop
Classical Propositional Logic
Peirce's law states forall P Q:Prop, ((P -> Q) -> P) -> P.
Thanks to forall P, False -> P, it is equivalent to the
following form
Lemma Peirce :
forall P:Prop, ((
P ->
False) ->
P) ->
P.
Lemma not_imply_elim :
forall P Q:Prop, ~ (
P ->
Q) ->
P.
Lemma not_imply_elim2 :
forall P Q:Prop, ~ (
P ->
Q) -> ~
Q.
Lemma imply_to_or :
forall P Q:Prop, (
P ->
Q) -> ~
P \/
Q.
Lemma imply_to_and :
forall P Q:Prop, ~ (
P ->
Q) ->
P /\ ~
Q.
Lemma or_to_imply :
forall P Q:Prop, ~
P \/
Q ->
P ->
Q.
Lemma not_and_or :
forall P Q:Prop, ~ (
P /\
Q) -> ~
P \/ ~
Q.
Lemma or_not_and :
forall P Q:Prop, ~
P \/ ~
Q -> ~ (
P /\
Q).
Lemma not_or_and :
forall P Q:Prop, ~ (
P \/
Q) -> ~
P /\ ~
Q.
Lemma and_not_or :
forall P Q:Prop, ~
P /\ ~
Q -> ~ (
P \/
Q).
Lemma imply_and_or :
forall P Q:Prop, (
P ->
Q) ->
P \/
Q ->
Q.
Lemma imply_and_or2 :
forall P Q R:Prop, (
P ->
Q) ->
P \/
R ->
Q \/
R.
Lemma proof_irrelevance :
forall (
P:Prop) (
p1 p2:P),
p1 =
p2.
Ltac classical_right :=
match goal with
|
_:_ |-?X1 \/
_ => (
elim (
classic X1);
intro;[
left;
trivial|right])
end.
Ltac classical_left :=
match goal with
|
_:_ |-
_ \/?X1 => (
elim (
classic X1);
intro;[
right;
trivial|left])
end.
Require Export EqdepFacts.
Module Eq_rect_eq.
Lemma eq_rect_eq :
forall (
U:Type) (
p:U) (
Q:U ->
Type) (
x:Q
p) (
h:p =
p),
x =
eq_rect p Q x p h.
End Eq_rect_eq.
Module EqdepTheory :=
EqdepTheory(
Eq_rect_eq).
Export EqdepTheory.