(* Prove that "p /\ q, r |- q /\ r"
Problem 2 of the notes on Propositional Logic *)

Section Problem2.

Variable p q r : Prop.
Hypothesis H1 : p /\ q.
Hypothesis H2 : r.

Lemma p2 : q /\ r.

(* Solution 1 : top-down

destruct H1 as [_ H3].
split.
assumption.
assumption. *)


(* Solution 2 : bottom-up

split.
destruct H1 as [_ H3].
assumption.
assumption. *)

(* Solution 3 : using elim *)

split.
elim H1.
intros.
assumption.
assumption.

Qed.

End Problem2.






(* Prove that "p, ~~(q /\ r) |- ~~p /\ r"
Problem 5 of the notes on Propositional Logic *)

Section Problem5.

Variable p q r : Prop.
Hypothesis H1 : p.
Hypothesis H2 : ~~(q /\ r).

Lemma p5 : ~~p /\ r.

(* Intuitionistic logic fails to prove - Try the following and see what happens.

tauto.
*)

(* Import classical logic *)

Require Import Classical.

(* In particular, the thing missing from intuitionistic logic is the following *)
Print NNPP.
(* NNPP is essentially the double-negation elimination rule in
Natural Deduction for Propositional Logic : from ~~p, deduce p *)

split. intro. elim H. assumption.
Print NNPP.
apply NNPP in H2. destruct H2 as [_ H3]. assumption.

(* Here's an alternative way to prove it, using an "assert"

split. intro. elim H. assumption.
assert (q /\ r). apply NNPP. assumption.
destruct H as [_ H3]. assumption. *)

Qed.

End Problem5.