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