Basics

Posted on In , , Reading time ≈ 10 mins.

Curry–Howard correspondence

Functional Programming Language는 Mathematics랑 일대일 대응된다!

P: T라면 T(Type)은 proposal(명제), P(Program)은 proof(증명)이라고 생각할 수 있다.
만약 type checking이 된다면, proposal에 맞는 proof가 있다는 뜻이므로, 명제가 참이다!

이걸 왜 하냐?
엄밀하게 수학, 또는 프로그램의 정확성을 증명할 수 있다!
특히 LLM 시대에 LLM이 내놓은 출력을 사실 믿을 수가 없는 상황임 -> 증명보조기로 검증할 수 있다면?

실제로 수학자들도 증명을 (Coq이 아니라 Lean을 쓰지만) 컴퓨터로 검증하고 있다!

더 들어가자면 T(Type)은 어떤 집합이라고 볼 수 있는데, 여기에 속한 element P(Program)을 찾을 수 있다면 T는 참이라는 뜻!
반대로 T에 속한 element가 없다면 T는 거짓이다!

Rocq Calculus

Rocq에는 Type이라는 것만 존재함 (그냥 키워드임), 나머지는 전부 사용자가 정의하는 것!
사실 Proposal용 Prop이랑 Value용 Set이 따로 존재하긴 하는데 일단은 둘 다 그냥 Type이라고 생각하고 무시
실제로 Type이랑 똑같은데 그냥 편의상 구분해놓은 것

태초에는 Type이라는 것만 존재 (그냥 키워드임)
나머지는 전부 사용자가 정의하는거

Type은 모든 set의 set,
MyType: Type은 특정 set,
MyElement: MyType는 그 set의 element

모든 element는 딱 하나의 Type에만 소속되어있음!!!
Rocq에 subtype는 존재하지 않는다!
(예외로 Prop, Set은 Type의 subtype이지만 그냥 Type이라고 생각해도 됨)
즉, 1이 int이면서 short이면서 bool일수는 없다는거임

Inductive

1
2
3
4
5
6
7
8
9
10
11
Inductive day : Type :=
  | monday
  | tuesday
  | wednesday
  | thursday
  | friday
  | saturday
  | sunday.

Check (day: Type). (* 그냥 Check day.하면 day: Set으로 뜨는데 무시!!! *)
Check (monday: day).

Inductive로 set과 그 set의 element를 정의할 수 있음.
Check를 통해 Type 확인 가능!

여기서 monday는 set의 element를 정의한 것이기 때문에 Check (monday: Type).는 실패하게 됨

Definition

1
2
3
4
5
6
7
8
9
10
11
12
Definition next_working_day (d: day) : day :=
  match d with
  | monday => tuesday
  | tuesday => wednesday
  | wednesday => thursday
  | thursday => friday
  | friday => monday
  | saturday => monday
  | sunday => monday
  end.

Compute (next_working_day friday). (* monday: day *)

Definition으로 함수를 정의할 수 있음.
프로그램을 계산했을 때 같다 = 수학에서 동치관계를 의미함.
e.g. next_working_day friday는 monday랑 동치!

하지만 프로그램이다 보니까 "계산"은 아무 동치관계로나 움직일 수 있는게 아니라 제일 단순해지는 방향으로 (즉, reduced form으로) 계산됨.
즉 monday가 갑자기 next_working_day friday로 계산될 수는 없음!

만약 T1: Type면서 T2: Type이라면 T1->T2: Type임
즉 T1->T2도 set임! T1 set에서 T2 set으로 가는 함수들의 집합을 나타냄.
e.g. next_working_day: day -> day

Inductive처럼 T1->T2 set의 원소를 바로 만들어내고 싶다면 lambda function을 사용할 수 있음.

1
Check ((fun d: day => monday): day -> day).

사실 Definition은 엄밀히 따지면 함수를 정의하는 syntax가 아니라 lambda function에 이름 붙이는 syntax sugar임...

1
2
3
4
5
Definition foo (b: bool): day :=
  match b with
  | true => monday
  | false => tuesday
  end.

사실 이건

1
2
3
4
5
6
7
Definition foo: bool -> day := (
  fun b: bool =>
    match b with
    | true => monday
    | false => tuesday
    end
).

이거랑 똑같음!

여담) syntax의 집합은 countable이지만, set에서 set으로 가는 함수의 집합은 uncountable임.
즉, 수학적으로 존재하지만 우리가 Rocq로 표현할 수 없는 함수가 존재함! (그것도 uncountable 만큼이나 존재함!!)
하지만 생각해보면 굳이 Rocq가 아니라 어떤 언어여도 (심지어 자연어여도) 성립하는 말이다..?

match

왠지 모르겠는데 수학에는 dual이 있어야함 (사실 수학자는 몰랐는데 컴공한테서 자연스럽게 배움)
Set의 element를 만들 수도 있다면 element를 없앨 수도 있어야 함?

