Library predicate_logic_answers

Predicate Logic in Coq

Section predicate_logic.
We declare the domain of quantification as a type in Set. The formulas are in Prop, so a unray predicate lives in D -> Prop
Variable D: Set.
Variable c d e :D.
Variable P Q T: D-> Prop.

Theorem example_12 : (exists x, ~ P x) -> ~forall x, P x.
Proof.
intros.
intro H1.
destruct H as [y H'].
this replaces the assumption
exists x : D, ~ P x
by a fresh variable y : D and a hypothesis H : ~ P y
also try elim H and then intros and compare.
Note that [y H'] describes the "intro pattern" for exists: we get two pieces of data, y : D and H : ~ P y
apply H'.
apply H1.
apply uses a "unification algorithm": The P x in H : forall x : D, P x is unified with the goal P y, which means that an instantiation for the universally quantified x is found such that P x equals P y. That is: we take y for x in the hypothesis H
Qed.

Theorem pred_023 : ((exists x, P x) -> forall x, Q x) ->
  forall y, P y -> Q y.
Proof.
intros.
apply H.
exists y.
This says that we take y for the existentially quantified variable in the goal exists x : D, P x
assumption.
Qed.

Theorem pred_008 : ~(forall x, P x) -> ~ forall x, P x /\ Q x.
Proof.
intros.
intro H1.
apply H.
intros x.
elim (H1 x).
intros; assumption.
Qed.

Theorem coq_pred_015 :
  ~(forall x : D, P x \/ (Q x -> T x)) -> ~forall x : D, T x.
Proof.
intros.
intro H1.
apply H.
intro x.
right.
intro H2.
apply H1.
Qed.

Theorem pred_025 : ~(forall x, P x /\ Q x) /\ (forall x, P x) ->
  ~forall x, Q x.
Proof.
intros.
intro H1.
elim H.
intros H2 H3.
apply H2.
intro x.
split.
- apply H3.
- apply H1.
Qed.

Note how a binary relation on D is declared in Coq
Variable R : D -> D -> Prop.

Theorem pred_031 : (forall x, P x /\ Q x) -> forall x, P x \/ exists y, R x y.
Proof.
intros.
destruct (H x) as [H1 H2].
left; assumption.
Qed.

Theorem pred_036 : (exists x, forall y, ~R x y) -> ~forall x, R x x.
Proof.
intros.
destruct H.
intro H1.
unfold not in H.
apply H with x.
apply H1.
Qed.

Theorem pred_013 : (exists x, P x \/ Q x) -> (forall x, ~Q x) -> exists x, P x.
Proof.
intros H H0.
Now destruct the \/ first to get two cases! This is a good rule of thumb, especially in case you get stuck: first destruct the existentials exists x, P x and the disjunctions A \/ B in the context
destruct H as [y Hy].
destruct Hy as [H1 | H2].
And now we can choose the exists
- exists y. assumption.
And this one follows from a contradiction
- destruct (H0 y). assumption.
Qed.

Theorem pred_035 : (forall y, Q y -> ~exists x, P x) /\ (forall x, P x) -> forall y, ~Q y.
Proof.
Admitted.

more difficult
Theorem pred_016 : (forall x, P x \/ R x x) -> (forall x, P x -> exists y, R x y /\ R y x) -> forall x, exists y, R x y.
Proof.
intros H H0 z.
Again: destruct the \/ first to get two cases!
destruct (H z).
-
Again: destruct the exists first to get a y0
  destruct (H0 z H1) as [y0 Hy0].
Now we can choose y
  exists y0.
  destruct Hy0; assumption.
- exists z; assumption.
Qed.

Theorem pred_067 : (forall x, ~P x) -> ~exists x, P x.
Proof.
Admitted.

Predicate logic with equality


Theorem example_14 : forall x y, R y y /\ x = y -> R y x.
Proof.
intros.
destruct H as [H1 H2].
rewrite <- H2 in H1.
rewrite <- H2.
rewrite H2 replaces x by y in the goal. Also try
rewrite <- H2
and see what happens. Also try
rewrite <- H2 in H1
and see what happens
assumption.
Qed.

Variable W : D -> D -> D -> Prop.

Theorem example_17 : forall x y, W x x y /\ x = y -> W x y y.
Proof.
intros.
destruct H.
rewrite H0.
rewrite H0 in H.
assumption.
Qed.

Theorem pred_059 : (forall x:D, forall y, x = y) -> (exists x, P x) -> forall x, P x.
Proof.
intros.
destruct H0.
rewrite (H x x0).
assumption.
Qed.

Theorem pred_058 : (forall x:D, forall y, x = y) /\ P d -> P e.
Proof.
Admitted.

Section pred_080.

Hypothesis Domain : forall x, (x = c \/ x = d \/ x = e).

Theorem pred_080 : (forall x, P x) -> P e /\ P d /\ P c.
Proof.
Admitted.

End pred_080.

Challenge Problem

This theorem shows that if we have a transitive relation on a 3-element set, and if each element has a successor, then some element must be reflexive for this relation

Section pred_078.

Hypothesis Domain : exists x1, exists x2, exists x3, forall x:D, (x = x1 \/ x = x2 \/ x = x3).
Hypothesis Successor : forall x, exists y, R x y.
Hypothesis Transitive : forall x, forall y, forall z, R x y /\ R y z -> R x z.

Theorem pred_078 : exists x, R x x.
Here is a structured proof that clearly shows the cases and also shows that there is a lot of repetition in the proof. But note that the repeating parts are not literally the same. It is not so clear here how one can subsume these into one proof that is repeated. But one can copy-paste pieces of proof script, replay it in the new case and repair the parts where it fails, i.e. fill in the appropriate variables at the right spot.
Note: naming the introduced variables yourself helps, so use destruct as in stead of destruct.
Proof.
destruct Domain as [x1 [x2 [x3 H]]].
destruct (Successor x1) as [x4 Hx4].
x4 = Successor x1
destruct (H x4) as [H1 | [H2 | H3]].
3 cases
*
case x4 = x1
  exists x1; rewrite H1 in Hx4 ; apply Hx4.
*
case x4 = x2
  rewrite H2 in Hx4. destruct (Successor x2) as [x5 Hx5].
  destruct (H x5) as [H51 |[H52 | H53]].
3 cases
  +
case x5 = x1
    rewrite H51 in Hx5. exists x1. apply Transitive with x2.
    split; assumption.
  +
case x5 = x2
    rewrite H52 in Hx5. exists x2; assumption.
  +
case x5 = x3
    rewrite H53 in Hx5. destruct (Successor x3) as [x6 Hx6].     destruct (H x6) as [H61 |[H62 | H63]].
3 cases
    -
case x6 = x1
      rewrite H61 in Hx6. exists x1. apply Transitive with x3. split.
      apply Transitive with x2. split; assumption. assumption.
    -
case x6 = x2
      rewrite H62 in Hx6. exists x2. apply Transitive with x3. split; assumption.
    -
case x6 = x3
      rewrite H63 in Hx6. exists x3. assumption.
*
case x4 = x3 This case is very much the same as case x4 = x2
  rewrite H3 in Hx4. destruct (Successor x3) as [x5 Hx5].
  destruct (H x5) as [H51 |[H52 | H53]].
3 cases
  + rewrite H51 in Hx5. exists x1. apply Transitive with x3.
      split; assumption.
  + rewrite H52 in Hx5. destruct (Successor x2) as [x6 Hx6].
    destruct (H x6) as [H61 |[H62 | H63]].
3 cases
    - rewrite H61 in Hx6. exists x1. apply Transitive with x2. split.
      apply Transitive with x3. split; assumption. assumption.
    - rewrite H62 in Hx6. exists x2. assumption.
    - rewrite H63 in Hx6. exists x3. apply Transitive with x2. split;assumption.
  + rewrite H53 in Hx5. exists x3; assumption.
Qed.

End pred_078.

End predicate_logic.