►Logic & Computation
▼Lectures
►Lecture 35:   Proofs with Tactics
On this page:
1 Purpose
2 Outline
3 Re-doing a propositional logic proof
8.11
    contents    up   

Lecture 35: Proofs with Tactics

1 Purpose

More tactics for proofs

2 Outline
3 Re-doing a propositional logic proof

Let’s prove a theorem that you did in Homework 2A:

\neg (P \lor Q) \equiv \neg P \land \neg Q

Here we’ve written \equiv as "if-and-only-if" double implication, rather than propositional equality. Both allow Lean to rewrite.

theorem demorgan1 : forall {P Q : Prop}, ¬(P ∨ Q) ↔ ¬P ∧ ¬Q :=
  by intros P Q
     constructor
     case mp => intro
                constructor
                case left =>
                  intro; apply ‹¬(P ∨ Q)›; apply Or.inl; assumption
                case right =>
                  intro; apply ‹¬(P ∨ Q)›; apply Or.inr; assumption
     case mpr => intro
                 intro
                 cases ‹¬ P ∧ ¬ Q›
                 cases ‹P ∨ Q›
                 case inl => apply ‹¬P›; assumption
                 case inr => apply ‹¬Q›; assumption

Here we used two new tactics:

Tactic Use

Tactic Description

constructor

if the goal is an inductive type, try applying its constructors to see if any match.

apply H

H must be a hypothesis or theorem with type P1 -> P2 -> ... -> PN -> Q, where the goal has type Q. This tactic will replace the goal with N separate goals, P1, through PN, as it corresponds to deciding to prove the premises of H and then using it to prove the goal. In the simply case where you just have P -> Q this will replace Q with P

Interestingly, the other proof that you did:

\neg (P \land Q) \equiv \neg P \lor \neg Q

cannot be done in the core logic of Lean. The issue is that it is not constructive; it can be done if we add classical axioms.

Stepping back: proofs here vs. proofs with truth tables

Now that we’ve seen a few proofs, including doing a proof that you did in propositional logic, it’s important to understand the difference between proofs in Lean and proofs in propositional logic.

In propositional logic, all variables can be either true or false, and thus any formula can be computed via a finite truth table. In a higher order logic like Lean, propositional variables are not either true or false, but rather, they are either provable or not provable. For a statement to be provable, it means that we have constructed a proof term with that type, but that type may involve data of arbitrary size, and thus the truth or falseness of a given statement cannot be determined by a finite truth table. Thus while the proof we just did of one of De Morgan’s laws is syntactically the same as what you did in Homework 2A, it is a much more powerful proof, as it holds for any provable propositions, not just for T/F propositional variables. Another way to think about this is that Lean has propositional logic embedded, by way of the boolean data type. Thus, our proof from Homework 2A was the following:

theorem demorganprop :
  forall {P Q : Bool}, not (or P Q) = and (not P) (not Q) :=
    by intros P Q
       cases P <;> cases Q <;> rfl

Here we can see a new tactic: <;>, which is used to chain tactics together by applying what follows to everything that comes out of the former. Here we can see that by doing case analysis on the two boolean inputs, we can complete the proof trivially, as once we have constants, simply evaluating the expression will give us the result.

Tactic Use

Tactic Description

tactic1 <;> tactic2

Apply tactic1 to the current goal, and then apply tactic2 to all goals that are generated by the result of tactic1 (0, 1, or more).

Attemptying to do that for the other proof will fail, as we cannot do case analysis on Prop: it is not an inductive type with a finite number of constructors.

    contents    up