프로그램을 "계산"하면 element를 없애버림.
그 중 Inductive는 match로 제거함.

1
2
3
4
match b with
| true => monday
| false => tuesday
end
  • value: 계산이 완전히 끝난 값
  • expression: 계산을 하면 값이 됨

Inductive의 value는 처음에 정의했던 값들밖에 없음!!
e.g. day의 value는 monday ~ sunday밖에 없음.

apply

1
2
3
4
5
6
Compute ((fun b: bool =>
        match b with
        | true => monday
        | false => tuesday
        end
) false).

Function의 elimination rule은 apply임...
말 그대로 f x하면 function을 사용한 것!

Compute

요약) Type에는 Inductive랑 Function이 있음
각 Type마다 introduction rule이랑 elimination rule이 있음
이 네 가지 rule을 type checking이 가능하도록 조합한 모든 것을 expression이라고 부름

Inductive의 introduction은 Inductive
Inductive의 elimination은 match
Function의 introduction은 lambda function
Function의 elimination은 apply (키워드는 아니지만...)

이제 계산을 좀 더 엄밀하게 정의할 수 있는데 같은 type(Inductive/Function)에 대해서 introduction과 elimination이 만날 경우 reduction이 일어남.

e.g. 아래 코드를 실행시키면

1
2
3
4
5
6
7
8
9
10
11
(fun x =>
  match x with
  | monday => tuesday
  | tuesday => wednesday
  | wednesday => thursday
  | thursday => friday
  | friday => monday
  | saturday => monday
  | sunday => monday
  end
) friday

먼저 함수 argument를 대체하고

1
2
3
4
5
6
7
8
9
match friday with
| monday => tuesday
| tuesday => wednesday
| wednesday => thursday
| thursday => friday
| friday => monday
| saturday => monday
| sunday => monday
end

match를 맞추게 됨.

1
monday

여담) Proof

이것들을 이용해서 증명을 어떻게 하냐?

1
2
3
4
Definition test_next_working_day:
  (next_working_day friday) = monday
  :=
  eq_refl.

eq_refl은 양변이 같은 등식들의 집합임.
만약 (next_working_day friday)가 monday가 아니라면 eq_refl에 속하지 않으므로 type checking에 실패함!
반대로 type checking이 된다면 (next_working_day friday)가 monday와 같다는게 증명이 되는 것

1
2
Goal (next_working_day friday) = monday.
Proof. simpl. reflexivity. Qed.

실제 증명은 일일히 type을 지정해주는게 아니라 이런 식으로 증명하지만... 이는 후술함

Standard library

Rocq는 사실 위에 있는 네 가지 rule과 계산만으로 정의되어있음!
하지만 손가락의 수명을 위해서 아주 다양한 syntax sugar들과, (e.g. Definition으로 함수 introduction)
미리 정의해둔 다양한 standard library가 있음.

엄밀히 따지면 여기 있는 모든 내용이 standard library인건 아니긴 함;;

bool

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
Inductive bool : Type :=
  | true
  | false.

Definition negb (b:bool) : bool :=
  match b with
  | true => false
  | false => true
  end.
Definition andb (b1:bool) (b2:bool) : bool :=
  match b1 with
  | true => b2
  | false => false
  end.
Definition orb (b1:bool) (b2:bool) : bool :=
  match b1 with
  | true => true
  | false => b2
  end.

Rocq에는 bool과 다양한 함수들이 정의되어있음.
위 코드는 실제 구현을 따라한 것!

잠만 andb, orb는 뭐 어떻게 생겨먹은거임?

1
2
3
4
5
6
Definition andb: bool -> (bool -> bool) :=
  fun b1: bool => (fun b2: bool =>
    match b1 with
    | true => b2
    | false => false
    end) : bool -> bool.

사실 이거랑 같은거임 bool을 받아서 bool -> bool fun을 리턴
최종 타입은 bool -> bool -> bool

참고로 무한 루프로 빠지는 함수는 output이 수학적으로 결정이 되지 않음..
그래서 Rocq는 무한 루프로 빠질 가능성이 있는 함수는 애초에 type checking을 실패하도록 만들었음!
(만약 항상 terminate하는 함수를 Rocq가 받아들이지 않는다면 수학적으로 항상 terminate한다는 것을 증명시켜야 type checking 가능함;;) 이러면 call by value, call by name의 결과가 똑같아서 신경 안 쓰고, 또한 reduction의 순서를 어떻게 해도 항상 같은 reduced form으로 계산됨.

즉, bool -> (bool -> bool)로 보든, (bool -> bool) -> bool로 보든 상관 없다는 소리!
물론 실제 type checker는 단순한 프로그램이기 때문에 reduction 순서가 존재하긴 함;

Q) 이렇게 and를 써도 되는거 아님?

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
Definition and1 (b1:bool) (b2:bool) :=
  match b1 with
  | true => b2
  | false => false
  end.

