add tmp stuff

Game/Levels/Tmp.lean

@@ -0,0 +1,10 @@
+import Game.Levels.Tmp.NullstellenSatz
+import Game.Levels.Tmp.NullstellenSatz_Example
+
+World "Tmp"
+Title "Tmp"
+
+Introduction "
+Diese Welt enthält WIP Aufgaben,
+die noch nicht einer Welt zugeordnet sind.
+"

Game/Levels/Tmp/LA1_exercises/.gitignore

@@ -0,0 +1,2 @@
+**.olean
+**.olean.lock

Game/Levels/Tmp/LA1_exercises/README.md

@@ -0,0 +1 @@
+Aufgaben LA: http://reh.math.uni-duesseldorf.de/~zibrowius/TeachingRepo/Lineare%20Algebra%20(2021-22)/Aufgaben-I/

Game/Levels/Tmp/LA1_exercises/game_config.toml

@@ -0,0 +1,167 @@
+name = "Lineare Algebra"
+version = "0.0.2"
+extra_files = "extras"
+intro = "src/intro.lean"
+
+[[worlds]]
+name = "Einführung & Logik"
+id = 1
+parents = []
+levels = [
+	"src/basics/equality/equality_001.lean",
+	"src/basics/equality/equality_002.lean",
+	"src/basics/logic/logic_001.lean",
+	"src/basics/logic/logic_002.lean",
+	"src/basics/logic/logic_003.lean",
+	"src/basics/logic/logic_004.lean",
+	"src/basics/logic/logic_005.lean",
+	"src/basics/logic/logic_006.lean",
+	"src/basics/logic/quantors_001.lean",
+	"src/basics/logic/quantors_002.lean",
+]
+
+[[worlds]]
+name = "Natürliche Zahlen"
+id = 2
+parents = [1]
+levels = [
+	"src/basics/numbers/nat_001.lean",
+	"src/basics/numbers/nat_002.lean",
+	"src/basics/numbers/nat_003.lean",
+	"src/basics/numbers/nat_004.lean",
+	"src/basics/numbers/nat_005.lean",
+	"src/basics/numbers/nat_006.lean",
+	"src/basics/numbers/nat_007.lean",
+	"src/basics/numbers/nat_008.lean",
+	"src/basics/numbers/nat_009.lean",
+]
+
+[[worlds]]
+name = "Mehr Zahlen"
+id = 3
+parents = [2]
+levels = [
+	"src/basics/numbers/pnat_001.lean",
+	"src/basics/numbers/pnat_002.lean",
+	"src/basics/numbers/integer.lean",
+	"src/basics/numbers/rational.lean",
+	"src/basics/numbers/real.lean",
+	"src/basics/numbers/complex.lean",
+]
+
+[[worlds]]
+name = "Mengenlehre"
+id = 4
+parents = []
+levels = [
+	"src/basics/union_sup.lean",
+	"src/basics/power_set_fin.lean",
+]
+
+[[worlds]]
+name = "Vektorräume/Moduln"
+id = 5
+parents = [2]
+levels = [
+	"src/vectorspace/definition/def_01.lean",
+	"src/vectorspace/definition/def_02.lean",
+	"src/vectorspace/definition/def_03.lean",
+	"src/vectorspace/definition/def_04.lean",
+	"src/vectorspace/definition/def_05.lean",
+	"src/vectorspace/definition/def_06.lean",
+]
+
+[[worlds]]
+name = "Vektornotation"
+id = 6
+parents = [5]
+levels = [
+	"src/vectorspace/definition/vector_notation.lean",
+	"src/vectorspace/definition/vector_notation_b.lean",
+]
+
+[[worlds]]
+name = "Untervektorräume"
+id = 7
+parents = [6]
+levels = [
+	"src/vectorspace/submodule/definition.lean",
+	"src/vectorspace/submodule/definition_b.lean",
+	"src/vectorspace/submodule/generating_set.lean",
+]
+
+[[worlds]]
+name = "Lineare Abbildungen"
+id = 8
+parents = [6]
+levels = [
+	"src/vectorspace/linear_map/linear_map.lean",
+	"src/vectorspace/linear_map/linear_map_b.lean",
+]
+
+[[worlds]]
+name = "Basis"
+id = 9
+parents = [7]
+levels = [
+	"src/vectorspace/basis/lin_indep.lean",
+	"src/vectorspace/basis/basis.lean",
+	"src/vectorspace/basis/basis_2.lean",
+]
+
+[[worlds]]
+name = "Untervektorräume 2"
+id = 10
+parents = [7, 8]
+levels = [
+	 "src/vectorspace/submodule/span_1.lean",
+	 "src/vectorspace/submodule/span_2.lean",
+	 "src/vectorspace/submodule/idempotent_fun_1.lean",
+	 "src/vectorspace/submodule/idempotent_fun_2.lean",
+]
+
+[[worlds]]
+name = "Summe/Produkt"
+id = 11
+parents = [10]
+levels = [
+	"src/vectorspace/submodule/sum_prod_1.lean",
+	"src/vectorspace/submodule/sum_prod_2.lean",
+	"src/vectorspace/submodule/sum_prod_3.lean",
+	"src/vectorspace/submodule/sum_prod_4.lean",
+	"src/vectorspace/submodule/sum_prod_5.lean",
+]
+
+
+[[worlds]]
+name = "Matrizen"
+id = 12
+parents = [8]
+levels = [
+	"src/dummy.lean",
+]
+
+[[worlds]]
+name = "Weiteres"
+id = 13
+parents = [9]
+levels = [
+	"src/vectorspace/basis/real_uncountable.lean",
+	"src/vectorspace/basis/card_fin_field.lean",
+]
+
+[[worlds]]
+name = "Rang und Dimension"
+id = 14
+parents = [9]
+levels = [
+	"src/dummy.lean",
+]
+
+[[worlds]]
+name = "Ergänzungs- und Hauptsatz"
+id = 15
+parents = [14]
+levels = [
+	"src/dummy.lean",
+]

