File CoMoEx.Groups

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 bool.
Print xorb.

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 := ∀ 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 := ∀ (x : G), f e x = x.

Definition is_left_inv (G : Set) (f : G → G → G) (e : G) (i : G → G) : Prop := ∀ (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 : ∀ (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.
  Print xorb.
  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 : ∃ (e : bool ), is_left_id bool xorb e ∧ ∃ (i : bool → bool ), is_left_inv bool xorb e i.
Proof.
unfold is_left_id, is_left_inv.
Admitted.