2. World 2: Building with Coins
Now you build a circuit. New p-coin lays down a coin, as a line; all coins have the same p and
are independent of each other. Tap one or several lines and then a function: a column takes the
lines with a dot as its inputs, and its result runs on as a new line. A line that a column only
crosses, without a dot, is not used. A coin may go into several functions; then the results depend
on each other, and the game takes that into account. At the end of each line is its distribution,
found by going through all outcomes of the coins it comes from: with two coins, true–true has
mass p^2, true–false p(1 - p), and so on. The circuit, read from left to right, is a
do block in Lean.
Check compares the selected line (or else the newest) with the target, for every p.
Jetzt baust du einen Schaltplan. Neue p-Münze legt eine Münze hin, als Leitung; alle Münzen haben
dasselbe p und sind unabhängig voneinander. Tippe eine oder mehrere Leitungen an und dann eine
Funktion: Eine Spalte nimmt die Leitungen mit einem Punkt als Eingänge, und ihr Ergebnis läuft als
neue Leitung weiter. Eine Leitung, die eine Spalte nur kreuzt, ohne Punkt, wird nicht benutzt. Eine
Münze darf in mehrere Funktionen gehen; dann hängen die Ergebnisse voneinander ab, und das Spiel
berücksichtigt das. Am Ende jeder Leitung steht ihre Verteilung, die sich ergibt, indem man alle
Ausgänge der Münzen durchgeht, aus denen sie kommt: Bei zwei Münzen hat true–true die Masse
p^2, true–false p(1 - p), und so weiter. Der Schaltplan, von links nach rechts gelesen, ist
ein do-Block in Lean.
Prüfen vergleicht die ausgewählte Leitung (sonst die neueste) mit dem Ziel, für jedes p.
Both true. Two coins, and true only when both show true.
Beide true. Zwei Münzen, und true nur, wenn beide true zeigen.
Your circuit, read from left to right, is a do block: let x ← coin p throws a coin and calls
its result x, each ← is a new throw, independent of the others, and pure at the end is the
result. The new rule is independence itself:
coin_and : (do let x ← coin p; let y ← coin q; pure (x && y)) = coin (p * q).
Dein Schaltplan, von links nach rechts gelesen, ist ein do-Block: let x ← coin p wirft eine
Münze und nennt ihr Ergebnis x, jedes ← ist ein neuer Wurf, unabhängig von den anderen, und
pure am Ende ist das Ergebnis. Die neue Regel ist die Unabhängigkeit selbst:
coin_and : (do let x ← coin p; let y ← coin q; pure (x && y)) = coin (p * q).
First true, then false.
Erst true, dann false.
Work backwards, on the right side: rw [← coin_and] uses the rule from right to left, and
rw [← coin_not] turns coin (σ p) into not <$> coin p. Then a move sits inside the do block;
the new rule bind_map_left : (do let x ← f <$> μ; g x) = (do let x ← μ; g (f x)) moves it into
the result. But rw cannot rewrite where the names x, y of a do block occur. The new tactic
simp only [rules] can: it rewrites everywhere, as often as it can, and closes the goal when the two
sides become the same.
Tip. rw [← coin_and], rw [← coin_not], simp only [bind_map_left].
Arbeite rückwärts, auf der rechten Seite: rw [← coin_and] benutzt die Regel von rechts nach
links, und rw [← coin_not] macht aus coin (σ p) ein not <$> coin p. Dann steht ein Zug im
do-Block; die neue Regel bind_map_left : (do let x ← f <$> μ; g x) = (do let x ← μ; g (f x))
schiebt ihn ins Ergebnis. Aber rw kann nicht dort umschreiben, wo die Namen x, y eines
do-Blocks vorkommen. Die neue Taktik simp only [Regeln] kann es: Sie schreibt überall um, so oft
es geht, und schließt das Ziel, wenn beide Seiten gleich werden.
Tipp. rw [← coin_and], rw [← coin_not], simp only [bind_map_left].
At least one true. false only when both show false: (1 - p)^2.
Mindestens einmal true. false nur, wenn beide false zeigen: (1 - p)^2.
At least one true is: not both false, with probability 1 - (1 - p)^2. Two new rules: De
Morgan, or_eq : (x || y) = !(!x && !y), and map_bind : f <$> (do let x ← μ; g x) = (do let x ← μ; f <$> g x):
a move after a do block goes into it.
Tip. On the right side, backwards: rw [← coin_not], rw [← coin_and], rw [← coin_not]; then
simp only [bind_map_left, map_bind, map_pure, or_eq].
Mindestens einmal true heißt: nicht beide false, mit Wahrscheinlichkeit 1 - (1 - p)^2. Zwei
neue Regeln: De Morgan, or_eq : (x || y) = !(!x && !y), und
map_bind : f <$> (do let x ← μ; g x) = (do let x ← μ; f <$> g x): Ein Zug nach einem do-Block
wandert in ihn hinein.
Tipp. Auf der rechten Seite, rückwärts: rw [← coin_not], rw [← coin_and], rw [← coin_not];
dann simp only [bind_map_left, map_bind, map_pure, or_eq].
Surely false, with a single coin. A coin that goes into two functions is the same coin in both:
the results depend on each other.
Sicher false, mit einer einzigen Münze. Eine Münze, die in zwei Funktionen geht, ist in beiden
dieselbe: Die Ergebnisse hängen voneinander ab.
Two new rules: Bool.and_not_self : (x && !x) = false, and
coin_unused : (do let _ ← coin p; ν) = ν: a coin whose result is not used changes nothing.
Tip. simp only [Bool.and_not_self], then rw [coin_unused].
Zwei neue Regeln: Bool.and_not_self : (x && !x) = false, und
coin_unused : (do let _ ← coin p; ν) = ν: Eine Münze, deren Ergebnis nicht benutzt wird, ändert
nichts.
Tipp. simp only [Bool.and_not_self], dann rw [coin_unused].
Exactly one true, without a function for it: at least one, but not both.
Genau einmal true, ohne eine Funktion dafür: mindestens einmal, aber nicht beide.
Exactly one true is xor. Both sides throw the same coins; go under the throws, with congr 1
and funext x (and again for y), and look at all four cases. New: t₁ <;> t₂ runs t₂ on every
goal that t₁ leaves.
Tip. congr 1, funext x, congr 1, funext y, cases x <;> cases y <;> rfl.
Genau einmal true ist xor. Beide Seiten werfen dieselben Münzen; geh unter die Würfe, mit
congr 1 und funext x (und nochmal für y), und sieh dir alle vier Fälle an. Neu: t₁ <;> t₂
führt t₂ auf jedem Ziel aus, das t₁ übrig lässt.
Tipp. congr 1, funext x, congr 1, funext y, cases x <;> cases y <;> rfl.
The number of true. From coins to numbers (0 and 1), and add them: the binomial distribution B(2, p).
Die Anzahl true. Von Münzen zu Zahlen (0 und 1), und addieren: die Binomialverteilung B(2, p).
The binomial distribution binom p n is defined as the natural numbers in the Natural Number Game:
by zero and successor. binom_zero : binom p 0 = pure 0: no throw, no true.
binom_succ : binom p (n + 1) = do let X ← coin p; let Y ← binom p n; pure (X.toNat + Y): one throw
more. To clean up do blocks: bind_assoc (a do block in a do block is one do block),
pure_bind : (do let x ← pure a; f x) = f a, and add_zero : n + 0 = n.
Tip. rw [binom_succ, binom_succ, binom_zero], then simp only [bind_assoc, pure_bind, add_zero].
Die Binomialverteilung binom p n ist definiert wie die natürlichen Zahlen im Natural Number Game:
durch Null und Nachfolger. binom_zero : binom p 0 = pure 0: kein Wurf, kein true.
binom_succ : binom p (n + 1) = do let X ← coin p; let Y ← binom p n; pure (X.toNat + Y): ein Wurf
mehr. Zum Aufräumen von do-Blöcken: bind_assoc (ein do-Block in einem do-Block ist ein
do-Block), pure_bind : (do let x ← pure a; f x) = f a, und add_zero : n + 0 = n.
Tipp. rw [binom_succ, binom_succ, binom_zero], dann simp only [bind_assoc, pure_bind, add_zero].
Boss: the majority of three. true when at least two of three coins show true. Each coin has to
go into two functions.
Boss: die Mehrheit von dreien. true, wenn mindestens zwei von drei Münzen true zeigen. Jede Münze
muss in zwei Funktionen gehen.
Boss. The majority of three is: at least two true, out of three throws. decide (2 ≤ n) is
true when 2 \le n. Everything of this world at once.
Tip. Unfold binom p 3 with binom_succ (three times) and binom_zero; clean up with
simp only [map_bind, bind_assoc, pure_bind, map_pure, add_zero]; then go under the three throws
and look at all eight cases.
Endgegner. Die Mehrheit von dreien heißt: mindestens zweimal true, bei drei Würfen.
decide (2 ≤ n) ist true, wenn 2 \le n. Alles aus dieser Welt auf einmal.
Tipp. Wickle binom p 3 mit binom_succ (dreimal) und binom_zero aus; räume auf mit
simp only [map_bind, bind_assoc, pure_bind, map_pure, add_zero]; dann geh unter die drei Würfe und
sieh dir alle acht Fälle an.