Library ex5

Blatt 5 —- Logic

SemProg SoSe 2013, Set 5

Based on the material of the online course "Software Foundations" by Pierce et al. Submit your solutions to tadeusz.m.litak at cs.fau.de
Please submit by Jun 2, anywhere on earth.
However, you are strongly encouraged to do the exercise before the Wed lecture. Submission of fully compiling file with all obligatory exericses solved by then is rewarded with 2.5 bonus points.
The file consists of 6 obligatory exercises, yielding 45 points altogether and one bonus exercise, which yields 10 additional points for those willing.

Require Export Logic.

Exercise 1: 5 points (or_distributes_over_and)

Write proof objects for distributivity of "or" over "and". That is, complete the following two definitions:

Definition or_distributes_over_and_1 : forall P Q R : Prop,
  P \/ (Q /\ R) -> (P \/ Q) /\ (P \/ R) := admit.

Definition or_distributes_over_and_2 : forall P Q R : Prop,
  (P \/ Q) /\ (P \/ R) -> P \/ (Q /\ R) := admit.

Exercise 2: 5 points (True)

Recall that during the lecture we mentioned the possibility of defining True as yet another - rather trivial - inductive proposition. Do this and as a sanity check provide proof objects for three propositions your definition should satisfy.

Inductive True : Prop := .
Definition true_top : forall P, P -> True := admit.

Definition true_prem_l : forall P, (True -> P) -> P := fun P h => admit.

Definition true_prem_r : forall P, P -> (True -> P) := fun P h t => admit.

Exercise 3 : 7.5 points (georgous_is_trivial)

Find and prove an auxiliary lemma which would allow to provide a proof object for the following proposition:

Definition georgous_is_trivial : forall n, gorgeous (n + 8) := admit.

Hint: remember how we proved equivalence of two definitions of evenness (or oddity) during the lecture? Which connective did we use? The lemma georgous_is_trivial_helper has to use the same connective. It should be a superficially stronger statement, yet obviously equivalent to forall n, gorgeous (n + 8). Of course, you're more than welcome to come up with another proof strategy

Exercise 4: 10 points (classical_equivalences)

Below, you can find a number of theorems of classical propositional logic, i.e., boolean logic. In fact, each one of these implies all others.

Definition peirce := forall P Q: Prop,
  ((P->Q)->P)->P.
Definition classic := forall P:Prop,
  ~~P -> P.
Definition excluded_middle := forall P:Prop,
  P \/ ~P.
Definition gen_ex_middle := forall P Q : Prop,
   P \/ (P -> Q).
Definition de_morgan_not_and_not := forall P Q:Prop,
  ~(~P/\~Q) -> P\/Q.
Definition implies_to_or := forall P Q:Prop,
  (P->Q) -> (~P\/Q).
Definition classical_contra := forall P Q : Prop,
   (~Q -> ~P) -> (P -> Q).

Prove the following implications:

Theorem pei_cla : peirce -> classic.
Proof. Admitted.

Theorem cla_gem : classic -> gen_ex_middle.
Proof. Admitted.

Theorem gem_em : gen_ex_middle -> excluded_middle.
Proof. Admitted.

Theorem dm_ior : de_morgan_not_and_not -> implies_to_or.
Proof. Admitted.

Theorem em_dm : excluded_middle -> de_morgan_not_and_not.
Proof. Admitted.

Theorem ior_em: implies_to_or -> excluded_middle.
Proof. Admitted.

Theorem class_contr : classic -> classical_contra.
Proof. Admitted.

Theorem contr_class : classical_contra -> classic.
Proof. Admitted.

Optionally: can you prove the remaining ones?

Exercise 5 : 10 points (constructive_existential_quantification)

Prove the following results about constructive existential quantification. Note you might need more some auxiliary lemmas.


Theorem dist_exists_or : forall (X:Type) (P Q : X -> Prop),
  (exists x, P x \/ Q x) <-> (exists x, P x) \/ (exists x, Q x).
Proof. Admitted.


Theorem forallnot_equiv_notexists : forall (X:Type) (P : X -> Prop),
  (forall x, ~ P x) <-> ~ (exists x, P x).
Proof. Admitted.

Theorem forallnotnot_equiv_notexistsnot : forall (X:Type) (P : X -> Prop),
  (forall x, ~~ P x) <-> ~ (exists x, ~ P x).
Proof. Admitted.

Theorem notforallnot_equiv_notnotexists : forall (X:Type) (P : X -> Prop),
  ~(forall x, ~ P x) <-> ~~ (exists x, P x).
Proof. Admitted.


Theorem existsnot_notforall : forall (X:Type) (P : X -> Prop),
  (exists x, ~ P x) -> ~ (forall x, P x).
Proof. Admitted.

Theorem forall_notexistsnot : forall (X:Type) (P : X -> Prop),
  (forall x, P x) -> ~ (exists x, ~ P x).
Proof. Admitted.

Theorem constructive_Berg_quantif : forall (R : Prop) (X: Type) (P : X -> Prop), (exists x, P x -> R) -> (forall x : X, P x) -> R.
Proof. Admitted.

Exercise 6 : 7.5 points (notexistsnot_forall)

The converse of forall_notexistsnot requires classical logic. Compare it with forallnotnot_equiv_notexistsnot above!

Theorem notexistsnot_forall :
  excluded_middle ->
  forall (X:Type) (P : X -> Prop),
    ~ (exists x, ~ P x) -> (forall x, P x).
Proof. Admitted.

This is the end of obligatory exercises

BONUSAUFGABE: 10 points

Here is an axiom significantly weaker than those of the classical logic:

Definition kuroda := forall (X:Type) (P : X -> Prop), (forall x, ~~ P x) -> ~~ (forall x, P x).

Prove this as a warm-up:

Theorem class_kuroda : classic -> kuroda.
Proof. Admitted.

As it turns out, this axioms also yields additional interactions between universal and existential quantification:

Theorem notforall_notnotexistsnot : kuroda -> forall (X:Type) (P : X -> Prop),
  ~ (forall x, P x) -> ~~ (exists x, ~ P x).
Proof. Admitted.

However, to prove really interesting ones, we need full strength of the classical logic:

Theorem notforallnot_exists : classic ->
  forall (X:Type) (P : X -> Prop),
     ~ (forall x, ~ P x) -> (exists x, P x) .
Proof. Admitted.

Theorem notforall_existsnot : classic ->
  forall (X:Type) (P : X -> Prop),
     ~ (forall x, P x) -> (exists x, ~ P x) .
Proof. Admitted.

And finally, if you feel some post-Berg-nostalgia, here is the full version of the Bergikirchweih paradox. Note that we need also to assume non-emptiness (inhabitation) of X for this one: we don't have it for free!

Theorem Berg_quantif : classic -> forall (R : Prop) (X: Type) (P : X -> Prop), (exists x: X, x=x) -> ((forall x : X, P x) -> R) -> (exists x, P x -> R).
Proof. Admitted.