# 2.4 Disjunction Disjunction represents "or". A proof of `P ∨ Q` contains one piece of evidence: either a proof of `P` or a proof of `Q`, tagged with the side from which it came. In Lean, disjunction behaves like a sum type for propositions. ## Problem You want to prove or use a statement of the form: ```lean P ∨ Q ``` To prove it, you must choose one side and provide a proof of that side. To use it, you must handle both possible cases. ## Solution Use `left` to prove the left side of a disjunction. ```lean theorem make_left_disjunction (P Q : Prop) : P -> P ∨ Q := by intro hp left exact hp ``` Use `right` to prove the right side. ```lean theorem make_right_disjunction (P Q : Prop) : Q -> P ∨ Q := by intro hq right exact hq ``` After `left`, the goal changes from: ```lean ⊢ P ∨ Q ``` to: ```lean ⊢ P ``` After `right`, the goal changes from: ```lean ⊢ P ∨ Q ``` to: ```lean ⊢ Q ``` ## Discussion A conjunction requires both sides. A disjunction requires one side. This makes introduction easy and elimination more careful. If you have a hypothesis: ```lean h : P ∨ Q ``` you cannot simply extract `P` or `Q`. The proof may have come from either side. To use `h`, you must perform case analysis. ```lean theorem disjunction_comm (P Q : Prop) : P ∨ Q -> Q ∨ P := by intro h cases h with | inl hp => right exact hp | inr hq => left exact hq ``` There are two cases. In the first case, Lean gives: ```lean hp : P ⊢ Q ∨ P ``` So the proof chooses the right side. In the second case, Lean gives: ```lean hq : Q ⊢ Q ∨ P ``` So the proof chooses the left side. ## Constructors The two constructors for disjunction are `Or.inl` and `Or.inr`. ```lean theorem disjunction_left_term (P Q : Prop) : P -> P ∨ Q := fun hp => Or.inl hp theorem disjunction_right_term (P Q : Prop) : Q -> P ∨ Q := fun hq => Or.inr hq ``` The constructor names mean "inject left" and "inject right". Their shapes are: ```lean Or.inl : P -> P ∨ Q Or.inr : Q -> P ∨ Q ``` The tactics `left` and `right` are tactic-mode wrappers around these constructors. ## Eliminating a Disjunction To prove a result `R` from `P ∨ Q`, prove `R` in both cases. ```lean theorem disjunction_elim (P Q R : Prop) : (P -> R) -> (Q -> R) -> P ∨ Q -> R := by intro hpr intro hqr intro hpq cases hpq with | inl hp => exact hpr hp | inr hq => exact hqr hq ``` The structure is important. A disjunction gives alternatives. To obtain a single conclusion from alternatives, both alternatives must lead to that conclusion. ## Nested Disjunctions Nested disjunctions require nested case analysis. ```lean theorem disjunction_assoc (P Q R : Prop) : (P ∨ Q) ∨ R -> P ∨ (Q ∨ R) := by intro h cases h with | inl hpq => cases hpq with | inl hp => left exact hp | inr hq => right left exact hq | inr hr => right right exact hr ``` The hypothesis has type: ```lean h : (P ∨ Q) ∨ R ``` The outer disjunction first splits into: ```lean hpq : P ∨ Q ``` or: ```lean hr : R ``` The `hpq` case must then be split again. ## Pattern Matching in `intro` You can destruct a disjunction when it is introduced. ```lean theorem disjunction_comm_intro_pattern (P Q : Prop) : P ∨ Q -> Q ∨ P := by intro h rcases h with hp | hq · right exact hp · left exact hq ``` The `rcases` tactic is often convenient for destructuring disjunctions, conjunctions, existentials, and nested combinations of them. For simple beginner proofs, `cases` is usually clearer because it directly displays the constructors. ## Disjunction with Existing Implications A common pattern is to combine disjunction elimination with implication application. ```lean theorem disjunction_map (P Q R S : Prop) : (P -> R) -> (Q -> S) -> P ∨ Q -> R ∨ S := by intro hpr intro hqs intro hpq cases hpq with | inl hp => left exact hpr hp | inr hq => right exact hqs hq ``` The proof says: if the disjunction was proved from `P`, map that proof to `R`; if it was proved from `Q`, map that proof to `S`. ## Choosing the Correct Side Lean does not choose a side of a disjunction automatically unless automation has enough information. ```lean theorem choose_right (P Q : Prop) (hq : Q) : P ∨ Q := by right exact hq ``` Trying `left` here would leave the goal: ```lean ⊢ P ``` but the context only contains: ```lean hq : Q ``` So the proof would fail unless you also had a proof of `P`. ## Disjunction and False `False` is the empty proposition. A disjunction with `False` can often be simplified by case analysis. ```lean theorem false_or (P : Prop) : False ∨ P -> P := by intro h cases h with | inl hf => cases hf | inr hp => exact hp ``` In the left case, `hf : False`. Since `False` has no constructors, `cases hf` closes the goal. ```lean theorem or_false (P : Prop) : P ∨ False -> P := by intro h cases h with | inl hp => exact hp | inr hf => cases hf ``` ## Common Patterns To prove: ```lean ⊢ P ∨ Q ``` use one of: ```lean left ``` or: ```lean right ``` then prove the selected side. To use: ```lean h : P ∨ Q ``` use: ```lean cases h with | inl hp => ... | inr hq => ... ``` To map a disjunction through implications, split it into cases and rebuild the target disjunction. ## Common Pitfalls Do not try to extract both sides from a disjunction. A proof of `P ∨ Q` contains one side, not both. Do not choose `left` or `right` before checking which proof is available. The chosen side becomes the new goal. Do not forget to handle both cases when using a disjunction hypothesis. A proof that only handles one case is incomplete. Do not confuse `P ∨ Q` with boolean `or`. A proof of `P ∨ Q` carries evidence for one side. ## Takeaway A disjunction is a tagged proof of one side. To prove `P ∨ Q`, choose `P` or choose `Q`. To use `P ∨ Q`, split into cases and prove the desired result in each case. This explains `left`, `right`, `Or.inl`, `Or.inr`, and case analysis on disjunctions.