7.1. 열거형🔗

가장 간단한 종류의 귀납적 타입은 유한하게 열거된 원소 목록을 가진 타입입니다.

inductive 명령은 새로운 타입 Weekday를 생성합니다. 생성자들은 모두 Weekday 네임스페이스에 속합니다.

Weekday.sunday : Weekday

Weekday.monday : Weekday

Weekday.sunday : Weekday

Weekday.monday : Weekday

Weekday 귀납적 타입을 선언할 때 : Weekday는 생략할 수 있습니다.

sunday, monday, ... , saturday를 다른 구별되는 특성이 전혀 없는, Weekday의 서로 다른 원소로 생각하십시오. 소거 원리인 Weekday.rec는 타입 Weekday와 그 생성자들과 함께 정의됩니다. 이는 재귀자라고도 알려져 있으며, 타입을 “귀납적”으로 만드는 것이 바로 이것입니다: 각 생성자에 대응하는 값을 지정함으로써 Weekday에 대한 함수를 정의할 수 있게 해줍니다. 직관적으로 귀납적 타입은 생성자들에 의해 남김없이 생성되며, 그것들이 구성하는 것 이외의 원소는 갖지 않습니다.

match 표현식을 사용하여 Weekday에서 자연수로 가는 함수를 정의하겠습니다:

1

2

3

Lean의 논리를 사용할 때, match 표현식은 귀납적 타입을 선언할 때 생성되는 재귀자(recursor) Weekday.rec를 사용하여 컴파일됩니다. 이는 결과로 나오는 항이 타입 이론에서 잘 정의되도록 보장합니다. 컴파일된 코드의 경우, match는 다른 함수형 프로그래밍 언어에서와 마찬가지로 컴파일됩니다.

def numberOfDay : (d : Weekday) → Nat :=
fun (d : Weekday) =>
  numberOfDay.match_1.{1} (fun (d : Weekday) => Nat) d
    (fun (_ : Unit) => @OfNat.ofNat.{0} Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))
    (fun (_ : Unit) => @OfNat.ofNat.{0} Nat (nat_lit 2) (instOfNatNat (nat_lit 2)))
    (fun (_ : Unit) => @OfNat.ofNat.{0} Nat (nat_lit 3) (instOfNatNat (nat_lit 3)))
    (fun (_ : Unit) => @OfNat.ofNat.{0} Nat (nat_lit 4) (instOfNatNat (nat_lit 4)))
    (fun (_ : Unit) => @OfNat.ofNat.{0} Nat (nat_lit 5) (instOfNatNat (nat_lit 5)))
    (fun (_ : Unit) => @OfNat.ofNat.{0} Nat (nat_lit 6) (instOfNatNat (nat_lit 6))) fun (_ : Unit) =>
    @OfNat.ofNat.{0} Nat (nat_lit 7) (instOfNatNat (nat_lit 7))

@[instance_reducible] def numberOfDay.match_1.{u_1} : (motive : Weekday → Sort u_1) →
  (d : Weekday) →
    (h_1 : (_ : Unit) → motive Weekday.sunday) →
      (h_2 : (_ : Unit) → motive Weekday.monday) →
        (h_3 : (_ : Unit) → motive Weekday.tuesday) →
          (h_4 : (_ : Unit) → motive Weekday.wednesday) →
            (h_5 : (_ : Unit) → motive Weekday.thursday) →
              (h_6 : (_ : Unit) → motive Weekday.friday) → (h_7 : (_ : Unit) → motive Weekday.saturday) → motive d :=