Definition and2 (b1:bool) :=
  match b1 with
  | true => (fun b2: bool => b2)
  | false => fun _ => false
  end.

Definition and3 (b1:bool) (b2:bool) :=
  match b2 with
  | true => b1
  | false => false
  end.

"사람이 보기엔" 같은 함수가 맞음
But 계산 방식이 다르기 때문에 Rocq가 보기엔 같은 함수가 아님...

정확히 말하자면 이 세 함수가 같다는 사실은 자명하지 않음
Rocq에서는 세 함수가 같다는 사실을 증명해야 함!

if then else

bool의 match는 Rocq에서 if then else로 바꿔줌
match랑 완전 똑같지만 단순 syntax sugar임

1
2
3
4
5
6
Definition negb' (b:bool) : bool :=
  if b then false else true.
Definition andb' (b1:bool) (b2:bool) : bool :=
  if b1 then b2 else false.
Definition orb' (b1:bool) (b2:bool) : bool :=
  if b1 then true else b2.

사실 bool은 엄밀히 따지면 builtin이 아니라 standard library에 속함!
그래서 if then else는 bool이 아니여도 쓸 수 있음...!! (실용성은 글쎄..)

1
2
3
4
5
6
7
8
9
Inductive bw : Type :=
| bw_black
| bw_white.

Definition invert (x: bw) : bw :=
  if x then bw_white
  else bw_black.

Compute (invert bw_black). (* bw_white : bw *)

정확히 clause가 2개인 모든 Inductive는 if then else syntax를 사용할 수 있음!
이때 첫 번째 clause를 true(?)로 취급함

Notation

1
2
3
Notation "x && y" := (andb x y).
Notation "x || y" := (orb x y).
Compute false || false || true. (* true: bool *)

Rocq에서는 내 맘대로 syntax를 정할 수 있음!!
예를 들어 위 Notation을 사용하면 다른 프로그래밍 언어처럼 &&랑 ||로 bool 값들을 계산할 수 있음!

Constructors

1
2
3
4
5
6
7
8
Inductive rgb : Type :=
  | red
  | green
  | blue.
Inductive color : Type :=
  | black
  | white
  | primary (p : rgb).

Inductive로부터 다른 Inductive를 정의할 수도 있음.
사실 여기서 primary는 rgb->color, 즉 함수임!

color는 black, white, primary red, primary green, primary blue 5개가 있는 set이라고 생각하면 됨
primary라는 함수를 갖고 있는 set이라고 생각하면 안 됨!

1
2
3
4
5
6
7
Definition isred (c : color) : bool :=
  match c with
  | black => false
  | white => false
  | primary red => true
  | primary _ => false
  end.

이런 식으로 constructor 전체나 일부를 matching할 수 있음.
사실 이것도 syntax sugar임! 원래는 Inductive에 정의된 모든 clause에 대해서 match해야 함.

1
2
3
4
5
6
7
8
9
10
11
Definition isred (c : color) : bool :=
  match c with
  | black => false
  | white => false
  | primary p =>
      match p with
      | red => true
      | green => false
      | blue => false
      end
  end.

primary red랑 primary _를 풀어쓰면 이렇게 생겼을거임

Module

1
2
3
4
5
6
7
8
Module Playground.
  Definition foo : rgb := blue.
End Playground.

Definition foo : bool := true.

Check Playground.foo : rgb.
Check foo : bool.

단순한 이름을 숨기는 목적을 갖고 있지만... 나중에 진짜 의미가 나온다고 함..?

Tuples

1
2
3
4
5
6
7
8
9
10
11
12
13
Inductive bit : Type :=
  | B1
  | B0.
Inductive nybble : Type :=
  | bits (b0 b1 b2 b3 : bit).

Check (bits B1 B0 B1 B0): nybble.

Definition all_zero (nb : nybble) : bool :=
  match nb with
  | (bits B0 B0 B0 B0) => true
  | (bits _ _ _ _) => false
  end.

Tuple을 사용해서 여러 Inductive가 묶여있는 타입을 정의할 수 있음.
c.f. 앞서 말한대로 첫 번째 clause를 true로 취급하기 때문에 Rocq에선 1 0 순서로 씀;

사실 이것도 syntax sugar고 match는 원래 모든 clause에 대해서 다 쓰는게 맞음...

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
Definition all_zero' (nb : nybble) : bool :=
  match nb with
  | (bits b0 b1 b2 b3) =>
    match b0 with
    | B0 => match b1 with
            | B0 => match b2 with
                    | B0 => match b3 with
                            | B0 => true
                            | B1 => false
                            end
                    | B1 => false
                    end
            | B1 => false
            end
    | B1 => false
    end
  end.

Nat

Problem) 지금은 유한한 set밖에 못 만듦
자연수같은 무한한 set은 어떻게 만듦?

