(** 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.