Logic in Lean, example sheet 1 : "implies" (→) #

We learn about propositions, and implications P → Q between them. You can get this arrow by typing \to or \r. Mathematicians usually write the implication arrow as P ⇒ Q but Lean prefers a single arrow.

The absolute basics #

P : Prop means that P is a true-false statement. h : P means that h is a proof that P is true, or you can regard h as an assumption that P is true; logically these are the same. Stuff above the ⊢ symbol is your assumptions. The statement to the right of it is the goal. Your job is to prove the goal from the assumptions.

Tactics you will need #

To solve the levels on this sheet you will need to know how to use the following tactics:

• intro
• exact
• apply

The intro tactic #

Mathematical background: intro h, says "To prove P → Q, you can assume that P is true (call this assumption h) and then it suffices to prove Q."

Lean: If your goal is ⊢ P → Q then intro h, will introduce a hypothesis h : P (i.e. a hypothesis that P is true) and change the goal to ⊢ Q.

The exact tactic #

Mathematics: If you have an assumption h that P is true, and your goal is to prove that P is true, then exact h, will solve this goal.

Lean: If your goal is ⊢ P and you have a hypothesis h : P then exact h, will solve it.

The apply tactic #

Mathematics: apply is arguing backwards. It is like "it suffices to...". If you're trying to prove Q, and you know h : P → Q is true, then it suffices to prove P. So apply h, changes the goal from Q to P. The key point to remember is that apply h will only work when h is an implication, and it will only work when the conclusion of h matches the goal.

Lean: If your goal is ⊢ Q and you have h : P → Q then apply h, will change the goal to ⊢ P.