(*

Midland Graduate School 2008: COQ

*)

Section Basics.

Variables P Q R : Prop.

Lemma S : (P -> Q -> R) -> (P -> Q) -> P -> R.
intros.
apply H.
assumption.
apply H0.
assumption.
Qed.

Print S.

Lemma S_clever :  (P -> Q -> R) -> (P -> Q) -> P -> R.
auto.
Qed.

Print S_clever.

Lemma dm1 : ~(P \/ Q) <-> ~P /\ ~Q.
split.
auto.
intros.
intro.
destruct H.
case H0.
auto.
auto.
Qed.

Lemma dm1_clever : ~(P \/ Q) <-> ~P /\ ~Q.
tauto.
Qed.

Print dm1.

Print dm1_clever.

Require Import Classical.

Print classic.

Lemma indirect : forall X:Prop,~~X -> X.
intros.
case (classic X).
auto.
intro.
contradiction.
Qed.

Lemma dm2 : ~(P /\ Q) <-> ~P \/~Q.
split.
2 : tauto.
intros.
apply indirect.
tauto.
Qed.