(** Mathematics for Computer Scientists 2 (G52MC2) Thorsten Altenkirch Version of 23/9/2009 L01 (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 L01. (* Assume some basic propositions *) Variables P Q R : Prop. (*** Implication (->) ***) (* Let's prove a simple tautology: *) Lemma I : P -> P. intro p. exact p. Qed. (* another example *) Lemma K : P -> (Q -> P). intro p. intro q. exact p. Qed. Lemma S : (P -> Q -> R) -> (P -> Q) -> P -> R. intro pqr. intro pq. intro p. apply pqr. exact p. apply pq. exact p. Qed.