1
2
3
Inductive nat: Type :=
  | O
  | S (n : nat).

Rocq에서는 nat으로 자연수를 정의하고 있음.
0은 O, 1은 S O, 2는 S S O, ...

lambda calculus에서 자연수를 정의했던 방식이랑 비슷함!
c.f. n=λf.λx.fn(x)n = \lambda f. \lambda x. f^n(x)

자연수는 너무 많이 쓰이기 때문에 특별하게 자연수는 알아서 계산해서 보여줌
예를 들어 Check (S (S (S (S O)))).는 알아서 4 : nat로 계산해서 나옴.

1
2
Set Printing All.
Check 5. (* S (S (S (S (S O)))) *)

이게 싫다면 Set Printing All.으로 syntax sugar를 꺼버릴 수 있다...

1
2
3
4
5
6
7
Inductive nat: Type :=
  | O
  | S (n : nat).

Inductive otherNat: Type :=
  | baba
  | fofo (jiji : otherNat).

사실 위의 otherNat이랑 nat은 같은 집합이지만 Rocq는 두 집합이 같다는 증명을 할 수가 없음...
심지어 otherNat이랑 nat이 다르다는 증명도 할 수가 없음!
Rocq에서는 두 집합이 같다는 증명을 할 수 없다는게 증명되어있음!

1
2
3
4
5
Definition pred (n : nat) : nat :=
  match n with
  | O => O
  | S n' => n'
  end.

-1은 이렇게 정의되어 있음
음수는 일단 나중에

c.f. S도 따지고 보면 nat -> nat인데 +1의 역할을 하는 것 아니냐?
하지만 pred와 S는 조금 다른데 pred는 계산을 하는 함수지만 S는 그냥 element를 만드는 정의임.
사실 S는 애초에 계산을 하지도 않음! (e.g. S O는 더 이상 reduce할 수 없음)

아래에서 설명하는 Fixpoint를 쓰면 덧셈 뺄셈 등등도 정의할 수 있음! n m: nat은 같은 타입 인자 여러 개를 한번에 정의시켜주는 syntax sugar임

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
Fixpoint plus (n m : nat) : nat :=
  match n with
  | O => m
  | S n' => S (plus n' m)
  end.

Compute (plus 3 4).

Fixpoint minus (n m : nat) : nat :=
  match n, m with
  | O, _ => O
  | n, O => n
  | S n', S m' => minus n' m'
  end.

Compute (minus 6 2).

Fixpoint mult (n m : nat) : nat :=
  match n with
  | O => O
  | S n' => plus m (mult n' m)
  end.

Compute (mult 3 3).

Fixpoint exp (base power : nat) : nat :=
  match power with
  | O => S O
  | S p => mult base (exp base p)
  end.

Compute (exp 2 10).

Notation "x + y" := (plus x y)
                       (at level 50, left associativity)
                       : nat_scope.
Notation "x - y" := (minus x y)
                       (at level 50, left associativity)
                       : nat_scope.
Notation "x * y" := (mult x y)
                       (at level 40, left associativity)
                       : nat_scope.
Compute ((1 + 3 - 2) * 5).

(Notation 뒤쪽에 나오는건 연산자 우선순위, 연산 방향 같은거 정의해준거임)
등호나 부등호도 두 nat을 받아서 bool을 내놓는 함수로 정의할 수 있음!

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
Fixpoint eqb (n m : nat) : bool :=
  match n with
  | O => match m with
         | O => true
         | S m' => false
         end
  | S n' => match m with
            | O => false
            | S m' => eqb n' m'
            end
  end.

Fixpoint leb (n m : nat) : bool :=
  match n with
  | O => true
  | S n' =>
      match m with
      | O => false
      | S m' => leb n' m'
      end
  end.

Notation "x =? y" := (eqb x y) (at level 70) : nat_scope.
Notation "x <=? y" := (leb x y) (at level 70) : nat_scope.
Compute (4 <=? 2).

Fixpoint

Fixpoint를 쓰면 Definition과 달리 재귀함수를 정의할 수 있음.
Definition은 계산을 한 번만 하지만 Fixpoint는 계산을 몇 번 할지 모름!

1
2
3
4
5
6
Fixpoint even (n:nat) : bool :=
  match n with
  | O => true
  | S O => false
  | S (S n') => even n'
  end.

Q) 그냥 Fixpoint만 쓰면 안 됨?
A) 그냥 Readability 용도임 전부 Fixpoint로 써도 되긴 하는데 Definition이라고 쓰면 재귀가 없다는게 확실해짐
c.f. Inductive에도 비슷한게 있음... 사실 Inductive가 Fixpoint에 가까운 형태임!
Variant는 Inductive랑 똑같지만 Definition처럼 재귀를 허용하지 않는 형태임. (nat 같은 것 정의 불가)

