(** Introduction to Formal Reasoning (G52IFR) Nicolai Kraus Tutorial 3: Bool **) Section Tutorial3. Require Import Coq.Bool.Bool. (** Repetition: discriminate **) Lemma unequ : ~(true = false). intro tf. discriminate. Qed. (** natural numbers: zero : nat suc : nat -> nat suc (suc zero) = suc zero **) (** First part: We do some lemmas **) Lemma aboutNegb : forall x : bool, negb x = true <-> x = false. intro x. unfold iff. split. unfold negb. intro. destruct x. (** discriminate. **) rewrite H. reflexivity. reflexivity. intro. destruct x. simpl. discriminate. reflexivity. Qed. Lemma boolSmall : forall x y : bool, (x = false) \/ (y = false) \/ (x = y). intros x y. destruct x. right. destruct y. right; reflexivity. left; reflexivity. left. reflexivity. Qed. Lemma oneMore : exists z : bool, exists y : bool, forall x : bool, z = x \/ y = x. exists true. exists false. intro x; destruct x. left; reflexivity. right; reflexivity. Qed. (** 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. intros a b. split. intro. destruct a. simpl in H. left. reflexivity. simpl in H. right. assumption. intro. destruct H. rewrite H. simpl. reflexivity. rewrite H. simpl. unfold orb. destruct a; reflexivity. Qed. (** If there is time left, we can define NAND for bool. NAND = "not AND" **) Definition nandb (b c : bool) : bool := match b with | true => match c with | true => false | _ => true end | _ => true end. Eval compute in (nandb true false). Eval compute in (nandb true true). Eval compute in (nandb false false). Eval compute in (nandb false true). (** 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 := ... **) Definition negbWithNAND (a : bool) : bool := nandb a a. Definition andWithNAND (a b : bool) : bool := negbWithNAND (nandb a b). Definition orWithNAND (a b : bool) : bool := nandb (negbWithNAND a) (negbWithNAND b). Definition xorWithNAND (a b : bool) : bool := orWithNAND (andWithNAND a (negbWithNAND b)) (andWithNAND (negbWithNAND a) b). End Tutorial3.