Game/Levels/Tmp/LA1_exercises/leanpkg.path

@@ -0,0 +1,3 @@
+builtin_path
+path _target/deps/mathlib/src
+path ./src

Game/Levels/Tmp/LA1_exercises/leanpkg.toml

@@ -0,0 +1,8 @@
+[package]
+name = "LA_game"
+version = "0.1"
+lean_version = "leanprover-community/lean:3.50.3"
+path = "src"
+
+[dependencies]
+mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "996b0ff959da753a555053a480f36e5f264d4207"}

Game/Levels/Tmp/LA1_exercises/src/OLD/basics/001_refl.lean

@@ -0,0 +1,31 @@
+-- Level name : Aller Anfang ist... ein Einzeiler?
+
+/-
+Willkommen zum Lean-Crashkurs wo du lernst wie man mathematische Beweise vom Computer
+unterstützt und verifiziert schreiben kann.
+
+Ein Beweis besteht in Lean aus verschiedenen **Taktiken**, welche ungefähr einem
+logischen Schritt entsprechen, den man auf Papier aufschreiben würde.
+
+Rechts im **Infoview** siehst den Status des aktuellen Beweis.
+Du siehst ein oder mehrere offene **Goals** (mit einem `⊢` davor), die du noch zeigen musst.
+Wenn du eine Taktik hinschreibst (Lean 3 : Komma am Ende), dann versucht Lean diesen Schritt beim
+ersten offenen Goal zu machen.
+Wenn der Beweis komplett ist, erscheint "goals accomplished".
+
+Die erste Taktik ist `refl`, die ein Goal von der Form `A = A` beweist.
+-/
+
+/- Lemma : no-side-bar
+In den natürlichen Zahlen gilt `42 = 42`.
+-/
+example : 42 = 42 :=
+begin
+  refl,
+end
+
+/- Tactic : refl
+Schliesst ein Goal von der Form `A = A`.
+(Hängt davon ab, dass die beiden Seiten in Lean intern gleich definiert sind, auch
+wenn diese anders dargestellt werden. z.B. sind `1 + 1` und `2` per Definition gleich in Lean.)
+-/

Game/Levels/Tmp/LA1_exercises/src/OLD/basics/002_refl.lean

@@ -0,0 +1,22 @@
+-- Level name : Definitionally equal
+
+/-
+Achtung: `refl` kann auch Gleichungen beweisen, wenn die beiden Terme Lean-intern gleich definiert sind,
+auch wenn diese unterschiedlich dargestellt werden.
+so sind `1 + 1` und `2` per Definition das Gleiche, da sie beide von Lean als `0.succ.succ` gelesen werden.
+
+Das kann anfänglich verwirrend sein und das Verhalten hängt von der Lean-Implementation ab. 
+-/
+
+/- Lemma : no-side-bar
+Beweise
+-/
+example : 1 + 1 = 2 :=
+begin
+  refl,
+end
+
+/-
+Im weiteren führen die meisten anderen Taktiken `refl` automatisch am Ende aus,
+deshalb musst du dieses häufig gar nicht mehr schreiben.
+-/

Game/Levels/Tmp/LA1_exercises/src/OLD/basics/003_assumption.lean