Fixpoint도 syntax sugar지만... 굳이 lambda function 형태로 재귀함수를 쓰고 싶다면 fun 대신 fix를 쓰고 알 수 없는 이유로 반드시 :=를 써야 함
재귀함수의 함수명은 아무거나 써도 되지만 관례상 self를 쓴다고 함

1
2
3
4
5
6
Compute (fix self n :=
  match n with
  | O => true
  | S O => false
  | S (S n') => self n'
  end) 5.

참고로 앞서 말한대로 Rocq 함수는 반드시 끝나야함
아래 함수는 Rocq이 보기에 안 끝날 수도 있는 함수라 reject됨

1
2
3
4
5
6
Fixpoint even (n:nat) : bool :=
  match n with
  | O => true
  | S O => false
  | S (S n') => even (S (S n'))
  end.

하지만 당연히 끝나는 함수도 Rocq이 멍청해서 안 끝난다고 판단할 수도 있음...

1
2
3
4
5
6
7
8
(* 외않됨 *)

Fixpoint iszero (n:nat) : bool :=
  match n with
  | O => true
  | S O => false
  | S (S n') => iszero (S n')
  end.

하지만 모든 끝나는 함수는 Rocq가 끝난다는 것을 알 수 있게 만들 수 있다는 증명이 있다고 함?

Mutual recursion

1
2
3
4
5
6
7
8
9
10
11
12
Fixpoint even (n: nat) : bool :=
  match n with
  | O => true
  | S n' => odd n'
  end
with odd (n: nat) : bool :=
  match n with
  | O => false
  | S n' => even n'
  end.

Compute (even 4).

Mutual recursion도 가능함! with를 써서 두 함수를 동시에 정의할 수 있음.
만약 even만 정의하고 싶고 odd는 숨기고 싶다면 let in을 써야함

1
2
3
4
5
6
7
8
9
10
Fixpoint even (n: nat) : bool :=
  let odd := (fix self n := match n with
    | O => false
    | S n' => even n'
    end)
  in
  match n with
  | O => true
  | S n' => odd n'
  end.

물론 mutual recursion은 syntax sugar라서 없애버릴수는 있긴 함...

1
2
3
4
5
6
7
8
9
10
11
12
13
14
Definition _even (odd: nat -> bool) (n: nat) : bool :=
  match n with
  | O => true
  | S n' => odd n'
  end.
Definition _odd (even: nat -> bool) (n: nat) : bool :=
  match n with
  | O => false
  | S n' => even n'
  end.
Fixpoint even (n: nat) : bool :=
  _even (_odd even) n.
Fixpoint odd (n: nat) : bool :=
  _odd (_even odd) n.

좀 더 현실적인 방법으로는 일반적으로 tuple로 묶어서 recursion을 동시에 돌리는 방법이 있음

1
2
3
4
5
6
7
8
9
10
11
Fixpoint evenodd (n : nat) : bool * bool :=
  match n with
  | O     => (true, false)
  | S n'  =>
    match evenodd n' with
    | (e, o) => (o, e)
    end
  end.

Definition even (n : nat) : bool := fst (evenodd n).
Definition odd  (n : nat) : bool := snd (evenodd n).

Proof

Rocq에선 놀랍게도 1+1 = 2를 간단하게 증명할 수 있음!

1
2
Example plus_1_1 : 1 + 1 = 2.
Proof. reflexivity. Qed.

이게 왜 증명임?
사실 아래랑 같은 말임

1
Definition plus_1_1' : 1 + 1 = 2 := eq_refl.

즉, 위에서 쓴 Proof는 사실 type checking 과정임!
하지만 사람이 조금이라도 더 알아먹기 쉽게 Proof와 tactic들로 증명하게 하는 것.

Rocq에서 =는 사실 Inductive로 정의된 set(+ Notation)으로, 1 + 1 = 2는 사실 @eq nat (1 + 1) 2임.
Print eq.로 정의를 보면 아래처럼 나와있음.

1
2
Inductive eq (A : Type) (x : A) : A -> Prop :=
| eq_refl : eq A x x.

사실 이 Inductive는 지금까지 본 Inductive보다 더 general한 버전인 Inductive family임.
A -> Prop이라는건 임의의 A를 받아서 Prop을 내놓는다는 거임. (Prop은 대충 Type이라고 생각하자)
즉 eq nat 1 1, eq nat 1 2 이런건 전부 Type임! 다른 언어의 Generics처럼 Inductive family로 수많은 Type을 한번에 정의했다고 생각해도 됨.
근데 이 Inductive의 construct은 eq_refl: eq A x x밖에 없기 때문에 eq nat 1 1의 element는 construct할 수 있는데 eq nat 1 2의 element는 construct할 수 없음.
즉 1 = 1은 참이지만 1 = 2는 거짓이다!

위 정의를 좀 더 쉽게 바꾸면

1
2
Inductive eq' (A : Type) : A -> A -> Type :=
| eq_refl (x: A) : eq' A x x.

