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