(*CS3234 Coq Workshop script
Chak Hanrui
Aquinas Hobor*)

Require Import Classical.
Require Import ClassicalFacts.

Parameter p:Prop.
Parameter q:Prop.
Parameter r:Prop.
Parameter a:Prop.
Parameter b:Prop.
Parameter c:Prop.
Parameter d:Prop.
Parameter e:Prop.
Parameter s:Prop.
Parameter k:Prop.


Tactic Notation "spec" hyp(H) constr(a) :=
  (generalize (H a); clear H; intro H). 
Tactic Notation "spec" hyp(H) constr(a) constr(b) :=
  (generalize (H a b); clear H; intro H).
 Tactic Notation "spec" hyp(H) constr(a) constr(b) constr(c) :=
  (generalize (H a b c); clear H; intro H).
Tactic Notation "spec" hyp(H) constr(a) constr(b) constr(c) constr(d) :=
  (generalize (H a b c d); clear H; intro H).
Tactic Notation "spec" hyp(H) constr(a) constr(b) constr(c) constr(d) constr(e) :=
  (generalize (H a b c d e); clear H; intro H).


Goal
p /\ q ->
q /\ p.
Proof.
intro.
destruct H.
split.
exact H0.
assumption.
Qed.

Goal p \/ q->
q \/ p.
intro.
destruct H.
right.
auto.
left.
auto.
Qed.

Goal
a ->
b ->
c ->
d ->
(a -> b -> c -> d -> e) ->
e.
Proof. (*apply above and below the bar*)


(*intros.
apply H4.*)

(*intros.
spec H3 H.
spec H3 H0 H1. (*sort of like currying in lambda calculus*)
auto.
*)


(*intros.
apply H3 in H2;assumption.
*)

admit.
Qed.

Goal
~(p->q) ->~q.
Proof.
intro.
intro.
apply H.
trivial.
Qed.





Axiom AAA: ClassicalFacts.prop_extensionality.
Implicit Arguments AAA.
(*
Definition AAA := forall A B:Prop, (A <-> B) -> A = B.
*)



Goal
((a->b->c) = (a /\ b -> c)).
Proof.
apply AAA.
split.
intro.
intro.
destruct H0.
apply H in H0.
auto.
auto.

intros.
apply H.
auto.
Qed.



(*
http://coq.inria.fr/stdlib/Coq.Logic.Classical_Prop.html
*)

Goal
~(p->q) ->p.
Proof.
intro.
assert (~~p).
intro.
apply H.
intro.
contradiction.
apply NNPP.
auto.
Qed.


(*Now, specifially without using unfold, solve the following
problem only "intro/s" & "apply".*)

Lemma Problem1:
(p->~p)->
(~p->p)->
False.
Proof.
admit.
Qed.



(* now using any amount of "intro/s" and "apply"s (No, "apply in"!)
and just 1 destruct*)

Lemma Problem2:
(p->q\/r)->
~q->
~r->
~p.
Proof.
admit.
Qed.

Lemma Problem3:
((s\/~s)->((c->s) \/ (s->k))).
intros.
destruct H.
left.
auto.
right.
intro.
contradiction.
Qed.

Goal
p \/ ~p.
Proof. (* with Peirce's Law*)
apply Peirce.
intro.
right.
intro.
apply H.
left.
auto.
Qed.

Goal
p \/ ~p.
Proof.
generalize (Peirce (p \/ ~p)).
intros.
apply H.
intro.
right.
intro.
apply H0.
left.
auto.
Qed.


Goal
p \/ ~p.
Proof. (*with Double Negation Elimination*)
generalize (NNPP (p\/~p)).
intro.
apply H.
intro.
apply H0.
right.
intro.
apply H0.
left.
auto.
Qed.

Goal
(((p -> q) -> p) -> p).
Proof.
generalize classic.
intro.
generalize (H p).
intro.
intro.
destruct H0.
auto.
apply H1.
intro.
contradiction.
Qed.