FOL.Exists

(*
    CoMoEx - Exists
    Copyright (C) 2024  Max Ole Elliger

    This program is free software: you can redistribute it and/or modify
    it under the terms of the GNU General Public License as published by
    the Free Software Foundation, either version 3 of the License, or
    (at your option) any later version.

    This program is distributed in the hope that it will be useful,
    but WITHOUT ANY WARRANTY; without even the implied warranty of
    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
    GNU General Public License for more details.

    You should have received a copy of the GNU General Public License
    along with this program.  If not, see <https://www.gnu.org/licenses/>.
 *)

Require Import Classical_Prop.

Ziel dieses Files ist es, den Existenzquantor in Coq näher zu betrachten.

Einführung


Section existsI_demo.

  Variable T : Set.

  Section existsI_demo_1.

    Variable Q : Prop.
    Variable some_t : T.

    Hypothesis A1 : Q.

Einfachstes Beispiel: Wir wollen zeigen, dass ein x existiert, sodass Q gilt. Q ist ein konstantes Prädikatensymbol, hängt also nicht von x ab. Zudem wissen wir schon, dass Q grundsätzlich gilt. Dieses Beispiel reduziert sich also darauf, zu zeigen, dass überhaupt irgendein x aus T existiert, dass also T nicht-leer ist. Dies ist über some_t sichergestellt. (Wir nehmen das hier also einfach an, da der Fokus auf dem Existenzquantor, nicht aber auf Inhabitation liegt.

    Theorem existsI_demo_1 : exists x : T, Q.
    Proof.
      exists some_t.
      exact A1.
    Qed.

  End existsI_demo_1.

  Section existsI_demo_2.

    Variable P : T -> Prop.
    Variable some_t : T.

    Hypothesis A1 : P some_t.

Ähnliches Beispiel.

    Theorem existsI_demo_2 : exists x, P x.
    Proof.
    Admitted.

  End existsI_demo_2.

  Section existsI_demo_3.

    Variable P : T -> Prop.
    Variable x : T.

    Hypothesis A1 : P x.

Ähnliches Beispiel. Welchen Zweck könnte es haben, dass ich existsI_demo_2 UND existsI_demo_3 anführe?

    Theorem existsI_demo_3 : exists x, P x.
    Proof.
    Admitted.

  End existsI_demo_3.

End existsI_demo.

Eliminierung


Section existsE_demo.

  Variable T : Set.
  Variable Q : Prop.

  Section existsE_demo_1.

    Hypothesis A1 : exists x : T, Q.

    Theorem existsE_demo_1 : Q.
    Proof.
A1 sagt "Es gibt ein x, sodass Q gilt." Also nehme ich dieses x einfach mal als gegeben an, zudem die zugehörige Aussage. Damit arbeite ich weiter.

      destruct A1 as [x A2].
      exact A2.
    Qed.

  End existsE_demo_1.

  Section existsE_demo_2.

    Variable P : T -> Prop.

    Hypothesis A1 : exists x, Q -> P x.
    Hypothesis A2 : Q.

Hier muss man wohl nicht nur eliminieren, sondern auch einführen...

    Theorem existsE_demo_2 : exists x, P x.
    Proof.
    Admitted.

  End existsE_demo_2.

End existsE_demo.

Kombinierte Beispiele

In dieser Section kommen nun ein paar kombinierte Beispiele, die grundsätzlich nach demselben Schema ablaufen. Konkret heißt das hier, dass wir den exists-Operator mit and und or kommutieren. Dadurch kann man nochmal die grundlegenden Funktionsweisen dieser bereits bekannten Operatoren kombinieren.

Section exists_comm_ops.

  Variable T : Set.

  Variables P Q : T -> Prop.

  Section exists_comm_and_1.

    Hypothesis H1 : exists x, P x /\ Q x.

    Theorem exists_comm_and_1_1 : (exists x, P x) /\ exists x, Q x.
    Proof.
    Admitted.

  End exists_comm_and_1.

  Section exists_comm_and_2.

    Hypothesis H1 : exists x y, P x /\ Q y.

    Theorem exists_comm_and_2_1 : (exists x, P x) /\ exists x, Q x.
    Proof.
    Admitted.

  End exists_comm_and_2.

  Section exists_comm_or_1.

    Hypothesis H1 : exists x, P x \/ Q x.

    Theorem exists_comm_or_1_1 : (exists x, P x) \/ exists x, Q x.
    Proof.
    Admitted.

  End exists_comm_or_1.

  Section exists_comm_or_2.

    Hypothesis H1 : exists x y, P x \/ Q y.

    Theorem exists_comm_or_2_1 : (exists x, P x) \/ exists x, Q x.
    Proof.
    Admitted.

  End exists_comm_or_2.

End exists_comm_ops.