7. World 7: Rewriting🔗

Equivalent statements may replace each other: from A ↔ B, a statement with A in it is equivalent to the same statement with B there. In Lean this is rw. Four new blocks:

↔rfl: A ↔ A.
↔sym: from A ↔ B, B ↔ A.
rw: from A ↔ B and a statement with B (?3 ?2), the same statement with A (?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 A, the one with B.

Äquivalente Aussagen dürfen einander ersetzen: Aus A ↔ B folgt, dass eine Aussage mit A darin äquivalent ist zu derselben Aussage mit B an dieser Stelle. In Lean ist das rw. Vier neue Bausteine:

↔rfl: A ↔ A.
↔sym: aus A ↔ B folgt B ↔ A.
rw: aus A ↔ B und einer Aussage mit B (?3 ?2) dieselbe Aussage mit A (?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 A die mit B.

A statement is equivalent to itself: rfl. In world 6 this took ↔I (in Lean constructor) and two →I.

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

rfl (↔rfl): A ↔ A, for any statement A.

rfl (↔rfl): A ↔ A, für jede Aussage A.

Turn it round: symm.

Umdrehen: symm.

symm (↔sym): from A ↔ B, B ↔ A. For a goal B ↔ A it leaves the goal A ↔ B.

symm (↔sym): aus A ↔ B folgt B ↔ A. Bei einem Ziel B ↔ A bleibt das Ziel A ↔ B.

Rewriting: equivalent statements may replace each other. rw [h₁] makes the goal A into B.

Umschreiben: Äquivalente Aussagen dürfen einander ersetzen. rw [h₁] macht aus dem Ziel A das Ziel B.

rw [h] (rw), for h : A ↔ B: in the goal, every A becomes B. As a block: from A ↔ B and the statement with B (?3 ?2), the statement with A (?3 ?1); ?3 is the goal with a hole.

rw [h] (rw), für h : A ↔ B: Im Ziel wird jedes A zu B. Als Baustein: aus A ↔ B und der Aussage mit B (?3 ?2) die Aussage mit A (?3 ?1); ?3 ist das Ziel mit einem Loch.

Backwards: rw [← h₁] makes every B into A.

Rückwärts: rw [← h₁] macht aus jedem B ein A.

rw [← h] (rw←), for h : A ↔ B: in the goal, every B becomes A.

rw [← h] (rw←), für h : A ↔ B: Im Ziel wird jedes B zu A.

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.