eq는 어떤 set A가 주어졌을 때, A의 element 두 개를 받고 set을 내놓는거라고 볼 수 있음
근데 construct가 eq_refl밖에 없으므로 주어진 두 element가 똑같을 때만 construct 됨.
eq A a b는 a, b가 같다면 원소가 있는 set, a, b가 다르다면 원소가 없는 set이 된다!

그럼 a와 b가 같다는 증명은 어떻게 하냐? 실제로 원소가 있다는 것을 보여주면 됨.
Rocq 식으로 표현하면 eq A a b 타입인 element를 찾으면 되는거고,
더 일반적으로는 Proposition 타입인 Proof를 만들면 Proposition이 참이라는 것을 증명한 것임.
즉, 단순한 type checking으로 증명할 수 있고, "증명을 코딩"한다는건 Proof를 type checking 통과하도록 코딩한다는 소리임.

이렇게 보면 뭔가 특별해보이지만 사실 type checking rule은 아래 세 가지 경우에서 모두 똑같음! 지금까지 우리가 쓰던 type checking rule을 Set, Prop, Type에서 똑같이 사용함.
다만 용도를 조금 구분하기 위해 Rocq 내부적으로는 Set이랑 Prop이라는 새로운 Type을 만들어서 사용중임.

  • element: Set
  • proof: Prop
  • program: Type
1
2
Definition plus_2_2 : 2+2 = 4 := @eq_refl nat 4.
Definition plus_2_2' : @eq nat (2+2) 4 := @eq_refl nat 4.

예시로 2+2 = 4를 보면 (@eq랑 =는 같은거임) 2+2 = 4는 2+2 = 4가 맞다는 set인데, @eq_refl nat 4가 이 set의 element로 type checking됐다는 소리는 2+2 = 4라는 set에 원소가 있다는거임.
근데 앞서 말했던대로 set에 원소가 있다는거 자체가 2+2 = 4는 참이라는거임.
즉, type checking이 성공했다는 것 자체가 2+2 = 4는 참이라는 증명이다!

c.f. A랑 B가 둘다 C로 reduction이 되면 A, B는 convertable하다고 함. (서로 바꿀 수 있다)
Rocq에서 계산이 되는 경우 reduction은 알아서 해줘서 2+2는 알아서 4가 됨
사실 우리는 4 = 4를 증명하고 있었던 것;;

c.f. Definition what: 1+1 = 3 := 1+1 = 3. 같은건 올바른 증명이 아님!!
1+1 = 3 : Type이고, what: 1+1 = 3임. Element와 Type은 다르다!
당연히 Type은 Type의 element일 수가 없음 (2: nat이지 nat: nat이 아니다..)

Q. 1+1 = 2, 2+2 = 4 같은 걸 쓸 때마다 계속 타입을 만듦?
A. 그건 C, Rust같이 어셈블리 만들어야 하는 애들이나 그러는거고 functional language는 물론이고, C나 Rust도 type checking 과정에선 polynomial type 상태를 유지하면서 type checking 가능함 (심지어 아래에 나오는 forall 같은 경우도 type checking이 됨!)

1
2
(* 이건 Typechecking 안 됨 *)
Definition foo (n: nat) : (n + 1) = (1 + n) := @eq_refl nat (S n).

위에껀 non-trivial함!
1 + n은 S n으로 reduction이 되긴 하지만, n + 1은 n을 몰라서 reduction이 안 됨
그래서 같다는게 trivial하지 않아서 증명이 안 됨..

1
2
3
4
5
6
Lemma bar (n : nat) : n + 1 = 1 + n.
Proof.
  induction n.
  - simpl. reflexivity.
  - simpl. rewrite IHn. simpl. reflexivity.
Qed.

그래서 이렇게 수학적 귀납법을 써서 증명해야 함.
이게 우리가 일반적으로 Rocq에서 증명하는 과정임!

  • Lemma, Example, Theorem, Goal 등등은 전부 똑같은 keyword임; 증명하고 싶은 명제를 정의해줌 (Goal은 이름을 지정할 수 없다는 차이점이 있음)
  • Proof는 지금부터 명제를 증명할 프로그램을 짜겠다는 소리
  • induction, simpl, reflexivity 같은 tactic으로 프로그램을 작성함
  • Qed는 완성한 프로그램을 type checking 해서 맞는지 검사함.

Proof ~ Qed는 우리가 @eq_refl nat 4로 짜던 프로그램을 Rocq가 대신 짜주는 거라고 생각하면 됨.

e.g. simpl.이라는 tactic은 제일 단순한 형태로 reduction시킴
예를 들어 2+2 = 4라는 goal을 4 = 4로 만듦
정확히 말하면 기존 goal을 수정하는게 아니라 더 쉬운 goal을 증명하면 기존 goal을 증명할 수 있게 해주는거임!
즉, simpl.이란 tactic은 q: 4 = 4를 만족하는 q가 있다면 q를 사용해서 p: 2+2 = 4를 만족하는 p를 만들어주는 tactic임.
사실 reduction은 항상 하기 때문에 simpl.은 안 써도 되는 tactic이지만 사람이 알아보기 편하게 사용함..

