(** Mathematics for Computer Scientists 2 (G52MC2) Thorsten Altenkirch Exercise 3 (Bool and Predicate logic) published 15/10/08, deadline 22/10/08, 17:00 electronic submission Use $ cw submit ex03.v on one of the CS servers then look for the coursework 223 labelled 'g52mc2 coursework 3' and enter the associated code. Multiple submissions are allowed, up to the deadline. Fill in the missing proofs. You are only supposed to use the tactics introduced in the lectures, e.g. cut, exact, assumption, intro(s), apply, split, elim, left, right, case, reflexivity, rewrite(<-), destruct, discriminate. If you want to use another simple tactic not on the list, please check with your tutor. **) Section ex03. Require Import Coq.Bool.Bool. (* prove the following properties of boolean functions: (to get full points you have to use as few cases as possible) *) Lemma orb_comm : forall a b : bool, a || b = b || a. intros a b. case a. case b. reflexivity. reflexivity. case b. reflexivity. reflexivity. Qed. Lemma orb_assoc : forall a b c : bool, (a || b) || c = a || (b || c). intros a b c. case a. reflexivity. reflexivity. Qed. Lemma notb_lem : forall b:bool, negb b = true -> b = false. intro b. case b. intro ft. discriminate ft. intro h. reflexivity. Qed. (* Use rewrite or rewrite<- to prove the following properties of equality. *) Lemma sym : forall a b : bool, a = b -> b = a. intros a b. intro hab. rewrite hab. reflexivity. Qed. Lemma trans : forall a b c:bool, a = b -> b = c -> a = c. intros a b c hab hbc. rewrite hab. exact hbc. Qed. (* Define a function eqb which decides wether two booleans are equal and prove it correct. You may use some lemmas. *) Definition eqb(a b : bool) : bool := if a then b else negb b. Lemma eqb_compl : forall a:bool, eqb a a = true. intro a. case a. reflexivity. reflexivity. Qed. Lemma eqb_sound : forall a b : bool, eqb a b = true -> a = b. intros a b. case a. intro hb. symmetry. exact hb. intro hb. symmetry. apply notb_lem. exact hb. Qed. Theorem eqb_ok : forall a b : bool, a = b <-> eqb a b = true. intros a b. split. intro hab. rewrite hab. apply eqb_compl. apply eqb_sound. Qed.