(* cf antwoorden voor laatste opgave *)

Section proplogic.
Parameters A B C : Prop.

(* exercise 1 *)
(* complete the following simply typed lambda terms *)

Definition prop1 := fun (x : C -> B -> A) (y : C -> B) (z : C) => x z (y z).

Definition prop2 := fun (x : B -> C -> A) (y : C -> B) (z : C) => x (y z) z.

Definition prop3 := fun (x : (A -> B) -> B -> C) (y : B) => x (fun z : A => y) y.

Definition prop4 := fun (x : A -> B -> C) (y : (A -> B -> C) -> A) (z : (A -> B -> C) -> B) => x (y x) (z x).

End proplogic.

Section deptypes.

(* exercise 2 *)
(* complete the following dependently typed lambda terms *)

Definition pred1 := fun (l : Set -> Set) (A : Set) (B : Set) (f : l A -> l B) (x : l A) => f x.

Definition pred2 := fun (e : nat -> nat -> Set) (n : nat) => forall m : nat, e n m.

End deptypes.



Section drinker.

(* we will prove (twice) the drinker's paradox:
   in a non-empty domain there is someone such that
   if he drinks then everyone drinks *)

(* use the following *)
Parameter D : Set.
Parameter d : D.
Parameter drinks : D -> Prop.

(* law of excluded middle *)
Parameter em: forall p:Prop, p \/ ~p.

(* double negation law *)
Parameter dn: forall p:Prop, ~~p -> p.

(* first proof *)

(* exercise 3 *)
(* prove the following auxiliary lemma
   use dn twice, first time quite soon *)
(* With help: https://stackoverflow.com/a/4418135/1544337 *)
Lemma aux : (~ forall x:D, drinks x) -> (exists x:D, ~drinks x).
Proof.
intro F.
apply dn.
intro E.
apply F.
intro x.
assert (drinks x \/ ~drinks x).
apply em.
inversion_clear H.
exact H0.
elimtype False.
apply E.
exists x.
exact H0.
Qed.

(* exercise 4 *)
(* prove the drinker's paradox *)
(* first step: use em to distinguish two cases: everyone drinks or not *)
(* for the second case, use aux *)

Theorem drinker : exists x:D, (drinks x) -> (forall y:D, drinks y).
Proof.
assert ((forall x:D, drinks x) \/ ~(forall x:D, drinks x)).
apply em.
inversion_clear H.
exists d.
intro.
exact H0.
assert (exists x:D, ~drinks x).
apply aux.
exact H0.
elim H.
intros x H'.
exists x.
intro.
elimtype False.
apply H'.
exact H1.
Qed.

(* second proof *)

(* exercise 5 *)
(* give another proof of the drinker
   using dn in the first step and then yet another time *)
Theorem drinker2 : exists x:D, (drinks x) -> (forall y:D, drinks y).
Proof.
apply dn.
intro.
(*assert (forall x:D, ~(drinks x -> forall y:D, drinks y)).*)
assert (forall x:D, drinks x /\ ~(forall y:D, drinks y)).
intro x.
split.
assert (drinks x \/ ~drinks x).
apply em.
inversion_clear H0.
exact H1.
elim H.
exists x.
intro.
elimtype False.
apply H1.
exact H0.
intro.
apply H.
exists x.
intro.
exact H0.
elim H0 with d.
intro.
intro.
apply H2.
(* Coq accepts, but prover rejects 'apply H0' here *)
intro.
elim H0 with y.
intro.
intro.
exact H3.
Qed.

End drinker.

Section barber.

(* the barber's paradox:
   it is not the case that
   there is someone who shaves exactly everyone who does not shave himself *)

(* setting *)
Parameter V : Set.
Parameter v : V.
Parameter shaves : V -> V -> Prop.

(* the barber's paradox *)
(* exercise 6: prove the barber's paradox
   use inversion twice,
   and distinguish cases using em: x shaves himself or not *)
Theorem barber : ~ exists x : V ,
  (forall y:V, (shaves x y -> ~ shaves y y))
   /\
  (forall y:V, (~ shaves y y -> shaves x y)).
Proof.
intro.
inversion_clear H.
inversion_clear H0.
assert (shaves x x \/ ~shaves x x).
apply em.
inversion_clear H0.

assert (~shaves x x).
apply H.
exact H2.
apply H0.
exact H2.

assert (shaves x x).
apply H1.
exact H2.
apply H2.
exact H0.
Qed.


(* possible additional exercise:
   prove the more elegant formulation of the barber's paradox
   with the forall inside the /\ *)

Theorem barber2 : ~exists x:V,
  (forall y:V, (shaves x y -> ~shaves y y) /\ (~shaves y y -> shaves x y)).
Proof.
intro.
inversion_clear H.
assert (shaves x x \/ ~shaves x x).
apply em.
inversion_clear H.

assert (~shaves x x).
apply H0.
exact H1.
contradiction.

assert (shaves x x).
apply H0.
exact H1.
contradiction.
Qed.

(* version accepted by the prover: *)

Theorem barber3 : ~exists x:V,
  (forall y:V, (shaves x y -> ~shaves y y) /\ (~shaves y y -> shaves x y)).
Proof.
intro.
inversion_clear H.
elim H0 with x.
intro.
intro.

assert (shaves x x \/ ~shaves x x).
apply em.
inversion_clear H2.

apply H. exact H3. exact H3.
apply H3. apply H1. exact H3.
Qed.

End barber.