Library CoLoR.Util.Logic.ClassicUtil

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Frederic Blanqui, 2007-08-08
basic classical meta-theorems

Set Implicit Arguments.


Basic meta-theorems.

Lemma contraposee : forall P Q, (~Q -> ~P) -> P -> Q.

Lemma not_forall_imply_exists_not : forall A (P : A -> Prop),
  ~(forall x, P x) -> exists x, ~P x.


Lemma not_forall_eq : forall (A : Type) (P : A -> Prop),
  ~(forall x, P x) <-> exists x, ~P x.

Lemma imply_eq : forall P Q : Prop, (P -> Q) <-> (~P \/ Q).

Lemma not_not_eq : forall P : Prop, ~~P <-> P.

Lemma not_and_eq : forall P Q : Prop, ~(P /\ Q) <-> ~P \/ ~Q.

Lemma not_or_eq : forall P Q : Prop, ~(P \/ Q) <-> ~P /\ ~Q.

Lemma not_imply_eq : forall P Q : Prop, ~(P -> Q) <-> P /\ ~Q.

Properties of Leibniz equality on sig.


Section sig.

  Variables (A : Type) (P : A -> Prop).

  Lemma sig_eq : forall x y : sig P, proj1_sig x = proj1_sig y <-> x = y.

  Lemma inj_proj1_sig : injective (proj1_sig (P:=P)).

End sig.