Seminar 2 – ✨apply✨

Summary

We worked on exercises 2.3-2.5 today, where the most important new tactic is apply.

Apply and implication, backward reasoning

We can use the apply tactic to prove our goals with backwards reasoning. For example, suppose that you have the following in your Lean InfoView:

h1: A → B
⊢ B

then, the line

apply h1

results in

h1: A → B
⊢ A

If we can prove $A$, then we know by h1 that we have a proof for $B$, too.

We often have theorems that consist of multiple implications. For example, suppose that your Lean InfoView looks like

h1: A → B → C
⊢ C

Note that $A \to B \to C$ has implicit brackets, and is short for $A \to (B \to C)$. The line

apply h1

result in two goals:

h1: A → B → C
⊢ A
⊢ B

Note that if we can show that $A \land B$ is true, we know that $C$ is true by h1. to prove $A$ and $B$ separately, you can type . at the start of each case, which will be replaced by ·. If $A$ and $B$ have the same proof, you can also type <;> and provide the simultaneous proof afterwards.

Apply and implication, forward reasoning

We can also use apply to rewrite a hypothesis. Consider an InfoView stating

h1: A → B
h2: A
⊢ whatever

then, we can think as h2 as a proof for $A$, and of $h1$ as an object that maps any proof for $A$ to a proof for $B$. if we run

apply h1 at h2

the InfoView changes to

h1: A → B
h2: B
⊢ whatever

Constructor for logic and

Another useful tactic is constructor. Consider the following InfoView:

⊢ A ∧ B

the tactic constructor will split this goal up into proving $A$ and $B$ separately.

For next week

As a homework for the next time, try to finish section 2 (Basics) entirely. If you run into any problems, we can solve them together at the start of the next seminar.