fun (motive : Weekday → Sort u_1) (d : Weekday) (h_1 : (_ : Unit) → motive Weekday.sunday)
    (h_2 : (_ : Unit) → motive Weekday.monday) (h_3 : (_ : Unit) → motive Weekday.tuesday)
    (h_4 : (_ : Unit) → motive Weekday.wednesday) (h_5 : (_ : Unit) → motive Weekday.thursday)
    (h_6 : (_ : Unit) → motive Weekday.friday) (h_7 : (_ : Unit) → motive Weekday.saturday) =>
  @Weekday.casesOn.{u_1} (fun (x : Weekday) => motive x) d (h_1 Unit.unit) (h_2 Unit.unit) (h_3 Unit.unit)
    (h_4 Unit.unit) (h_5 Unit.unit) (h_6 Unit.unit) (h_7 Unit.unit)

@[reducible] def Weekday.casesOn.{u} : {motive : (t : Weekday) → Sort u} →
  (t : Weekday) →
    (sunday : motive Weekday.sunday) →
      (monday : motive Weekday.monday) →
        (tuesday : motive Weekday.tuesday) →
          (wednesday : motive Weekday.wednesday) →
            (thursday : motive Weekday.thursday) →
              (friday : motive Weekday.friday) → (saturday : motive Weekday.saturday) → motive t :=
fun {motive : (t : Weekday) → Sort u} (t : Weekday) (sunday : motive Weekday.sunday) (monday : motive Weekday.monday)
    (tuesday : motive Weekday.tuesday) (wednesday : motive Weekday.wednesday) (thursday : motive Weekday.thursday)
    (friday : motive Weekday.friday) (saturday : motive Weekday.saturday) =>
  @Weekday.rec.{u} motive sunday monday tuesday wednesday thursday friday saturday t

@Weekday.rec.{u_1} : {motive : (t : Weekday) → Sort u_1} →
  (sunday : motive Weekday.sunday) →
    (monday : motive Weekday.monday) →
      (tuesday : motive Weekday.tuesday) →
        (wednesday : motive Weekday.wednesday) →
          (thursday : motive Weekday.thursday) →
            (friday : motive Weekday.friday) → (saturday : motive Weekday.saturday) → (t : Weekday) → motive t

귀납적 데이터 타입을 선언할 때, deriving Repr을 사용하여 Weekday 객체를 텍스트로 변환하는 함수를 생성하도록 Lean에 지시할 수 있습니다. 이 함수는 #eval 명령이 Weekday 객체를 표시하는 데 사용됩니다. Repr이 존재하지 않으면, #eval은 그 자리에서 하나를 유도하려고 시도합니다.

Weekday.tuesday

어떤 구조와 관련된 정의와 정리를 같은 이름의 네임스페이스로 묶는 것이 유용한 경우가 많습니다. 예를 들어, numberOfDay 함수를 Weekday 네임스페이스에 넣을 수 있습니다. 그러면 해당 네임스페이스를 열었을 때 더 짧은 이름을 사용할 수 있습니다.

Weekday에서 Weekday로의 함수를 정의할 수 있습니다:

Weekday.thursday

Weekday.tuesday

임의의 Weekday d에 대해 next (previous d) = d라는 일반적인 정리를 어떻게 증명할 수 있을까요? 각 생성자마다 주장에 대한 증명을 제공하기 위해 match를 사용할 수 있습니다:

택틱 증명을 사용하면 훨씬 더 간결하게 작성할 수 있습니다:

아래의 귀납적 타입을 위한 택틱에서는 귀납적 타입을 활용하도록 특별히 설계된 추가 택틱들을 소개합니다.

propositions-as-types 대응 관계에서, 함수를 정의할 때뿐만 아니라 정리를 증명할 때도 match를 사용할 수 있다는 점에 주목하십시오. 다시 말해, propositions-as-types 대응 관계에서 경우에 따른 증명은 일종의 경우에 따른 정의이며, 여기서 “정의”되는 것은 데이터 조각이 아니라 증명입니다.

Lean 라이브러리의 Bool 타입은 열거형 타입의 한 예시입니다.