실제로 만들어진 프로그램을 보고 싶으면 Print bar.를 해보면 됨!

1
2
3
4
5
6
7
8
9
10
Print bar.

(*
bar =
fun n : nat =>
nat_ind (fun n0 : nat => n0 + 1 = 1 + n0) (eq_refl : 0 + 1 = 1 + 0)
(fun (n0 : nat) (IHn : n0 + 1 = 1 + n0) => eq_ind_r (fun n1 : nat => S n1 = S (S n0)) (eq_refl : S (1 + n0) = S (S n0)) IHn :
S n0 + 1 = 1 + S n0) n
     : forall n : nat, n + 1 = 1 + n
*)

좀 더 알아듣기 쉽게 만들려면 unfold로 풀어쓸 수 있음.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
Lemma bar (n : nat) : n + 1 = 1 + n.
Proof.
  induction n.
  - simpl. reflexivity.
  - simpl. rewrite IHn. simpl. reflexivity.
Defined.
(* Defined로 끝내면 추후에 증명 내용을 사용할 수 있음. *)

Goal bar = bar.
unfold bar at 1.
unfold nat_ind.
unfold eq_ind_r.
unfold eq_ind.
unfold eq_sym.
(* Set Printing All. 쓰면 syntax sugar 다 없애버림 *)

(*
(fun n : nat =>
  (fix F (n0 : nat) : n0 + 1 = 1 + n0 :=
  match n0 as n1 return (n1 + 1 = 1 + n1) with
  | 0 => eq_refl
  | S n1 => match match F n1 in ([...]) return ([...]) with
      | eq_refl => eq_refl
      end in (_ = a) return (S a = S (S n1)) with
    | eq_refl => eq_refl
    end
  end) n) = bar
*)

참고로

1
2
Definition even (n: nat) : Type :=
  exists m: nat, n = 2 * m.

이렇게 하면 명제를 사용해서 성질을 나타낼 수가 있음!!
정확히 말하자면 even n은 n이 짝수라는 명제를 나타냄
even 4를 증명하면 4가 짝수라는 것을 나타낼 수 있음!

exists는 조건을 만족하는 m들의 집합을 나타냄
즉, 여기서 even은 n = 2 * m을 만족하는 m들의 집합으로 정의됨.
명제는 element가 있다면 참, 없다면 거짓이므로 n = 2 * m인 m이 있다면 even n은 참이 됨!

Tactics

아래 예제를 통해 다른 tactic들에 대해 알아보자!

1
2
3
4
Theorem plus_0_n : forall n : nat, 0 + n = n.
Proof.
  intros n. simpl. reflexivity.
Qed.

참고로 Require Import Utf8. 써주면 ∀로 forall을 대체할 수 있음!
e.g. Theorem plus_0_n : ∀ n : nat, 0 + n = n.
fun도 λ로 바뀌고 =>도 ⇒로 바뀌고 생각보다 유니코드로 바뀌는게 많음...

아니 근데 forall은 뭔데??
사실 그냥 function임 (n : nat) -> 0 + n = n
근데 우리가 알던 function A -> B랑 다른게 뭐냐?
우리가 지금까지 쓰던 A -> B는 non-dependent function; input/return type이 항상 같음
근데 (n : nat) -> 0 + n = n은 dependent function; input에 따라 return type이 다름!!
e.g. 1을 넣으면 return type은 0 + 1 = 1!

하여튼 (n : nat) -> 0 + n = n은 nat을 받아서 0 + n = n의 element를 내놓는 (즉 0 + n = n의 증명을 내놓는) 함수들의 집합임.
즉 plus_0_n : (n : nat) -> 0 + n = n이라는 프로그램이 있다면 이 집합에 속하는 element plus_0_n이 있다; 즉 이 집합은 공집합이 아니다; 즉 이 명제(모든 n에 대해서 0+n = n이다)를 증명할 수 있다!
사실 이거 n+0이면 non trivial해서 바로 증명 안 됨

intros

intros n.은 n을 fix시켜놓고 어떤 fix된 n 하나에 대해서 goal을 보이도록 만듦. 사실상 forall을 풀어주는 역할!

위 예시에선 n이 변수로 올라오고 goal은 0+n = n만 증명하면 됨

(단순히 forall만 풀어주는건 아니고 p -> q의 경우 가정 p를 올려주는 등 더 다양한 사용처가 있음)

simpl

앞서 봤던대로 simpl은 reduction을 알아서 해주는 역할, Rocq는 항상 reduction을 하기 때문에 안 써도 아무 문제 없음!

