(** Introduction to Formal Reasoning (G52IFR) Thorsten Altenkirch Exercise 3 (Bool and operations on sets) published 31/10/11, deadline 8/11/11, 18:00 electronic submission Use \$ cw submit ex03.v on one of the CS servers then look for the coursework 417 labelled 'g52cfr coursework 3' and enter the associated code. Multiple submissions are allowed, up to the deadline. Try to fill in the missing proofs, using only the basic tactics presented in the lectures. Do not use any additional libraries. **) Section Ex04. Require Import Coq.Bool.Bool. (** 1 **) Section AboutBool. (* For the following proposition about bool, either prove them or prove their negation (i.e. prove ~(...)) Lemma ex31 : exists x : bool, exists y : bool, ~(x = y). Lemma ex32 : exists x : bool, exists y : bool, exists z : bool, ~(x = y) /\ ~(y = z) /\ ~(x = z). Lemma ex33 : exists x : bool, negb x = x. Lemma ex34 : forall x y : bool, x || y = y || x. Lemma ex35 : forall x : bool, exists y : bool, x || y = x && y. Lemma ex36 : exists y : bool, forall x : bool, x || y = x && y. *) End AboutBool. (** 2 **) Section Implb. (* Define an operation implb which implements implication and show its correctness. *) Definition implb(a b : bool) : bool := (* Hint: It may be a good idea to prove the two directions separately. *) Theorem implb_correct : forall a b : bool, (a = true -> b = true) <-> implb a b = true. End Implb. (** 3 **) Section Tictactoe. Open Scope type_scope. Implicit Arguments inl [A B]. Implicit Arguments inr [A B]. (** Represent the game of Tic-tac-toe (see wikipedia) using finite sets, products and coproducts. In particular define the following sets - Piece : the set pof pieces - Coord : the set of coordinates - Field : the set of contents of a field - Board : the set of boards Construct the following board as myboard : Board XXO .O. ... Define a function mirrorBoard : Board -> Board which mirrors a board along the diagonal, i.e. in the example we would get ..O .OX ..X *) End Tictactoe. (** 4 **) Section Surprise. (* Prove the following (surprising ?) theorem: Given any function f : bool -> bool, applying the function three times is the same as applying it once. Hint: It is useful to use the tactic case_eq, see the reference manual for details. *) Lemma tricky : forall (f:bool -> bool) (b:bool), f( f( f( b))) = f b. End Surprise. End Ex03.