(이 예제들을 실행하기 위해, Bool과 같은 이름이 표준 라이브러리의 Bool과 충돌하지 않도록 이들을 Hidden이라는 네임스페이스에 넣었습니다. 이는 이러한 타입들이 시스템이 시작될 때 자동으로 임포트되는 Lean “프렐루드”의 일부이기 때문에 필요합니다.)

연습 문제로서, 이 타입들에 대한 도입 규칙과 소거 규칙이 무엇을 하는지 생각해 보십시오. 추가 연습 문제로, Bool 타입에 불리언 연산 and, or, not을 정의하고 일반적인 항등식을 검증해 볼 것을 제안합니다. and와 같은 이항 연산은 match를 사용해서 정의할 수 있다는 점에 유의하십시오.

마찬가지로, 대부분의 항등식은 적절한 match를 도입한 다음 rfl을 사용하여 증명할 수 있습니다.

7.2. 인자를 갖는 생성자🔗

열거형 타입은 귀납적 타입의 매우 특별한 경우로, 이 경우 생성자가 아무런 인자도 취하지 않습니다. 일반적으로 “구성”은 데이터에 의존할 수 있으며, 그 데이터는 구성된 인자에 표현됩니다. 라이브러리에 있는 곱 타입과 합 타입의 정의를 살펴봅시다.

이 예제들에서 무슨 일이 일어나고 있는지 살펴봅시다. 곱 타입에는 두 개의 인자를 받는 생성자 Prod.mk 하나가 있습니다. Prod α β에 대한 함수를 정의하려면, 입력이 Prod.mk a b 형태라고 가정할 수 있으며, a와 b를 이용하여 출력을 명시해야 합니다. 이를 이용하여 Prod에 대한 두 개의 사영을 정의할 수 있습니다. 표준 라이브러리는 Prod α β에 대해 α × β 표기법을, Prod.mk a b에 대해 (a, b) 표기법을 정의한다는 점을 기억하십시오.

함수 fst는 순서쌍 p를 인자로 받습니다. match는 p를 순서쌍 Prod.mk a b로 해석합니다. 또한 의존 타입 이론에서 살펴보았듯이, 이 정의들에 가능한 한 최대의 일반성을 부여하기 위해 타입 α와 β가 임의의 유니버스에 속하도록 허용한다는 점을 상기하십시오.

다음은 match 대신 재귀자 Prod.casesOn을 사용하는 또 다른 예시입니다.

6

7

인자 motive는 구성하려는 객체의 타입을 지정하는 데 사용되며, 이는 쌍(pair)에 의존할 수 있기 때문에 함수입니다. cond 함수는 불리언 조건문으로, cond b t1 t2는 b가 참이면 t1을, 그렇지 않으면 t2를 반환합니다. 함수 prod_example은 불리언 b와 숫자 n으로 이루어진 쌍을 받아, b가 참인지 거짓인지에 따라 2 * n 또는 2 * n + 1을 반환합니다.

반면, 합 타입은 inl과 inr(각각 “왼쪽 삽입”과 “오른쪽 삽입”을 뜻함)이라는 두 개의 생성자를 가지며, 이들 각각은 하나의 (명시적) 인자를 받습니다. Sum α β에 대한 함수를 정의하려면 두 가지 경우를 처리해야 합니다: 입력이 inl a 형태이면 a를 이용해 출력 값을 지정해야 하고, 입력이 inr b 형태이면 b를 이용해 출력 값을 지정해야 합니다.

6

7

이 예제는 이전 예제와 유사하지만, 이번에는 sum_example에 대한 입력이 암묵적으로 inl n 또는 inr n 형태 중 하나입니다. 첫 번째 경우 함수는 2 * n을 반환하고, 두 번째 경우에는 2 * n + 1을 반환합니다.

곱 타입이 Prod뿐만 아니라 생성자에도 인자로 쓰이는 매개변수 α β : Type에 의존한다는 점에 주목하십시오. Lean은 이러한 인자가 생성자의 이후 인자나 반환 타입으로부터 추론될 수 있는 경우를 감지하며, 그러한 경우에는 이들을 암묵적 인자로 만듭니다.

