lean-tp-propositions

name: lean-tp-propositions description: Curry-Howard correspondence and logical connectives. Use when constructing proofs, understanding proof terms, or working with And/Or/Not/implication. allowed-tools: Read, Grep, Glob

Lean 4 Propositions and Proofs

Curry-Howard correspondence and logical connectives in Lean. Use when constructing proofs of logical statements, understanding proof terms, or working with And/Or/Not.

Trigger terms: "proposition", "proof", "And", "Or", "Not", "implication", "Curry-Howard", "logical connective", "prove"

Core Concept: Propositions as Types

Curry-Howard correspondence:

• Propositions are types in Prop
• Proofs are terms inhabiting those types
• To prove p : Prop, construct a term t : p

-- Proposition (a type)
#check (∀ p q : Prop, p → q → p) -- Prop

-- Proof (a term)
theorem t1 (p q : Prop) : p → q → p :=
  fun hp _ => hp

Implication (→)

Proof pattern: Lambda abstraction (assume hypothesis, derive conclusion)

-- To prove p → q: assume p, construct q
example (hp : p) (hq : q) : p := hp

-- Lambda explicitly
example : p → q → p := fun hp _ => hp

Conjunction (∧)

Introduction - Combine two proofs:

And.intro hp hq : p ∧ q
⟨hp, hq⟩ : p ∧ q          -- Anonymous constructor

Elimination - Extract components:

h.left  : p    -- And.left h
h.right : q    -- And.right h

Example:

example (h : p ∧ q) : q ∧ p := ⟨h.right, h.left⟩

Disjunction (∨)

Introduction - Provide one side:

Or.inl hp : p ∨ q    -- From left
Or.inr hq : p ∨ q    -- From right

Elimination - Case analysis:

example (h : p ∨ q) : q ∨ p :=
  h.elim
    (fun hp => Or.inr hp)
    (fun hq => Or.inl hq)

-- Or with match
match h with
| Or.inl hp => Or.inr hp
| Or.inr hq => Or.inl hq

Negation (¬)

Definition: ¬p := p → False

To prove ¬p: Assume p, derive False

example (hpq : p → q) (hnq : ¬q) : ¬p :=
  fun hp => hnq (hpq hp)

From contradiction: Derive anything

absurd hp hnp : q    -- From hp : p and hnp : ¬p
False.elim hf : q    -- From hf : False

Proof Constructs

have - Introduce intermediate step:

example (h : p ∧ q) : q ∧ p :=
  have hp : p := h.left
  have hq : q := h.right
  ⟨hq, hp⟩

show ... from - Explicit result type:

show q ∧ p from And.intro hq hp

suffices - Backward reasoning:

suffices h : intermediate from use_h
-- now prove intermediate

Quick Reference

Common Mistakes

Forgetting to handle both Or cases:

-- ❌ Incomplete
example (h : p ∨ q) : r := ...  -- Must handle both

-- ✓ Handle both
h.elim (fun hp => ...) (fun hq => ...)

Confusing ∧ and →:

-- ❌ p ∧ q is NOT p → q
-- ∧ means "both hold", → means "implies"

-- ✓ From p ∧ q you have both p AND q
-- From p → q you get q only IF you have p

See Also

• lean-tp-foundations - Type theory background
• lean-tp-quantifiers - Universal and existential quantifiers
• lean-tp-tactics - Tactic mode proofs

Source: Theorem Proving in Lean 4