Tactic Trainer🔗

Here you prove with tactics only, as in Lean, but still on the board. Tap a red circle (a goal) or a blue dot (something you have): the tactics that fit appear beside it, and each one puts its block in, already connected. A tapped goal also shows, below the board, what you have there, as Lean shows it: h₁ : A ∧ B ⊢ B ∧ A.

Hier beweist du nur mit Taktiken, wie in Lean, aber weiter auf dem Spielfeld. Tippe einen roten Kreis (ein Ziel) oder einen blauen Punkt (etwas, das du hast) an: Daneben erscheinen die Taktiken, die passen, und jede setzt ihren Baustein ein, schon verbunden. Bei einem angetippten Ziel steht unter dem Spielfeld außerdem, was du dort hast, so wie Lean es zeigt: h₁ : A ∧ B ⊢ B ∧ A.

exact: the goal is exactly something you have.

exact: Das Ziel ist genau etwas, das du hast.

exact h₂ — when the goal is exactly one of the things you have. Tap the goal B (the red circle at the bottom): it offers exact h₂, because h₂ : B. On the board this is just a line from h₂ to the goal. In Lean the goal is then closed.

exact h₂ — wenn das Ziel genau eines der Dinge ist, die du hast. Tippe das Ziel B an (den roten Kreis unten): Es bietet exact h₂ an, denn h₂ : B. Auf dem Spielfeld ist das einfach eine Linie von h₂ zum Ziel. In Lean ist das Ziel damit erledigt.

constructor: split a goal A ∧ B in two.

constructor: ein Ziel A ∧ B in zwei zerlegen.

constructor — for a goal A ∧ B. It puts in an ∧I block, which proves A ∧ B from two inputs, A and B: one goal becomes two red circles. In Lean, constructor leaves two goals, A and B, one after the other (in a proof written out, each starts with ·).

constructor — für ein Ziel A ∧ B. Es setzt einen ∧I-Baustein ein, der A ∧ B aus zwei Eingängen A und B beweist: Aus einem Ziel werden zwei rote Kreise. In Lean hinterlässt constructor zwei Ziele, A und B, eines nach dem anderen (in einem ausgeschriebenen Beweis beginnt jedes mit ·).

obtain: take apart what you have.

obtain: zerlegen, was du hast.

obtain ⟨h₂, h₃⟩ := h₁ — for something you have, h₁ : A ∧ B. Tap the blue dot of h₁: it puts in an ∧E block, which gives you its two parts, h₂ : A and h₃ : B, as two new blue dots. Unlike constructor, it works on what you have, not on the goal.

obtain ⟨h₂, h₃⟩ := h₁ — für etwas, das du hast, h₁ : A ∧ B. Tippe den blauen Punkt von h₁ an: Es setzt einen ∧E-Baustein ein, der dir die beiden Teile h₂ : A und h₃ : B als zwei neue blaue Punkte gibt. Anders als constructor wirkt es auf das, was du hast, nicht auf das Ziel.

intro: to prove A → B, assume A.

intro: Um A → B zu beweisen, nimm A an.

intro h₁ — for a goal A → B. It puts in an →I block: you get h₁ : A (the blue dot with the purple ring), and the goal becomes B. You may use h₁ only for this goal; below the board, a tapped goal shows what you have there.

intro h₁ — für ein Ziel A → B. Es setzt einen →I-Baustein ein: Du bekommst h₁ : A (den blauen Punkt mit lila Ring), und das Ziel wird B. Du darfst h₁ nur für dieses Ziel verwenden; unter dem Spielfeld zeigt ein angetipptes Ziel, was du dort hast.

apply: work backwards from the goal.

apply: vom Ziel aus rückwärts arbeiten.

apply h₁ — when the goal is B and you have h₁ : A → B. It puts in an →E block, which gives B once you prove A: the goal becomes A.

apply h₁ — wenn das Ziel B ist und du h₁ : A → B hast. Es setzt einen →E-Baustein ein, der B liefert, sobald du A bewiesen hast: Das Ziel wird A.

intro and apply together.

intro und apply zusammen.

left and right: choose a side.

left und right: eine Seite wählen.

left and right — for a goal A ∨ B. left puts in ∨I₁ and leaves the goal A, right puts in ∨I₂ and leaves B. Choose the side you can prove.

left und right — für ein Ziel A ∨ B. left setzt ∨I₁ ein und lässt das Ziel A, right setzt ∨I₂ ein und lässt B. Wähle die Seite, die du beweisen kannst.

obtain on A ∨ B: two cases.

obtain bei A ∨ B: zwei Fälle.

obtain (h₂ | h₃) := h₁ — for h₁ : A ∨ B. It puts in an ∨E block with two cases: in the first you have h₂ : A, in the second h₃ : B, and in each the goal is the same as before. Each case has its own box: tap the goal of one case, and below the board you see what you have there; the hypothesis of the other case is dimmed.

obtain (h₂ | h₃) := h₁ — für h₁ : A ∨ B. Es setzt einen ∨E-Baustein mit zwei Fällen ein: Im ersten hast du h₂ : A, im zweiten h₃ : B, und in beiden ist das Ziel dasselbe wie vorher. Jeder Fall hat seinen eigenen Kasten: Tippe das Ziel eines Falls an, und unter dem Spielfeld siehst du, was du dort hast; die Annahme des anderen Falls ist ausgegraut.

exfalso: prove ⊥ instead.

exfalso: stattdessen ⊥ beweisen.

exfalso — for any goal. It puts in a ⊥E block: from ⊥ anything follows, so the goal becomes ⊥. That pays off when what you have contradicts itself, like A and A → ⊥ here.

exfalso — für jedes Ziel. Es setzt einen ⊥E-Baustein ein: Aus ⊥ folgt alles, also wird das Ziel ⊥. Das lohnt sich, wenn sich widerspricht, was du hast, wie hier A und A → ⊥.

by_contra: assume the opposite.

by_contra: das Gegenteil annehmen.

by_contra h₂ — for any goal A. It puts in an RAA block: you get h₂ : A → ⊥ (that is, ¬A), and the goal becomes ⊥. If the opposite of A leads to a contradiction, A holds.

by_contra h₂ — für jedes Ziel A. Es setzt einen RAA-Baustein ein: Du bekommst h₂ : A → ⊥ (also ¬A), und das Ziel wird ⊥. Führt das Gegenteil von A zu einem Widerspruch, dann gilt A.