(** Introduction to Formal Reasoning (G52IFR) Nuo Li T03 **) Section T03. (* Please read the comments in courseworks completely so that you won't miss any important information *) Require Import Coq.Bool.Bool. (* What new things are added when we write the line above *) Lemma Example1 : exists x : bool, x = false. exists false. reflexivity. Qed. (* To prove the negation of P is just to prove ~P *) Lemma Example2 : ~(exists b : bool, b = true /\ b = false). intro. destruct H. destruct H. destruct x. discriminate H0. discriminate H. Qed. (* Which one we cannot simplify. Explain the reason *) Lemma simp1 : forall b : bool, (true && b) = b. simpl. reflexivity. Qed. Lemma simp2 : forall b : bool, (b && true) = b. intro. destruct b. reflexivity. simpl. reflexivity. Qed. Lemma aboutNegb : forall x : bool, negb x = true <-> x = false. destruct x; split; intro; try discriminate H; reflexivity. Qed. Lemma T01 : forall a:bool, (exists b:bool,a || b = false) -> forall b, a && b = false. intros. destruct H. destruct a. discriminate H. split. Qed. Lemma only_one: forall a : bool, exists b : bool, a && true = b || false . intro. exists a. destruct a;split. Qed. Lemma impossible : (forall a b : bool, a && b = false) -> False. intros. discriminate (H true true). Qed. (* To do the second part, please first try to understand the examples in lecture notes *) (* Redefine && and try to prove &&-associativity *) Definition andb' (a b:bool) : bool := match a with | true => b | false => false end. Definition andb (a b:bool) : bool := if b then a else false. (* Destruct as less as possible *) Lemma and_assoc : forall a b c : bool, andb (andb a b) c = andb a (andb b c). intros. destruct c. simpl. reflexivity. simpl. reflexivity. Qed. (* Use true table to find out the definition *) Definition xorb (b c : bool) : bool := if b then negb c else c. Eval compute in xorb true true. Eval compute in xorb true false. Eval compute in xorb false true. Eval compute in xorb false false. (* How many elements in Bool -> Bool Please check reference manual for case_eq ? *) (* If still have time *) (* What does this mean *) Hypothesis h1 : forall x : Guests, Celebrity x. (* Celebrities only know Celebrities *) (* First step: A General statement about all Celebrities *) Hypothesis h2_1 : forall x : Guests, Celebrity x -> P. (* Second step: who is talked about in the second part? All guests who are celebrities or all guests who are known by x ? *) Hypothesis h2_2 : forall x : Guests, Celebrity x -> (forall y : Guests, Knows x y -> P). (* Third step: what statement are we going to give for them ? *) *) Hypothesis h2_3 : forall x : Guests, Celebrity x -> (forall y : Guests, Knows x y -> Celebrity y). (* Last but not least step: REREAD your hypothesis, think of whether it is something you are intended to give *) (* There are similar questions in final exams so don't just forget them *) End T03.