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.