(** Introduction to Formal Reasoning (G52IFR)
    Nuo Li

    T03

    Read this part carefully in the course work.

**)

Section CW1.

Variables P Q : Prop.


(** Lemma ex04 : (P -> Q) -> ~P -> ~Q.
not provable **)

Lemma inv : forall P Q : Prop, (P -> Q) -> ~Q -> ~P.
intros p q pq nq.
intro.

(**
apply nq.
apply pq.
exact H.
**)
exact (nq (pq H)).
Qed.


Lemma ex05 : (P -> Q) -> ~~P -> ~~Q.
intro.
apply inv.
apply inv.
exact H.
Qed.

Lemma ex06 : ~( P <-> ~P ).
intro.
destruct H.
assert (~P).
intro.
exact (H H1 H1).
exact (H1 (H0 H1)).
Qed.

Require Import Coq.Logic.Classical.
(* asserts the axiom classic : P \/ ~P *)

Lemma ex08 : ~(P /\ Q) <-> ~P \/ ~Q.
split;intros.
destruct (classic P).
right.
intro.
apply H.
split;assumption.

left.
assumption.

intro.
destruct H0.
destruct H.
exact (H H0).
exact (H H1).
Qed.

End CW1.

Section T03.

Require Import Coq.Bool.Bool.


(* Which one we cannot simplify. Explain the reason *)

Definition and (a b : bool) :=
  match a with
    | true => b
    | false => false
  end.

Lemma simp1 : forall b : bool, (true && b) = b.
simpl.
reflexivity.
Qed.

Lemma simp2 : forall b : bool, (b && true) = b.
destruct b;simpl;reflexivity.
Qed.

Lemma T01 : forall a:bool,
  (exists b:bool,a || b = false) -> 
  forall b, a && b = false.
intros.
destruct H.
destruct a.
simpl.
destruct b.
unfold orb in H.
discriminate H.
reflexivity.
simpl.
reflexivity.
Qed.

(* Redefine && and try to prove &&-associativity *)


(* alternative way *)
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.
Qed.

(* Use true table to find out the definition *)

Definition xorb (a b : bool) : bool :=
  if a then negb b else b.

(* exists true, false is similar to left, right *)

Lemma only_one: forall a : bool,
 exists b : bool, a && true = b || false .
intro.
destruct a.
exists true.
split.
exists false.
split.
Qed.

(* What is the negation of exists ? *)

Lemma ne : forall P : bool -> Prop,
 ~ (exists a : bool , P a) ->
 forall a : bool, ~ (P a).
intros.
intro.
apply H.
exists a.
exact H0.
Qed.

Lemma na : forall P : bool -> Prop,
 ~ (forall a : bool, P a) ->
 exists a : bool, ~ P a.
intros.
apply NNPP.
intro.
apply H.
intro.
apply NNPP.
intro.
apply H0.
exists a.
exact H1.
Qed.

Lemma impossible : 
 (forall a b : bool, a && b = false) -> False.
intro.
discriminate  (H true true).
Qed.

End T03.


Section Pub.


Require Import Classical.

Variables People Pubs : Set.
Variable Drinks : People -> Prop.
Variable In : People -> Pubs -> Prop.


Theorem drink : 
  forall p:Pubs, (exists anybody:People,In anybody p)
  -> exists somebody:People,(In somebody p) /\
        (Drinks somebody -> forall a : People, In a p -> Drinks a).
intros.
destruct H.
destruct (classic (forall a : People, In a p -> Drinks a)).
exists x.
split.
assumption.
intro.
assumption.
apply NNPP.
intro.
apply H0.
intros.
apply NNPP.
intro.
apply H1.
exists a.
split.
assumption.
intro.
destruct (H3 H4).
Qed.

End Pub.