Lean 4로 정리 증명하기

9. 구조체와 레코드🔗

Lean의 기초 체계에 귀납적 타입이 포함되어 있음을 살펴보았습니다. 더 나아가, 타입 유니버스와 의존 화살표 타입, 귀납적 타입만을 기반으로 상당한 규모의 수학 체계를 구축할 수 있다는 것이 놀라운 사실임을 살펴보았습니다. 그 밖의 모든 것은 이들로부터 도출됩니다. Lean 표준 라이브러리에는 귀납적 타입의 수많은 사례(예: Nat, Prod, List)가 포함되어 있으며, 논리 연결사조차도 귀납적 타입을 이용해 정의됩니다.

생성자를 하나만 갖는 비재귀적 귀납적 타입을 구조체(structure) 또는 레코드(record)라고 부른다는 것을 기억하십시오. 곱 타입(product type)은 구조체이며, 의존 곱(시그마) 타입도 마찬가지입니다. 일반적으로, 구조체 S를 정의할 때마다 우리는 보통 S의 각 인스턴스를 “분해”하여 그 필드에 저장된 값을 가져올 수 있게 해 주는 투영(projection) 함수를 정의합니다. 쌍의 첫 번째와 두 번째 요소를 반환하는 함수 Prod.fst와 Prod.snd는 이러한 투영의 예입니다.

프로그램을 작성하거나 수학을 형식화할 때, 많은 필드를 포함하는 구조체를 정의하는 일이 드물지 않습니다. Lean에서 사용할 수 있는 structure 명령은 이러한 과정을 지원하는 기반 시설을 제공합니다. 이 명령을 사용하여 구조체를 정의하면, Lean은 모든 투영 함수를 자동으로 생성합니다. structure 명령을 사용하면 이전에 정의한 구조체를 기반으로 새로운 구조체를 정의할 수도 있습니다. 게다가 Lean은 주어진 구조체의 인스턴스를 정의하기 위한 편리한 표기법을 제공합니다.

9.1. 구조체 선언하기🔗

structure 명령은 본질적으로 귀납적 데이터 타입을 정의하기 위한 “프런트 엔드”입니다. 모든 structure 선언은 자신과 같은 이름의 네임스페이스를 도입합니다. 일반적인 형식은 다음과 같습니다:

    structure <name> <parameters> <parent-structures> where
      <constructor> :: <fields>

대부분의 부분은 선택 사항입니다. 예시는 다음과 같습니다:

structure Point (α : Type u) where mk :: x : α y : α

Point 타입의 값은 Point.mk a b를 사용하여 생성되며, 포인트 p의 필드는 Point.x p와 Point.y p를 사용하여 접근합니다(하지만 p.x와 p.y도 작동합니다. 아래를 참고하십시오). structure 명령은 유용한 재귀자와 정리도 생성합니다. 위 선언에 대해 생성된 구성 요소 중 일부는 다음과 같습니다.

-- a Type Point.{u} (α : Type u) : Type u#check Point
Point.{u} (α : Type u) : Type u
-- the eliminator @Point.rec : {α : Type u_2} → {motive : Point α → Sort u_1} → ((x y : α) → motive { x := x, y := y }) → (t : Point α) → motive t#check @Point.rec
@Point.rec : {α : Type u_2} →
  {motive : Point α → Sort u_1} → ((x y : α) → motive { x := x, y := y }) → (t : Point α) → motive t
-- the constructor @Point.mk : {α : Type u_1} → α → α → Point α#check @Point.mk
@Point.mk : {α : Type u_1} → α → α → Point α
-- a projection @Point.x : {α : Type u_1} → Point α → α#check @Point.x
@Point.x : {α : Type u_1} → Point α → α
-- a projection @Point.y : {α : Type u_1} → Point α → α#check @Point.y
@Point.y : {α : Type u_1} → Point α → α

생성자 이름이 제공되지 않으면 생성자는 기본적으로 mk라는 이름을 갖습니다.

