(** Introduction to Formal Reasoning (G52IFR)
    Nicolai Kraus

    Tutorial 3: Bool
**)

Section Tutorial3.

Require Import Coq.Bool.Bool.


(** Repetition: discriminate **)

Lemma unequ : ~(true = false).



(** First part: We do some lemmas **)

Lemma aboutNegb : 
   forall x : bool, negb x = true <-> x = false.



Lemma boolSmall : forall x y : bool, 
   (x = false) \/ (y = false) \/ (x = y).



Lemma oneMore : exists z : bool, exists y : bool, 
   forall x : bool, z = x \/ y = x.




(** Second part: We define or for 
bool and prove that it is correct **)

Definition orb (b c : bool) : bool :=
   if b then true else c.


Lemma orb_correct : forall a b : bool, 
   orb a b = true
      <->
   a = true \/ b = true.



(** If there is time left, we can 
define NAND for bool. NAND = "not AND" **)
Definition nandb (b c : bool) : bool := 


Eval compute in (nandb true false).

(** AND is functional complete 
(more precisely, the set containing NAND)! 
This means, we can define every function 
on bool by only using NAND **)

(** for example: 
Definition negb2 (b : bool) : bool :=
Definition orb2 (a b : bool) : bool := 
... 
**)

End Tutorial3.