Logic in Lean 2

Continuing from the last post, we will look into proving logic in Lean 4. This time, we will cover three concepts: Equivalence (If and Only If), Conjunction (And), and Disjunction (Or). We are continuing to use the textbook "Introduction to Lean from Scratch: Hands-on Formal Mathematics Library Development."

Equivalence (↔)

Two propositions P and Q are equivalent if both P → Q and Q → P hold true. In Lean 4, this is represented by the ↔ operator.

#eval True ↔ True   -- true
#eval True ↔ False  -- false

The constructor Tactic

To prove P ↔ Q, use the constructor tactic. Applying it splits your goal into two subgoals: "show P → Q" and "show Q → P". You declare the beginning of each subgoal using · (\. + Tab).

example (P Q: Prop) (h1 : P → Q) (h2 : Q → P) : P ↔ Q := by
  constructor
  · apply h1
  · apply h2

case mp / case mpr

Instead of ·, you can use case mp => and case mpr => to explicitly state which goal you are proving. mp (modus ponens direction) corresponds to P → Q, while mpr (reverse direction) corresponds to Q → P.

example (P Q: Prop) (h1 : P → Q) (h2 : Q → P) : P ↔ Q := by
  constructor
  case mp =>
    apply h1
  case mpr =>
    apply h2

Batch Declaration with constructor <;>

Writing constructor <;> allows you to apply the same tactic to both split goals at once. For example, if both proofs require intro h at the beginning, you can write it like this:

-- Apply intro to both goals at once using constructor <;> intro h
example (P Q : Prop) (h1 : P → Q) (h2 : Q → P) : P ↔ Q := by
  constructor <;> intro h
  · exact h1 h
  · exact h2 h

The intro h is applied simultaneously to both goals generated by constructor (P → Q and Q → P), adding h to each context. This is highly convenient for reducing repetition.

The rw (rewrite) Tactic

The rw (rewrite) tactic allows you to rewrite your goal. When you have the hypothesis h : P ↔ Q, you can replace P with Q within your goal using rw [h].

-- Rewrite P to Q in the goal using h : P ↔ Q
example (P Q : Prop) (h : P ↔ Q) (hq : Q) : P := by
  rw [h]
  exact hq

In the example above, applying rw [h] to the goal P rewrites it to Q. You can then close the proof using exact hq.

Conjunction (∧)

A conjunction is a proposition stating that two propositions both hold true at the same time. In Lean 4, it is represented by the ∧ operator.

#eval True ∧ True   -- true
#eval True ∧ False  -- false
#eval False ∧ True  -- false
#eval False ∧ False -- false

The constructor Tactic

You also use the constructor tactic to prove conjunctions. A goal of P ∧ Q splits into two subgoals: "show P" and "show Q".

example (P Q : Prop) (hp : P) (hq : Q) : P ∧ Q := by
  constructor
  · exact hp
  · exact hq

case left / case right

For conjunctions, you specify left and right in your case statements.

example (P Q : Prop) (hp : P) (hq : Q) : P ∧ Q := by
  constructor
  case left =>
    exact hp
  case right =>
    exact hq

Disjunction (∨)

A disjunction is a proposition stating that at least one of two propositions holds true. In Lean 4, it is represented by the ∨ operator.

#eval True ∨ True   -- true
#eval True ∨ False  -- true
#eval False ∨ True  -- true
#eval False ∨ False -- false

The left Tactic / right Tactic

When proving a disjunction P ∨ Q, you use either the left tactic or the right tactic. Use left when you want to prove the left side (P) of the ∨, and right when you want to prove the right side (Q).

-- Prove P ∨ Q using the left side (P)
example (P Q : Prop) (hp : P) : P ∨ Q := by
  left
  exact hp

-- Prove P ∨ Q using the right side (Q)
example (P Q : Prop) (hq : Q) : P ∨ Q := by
  right
  exact hq

The cases Tactic (Using a Disjunction as a Hypothesis)

When you want to use a disjunction as a hypothesis, use the cases tactic. Applying cases h with to a hypothesis h : P ∨ Q branches your proof into two cases: the case where P holds true (inl) and the case where Q holds true (inr).

example (P Q : Prop) (h : P ∨ Q) : Q ∨ P := by
  cases h with
  | inl hp =>
    right
    exact hp
  | inr hq =>
    left
    exact hq

In the example above, we take P ∨ Q as a hypothesis to prove Q ∨ P (the disjunction with its terms swapped). Since inl hp gives us P, we use right to show the right side (P) of the goal Q ∨ P. Conversely, since inr hq gives us Q, we use left to show the left side (Q).

Summary

Here is a summary of the tactics we learned today.