다음은 생성된 구성 요소를 사용하는 간단한 정리와 표현식입니다. 평소와 마찬가지로, open Point 명령을 사용하면 Point 접두사를 피할 수 있습니다.

10#eval Point.x (Point.mk 10 20)
10
20#eval Point.y (Point.mk 10 20)
20
open Point example (a b : α) : x (mk a b) = a := rfl example (a b : α) : y (mk a b) = b := rfl

p : Point Nat가 주어졌을 때, 점 표기법 p.x는 Point.x p의 축약형입니다. 이는 구조체의 필드에 접근하는 편리한 방법을 제공합니다.

def p := Point.mk 10 20 p.x : Nat#check p.x
p.x : Nat
10#eval p.x
10
20#eval p.y
20

점 표기법은 레코드의 사영에 접근할 때뿐 아니라, 같은 이름의 네임스페이스에 정의된 함수를 적용할 때도 편리합니다. 논리곱 절에서 살펴보았듯이, p가 Point 타입을 가진다면, foo의 첫 번째 암시적이지 않은 인자가 Point 타입이라고 가정할 때 p.foo라는 식은 Point.foo p로 해석됩니다. 따라서 아래 예제에서 p.add q라는 식은 Point.add p q의 축약형입니다.

structure Point (α : Type u) where x : α y : α deriving Repr def Point.add (p q : Point Nat) := mk (p.x + q.x) (p.y + q.y) def p : Point Nat := Point.mk 1 2 def q : Point Nat := Point.mk 3 4 { x := 4, y := 6 }#eval p.add q
{ x := 4, y := 6 }

다음 장에서는 add와 같은 함수를 정의하여, α에 연관된 덧셈 연산이 있다고 가정할 때 Point Nat뿐만 아니라 Point α의 원소에 대해서도 일반적으로 작동하도록 하는 방법을 배우게 됩니다.

더 일반적으로, p : Point인 표현식 p.foo x y z가 주어지면, Lean은 Point.foo의 인자 중 타입이 Point인 첫 번째 인자 자리에 p를 삽입합니다. 예를 들어, 아래의 스칼라 곱셈 정의를 사용하면 p.smul 3은 Point.smul 3 p로 해석됩니다.

def Point.smul (n : Nat) (p : Point Nat) := Point.mk (n * p.x) (n * p.y) def p : Point Nat := Point.mk 1 2 { x := 3, y := 6 }#eval p.smul 3
{ x := 3, y := 6 }
example {p : Point Nat} : p.smul 3 = Point.smul 3 p := rfl

두 번째 명시적 인자로 리스트를 받는 List.map 함수에서도 비슷한 요령을 사용하는 것이 일반적입니다:

@List.map : {α : Type u_1} → {β : Type u_2} → (α → β) → List α → List β#check @List.map
@List.map : {α : Type u_1} → {β : Type u_2} → (α → β) → List α → List β
def xs : List Nat := [1, 2, 3] def f : Nat → Nat := fun x => x * x [1, 4, 9]#eval xs.map f
[1, 4, 9]
example {xs : List α} {f : α → β} : xs.map f = List.map f xs := rfl

여기서 xs.map f는 List.map f xs로 해석됩니다.

9.2. 객체🔗

지금까지 우리는 구조체 타입의 원소를 만들기 위해 생성자를 사용해 왔습니다. 필드를 많이 포함하는 구조체의 경우, 필드가 정의된 순서를 기억해야 하기 때문에 이 방식은 종종 불편합니다. 따라서 Lean은 구조체 타입의 원소를 정의하기 위한 다음과 같은 대안 표기법을 제공합니다.

    { (<field-name> := <expr>)* : structure-type }
    or
    { (<field-name> := <expr>)* }

