Library hw05_predicates

Back to Discrete Assignments

Require Import Classical.
Require Import Classical_Prop.

Section Homework5_Problems.

Variables A : Set.
Variables something: A.
Variables P Q : A->Prop.

Warmup Exercises

Lemma ex_dist_or_for : (exists x:A, P x \/ Q x) -> (ex P) \/ (ex Q).
Proof.
  Admitted.

Lemma demorgan_forall : (forall x : A, P x) -> ~ (exists y : A, ~P y).
Proof.
  Admitted.

Lemma distribute_forall:
    (forall (x:A), (P x) /\ (Q x)) <-> (forall (x:A),(P x)) /\ (forall (x:A), (Q x)).
Proof.
  Admitted.

Lemma allIMPL_exIMPL: ((forall (x:A), (P x)) -> (forall (x:A), (Q x))) -> (exists (x:A), (P x) -> (Q x)).
Proof.
  Admitted.

Problems in H5.Q5

H5.Q5.Lemma1: Can distribute 'exists' quantifier over a disjunction

Lemma sample5_1:
    (exists (y:A), (P y)) \/ (exists (y:A), (Q y)) <->
    exists (x:A), (P x) \/ (Q x).
Proof.
  Admitted.

H5.Q5.Lemma2: Some variant of De Morgans law

Lemma sample5_2: (exists (x:A), ~~(P x)) <-> ~(forall (y:A), ~(P y)).
Proof.
Admitted.

H5.Q5.Lemma3: If (P x) always implies (Q x), then the existence of some (P x0) leads to existence of some (Q x1)

Lemma sample5_3: (forall (x:A), P x -> Q x) -> ((exists (x:A), (P x)) -> exists (x:A), (Q x)).
Proof.
Admitted.

H5.Q5.Lemma4: If P being true sometimes implies that also Q is true sometimes, then there is some x0 for which (P x) implies (Q x) Note: This result would not be true, if set A is empty. It is the reason why element <tt>something</tt> was introduced.

Lemma sample5_4: ((exists (x:A), (P x)) -> (exists (x:A), (Q x))) -> (exists (x:A), ((P x) -> (Q x))).
Proof.
Admitted.

H5.Q5.Lemma5: If P(x) always implies Q(x), and P(x) is always true, then Q(x) is always true.

Lemma sample5_5: (forall (x:A), ((P x) -> (Q x))) -> ((forall (x:A), (P x)) -> forall (x:A), (Q x)).
Proof.
Admitted.

End Homework5_Problems.