Lean에서 자명한 정리 증명하기

2019년 2월 1일 · 태그: mathematics, formal · 원문 · 한국어 번역(원문에서 변경됨)

Lean 4와 같은 증명 보조기를 처음 시작할 때는 가능한 한 가장 기초적인 증명부터 시작하는 것이 좋습니다. 이러한 증명은 수학자에게는 너무나 자명해 보일 수 있지만, 이를 형식 체계에서 구현해 보면 증명 보조기가 어떻게 동작하는지에 대한 직관을 기르는 데 도움이 됩니다. 참임을 이미 알고 있는 기본적인 논리 명제부터 시작하면, 복잡한 수학에 빠져 헤매지 않고 형식 검증의 문법과 작동 방식을 익히는 데 집중할 수 있습니다. Lean의 증명 체계에 익숙해지기 위해 이러한 기초적인 증명 몇 가지를 살펴봅시다.

예제 1: 항등

첫 번째 정리는 모든 명제가 자기 자신을 함의함을 보여 줍니다:

theorem self_implies_self (p : Prop) :
    p → p := fun h => h

이는 λ 표기법을 사용하거나 명시적인 증명으로도 작성할 수 있습니다:

theorem self_implies_self' (p : Prop) :
    p → p :=
    λ h => h

theorem self_implies_self'' (p : Prop) :
    p → p := by
  intro h
  exact h

예제 2: 논리곱 제거

p ∧ q가 있으면 p가 있음을 증명할 수 있습니다:

theorem and_elim_left (p q : Prop) : p ∧ q → p := by
  intro h
  exact h.left

예제 3: 논리합 도입

p가 있으면 p ∨ q가 있음을 증명할 수 있습니다:

theorem or_intro_left (p q : Prop) : p → p ∨ q := by
  intro h
  exact Or.inl h

예제 4: 이중 부정 도입

p가 참이면 ¬¬p도 참임을 증명할 수 있습니다:

theorem double_neg_intro (p : Prop) : p → ¬¬p := by
  intro h
  intro hn
  exact hn h

예제 5: 배중률

고전 논리에서는 임의의 명제 p에 대해 p가 참이거나 ¬p가 참입니다. 이는 Lean의 고전 논리에서 공리입니다:

theorem excluded_middle (p : Prop) : p ∨ ¬p := by
  exact Classical.em p

이것은 앞의 예제들과 다르다는 점에 유의하십시오. 다른 정리들은 구성적으로 증명할 수 있었지만, 배중률에는 Classical 공리가 필요합니다. 직관주의 논리에서는 이 원리를 가정하지 않습니다. Lean에서는 Classical.em을 사용하여 이 공리에 접근합니다.

이는 패턴 매칭을 사용하여 작성할 수도 있습니다:

theorem excluded_middle' (p : Prop) : p ∨ ¬p :=
  match Classical.em p with
  | Or.inl h  => Or.inl h    -- if p is true, return p
  | Or.inr h  => Or.inr h    -- if ¬p is true, return ¬p