(** * 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 #<br># 
       [exists x : D, ~ P x] #<br># 
    by a fresh variable [y : D] and a hypothesis [H : ~ P y] #<br># 
    also try 
       [elim H] and then [intros] and compare. #<br># 
   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 #<br>#
      [rewrite <- H2] #<br>#
    and see what happens.
    Also try#<br>#
      [rewrite <- H2 in H1] #<br>#
    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 #<br>#
    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.