귀납법: 귀납적 증명

시작하기 전에 이전 장의 모든 정의들을 불러올 필요가 있다.

Require Export가 동작하려면 coqc를 사용하여 Basics.v를 Basics.vo로 우선 컴파일할 필요가 있다. .java 파일에서 .class 파일을 만들거나 .c 파일에서 .o 파일을 만드는 것과 비슷하다. 이렇게 컴파일하는 방법이 두 가지가 있다.

• CoqIDE:
  Basics.v를 열고, "컴파일" 메뉴에서 "컴파일 버퍼"를 클릭한다.
  (주의: "-R LF"을 고려하도록 이 명령어들을 업데이트할 필요가 있다. CoqIDE 전문가 중에 이것을 어떻게 하는지 얘기해 줄 수 있나요?)
• 명령어:
  make Basics.vo

문제가 있으면 (예를 들어, 콕 파일에서 나중에 식별자를 못찾는 것과 같은) 콕에서 "load path"가 적절히 설정되지 않았기 때문일 수도 있다. Print LoadPath. 명령어는 이런 문제들을 해결하는데 도움이 될 수 있다.

귀납적 증명

지난 장에서 간략화 방법으로 쉽게 0이 +의 왼편 중립 원소라는 것을 증명했다. _오른편_ 중립 원소이기도 함을 ...

... 똑같이 간단하게 증명할 수 없다는 것을 보기도 하였다. 왜냐하면 n + 0에서 n은 임의의 알려지지 않은 숫자이기 때문에 단순히 reflexivity를 적용하는 것으로 증명되지 않는다. 그래서 + 정의에 있는 match를 간략화시킬 수 없다.

destruct n을 사용하여 가능한 경우들로 나누어도 더 진전할 수 없다. n = 0을 가정하는 경우의 분석 쪽은 증명할 수 있다. 어떤 n'의 n = S n'인 경우에 똑같이 막힌다.

한 단계 나아가기 위해 destruct n'을 사용할 수도 있지만 n은 임의로 큰 숫자일 수 있기 때문에 이렇게 그냥 진행하면 증명이 결코 끝나지 않을 것이다. 숫자, 리스트, 다른 귀납적 집합들에 대한 흥미로운 사실들을 증명하기 위해 보통 더 강력한 추론 원리 _귀납법_이 필요하다. (고등학교부터, 이산수학 강의 등) _자연수에 대한 귀납법 원리_를 떠올려 보자. P(n)이 자연수 n을 사용하는 어떤 명제이고 모든 n에 대해 P가 성립한다고 보이고 싶다면 이렇게 추론할 수 있다.

• P(O)이 성립한다고 보인다. - 어떤 n'에 대해 P(n')이