자연수 정의하기에서는 귀납적 타입의 생성자가 그 귀납적 타입 자체로부터 인자를 취할 때 어떤 일이 일어나는지 살펴보겠습니다. 이 절에서 다루는 예제들의 특징은 각 생성자가 이전에 지정된 타입에만 의존한다는 점입니다.

생성자가 여러 개인 타입은 선언적임에 유의하십시오. Sum α β의 원소는 inl a 형태이거나 또는 inl b 형태입니다. 인수가 여러 개인 생성자는 결합적 정보를 도입합니다. Prod α β의 원소 Prod.mk a b로부터 a 그리고 b를 추출할 수 있습니다. 임의의 귀납적 타입은 원하는 개수의 생성자를 가지고, 각 생성자가 원하는 개수의 인수를 취함으로써 두 특성을 모두 포함할 수 있습니다.

함수 정의에서와 마찬가지로, Lean의 귀납적 정의 문법에서도 생성자의 이름 있는 인자를 콜론 앞에 둘 수 있습니다.

이러한 정의의 결과는 본질적으로 이 절에서 앞서 제시한 것과 동일합니다.

Prod와 같이 생성자가 단 하나뿐인 타입은 순수하게 논리곱적입니다. 즉, 생성자는 단순히 인자 목록을 하나의 데이터로 묶으며, 이는 본질적으로 이후 인자의 타입이 앞선 인자의 타입에 의존할 수 있는 튜플입니다. 이러한 타입은 “레코드” 또는 “구조체”로도 생각할 수 있습니다. Lean에서는 structure 키워드를 사용하여 이러한 귀납적 타입과 그 사영을 동시에 정의할 수 있습니다.

이 예제는 귀납적 타입 Prod와 그 생성자인 mk, 일반적인 소거자(rec와 recOn), 그리고 위에서 정의된 사영 함수인 fst와 snd를 동시에 도입합니다.

생성자의 이름을 지정하지 않으면 Lean은 기본값으로 mk를 사용합니다. 예를 들어, 다음 코드는 색상을 RGB 값의 삼중항으로 저장하는 레코드를 정의합니다.

255

yellow의 정의는 제시된 세 값으로 레코드를 구성하며, 프로젝션 Color.red는 빨간색 성분을 반환합니다.

structure 명령은 대수적 구조를 정의하는 데 특히 유용하며, Lean은 이를 다루는 데 필요한 상당한 기반 시설을 제공합니다. 예를 들어, 다음은 반군(semigroup)의 정의입니다:

더 많은 예제는 구조체와 레코드를 다루는 장에서 살펴보겠습니다.

의존 곱 타입 Sigma에 대해서는 이미 살펴본 바 있습니다:

라이브러리에 있는 귀납적 타입의 예시를 두 가지 더 들면 다음과 같습니다:

의존 타입 이론의 의미론에는 부분 함수라는 내장된 개념이 없습니다. 함수 타입 α → β나 의존 함수 타입 (a : α) → β의 모든 원소는 모든 입력에 대해 값을 갖는다고 가정됩니다. Option 타입은 부분 함수를 표현하는 방법을 제공합니다. Option β의 원소는 none이거나, 어떤 값 b : β에 대해 some b 형태입니다. 따라서 타입 α → Option β의 원소 f를 α에서 β로 가는 부분 함수로 생각할 수 있습니다. 모든 a : α에 대해, f a는 f a가 “정의되지 않음”을 나타내는 none을 반환하거나, some b를 반환합니다.

Inhabited α의 원소는 단순히 α의 원소가 존재한다는 사실에 대한 증거입니다. 나중에 우리는 Inhabited가 Lean에서 타입 클래스의 한 예시임을 보게 될 것입니다: Lean에게 적절한 기본 타입들이 거주된다는 것을 알려줄 수 있으며, 이를 바탕으로 다른 구성된 타입들이 거주된다는 것을 자동으로 추론할 수 있습니다.

