8.5. 범위가 제한된 수🔗

Array와 Nat에 대한 GetElem 인스턴스는 주어진 Nat이 배열의 크기보다 작다는 증명을 요구합니다. 실제로는 이러한 증명이 인덱스와 함께 함수에 전달되는 경우가 많습니다. 인덱스와 증명을 따로 전달하는 대신, Fin이라는 타입을 사용하여 인덱스와 증명을 하나의 값으로 묶을 수 있습니다. 이렇게 하면 코드를 더 읽기 쉽게 만들 수 있습니다.

타입 Fin n은 n보다 엄격하게 작은 수를 나타냅니다. 다시 말해, Fin 3은 0, 1, 2를 나타내는 반면, Fin 0에는 값이 전혀 없습니다. Fin의 정의는 Subtype과 비슷합니다. Fin n은 Nat 하나와 그 값이 n보다 작다는 증명을 담은 구조체이기 때문입니다:

structure Fin (n : Nat) where
  val  : Nat
  isLt : LT.lt val n

Lean에는 Fin 값을 숫자처럼 편리하게 사용할 수 있도록 해 주는 ToString 및 OfNat 인스턴스가 포함되어 있습니다. 다시 말해, #eval (5 : Fin 8)의 출력은 {val := 5, isLt := _}와 같은 형태가 아니라 5입니다.

주어진 수가 상한보다 클 때 실패하는 대신, Fin에 대한 OfNat 인스턴스는 상한으로 나눈 나머지 값을 반환합니다. 즉, #eval (45 : Fin 10)은 컴파일 타임 오류가 아니라 5가 됩니다.

반환 타입에서, 찾은 인덱스로 반환되는 Fin은 그 인덱스를 찾은 자료 구조와의 연관성을 더 분명하게 드러냅니다. 이전 절의 Array.find는 호출자가 배열 조회에 곧바로 사용할 수 없는 인덱스를 반환하는데, 이는 그 인덱스의 유효성에 관한 정보가 사라졌기 때문입니다. 더 구체적인 타입을 사용하면 프로그램을 크게 복잡하게 만들지 않고도 사용할 수 있는 값을 얻게 됩니다:

def findHelper (arr : Array α) (p : α → Bool) (i : Nat) :
    Option (Fin arr.size × α) :=
  if h : i < arr.size then
    let x := arr[i]
    if p x then
      some (⟨i, h⟩, x)
    else findHelper arr p (i + 1)
  else none

def Array.find (arr : Array α) (p : α → Bool) : Option (Fin arr.size × α) :=
  findHelper arr p 0

8.5.1. 연습 문제🔗

범위 안에 있으면 그다음으로 큰 Fin을 반환하고, 그렇지 않으면 none을 반환하는 함수 Fin.next? : Fin n → Option (Fin n)을 작성하십시오. 다음을 확인하십시오.

some 4#eval (3 : Fin 8).next?

출력

some 4

그리고 다음이 성립합니다

none#eval (7 : Fin 8).next?

출력

none