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

Merge branch 'docs/headlines' into 'main' 

Docs/headlines

See merge request !36
parents d49e387c 3c9713d7
No related branches found
No related tags found
1 merge request!36Docs/headlines
Pipeline #134354 passed
Stage: build
Show whitespace changes
Inline Side-by-side
fol/Exists.v
+ 35
− 4
View file @ eb4d2881
......@@ -2,6 +2,8 @@ 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.
......@@ -13,7 +15,16 @@ Section existsI_demo.
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. *)
(** 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.
......@@ -30,6 +41,7 @@ Section existsI_demo.
Hypothesis A1 : P some_t.
(** Ähnliches Beispiel. *)
Theorem existsI_demo_2 : exists x, P x.
Proof.
Admitted.
......@@ -43,7 +55,10 @@ Section existsI_demo.
Hypothesis A1 : P x.
(** Ähnliches Beispiel. Welchen Zweck könnte es haben, dass ich Bsp. 2 UND 3 anführe? *)
(** Ä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.
......@@ -52,6 +67,8 @@ Section existsI_demo.
End existsI_demo.
(** * Eliminierung *)
Section existsE_demo.
Variable T : Set.
......@@ -63,7 +80,12 @@ Section existsE_demo.
Theorem existsE_demo_1 : Q.
Proof.
destruct A1 as [x A2]. (** 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. *)
(** 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.
......@@ -77,6 +99,7 @@ Section existsE_demo.
Hypothesis A2 : Q.
(** Hier muss man wohl nicht nur eliminieren, sondern auch einführen... *)
Theorem existsE_demo_2 : exists x, P x.
Proof.
Admitted.
......@@ -85,7 +108,15 @@ Section existsE_demo.
End existsE_demo.
(** 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. *)
(** * 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.
......
fol/Forall.v
+ 17
− 5
View file @ eb4d2881
......@@ -2,6 +2,8 @@ Require Import Classical_Prop.
(** Ziel dieses Files ist es, den Allquantor näher kennenzulernen. *)
(** * Elimination *)
Section forallE_demo.
Variable T : Set.
......@@ -11,7 +13,7 @@ Section forallE_demo.
Variable Q : Prop.
Hypothesis A1 : forall x : T, Q. (** Aussage Q gilt also für alle x aus T. *)
Hypothesis A1 : forall x : T, Q. (** Aussage [Q] gilt also für alle [x] aus [T]. *)
Theorem forallE_demo_1 : Q.
Proof.
......@@ -19,7 +21,7 @@ Section forallE_demo.
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). *)
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.
......@@ -31,7 +33,7 @@ Section forallE_demo.
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. *)
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.
......@@ -39,6 +41,8 @@ Section forallE_demo.
End forallE_demo.
(** * Einführung *)
Section forallI_demo.
Variable T : Set.
......@@ -51,7 +55,7 @@ Section forallI_demo.
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. *)
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.
......@@ -75,7 +79,15 @@ Section forallI_demo.
End forallI_demo.
(** 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. *)
(** * 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.
......
fol/Groups.v
+ 27
− 8
View file @ eb4d2881
......@@ -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.
......
prop/IntroElim.v
+ 137
− 16
View file @ eb4d2881
Require Import Classical_Prop.
Require Classical_Prop.
(** In diesem File geht es um die Nachbildung der üblichen Fitch-Regeln. Die Beispiele führen also die Einführungs- (Introduction-) und Eliminationsregeln (Elimination) an den einfachsten Beispielen vor. Insbesondere sind die entsprechenden Theoreme nicht dazu gedacht, in den anderen Files verwendet zu werden. *)
(**
In diesem File geht es um die Nachbildung der üblichen Fitch-Regeln.
Die Beispiele führen also die Einführungs- (Introduction-)
und Eliminationsregeln (Elimination) an den einfachsten Beispielen vor.
Insbesondere sind die entsprechenden Theoreme nicht dazu gedacht,
in den anderen Files verwendet zu werden.
*)
(** * Falsum *)
(** ** Einführung *)
Section bot_1.
Variables p : Prop.
(** Falsum führt man üblicherweise dadurch ein, dass widersprüchliche Informationen vorhanden sind: Eine Aussage p kommt also negiert und nicht negiert in den Annahmen von. *)
(**
Falsum führt man üblicherweise dadurch ein,
dass widersprüchliche Informationen vorhanden sind:
Eine Aussage [p] kommt also negiert und nicht negiert
in den Annahmen vor.
*)
Hypothesis A1 : p.
Hypothesis A2 : ~p.
......@@ -17,11 +31,16 @@ Section bot_1.
End bot_1.
(** ** Eliminierung *)
Section bot_2.
Variables p : Prop.
(** Hingegen kann man aus etwas Falschen Beliebiges herleiten. *)
(**
Hingegen kann man aus etwas Falschen Beliebiges herleiten.
*)
Hypothesis A1 : False.
Theorem bot_E : p.
......@@ -30,11 +49,25 @@ Section bot_2.
End bot_2.
(** * Negation *)
(** ** Einführung *)
Section neg_1.
Variables p : Prop.
(** Die Negations-Einführung ist trivial, wenn man die Codierung von "~" mit `unfold ~ _.` aufdeckt. Wie geht man etwas kleinschrittiger vor? *)
(**
Die Negations-Einführung ist trivial,
wenn man die Codierung von [~] aufdeckt: *)
Print "~ _".
(**
Dies geht übrigens in einem Beweis auch direkt mittels
[unfold "~ _".].
Wie geht man etwas kleinschrittiger vor?
*)
Hypothesis A1 : p -> False.
Theorem neg_I : ~p.
......@@ -43,11 +76,34 @@ Section neg_1.
End neg_1.
(** ** Eliminierung *)
Section neg_2.
Variables p : Prop.
(** Die Negations-Eliminierungsregel mussten wir erst mittels `Require Import Classical_Prop.` importieren. Dadurch können wir axiomatisch `NNPP` annehmen. Was ist NNPP? -> Siehe `Check NNPP.`. *)
(**
Für die Negations-Eliminierungsregel benötigen wir klassische Logik: *)
Import Classical_Prop.
(**
In späteren Files werden wir häufig direkt zu Beginn
[Require Import Classical_Prop.] schreiben.
Dadurch können wir axiomatisch [NNPP] annehmen: *)
Check NNPP.
(**
Durch den folgenden Befehl können wir sogar die Notwendigkeit von
klassischer Logik sichtbar machen! *)
Print Assumptions NNPP.
(**
Der Beweis unserer Negations-Elimierungsregel ist jetzt nur noch
eine Anwendung von [NNPP]. *)
Hypothesis A1 : ~ ~ p.
Theorem neg_E : p.
......@@ -56,11 +112,19 @@ Section neg_2.
End neg_2.
(** * Konjunktion *)
(** ** Einführung *)
Section and_1.
Variables p q : Prop.
(** Um eine Konjunktion zu zeigen, muss man sowohl ihre linke als auch rechte Seite zeigen. Wie bekommt man aus einem Goal zwei Goals? *)
(**
Um eine Konjunktion zu zeigen,
muss man sowohl ihre linke als auch
rechte Seite zeigen.
Wie bekommt man aus einem Goal zwei Goals? *)
Hypothesis A1 : p.
Hypothesis A2 : q.
......@@ -70,28 +134,42 @@ Section and_1.
End and_1.
(** ** Eliminierung *)
Section and_2.
Variables p q : Prop.
(** Wenn p und q gelten, gelten sowohl p als auch q. *)
(**
Wenn [p] und [q] gelten, gelten sowohl [p] als auch [q]. *)
Hypothesis A1 : p /\ q.
(** *** Linke Seite *)
Theorem and_E1 : p.
Proof.
Admitted.
(** *** Rechte Seite *)
Theorem and_E2 : q.
Proof.
Admitted.
End and_2.
(** * Disjunktion *)
(** ** Einführung *)
(** *** Linke Seite *)
Section or_1.
Variables p q : Prop.
(** Wenn p gilt, gilt ja p oder q.*)
(**
Wenn [p] gilt, gilt ja [p] oder [q]. *)
Hypothesis A1 : p.
Theorem or_I1 : p \/ q.
......@@ -100,11 +178,14 @@ Section or_1.
End or_1.
(** *** Rechte Seite *)
Section or_2.
Variables p q : Prop.
(** Wenn q gilt, gilt ja p oder q. *)
(**
Wenn [q] gilt, gilt ja [p] oder [q]. *)
Hypothesis A1 : q.
Theorem or_I2 : p \/ q.
......@@ -113,11 +194,19 @@ Section or_2.
End or_2.
(** ** Eliminierung *)
Section or_3.
Variables p q r : Prop.
(** Ok, wir wollen r zeigen und wissen, dass zumindest p oder q gelten. Wenn wir jetzt also sowohl aus p als auch aus q unser Ziel r herleiten können, können wir auch aus "p oder q" r herleiten. *)
(**
Ok, wir wollen [r] zeigen und wissen,
dass zumindest [p] oder [q] gilt.
Wenn wir jetzt also sowohl aus [p] als auch aus [q]
unser Ziel [r] herleiten können,
können wir auch aus [p \/ q] [r] herleiten. *)
Hypothesis A1 : p -> r.
Hypothesis A2 : q -> r.
Hypothesis A3 : p \/ q.
......@@ -128,11 +217,21 @@ Section or_3.
End or_3.
(** * Implikation *)
(** ** Einführung *)
Section impl_1.
Variables p q : Prop.
(** Ich schätze, dass dies die Stelle in dem File ist, die am meisten trivial wirkt. Ich finde aber, dass dieses Theorem nochmal den Fokus darauf lenkt, dass in Coq kein großer Unterschied zwischen einer Herleitung und einer Implikation vorhanden ist. *)
(**
Ich schätze, dass dies die Stelle in dem File ist,
die am meisten trivial wirkt.
Ich finde aber,
dass dieses Theorem nochmal den Fokus darauf lenkt,
dass in Coq kein großer Unterschied zwischen einer Herleitung
und einer Implikation vorhanden ist. *)
Hypothesis A1 : p -> q.
Theorem impl_I : p -> q.
......@@ -141,11 +240,16 @@ Section impl_1.
End impl_1.
(** ** Eliminierung *)
Section impl_2.
Variables p q : Prop.
(** Ein bisschen Wissen für Zwischendurch: Dieser Schluss nennt sich "Modus Ponens". *)
(**
Ein bisschen Wissen für Zwischendurch:
Dieser Schluss nennt sich "Modus Ponens". *)
Hypothesis A1 : p -> q.
Hypothesis A2 : p.
......@@ -155,11 +259,19 @@ Section impl_2.
End impl_2.
(** * Biimplikation *)
(** ** Einführung *)
Section iff_1.
Variables p q : Prop.
(** Um eine Äquivalenz zu beweisen, braucht man meistens zwei Beweise. *)
(**
Um eine Äquivalenz zu beweisen, braucht man meistens zwei Beweise.
Hierzu ein kleiner Tipp: *)
Print "<->".
Hypothesis A1 : p -> q.
Hypothesis A2 : q -> p.
......@@ -169,11 +281,16 @@ Section iff_1.
End iff_1.
(** ** Eliminierung *)
(** *** Von Links nach Rechts *)
Section iff_2.
Variables p q : Prop.
(** Wird schon! *)
(**
Wird schon! *)
Hypothesis A1 : p <-> q.
Hypothesis A2 : p.
......@@ -183,11 +300,15 @@ Section iff_2.
End iff_2.
(** *** Von Rechts nach Links *)
Section iff_3.
Variables p q : Prop.
(** Wird schon! *)
(**
Wird schon! *)
Hypothesis A1 : p <-> q.
Hypothesis A2 : q.
......
prop/Laws.v
+ 53
− 1
View file @ eb4d2881
(** In diesem File soll es um übliche und (teilweise) bekannte klassische logische Gesetze gehen. Eine weitere Annotierung bleibt hier aktuell aus, da die Gesetze ja eh schon ausgeschrieben sind.*)
Require Import Classical_Prop.
(** In diesem File soll es um übliche und (teilweise) bekannte klassische logische Gesetze gehen. Eine weitere Annotierung bleibt hier aktuell aus, da die Gesetze ja eh schon ausgeschrieben sind.*)
(** * Triviale Biimplikationen *)
Section trivial_iff.
......@@ -16,33 +18,47 @@ Section trivial_iff.
End trivial_iff.
(** * Kommutativität *)
Section comm.
Variables p q : Prop.
(** ** Konjunktion *)
Theorem and_comm : (p /\ q) -> (q /\ p).
Proof.
Admitted.
(** ** Disjunktion *)
Theorem or_comm : (p \/ q) -> (q \/ p).
Proof.
Admitted.
End comm.
(** * Assoziativität *)
Section assoc.
Variables p q r : Prop.
(** ** Konjunktion *)
Theorem and_assoc : ((p /\ q) /\ r) <-> (p /\ (q /\ r)).
Proof.
Admitted.
(** ** Disjunktion *)
Theorem or_assoc : ((p \/ q) \/ r) <-> (p \/ (q \/ r)).
Proof.
Admitted.
End assoc.
(** * Gesetze von De Morgan *)
Section de_morgan.
Variables p q : Prop.
......@@ -57,20 +73,28 @@ Section de_morgan.
End de_morgan.
(** * Weitere Implementierungen von Implikationen *)
Section implsem.
Variables p q : Prop.
(** ** Konjunktion *)
Theorem impl_with_disj : (p -> q) <-> (~p \/ q).
Proof.
Admitted.
(** ** Disjunktion *)
Theorem impl_with_conj : (p -> q) <-> ~(p /\ ~q).
Proof.
Admitted.
End implsem.
(** * Distributivität von Konjunktion und Disjunktion *)
Section distr.
Variables p q r : Prop.
......@@ -85,6 +109,8 @@ Section distr.
End distr.
(** * Typische klassische Gesetze *)
Section p_not_p.
Variables p : Prop.
......@@ -99,48 +125,68 @@ Section p_not_p.
End p_not_p.
(** * Idempotenz *)
Section idem.
Variables p : Prop.
(** ** Konjunktion *)
Theorem idem_and : p /\ p <-> p.
Proof.
Admitted.
(** ** Disjunktion *)
Theorem idem_or : p \/ p <-> p.
Proof.
Admitted.
End idem.
(** * Absorbtion *)
Section absorb.
Variables p q : Prop.
(** ** Konjunktion *)
Theorem absorb_and : p /\ (p \/ q) <-> p.
Proof.
Admitted.
(** ** Disjunktion *)
Theorem absorb_or : p \/ (p /\ q) <-> p.
Proof.
Admitted.
End absorb.
(** * Neutrale Elemente *)
Section neutr.
Variables p : Prop.
(** ** Konjunktion *)
Theorem neutr_and : p /\ True <-> p.
Proof.
Admitted.
(** ** Disjunktion *)
Theorem neutr_or : p \/ False <-> p.
Proof.
Admitted.
End neutr.
(** * Kontraposition & Modus Tollens *)
Section contrapos.
Variables p q : Prop.
......@@ -155,6 +201,8 @@ Section contrapos.
End contrapos.
(** * Transitivität der Implikation *)
Section impl_trans.
Variables p q r : Prop.
......@@ -168,6 +216,8 @@ Section impl_trans.
End impl_trans.
(** * Currying *)
Section currying.
Variables p q r : Prop.
......@@ -178,6 +228,8 @@ Section currying.
End currying.
(** * Gesetz von Peirce *)
Section peirce_law.
Variables p q : Prop.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment