(** Mathematics for Computer Scientists 2 (G52MC2)
Thorsten Altenkirch
L02 (Propositional logic)
This lecture introduces propositional logic using the proof
assistant Coq. The material in this file contains coq proofs
which can be read and animated with coqide or xemacs+proofgeneral.
**)
Section L02.
(*
We start by introducing the basic connectives of propositional
logic:
-> (implication), /\ (conjunction, and), \/ (disjunction, or)
In each case we show how to prove simple tautologies
(generic true statements).
*)
(* Assume some basic propositions *)
Variables P Q R : Prop.
(* Properties of conjunction. *)
Lemma andCom : P /\ Q -> Q /\ P.
intro pq.
elim pq.
intros p q.
split.
exact q.
exact p.
Qed.
Lemma curry : (P /\ Q -> R) -> (P -> Q -> R).
intros H p q.
apply H.
split.
exact p.
exact q.
Qed.
Lemma uncurry : (P -> Q -> R) -> (P /\ Q -> R).
intros pqr pq.
apply pqr.
elim pq.
intros p q.
exact p.
elim pq.
intros p q.
exact q.
Qed.
(*
P <-> Q is defined as (P -> Q) /\ (Q -> P)
*)
Lemma curry2 : (P /\ Q -> R) <-> (P -> (Q -> R)).
split.
exact curry.
exact uncurry.
Qed.
(* Properties of disjunction (\/) *)
Lemma orCom : P \/ Q -> Q \/ P.
intro pq.
case pq.
intro p.
right.
exact p.
intro q.
left.
exact q.
Qed.
(* True and False *)
Lemma triv : True.
split.
Qed.
Lemma exFalso : False -> P.
intro f.
case f.
Qed.
(* negation : ~A is defined as A -> False *)
Lemma contra : ~ (P /\ ~P).
unfold not.
intro pnp.
elim pnp.
intro p.
intro np.
apply np.
exact p.
Qed.