Library predicate_logic

Predicate Logic in Coq

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.
Admitted.

Theorem coq_pred_015 :
~(forall x : D, P x \/ (Q x -> T x )) -> ~forall x : D, T x.
Proof.
Admitted.

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

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.
Admitted.

Theorem pred_036 : (exists x , forall y, ~R x y ) -> ~forall x, R x x.
Proof.
Admitted.

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

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.
Admitted.

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.
Admitted.

Theorem pred_059 : (forall x:D, forall y, x = y ) -> (exists x , P x ) -> forall x, P x.
Proof.
Admitted.

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.
Proof.
Admitted.

End pred_078.

End predicate_logic.