- [[Gemini 3.5]] prompt: Lean4: explain the match tactic and provide 5 examples of increasing complexity
## Summary
The `match` tactic allows you to perform case analysis and pattern matching on expressions or hypotheses directly within a proof.
While Lean also has term-mode `match` expressions, the tactic-mode `match` follows the exact same pattern-matching syntax (handling inductives, constructors, tuples, booleans, etc.), but expects a **tactic script** inside each branch rather than a direct term.
## Core Syntax
```lean
match expr1, expr2 with
| pattern1, pattern2 =>
-- Tactic script for case 1
| pattern3, pattern4 =>
-- Tactic script for case 2
```
You can also name the discriminant expression using `match h : expr with`. This automatically introduces an equality hypothesis into your context for each branch, stating that the expression equals the pattern being matched.
## 5 Examples of Increasing Complexity
### 1. Basic Boolean Matching
_Complexity: Beginner_
This example performs case analysis on a boolean value `b` to prove a simple logical identity.
```lean
example (b : Bool) : (b && true) = b := by
match b with
| true => rfl
| false => rfl
```
### 2. Natural Numbers (`Nat`) Case Analysis
_Complexity: Elementary_
Here, we match on a natural number `n` to show that it is either zero or the successor of some natural number `k`.
```lean
example (n : Nat) : n = 0 ∨ n > 0 := by
match n with
| 0 =>
left
rfl
| k + 1 =>
right
exact Nat.succ_pos k
```
### 3. Named Discriminants (`match h : e with`)
_Complexity: Intermediate_
When you need to remember _what_ expression you split on, you can bind it to a name and an equality hypothesis `hn`. This is especially useful when hypotheses in your context depend on the value of `n`.
```lean
example (n : Nat) (h : n ≠ 0) : ∃ k, n = k + 1 := by
match hn : n with
| 0 =>
-- hn provides the hypothesis n = 0, which contradicts h : n ≠ 0
contradiction
| k + 1 =>
exact ⟨k, rfl⟩
```
### 4. Multi-Variable Pattern Matching
_Complexity: Advanced_
The `match` tactic can accept multiple discriminants simultaneously. This allows you to check all truth value combinations of two booleans at once, avoiding nested case splits.
```lean
example (b1 b2 : Bool) : (b1 && b2) = (b2 && b1) := by
match b1, b2 with
| true, true => rfl
| true, false => rfl
| false, true => rfl
| false, false => rfl
```
### 5. Destructuring Logical Disjunctions (`Or`)
_Complexity: Expert_
Pattern matching isn't restricted to data types like `Nat` or `Bool`; it also works on propositions like `Or` (`∨`) and `And` (`∧`). Here, we match on a disjunction hypothesis `h` to prove its symmetric counterpart.
```lean
example (p q : Prop) (h : p ∨ q) : q ∨ p := by
match h with
| Or.inl hp =>
-- hp : p
exact Or.inr hp
| Or.inr hq =>
-- hq : q
exact Or.inl hq
```