연습 문제로서, α에서 β로, 그리고 β에서 γ로 가는 부분 함수의 합성 개념을 개발하고, 그것이 예상대로 동작함을 보이시기 바랍니다. 또한 Bool과 Nat이 거주됨을, 두 거주된 타입의 곱이 거주됨을, 그리고 거주된 타입으로 가는 함수의 타입이 거주됨을 보이시기 바랍니다.

7.3. 귀납적으로 정의된 명제🔗

귀납적으로 정의된 타입은 최하위 유니버스인 Prop을 포함하여 어떤 타입 유니버스에도 존재할 수 있습니다. 실제로 논리 연결사가 정의되는 방식이 바로 이것입니다.

이러한 것들이 여러분이 이미 살펴본 도입 규칙과 소거 규칙을 어떻게 발생시키는지 생각해 보아야 합니다. 귀납적 타입의 소거자가 어디로 소거할 수 있는지, 즉 어떤 종류의 타입이 재귀자의 대상이 될 수 있는지를 지배하는 규칙들이 있습니다. 대략적으로 말하면, Prop에 속한 귀납적 타입을 특징짓는 것은 오직 Prop에 속한 다른 타입으로만 소거할 수 있다는 점입니다. 이는 p : Prop일 때 원소 hp : p가 어떤 데이터도 담지 않는다는 이해와 일치합니다. 하지만 이 규칙에는 작은 예외가 하나 있는데, 이는 아래 귀납적 패밀리에서 다루겠습니다.

존재 한정사조차도 귀납적으로 정의됩니다:

표기법 ∃ x : α, p는 Exists (fun x : α => p)의 문법적 설탕(syntactic sugar)임을 유념하십시오.

False, True, And, Or의 정의는 Empty, Unit, Prod, Sum의 정의와 완벽하게 유사합니다. 차이점은 첫 번째 그룹은 Prop의 원소를 산출하고, 두 번째 그룹은 어떤 u에 대해 Type u의 원소를 산출한다는 것입니다. 이와 유사한 방식으로, ∃ x : α, p는 Σ x : α, β의 Prop 값 변형입니다.

