1. World 1: One Coin
A coin shows true with probability p and false with probability 1 - p, for any p, as in
Lean, where a coin is a random Bool. Its
distribution is drawn as two columns of sand. A move applies a map f to the outcome: the sand
of each outcome flows to its image, and where several outcomes have the same image, their sand piles
up. What you get is the distribution of f(X), the image measure P \circ f^{-1}:
P(f(X) = b) = P(X \in f^{-1}(\{b\})). Tap a column to see where its sand came from.
Bring the sand into the shape of the target, drawn on the right (and dashed on the board when it
lives on the same space). The masses are p and 1 - p; the picture shows them for an example
p, which the slider changes.
Eine Münze zeigt true mit Wahrscheinlichkeit p und false mit Wahrscheinlichkeit 1 - p, für
ein beliebiges p, wie in Lean, wo eine Münze ein zufälliges Bool ist. Ihre Verteilung ist als zwei Säulen aus Sand gezeichnet. Ein Zug wendet eine
Abbildung f auf das Ergebnis an: Der Sand jedes Ergebnisses fließt zu seinem Bild, und wo mehrere
Ergebnisse dasselbe Bild haben, häuft er sich. Was herauskommt, ist die Verteilung von f(X), das
Bildmaß P \circ f^{-1}: P(f(X) = b) = P(X \in f^{-1}(\{b\})). Tippe eine Säule an, um zu
sehen, woher ihr Sand kommt.
Bring den Sand in die Form des Ziels, das rechts gezeichnet ist (und gestrichelt auf dem Spielfeld,
wenn es auf demselben Raum lebt). Die Massen sind p und 1 - p; das Bild zeigt sie für ein
Beispiel-p, das der Schieberegler ändert.
Flip the coin. not makes true into false and false into true: the two columns swap.
Dreh die Münze um. not macht aus true false und aus false true: Die beiden Säulen tauschen.
Now the proof. What the board showed, now in Lean, for every p. In Lean the coin is coin p,
and f <$> μ is the image measure of μ under f: the move f applied to the distribution μ;
σ p is 1 - p, and p : I says that p lies in the unit interval I = [0, 1]. Below is the
goal, what is to be shown.
The first rule of the game is coin_not : not <$> coin p = coin (σ p): flipping swaps the masses.
The tactic rw [coin_not] rewrites the goal with it: it replaces the left side of the rule by its
right side. When both sides of the goal are then the same, the goal is closed. Type it (or tap
coin_not in the inventory) and press Run.
Jetzt der Beweis. Was das Spielfeld gezeigt hat, jetzt in Lean, für jedes p. In Lean ist die
Münze coin p, und f <$> μ ist das Bildmaß von μ unter f: der Zug f, angewandt auf die
Verteilung μ; σ p ist 1 - p, und p : I sagt, dass p im Einheitsintervall I = [0, 1] liegt. Unten
steht das Ziel, also das, was zu zeigen ist.
Die erste Regel des Spiels ist coin_not : not <$> coin p = coin (σ p): Umdrehen tauscht die
Massen. Die Taktik rw [coin_not] schreibt das Ziel damit um: Sie ersetzt die linke Seite der
Regel durch ihre rechte. Sind danach beide Seiten des Ziels gleich, ist das Ziel erledigt. Tippe sie
ein (oder tippe coin_not im Inventar an) und drücke Ausführen.
Always true. A constant map sends both outcomes to the same point: all the sand flows together.
The result is sure, a point mass (Dirac measure).
Immer true. Eine konstante Abbildung schickt beide Ergebnisse auf denselben Punkt: Der ganze Sand
fließt zusammen. Das Ergebnis ist sicher, eine Punktmasse (Dirac-Maß).
pure b is the point mass at b, and fun _ => true is the constant map. The new rule
coin_const : (fun _ => b) <$> coin p = pure b says what the board showed: all the sand flows to
one point.
pure b ist die Punktmasse in b, und fun _ => true ist die konstante Abbildung. Die neue
Regel coin_const : (fun _ => b) <$> coin p = pure b sagt, was das Spielfeld gezeigt hat: Der ganze
Sand fließt zu einem Punkt.
Surely false, but there is no “always false”. Two moves one after the other: the image measure of
the image measure is the image measure of the composition, (P \circ f^{-1}) \circ g^{-1} = P \circ (g \circ f)^{-1}.
Sicher false, aber es gibt kein „immer false“. Zwei Züge nacheinander: Das Bildmaß des Bildmaßes ist
das Bildmaß der Verkettung, (P \circ f^{-1}) \circ g^{-1} = P \circ (g \circ f)^{-1}.
Two new tools. The rule map_pure : f <$> pure a = pure (f a): a move on a point mass moves the
point. And the tactic rfl, which closes a goal whose two sides are the same after computing: !true
is false.
Tip. rw [coin_const], then rw [map_pure] (or both at once: rw [coin_const, map_pure]), then
rfl.
Zwei neue Werkzeuge. Die Regel map_pure : f <$> pure a = pure (f a): Ein Zug auf einer
Punktmasse verschiebt den Punkt. Und die Taktik rfl, die ein Ziel schließt, dessen beide Seiten
nach Ausrechnen gleich sind: !true ist false.
Tipp. rw [coin_const], dann rw [map_pure] (oder beides auf einmal: rw [coin_const, map_pure]),
dann rfl.
From sides to numbers. Bool.toNat counts true as 1 and false as 0: the distribution
moves to the natural numbers. This is how a coin becomes a random number.
Von Seiten zu Zahlen. Bool.toNat zählt true als 1 und false als 0: Die Verteilung
wandert zu den natürlichen Zahlen. So wird aus einer Münze eine Zufallszahl.
Bool.toNat counts true as 1 and false as 0. Both sides move the same coin, with two
maps that agree. Three new tactics: congr 1 reduces the goal to the two maps being equal;
funext b to their being equal at every b; cases b splits into the cases false and true, two
goals, one after the other.
Tip. congr 1, funext b, cases b, rfl, rfl.
Bool.toNat zählt true als 1 und false als 0. Beide Seiten bewegen dieselbe Münze, mit
zwei Abbildungen, die übereinstimmen. Drei neue Taktiken: congr 1 führt das Ziel darauf zurück,
dass die beiden Abbildungen gleich sind; funext b darauf, dass sie an jeder Stelle b gleich sind;
cases b teilt in die Fälle false und true, zwei Ziele, eines nach dem anderen.
Tipp. congr 1, funext b, cases b, rfl, rfl.
The order matters. Once the coin has become a number, it cannot be flipped any more.
Die Reihenfolge zählt. Ist die Münze erst eine Zahl, lässt sie sich nicht mehr umdrehen.
Nothing new: rw also finds the left side of a rule inside a bigger term.
Nichts Neues: rw findet die linke Seite einer Regel auch in einem größeren Term.
A bet. true wins 5 euros, false loses 2. The image measure is the distribution of your gain.
Eine Wette. Bei true gewinnst du 5 Euro, bei false verlierst du 2. Das Bildmaß ist die Verteilung
deines Gewinns.
The bet is 7 \cdot (\text{the coin as a number}) - 2. The new rule
map_map : g <$> (f <$> μ) = (fun x => g (f x)) <$> μ: two moves are one move.
Tip. rw [map_map], then as in level 4.
Die Wette ist 7 \cdot (\text{die Münze als Zahl}) - 2. Die neue Regel
map_map : g <$> (f <$> μ) = (fun x => g (f x)) <$> μ: Zwei Züge sind ein Zug.
Tipp. rw [map_map], dann wie in Level 4.
A better bet. Make winning the likely outcome.
Eine bessere Wette. Mach den Gewinn zum wahrscheinlichen Ausgang.
The better bet is the bet on the flipped coin: 1 - p instead of p.
Die bessere Wette ist die Wette auf die umgedrehte Münze: 1 - p statt p.
Surely zero. A point mass on the numbers, however you get there.
Sicher null. Eine Punktmasse auf den Zahlen, egal auf welchem Weg.
World 1 in one proof.
Welt 1 in einem Beweis.