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