여기서 {x : α // p}로 표시되는 또 다른 귀납적 타입을 언급하는 것이 좋겠습니다. 이는 ∃ x : α, p와 Σ x : α, β의 일종의 혼합체입니다.

실제로 Lean에서 Subtype은 structure 명령을 사용하여 정의됩니다:

{x : α // p x} 표기법은 Subtype (fun x : α => p x)의 문법적 설탕(syntactic sugar)입니다. 이는 집합론에서의 부분집합 표기법을 본떠 만들어졌습니다. 즉, {x : α // p x}는 α의 원소 중 속성 p를 만족하는 것들의 모임을 나타낸다는 발상입니다.

7.4. 자연수 정의하기🔗

지금까지 살펴본 귀납적으로 정의된 타입들은 “평평”합니다: 생성자는 데이터를 감싸서 타입에 삽입하며, 그에 대응하는 재귀자는 데이터를 풀어서 그것에 대해 작동합니다. 생성자가 정의되고 있는 바로 그 타입의 원소들에 대해 작동할 때 상황은 훨씬 더 흥미로워집니다. 자연수 타입 Nat이 대표적인 예입니다:

생성자는 두 개가 있습니다. 먼저 zero : Nat부터 시작하는데, 이는 인자를 받지 않으므로 처음부터 가지고 있는 셈입니다. 이와 대조적으로, 생성자 succ은 이전에 구성된 Nat에만 적용할 수 있습니다. 이를 zero에 적용하면 succ zero : Nat이 만들어집니다. 이를 다시 적용하면 succ (succ zero) : Nat이 만들어지며, 이런 식으로 계속됩니다. 직관적으로 Nat은 이러한 생성자들을 갖는 “가장 작은” 타입이며, 이는 zero에서 시작하여 succ을 반복적으로 적용함으로써 남김없이 (그리고 자유롭게) 생성됨을 의미합니다.

이전과 마찬가지로, Nat에 대한 재귀자는 Nat에서 임의의 정의역으로 향하는 의존 함수 f, 즉 어떤 motive : Nat → Sort u에 대해 (n : Nat) → motive n의 원소인 f를 정의하도록 설계되어 있습니다. 이 재귀자는 두 가지 경우를 처리해야 하는데, 입력이 zero인 경우와 입력이 어떤 n : Nat에 대해 succ n 형태인 경우입니다. 첫 번째 경우에는, 이전과 마찬가지로 알맞은 타입을 갖는 목표 값을 그냥 지정합니다. 그러나 두 번째 경우에는, 재귀자가 n에서의 f의 값이 이미 계산되어 있다고 가정할 수 있습니다. 그 결과, 재귀자의 다음 인자는 n과 f n을 이용하여 f (succ n)의 값을 지정합니다. 재귀자의 타입을 확인해 보면 다음과 같습니다.

암시적 인자인 motive는 정의되는 함수의 공역입니다. 타입 이론에서는 motive가 소거/재귀의 동기라고 흔히 말하는데, 이는 우리가 구성하고자 하는 대상의 종류를 나타내기 때문입니다. 다음 두 인자는 위에서 설명한 것처럼 0의 경우와 후행자의 경우를 계산하는 방법을 명시합니다. 이들은 부전제라고도 알려져 있습니다. 마지막으로, t : Nat은 함수의 입력입니다. 이는 주전제라고도 알려져 있습니다.

Nat.recOn은 Nat.rec과 유사하지만, 주요 전제가 부차 전제들보다 앞에 옵니다.

예를 들어, 자연수에 대한 덧셈 함수 add m n을 생각해 봅시다. m을 고정하면, n에 대한 재귀법으로 덧셈을 정의할 수 있습니다. 기본 단계에서는 add m zero를 m으로 둡니다. 후행자 단계에서는, add m n의 값이 이미 결정되어 있다고 가정하고, add m (succ n)을 succ (add m n)으로 정의합니다.

Hidden.Nat.succ (Hidden.Nat.succ (Hidden.Nat.succ (Hidden.Nat.zero)))

이러한 정의는 Nat 네임스페이스에 넣어두는 것이 유용합니다. 그런 다음 이 네임스페이스에서 익숙한 표기법을 정의할 수 있습니다. 덧셈에 대한 두 정의 방정식은 이제 정의적으로 성립합니다:

instance 명령이 어떻게 작동하는지는 타입 클래스 장에서 설명하겠습니다. 아래 예제에서는 Lean 버전의 자연수를 사용하겠습니다.

하지만 0 + n = n과 같은 사실을 증명하려면 귀납법에 의한 증명이 필요합니다. 앞서 살펴본 바와 같이, 공역 motive n이 Prop의 원소인 경우 귀납법 원리는 재귀 원리의 특수한 경우일 뿐입니다. 이는 귀납적 증명의 익숙한 패턴을 나타냅니다: ∀ n, motive n을 증명하려면 먼저 motive 0을 증명하고, 그다음 임의의 n에 대해 ih : motive n을 가정하고 motive (n + 1)을 증명합니다.

다시 한번 주목할 점은, 증명의 맥락에서 Nat.recOn이 사용될 때 이는 실제로 귀납법 원리를 변장한 것에 지나지 않는다는 것입니다. rw와 simp 택틱은 이러한 증명에서 매우 효과적인 경향이 있습니다. 이 경우 각 택틱을 사용하여 증명을 다음과 같이 축소할 수 있습니다: