factor out adam game
Jon Eugster
2 years ago
parent
f9614b3bcd
commit
2097eddb2f
@ -1 +0,0 @@
|
||||
build
|
||||
@ -1,10 +0,0 @@
|
||||
{
|
||||
"editor.insertSpaces": true,
|
||||
"editor.tabSize": 2,
|
||||
"editor.rulers" : [100],
|
||||
"files.encoding": "utf8",
|
||||
"files.eol": "\n",
|
||||
"files.insertFinalNewline": true,
|
||||
"files.trimFinalNewlines": true,
|
||||
"files.trimTrailingWhitespace": true
|
||||
}
|
||||
@ -1,76 +0,0 @@
|
||||
import Adam.Metadata
|
||||
|
||||
import Adam.Levels.Proposition
|
||||
import Adam.Levels.Implication
|
||||
import Adam.Levels.Predicate
|
||||
import Adam.Levels.Contradiction
|
||||
-- import Adam.Levels.Prime
|
||||
import Adam.Levels.Sum
|
||||
-- import Adam.Levels.Induction
|
||||
|
||||
--import Adam.Levels.Numbers
|
||||
import Adam.Levels.Inequality
|
||||
|
||||
import Adam.Levels.Lean
|
||||
import Adam.Levels.SetTheory
|
||||
import Adam.Levels.Function
|
||||
--import Adam.Levels.SetFunction
|
||||
--import Adam.Levels.LinearAlgebra
|
||||
|
||||
|
||||
|
||||
Game "Adam"
|
||||
Title "Lean 4 game"
|
||||
Introduction
|
||||
"
|
||||
# Game Over oder QED?
|
||||
|
||||
Willkommen zu unserem Prototyp eines Lean4-Lernspiels. Hier lernst du computer-gestützte
|
||||
Beweisführung. Das Interface ist etwas vereinfacht, aber wenn du den *Editor Mode* aktivierst, fühlt es sich
|
||||
fast genauso an wie in VSCode, der Standard-IDE für Lean.
|
||||
|
||||
Rechts siehst du eine Übersicht. Das Spiel besteht aus mehreren Planeten, und jeder Planet hat mehrere Levels,
|
||||
die in Form von grauen Punkten dargestellt sind. Gelöste Levels werden grün.
|
||||
|
||||
Klicke auf den ersten Planeten *Logo*, um deine Reise zu starten.
|
||||
|
||||
### Spielstand
|
||||
|
||||
Dein Spielstand wird lokal in deinem Browser als *site data* gespeichert.
|
||||
Solltest du diese löschen, verlierst du deinen Spielstand!
|
||||
Viele Browser löschen *site data* und *cookies* zusammen.
|
||||
Du kannst aber jederzeit jedes Level spielen, auch wenn du vorhergende Levels noch nicht gelöst hast.
|
||||
|
||||
### Funding
|
||||
|
||||
Dieses Lernspiel wurde und wird im Rahmen des Projekts
|
||||
[ADAM: Anticipating the Digital Age of Mathematics](https://hhu-adam.github.io/)
|
||||
an der Heinrich-Heine-Universität Düsseldorf entwickelt.
|
||||
Es wird finanziert durch das Programm *Freiraum 2022* der *Stiftung Innovation in der Hochschullehre*.
|
||||
|
||||
### Kontakt
|
||||
|
||||
Das Spiel befindet sich noch in der Entwicklung.
|
||||
Wenn du Anregungen hast oder Bugs findest, schreib doch ein Email oder erstelle einen
|
||||
[Issue auf Github](https://github.com/leanprover-community/lean4game/issues).
|
||||
|
||||
[Jon Eugster](https://www.math.hhu.de/lehrstuehle-/-personen-/-ansprechpartner/innen/lehrstuehle-des-mathematischen-instituts/lehrstuhl-fuer-algebraische-geometrie/team/jon-eugster)
|
||||
"
|
||||
|
||||
Conclusion
|
||||
"Fertig!"
|
||||
|
||||
|
||||
Path Proposition → Implication → Predicate → Predicate → Contradiction → Sum → Lean → Function
|
||||
Path Predicate → Inequality → Sum
|
||||
-- Path Inequality → Prime
|
||||
-- Path Sum → Inequality -- → Induction
|
||||
-- Path SetTheory2 → Numbers
|
||||
|
||||
Path Lean → SetTheory -- → SetTheory2
|
||||
|
||||
-- Path SetTheory2 → SetFunction → Module
|
||||
-- Path Function → SetFunction
|
||||
-- Path Module → Basis → Module2
|
||||
|
||||
MakeGame
|
||||
@ -1,11 +0,0 @@
|
||||
import Lean
|
||||
|
||||
-- show all available options
|
||||
instance : ToString Lean.OptionDecl where
|
||||
toString a := toString a.defValue ++ ", [" ++ toString a.group ++ "]: " ++ toString a.descr
|
||||
|
||||
def showOptions : IO Unit := do
|
||||
let a <- Lean.getOptionDeclsArray
|
||||
IO.println f! "{a}"
|
||||
|
||||
#eval showOptions
|
||||
@ -1,29 +0,0 @@
|
||||
import Adam.Levels.Contradiction.L01_Have
|
||||
import Adam.Levels.Contradiction.L02_Suffices
|
||||
import Adam.Levels.Contradiction.L03_ByContra
|
||||
import Adam.Levels.Contradiction.L04_ByContra
|
||||
import Adam.Levels.Contradiction.L05_Contrapose
|
||||
import Adam.Levels.Contradiction.L06_Summary
|
||||
|
||||
Game "Adam"
|
||||
World "Contradiction"
|
||||
Title "Spinoza"
|
||||
|
||||
Introduction "
|
||||
**Robo**: Ich glaube, das ist Spinoza, einer der ganz wenigen Asteroiden vom Type QED. Schnell. Wir müssen uns ein bisschen beeilen, sonst verpassen wir ihn.
|
||||
|
||||
Eine halbe Stunde später seid ihr gelandet. Sehr einladend wirkt Spinoza nicht. Seine gesamte Oberfläche ist von feinem, rötlichen Sand bedeckt.
|
||||
Ein einziger, einsamer Formalosoph, der sich als Benedictus vorstellt, erwartet euch.
|
||||
|
||||
**Benedictus**: Schön, dass Ihr gekommen seid! Ich habe schon auf Euch gewartet!
|
||||
|
||||
**Du**: Hast du auch ein paar dringende Fragen … ?
|
||||
|
||||
**Benedictus**: Ach nein, aus dem Alter bin ich heraus. Aber ich kann mir denken, wie es Euch auf Implis und Quantus ergangen ist. Und glaubt, mir auf den anderen Planeten wird es nicht viel besser. Aber ich kann Euch vielleicht ein bisschen vorbereiten.
|
||||
|
||||
**Du**: Können wir nicht einfach hier bleiben und uns ein wenig ausruhen?
|
||||
|
||||
Benedictus schüttelt den Kopf.
|
||||
|
||||
**Benedictus**: Nein. Spinoza verträgt keine drei Bewohner. Und Ihr müsst bald wieder weiter, sonst wird der Weg zu weit. Wir kommen nur alle 400 Jahre bei den Planeten vorbei.
|
||||
"
|
||||
@ -1,57 +0,0 @@
|
||||
import Adam.Metadata
|
||||
|
||||
import Adam.ToBePorted
|
||||
|
||||
set_option tactic.hygienic false
|
||||
|
||||
Game "Adam"
|
||||
World "Contradiction"
|
||||
Level 1
|
||||
|
||||
Title "Was wir haben, haben wir."
|
||||
|
||||
Introduction
|
||||
"
|
||||
**Benedictus**: Hier, schaut mal. Das habe ich für Euch vorbereitet.
|
||||
"
|
||||
|
||||
-- Manchmal, wollen wir nicht am aktuellen Goal arbeiten, sondern zuerst ein
|
||||
-- Zwischenresultat beweisen, welches wir dann benützen können.
|
||||
|
||||
-- Mit `have [Name] : [Aussage]` kann man ein Zwischenresultat erstellen,
|
||||
-- dass man anschliessen beweisen muss.
|
||||
|
||||
-- Wenn du zum Beispiel die Annahmen `(h : A → ¬ B)` und `(ha : A)` hast, kannst
|
||||
-- du mit
|
||||
-- ```
|
||||
-- have g : ¬ B
|
||||
-- apply h
|
||||
-- assumption
|
||||
-- ```
|
||||
-- eine neue Annahme `(g : ¬ B)` erstellen. Danach beweist du zuerst diese Annahme,
|
||||
-- bevor du dann mit dem Beweis forfährst.
|
||||
|
||||
Statement (A B : Prop) (h : A → ¬ B) (k : A ∧ B) : False := by
|
||||
Hint "**Du**: Also als erstes teile ich wohl mal das Und (`∧`) auf."
|
||||
rcases k with ⟨h₁, h₂⟩
|
||||
Hint "**Du**: Und jetzt …
|
||||
|
||||
**Benedictus**: … solltest du dir ein passendes Zwischenresultat zurechtlegen.
|
||||
|
||||
**Robo**: Ja! Probier mal `have g : ¬ B`!"
|
||||
have g : ¬ B
|
||||
· Hint "**Du**: Was? Jetzt hab ich einfach angenommen, dass sei richtig?
|
||||
|
||||
**Robo**: Nee, jetzt musst du das erst noch beweisen, bevor du es dann benutzen kannst."
|
||||
Hint (hidden := true) "**Robo**: `apply` sollte helfen"
|
||||
apply h
|
||||
assumption
|
||||
Hint "**Du**: Und wie war das nochmals wenn zwei Annahmen sich widersprechen?
|
||||
|
||||
**Robo**: `contradiction`."
|
||||
contradiction
|
||||
|
||||
NewTactic «have»
|
||||
DisabledTactic «suffices»
|
||||
|
||||
Conclusion "**Benedictus**: Das sieht gut aus!"
|
||||
@ -1,53 +0,0 @@
|
||||
import Adam.Metadata
|
||||
|
||||
import Adam.ToBePorted
|
||||
|
||||
Game "Adam"
|
||||
World "Contradiction"
|
||||
Level 2
|
||||
|
||||
Title "Es reicht!"
|
||||
|
||||
Introduction
|
||||
"
|
||||
**Benedictus**: Ihr hättet natürlich auch erst das Hauptresultat und dann das Zwischenresultat beweisen können. Das könnt Ihr ja mal an dieser Aufgabe probieren, die ist ganz ähnlich.
|
||||
"
|
||||
|
||||
-- Die Taktik `suffices` funktioniert genau gleich wie `have`,
|
||||
-- vertauscht aber die beiden Beweisblöcke:
|
||||
|
||||
-- ```
|
||||
-- suffices h : [Aussage]
|
||||
-- [Beweis des Goals (mithilfe von h)]
|
||||
-- [Beweis der Aussage h]
|
||||
-- ```
|
||||
-- Auf Deutsch entspricht `suffices g : [Aussage]` dem Ausdruck
|
||||
-- \"Es genügt zu zeigen, dass `[Aussage]` wahr ist.\"
|
||||
|
||||
-- Man kann `have` und `suffices` nach belieben vertauschen. Bevorzugt, wählt man es so,
|
||||
-- dass der erste Beweisblock der kürzere ist. Zum Beispiel wäre bei der vorigen Aufgabe
|
||||
-- `suffices` schöner gewesen:
|
||||
|
||||
-- "Angenommen, man hat eine Implikation $A \\Rightarrow \\neg B$ und weiss, dass
|
||||
-- $A \\land B$ wahr ist. Zeige, dass dies zu einem Widerspruch führt."
|
||||
|
||||
Statement
|
||||
(A B : Prop) (h : A → ¬ B) (k₁ : A) (k₂ : B) : False := by
|
||||
Hint "**Robo**: Ich weiss was er meint! Anstatt `have` kannst du auch `suffices`
|
||||
verwenden. Das funktioniert genau gleich, außer, dass dann die beiden Beweisziele vertauscht sind.
|
||||
|
||||
**Du**: Also nach `suffices g : ¬B` muss ich dann zuerst zeigen, wie man mit `g` den Beweis
|
||||
abschliesst, bevor ich `g` beweise?
|
||||
|
||||
**Robo**: Genau!"
|
||||
suffices g : ¬ B
|
||||
Hint "**Robo**: Also hier beendest du den Beweis unter der Annahme `{g}` sei wahr."
|
||||
contradiction
|
||||
Hint "**Robo**: Und hier beweist du das Zwischenresultat."
|
||||
apply h
|
||||
assumption
|
||||
|
||||
NewTactic «suffices»
|
||||
DisabledTactic «have»
|
||||
|
||||
Conclusion "**Benedictus**: Genau so meinte ich das. Ob Ihr nun in Zukunft `have` und `suffices` verwendet, ist reine Geschmacksfrage. Hauptsache, Ihr wisst, wie Ihr entfernte Ziele in kleinen Schritte erreicht."
|
||||
@ -1,47 +0,0 @@
|
||||
import Adam.Metadata
|
||||
|
||||
import Adam.ToBePorted
|
||||
|
||||
Game "Adam"
|
||||
World "Contradiction"
|
||||
Level 3
|
||||
|
||||
Title "Widerspruch"
|
||||
|
||||
Introduction
|
||||
"**Benedictus**: Hier ist noch eine Variante.
|
||||
"
|
||||
|
||||
-- Eine sehr nützliche Beweismethode ist per Widerspruch.
|
||||
|
||||
-- Wir habe schon gesehen, dass `contradiction` einen Widerspruch in den Annahmen
|
||||
-- sucht, und damit jegliches beweisen kann.
|
||||
|
||||
-- Um dorthin zu kommen, können wir `by_contra h` brauchen, welches das aktuelle
|
||||
-- Goal auf `False` setzt und die Negierung des Goals als Annahme hinzufügt.
|
||||
|
||||
-- Insbesondere braucht man `by_contra h` meistens, wenn im Goal eine Negierung
|
||||
-- steht:
|
||||
|
||||
Statement (A B : Prop) (g : A → B) (b : ¬ B) : ¬ A := by
|
||||
Hint "**Robo**: Ein `¬` im Goal heißt häufig, dass du einen Widerspruchsbeweis führen
|
||||
möchtest.
|
||||
|
||||
**Du**: Und wie mache ich das? Mit `contradiction`?
|
||||
|
||||
**Robo**: Mit `by_contra h` fängst du einen Widerspruchsbeweis an. Und mit `contradiction` schließt du ihn ab."
|
||||
by_contra h
|
||||
Hint "**Robo**: Jetzt hast du also eine Annahme `{h} : {A}`, und damit musst du einen Widerspruch herleiten.
|
||||
|
||||
Du könntest zum Beispiel jetzt mit `suffices` sagten, welchen Widerspruch du gern herleiten möchtest, etwa `suffices k : B`
|
||||
"
|
||||
suffices k : B
|
||||
Hint "**Du**: Ah, und jetzt kann ich einfach sagen dass sich die Annahmen `{B}` und `¬{B}` sich widersprechen."
|
||||
contradiction
|
||||
Hint "**Robo**: Und jetzt musst du nur noch das Zwischenresultat herleiten, dass zu diesem Widerspruch geführt hat."
|
||||
apply g
|
||||
assumption
|
||||
|
||||
NewTactic by_contra
|
||||
|
||||
Conclusion "**Benedictus**: Ich sehe schon, Ihr lernt schnell!"
|
||||
@ -1,43 +0,0 @@
|
||||
import Adam.Metadata
|
||||
|
||||
import Adam.ToBePorted
|
||||
|
||||
Game "Adam"
|
||||
World "Contradiction"
|
||||
Level 4
|
||||
|
||||
Title "Kontraposition"
|
||||
|
||||
Introduction
|
||||
"
|
||||
**Benedictus**: Ich habe noch eine schöne Frage zu ungeraden Quadraten für Euch. Aber vorher beweist Ihr besser noch diese Äquivalenz hier. Ich gaube, die hat sogar bei Euch einen Namen: *Kontrapositionsäquivalenz*, oder so etwas. Auf Leansch nennen wir die Äuqivalenz einfach `not_imp_not`. Ist doch viel einleuchtender, oder?
|
||||
"
|
||||
|
||||
Statement not_imp_not (A B : Prop) : A → B ↔ (¬ B → ¬ A) := by
|
||||
Hint "**Du**: Ja, das habe ich tatsächlich schon einmal gesehen.
|
||||
|
||||
**Robo**: Ja, klar hast du das schon einmal gesehen. Das benutzen Mathematiker doch ständig. Wenn ihnen zu $A ⇒ B$ nichts einfällt, zeigen sie stattdessen $¬B ⇒ ¬A$. Ich würde das ja statt *Kontraposition* oder `not_imp_not` eher *von_hinten_durch_die_Brust_ins_Auge* nennen. Aber gut, ich will mich nicht einmisschen.
|
||||
"
|
||||
Hint (hidden := true) "**Robo**: Fang doch mal mit `constructor` an."
|
||||
constructor
|
||||
intro h b
|
||||
by_contra a
|
||||
Hint "**Robo**: Ich würde wieder mit `suffices g : B` einen Widerspruch herbeiführen."
|
||||
suffices b : B
|
||||
contradiction
|
||||
apply h
|
||||
assumption
|
||||
intro h a
|
||||
Hint "**Robo**: Hier würde ich ebenfalls einen Widerspruchsbeweis anfangen."
|
||||
by_contra b
|
||||
Hint (hidden := true) "**Robo**: `suffices g : ¬ A` sieht nach einer guten Option aus."
|
||||
suffices g : ¬ A
|
||||
contradiction
|
||||
apply h
|
||||
assumption
|
||||
|
||||
DisabledTactic rw
|
||||
DisabledLemma not_not
|
||||
LemmaTab "Logic"
|
||||
|
||||
Conclusion ""
|
||||
@ -1,23 +0,0 @@
|
||||
import Adam.Levels.Function.L01_Function
|
||||
import Adam.Levels.Function.L02_Let
|
||||
import Adam.Levels.Function.L03_Piecewise
|
||||
import Adam.Levels.Function.L04_Injective
|
||||
import Adam.Levels.Function.L05_Injective
|
||||
import Adam.Levels.Function.L06_Injective
|
||||
import Adam.Levels.Function.L07_Surjective
|
||||
import Adam.Levels.Function.L08_Bijective
|
||||
import Adam.Levels.Function.L09_Inverse
|
||||
|
||||
Game "Adam"
|
||||
World "Function"
|
||||
Title "Abbildungen"
|
||||
|
||||
Introduction "
|
||||
Auf der Suche nach dem Buch der Urbilder landet ihr auf einem kleinen Mond, der bis auf
|
||||
eine Insel komplett mit Wasser bedeckt zu sein scheint.
|
||||
|
||||
Auf der Insel seht ihr verschiedene große und kleine Behausungen, manche aus Stroh und Holz,
|
||||
vereinzelte aus Lehm.
|
||||
|
||||
Planlos geht ihr zum ersten Haus bei dem jemand vorne außen sitzt.
|
||||
"
|
||||
@ -1,112 +0,0 @@
|
||||
import Adam.Metadata
|
||||
|
||||
import Adam.Options.MathlibPart
|
||||
|
||||
Game "Adam"
|
||||
World "Function"
|
||||
Level 9
|
||||
|
||||
Title "Inverse"
|
||||
|
||||
set_option tactic.hygienic false
|
||||
|
||||
Introduction
|
||||
"
|
||||
Eigentlich hast du nur beiläufig Robo gefragt, ob bijektiv nicht auch bedeute, dass
|
||||
eine Inverse Funktion bestehe. Jetzt steht ihr aber schon seit einer halben Stunde rum
|
||||
und der Gelehrte möchte wissen, wie das den genau ginge.
|
||||
|
||||
Offensichtlich kennt er diese Aussage als `Function.bijective_iff_has_inverse` aus seinen Büchern,
|
||||
aber er möchte, dass du ihm das hier und jetzt nochmals von Grund auf zeigst.
|
||||
"
|
||||
|
||||
open Function
|
||||
|
||||
--TODO: This is a really hard proof
|
||||
Statement Function.bijective_iff_has_inverse "" {A B : Type} (f : A → B) :
|
||||
Bijective f ↔ ∃ g, LeftInverse g f ∧ RightInverse g f := by
|
||||
Hint "**Du**: Nah da sagt mir so manches nichts, aber ich kann ja mal mit dem `↔` anfangen,
|
||||
das kenn ich ja schon."
|
||||
constructor
|
||||
· intro h
|
||||
Hint "**Robo**: Tipp. Teil doch `Bijective` mit `rcases {h} with ⟨hI, hS⟩` in
|
||||
`Injective` und `Surjective` auf!"
|
||||
rcases h with ⟨hI, hS⟩
|
||||
Hint "**Du**: Ja was ist eigentlich die Inverse von `f`…?
|
||||
|
||||
**Robo**: Hast du eine Idee?
|
||||
|
||||
**Du**: Also von der Surjektivität weiss ich, dass für alle `y` ein Urbild existiert
|
||||
und mit der Injektivität könnte ich dann zeigen, dass dieses eindeutig ist.
|
||||
|
||||
**Robo**: Also Schritt für Schritt: Mit `fun y ↦ ({hS} y).choose ` kannst du eine Funktion
|
||||
definieren, die `y` irgendein Urbild zuweist.
|
||||
|
||||
**Du**: Die ist aber nicht wohldefiniert, oder?
|
||||
|
||||
**Robo**: In der Mathe nicht. In Lean geht das ganz gut, aber es ist dann unmöglich etwas
|
||||
darüber zu beweisen, wenn es mehrere Möglichkeiten gäbe."
|
||||
use fun x => (hS x).choose
|
||||
constructor
|
||||
· Hint "**Robo**: fang mal mit `intro` an."
|
||||
intro x
|
||||
Hint "**Du**: kompliziert.
|
||||
|
||||
**Robo**: Aber mit `simp` kannst du es ja etwas vereinfachen."
|
||||
simp
|
||||
Hint "**Du**: Das kann ich jetzt nicht zeigen solange ich nicht weiss, dass nur genau ein
|
||||
Urbild besteht.
|
||||
|
||||
**Robo**: Dann wende doch mit `apply {hI}` die Injektivität an!"
|
||||
apply hI
|
||||
Hint "**Robo**: Dies ist jetzt eine etwas tautologische Aussage. In Lean ist das
|
||||
`Exists.choose_spec`. Konkret `apply Exists.choose_spec (hS (f x))`."
|
||||
apply Exists.choose_spec (hS (f x))
|
||||
· Hint "**Robo**: Gut! Auf zum Rechtsinversen! Fang auch hier wieder mit `intro` an."
|
||||
intro x
|
||||
Hint "**Du**: Kann ich das vereinfachen?"
|
||||
simp
|
||||
Hint "**Du**: Also wieder `Exists.choose_spec`?
|
||||
|
||||
**Robo**: Genau! Diesmal mit dem Argument `(hS x)`."
|
||||
apply Exists.choose_spec (hS x)
|
||||
· Hint "**Robo**: Die eine Richtung ist gezeigt. Jetzt auf zur Rückrichtung!"
|
||||
intro h
|
||||
Hint "**Robo**: Zerlege {h} noch soweit du kannst!"
|
||||
rcases h with ⟨g, h⟩
|
||||
Hint "**Robo**: Das UND auch noch!"
|
||||
rcases h with ⟨hL, hR⟩
|
||||
Hint "**Robo**: Das `Bijective` kannst du auch aufteilen."
|
||||
constructor
|
||||
· Hint "**Robo**: Injektivität ist der schwierige Teil. Fang mal an mit `intro`."
|
||||
intro a b hab
|
||||
Hint "**Robo**: Im nächsten Schritt must du `LeftInverse` brauchen um das Goal
|
||||
zu `g (f a) = g (f b)` zu wechseln: benutze `rw [←{hL} {a}, …]`."
|
||||
rw [← hL a, ← hL b]
|
||||
Hint "**Du**: Wenn die Argumente `f a = f b` gleich sind, ist dann auch `g (f a) = g (f b)`,
|
||||
wie sag ich das?
|
||||
|
||||
**Robo**: Das heisst `apply congrArg`."
|
||||
apply congrArg
|
||||
assumption
|
||||
· Hint "Die Surjektivität sollte einfacher sein."
|
||||
intro x
|
||||
Hint (hidden := true) "**Robo**: Psst, mit `RightInverse g f` weisst du, dass `f (g x) = x`.
|
||||
Hilft das rauszufinden was du hier brauchen musst?"
|
||||
use g x
|
||||
Hint (hidden := true) "**Robo**: Du kannst die `RightInverse`-Annahme einfach mit `rw`
|
||||
benützen."
|
||||
rw [hR]
|
||||
|
||||
NewDefinition LeftInverse RightInverse
|
||||
NewLemma Exists.choose Exists.choose_spec congrArg congrFun
|
||||
DisabledLemma Function.bijective_iff_has_inverse
|
||||
LemmaTab "Logic"
|
||||
|
||||
|
||||
Conclusion
|
||||
"Endlich entkommt ihr der Bibliothek.
|
||||
|
||||
**Robo**: Da würden mich keine zehn Pferde nochmals hineinbringen!
|
||||
|
||||
**Du**: Von wegen Pferden, wie viele PS hat eigentlich unser Raumschiff?"
|
||||
@ -1,37 +0,0 @@
|
||||
import Adam.Levels.Implication.L01_Intro
|
||||
import Adam.Levels.Implication.L02_Revert
|
||||
import Adam.Levels.Implication.L03_Apply
|
||||
import Adam.Levels.Implication.L04_Apply
|
||||
import Adam.Levels.Implication.L05_Apply
|
||||
import Adam.Levels.Implication.L06_Iff
|
||||
import Adam.Levels.Implication.L07_Rw
|
||||
import Adam.Levels.Implication.L08_Iff
|
||||
import Adam.Levels.Implication.L09_Iff
|
||||
import Adam.Levels.Implication.L10_Apply
|
||||
import Adam.Levels.Implication.L11_ByCases
|
||||
import Adam.Levels.Implication.L12_Rw
|
||||
import Adam.Levels.Implication.L13_Summary
|
||||
|
||||
Game "Adam"
|
||||
World "Implication"
|
||||
Title "Implis"
|
||||
|
||||
Introduction
|
||||
"
|
||||
Zurück im Raumschiff macht ihr euch auf den Weg zu einem der beiden Monde, die ebenfalls
|
||||
bewohnt zu sein scheinen.
|
||||
|
||||
**Du**: Ich habe immer noch das Gefühl, dass ich die Aufgabe von Königin *Logisinde* ohne `tauto` nicht hätte lösen können.
|
||||
Kamen in der Aufgabe nicht auch Implikationen vor?
|
||||
|
||||
**Robo**: Vielleicht haben wir ja auf dem Mond *Implis*, den wir gerade ansteuern, Gelegenheit, noch etwas dazuzulernen. Festhalten bitte …
|
||||
|
||||
Und damit leitet Robo den Landeanflug ein.
|
||||
|
||||
Implis scheint ein riesiger Tagebau zu sein.
|
||||
Überall verlaufen Förderbänder, kreuz und quer, aber die meisten stehen still.
|
||||
Ein schüchterner Operationsleiter erwartet Euch bereits.
|
||||
|
||||
**Operationsleiter**: Ihr kommt mir gerade recht! Ich habe schon gehört. Echte Mathematiker! Wisst Ihr, wir fördern hier Wahrheitswerte. Und dabei muss man höllisch aufpassen. Ein Fehler, und alles bricht zusammen. Aber ich bin sehr vorsichtig. Ich sage immer: Lieber Stillstand als Untergang!
|
||||
|
||||
"
|
||||
@ -1,49 +0,0 @@
|
||||
import Adam.Metadata
|
||||
import Adam.Options.MathlibPart
|
||||
|
||||
set_option tactic.hygienic false
|
||||
|
||||
Game "Adam"
|
||||
World "Implication"
|
||||
Level 1
|
||||
|
||||
Title "Intro"
|
||||
|
||||
Introduction
|
||||
"
|
||||
**Operationsleiter**: Hier, zum Beispiel:
|
||||
"
|
||||
|
||||
Statement (A B : Prop) (hb : B) : A → (A ∧ B) := by
|
||||
Hint "
|
||||
**Operationsleiter:** Die Arbeiten meinen, das wäre so richtig und wir würden das dringend brauchen. Aber keiner kann es mir beweisen.
|
||||
|
||||
**Du**: Einen Moment. Das ist ja gerade so eine Implikation (`\\to`). Wir nehmen an, dass `{B}` gilt, und wollen zeigen, dass dann gilt `{A}` impliziert `{A} und {B}`. Ja, klar! Natürlich stimmt das.
|
||||
|
||||
Der Operationsleiter sieht dich erwartungsvoll an.
|
||||
|
||||
**Du** *(leise zu Robo)*: Soll ich ihm `tauto` aufschreiben?
|
||||
|
||||
**Robo** *(leise zurück)*: So wie der aussieht, fürchte ich, das wird er auch nicht verstehen.
|
||||
Schreib den Beweis lieber aus.
|
||||
|
||||
**Du**: Aber wie denn? Ich glaube, ich würde als erstes gern so etwas sagen wie 'Nehmen wir also an, `{A}` gilt …'
|
||||
|
||||
**Robo**: Ja, gute Idee. Wähle dazu für deine Annahme einfach einen Namen, zum Beispiel `h`, und schreib `intro h`."
|
||||
intro hA
|
||||
Hint "**Du**: OK. Jetzt habe ich also sowohl `{A}` als auch `{B}` in meinen Annahmen und muss `{A} ∧ {B}` zeigen.
|
||||
|
||||
**Robo**: Genau. Und wie das geht, weißt du ja schon."
|
||||
constructor
|
||||
assumption
|
||||
assumption
|
||||
|
||||
Conclusion "**Operationsleiter:** Perfekt! Danke schön!
|
||||
|
||||
Er geht zu einer Schalttafel und ein paar Knöpfe. Irgendwo setzt sich lautstark ein Förderband in Bewegung.
|
||||
|
||||
**Operationsleiter:** Habt Ihr vielleicht noch ein paar Minuten?
|
||||
"
|
||||
|
||||
NewTactic intro
|
||||
DisabledTactic tauto
|
||||
@ -1,35 +0,0 @@
|
||||
import Adam.Metadata
|
||||
|
||||
set_option tactic.hygienic false
|
||||
|
||||
Game "Adam"
|
||||
World "Implication"
|
||||
Level 2
|
||||
|
||||
Title "Revert"
|
||||
|
||||
Introduction
|
||||
"Der Operationsleiter holt aus einem Container einen Stapel Papier hervor.
|
||||
|
||||
**Operationsleiter:** Hier hat sich echt einiges angesammelt. Wäre echt super, wenn Ihr mir noch ein bisschen helfen könntet.
|
||||
|
||||
Er übergibt Euch das oberste Blatt."
|
||||
|
||||
Statement (A B : Prop) (ha : A) (h : A → B) : B := by
|
||||
Hint "**Operationsleiter:** Das ist von einem Kollegen.
|
||||
|
||||
**Robo**: Oh, das hab ich schon einmal irgendwo gelesen. Warte mal … Richtig! Das war damals, als ich Wikipedia gecrawlt habe: `Der Modus ponens ist eine schon in der antiken Logik geläufige Schlussfigur, die in vielen logischen …`
|
||||
|
||||
**Du**: Robo! Gefragt ist ein Beweis und kein historischer Aufsatz! Oder komme ich hier etwa mit `mopo` oder so etwas weiter?
|
||||
|
||||
**Robo**: Ok, nein, sorry. `mopo` gibt es nicht. Probier lieber `revert {ha}`."
|
||||
revert ha
|
||||
Hint "**Du**: Aha. `revert` ist qausi `intro` rückwärts.
|
||||
|
||||
**Robo:** Genau. `intro` nimmt die Prämisse aus einer Implikation `{A} \\to {B}` im Beweisziel und macht daraus eine Annahme. `revert` nimmt umgekehrt eine Annahme und setzt sie als Implikationsprämisse vor das Beweisziel. Aber nun mach schon fertig."
|
||||
assumption
|
||||
|
||||
Conclusion "Der Operationsleiter nimmt erfreut Eure Lösung entgegen, und greift zum Telefon."
|
||||
|
||||
NewTactic revert
|
||||
DisabledTactic tauto
|
||||
@ -1,33 +0,0 @@
|
||||
import Adam.Metadata
|
||||
|
||||
Game "Adam"
|
||||
World "Implication"
|
||||
Level 3
|
||||
|
||||
Title "Apply"
|
||||
|
||||
Introduction
|
||||
"
|
||||
Leider läuft das Telefonat nicht so gut. Er legt wieder auf und schüttelt mit dem Kopf.
|
||||
|
||||
**Operationsleiter**: Der Kollege auf der anderen Seite des Mondes versteht kein `revert`. Oder er tut zumindest so. Habt Ihr noch eine andere Idee?
|
||||
|
||||
Er zieht eine Linie unter Euren Beweis, ergänzt ein durchgestrichenes ~`revert`~, und legt Euch das Blatt ein zweites Mal vor.
|
||||
"
|
||||
|
||||
Statement (A B : Prop) (hA : A) (h : A → B) : B := by
|
||||
Hint "**Robo**: Vielleicht wäre es ohnehin eleganter gewesen, mit Implikation mit `apply {h}` anzuwenden."
|
||||
apply h
|
||||
Hint "**Du**: Ja, das kommt mir jetzt auch natürlich vor."
|
||||
assumption
|
||||
|
||||
Conclusion "Diesmal scheint das Telefont erfolgreich zu verlaufen."
|
||||
|
||||
NewTactic apply
|
||||
DisabledTactic revert tauto
|
||||
|
||||
-- Katex notes
|
||||
-- `\\( \\)` or `$ $` for inline
|
||||
-- and `$$ $$` block.
|
||||
-- align block:
|
||||
-- $$\\begin{aligned} 2x - 4 &= 6 \\\\ 2x &= 10 \\\\ x &= 5 \\end{aligned}$$
|
||||
@ -1,29 +0,0 @@
|
||||
import Adam.Metadata
|
||||
|
||||
set_option tactic.hygienic false
|
||||
|
||||
Game "Adam"
|
||||
World "Implication"
|
||||
Level 4
|
||||
|
||||
Title "Implikation"
|
||||
|
||||
Introduction
|
||||
"
|
||||
**Operationsleiter**: Das hier ist jetzt weider ein lokales Problem.
|
||||
"
|
||||
|
||||
Statement (A B C : Prop) (f : A → B) (g : B → C) : A → C := by
|
||||
Hint "**Du**: Ich soll Implikationen $A \\Rightarrow B \\Rightarrow C$ zu $A \\Rightarrow C$
|
||||
kombinieren?
|
||||
|
||||
**Robo**: Am besten fängst du mit `intro` an und arbeitest dich dann rückwärts durch."
|
||||
intro hA
|
||||
Hint (hidden := true) "**Robo**: Das ist wieder eine Anwendung von `apply`."
|
||||
apply g
|
||||
apply f
|
||||
assumption
|
||||
|
||||
Conclusion "**Operationsleiter**: Ihr seid echt super!"
|
||||
|
||||
DisabledTactic tauto
|
||||
@ -1,49 +0,0 @@
|
||||
import Adam.Metadata
|
||||
|
||||
Game "Adam"
|
||||
World "Implication"
|
||||
Level 5
|
||||
|
||||
Title "Implikation"
|
||||
|
||||
Introduction
|
||||
"
|
||||
Die nächste Seite sieht ein bisschen komplizierter aus. Damit Ihr nicht die Übersicht verliert, fasst Robo sofort die verschiedenen Implikationen in einem Diagramm zusammen.
|
||||
$$
|
||||
\\begin{CD}
|
||||
A @>{f}>> B @<{g}<< C \\\\
|
||||
@. @V{h}VV @V{m}VV \\\\
|
||||
D @>{i}>> E @>{k}>> F \\\\
|
||||
@A{m}AA @A{n}AA @V{p}VV \\\\
|
||||
G @<{q}<< H @>{r}>> I
|
||||
\\end{CD}
|
||||
$$
|
||||
"
|
||||
Statement
|
||||
(A B C D E F G H I : Prop)
|
||||
(f : A → B) (g : C → B) (h : B → E) (i : D → E) (k : E → F) (m : G → D)
|
||||
(n : H → E) (p : F → I) (q : H → G) (r : H → I) : A → I := by
|
||||
Hint "**Du**: Also ich muss einen Pfad von Implikationen $A \\Rightarrow I$ finden.
|
||||
|
||||
**Robo**: Dann fängst du am besten wieder mit `intro` an."
|
||||
|
||||
intro ha
|
||||
Branch
|
||||
apply r
|
||||
Hint "**Robo**: Das sieht nach einer Sackgasse aus …"
|
||||
Hint (hidden := true) "**Robo**: Na wieder `apply`, was sonst."
|
||||
apply p
|
||||
apply k
|
||||
apply h
|
||||
Branch
|
||||
apply g
|
||||
Hint "**Robo**: Nah, da stimmt doch was nicht …"
|
||||
apply f
|
||||
assumption
|
||||
|
||||
Conclusion
|
||||
"Der Operationsleiter bedankt sich wieder artig. Er drückt wieder auf ein paar Knöpfe, und mit einem lauten Ratteln springen mehrere Förderbänder gleichzeitig wieder an."
|
||||
|
||||
DisabledTactic tauto
|
||||
|
||||
-- https://www.jmilne.org/not/Mamscd.pdf
|
||||
@ -1,41 +0,0 @@
|
||||
import Adam.Metadata
|
||||
|
||||
Game "Adam"
|
||||
World "Implication"
|
||||
Level 6
|
||||
|
||||
Title "Genau dann, wenn"
|
||||
|
||||
Introduction
|
||||
"
|
||||
**Operationsleiter:** Wir hatten auch mal ein paar Förderbänder, die in beide Richtungen laufen konnten. Die hatte ich vorsichtshalber alle abgestellt, weil in den neusten Handbüchern von solchen Doppelbändern abgeraten wird. Aber vielleicht sind sie ja unter bestimmten Voraussetzungen doch sicher? Was meint Ihr zu diesem Fall?
|
||||
"
|
||||
|
||||
Statement (A B : Prop) (mp : A → B) (mpr : B → A) : A ↔ B := by
|
||||
Hint "**Robo**: `→` ist natürlich Leansch für `$\\iff$`.
|
||||
Die Aussage `A ↔ B` besteht also aus zwei Teilen; sie ist als `⟨A → B, B → A⟩` definiert.
|
||||
|
||||
**Du**: Also ganz ähnlich wie das UND, `A ∧ B`?
|
||||
|
||||
**Robo**: Genau. Entsprechend kannst du auch hier mit `constructor` anfangen."
|
||||
constructor
|
||||
Hint "**Du**: Ah, und die beiden Teile habe ich schon in den Annahmen."
|
||||
assumption
|
||||
assumption
|
||||
|
||||
Conclusion
|
||||
"
|
||||
**Operationsleiter**: Ok, das leuchtet mir ein.
|
||||
|
||||
**Robo** *(zu dir)*: Übrigens, so wie bei `(h : A ∧ B)` die beiden Teile `h.left` und `h.right` heißen,
|
||||
heißen bei `(h : A ↔ B)` die beiden Teile `h.mp` und `h.mpr`.
|
||||
|
||||
**Du**: Also `h.mp` ist `A → B`? Wieso `mp`?
|
||||
|
||||
**Robo**: `mp` steht für Modus Ponens`. Der Modus ponens ist eine schon in der antiken Logik geläufige Schlussfigur, die in vielen logischen Systemen … Ach nee, das wolltest du ja nicht hören. Das \"r\" in `mpr` steht für \"reverse\", weil's die Rückrichtung ist.
|
||||
"
|
||||
|
||||
NewTactic constructor
|
||||
DisabledTactic tauto rw
|
||||
|
||||
-- TODO : `case mpr =>` ist mathematisch noch sinnvoll.
|
||||
@ -1,45 +0,0 @@
|
||||
import Adam.Metadata
|
||||
|
||||
import Init.Data.ToString
|
||||
-- #check List UInt8
|
||||
|
||||
set_option tactic.hygienic false
|
||||
|
||||
Game "Adam"
|
||||
World "Implication"
|
||||
Level 7
|
||||
|
||||
Title "Genau dann, wenn"
|
||||
|
||||
Introduction
|
||||
"
|
||||
**Operationsleiter**: Hier ist noch so etwas.
|
||||
"
|
||||
|
||||
Statement (A B C D : Prop) (h₁ : C ↔ D) (h₂ : A ↔ B) (h₃ : A ↔ D) : B ↔ C := by
|
||||
Hint "**Du**: $B \\iff A \\iff D \\iff C$, die sind doch alle äquivalent…
|
||||
|
||||
**Robo**: Ja, aber du musst ihm helfen, die Äquivalenzen umzuschreiben. Mit `rw [h₁]` kannst du `C` durch `D`
|
||||
ersetzen."
|
||||
rw [h₁]
|
||||
Hint "**Du** Und wenn ich in die andere Richtung umschreiben möchte?
|
||||
|
||||
**Robo**: Dann schreibst du ein `←` (`\\l`, also klein \"L\") vor den Namen, also `rw [← hₓ]`."
|
||||
Branch
|
||||
rw [← h₃]
|
||||
Hint "**Du**: Ehm, das war verkehrt.
|
||||
|
||||
**Robo**: Ja, anders herum wär's besser gewesen. Aber wenn du jetzt einfach weitermachst, bis Du
|
||||
sowas wie `A ↔ A` erhältst, kann `rfl` das beweisen.
|
||||
|
||||
**Robo: Da fällt mir ein, `rw` wendet ohnehin auch versuchsweise `rfl` an.
|
||||
Das heißt, du musst `rfl` nicht einmal ausschreiben."
|
||||
rw [h₂]
|
||||
rw [←h₂]
|
||||
assumption
|
||||
|
||||
Conclusion "**Operationsleiter**: Wenn Ihr so weitermacht, dann kommen wir ja durch den ganzen Packen durch!"
|
||||
|
||||
NewTactic rw assumption
|
||||
DisabledTactic tauto
|
||||
-- NewLemma Iff.symm
|
||||
@ -1,44 +0,0 @@
|
||||
import Adam.Metadata
|
||||
|
||||
set_option tactic.hygienic false
|
||||
|
||||
Game "Adam"
|
||||
World "Implication"
|
||||
Level 8
|
||||
|
||||
Title "Genau dann wenn"
|
||||
|
||||
Introduction
|
||||
"
|
||||
**Operationsleiter**: Das hier ist wieder für meinen beschränkten Kollegen. Ich glaube, `rw` mag der auch nicht. Geht das trotzdem?
|
||||
"
|
||||
|
||||
Statement (A B C : Prop) (h : A ↔ B) (g : B → C) : A → C := by
|
||||
Hint "**Du**: Naja ich kann wohl immerhin mal mit `intro` anfangen und annehmen,
|
||||
dass `{A}` wahr sei …
|
||||
|
||||
**Robo**: … und dann schauen wir weiter!"
|
||||
intro hA
|
||||
Hint "**Robo**: Also eine Implikation wendet man mit `apply` an …
|
||||
|
||||
**Du**: Weiß ich doch!"
|
||||
apply g
|
||||
Hint "**Robo**: … und du kannst die Implikation `{A} → {B}` genau gleich mit
|
||||
`apply {h}.mp` anwenden.
|
||||
|
||||
**Du**: Aber normalerweise könnte ich hier auch `rw [← h]` sagen, oder?
|
||||
|
||||
**Robo**: Ja ja, nur nicht auf der anderen Seite des Mondes.
|
||||
"
|
||||
apply h.mp
|
||||
assumption
|
||||
|
||||
Conclusion "**Operationsleiter**: Ok, super. Das müsste passen.
|
||||
|
||||
Er telefoniert wieder.
|
||||
|
||||
**Operationsleiter**: Bingo!
|
||||
"
|
||||
|
||||
NewTactic apply assumption
|
||||
DisabledTactic tauto rw
|
||||
@ -1,53 +0,0 @@
|
||||
import Adam.Metadata
|
||||
import Std.Tactic.RCases
|
||||
import Adam.Options.MathlibPart
|
||||
|
||||
Game "Adam"
|
||||
World "Implication"
|
||||
Level 9
|
||||
|
||||
Title "Genau dann wenn"
|
||||
|
||||
Introduction
|
||||
"
|
||||
**Operationsleiter**: Ah, die nächste Seite ist auch von diesem Kollegen. Aber da ist noch eine Notiz bei. Wir hatten hierfür schon einmal einen Beweis, aber den mochte er nicht. Er wollte einen Beweis, der weder `rw` noch `apply` verwendet!!
|
||||
|
||||
Er holt tief Luft und seuft.
|
||||
|
||||
**Operationsleiter**: Ich glaube, der stellt sich immer viel dümmer, als er ist. Aber meint Ihr, Ihr schafft das?
|
||||
"
|
||||
|
||||
Statement (A B : Prop) : (A ↔ B) → (A → B) := by
|
||||
Hint "**Du**: Hmm, mindestens mit der Implikation kann ich anfangen."
|
||||
Hint (hidden := true) "**Robo**: Genau, das war `intro`."
|
||||
intro h
|
||||
Hint "**Du**: Also, ich kenne `rw [h]` und `apply h.mp`, aber das wollten wir ja diesmal vermeiden.
|
||||
|
||||
**Robo**: Was du machen könntest, ist, mit `rcases h with ⟨mp, mpr⟩` die Annahme in zwei
|
||||
Teile aufteilen."
|
||||
Branch
|
||||
intro a
|
||||
Hint "**Robo**: Hier müsstest du jetzt `rw [←h]` oder `apply h.mp` benutzen.
|
||||
Geh lieber einen Schritt zurück, sodass das Goal `A → B` ist."
|
||||
rcases h with ⟨mp, mpr⟩
|
||||
Hint (hidden := true) "**Du**: Ah, und jetzt ist das Beweisziel in den Annahmen."
|
||||
assumption
|
||||
|
||||
Conclusion
|
||||
"
|
||||
**Operationsleiter**: Perfekt, das sollte reichen!
|
||||
"
|
||||
OnlyTactic intro rcases assumption
|
||||
DisabledTactic rw apply tauto
|
||||
|
||||
-- -- TODO: The new `cases` works differntly. There is also `cases'`
|
||||
-- example (A B : Prop) : (A ↔ B) → (A → B) := by
|
||||
-- intro h
|
||||
-- cases h with
|
||||
-- | intro a b =>
|
||||
-- assumption
|
||||
|
||||
-- example (A B : Prop) : (A ↔ B) → (A → B) := by
|
||||
-- intro h
|
||||
-- cases' h with a b
|
||||
-- assumption
|
||||
@ -1,5 +0,0 @@
|
||||
import Adam.Levels.Induction.L01_Induction
|
||||
|
||||
Game "Adam"
|
||||
World "Induction"
|
||||
Title "Übungen Induktions"
|
||||
@ -1,17 +0,0 @@
|
||||
import Adam.Levels.Inequality.L01_LE
|
||||
import Adam.Levels.Inequality.L02_Pos
|
||||
import Adam.Levels.Inequality.L03_Linarith
|
||||
import Adam.Levels.Inequality.L04_Linarith
|
||||
import Adam.Levels.Inequality.L05_DrinkersParadox
|
||||
|
||||
Game "Adam"
|
||||
World "Inequality"
|
||||
Title "Traum"
|
||||
|
||||
Introduction "
|
||||
Später erinnerst du dich gar nicht mehr wo und wann du diese Unterhaltung hattest, geschweige
|
||||
denn mit wem. Vielleicht war es ein Traum, oder eine Erscheinung. Vielleicht war es
|
||||
auch nur eines Abends über einer Runde Getränke.
|
||||
|
||||
Aber auf jedenfall hast du irgendwo gelernt, was du nun weisst.
|
||||
"
|
||||
@ -1,62 +0,0 @@
|
||||
import Adam.Metadata
|
||||
|
||||
import Adam.Options.MathlibPart
|
||||
|
||||
Game "Adam"
|
||||
World "Inequality"
|
||||
Level 5
|
||||
|
||||
Title "Drinker's Paradox"
|
||||
|
||||
set_option tactic.hygienic false
|
||||
|
||||
Introduction
|
||||
"
|
||||
**weitere Person**: Jetzt aber zu einem anderen Thema. Kennt ihr eigentlich das
|
||||
Drinker-Paradoxon?
|
||||
|
||||
**Robo**: Das ist in meinem System. *In dieser Bar gibt es eine Person, so dass
|
||||
falls diese Person jetzt am drinken ist, dann sind alle am trinken*.
|
||||
|
||||
**weitere Person**: Genau! Könnt ihr mir das beweisen?
|
||||
"
|
||||
|
||||
open Function
|
||||
|
||||
Statement {People : Type} [Inhabited People] (isDrinking : People → Prop) :
|
||||
∃ (x : People), isDrinking x → ∀ (y : People), isDrinking y := by
|
||||
Hint "**Du**: Wenn `p` eine Person ist, dann ist also `isDrinking p` eine Aussage,
|
||||
die wahr oder falsch ist. Soweit so gut.
|
||||
Wieso hat er aber `Inhabited People` hinzugefügt?
|
||||
|
||||
**Robo**: Die Aussage ist falsch, wenn die Bar leer wäre, da dann keine solche
|
||||
Person existieren kann. Jedenfalls kannst du dadurch jederzeit `default`, oder lang
|
||||
`(default : Person)`, schreiben, wenn du einfach irgendeine Person brauchst.
|
||||
|
||||
**Du**: Und wie fang ich jetzt an?
|
||||
|
||||
**Robo**: Du könntest eine Fallunterscheidung machen, ob die Aussage
|
||||
`∀ (y : People), isDrinking y` wahr oder falsch ist."
|
||||
Hint (hidden := true) "**Robo**: Schau mal `by_cases` an."
|
||||
by_cases ∀ y, isDrinking y
|
||||
Hint (hidden := true) "**Du**: Und wen nehm ich jetzt?
|
||||
|
||||
**Robo**: Wie gesagt, `default` ist eine x-beliebige Person."
|
||||
use (default : People)
|
||||
intro
|
||||
assumption
|
||||
Hint (hidden := true) "**Robo**: Du könntest hier mit `push_neg at {h}` weitermachen."
|
||||
push_neg at h
|
||||
rcases h with ⟨p, hp⟩
|
||||
use p
|
||||
intro hp'
|
||||
Hint (hidden := true) "**Robo**: Was siehst du, wenn du `{hp}` und `{hp'}` anschaust?"
|
||||
contradiction
|
||||
|
||||
LemmaTab "Logic"
|
||||
NewDefinition Inhabited
|
||||
|
||||
Conclusion
|
||||
"**weitere Person**: Fantastisch! Zum wohl!
|
||||
|
||||
…und damit endet auch deine Erinnerung und wer weiss was du anschließend gemacht hast…"
|
||||
@ -1,26 +0,0 @@
|
||||
import Adam.Levels.Lean.L01_Type
|
||||
import Adam.Levels.Lean.L02_Universe
|
||||
import Adam.Levels.Lean.L03_ImplicitArguments
|
||||
import Adam.Levels.Lean.L04_InstanceArguments
|
||||
|
||||
Game "Adam"
|
||||
World "Lean"
|
||||
Title "Lean"
|
||||
|
||||
Introduction
|
||||
"Während ihr weiter durch Täler, über Geröllhalden und zwischen monumentalen Steintürmen
|
||||
umherzieht, fragst du eines Tages Robo.
|
||||
|
||||
**Du**: Sag mal, hast du dir je Gedanken dazu gemacht, wie du eigentlich funktionierts?
|
||||
|
||||
**Robo**: Was meinst du, wie ich funktioniere? Ich bin halt… ich…
|
||||
|
||||
**Du**: Ja schon, aber was woher weisst du denn alles was du weisst?
|
||||
|
||||
**Robo**: Das kann ich dir sagen. Früher habe ich viele Datenträger verschlungen,
|
||||
und dadurch gelernt.
|
||||
|
||||
**Du**: Ob so eine Diskette wohl lecker schmeckt? Egal, ich hab ein paar Fragen zu deinem
|
||||
Lean-Modul.
|
||||
|
||||
**Robo**: Na dann nur zu!"
|
||||
@ -1,49 +0,0 @@
|
||||
import Adam.Metadata
|
||||
|
||||
import Adam.Options.MathlibPart
|
||||
|
||||
set_option tactic.hygienic false
|
||||
|
||||
Game "Adam"
|
||||
World "Lean"
|
||||
Level 2
|
||||
|
||||
Title "Universen"
|
||||
|
||||
Introduction
|
||||
"**Du**: Aber wenn alles Typen sind, welcher Typ hat dann `Type`?
|
||||
|
||||
**Robo**: `Type 1` und dieser hat Typ `Type 2`, etc.
|
||||
|
||||
**Robo**: Die Zahl nennt man *Universum*. Manchmal führt man Universen explizit
|
||||
mit `universum u` ein, öfter siehst du `(R : Type _)`, was einfach ein Platzhalter
|
||||
für irgend ein Universum ist.
|
||||
|
||||
**Du**: Das klingt ein bisschen nach Mengentheoretische Probleme, die man normalerweise
|
||||
ignoriert.
|
||||
|
||||
**Robo**: Genau! Deshalb schreibt man eigentlich immer einfach `Type _` und ist glücklich.
|
||||
Spezifischer muss man erst werden wenn man sowas wie Kategorientheorie anschaut, wo
|
||||
man die Universen tatsächlich kontrollieren muss.
|
||||
|
||||
**Du**: Oke, hier rein, da raus. Aber hast du mir noch eine Aufgabe?
|
||||
"
|
||||
|
||||
universe u
|
||||
|
||||
Statement
|
||||
(R : Type u) [CommRing R] (a b : R) : a + b = b + a := by
|
||||
Hint "**Robo**: Naja, Aufgaben zu Universen sind nicht so natürlich,
|
||||
aber vorige Aufgabe würde man eigentlich besser so schreiben, da
|
||||
kannst du mindestens das Uniersum beobachten.
|
||||
|
||||
**Du**: Ah ich sehe, `(R: Type u)` anstatt `(R : Type)`. Muss mich
|
||||
das interessieren?
|
||||
|
||||
**Robo**: Nicht wirklich…"
|
||||
ring
|
||||
|
||||
Conclusion "**Du**: Na dann. Aber gut dass ich's mal gesehen hab."
|
||||
|
||||
-- Hint (R : Type) (h : CommRing R) (a : R) (b : R) : a + b = b + a =>
|
||||
-- ""
|
||||
@ -1,23 +0,0 @@
|
||||
import Adam.Metadata
|
||||
import Adam.Options.MathlibPart
|
||||
|
||||
Game "Adam"
|
||||
World "Nat2"
|
||||
Level 3
|
||||
|
||||
Title "Primzahlen"
|
||||
|
||||
Introduction
|
||||
"
|
||||
TODO: Primzahl
|
||||
|
||||
"
|
||||
|
||||
Statement "" : True := by
|
||||
trivial
|
||||
|
||||
Conclusion
|
||||
"
|
||||
"
|
||||
|
||||
NewTactic ring
|
||||
@ -1,23 +0,0 @@
|
||||
import Adam.Metadata
|
||||
import Adam.Options.MathlibPart
|
||||
|
||||
Game "Adam"
|
||||
World "Nat2"
|
||||
Level 5
|
||||
|
||||
Title "Exists unique"
|
||||
|
||||
Introduction
|
||||
"
|
||||
TODO: Es existiert genau eine gerade Primzahl.
|
||||
|
||||
"
|
||||
|
||||
Statement "" : True := by
|
||||
trivial
|
||||
|
||||
Conclusion
|
||||
"
|
||||
"
|
||||
|
||||
NewTactic ring
|
||||
@ -1 +0,0 @@
|
||||
-- tauto is not implemented yet... duper?
|
||||
@ -1 +0,0 @@
|
||||
-- not implemented yet
|
||||
@ -1,18 +0,0 @@
|
||||
import Adam.Metadata
|
||||
|
||||
|
||||
-- -- INCORPORATED
|
||||
-- example (A B : Prop) : (A → B) ↔ (¬ B → ¬A) := by
|
||||
-- constructor
|
||||
-- intro h nb
|
||||
-- by_contra
|
||||
-- have : B
|
||||
-- apply h
|
||||
-- assumption
|
||||
-- contradiction
|
||||
-- intro h a
|
||||
-- by_contra
|
||||
-- have : ¬ A
|
||||
-- apply h
|
||||
-- assumption
|
||||
-- contradiction
|
||||
@ -1,41 +0,0 @@
|
||||
import Adam.Levels.LinearAlgebra.L01_Module
|
||||
import Adam.Levels.LinearAlgebra.L02_VectorNotation
|
||||
import Adam.Levels.LinearAlgebra.L03_VectorNotation
|
||||
import Adam.Levels.LinearAlgebra.L04_Submodule
|
||||
import Adam.Levels.LinearAlgebra.L05_Submodule
|
||||
import Adam.Levels.LinearAlgebra.L06_Span
|
||||
import Adam.Levels.LinearAlgebra.L07_Span
|
||||
import Adam.Levels.LinearAlgebra.L08_GeneratingSet
|
||||
|
||||
import Adam.Levels.LinearAlgebra.M01_LinearMap
|
||||
import Adam.Levels.LinearAlgebra.M02_LinearIndep
|
||||
import Adam.Levels.LinearAlgebra.M04_Basis
|
||||
|
||||
import Adam.Levels.LinearAlgebra.N01_Span
|
||||
import Adam.Levels.LinearAlgebra.N02_Span
|
||||
import Adam.Levels.LinearAlgebra.N03_Idempotent
|
||||
import Adam.Levels.LinearAlgebra.N04_Idempotent
|
||||
import Adam.Levels.LinearAlgebra.N05_Sum
|
||||
import Adam.Levels.LinearAlgebra.N06_Sum
|
||||
import Adam.Levels.LinearAlgebra.N07_Prod
|
||||
import Adam.Levels.LinearAlgebra.N08_Prod
|
||||
import Adam.Levels.LinearAlgebra.N09_Prod
|
||||
|
||||
Game "Adam"
|
||||
World "Module"
|
||||
Title "Vektorraum"
|
||||
|
||||
Introduction "Hier lernst du die Grundlagen zur linearen Algebra.
|
||||
|
||||
Vektorräume sind in Lean etwas algemeiner definiert als dies normalerweise in
|
||||
einer Einführungsvorlesung antrifft: Man definiert ein \"Modul\" (Plural: Moduln)
|
||||
über einem Ring. Ein Modul über einem *Körper* wird dann auch \"Vektorraum\" genannt.
|
||||
"
|
||||
|
||||
Game "Adam"
|
||||
World "Basis"
|
||||
Title "Lineare Abbildungen"
|
||||
|
||||
Game "Adam"
|
||||
World "Module2"
|
||||
Title "Mehr Vektorräume"
|
||||
@ -1,24 +0,0 @@
|
||||
import Adam.Metadata
|
||||
|
||||
import Adam.Options.MathlibPart
|
||||
|
||||
Game "Adam"
|
||||
World "Module2"
|
||||
Level 1
|
||||
|
||||
open Submodule
|
||||
|
||||
-- Verpackungswahn 1a)
|
||||
Title "Verpackungswahn"
|
||||
|
||||
Introduction
|
||||
"
|
||||
|
||||
"
|
||||
|
||||
Statement
|
||||
""
|
||||
{K V : Type _} [Field K] [AddCommMonoid V] [Module K V] (M : Set V) :
|
||||
span K ↑(span K M) = span K M := by
|
||||
apply Submodule.span_eq
|
||||
-- or : simp
|
||||
@ -1,38 +0,0 @@
|
||||
import Adam.Metadata
|
||||
|
||||
import Adam.Options.MathlibPart
|
||||
|
||||
open Submodule
|
||||
|
||||
Game "Adam"
|
||||
World "Module2"
|
||||
Level 2
|
||||
|
||||
Title "Lineare Abbildung"
|
||||
|
||||
Introduction
|
||||
"
|
||||
(Verpackungswahn)
|
||||
If `f` is a function and `M` a subset of its domain, then
|
||||
`f '' M` or `set.image f M` is the notation for the image, which is
|
||||
usally denoted `f(M) = {y | ∃ x ∈ M, f(x) = y}` in mathematical texts.
|
||||
"
|
||||
|
||||
-- TODO: This is blocked by
|
||||
-- https://github.com/leanprover/lean4/issues/2074
|
||||
|
||||
set_option autoImplicit false
|
||||
-- set_option pp.all true
|
||||
|
||||
Statement
|
||||
"" : True := by
|
||||
sorry
|
||||
|
||||
-- example {K V W : Type} [Field K] [AddCommMonoid V] [AddCommMonoid W]
|
||||
-- [Module K V] [Module K W] (M : Set V) (f : V →ₗ[K] W) :
|
||||
-- f '' span K M = @span K (f '' M) := by
|
||||
-- sorry
|
||||
|
||||
-- example {K V : Type} [Field K] [AddCommMonoid V]
|
||||
-- [Module K V] (M : Set V) (f : V →ₗ[K] V) : f '' M = f '' M = := by
|
||||
-- rfl
|
||||
@ -1,31 +0,0 @@
|
||||
import Adam.Metadata
|
||||
|
||||
import Adam.Options.MathlibPart
|
||||
|
||||
Game "Adam"
|
||||
World "Module2"
|
||||
Level 4
|
||||
|
||||
Title "Lineare Abbildung"
|
||||
|
||||
Introduction
|
||||
"
|
||||
|
||||
"
|
||||
|
||||
Statement
|
||||
""
|
||||
{R V : Type _} [Semiring R] [AddCommGroup V] [Module R V]
|
||||
(p : V →ₗ[R] V)(h : p ∘ p = p) : LinearMap.ker p ⊓ LinearMap.range p = ⊥ := by
|
||||
sorry
|
||||
-- rw eq_bot_iff,
|
||||
-- intros v hv,
|
||||
-- rw submodule.mem_bot,
|
||||
-- rw submodule.mem_inf at hv,
|
||||
-- cases hv.2 with w hw,
|
||||
-- rw ←hw,
|
||||
-- rw ←h,
|
||||
-- change p (p w) = _,
|
||||
-- rw hw,
|
||||
-- rw ←linear_map.mem_ker,
|
||||
-- exact hv.1,
|
||||
@ -1,4 +0,0 @@
|
||||
- `trivial` uses a bunch of other tactics:
|
||||
(contradiction, assumption, rfl, decide, True.intro, And.intro)
|
||||
so it's maybe not a good candidate to introduce at the beginning of the level.
|
||||
- Ringschluss (tfae) is not in mathlib4 yet.
|
||||
@ -1,2 +0,0 @@
|
||||
import Adam.Levels.Numbers.L01_PNat
|
||||
import Adam.Levels.Numbers.L02_PNat
|
||||
@ -1,44 +0,0 @@
|
||||
import Adam.Levels.Predicate.L01_Ring
|
||||
import Adam.Levels.Predicate.L02_Rewrite
|
||||
import Adam.Levels.Predicate.L03_Rewrite
|
||||
import Adam.Levels.Predicate.L04_Ring
|
||||
import Adam.Levels.Predicate.L05_Rfl
|
||||
import Adam.Levels.Predicate.L06_Exists
|
||||
import Adam.Levels.Predicate.L07_Exists
|
||||
import Adam.Levels.Predicate.L08_Forall
|
||||
import Adam.Levels.Predicate.L09_PushNeg
|
||||
|
||||
Game "Adam"
|
||||
World "Predicate"
|
||||
Title "Quantus"
|
||||
|
||||
Introduction "Auf dem Schwestermond Quantus erwartet Euch bereits ein großer Ansammlung von Formalosopheninnen. Sie reden alle wild durcheinander und Ihr habt Probleme, Euch überhaupt Gehör zu verschaffen. Robo produziert schließlich ein lautes Gong-Geräusch, das sie kurzzeitig zur Ruhe bringt.
|
||||
|
||||
**Du**: Wir haben einen Brief für Eure Königin. Könntet Ihr uns zu Eurer Königin führen?
|
||||
|
||||
**Alle** *(im Chor)*: Wir sind schon alle hier!
|
||||
|
||||
**Du**: Ok. Und wer von Euch ist die Königin?
|
||||
|
||||
Nun herrscht betretenes Schweigen. Alle zucken mit den Schultern.
|
||||
|
||||
**Du**: Habt Ihr überhaupt eine Königin?
|
||||
|
||||
**Alle** *(im Chor)*: Ja, ja. Wir haben eine Königen, wir haben eine Königen.
|
||||
|
||||
**Robo** *(zu dir)*: Ich fasse mal zusammen. Es existiert eine Königen, aber keiner weiß, wer sie ist …
|
||||
|
||||
**Du**: Ist das nicht ein Widerspruch?
|
||||
|
||||
**Robo**: Fragst du, du als Mathematiker? Nein, das ist kein Widerspruch. Das ist einfach eine „reine Existenzaussage“.
|
||||
|
||||
Du bist dir nicht ganz sicher, wie ernst er das meint.
|
||||
|
||||
**Du**: Dann ich schlage vor, wir übergeben das Päckchen einfach an *alle* Bewohner. Dann haben wir es ja insbesondere der Königin übergeben.
|
||||
|
||||
**Du** *(in die Menge*): Wir haben Euch ein Päckchen von Implis gebracht. Hier, das ist für Euch.
|
||||
|
||||
Robo spuckt es aus, wirft es in die Menge, und die Formalosophinnen reißen es auf. Darin befinden sich ein paar loser Seiten, die sie sofort eingehend studieren.
|
||||
|
||||
Zwei Minuten später liegen die Seiten wieder bei Euch. Es sind wieder mathematische Probleme. Und die Formalosophinnen wollen sehen, wie Ihr sie löst.
|
||||
"
|
||||
@ -1,32 +0,0 @@
|
||||
import Adam.Metadata
|
||||
import Adam.Options.MathlibPart
|
||||
|
||||
Game "Adam"
|
||||
World "Predicate"
|
||||
Level 5
|
||||
|
||||
Title "Definitionally equal"
|
||||
|
||||
Introduction
|
||||
"
|
||||
Beim nächsten Problem bekommt ihr ausnahmsweise Hilfe vom Publikum.
|
||||
|
||||
**Alle**: `rfl`, `rfl`, …
|
||||
"
|
||||
|
||||
Statement : 1 + 1 = 2 := by
|
||||
Hint "**Du**: Wieso nicht `ring`?
|
||||
|
||||
**Robo**: Klar, `ring` würde normalerweise auch funktioneren. Aber ich würde mich hier dem Mehrheitswillen beugen …"
|
||||
rfl
|
||||
|
||||
OnlyTactic rfl
|
||||
|
||||
Conclusion
|
||||
"
|
||||
**Robo**: Der Grund, warum hier ausnahmsweise auch mal `rfl` funktioniert hat, ist, dass auf beiden Seiten tatsächlich *per Definition* dasselbe steht. Das soll heißen, wenn man links in `1 + 1` die Definition von `1` und `+ 1` einsetzt, und rechts die Definition von `2`, dann erhält man *buchstäblich* dasselbe (nämlich `(0.succ).succ`).
|
||||
|
||||
**Du**: Na schön. Muss ich mir jetzt diese Definition von `2` merken?
|
||||
|
||||
**Robo**: Ich glaube eher nicht.
|
||||
"
|
||||
@ -1,11 +0,0 @@
|
||||
import Adam.Levels.Prime.L01_Dvd
|
||||
-- import Adam.Levels.Prime.L04_Prime
|
||||
-- import Adam.Levels.Prime.L05_Prime
|
||||
-- import Adam.Levels.Prime.L06_ExistsUnique
|
||||
|
||||
Game "Adam"
|
||||
World "Prime"
|
||||
Title "Teilbarkeit"
|
||||
|
||||
Introduction "Ihr schlendert durch die Befestigung ohne direktes Ziel. Und sprecht mit
|
||||
verschiedenen Einwohnern."
|
||||
Some files were not shown because too many files have changed in this diff Show More
Loading…
Reference in New Issue