[Lean] Natural Number Game 1. Tutorial World

 

Lean은 프로그래밍 언어이자 증명보조기로 사용되는 도구이다.

Natural Number Game을 통해, 인터랙티브 Lean을 사용하여 Lean의 문법을 간략히 학습할 수 있었다. 또한, 0을 포함한 (페아노 공리계를 따라 정의된) 자연수에서의 여러 Theorem을 순차적으로 증명하는 방법을 알 수 있었다. 다만, 인터랙티브인 만큼 증명이 긴 Theorem의 경우 가독성이 좋지 않기 때문에, indentation을 비롯한 추가적인 문법에 대해서는 추가로 알아둘 필요가 있을 것 같다.

---

Tutorial World Level 1

If \(x\) and \(q\) are arbitrary natural numbers, then \(37x+q=37x+q\).

example (x q : ℕ) : 37 * x + q = 37 * x + q := by

rfl

rfl은 reflexivity를 의미하는 Tactic으로, 좌변과 우변이 같은 \(X=X\) 형태의 Goal이 성립함을 증명하는 데 사용한다.

---

Tutorial World Level 2

If \(x\) and \(y\) are natural numvers, and \(y=x+7\), then \(2y=2(x+7)\).

example (x y : ℕ) (h : y = x + 7) : 2 * y = 2 * (x + 7) := by

rw [h]
rfl

rw은 rewrite를 의미하는 Tactic으로, 대괄호 안에 들어가 있는 equation의 좌변과 같은 형태를 Goal에서 찾아서 우변으로 substitute하는 명령을 수행한다. 이 문제의 경우 \(y=x+7\)의 좌변인 \(y\)를 Goal인 \(2y=2(x+7)\)에서 찾아서 \(x+7\)로 바꾼다. 그러면 \(2(x+7)=2(x+7)\)로 양변이 완전히 같은 형태가 되기 때문에 rfl을 통해 증명이 완료된다.

---

Tutorial World Level 3

\(2\) is the number after the number after \(0\).

example : 2 = succ (succ 0) := by

rw [two_eq_succ_one, one_eq_succ_zero]
rfl

rw의 대괄호 안에는 여러 equation들이 comma로 연결되어 들어갈 수 있다. 이 경우 각각의 equation을 순차적으로 대입한다. two_eq_succ_one과 one_eq_succ_zero는 각각 2 = succ 1과 1 = succ 0을 나타내는 Theorem으로, 별도의 증명 없이 사용 가능하다.

---

Tutorial World Level 4

\(2\) is the number after the number after \(0\).

example : 2 = succ (succ 0) := by

rw [← one_eq_succ_zero, ← two_eq_succ_one]
rfl

Level 3과 같은 문제를 다르게 증명하는 방법이다. 이때, backslach + l로 입력할 수 있는 \(\leftarrow\)는 equation의 우변과 같은 형태를 찾아 좌변의 형태로 substitute하는 명령을 수행한다. 즉, 이 경우 rw를 수행한 결과는 2 = 2가 된다.

---

Tutorial World Level 5

\(a+(b+0)+(c+0)=a+b+c\).

example (a b c : ℕ) : a + (b + 0) + (c + 0) = a + b + c := by

repeat rw [add_zero]
rfl

rw 앞에 repeat이 붙는 경우, 내부의 equation을 모두 찾아 대입하라는 의미이다. add_zero는 자연수 \(x\)에 대하여, \(x+0=x\)을 나타내는 Theorem이다. 이 또한 별도의 증명 없이 사용 가능하다.

---

Tutorial World Level 6

\(a+(b+0)+(c+0)=a+b+c\).

example (a b c : ℕ) : a + (b + 0) + (c + 0) = a + b + c := by

rw [add_zero c]
rw [add_zero b]
rfl

Level 5와 같은 문제를 다르게 증명하는 방법이다. add_zero는 뒤에 매개변수를 가질 수 있는데, 매개변수를 명시한 경우 그 문자의 Object가 포함된 식을 substitute한다. 예를 들어 처음의 add_zero c는 \(c+0=c\)를 의미하는 식이다.

---

Tutorial World Level 7

Theorem succ_eq_add_one: For all natural numbers \(a\), we have \(\text{succ}(a)=a+1\).

theorem succ_eq_add_one n : succ n = n + 1 := by

rw [one_eq_succ_zero]
rw [add_succ]
rw [add_zero]
rfl

 

add_succ은 두 자연수 \(a\), \(d\)에 대하여 \(a+\text{succ} \ d=\text{succ}(a+d)\)가 성립한다는 식으로, 별도의 증명 없이 사용 가능하다. 순차적으로 \(\text{succ} \ n=n+\text{succ} \ 0\), \(\text{succ} \ n=\text{succ} (n+0)\), \(\text{succ} \ n=\text{succ} \ n\)이 성립하므로 증명이 완료된다. 이제, succ_eq_add_one을 다른 Theorem의 증명에 사용할 수 있게 되었다.

---

Tutorial World Level 8

\(2+2=4\).

 

example : (2 : ℕ) + 2 = 4 := by

nth_rewrite 2 [two_eq_succ_one]
rw [add_succ]
rw [one_eq_succ_zero]
rw [add_succ]
rw [add_zero]
rw [four_eq_succ_three]
rw [three_eq_succ_two]
rfl

nth_rewrite는 대괄호 전에 수를 매개변수로 받아서, equation을 대입할 수 있는 해당 수 번째 표현을 바꾼다. 이 경우 두 번째 \(2\)가 \(\text{succ} \ 1\)로 바뀐다. 이후 add_succ를 사용하면 \(\text{succ}(2+1)\)이 된다. 같은 방법을 한 번 더 반복하면 \(\text{succ} \ \text{succ}(2+0)\)을 얻는다. 이제 add_zero를 사용하면 좌변은 \(\text{succ} \ \text{succ} \ 2\)가 되고, \(\text{succ}\)을 사용하여 \(4\)를 \(2\)의 successor의 successor로 만들면 좌변과 우변이 같아진다.