Section predicate_logic. 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 applies a "unification algorithm": The "P x" in "H : forall x : D, P x" is unified with the goal "P y", which means that and instantiation for the universally quatified 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. 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. (* Exercise 31 *) (* 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. (* Exercise 36 *) 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 "exists" and the "disjunctions" 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 exist 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. (* This 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. 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. (*! pred_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]]. (* x5 = Successor x2 *) (* 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]. (* x6 = Successor x3 *) 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.