@@ -0,0 +1,66 @@
+-- Level name : Annahmen
+
+/-
+Um Aussagen zu formulieren braucht man Annahmen. Zum einen sind das Objekte, von denen eine Aussage handelt,
+wie zum Beispiel "sei `n` eine natürliche Zahl", oder "seien `A`, `B` logische Aussagen", zum anderen
+sind dass Annahmen wie "angenommen dass `n` nicht Null ist" oder "angenommen `A` ist wahr".
+
+In Lean schreibt man beides mit der gleichen Notation: `(n : ℕ)` ist eine natürliche Zahl, 
+`(A B : Prop)` sind Aussagen, `(h : n ≠ 0)` ist eine Annahme, dass `n` nicht Null ist, und
+`(hA : A)` ist die Annahme, dass `A` wahr ist (`hA` ist ein Beweis von `A`).
+
+Die Annahmen kommen dann vor den Doppelpunkt oder vor dem Lemma also `variables (n : ℕ)`.
+Beide Schreibweisen sind äquivalent, der Unterschied ist nur, dass eine Annahme in einer
+`variables`-Zeile dann für alle folgenden Lemmas zur Verfügung steht.
+
+```
+/-- Sei n eine natürliche Zahl ungleich Null. Dann ist n strickt grösser als Null. -/
+example (n : ℕ) (hn: n ≠ 0) : 0 < n :=
+begin
+  sorry
+end
+
+/-- Seien A und B logische Aussagen und A sei wahr. Dann ist "A oder B" wahr. -/
+example (A B : Prop) (hA: A) : A ∨ B :=
+begin
+  sorry
+end
+```
+
+Wenn eine Annahme `h` genau dem Goal entspricht, kannst du `exact h` verwenden.
+-/
+
+variables (n : ℕ)
+
+/- Lemma : no-side-bar
+Wenn `n = 0` dann ist `n = 0`.
+-/
+example (h : n = 0) : n = 0 :=
+begin
+  exact h,
+end
+
+/-
+Alternativ kannst du `assumption` brauchen, welches automatisch nach der richtigen
+Annahme sucht.
+-/
+
+/- Lemma : no-side-bar
+Wenn `n = 0` dann ist `n = 0`.
+-/
+example (h : n ≠ 0) : n ≠ 0 :=
+begin
+  assumption,
+end
+
+/- Tactic : exact
+`exact h` schliesst den Beweis wenn `h` und das Goal exact übereinstimmen.
+`assumption` funktioniert gleich, sucht aber selbständig, welche Annahme mit dem Goal
+übereinstimmt.
+-/
+
+/- Tactic : assumption
+`assumption` sucht in den Annahmen nach einer, die mit dem Goal übereinstimmt, und schliesst den Beweis.
+-/
+
+/- Typen : `Prop`, `ℕ` -/

Game/Levels/Tmp/LA1_exercises/src/OLD/basics/004_rewrite.lean

@@ -0,0 +1,40 @@
+-- Level name : Rewrite
+
+/-
+Oft sind aber die Annahmen nicht genau das, was man zeigen will, sondern helfen einem
+nur, dorthin zu kommen.
+
+Wenn man eine Annahme `(h : a = b)` hat, kann man mit `rw [h]` (oder `rewrite [h]`) das erste
+`a` im Goal mit `b` ersetzen.
+Mit `rw [←h]` (`←` tippt man mit `\l`) ersetzt man in der Gegenrichtung `b` mit `a`.
+
+(PS: die kleinen Zahlen `h₁ h₂ h₃` werden in Lean oft verwendet und man schreibt diese mit
+`\1`, `\2`, `\3`, …)
+-/
+
+/- Lemma : no-side-bar
+Angenommen man hat `a = b`, `c = d` und `a = d`, zeige dass `b = c`.
+-/
+example (a b c d : ℕ) (h₁ : a = b) (h₂ : c = d) (h₃ : a = d) : b = c :=
+begin
+  rw [h₂, ←h₁],
+  exact h₃,
+end
+
+/-
+Man kann übrigens auch mit `rw` in einer anderen Annahme umschreiben:
+Probier mal `rw h₁ at h₃` als erstes. Danach hast du `(h₃ : b = d)` als Annahme.
+
+Im weiteren kann man mit `rw [h, h, g, f]` mehrere rewrites auf einmal machen.
+-/
+
+
+
+
+/- Tactic : rw/rewrite
+Gegeben eine Annahme `(h : X = Y)`, `rw [h]` ersetzt `X` im Goal mit `Y`.
+`rw [←h]` ersetzt in der anderen Richtung.
+
+`rw [h] at g` wendet die Taktik auf eine Annahme `g` an anstatt auf das aktuelle Goal.
+-/
+