(** Introduction to Formal Reasoning (G52IFR) Nicolai Kraus, Nuo Li Tutorial 8 November 27/28, 2012 **) Section RevisionPart1. (** 4 out of 6 parts to be completed in the exam *) (** 1. Propositional Logic *) (** tactics for \/ -> /\ ~ ... assert, classic, NNPP *) Require Import Coq.Logic.Classical. Variable P Q R : Prop. Lemma implToOr : (P -> Q) <-> ~P \/ Q. split. intro pq. destruct (classic P). right; exact (pq H). left; assumption. intros npq p. destruct npq. destruct (H p). assumption. Qed. (** Predicate logic *) (** tactics for exists, forall, formalize statements *) Variable PeopleInPub : Set. Variable Drinks : PeopleInPub -> Prop. (** Formalize the statement: If there is someone in the pub, then we can find a person X such that: If X drinks, then everybody drinks! *) Hypothesis drinker : (exists p : PeopleInPub, True) -> exists X : PeopleInPub, (Drinks X -> forall y : PeopleInPub, Drinks y). End RevisionPart1. Section RevisionPart2. (** Bool *) (* inductive type -> you can use 'destruct' (or 'induction'), and case_eq *) Require Import Coq.Bool.Bool. Lemma forallExists : forall x : bool, exists y : bool, x || y = x && y. intro x; destruct x. exists true; reflexivity. exists false; reflexivity. Qed. (** Sets *) (** know inductive definitions of sets, pattern matching, induction, etc *) Inductive Brightness := | light : Brightness | dark : Brightness. Inductive Colour := | red : Brightness -> Colour | blue : Brightness -> Colour | green: Brightness -> Colour | white: Colour | black: Colour. (** Arithmetic *) (** lemmas for +, * know how to do induction on natural numbers *) Require Import Coq.Arith.Arith. Lemma exchange : forall a b x y, (x + y) + (a + b) = (x + a) + (y + b). intros. repeat rewrite plus_assoc. pattern (x + y + a). rewrite <- plus_assoc. pattern (y + a). rewrite plus_comm. rewrite plus_assoc. reflexivity. Qed. (** Lists *) (** know how they are constructed know rev, length, map ... know simple lemmas: app_nil_r, app_nil_l, ... *) Require Import Coq.Lists.List. Set Implicit Arguments. Fixpoint map (A B : Set)(f : A -> B)(l : list A) : list B := match l with | nil => nil | a :: l => f a :: map f l end. Variables A B C : Set. Lemma map_comp : forall (l : list A)(f : A -> B)(g : B -> C), map g (map f l) = map (fun a => g (f a)) l. intros. induction l; simpl. reflexivity. rewrite IHl. reflexivity. Qed. (** Trees, Expressions, Compilers *) (** similar to lists *) Inductive BinTree (X : Set) : Set := leaf : X -> BinTree X | node : BinTree X -> BinTree X -> BinTree X. Fixpoint subst (A B : Set) (bina: BinTree A) (a2binb: A -> BinTree B) : BinTree B := match bina with | leaf a => a2binb a | node t1 t2 => node (subst t1 a2binb) (subst t2 a2binb) end. Lemma rneutr : forall (t : BinTree A), subst t (fun a => leaf a) = t. intros. induction t; simpl. reflexivity. rewrite IHt1. rewrite IHt2. reflexivity. Qed. End RevisionPart2.