접미사 : structure-type은 구조체의 이름을 기대 타입으로부터 추론할 수 있는 경우 언제나 생략할 수 있습니다. 예를 들어, 우리는 이 표기법을 사용하여 “점(point)”을 정의합니다. 필드를 지정하는 순서는 중요하지 않으므로, 아래의 모든 표현식은 동일한 점을 정의합니다.

structure Point (α : Type u) where x : α y : α { x := 10, y := 20 } : Point Nat#check { x := 10, y := 20 : Point Nat }
{ x := 10, y := 20 } : Point Nat
{ x := 10, y := 20 } : Point Nat#check { y := 20, x := 10 : Point _ }
{ x := 10, y := 20 } : Point Nat
{ x := 10, y := 20 } : Point Nat#check ({ x := 10, y := 20 } : Point Nat)
{ x := 10, y := 20 } : Point Nat
example : Point Nat := { y := 20, x := 10 }

필드는 중괄호를 사용하여 암시적으로 표시할 수 있습니다. 암시적 필드는 생성자의 암시적 매개변수가 됩니다.

필드의 값이 지정되지 않은 경우, Lean은 이를 추론하려 시도합니다. 지정되지 않은 필드를 추론할 수 없는 경우, Lean은 해당 자리표시자를 합성할 수 없었음을 나타내는 오류를 표시합니다.

`MyStruct`: universes `u`, `v` only occur together. This usually means there is a `max` expression in the type where none of these universes appear on their own. Note: This linter can be disabled with `set_option linter.checkUnivs false`structure MyStruct where {α : Type u} {β : Type v} a : α b : β { α := Nat, β := Bool, a := 10, b := true } : MyStruct#check { a := 10, b := true : MyStruct }
{ α := Nat, β := Bool, a := 10, b := true } : MyStruct

레코드 갱신은 이전 레코드 객체의 하나 이상의 필드 값을 수정하여 새로운 레코드 객체를 만드는 것에 해당하는 또 다른 일반적인 연산입니다. Lean에서는 필드 할당 앞에 s with 라는 주석을 추가하여, 레코드 명세에서 지정되지 않은 필드를 이전에 정의된 구조체 객체 s에서 가져오도록 지정할 수 있습니다. 레코드 객체가 두 개 이상 제공되면, Lean이 지정되지 않은 필드를 포함하는 객체를 찾을 때까지 순서대로 방문합니다. 모든 객체를 방문한 후에도 지정되지 않은 필드 이름이 남아 있으면, Lean은 오류를 발생시킵니다.

structure Point (α : Type u) where x : α y : α deriving Repr def p : Point Nat := { x := 1, y := 2 } { x := 1, y := 3 }#eval { p with y := 3 }
{ x := 1, y := 3 }
{ x := 4, y := 2 }#eval { p with x := 4 }
{ x := 4, y := 2 }
structure Point3 (α : Type u) where x : α y : α z : α def q : Point3 Nat := { x := 5, y := 5, z := 5 } def r : Point3 Nat := { p, q with x := 6 } example : r.x = 6 := rfl example : r.y = 2 := rfl example : r.z = 5 := rfl

9.3. 상속🔗

새로운 필드를 추가함으로써 기존 구조체를 확장할 수 있습니다. 이 기능을 사용하면 일종의 상속을 흉내 낼 수 있습니다.

structure Point (α : Type u) where x : α y : α inductive Color where | red | green | blue structure ColorPoint (α : Type u) extends Point α where c : Color

다음 예제에서는 다중 상속을 사용하여 구조체를 정의한 다음, 부모 구조체들의 객체를 사용하여 객체를 정의합니다.

structure Point (α : Type u) where x : α y : α z : α structure RGBValue where red : Nat green : Nat blue : Nat structure RedGreenPoint (α : Type u) extends Point α, RGBValue where no_blue : blue = 0 def p : Point Nat := { x := 10, y := 10, z := 20 } def rgp : RedGreenPoint Nat := { p with red := 200, green := 40, blue := 0, no_blue := rfl } example : rgp.x = 10 := rfl example : rgp.red = 200 := rfl