7. World 7: Rewriting🔗

Equivalent statements may replace each other: from ?1 ↔ ?2, a statement with ?1 in it is equivalent to the same statement with ?2 there. Four new blocks:

↔rfl: ?1 ↔ ?1.
↔sym: from ?1 ↔ ?2, ?2 ↔ ?1.
rw: from ?1 ↔ ?2 and a statement with ?2 (?3 ?2), the same statement with ?1 (?3 ?1). ?3 is the goal with a hole: the block finds it when you connect it to a goal.
rw←: the same backwards, from a statement with ?1, the one with ?2.

Äquivalente Aussagen dürfen einander ersetzen: Aus ?1 ↔ ?2 folgt, dass eine Aussage mit ?1 darin äquivalent ist zu derselben Aussage mit ?2 an dieser Stelle. Vier neue Bausteine:

↔rfl: ?1 ↔ ?1.
↔sym: aus ?1 ↔ ?2 folgt ?2 ↔ ?1.
rw: aus ?1 ↔ ?2 und einer Aussage mit ?2 (?3 ?2) dieselbe Aussage mit ?1 (?3 ?1). ?3 ist das Ziel mit einem Loch: Der Baustein findet es, wenn du ihn mit einem Ziel verbindest.
rw←: dasselbe rückwärts, aus einer Aussage mit ?1 die mit ?2.

A statement is equivalent to itself: ↔rfl. In world 6 this took ↔I and two →I.

Eine Aussage ist zu sich selbst äquivalent: ↔rfl. In Welt 6 brauchte das noch ↔I und zwei →I.

↔rfl: ?1 ↔ ?1, for any statement ?1. In Lean: Iff.rfl.

↔rfl: ?1 ↔ ?1, für jede Aussage ?1. In Lean: Iff.rfl.

Turn it round: ↔sym.

Umdrehen: ↔sym.

↔sym: from ?1 ↔ ?2, ?2 ↔ ?1. In Lean: Iff.symm.

↔sym: aus ?1 ↔ ?2 folgt ?2 ↔ ?1. In Lean: Iff.symm.

Rewriting: equivalent statements may replace each other. With rw, A ↔ B makes the goal A into B.

Umschreiben: Äquivalente Aussagen dürfen einander ersetzen. Mit rw macht A ↔ B aus dem Ziel A das Ziel B.

rw: from ?1 ↔ ?2 and the statement with ?2 (?3 ?2), the statement with ?1 (?3 ?1); ?3 is the goal with a hole.

rw: aus ?1 ↔ ?2 und der Aussage mit ?2 (?3 ?2) die Aussage mit ?1 (?3 ?1); ?3 ist das Ziel mit einem Loch.

Backwards: With rw←, A ↔ B makes the goal B into A.

Rückwärts: Mit rw← macht A ↔ B aus dem Ziel B das Ziel A.

rw←: from ?1 ↔ ?2 and the statement with ?1 (?3 ?1), the statement with ?2 (?3 ?2).

rw←: aus ?1 ↔ ?2 und der Aussage mit ?1 (?3 ?1) die Aussage mit ?2 (?3 ?2).

rw also works inside a statement. A goal that becomes X ↔ X is done at once.

rw wirkt auch innerhalb einer Aussage. Ein Ziel, das dabei zu X ↔ X wird, ist sofort erledigt.

The same behind an implication.

Dasselbe hinter einer Implikation.

Two steps: rewrite, then what is left.

Zwei Schritte: umschreiben, dann den Rest.

Make the goal fit what you have.

Bring das Ziel in die Form dessen, was du hast.

Equivalent statements have equivalent negations.

Äquivalente Aussagen haben äquivalente Verneinungen.

A chain of equivalences.

Eine Kette von Äquivalenzen.

After the rewriting, the goal is a conjunction.

Nach dem Umschreiben ist das Ziel eine Konjunktion.

Every B at once.

Jedes B auf einmal.

The final level: one rewriting replaces every A.

Das letzte Level: Ein Umschreiben ersetzt jedes A.