(** 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 *) (** Propositional Logic *) (** tactics for \/ -> /\ ~ ... assert, classic, NNPP *) Require Import Coq.Logic.Classical. Variable P Q R : Prop. Lemma implToOr : (P -> Q) <-> ~P \/ Q. (** 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 : 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. (** Sets *) (** know inductive definitions of sets, pattern matching, induction, etc *) Inductive Brightness := Inductive 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). (** 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. (** 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 := Lemma rneutr : forall (t : BinTree A), subst t (fun a => leaf a) = t. End RevisionPart2.