(** 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.
(* insert your proof here. *)

Lemma orb_assoc : forall a b c : bool, (a || b) || c = a || (b || c).
(* insert your proof here. *)

Lemma notb_lem : forall b:bool, negb b = true -> b = false.
(* insert your proof here. *)

(* Use rewrite or rewrite<- to prove the following properties of equality. *)

Lemma sym : forall a b : bool, a = b -> b = a.
(* insert your proof here. *)

Lemma trans : forall a b c:bool, a = b -> b = c -> a = c.
(* insert your proof here. *)

(* 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 :=
(* insert your definition here. *)

Theorem eqb_ok : forall a b : bool, a = b <-> eqb a b = true.
(* insert your proof here. *)