(** Introduction to Formal Reasoning (G52IFR)
    Nicolai Kraus
    Tutorial 1

    October 09/10, 2012
**)

Section FirstTutorial.

Variable P Q R : Prop.

(** first, we repeat the basic commands **)

Lemma id : P -> P.


Lemma and : P -> Q -> P /\ Q.


Lemma proj1 : P /\ Q -> P.


Lemma inright : Q -> P \/ Q.


Lemma p2nnp : P -> ~~P.


Lemma refl : P <-> P.



(** now, let us do more complicated things **)

(** from the lecture **)
Lemma incons : ~ (P /\ ~ P).


Lemma danger : (P /\ R -> Q /\ R) -> P -> Q.


Lemma again : P \/ Q -> Q.


Lemma similar : Q \/ Q -> Q.



Require Import Coq.Logic.Classical.
(** you can use things like
assert (cl : classic P)
or
destruct (classic P)
**)

Lemma p2nnp2p : ~~P <-> P.


Lemma implToOr : (P -> Q) <-> ~P \/ Q.




End FirstTutorial.