7.5. Pitfalls of Programming with Dependent Types
종속 타입의 유연성은 타입 언어가 표현력이 낮은 타입 시스템으로는 기술할 수 없는 변형까지 표현할 수 있게 하므로 더 유용한 프로그램을 타입 검사기가 받아들이게 한다. 동시에 종속 타입이 매우 세밀한 명세를 표현할 수 있어 더 많은 버그 있는 프로그램을 타입 검사기가 거부하게 한다. 이 능력에는 비용이 따른다.
Row처럼 타입을 반환하는 함수의 내부와 그 함수가 생성하는 타입이 강하게 결합되는 현상은 더 큰 어려움의 한 사례다. 함수를 타입에서 사용하면 함수의 인터페이스와 구현의 구분이 무너지기 시작한다.
보통 함수의 타입 서명이나 입력-출력 동작을 바꾸지 않는 한 모든 리팩터링은 유효하다.
클라이언트 코드를 깨뜨리지 않고 더 효율적인 알고리즘과 자료구조를 사용하도록 함수를 다시 쓰고, 버그를 고치고, 코드의 명확성을 높일 수 있다.
그러나 함수를 타입에서 사용하면 구현의 내부가 타입의 일부가 되고, 따라서 다른 프로그램에 대한 인터페이스의 일부가 된다.
예로 Nat의 덧셈을 구현한 다음 두 가지를 보자.
Nat.plusL은 첫 번째 인자에 대해 재귀적이다:
def Nat.plusL : Nat → Nat → Nat
| 0, k => k
| n + 1, k => plusL n k + 1
반면 Nat.plusR은 두 번째 인자에 대해 재귀적이다:
def Nat.plusR : Nat → Nat → Nat
| n, 0 => n
| n, k + 1 => plusR n k + 1두 덧셈 구현은 바탕의 수학적 개념을 충실히 따르므로 같은 인자에 같은 결과를 반환한다.
그러나 이 두 구현은 타입에서 사용될 때 상당히 다른 인터페이스를 제공한다.
예를 들어 두 Vect를 덧붙이는 함수를 생각하자.
이 함수는 인자 길이의 합을 길이로 갖는 Vect를 반환해야 한다.
Vect는 더 많은 정보를 담은 타입을 가진 List와 본질적으로 같으므로 List.append처럼 첫 번째 인자에 패턴 매칭과 재귀를 적용해 작성하는 것이 자연스럽다.
타입 서명과 자리표시자를 가리키는 초기 패턴 매칭에서 시작하면 두 메시지가 나온다:
def appendL : Vect α n → Vect α k → Vect α (n.plusL k)
| .nil, ys => _
| .cons x xs, ys => _
첫 번째 메시지의 nil 경우는 자리표시자를 길이 plusL 0 k인 Vect로 바꿔야 한다고 말한다:
두 번째 메시지의 cons 경우는 자리표시자를 길이 plusL (n✝ + 1) k인 Vect로 바꿔야 한다고 말한다:
n 뒤의 대거 기호는 Lean이 내부적으로 만든 이름을 나타낸다.
내부적으로 첫 번째 Vect에 패턴 매칭을 적용하면 첫 번째 Nat의 값도 암묵적으로 정제된다. cons 생성자의 인덱스가 n + 1이고 Vect 꼬리의 길이가 n이기 때문이다.
여기서 n✝은 인자 n보다 1 작은 Nat을 나타낸다.
7.5.1. Definitional Equality
plusL의 정의에는 0, k => k 패턴 경우가 있다.
이는 첫 번째 자리표시자에 사용된 길이에 적용되므로 자리표시자 타입 Vect α (Nat.plusL 0 k)을 Vect α k로도 쓸 수 있다.
마찬가지로 plusL에는 n + 1, k => plusL n k + 1 패턴 경우가 있다.
따라서 두 번째 자리표시자의 타입은 Vect α (plusL n✝ k + 1)로 동등하게 쓸 수 있다.
내부에서 일어나는 일을 드러내려면 먼저 Nat 인자를 명시적으로 써야 한다. 프로그램에 이름을 명시했으므로 오류 메시지에서도 대거가 사라진다:
def appendL : (n k : Nat) → Vect α n → Vect α k → Vect α (n.plusL k)
| 0, k, .nil, ys => _
| n + 1, k, .cons x xs, ys => _자리표시자에 타입의 단순화된 버전으로 주석을 달아도 타입 오류가 나지 않는다. 즉 프로그램에 쓴 타입이 Lean이 스스로 찾은 타입과 동등하다는 뜻이다:
def appendL : (n k : Nat) → Vect α n → Vect α k → Vect α (n.plusL k)
| 0, k, .nil, ys => (_ : Vect α k)
| n + 1, k, .cons x xs, ys => (_ : Vect α (n.plusL k + 1))
첫 번째 경우에는 Vect α k가 필요하고 ys가 바로 그 타입이다.
이는 빈 리스트를 다른 리스트에 덧붙이면 그 리스트가 반환되는 것과 같다.
첫 번째 자리표시자 대신 ys로 정의를 정제하면 채워야 할 자리표시자가 하나만 남는다:
def appendL : (n k : Nat) → Vect α n → Vect α k → Vect α (n.plusL k)
| 0, k, .nil, ys => ys
| n + 1, k, .cons x xs, ys => (_ : Vect α (n.plusL k + 1))
여기서 매우 중요한 일이 일어났다.
Lean이 Vect α (Nat.plusL 0 k)를 예상한 문맥에서 Vect α k를 받았다.
하지만 Nat.plusL은 abbrev가 아니므로 타입 검사 중 실행되면 안 될 것처럼 보인다.
다른 일이 일어나고 있다.
핵심은 Lean이 타입 검사 중 abbrev만 전개하는 것이 아니라는 점이다.
두 타입이 동등한지 검사할 때도 계산을 수행하므로 한 타입의 표현식을 다른 타입을 예상하는 문맥에서 사용할 수 있다.
이 성질을 정의적 동등성이라고 하며 미묘한 성질이다.
당연히 똑같이 쓰인 두 타입은 정의적으로 동등하다. Nat과 Nat, 또는 List String과 List String은 같다고 보아야 한다.
서로 다른 데이터 타입으로 만든 두 구체 타입은 같지 않으므로 List Nat은 Int와 다르다.
내부 이름만 바꾼 타입도 같으므로 (n : Nat) → Vect String n은 (k : Nat) → Vect String k와 같다.
타입은 일반 데이터를 포함할 수 있으므로 정의적 동등성은 데이터가 언제 같은지도 설명해야 한다.
같은 생성자의 사용은 같으므로 0은 0과 같고 [5, 3, 1]은 [5, 3, 1]과 같다.
그러나 타입에는 함수 화살표, 데이터 타입, 생성자만 있는 것이 아니다.
타입에는 변수와 함수도 들어 있다.
변수의 정의적 동등성은 비교적 간단하다. 각 변수는 자기 자신과만 같으므로 (n k : Nat) → Vect Int n은 (n k : Nat) → Vect Int k와 정의적으로 동등하지 않다.
반면 함수는 더 복잡하다.
수학에서는 입력과 출력의 동작이 동일하면 두 함수를 같다고 보지만, 이를 확인할 효율적인 알고리즘은 없다. 게다가 정의적 동등성의 핵심 목적은 Lean이 두 타입을 서로 바꾸어 써도 되는지 확인하게 하는 것이다.
대신 Lean은 두 함수가 모두 정의적으로 동등한 본문을 가진 fun 표현식일 때 정의적으로 동등하다고 본다.
다시 말해 정의적으로 동등하려면 두 함수가 같은 도우미 함수를 호출하는 같은 알고리즘을 사용해야 한다.
이는 보통 그다지 유용하지 않으므로, 함수의 정의적 동등성은 주로 두 타입에 정확히 같은 정의된 함수가 나타날 때 사용된다.
타입에서 함수가 호출되면 정의적 동등성을 검사하는 과정에 함수 호출을 줄이는 일이 포함될 수 있다.
1 + 4가 3 + 2와 정의적으로 동등하므로, Vect String (1 + 4) 타입은 Vect String (3 + 2) 타입과 정의적으로 동등하다.
둘이 같은지 확인하려면 두 식을 모두 5로 줄인 다음 생성자 규칙을 다섯 번 적용하면 된다.
데이터에 적용된 함수의 정의적 동등성은 먼저 두 식이 이미 같은지 확인해서 검사할 수 있다. 예를 들어 ["a", "b"] ++ ["c"]가 ["a", "b"] ++ ["c"]와 같은지 확인하기 위해 굳이 줄일 필요는 없다.
이미 같지 않다면 함수를 호출해 그 값으로 바꾼 다음, 그 값을 검사할 수 있다.
모든 함수 인자가 구체적인 데이터인 것은 아니다.
예를 들어 타입에는 zero와 succ 생성자로 만들어지지 않은 Nat도 들어갈 수 있다.
(n : Nat) → Vect String n 타입에서 변수 n은 Nat이지만, 함수를 호출하기 전에는 그것이 어떤 Nat인지 알 수 없다.
실제로 이 함수는 처음에는 0으로 호출되고, 나중에는 17로, 다시 33으로 호출될 수 있다.
appendL의 정의에서 보았듯이, Nat 타입의 변수는 plusL 같은 함수에 전달될 수도 있다.
실제로 (n : Nat) → Vect String n 타입은 (n : Nat) → Vect String (Nat.plusL 0 n) 타입과 정의적으로 동등하다.
n과 Nat.plusL 0 n이 정의적으로 동등한 이유는 plusL의 패턴 매칭이 첫 번째 인자를 살펴보기 때문이다.
이는 문제가 된다. 0은 덧셈의 왼쪽 항등원이자 오른쪽 항등원이어야 하지만, (n : Nat) → Vect String n은 (n : Nat) → Vect String (Nat.plusL n 0)과 정의적으로 동등하지 않다.
패턴 매칭은 변수를 만나면 막히기 때문이다.
n의 실제 값이 알려지기 전에는 Nat.plusL n 0의 어느 경우를 선택해야 하는지 알 방법이 없다.
쿼리 예제의 Row 함수에서도 같은 문제가 나타난다.
Row (c :: cs) 타입이 어떤 데이터 타입으로도 줄어들지 않는 이유는 Row의 정의가 원소가 하나인 리스트와 원소가 둘 이상인 리스트에 대해 별도의 경우를 갖기 때문이다.
다시 말해 구체적인 List 생성자와 변수 cs를 매칭하려 할 때 계산이 막힌다.
따라서 Row를 분해하거나 구성하는 거의 모든 함수가 Row 자체와 같은 세 경우를 매칭해야 한다. 막힌 계산을 풀면 패턴 매칭이나 생성자에 사용할 수 있는 구체적인 타입이 드러난다.
appendL에서 빠진 경우에는 Vect α (Nat.plusL n k + 1)이 필요하다.
인덱스의 + 1은 다음 단계에서 Vect.cons를 사용해야 함을 암시한다.
def appendL : (n k : Nat) → Vect α n → Vect α k → Vect α (n.plusL k)
| 0, k, .nil, ys => ys
| n + 1, k, .cons x xs, ys => .cons x (_ : Vect α (n.plusL k))
appendL을 재귀 호출하면 원하는 길이의 Vect를 구성할 수 있다.
def appendL : (n k : Nat) → Vect α n → Vect α k → Vect α (n.plusL k)
| 0, k, .nil, ys => ys
| n + 1, k, .cons x xs, ys => .cons x (appendL n k xs ys)
프로그램이 완성되었으므로 n과 k에 대한 명시적인 매칭을 없애면 함수를 읽고 호출하기가 더 쉬워진다.
def appendL : Vect α n → Vect α k → Vect α (n.plusL k)
| .nil, ys => ys
| .cons x xs, ys => .cons x (appendL xs ys)
정의적 동등성을 사용해 타입을 비교하면 함수 정의의 내부를 비롯해 정의적 동등성에 관여하는 모든 것이 종속 타입과 인덱스 패밀리를 사용하는 프로그램의 인터페이스 일부가 된다.
타입에서 함수의 내부를 드러내면 드러난 프로그램을 리팩터링할 때 그 함수를 사용하는 프로그램이 더 이상 타입 검사를 통과하지 못할 수 있다.
특히 appendL의 타입에서 plusL을 사용하므로, 그 밖의 동작은 동등한 plusR로 plusL의 정의를 바꿀 수 없다.
7.5.2. Getting Stuck on Addition
append를 대신 plusR로 정의하면 어떻게 될까?
같은 방식으로 각 경우에 길이를 명시하고 자리표시자 밑줄을 넣어 시작하면 다음과 같은 유용한 오류 메시지가 나타난다.
def appendR : (n k : Nat) → Vect α n → Vect α k → Vect α (n.plusR k)
| 0, k, .nil, ys => _
| n + 1, k, .cons x xs, ys => _
그러나 첫 번째 자리표시자에 Vect α k 타입 주석을 붙이면 타입 불일치 오류가 발생한다.
def appendR : (n k : Nat) → Vect α n → Vect α k → Vect α (n.plusR k)
| 0, k, .nil, ys => (_ : Vect α k)
| n + 1, k, .cons x xs, ys => _
이 오류는 Nat.plusR 0 k와 k가 정의적으로 동등하지 않다는 뜻이다.
이는 plusR의 정의가 다음과 같기 때문이다.
def Nat.plusR : Nat → Nat → Nat
| n, 0 => n
| n, k + 1 => plusR n k + 1
이 함수는 첫 번째 인자가 아니라 두 번째 인자에 대해 패턴 매칭을 수행한다. 따라서 그 자리에 변수 k가 있으면 계산이 줄어들지 않는다.
Lean 표준 라이브러리의 Nat.add는 plusL이 아니라 plusR와 동등하다. 그러므로 이 정의에서 사용하려 하면 정확히 같은 어려움이 생긴다.
def appendR : (n k : Nat) → Vect α n → Vect α k → Vect α (n + k)
| 0, k, .nil, ys => (_ : Vect α k)
| n + 1, k, .cons x xs, ys => _덧셈 계산이 변수에서 막힌다. 이를 풀려면 명제적 동등성이 필요하다.
7.5.3. Propositional Equality
명제적 동등성은 두 표현식이 같다는 수학적 명제다. 정의적 동등성이 필요할 때 Lean이 자동으로 검사하는 일종의 주변 사실인 반면, 명제적 동등성에 관한 명제에는 명시적인 증명이 필요하다. 동등성 명제를 한 번 증명하면 프로그램에서 이를 사용해 타입의 한쪽을 동등성의 다른 쪽으로 바꿀 수 있고, 그 결과 타입 검사기가 막힌 상태를 풀 수 있다.
정의적 동등성이 이처럼 제한적인 이유는 알고리즘으로 검사할 수 있게 하려는 것이다. 명제적 동등성은 훨씬 풍부하지만, 컴퓨터는 일반적으로 두 표현식이 명제적으로 동등한지 검사할 수 없다. 다만 어떤 증명이라고 제시된 것이 실제로 증명인지 여부는 확인할 수 있다. 정의적 동등성과 명제적 동등성을 나누는 것은 인간과 기계의 역할 분담을 나타낸다. 가장 지루한 동등성은 정의적 동등성의 일부로 자동 검사하고, 사람은 명제적 동등성에서 다룰 만한 흥미로운 문제에 집중할 수 있다. 마찬가지로 타입 검사기는 정의적 동등성을 자동으로 호출하지만, 명제적 동등성은 명시적으로 사용해야 한다.
명제, 증명, 인덱싱에서는 일부 동등성 명제를 decide를 사용해 증명한다.
이 동등성 명제들은 모두 실제로는 이미 정의적 동등성인 명제다.
보통 명제적 동등성 명제는 먼저 정의적 동등성이거나 이미 증명된 동등성에 충분히 가까운 형태로 만든 다음, decide나 simp 같은 도구로 단순화된 경우를 처리해 증명한다.
simp 전술은 매우 강력하다. 내부적으로 빠르고 자동화된 여러 도구를 사용해 증명을 구성한다.
rfl이라는 더 간단한 전술은 명제적 동등성을 증명할 때 정의적 동등성을 직접 사용한다.
rfl이라는 이름은 반사성(reflexivity)을 줄인 말로, 모든 것이 자기 자신과 같다는 동등성의 성질을 뜻한다.
appendR의 막힌 계산을 풀려면 k = Nat.plusR 0 k라는 증명이 필요하다. plusR가 두 번째 인자의 변수에서 막히므로 이는 정의적 동등성이 아니다.
계산이 진행되게 하려면 k가 구체적인 생성자가 되어야 한다.
이 작업은 패턴 매칭으로 수행한다.
특히 k는 어떤 Nat일 수 있으므로, 이 작업에는 임의의 k에 대해 k = Nat.plusR 0 k라는 증거를 반환하는 함수가 필요하다.
이는 (k : Nat) → k = Nat.plusR 0 k 타입의 동등성 증명을 반환하는 함수여야 한다.
초기 패턴과 자리표시자를 넣어 작성을 시작하면 다음 메시지가 나타난다.
def plusR_zero_left : (k : Nat) → k = Nat.plusR 0 k
| 0 => _
| k + 1 => _
패턴 매칭으로 k를 0으로 구체화했으므로, 첫 번째 자리표시자는 정의적으로 성립하는 명제의 증거를 나타낸다.
rfl 전술로 이를 처리하면 두 번째 자리표시자만 남는다.
def plusR_zero_left : (k : Nat) → k = Nat.plusR 0 k
⊢ 0 = Nat.plusR 0 0 ⊢ 0 = Nat.plusR 0 0 All goals completed! 🐙
| k + 1 => _
두 번째 자리표시자는 조금 더 까다롭다.
Nat.plusR 0 k + 1 표현식은 Nat.plusR 0 (k + 1)과 정의적으로 동등하다.
따라서 목표를 k + 1 = Nat.plusR 0 k + 1로 써도 된다.
def plusR_zero_left : (k : Nat) → k = Nat.plusR 0 k
⊢ 0 = Nat.plusR 0 0 ⊢ 0 = Nat.plusR 0 0 All goals completed! 🐙
| k + 1 => (_ : k + 1 = Nat.plusR 0 k + 1)
동등성 명제의 양쪽에 있는 + 1 아래에는 이 함수 자체가 반환하는 것과 같은 형태가 다시 들어 있다.
다시 말해 k를 재귀 호출하면 k = Nat.plusR 0 k라는 증거를 반환한다.
함수 인자에 적용되지 않는다면 동등성이라고 할 수 없다.
즉 x = y이면 f x = f y이다.
표준 라이브러리에는 함수와 동등성 증명을 받아 동등성의 양쪽에 함수를 적용한 새 증명을 반환하는 congrArg 함수가 있다.
이 경우 함수는 (· + 1)이다.
def plusR_zero_left : (k : Nat) → k = Nat.plusR 0 k
⊢ 0 = Nat.plusR 0 0 ⊢ 0 = Nat.plusR 0 0 All goals completed! 🐙
| k + 1 =>
congrArg (· + 1) (plusR_zero_left k)
이는 실제로 명제의 증명이므로 theorem으로 선언해야 한다.
theorem plusR_zero_left : (k : Nat) → k = Nat.plusR 0 k
⊢ 0 = Nat.plusR 0 0 ⊢ 0 = Nat.plusR 0 0 All goals completed! 🐙
| k + 1 =>
congrArg (· + 1) (plusR_zero_left k)
프로그램에서는 오른쪽 삼각형 연산자 ▸를 사용해 명제적 동등성을 적용할 수 있다.
이 연산자는 첫 번째 인자로 동등성 증명을 받고 두 번째 인자로 다른 표현식을 받으며, 두 번째 인자의 타입에서 동등성의 한쪽을 다른 쪽으로 바꾼다.
다시 말해 다음 정의에는 타입 오류가 없다.
def appendR : (n k : Nat) → Vect α n → Vect α k → Vect α (n.plusR k)
| 0, k, .nil, ys => plusR_zero_left k ▸ (_ : Vect α k)
| n + 1, k, .cons x xs, ys => _첫 번째 자리표시자의 타입은 예상한 타입이다.
이제 ys로 채울 수 있다.
def appendR : (n k : Nat) → Vect α n → Vect α k → Vect α (n.plusR k)
| 0, k, .nil, ys => plusR_zero_left k ▸ ys
| n + 1, k, .cons x xs, ys => _남은 자리표시자를 채우려면 덧셈의 또 다른 막힌 계산을 풀어야 한다.
여기서 증명해야 할 명제는 Nat.plusR (n + 1) k = Nat.plusR n k + 1이다. 이 명제를 ▸와 함께 사용하면 표현식의 바깥으로 + 1을 끌어내 cons의 인덱스와 맞출 수 있다.
이 증명은 plusR의 두 번째 인자인 k에 대해 패턴 매칭하는 재귀 함수다.
plusR 자체가 두 번째 인자에 대해 패턴 매칭하기 때문에, 이 증명도 패턴 매칭을 통해 계산을 “막힘에서 풀어” 계산 동작을 드러낼 수 있다.
증명의 뼈대는 plusR_zero_left의 뼈대와 매우 비슷하다.
theorem plusR_succ_left (n : Nat) :
(k : Nat) → Nat.plusR (n + 1) k = Nat.plusR n k + 1
n:Nat⊢ (n + 1).plusR 0 = n.plusR 0 + 1 n:Nat⊢ (n + 1).plusR 0 = n.plusR 0 + 1 All goals completed! 🐙
| k + 1 => _
남은 경우의 타입은 Nat.plusR (n + 1) k + 1 = Nat.plusR n (k + 1) + 1과 정의적으로 동등하므로, plusR_zero_left에서처럼 congrArg로 풀 수 있다.
그러면 증명이 완성된다.
theorem plusR_succ_left (n : Nat) :
(k : Nat) → Nat.plusR (n + 1) k = Nat.plusR n k + 1
n:Nat⊢ (n + 1).plusR 0 = n.plusR 0 + 1 n:Nat⊢ (n + 1).plusR 0 = n.plusR 0 + 1 All goals completed! 🐙
| k + 1 => congrArg (· + 1) (plusR_succ_left n k)
완성된 증명을 사용하면 appendR의 두 번째 경우에서 막힌 계산을 풀 수 있다.
def appendR : (n k : Nat) → Vect α n → Vect α k → Vect α (n.plusR k)
| 0, k, .nil, ys =>
plusR_zero_left k ▸ ys
| n + 1, k, .cons x xs, ys =>
plusR_succ_left n k ▸ .cons x (appendR n k xs ys)
appendR의 길이 인자를 다시 암시적으로 만들면, 증명에서 참조할 수 있도록 그 인자에 명시적인 이름을 붙일 수 없게 된다.
그러나 타입을 일치시킬 수 있는 다른 값이 없으므로 Lean의 타입 검사기는 충분한 정보를 바탕으로 내부에서 이 인자들을 자동으로 채운다.
def appendR : Vect α n → Vect α k → Vect α (n.plusR k)
| .nil, ys => plusR_zero_left _ ▸ ys
| .cons x xs, ys => plusR_succ_left _ _ ▸ .cons x (appendR xs ys)7.5.4. Pros and Cons
인덱스 패밀리에는 중요한 성질이 있다. 인덱스 패밀리에 대한 패턴 매칭이 정의적 동등성에 영향을 준다는 것이다.
예를 들어 Vect에 대한 match 표현식에서 nil 경우를 만나면 길이가 단순히 0이 된다.
정의적 동등성은 항상 활성화되어 있고 명시적으로 호출할 필요가 없으므로 매우 편리할 수 있다.
그러나 종속 타입 및 패턴 매칭과 함께 정의적 동등성을 사용하면 소프트웨어 공학 측면에서 심각한 단점이 생긴다. 첫째, 함수를 타입에서 사용할 수 있도록 특별히 작성해야 하며, 타입에서 사용하기 편리한 함수가 가장 효율적인 알고리즘을 사용하지 않을 수도 있다. 함수를 타입에서 사용해 그 내부를 드러내고 나면 구현이 인터페이스의 일부가 되므로 이후 리팩터링이 어려워진다. 둘째, 정의적 동등성은 느릴 수 있다. 두 표현식이 정의적으로 동등한지 검사할 때 해당 함수가 복잡하고 추상화 계층이 많으면 Lean이 많은 코드를 실행해야 할 수 있다. 셋째, 정의적 동등성 검사 실패로 생기는 오류 메시지는 함수의 내부를 기준으로 표현될 수 있어 항상 이해하기 쉽지는 않다. 오류 메시지에 나타난 표현식이 어디에서 왔는지 파악하기도 늘 쉽지는 않다. 마지막으로, 인덱스 패밀리와 종속 타입 함수의 모음에 사소하지 않은 불변식을 인코딩하는 일은 흔히 취약할 수 있다. 함수의 드러난 축약 동작이 편리한 정의적 동등성을 제공하지 못하는 것으로 드러나면 시스템 초기에 정의한 내용을 바꿔야 하는 경우가 많다. 대안은 프로그램 곳곳에 동등성 증명을 호출하는 것이지만, 그러면 프로그램이 상당히 다루기 어려워질 수 있다.
관용적인 Lean 코드에서는 인덱스 데이터 타입을 자주 사용하지 않는다. 대신 중요한 불변식을 강제할 때는 보통 서브타입과 명시적 명제를 사용한다. 이 접근법에는 명시적인 증명이 많이 필요하고 정의적 동등성을 호출하는 일은 거의 없다. 대화형 정리 증명기에 걸맞게 Lean은 명시적인 증명을 편리하게 만들도록 설계되었다. 일반적으로 대부분의 경우에는 이 접근법을 우선해야 한다.
그러나 인덱스 데이터 타입의 인덱스 패밀리를 이해하는 것은 중요하다.
plusR_zero_left와 plusR_succ_left 같은 재귀 함수는 사실 수학적 귀납법에 의한 증명이다.
재귀의 기본 경우는 귀납법의 기본 경우에 대응하고, 재귀 호출은 귀납 가설을 적용하는 것을 나타낸다.
더 일반적으로 Lean의 새로운 명제는 증거를 나타내는 귀납 타입으로 정의되는 경우가 많으며, 이러한 귀납 타입에는 보통 인덱스가 있다.
정리를 증명하는 과정은 실제로 내부에서 이러한 타입의 표현식을 구성하는 과정이며, 이 절의 증명과 크게 다르지 않다.
또한 인덱스 데이터 타입이 문제에 정확히 맞는 도구인 경우도 있다.
언제 이를 사용해야 하는지 알려면 인덱스 데이터 타입을 능숙하게 다룰 수 있어야 한다.
7.5.5. Exercises
-
plusR_succ_left와 같은 방식의 재귀 함수를 사용해 모든Natn과k에 대해n.plusR k = n + k임을 증명하라. -
Vect에 대해plusR가plusL보다 자연스러운 함수를 작성하라.plusL을 정의하려면 증명을 사용해야 한다.