Skip to content
Snippets Groups Projects
Commit 3c9713d7 authored by Max Ole Elliger's avatar Max Ole Elliger :penguin:
Browse files

docs groups

parent 84eddeed
No related branches found
No related tags found
1 merge request!36Docs/headlines
Pipeline #128005 passed
......@@ -3,10 +3,20 @@
(** Wir benutzen hier ein paar bereits in der Standardbibliothek implementierte Funktionen: *)
Print bool.
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. *)
(** 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).
......@@ -14,7 +24,10 @@ Definition is_left_id (G : Set) (f : G -> G -> G) (e : G) : Prop := forall (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: *)
(** 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.
......@@ -26,7 +39,10 @@ Proof.
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. *)
(** 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.
......@@ -46,8 +62,7 @@ Proof.
}
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. *)
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.
......@@ -57,8 +72,12 @@ 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.
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.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment