FOL.Groups

(*
    CoMoEx - Groups
    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/>.
 *)

Ziel dieses Files ist es, All- und Existenzquantoren in Kombination mit Gleichheits-Einführung und Eliminierung anhand von Gruppentheorie zu üben.
Wir benutzen hier ein paar bereits in der Standardbibliothek implementierte Funktionen:

Print xorb.
fun b1 b2 : bool => if b1 then if b2 then false else true else b2
     : bool -> bool -> bool
Wir möchten nun zeigen, dass die Menge bool, bestehend aus true und false, zusammen mit der Operation xorb eine Gruppe bildet. Dazu müssen wir sowohl Assoziativität als auch die Existenz eines neutralen Elements zeigen. Außerdem brauchen wir noch eine Inversenfunktion.

Definition is_assoc (G : Set) (f : G -> G -> G) : Prop := forall x y z, f (f x y) z = f x (f y z).

Definition is_left_id (G : Set) (f : G -> G -> G) (e : G) : Prop := forall (x : G), f e x = x.

Definition is_left_inv (G : Set) (f : G -> G -> G) (e : G) (i : G -> G) : Prop := forall (x : G), f (i x) x = e.

Bevor wir mit dem Beweis starten, bringen wir bool noch in unseren (prädikatenlogischen) Kontext:

Lemma bool_charac : forall (x : bool), x = true \/ x = false.
Proof.
  intros [].

  Restart.

  intro x.
  destruct x.
Was ist hier passiert?
Admitted.

Hier noch ein Tipp zum "Mindsetting" in dieser Aufgabe: Man sollte hier differenzieren zwischen der Menge an Termen "bool", die aus den beiden Termen "true" und "false" besteht, und First-Order-Logic, in Coq durch "Prop" dargestellt.

Theorem xor_assoc : is_assoc bool xorb.
Proof.
  unfold is_assoc.

  intro x.
  destruct (bool_charac x) as [A1|A1].
Als kleine Starthilfe.

  Undo.

  assert (H1 : x = true \/ x = false).
Ausführlichere Variante.
  {
    apply bool_charac.

    Undo.

    apply (bool_charac x).
    }
  destruct H1 as [A1|A1].
  rewrite A1.
  simpl.
simpl sorgt hier dafür, dass die Funktion xorb teilweise ausgewertet wird. Das ist möglich, da das erste Argument bekannt ist. Vgl. mit der Definition von xorb.

  Restart.

  unfold is_assoc.

Admitted.

Hier gibt es jetzt zwei kreative Stellen: 1) Finde das neutrale Element. 2) Finde die Inversen-Funktion.
Tipp: Angenommen, x ist das Inverse zu sich selbst (also zu x), dann kann man das als Funktion (fun x => x) angeben.

Theorem xor_left_id_inv_exists : exists (e : bool), is_left_id bool xorb e /\ exists (i : bool -> bool), is_left_inv bool xorb e i.
Proof.
  unfold is_left_id, is_left_inv.
Admitted.