이제 Coq를 이용해 간단한 증명을 직접 작성해보자.
Notation 본론을 시작하기에 앞서 전에 만들었던 plus, mult 에 infix notation을 정의하자.
Notation "x + y" := (plus x y) (at level 50, left associativity) : nat_scope. Notation "x * y" := (mult x y) (at level 40, left associativity) : nat_scope. 이전에 bool에 대해 x && y 를 정의하던 때보다 뭔가 이것저것 늘어났다. prefix, postfix notation과는 달리 infix notation에서는 모호한(ambiguous) 문장이 생길 수 있다. 일반적으로 (x+y*z)라는 표현식을 쓸 때 우리는 ((x+y)*z)가 아닌 (x+(y*z))를 의도한다. 위 코드에서의 역할을 간단히 요약하면
Define Numbers 이전 글에서는 day, bool, color 와 같이 원소의 개수가 유한한 타입, 다시 말해 타입 \(T\)에 대해 \(\{x \| x \mathrm\{\,has\,type\,\}T\} \)가 유한집합인 경우만을 다뤘다. 무한한 원소를 가지는 타입을 정의하려면 어떻게 해야 할까? 집합론에서와 마찬가지로 자연수에서 시작해보자. 페아노 공리계(Peano axioms)에서 필요한 부분을 빌려오자. 크게 중요하지 않은 공리들은 생략했다
Introduction 여기서는 Coq에서 사용되는 Galina라는 functional programming language의 기초적인 사용법과, Coq에서 증명에 실제 활용되는 기초적인 tactic에 대해 다룬다.
Data and Functions Days of the Week 먼저 Coq에서 타입을 선언하는 법을 알아보자. 모든 Coq 구문은 .(마침표)로 끝남에 유의하자
Coq를 공부해보겠다는 막연한 목표와 함께 이런저런 자료를 찾아보고 그만두기를 반복하던 중, DeepSpec Summer School 세미나에서 나온 영상을 발견했다. 유투브에서 찾은 다른 영상들이 4,5년 전 자료였던 반면 DeepSpec에서는 최근인 2017, 2018년까지 꾸준히 학습자료와 세미나 영상이 업로드되고 있다.
사실 예전 LaTeX을 익힐 때에도 이것저것 찾아보기만 하다가 결국 학교 과제를 LaTeX으로 작성해보고서야 익숙해졌는데, 이번에도 실 사용 없이 공부하는게 얼마나 갈지는 잘 모르겠다.. 자료 초반에 “All the core chapters are suitable for both upper-level undergraduate and graduate students.” 라는 말이 있던데, 물론 저런 말들이 다 그렇듯이 전부 거짓말이겠지만 이젠 undergraduate 신분이라는 핑계도 사라졌으니 좀더 확실히 짚고 넘어가야겠다는 생각도 든다.
동아리 톡방에서 이데일리 코딩대회에 대한 소식을 들었다. 학부를 졸업했지만 아직 대학원생은 아니라는 애매한 신분 때문에 대부분의 대회를 참가하지 못했었는데, 이번 대회는 청소년부/성인부로만 나뉘어져 있어 참가신청을 할 수 있었다.
예선 10월 26일 온라인 예선이 다가오자 안내문자가 날아왔는데, 처음엔 눈을 의심했다. 48시간 대회라는 점도 특이했지만 120문제라는 엄청난 문제 수에선 말이 나오지 않았다. 다른 대회들이 보통 3~5시간 동안 5문제, 팀으로 진행하는 ICPC도 많아야 12,13문제를 내는데 예선에서부터 120문제라는 공지를 보고 과연 어떤 문제들이 나올지 기대(?)되기도 했다.
어째 코드잼 관련 글만 계속 올라오는 것 같다.. 여튼 이틀 전 Code Jam Kickstart Round G가 있길래 참가했다. 일요일 오후 10시라는 시간대가 조금 걸렸지만 월요일 연차휴가라는 사실에 힘입어 대회를 치르기로 했다.
대회 초반에 빠르게 문제를 풀고 중간 등수가 6등까지 올라갔다. 남은 1시간 반 동안 C 라지를 마저 풀까 하다가 exponential 한 알고리즘밖에 떠오르지 않길래 gg 후 웹툰으로 넘어갔다.
TL;DR : 로컬의 문제점을 깨닫지 못하고 폭사(…)
페이스북 해커컵이 끝났다. 구글 코드잼 본대회는 대회 당시 인터넷을 쓸 수 없는 환경(…)에 있어서 아쉬운 마음이었는데, 다행히 해커컵은 일정이 맞아 모두 참가할 수 있었다. 생각치 못한 실수로 Round 2에서 탈락했지만 각 라운드를 간단히 요약해봤다.
Qualification Round 당시 아직 ‘전직’을 한 상태가 아니었지만 주말이라 외출을 할 수 있었다. 대전의 한 PC방에서 파이썬3을 다운받아 대회를 진행했다.
공식적으로 전직(…)을 했지만 가능한 한 PS대회는 계속 나가보고 싶었다. SCPC나 UCPC는 이제 대학생이 아니라 참가를 못했지만, 지난 주말에 Code Jam Kickstart Round D가 있어 여기 참가해볼 수 있었다. 코드잼 킥스타트에 대한 설명은 Round C 후기에서 한번 작성한 바 있으니 이 글에서는 생략했다.
이날 대회는 오후 2시부터 열렸는데, 내가 3시부터 세미나가 있어 그전까지는 약속장소 근처 스타벅스, 이후엔 세미나실에서 틈틈히 코딩을 진행했다. 저번 Round C를 1시간 20분만에 올클했었기에 이번에도 비슷하게 걸리지 않을까라는 근자감이 가득한 예상을 했지만 A를 보는 순간 그런 기대는 깔끔하게 접혔다. 결국 C에 와서는 “그냥 small만 통과하자"라는 마음으로 small 전용 코드를 짜서 제출하고 다시 세미나에 합류했다.
한동안 개인 사정으로 인해 다른 일을 할 수 없어 Google Code Jam 본대회 Qualification Round를 불참했는데, 마침 오늘 Code Jam Kickstart 가 있길래 참가해봤다.
Kickstart는 CodeJam 본대회와 달리 비교적 자주 진행되고(2017년 기준 7회), 다양한 시간대에 분포해 있어 코포처럼 새벽까지 깨어있지 않아도 참가할 수 있다. 대회 자체적으로 상을 주지는 않지만 좋은 성적을 낼 경우 구글에서 인턴/입사 인터뷰 메일이 오기도 하니 시간이 된다면 참가해보자. 실제로 2017년 Kickstart Round G 때 15등 찍어서 메일 받아봄.
대부분의 reference가 그렇듯이 읽다보면 쉽게 지루해진다. 지루함을 덜하고 Coq에 익숙해지기 위해 일단 예제를 조금씩 따라해보면서 익혀가기로 했다. 자바를 처음 배울 때 public static void main(int argv, char **argc)가 정확히 뭔지는 몰라도 “Hello World” 부터 찍어보는 그런 마음으로 진행해봤다.
CoqIDE 실행 프로그램을 처음 실행하면 다음과 같은 화면을 볼 수 있다. 크게 3가지 창으로 나뉘어져 있으며, 왼쪽은 코드 작성을, 오른쪽 위/아래는 각각 Proof 보조/결과 출력을 담당하는 역할이었다.
