Logic in Lean, example sheet 5 : "iff" (↔) #

We learn about how to manipulate P ↔ Q in Lean.

Tactics #

You'll need to know about the tactics from the previous sheets, and also the following two new tactics:

• refl
• rw

The refl tactic #

If your goal is P ↔ P then refl, will solve it.

The rw tactic #

If h : P ↔ Q is a hypothesis, you can decompose it using cases h with hPQ hQP,. However, if you keep it around then you can do rw h, which changes all Ps in the goal to Qs. Variant: rw h at h2, will change all Ps to Qs in hypothesis h2.