Logic in Lean, example sheet 2 : true and false #

We learn about the true and false propositions.

Tactics you will need #

To solve the levels on this sheet you will need to know all previous tactics, plus the following two new ones:

• trivial
• exfalso

The trivial tactic #

If your goal is ⊢ true then trivial, will solve it.

The exfalso tactic #

The tactic exfalso, turns any goal ⊢ P into ⊢ false. This is mathematically valid because false implies any goal.