FOL.Forall

(*
    CoMoEx - Forall
    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 Allquantor näher kennenzulernen.

Elimination


Section forallE_demo.

  Variable T : Set.
  Variable some_t : T.

  Section forallE_demo_1.

    Variable Q : Prop.

    Hypothesis A1 : forall x : T, Q.
Aussage Q gilt also für alle x aus T.

    Theorem forallE_demo_1 : Q.
    Proof.
      exact (A1 some_t).

      Restart.

      apply A1.
Hier wird noch ein x aus T gefordert, da es in Coq wichtig ist, ob ein "Datentyp" (hier T) nicht-leer ist (inhabited).
      exact some_t.
Hiermit geben wir ein gefordertes Element an.
    Qed.

  End forallE_demo_1.

  Section forallE_demo_2.

    Variable P : T -> Prop.

    Hypothesis A1 : forall x, P x.

    Theorem forallE_demo_2 : P some_t.
Unteschied zum ersten Beispiel: jetzt werden wir nicht mehr irgendein beliebiges x aus T brauchen, sondern ein bestimmtes spezielles Element.
    Proof.
    Admitted.

  End forallE_demo_2.

End forallE_demo.

Einführung


Section forallI_demo.

  Variable T : Set.

  Section forallI_demo_1.

    Variable Q : Prop.

    Hypothesis A1 : Q.

    Theorem forallI_demo_1 : forall x : T, Q.
    Proof.
      intro t.
In typischen Mathe-Beweisen: "Sei t aus T." Wir wollen also Q für ein beliebiges, festes x zeigen. Dieses muss offensichtlich auch nicht so heißen wie die an den Allquantor gebundene Variable.
      exact A1.
    Qed.

  End forallI_demo_1.

  Section forallI_demo_2.

    Variable P : T -> Prop.

    Hypothesis A1 : forall x, P x.

    Theorem forallI_demo_2 : forall x, P x.
    Proof.
      exact A1.
Natürlich kann man dieses Goal ziemlich trivial lösen. Dies ist jedoch nicht der Sinn dieser Aufgabe.
      Restart.
Ziel ist es, hier sowohl Eliminierung als auch Einführung von Allquantoren explizit anzuwenden.

    Admitted.

  End forallI_demo_2.

End forallI_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 forall-Operator mit and, or, impl und iff kommutieren. Dadurch kann man nochmal die grundlegenden Funktionsweisen dieser bereits bekannten Operatoren kombinieren.

Section forall_comm_ops.

  Variable T : Set.

  Variables P Q : T -> Prop.

  Section forall_comm_and_1.

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

    Theorem forall_comm_and_1_1 : (forall x, P x) /\ forall x, Q x.
    Proof.
    Admitted.

  End forall_comm_and_1.

  Section forall_comm_and_2.

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

    Theorem forall_comm_and_2_1 : (forall x, P x) /\ forall x, Q x.
    Proof.
    Admitted.

  End forall_comm_and_2.

  Section forall_comm_or_1.

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

    Theorem forall_comm_or_1_1 : (forall x, P x) \/ forall x, Q x.
    Proof.
    Admitted.

  End forall_comm_or_1.

  Section forall_comm_or_2.

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

    Theorem forall_comm_or_2_1 : (forall x, P x) \/ forall x, Q x.
    Proof.
    Admitted.

  End forall_comm_or_2.

  Section forall_comm_impl_1.

    Hypothesis H1 : forall x, P x -> Q x.

    Theorem forall_comm_impl_1_1 : (forall x, P x) -> forall x, Q x.
    Proof.
    Admitted.

  End forall_comm_impl_1.

  Section forall_comm_impl_2.

    Hypothesis H1 : forall x y, P x -> Q y.

    Theorem forall_comm_impl_2_1 : (forall x, P x) -> forall x, Q x.
    Proof.
    Admitted.

  End forall_comm_impl_2.

  Section forall_comm_iff_1.

    Hypothesis H1 : forall x, P x <-> Q x.

    Theorem forall_comm_iff_1_1 : (forall x, P x) <-> forall x, Q x.
    Proof.
    Admitted.

  End forall_comm_iff_1.

  Section forall_comm_iff_2.

    Hypothesis H1 : forall x y, P x <-> Q y.

    Theorem forall_comm_iff_2_1 : (forall x, P x) <-> forall x, Q x.
    Proof.
    Admitted.

  End forall_comm_iff_2.

End forall_comm_ops.

Section forall_ex_1.

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

  Hypothesis A1 : exists x, forall y, P x y.

  Theorem forall_ex_1_1 : forall y, exists x, P x y.
  Proof.
  Admitted.

End forall_ex_1.

Section forall_ex_2.

  Variable T : Set.
  Variables P Q : T -> Prop.
  Variable R : T -> T -> Prop.

  Hypothesis A1 : forall x, exists y, R x y /\ P y.
  Hypothesis A2 : forall x, P x -> Q x.

  Theorem forall_ex_2_1 : forall x, exists y, R x y /\ Q y.
  Proof.
  Admitted.

End forall_ex_2.

Section forall_ex_3.

  Variable T : Set.
  Variables P Q : T -> Prop.
  Variable R : T -> T -> Prop.

  Hypothesis A1 : forall x y z, (R x y /\ R x z) -> R y z.
  Hypothesis A2 : forall x, R x x.
  Hypothesis A3 : forall x, exists y, R x y /\ P y.

  Theorem forall_ex_3_1 : forall x, exists y, R y x /\ P y.
  Proof.
  Admitted.

End forall_ex_3.

Section forall_ex_4.

  Variable T : Set.
  Variable P : T -> Prop.
  Variables R S : T -> T -> Prop.

  Hypothesis A1 : forall x y, S x y -> P y.
  Hypothesis A2 : forall x y, R x y -> exists z, S z y.

  Theorem forall_ex_4_1 : forall x y, R x y -> P y.
  Proof.
  Admitted.

End forall_ex_4.

Section forall_ex_5.

  Variable T : Set.
  Variable R : T -> T -> Prop.

  Hypothesis A1 : forall x, exists y, R x y.
  Hypothesis A2 : forall x y z, (R x y /\ R y z) -> R x z.
  Hypothesis A3 : forall x y, R x y -> R y x.

  Theorem forall_ex_5_1 : forall x, R x x.
  Proof.
  Admitted.

End forall_ex_5.

Section forall_ex_6.

  Variable T : Set.
  Variable z : T.
  Variable P : T -> Prop.
  Variable R : T -> T -> Prop.

  Hypothesis A1 : forall x, exists y, R x y.
  Hypothesis A2 : forall y, R z y -> ~ P y.

  Theorem forall_ex_6_1 : ~ forall y, R z y -> P y.
  Proof.
  Admitted.

End forall_ex_6.

Section forall_ex_7.

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

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

End forall_ex_7.