순수하게 사람이 알아보기 편하라고 만들어진 tactic임;
만약 너무 한번에 reduction이 돼서 이해하기가 어렵다면 simpl Nat.eqb.처럼 단계별로 reduction을 할 수 있음.

reflexivity

지금까지 봤던 eq_refl을 만들어주는 역할!
등호 양변이 같으면 goal을 풀어버림

induction

1
2
3
4
5
6
7
Theorem plus_n_0: forall n: nat, n + 0 = n.
Proof.
  intros n.
  induction n.
  - simpl. reflexivity.
  - simpl. rewrite IHn. reflexivity.
Qed.

0+n은 simpl.이 먹히지만 n+0은 simpl.이 안 먹힘..
이 경우 induction으로 수학적 귀납법을 써야 함!

induction n을 하면 2개의 subgoal을 만들어 냄

  1. n = 0일때 성립
  2. n 일때 성립하면 S n에서 성립

subgoal을 증명하고 싶으면 -를 사용해서 subgoal을 하나씩 증명할 수 있음.
c.f. subgoal 단계가 깊어지면 +, *, --, ++, **를 쓰거나 다른 프로그래밍 언어처럼 중괄호를 여닫는 식으로 subgoal을 표시할 수 있음.
아니면 아예 subgoal이 너무 많다면 ;를 사용해서 모든 subgoal마다 똑같은 tactic을 사용해서 증명하라고 할 수 있음!

rewrite

rewrite는 등식을 바꿔주는 tactic임.

위에서 induction을 하면 두 번째 subgoal에서 귀납가정이 (n일때 n + 0 = n이 성립) IHn이라는 이름으로 생기는데,
rewrite IHn.은 귀납가정을 사용해서 n + 0을 n으로 바꾸라는 소리임.

기본적으로 rewrite H.는 왼쪽에서 오른쪽으로 치환하지만,
rewrite <- H.로 쓰면 오른쪽에서 왼쪽으로 치환해줌.

destruct

1
2
3
4
5
6
7
8
9
10
11
Notation "x =? y" := (Nat.eqb x y) (at level 70) : nat_scope.

Theorem plus_1_neq_0: forall n: nat,
  ((n + 1) =? 0) = false.
Proof.
  intros n.
  simpl. (* n + 1은 reduction이 안 됨... *)
  destruct n.
  - simpl. reflexivity. (* 0 + 1은 reduction이 됨! *)
  - simpl. reflexivity. (* S n + 1은 reduction이 됨! *)
Qed.

destruct는 Introduction에서 정의했던 constructor들로 나눠버림

이게 뭔 소리냐? 위의 경우에는 n은 nat임
이때 그냥 nat을 정의했던대로 O인 경우, S n인 경우로 풀어서 쓸 수 있음!

원래 (n + 1 =? 0) = false인 goal을 두 개의 subgoal (0 + 1 =? 0) = false이랑 (S n + 1 =? 0) = false으로 풀어줌.
만약 두 subgoal 모두 증명된다면 모든 constructor에서 증명했으니 모든 nat에 대해서 증명한게 되는거임!

사실 보통은 destruct n as [| n'] eqn:E.로 씀
n'은 n 돌려쓰면 헷갈리니까 subgoal에서는 S n'처럼 다른 변수로 쓰라고 하는거고,
eqn:E는 destruct한 가정을 E로 정의함 (첫 번째 subgoal에선 E: n = 0, 두 번째 subgoal에선 E: n = S n')

induction도 비슷하게 induction n as [| n' IHn']처럼 정의할 수 있음!

Rocq의 한계?

Rocq는 constructive logic이기 때문에 명제를 증명할 때는 항상 실제로 증명 방법을 제시해야 함.
하지만 constructive하게 증명을 만들어낼 수 없는 명제도 있음...

1
2
3
Theorem baejungrule: forall p: Prop,
  p \/ ~p.
Proof. Admitted.

이런 명제들은 Rocq에서 참이라는 증명을 할 수가 없음...
왜냐? evidence(실제 증명)을 줄 수가 없음 만약 evidence를 만들 수 있으면 p에 밀레니엄 문제 넣고 참인 evidence가 있는지 거짓인 evidence가 있는지 보고 10억 타면 됨
Rocq는 반드시 프로그램을 짜야 증명이 되기 때문에, 저걸 증명하려면 p의 프로그램을 짜거나 ~p의 프로그램을 짜야함. 하지만 이걸 임의의 Prop에 대해서 증명할 수가 없음...

이런 경우 Adimitted.를 써서 강제로 증명하거나 아예 Axiom baejungrule: forall p: Prop, p \/ ~p.처럼 애초에 이 명제는 참이라고 정의할 수 있음.
하지만 이렇게 하면 Rocq를 사용하는 이유인 엄밀성이 깨지니까 웬만하면 쓰지 말자...

c.f. 괴델의 불완전성 정리: 수학체계는 스스로 수학체계가 무모순이라는 증명을 할 수가 없음