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

    October 09/10, 2012
**)

Section FirstTutorial.

(** we use the following variables: **)
Variable P Q R : Prop.

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

Lemma id : P -> P.
intro p.
exact p.
Qed.


Lemma and : P -> Q -> P /\ Q.
intros.
split.
assumption.
assumption.
Qed.


Lemma proj1 : P /\ Q -> P.
intro.
destruct H.
exact H.
Qed.


Lemma inright : Q -> P \/ Q.
intro q.
(** Now, we have to choose: do we want to prove the 
   left side or the right side?
   If we choose incorrectly, we get stuck, so care! **)
right.
assumption.
Qed.


Lemma p2nnp : P -> ~~P.
unfold not.
intros.
apply H0.
exact H.
Qed.


Lemma refl : P <-> P.
split.
exact id.
exact id.
Qed.


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

(** from the lecture **)
Lemma incons : ~ (P /\ ~ P).
intro pnp.
destruct pnp as [p np].
apply np.
exact p.
Qed.


(** 
Lemma danger : (P /\ R -> Q /\ R) -> P -> Q.
Try to solve this lemma. It is not possible. 
Let us construct a counter example:

To make the formula 'danger' false, we need 
make the 'conditions' true, but the 'conclusion'
false. So:

Q: false
P: true
R: false

Now:
(P    /\ R     -> Q     /\ R)     -> P    -> Q
becomes
(true /\ false -> false /\ false) -> true -> false
and this is false!

So, we cannot prove 'danger'!
(Because this interpretation is sound.
That means, if we can prove something, it is true
for all examples, where we chose a boolean value 
for each variable.)

But care, this does not always work!
If you cannot find a counterexample, but also
don't manage to prove it, it might still be
provable with classical logic!
**)

(**
Lemma again : P \/ Q -> Q.
Same again. Try to find the counter example.
**)


Lemma similar : Q \/ Q -> Q.
intro.
destruct H.
assumption.
assumption.
Qed.



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

(** The only difference to intutionistic logic is that 
you are always allowed to assume P \/ ~P, if P is any 
proposition. **)

Lemma p2nnp2p : ~~P <-> P.
split.
intro nnp.
(** We can use the following to get an additional assumption: **)
assert (c := classic P).
(** The following is possible, but useless here: *)
assert (d := classic Q).
(** We can now use these new assumption like any other assumption. **)
destruct c.
assumption.
(** We can choose to prove something else first. Then, we can use 
whatever we have proved later. Here, we choose to prove False first: **)
assert (f : False).
apply nnp.
assumption.
(** Now, we have f : False as an assumption. Not that False is an
'empty disjunction': 
A \/ B is true if one of A, B is true (2 possibilities)
A is true if A is true (1 possibility)
False is true if one of the variables is true. But there is non. (0 possibilities)
We can use destruct and we get 0 new subgoals, so that solves the current goal **)
destruct f.
(** We have done the current goal before: **)
exact p2nnp.
Qed.


Lemma implToOr : (P -> Q) <-> ~P \/ Q.
split.
intro.
(** Is P \/ ~~P or Q \/ ~~Q more useful here? We can destruct it immediately: **)
destruct (classic P).
right.
apply H.
assumption.
left.
assumption.
intro.
destruct H.
intro.
(** We could use 'assert False' as before, but there is something quicker.
Think of H as a function: **)
destruct (H H0).
intro.
assumption.
Qed.


(** The lab sessions on Thursday are important as well! **)



End FirstTutorial.