성립하면 P(S n')도 성립한다고 보인다. - 모든 n에 대해 P(n)이 성립한다고 결론 내린다. 콕에서 증명 방법은 동일하다. 모든 n에 대해 P(n)을 증명하는 목적을 가지고 시작하고 (induction 전술을 적용해서) 두 가지 분리된 부분 목적들로 나눈다. 하나는 P(O)를 증명하는 것이고, 다른 하나는 P(n') → P(S n')을 증명하는 것이다. 이 방법이 다음 정리에 대해 어떻게 작동하는지 보자.

destruct처럼, induction 전술은 부분 목적들에 도입한 변수 이름들을 지정하는 as... 절을 받는다. 두 개의 부분 목적들이 있기 때문에 as... 절에 |로 분리된 두 부분들이 있다. (엄밀히 말하면 as... 절을 생략할 수 있고 콕이 우리 대신 이름들을 선택할 것이다. 콕이 자동으로 지어준 이름들은 혼돈스러운 경향이 있기 때문에 실제로 절을 생략하는 것은 좋지 않다.) 첫 번째 부분 목적에서 n은 0으로 바꾼다. (as...의 처음 부분은 비어있기 때문에) 새로운 변수들을 도입하지 않는다. 그리고 목적은 0 = 0 + 0이 되고 간략화를 적용하면 증명을 마칠 수 있다. 두 번째 부분 목적에서 n은 S n'으로 바꾸고, n' + 0 = n' 가정을 현재 문맥에 추가하고 IHn' (즉, n'에 대한 귀납 가정) 이름을 붙인다. n'과 IHn' 이 두 이름들은 as... 절의 두 번째 부분에 지정되어 있다. 이 경우 부분 목적은 S n' = (S n') + 0이 되고 S n' = S (n' + 0)으로 간략화시킬 수 있는데 IHn'으로부터 유추할 수 있다.

(이 증명들에서 intros 전술은 사실 중복 사용된 것이다. 한정 변수들을 포함하는 목적에 induction 전술을 적용할 때 필요한 만큼 그 변수들을 자동으로 현재 문맥에 도입하기 때문이다.)

연습문제: 별 두 개, 추천 (basic_induction)

귀납법을 사용하여 다음을 증명하라. 이전에 증명한 결과들을 필요로 할 수도 있다.

☐

연습문제: 별 두 개 (double_plus)

인자를 두 배로 늘리는 다음 함수를 고려하시오:

귀납법을 사용하여 double에 대한 간단한 사실을 증명하시오:

☐

연습문제: 별 두 개, 선택사항 (evenb_S)

evenb n 정의에서 n-2에 대한 재귀 함수 호출은 불편한 점이 있다. n에 대한 귀납법으로 evenb n에 대해 증명할 때 더 어렵게 만들다. 왜냐하면 n - 2에 대한 귀납적 가정을 필요로 할 수 있기 때문이다. 다음 보조 정리는 귀납법을 더 활용하기 쉬운 다른 형태의 evenb (S n)의 성질을 제공한다.

연습문제: 별 한 개 (destruct_induction)

destruct 전술과 induction 전술의 차이를 간략히 설명하시오. ☐

증명 안에서 증명하기

콕에서도 비공식적인 수학에서와 같이 커다란 증명들은 일련의 정리들로 종종 나누어 나중에 증명할 때 이전에 증명해놓은 정리들을 참고하곤 한다. 하지만 때때로 증명하는 중에 너무 사소하고 일반적이지 않고 너무 특별한 잡다한 사실이 필요하면 맨 상위 수준의 이름을 붙이는 것이 꺼려진다. 그러한 경우에 필요한 곳에 필요한 "부분 정리"를 간단히 기술하고 증명하는 것이 편리하다. assert 전술은 이런 것을 하도록 해준다. 예를 들어 이전에 mult_0_plus 정리를 증명하면 이전 정리 plus_0_n을 참조한다. 그 자리에서 plus_0_n을 서술하고 증명하는 대신 assert를 사용할 수 있다.

assert 전술은 두 개의 부분 목적들을 도입한다. 첫 번째 부분 목적은 선언한 명제 그 자체이다. 그 전술에 H:를 뒤이어 주어 그 명제를 H로 이름 짓는다. (destruct와 induction 전술을 이 전에 사용했을 때처럼 as를 가지고 명제 이름을 지을 수도 있다. assert (0 + n = n) as H.) 이 명제의 증명을 중괄호 { ... }로 감싸는 것을 확인하시오. 이것은 콕을 대화식으로 사용할 때 이 부분 증명을 끝냈을 때를 더 쉽게 볼 수 있게 하는 가독성을 위한 것이다. 두 번째 목적은 assert를 실행한 지점에서의 목적과 동일한 것이다. 다만 0 + n = n이라는 가정 H를 이제 이 문맥에서 활용할 수 있다는 점이 차이가 있다. 즉, assert는 선언한 명제를 증명해야 하는 부분 목적과 선언한 명제를 사용하여 증명하고자 했던 것을 진행하기 위한 두 번째 부분 목적을 생성한다. assert의 다른 예제... 예를 들어, (n + m) + (p + q) = (m + n) + (p + q)을 증명한다고 가정하자. =의 양쪽에서 유일한 차이점은 첫 번째 +의 m과 n 인자들이 뒤집혀있어서 덧셈의 교환 법칙(plus_comm)을 사용해서 한 쪽을 다른 쪽으로 다시 작성할 수 있을 것처럼 보인다. 하지만 rewrite 전술은 그다지 영리하지 않아서 _어디에_ 이 전술을 적용할지 모른다. +을 세 군데에서 사용하는데 rewrite → plus_comm은 _바깥쪽_ 덧셈에만 적용될 것이다...

필요한 지점에 plus_comm을 사용하려면 (여기에서 다루는 특별한 m과 n에 대해) 내부적으로 보조 정리 n + m = m + n을 도입해서 plus_comm으로 증명하면 원하는 곳에 plus_comm을 사용한다.

형식적 증명 대 비형식적 증명

"_비형식적 증명은 알고리즘이고; 형식적 증명은 코드다_." 수학적 주장의 성공적인 증명이란 무엇인가? 이 질문은 천 년간 철학자들이 품어온 질문이다. 하지만 대략적으로 준비된 정의는 이럴 수 있다. 수학적 명제 P의 증명은 독자나 청자에게 P가 확실히 사실 임(P의 참에 대한 논쟁의 여지가 없음)을 주입시키는 글로 작성하거나 말로 설명하는 텍스트이다. 즉, 증명은 커뮤니케이션 행위이다. 커뮤니케이션 행위는 다른 종류의 독자들과 관여할 수 있다. 한편으로 이 "독자"는 콕과 같은 프로그램으로 이런 경우 "믿음"이 주입되는 방식이란 P를 어떤 형식적인 논리 규칙들로부터 기계적으로 유도될 수 있다는 것이다. 그리고 이 증명은 이 사실을 검사하는데 있어서 이 프로그램을 가이드하는 수단이다. 그러한 수단이 _형식적_ 증명이다. 또 다른 각도에서 보면, 독자는 사람이 될 수 있고, 영어나 어떤 다른 자연어로 증명을 작성할 수 있다. 따라서 반드시 _비형식적_이 될 것이다. 여기서 성공에 대한 기준은 다소 명확하지 않게 정해진다. "유효한" 증명은 독자가 P를 믿게 만드는 것이다. 하지만 동일한 증명을 읽은 많은 다른 독자들 중에 일부는 주장을 설명하는 특별한 방법으로 설득될 수 있고 다른 사람들은 그렇지 않을 수도 있다. 어떤 독자들은 특별히 현학적이거나, 경험이 부족하거나 단지 단순히 아둔할 수 있다. 그들을 설득하는 유일한 방법은 매우 고심해서 상세하게 주장을 펼치는 것이다. 하지만 다른 독자들은 이 분야에 더 익숙해서 모든 이 상세 내용으로 압도당해서 전체적인 주제를 잃을 수도 있다. 그들이 원하는 것은 주요 아이디어들을 듣는 것이다. 자세한 내용을 글로 작성하여 설명하며 진행하기보다 그들 스스로 상세 사항들을 채우는 것이 더 쉬울 수 있기 때문이다. 궁극적으로 일반적인 척도는 없다. 왜냐하면 생각할 수 있는 모든 독자를 설득할 수 있는 비형식적 증명을 작성하는 방법이 유일하지 않기 때문이다. 하지만 실제 상황에서 수학은 풍부한 관습들과 관용어구들을 개발해서 복잡한 수학 대상들에 대해 글로 작성하는 것을 가능하게 만들었다. 적어도 특정 커뮤니티 내에서는 커뮤니케이션을 꽤 잘할 수 있다. 이러한 스타일의 커뮤니케이션 관습들은 증명이 좋은가 나쁜가를 판단하는 꽤 분명한 척도를 제공한다. 이 강의에서 우리는 콕을 사용하기 때문에 형식적 증명들에 대해 열심히 공부할 것이다. 하지만 비형식적 증명들을 완전히 잊어버릴 수는 없다! 형식적 증명은 다양한 방법에서 유용하지만 사람들이 아이디어를 교환하는데 _그다지_ 효과적이지 않다. 예를 들어, 덧심이 결합성을 갖음을 보이는 증명이 있다.

콕은 이 증명을 완벽하다고 여길 것이다. 하지만 사람에게는 증명의 의도를 파악하기 어렵다. 주석들과 구분점들을 사용하여 조금 더 분명하게 구조를 보여줄 수 있다...

... 그리고 만일 콕에 익숙하다면 증명에 사용한 전술들을 하나씩 마음 속으로 따라가며 각각에서 문맥과 목적 스택이 어떤지 상상할 수 있다. 하지만 증명이 조금 더 복잡하면 머릿속으로 증명 과정을 그려보는 것은 불가능할 것이다. (현학적인) 수학자는 이 증명을 다음과 같이 작성할 수도 있다.

• Theorem: 어떤 n, m, p에 대하여,
  n + (m + p) = (n + m) + p.
  _증명_: n에 관한 귀납법에 의하여.
  • 첫째, n = 0을 가정하자. 다음을 증명해야 한다.
    0 + (m + p) = (0 + m) + p.
    + 정의에 의해 위 명제가 바로 참이다.
  • 다음, n = S n'을 가정하고, 아래와 같다.
    n' + (m + p) = (n' + m) + p.
    다음을 반드시 증명해야 한다.
    (S n') + (m + p) = ((S n') + m) + p.
    +의 정의에 의해, 위 명제는 아래 명제로 부터 증명 가능하다.
    S (n' + (m + p)) = S ((n' + m) + p),
    이 명제는 귀납적 가정에 의해 바로 참이다. Qed.

이 증명의 전체적인 형태는 기본적으로 비슷하다. 그리고 이것은 물론 우연히 아니다. 콕은 induction 전술은 동일한 부분 목적들을 동일한 순서로 생성하도록 설계되었다. 마치 수학자가 작성하는 점 표시들과 같다. 하지만 상세히 들여다보면 중요한 차이점들이 있다. 형식적 증명은 어떤 면들에서 훨씬 더 명시적이다 (예를 들어, reflexivity를 사용하는 것과 같이) 하지만 다른 점에서는 훨씬 덜 명시적이다 (특히 콕 증명에서 어떤 시점의 "증명 상태"는 완전히 묵시적이지만 반면에 비형식적 증명은 독자로 하여금 현재 어느 시점인가를 반복해서 독자에게 상기시킨다.)

연습문제: 별 두 개, 고급, 추천 (plus_comm_informal)

plus_comm을 증명한 것을 비형식적 증명으로 변환해보시오. Theorem: Addition is commutative. Proof: ☐

연습문제: 별 두 개, 선택 사항 (beq_nat_refl_informal)

다음 정리를 비형식적으로 증명하시오. plus_assoc에 대한 비형식적 증명을 참고하시오. 콕 전술들을 영어로 바꾸기만 하는 방식을 사용하지 마시오! Theorem: true = beq_nat n n for any n. Proof: ☐

추가 연습문제들

연습문제: 별 세 개, 추천 (mult_comm)

assert를 사용해서 다음 정리를 증명하시오. plus_swap에 대한 귀납법을 사용할 필요가 없다.

이제 곱셈의 교환법칙을 증명하시오. (증명할 때 별도의 보조 정리를 정의해서 증명할 필요가 분명히 있을 것이다. plus_swap이 유용하다는 것을 발견할 수도 있다.)

☐

연습문제: 별 세 개, 선택 사항 (more_exercises)

종이를 들어, 아래 정리들 각각에 대해 먼저 (a) 간략화와 다시 작성하기만으로 증명할 수 있는지, (b) 경우를 나누어 분석(destruct)을 또한 요구하는지, (c) 귀납법을 또한 요구하는지 _생각_해보시오. 예상을 해본 다음 증명을 채워보시오. (작성한 종이를 제출할 필요는 없다. 콕으로 증명하기 전에 생각해보는 연습을 권하기 위한 것이다!)

☐

연습문제: 별 두 개, 선택 사항 (beq_nat_refl)

다음 정리를 증명하시오. (true를 등식의 왼편에 놓은 것이 이상하게 보일 수도 있지만 콕 표준 라이브러리에서 이 정리를 서술하는 형태이어서 따른 것이다. 다시 작성하는 방식을 사용하면 어느 방향이든 똑같이 잘 적용된다. 그래서 어느 방식으로 서술하든 이 정리를 사용하면 문제가 없을 것이다.)

☐

연습문제: 별 두 개, 선택 사항 (plus_swap')

replace 전술로 다시 작성할 특정 부분 낱말을 지정할 수 있고 무엇으로 다시 작성할지 지정할 수 있다. replace (t)를 (u)를 증명 목적에 나타난 식 t(의 모든 경우)를 식 u로 바꾸고, t = u를 추가적으로 부분 목적으로 생성한다. 이것은 단순히 rewrite를 적용했을 때 목적의 틀린 부분에 대해 적용될 때 종종 유용하다. replace 전술을 사용하여 마치 plus_swap에 대해서처럼 plus_swap'을 증명하시오. 이 경우 assert (n + m = m + n)이 필요하지 않을 것이다.

☐

연습문제: 별 세 개, 추천 (binary_commute)

Basics 장의 binary 연습문제에서 작성했던 incr과 bin_to_nat 함수들을 가지고, 다음 다이어그램이 어느 방향으로 가도 동일함을 증명하시오. incr bin ----------------------> bin | | bin_to_nat | | bin_to_nat | | v v nat ----------------------> nat S 즉, 이진수를 증가하고 (단항) 자연수로 변환하면 먼저 자연수로 변환하고 증가시킨 것과 동일한 결과를 낸다는 것이다. bin_to_nat_pres_incr 정리 ("pres"는 "preserves"로 사용)에 이름을 붙이시오. 이 연습문제를 풀기 전에 당신의 연습문제 풀이의 정의들을 binary 여기 연습문제로 복사해서 이 파일 자체로 채점할 수 있도록 하시오. 원래 정의들을 변경해서 이 성질을 더 쉽게 증명하고 싶다면 자유롭게 그렇게 진행하면 된다!

☐

연습문제: 별 다섯 개, 고급 (binary_inverse)

이 연습문제는 이진수들에 대한 이전 연습문제의 연장이다. 이 연습문제를 풀기 위해서 거기에 있는 정의들과 정리들이 필요할 것이다. 채점을 위해 이 파일에 다른 파일을 참조하지 않아도 완전하도록 그것들을 이 파일에 복사하시오. (a) 첫째, 자연수를 이진수로 변환하는 함수를 작성하시오. 그다음 어떤 자연수라도 이진수로 변환한 다음 다시 자연수로 변환하면 동일한 자연수로 돌아온다는 것을 증명하시오. (b) 자연스럽게 반대 방향에 대해서도 증명해야 한다고 생각할 수 있다. 이진수에서 시작해서 자연수로 변환하고 다시 이진수로 돌아가면 동일한 이진수가 된다. 하지만 이 경우는 참이 아니다! 그 이유를 설명하시오. (c) "직접" 정규화하는 함수를 정의하시오. 즉, 이진수를 이진수로 매핑하는 함수 normalize는 어떠한 이진수 b를 자연수로 변환하고 다시 이진수로 변환한다 (normalize b). 이 함수를 이용하여 반대 방향의 정리를 증명하시오. (경고: 이 부분은 신중해야 한다!) 다시 말하는데, 여기서 증명하는데 도움이 된다면 이전 정의들을 자유롭게 변경하시오.

☐