6. Lean과 상호작용하기
이제 여러분은 수학적 대상을 정의하는 언어이자 증명을 구성하는 언어로서, 의존 타입 이론의 기본 원리에 익숙해졌습니다. 여러분에게 부족한 한 가지는 새로운 데이터 타입을 정의하는 메커니즘입니다. 이 공백은 다음 장에서 채우게 될 것인데, 그 장에서는 귀납적 데이터 타입이라는 개념을 소개합니다. 하지만 그에 앞서 이 장에서는 타입 이론의 메커니즘에서 잠시 벗어나, Lean과 상호작용하는 실용적인 측면들을 살펴보겠습니다.
여기서 찾을 수 있는 정보가 모두 당장 유용한 것은 아닙니다. 이 절을 훑어보며 Lean의 기능들을 대략적으로 파악한 다음, 필요할 때 다시 돌아와 참고할 것을 권장합니다.
6.1. 메시지
Lean은 세 가지 종류의 메시지를 생성합니다:
:오류
코드에 일관성이 없어 처리할 수 없을 때 오류가 발생합니다. 예를 들어 구문 오류(예: )가 누락된 경우)와 자연수를 함수에 더하려 시도하는 것과 같은 타입 오류가 있습니다.
:경고
경고는 sorry의 존재와 같이 코드에 있을 수 있는 잠재적 문제를 설명합니다. 오류와 달리 코드가 무의미해지는 것은 아니지만, 경고에는 세심한 주의를 기울일 필요가 있습니다.
:정보
정보는 코드에 문제가 있음을 나타내지 않으며, #check와 #eval 같은 명령의 출력을 포함합니다.
Lean은 어떤 명령이 예상되는 메시지를 생성하는지 확인할 수 있습니다. 메시지가 일치하면 어떤 오류든 무시됩니다. 이는 올바른 오류가 발생하는지 확인하는 데 사용할 수 있습니다. 메시지가 일치하지 않으면 오류가 발생합니다. #guard_msgs 명령을 사용하여 어떤 메시지가 예상되는지 나타낼 수 있습니다.
예시는 다음과 같습니다:
/--
error: Type mismatch
"Not a number"
has type
String
but is expected to have type
Nat
-/
#guard_msgs in
def x : Nat := "Not a number"
#guard_msgs 뒤에 괄호로 메시지 범주를 포함하면 지정된 범주만 검사하고 나머지는 통과시킵니다. 이 예제에서 #eval은 sorry의 존재로 인해 오류를 발생시키지만, sorry에 대해 항상 발생하는 경고는 평소와 같이 표시됩니다.
/--
error: Aborting evaluation since the expression depends on the
'sorry' axiom, which can lead to runtime instability and crashes.
To attempt to evaluate anyway despite the risks, use the '#eval!'
command.
-/
#guard_msgs(error) in
#eval (sorry : Nat)이러한 설정이 없으면 두 메시지가 모두 포착됩니다:
/--
error: Aborting evaluation since the expression depends on the 'sorry'
axiom, which can lead to runtime instability and crashes.
To attempt to evaluate anyway despite the risks, use the '#eval!'
command.
---
warning: declaration uses `sorry`
-/
#guard_msgs in
#eval (sorry : Nat)
이 책의 일부 예제는 예상되는 오류를 나타내기 위해 #guard_msgs를 사용합니다.
6.2. 파일 가져오기
Lean의 프론트엔드가 지닌 목표는 사용자 입력을 해석하고, 형식적 표현식을 구성하며, 그것이 올바른 형태를 갖추고 타입이 올바른지 검사하는 것입니다. Lean은 또한 다양한 편집기의 사용을 지원하며, 이러한 편집기는 지속적인 검사와 피드백을 제공합니다. 더 많은 정보는 Lean 문서 페이지에서 확인할 수 있습니다.
Lean의 표준 라이브러리에 있는 정의와 정리는 여러 파일에 걸쳐 흩어져 있습니다. 사용자는 추가 라이브러리를 활용하거나, 여러 파일에 걸쳐 자신의 프로젝트를 개발하고자 할 수도 있습니다. Lean이 시작될 때, 여러 기본적인 정의와 구성을 포함하는 라이브러리 Init 폴더의 내용을 자동으로 가져옵니다. 그 결과, 여기서 제시하는 예제 대부분은 “바로 사용” 가능합니다.
하지만 추가 파일을 사용하려면 파일 시작 부분에 import 문을 통해 수동으로 임포트해야 합니다. 다음 명령은
importBar.Baz.Blah
이는 Bar/Baz/Blah.olean 파일을 임포트하며, 여기서 설명은 Lean 검색 경로를 기준으로 해석됩니다. 검색 경로가 어떻게 결정되는지에 대한 정보는 문서 페이지에서 확인할 수 있습니다. 기본적으로 여기에는 표준 라이브러리 디렉터리와 (일부 맥락에서는) 사용자 로컬 프로젝트의 루트가 포함됩니다.
임포트는 전이적입니다. 다시 말해, Foo를 임포트하고 Foo가 Bar를 임포트한다면, Bar의 내용에도 접근할 수 있으며 이를 명시적으로 임포트할 필요가 없습니다.
6.3. 섹션에 대해 더 알아보기
Lean은 이론을 구조화하는 데 도움이 되는 다양한 절 구분 메커니즘을 제공합니다. 변수와 절에서 section 명령이 이론의 서로 관련된 요소들을 함께 묶을 수 있게 해줄 뿐만 아니라, 필요에 따라 정리와 정의의 인자로 삽입되는 변수를 선언할 수 있게 해준다는 것을 보았습니다. 다음 예시에서와 같이, variable 명령의 요점은 정리에서 사용할 변수를 선언하는 것임을 기억하십시오.
section
variable (x y : Nat)
def double := x + x
#check double y
#check double (2 * x)
attribute [local simp] Nat.add_assoc Nat.add_comm Nat.add_left_comm
theorem t1 : double (x + y) = double x + double y := x:Naty:Nat⊢ double (x + y) = double x + double y
All goals completed! 🐙
#check t1 y
#check t1 (2 * x)
theorem t2 : double (x * y) = double x * y := x:Naty:Nat⊢ double (x * y) = double x * y
All goals completed! 🐙
end
double의 정의에서 x를 인자로 선언할 필요는 없습니다. Lean이 의존성을 감지하여 자동으로 삽입합니다. 마찬가지로, Lean은 t1과 t2에서 x가 나타나는 것을 감지하여 그곳에도 자동으로 삽입합니다. double은 y를 인자로 가지지 않는다는 점에 유의하십시오. 변수는 실제로 사용되는 선언에만 포함됩니다.
6.4. 네임스페이스에 대해 더 알아보기
Lean에서 식별자는 Foo.Bar.baz와 같은 계층적 이름으로 주어집니다. Namespaces에서 Lean이 계층적 이름을 다루기 위한 메커니즘을 제공한다는 것을 살펴보았습니다. namespace Foo 명령은 end Foo가 나타날 때까지 각 정의와 정리의 이름 앞에 Foo를 붙입니다. 그러면 open Foo 명령은 접두사 Foo로 시작하는 정의와 정리에 대한 임시 별칭을 생성합니다.
다음 정의는
def Foo.bar : Nat := 1
매크로로 취급되어 다음과 같이 확장됩니다
정리와 정의의 이름은 고유해야 하지만, 이를 식별하는 별칭은 그렇지 않습니다. 네임스페이스를 열면 식별자가 모호해질 수 있습니다. Lean은 타입 정보를 사용하여 문맥상의 의미를 명확히 하려 시도하지만, 전체 이름을 지정하여 언제나 명확하게 만들 수 있습니다. 이를 위해 문자열 _root_는 빈 접두사를 명시적으로 나타냅니다.
def String.add (a b : String) : String :=
a ++ b
def Bool.add (a b : Bool) : Bool :=
a != b
def add (α β : Type) : Type := Sum α β
open Bool
open String
-- This reference is ambiguous:
-- #check add
#check String.add
#check Bool.add
#check _root_.add
#check add "hello" "world"
#check add true false
#check add Nat Nat
protected 키워드를 사용하면 더 짧은 별칭이 생성되는 것을 막을 수 있습니다:
protected def Foo.bar : Nat := 1
open Foo
/-- error: Unknown identifier `bar` -/
#guard_msgs in
#check bar -- message: error
#check Foo.bar
이는 일반적인 이름의 오버로딩을 방지하기 위해 Nat.rec이나 Nat.recOn과 같은 이름에 흔히 사용됩니다.
open 명령은 다양한 변형을 허용합니다. 다음 명령은
명시된 식별자에 대해서만 별칭을 생성합니다. 다음 명령은
open Nat hiding succ gcd
#check zero
/-- error: Unknown identifier `gcd` -/
#guard_msgs in
#eval gcd 15 6 -- message: error
#eval Nat.gcd 15 6
나열된 식별자를 제외한 Nat 네임스페이스 내의 모든 것에 대해 별칭을 생성합니다.
Nat.mul을 times로, Nat.add를 plus로 이름을 바꾸는 별칭을 생성합니다.
별칭을 한 네임스페이스에서 다른 네임스페이스로, 또는 최상위 레벨로 export하는 것이 유용할 때가 있습니다. 다음 명령은
현재 네임스페이스 안에 succ, add, sub에 대한 별칭을 만들어, 해당 네임스페이스가 열려 있을 때마다 이 별칭들을 사용할 수 있도록 합니다. 이 명령을 네임스페이스 밖에서 사용하면, 별칭들은 최상위로 내보내집니다.
6.5. 속성
Lean의 주된 기능은 사용자 입력을 형식적 표현식으로 번역하는 것이며, 이 표현식은 커널에 의해 정확성이 검사된 후 나중에 사용할 수 있도록 환경에 저장됩니다. 하지만 일부 명령은 환경에 다른 영향을 미치기도 하는데, 타입 클래스에 관한 장에서 설명하는 바와 같이 환경 내 객체에 속성을 지정하거나, 표기법을 정의하거나, 타입 클래스의 인스턴스를 선언하는 식입니다. 이러한 명령 대부분은 전역적인 효과를 가지는데, 이는 현재 파일뿐 아니라 이를 임포트하는 모든 파일에서도 그 효과가 유지된다는 뜻입니다. 그러나 이러한 명령은 흔히 local 수정자를 지원하는데, 이는 현재 section 또는 namespace가 닫히거나 현재 파일이 끝날 때까지만 효과가 있음을 나타냅니다.
단순화기 사용하기에서, 정리에 [simp] 속성을 표시할 수 있으며 이를 통해 단순화기가 해당 정리를 사용할 수 있게 됨을 살펴보았습니다. 다음 예제는 리스트에 대한 접두사 관계를 정의하고, 이 관계가 반사적임을 증명한 다음, 해당 정리에 [simp] 속성을 부여합니다.
def isPrefix (l₁ : List α) (l₂ : List α) : Prop :=
∃ t, l₁ ++ t = l₂
@[simp] theorem List.isPrefix_self (as : List α) : isPrefix as as :=
⟨[], α:Type u_1as:List α⊢ as ++ [] = as All goals completed! 🐙⟩
example : isPrefix [1, 2, 3] [1, 2, 3] := ⊢ isPrefix [1, 2, 3] [1, 2, 3]
All goals completed! 🐙
그러면 단순화기(simplifier)는 isPrefix [1, 2, 3] [1, 2, 3]를 True로 다시 쓰서 증명합니다.
정의가 이루어진 이후 언제든지 이 속성을 지정할 수도 있습니다:
theorem List.isPrefix_self (as : List α) : isPrefix as as :=
⟨[], α:Type u_1as:List α⊢ as ++ [] = as All goals completed! 🐙⟩
attribute [simp] List.isPrefix_self
이 모든 경우에서, 해당 속성은 선언이 발생한 파일을 임포트하는 모든 파일에서 계속 효력을 유지합니다. local 수식어를 추가하면 범위가 제한됩니다:
section
theorem List.isPrefix_self (as : List α) : isPrefix as as :=
⟨[], α:Type u_1as:List α⊢ as ++ [] = as All goals completed! 🐙⟩
attribute [local simp] List.isPrefix_self
example : isPrefix [1, 2, 3] [1, 2, 3] := ⊢ isPrefix [1, 2, 3] [1, 2, 3]
All goals completed! 🐙
end
/-- error: `simp` made no progress -/
#guard_msgs in
example : isPrefix [1, 2, 3] [1, 2, 3] := ⊢ isPrefix [1, 2, 3] [1, 2, 3]
⊢ isPrefix [1, 2, 3] [1, 2, 3]
다른 예로, instance 명령을 사용하여 isPrefix 관계에 표기법 ≤를 할당할 수 있습니다. 타입 클래스를 다루는 장에서 설명할 이 명령은 관련 정의에 [instance] 속성을 할당하는 방식으로 작동합니다.
def isPrefix (l₁ : List α) (l₂ : List α) : Prop :=
∃ t, l₁ ++ t = l₂
instance : LE (List α) where
le := isPrefix
theorem List.isPrefix_self (as : List α) : as ≤ as :=
⟨[], α:Type u_1as:List α⊢ as ++ [] = as All goals completed! 🐙⟩
해당 대입은 지역적으로도 만들 수 있습니다:
abbrev instLe : LE (List α) :=
{ le := isPrefix }
section
attribute [local instance] instLe
example (as : List α) : as ≤ as :=
⟨[], α:Type u_1as:List α⊢ as ++ [] = as All goals completed! 🐙⟩
end
/--
error: failed to synthesize instance of type class
LE (List α)
Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
-/
#guard_msgs in
example (as : List α) : as ≤ as :=
⟨[], by simp⟩
아래의 표기법에서는 표기법을 정의하는 Lean의 메커니즘을 다루며, 이들 역시 local 수정자를 지원함을 살펴볼 것입니다. 그러나 옵션 설정에서는 옵션을 설정하는 Lean의 메커니즘을 다룰 것인데, 이는 이러한 패턴을 따르지 않습니다: 옵션은 오직 지역적으로만 설정할 수 있으며, 다시 말해 그 범위는 항상 현재 섹션이나 현재 파일로 제한됩니다.
6.6. 암시적 인자에 대해 더 알아보기
암시적 인자에서, Lean이 항 t의 타입을 {x : α} → β x로 표시한다면 중괄호는 x가 t의 암시적 인자로 표시되었음을 나타낸다는 것을 살펴보았습니다. 이는 t를 쓸 때마다 자리 표시자, 즉 “구멍(hole)”이 삽입되어 t가 @t _로 대체된다는 것을 의미합니다. 그런 일이 일어나지 않기를 원한다면, 대신 @t를 써야 합니다.
암시적 인자는 즉시 삽입된다는 점에 유의하십시오. f : (x : Nat) → {y : Nat} → (z : Nat) → Nat라는 함수를 정의한다고 가정합시다. 그러면 더 이상의 인자 없이 f 7이라는 식을 작성할 때, 이는 @f 7 _로 파싱됩니다.
Lean은 플레이스홀더가 후속 명시적 인자 앞에만 추가되어야 함을 지정하는 더 약한 주석을 제공합니다. 이는 이중 중괄호로 작성할 수 있으며, 이 경우 f의 타입은 f : (x : Nat) → {{y : Nat}} → (z : Nat) → Nat가 됩니다. 이 주석을 사용하면 f 7이라는 표현식은 그대로 파싱되지만, f 7 3은 강한 주석을 사용했을 때와 마찬가지로 @f 7 _ 3으로 파싱됩니다. 이 주석은 ⦃y : Nat⦄처럼 작성할 수도 있는데, 이때 유니코드 괄호는 각각 \{{와 \}}로 입력합니다.
그 차이를 설명하기 위해, 재귀적 유클리드 관계가 대칭이면서 동시에 추이적임을 보이는 다음 예제를 살펴봅시다.
def reflexive {α : Type u} (r : α → α → Prop) : Prop :=
∀ (a : α), r a a
def symmetric {α : Type u} (r : α → α → Prop) : Prop :=
∀ {a b : α}, r a b → r b a
def transitive {α : Type u} (r : α → α → Prop) : Prop :=
∀ {a b c : α}, r a b → r b c → r a c
def Euclidean {α : Type u} (r : α → α → Prop) : Prop :=
∀ {a b c : α}, r a b → r a c → r b c
theorem th1 {α : Type u} {r : α → α → Prop}
(reflr : reflexive r) (euclr : Euclidean r)
: symmetric r :=
fun {a b : α} =>
fun (h : r a b) =>
show r b a from euclr h (reflr _)
theorem th2 {α : Type u} {r : α → α → Prop}
(symmr : symmetric r) (euclr : Euclidean r)
: transitive r :=
fun {a b c : α} =>
fun (rab : r a b) (rbc : r b c) =>
euclr (symmr rab) rbc
theorem th3 {α : Type u} {r : α → α → Prop}
(reflr : reflexive r) (euclr : Euclidean r)
: transitive r :=
th2 (th1 reflr @euclr) @euclr
variable (r : α → α → Prop)
variable (euclr : Euclidean r)
#check euclr
결과는 작은 단계로 나뉘어 있습니다. th1은 반사적이면서 유클리드적인 관계가 대칭적임을 보여주며, th2는 대칭적이면서 유클리드적인 관계가 추이적임을 보여줍니다. 그런 다음 th3은 두 결과를 결합합니다. 하지만 euclr에서는 암묵적 인자를 수동으로 비활성화해야 한다는 점에 유의하십시오. 그렇지 않으면 너무 많은 암묵적 인자가 삽입됩니다. 약한 암묵적 인자를 사용하면 이 문제가 사라집니다.
def reflexive {α : Type u} (r : α → α → Prop) : Prop :=
∀ (a : α), r a a
def symmetric {α : Type u} (r : α → α → Prop) : Prop :=
∀ {{a b : α}}, r a b → r b a
def transitive {α : Type u} (r : α → α → Prop) : Prop :=
∀ {{a b c : α}}, r a b → r b c → r a c
def Euclidean {α : Type u} (r : α → α → Prop) : Prop :=
∀ {{a b c : α}}, r a b → r a c → r b c
theorem th1 {α : Type u} {r : α → α → Prop}
(reflr : reflexive r) (euclr : Euclidean r)
: symmetric r :=
fun {a b : α} =>
fun (h : r a b) =>
show r b a from euclr h (reflr _)
theorem th2 {α : Type u} {r : α → α → Prop}
(symmr : symmetric r) (euclr : Euclidean r)
: transitive r :=
fun {a b c : α} =>
fun (rab : r a b) (rbc : r b c) =>
euclr (symmr rab) rbc
theorem th3 {α : Type u} {r : α → α → Prop}
(reflr : reflexive r) (euclr : Euclidean r)
: transitive r :=
th2 (th1 reflr euclr) euclr
variable (r : α → α → Prop)
variable (euclr : Euclidean r)
#check euclr
대괄호, 즉 [와 ]로 표시되는 세 번째 종류의 암묵적 인자가 있습니다. 이는 타입 클래스 장에서 설명하는 바와 같이 타입 클래스에 사용됩니다.
6.7. 표기법
Lean의 식별자는 그리스 문자를 포함하여 모든 영숫자 문자를 포함할 수 있습니다(단, 앞서 살펴보았듯 의존 타입 이론에서 특별한 의미를 갖는 ∀, Σ, λ는 제외합니다). 식별자는 또한 아래첨자를 포함할 수 있으며, 이는 \_를 입력한 다음 원하는 아래첨자 문자를 입력하여 넣을 수 있습니다.
Lean의 파서는 확장 가능합니다. 다시 말해, 새로운 표기법을 정의할 수 있습니다.
Lean의 문법은 기본적인 “믹스픽스(mixfix)” 표기법부터 사용자 정의 정교화기(elaborator)에 이르기까지, 모든 수준에서 사용자가 확장하고 사용자 정의할 수 있습니다. 실제로 모든 내장 문법은 사용자에게 공개된 것과 동일한 메커니즘과 API를 사용하여 파싱되고 처리됩니다. 이 절에서는 다양한 확장 지점을 설명합니다.
새로운 표기법을 도입하는 것은 프로그래밍 언어에서 비교적 드문 기능이며 때로는 코드를 모호하게 만들 가능성 때문에 꺼려지기도 하지만, 형식화에 있어서는 해당 분야의 기존 관례와 표기법을 코드로 간결하게 표현할 수 있는 매우 유용한 도구입니다. 기본적인 표기법을 넘어서, 흔히 반복되는 상용구 코드를 (잘 작동하는) 매크로로 분리해 내고 부분 문제를 효율적이고 가독성 있게 텍스트로 인코딩하기 위한 완전한 사용자 정의 도메인 특화 언어(DSL)를 내장할 수 있는 Lean의 능력은 프로그래머와 증명 엔지니어 모두에게 큰 도움이 될 수 있습니다.
6.7.1. 표기법과 우선순위
가장 기본적인 문법 확장 명령은 새로운 전위, 중위, 후위 연산자를 도입하거나 기존 연산자를 중복 정의할 수 있게 해 줍니다.
infixl:65 " + " => HAdd.hAdd -- left-associative
infix:50 " = " => Eq -- non-associative
infixr:80 " ^ " => HPow.hPow -- right-associative
prefix:100 "-" => Neg.neg
postfix:max "⁻¹" => Inv.inv
연산자 종류를 설명하는 초기 명령어 이름(그 “결합 방식”) 다음에는, 콜론 : 뒤에 연산자의 구문 분석 우선순위를 표시하고, 이어서 큰따옴표로 둘러싼 새 토큰 또는 기존 토큰(공백은 보기 좋게 출력하는 데 사용됩니다)을 표시한 다음, 화살표 => 뒤에 이 연산자가 변환되어야 할 함수를 표시합니다.
우선순위는 연산자가 자신의 인자에 얼마나 “단단히” 결합하는지를 나타내는 자연수로, 연산 순서를 인코딩합니다. 위 코드가 펼쳐지는 명령들을 살펴보면 이를 더 정확하게 파악할 수 있습니다.
notation:65 lhs:65 " + " rhs:66 => HAdd.hAdd lhs rhs
notation:50 lhs:51 " = " rhs:51 => Eq lhs rhs
notation:80 lhs:81 " ^ " rhs:80 => HPow.hPow lhs rhs
notation:100 "-" arg:100 => Neg.neg arg
-- `max` is a shorthand for precedence 1024:
notation:1024 arg:1024 "⁻¹" => Inv.inv arg
알고 보면 첫 번째 코드 블록의 모든 명령은 실제로는 더 일반적인 notation 명령으로 변환되는 명령 매크로입니다. 이러한 매크로를 작성하는 방법은 아래에서 배우겠습니다. 단일 토큰 대신, notation 명령은 토큰과 우선순위가 있는 이름 붙은 항 자리표시자가 섞인 시퀀스를 받으며, 이 자리표시자는 =>의 오른쪽에서 참조할 수 있고 해당 위치에서 파싱된 항으로 대체됩니다. 우선순위 p를 갖는 자리표시자는 그 자리에서 우선순위가 최소 p 이상인 표기법만 받아들입니다. 따라서 문자열 a + b + c는 a + (b + c)와 동등하게 파싱될 수 없는데, 이는 infixl 표기법의 오른쪽 피연산자가 그 표기법 자체보다 우선순위가 1 더 높기 때문입니다. 반대로, infixr는 오른쪽 피연산자에 표기법 자체의 우선순위를 재사용하므로, a ^ b ^ c는 a ^ (b ^ c)로 파싱될 수 있습니다. notation을 직접 사용하여 다음과 같이 중위 표기법을 도입했다면 유의하십시오.
우선순위만으로 결합성이 충분히 결정되지 않는 경우, Lean의 파서는 기본적으로 오른쪽 결합성을 따릅니다. 더 정확히 말하면, Lean의 파서는 모호한 문법이 존재할 때 지역적인 최장 파싱 규칙을 따릅니다. 즉, a ~ b ~ c에서 a ~의 우변을 파싱할 때, (현재 우선순위가 허용하는 한) 가능한 한 길게 파싱을 계속하며, b 다음에서 멈추지 않고 ~ c까지도 파싱합니다. 따라서 이 항은 a ~ (b ~ c)와 동치입니다.
위에서 언급했듯이, notation 명령을 사용하면 토큰과 자리표시자를 자유롭게 섞은 임의의 mixfix 구문을 정의할 수 있습니다.
set_option quotPrecheck false
notation:max "(" e ")" => e
notation:10 Γ " ⊢ " e " : " τ => Typing Γ e τ
우선순위가 없는 자리표시자는 기본값 0을 가집니다. 즉 어떤 우선순위의 표기법이든 그 자리에 올 수 있습니다. 두 표기법이 겹치는 경우, 다시 최장 파싱 규칙을 적용합니다.
새 표기법은 이항 표기법보다 우선시되는데, 이는 사슬화(chaining) 이전의 이항 표기법이 1 + 2 이후에는 파싱을 멈추기 때문입니다. 동일한 최장 파싱을 허용하는 표기법이 여러 개 있는 경우, 선택은 정교화 시점까지 지연되며, 정확히 하나의 오버로드만 타입이 올바를 때가 아니면 실패하게 됩니다.
6.8. 강제 변환
Lean에서 자연수의 타입인 Nat은 정수의 타입인 Int와 다릅니다. 하지만 자연수를 정수에 임베딩하는 함수 Int.ofNat이 있으며, 이는 필요할 때 임의의 자연수를 정수로 볼 수 있음을 의미합니다. Lean에는 이러한 종류의 강제 변환을 감지하여 삽입하는 메커니즘이 있습니다. 강제 변환은 오버로드된 ↑ 연산자를 사용하여 명시적으로 요청할 수 있습니다.
6.9. 정보 표시
Lean의 현재 상태와 현재 컨텍스트에서 사용 가능한 객체 및 정리에 대한 정보를 조회할 수 있는 방법에는 여러 가지가 있습니다. #check와 #eval, 이 가장 흔히 쓰이는 두 가지는 이미 살펴보았습니다. #check는 정리나 정의의 모든 인자를 명시적으로 만드는 @ 연산자와 함께 사용되는 경우가 많다는 점을 기억하십시오. 또한 #print 명령을 사용하면 임의의 식별자에 대한 정보를 얻을 수 있습니다. 식별자가 정의나 정리를 나타내는 경우, Lean은 해당 기호의 타입과 그 정의를 출력합니다. 그것이 상수나 공리인 경우, Lean은 그 사실을 알리고 타입을 보여줍니다.
6.10. 옵션 설정
Lean은 사용자가 설정하여 동작을 제어할 수 있는 다수의 내부 변수를 유지합니다. 그렇게 하는 문법은 다음과 같습니다:
set_option <name> <value>
매우 유용한 옵션 계열 중 하나는 Lean의 pretty printer가 항을 표시하는 방식을 제어합니다. 다음 옵션들은 true 또는 false 값을 입력으로 받습니다:
pp.explicit : display implicit arguments pp.universes : display hidden universe parameters pp.notation : display output using defined notations
예를 들어, 다음 설정은 훨씬 더 긴 출력을 만들어냅니다:
set_option pp.explicit true
set_option pp.universes true
set_option pp.notation false
#check 2 + 2 = 4
#reduce (fun x => x + 2) = (fun x => x + 3)
#check (fun x => x + 1) 1
set_option pp.all true 명령은 이러한 설정들을 한꺼번에 적용하는 반면, set_option pp.all false 명령은 이전 값들로 되돌립니다. 추가 정보를 예쁜 출력하는 것은 증명을 디버깅하거나 난해한 오류 메시지를 이해하려 할 때 흔히 매우 유용합니다. 하지만 정보가 너무 많으면 압도당할 수 있으며, 일반적인 상호작용에서는 Lean의 기본값으로 대체로 충분합니다.
6.11. 라이브러리 사용하기
Lean을 효과적으로 사용하려면 라이브러리에 있는 정의와 정리를 필연적으로 활용해야 합니다. 파일 시작 부분의 import 명령이 다른 파일에서 미리 컴파일된 결과를 가져온다는 것과, 임포트가 전이적이라는 것을 상기하십시오. 즉, Foo를 임포트하고 Foo가 Bar를 임포트한다면, Bar의 정의와 정리 역시 사용할 수 있습니다. 하지만 더 짧은 이름을 제공하는 네임스페이스를 여는 행위는 전이되지 않습니다. 각 파일에서 사용하고자 하는 네임스페이스를 직접 열어야 합니다.
일반적으로 어떤 정리, 정의, 표기법, 자원을 사용할 수 있는지 알기 위해서는 라이브러리와 그 내용에 익숙해지는 것이 중요합니다. 아래에서 Lean의 편집기 모드가 필요한 것을 찾는 데에도 도움이 될 수 있음을 살펴보겠지만, 라이브러리의 내용을 직접 살펴보는 일은 대개 피할 수 없습니다. Lean의 표준 라이브러리는 온라인 GitHub에서 찾을 수 있습니다.
GitHub의 브라우저 인터페이스를 사용하여 이러한 디렉터리와 파일의 내용을 볼 수 있습니다. 자신의 컴퓨터에 Lean을 설치했다면, lean 폴더에서 라이브러리를 찾아 파일 관리자로 탐색할 수 있습니다. 각 파일 상단의 주석 헤더는 추가 정보를 제공합니다.
Lean 라이브러리 개발자들은 필요한 정리의 이름을 더 쉽게 추측하거나, 다음 절에서 다룰 이를 지원하는 Lean 모드가 있는 편집기에서 탭 완성을 통해 찾을 수 있도록 일반적인 명명 지침을 따릅니다. 식별자는 일반적으로 camelCase이고, 타입은 CamelCase입니다. 정리 이름의 경우, 서로 다른 구성 요소를 _로 구분한 서술적인 이름에 의존합니다. 흔히 정리의 이름은 단순히 결론을 서술합니다:
Lean에서 식별자는 계층적 네임스페이스로 조직될 수 있다는 점을 기억하십시오. 예를 들어, 네임스페이스 Nat에 있는 le_of_succ_le_succ라는 이름의 정리는 전체 이름이 Nat.le_of_succ_le_succ이지만, protected로 표시되지 않은 이름에 대해서는 open Nat 명령을 통해 더 짧은 이름을 사용할 수 있게 됩니다. 귀납적 타입과 구조체와 레코드에 관한 장에서, Lean에서 구조체와 귀납적 데이터 타입을 정의하면 연관된 연산들이 생성되며, 이들이 정의 대상 타입과 같은 이름의 네임스페이스에 저장된다는 것을 살펴볼 것입니다. 예를 들어, 곱 타입에는 다음과 같은 연산들이 딸려 있습니다.
첫 번째는 쌍을 구성하는 데 사용되는 반면, 다음 두 개인 Prod.fst와 Prod.snd는 두 요소를 투영합니다. 마지막인 Prod.rec는 두 구성 요소에 대한 함수를 이용해 곱에 대한 함수를 정의하는 또 다른 방법을 제공합니다. Prod.rec와 같은 이름은 protected이며, 이는 Prod 네임스페이스가 열려 있더라도 전체 이름을 사용해야 함을 의미합니다.
명제를 타입으로 보는 대응 관계에서는 논리 연결사 또한 귀납적 타입의 인스턴스이므로, 이들에 대해서도 점 표기법을 사용하는 경향이 있습니다:
6.12. 자동 바인딩 암시적 인자
이전 절에서는 암시적 인자가 함수를 어떻게 더 편리하게 사용할 수 있게 해 주는지 보였습니다. 하지만 compose와 같은 함수는 정의하기가 여전히 상당히 장황합니다. 유니버스 다형적인 compose는 앞서 정의한 것보다 훨씬 더 장황하다는 점에 유의하십시오.
universe u v w
def compose {α : Type u} {β : Type v} {γ : Type w}
(g : β → γ) (f : α → β) (x : α) : γ :=
g (f x)
compose를 정의할 때 유니버스 매개변수를 제공하면 universe 명령을 사용하지 않을 수 있습니다.
def compose.{u, v, w}
{α : Type u} {β : Type v} {γ : Type w}
(g : β → γ) (f : α → β) (x : α) : γ :=
g (f x)
Lean 4는 자동 바운드 암시적 인자라는 새로운 기능을 지원합니다. 이 기능은 compose와 같은 함수를 작성하기 훨씬 편리하게 만들어 줍니다. Lean이 선언의 헤더를 처리할 때, 바인딩되지 않은 식별자는 자동으로 암시적 인자로 추가됩니다. 이 기능을 사용하면 compose를 다음과 같이 작성할 수 있습니다.
Lean이 Type 대신 Sort를 사용하여 더 일반적인 타입을 추론했다는 점에 유의하십시오.
저희는 이 기능을 매우 좋아하며 Lean을 구현할 때도 광범위하게 사용하고 있지만, 일부 사용자에게는 불편하게 느껴질 수 있다는 점을 인지하고 있습니다. 따라서 set_option autoImplicit false 명령을 사용하여 이 기능을 비활성화할 수 있습니다.
set_option autoImplicit false
/--
error: Unknown identifier `β`
Note: It is not possible to treat `β` as an implicitly bound variable here because the `autoImplicit` option is set to `false`.
---
error: Unknown identifier `γ`
Note: It is not possible to treat `γ` as an implicitly bound variable here because the `autoImplicit` option is set to `false`.
---
error: Unknown identifier `α`
Note: It is not possible to treat `α` as an implicitly bound variable here because the `autoImplicit` option is set to `false`.
---
error: Unknown identifier `β`
Note: It is not possible to treat `β` as an implicitly bound variable here because the `autoImplicit` option is set to `false`.
---
error: Unknown identifier `α`
Note: It is not possible to treat `α` as an implicitly bound variable here because the `autoImplicit` option is set to `false`.
---
error: Unknown identifier `γ`
Note: It is not possible to treat `γ` as an implicitly bound variable here because the `autoImplicit` option is set to `false`.
-/
#guard_msgs in
def compose (g : β → γ) (f : α → β) (x : α) : γ :=
g (f x)
6.13. 암시적 람다
표현식의 예상 타입이 암시적 인자를 기다리는 함수인 경우, 정교화기는 해당하는 람다를 자동으로 도입합니다. 예를 들어, pure의 타입은 첫 번째 인자가 암시적 타입 α라고 명시하지만, ReaderT.pure의 첫 번째 인자는 리더 모나드의 컨텍스트 타입 ρ입니다. 이는 fun {α} => ...로 자동으로 둘러싸이며, 이를 통해 정교화기는 본문 내의 암시적 인자를 올바르게 채울 수 있습니다.
instance : Monad (ReaderT ρ m) where
pure := ReaderT.pure
bind := ReaderT.bind
사용자는 @를 사용하거나 {} 또는 [] 바인더 표기와 함께 람다 표현식을 작성하여 암시적 람다 기능을 비활성화할 수 있습니다. 다음은 몇 가지 예시입니다
set_option linter.unusedVariables false
namespace Ex2
def id1 : {α : Type} → α → α :=
fun x => x
def listId : List ({α : Type} → α → α) :=
(fun x => x) :: []
-- In this example, implicit lambda introduction has been disabled because
-- we use `@` before {kw}`fun`
def id2 : {α : Type} → α → α :=
@fun α (x : α) => id1 x
def id3 : {α : Type} → α → α :=
@fun α x => id1 x
def id4 : {α : Type} → α → α :=
fun x => id1 x
-- In this example, implicit lambda introduction has been disabled
-- because we used the binder annotation `{...}`
def id5 : {α : Type} → α → α :=
fun {α} x => id1 x
end Ex2
6.14. 단순 함수를 위한 문법 설탕
Lean에는 fun 대신 익명 자리표시자를 사용하여 간단한 함수를 기술하는 표기법이 있습니다. ·가 항의 일부로 나타나면, 이를 감싸는 가장 가까운 괄호가 ·를 인자로 하는 함수가 됩니다. 괄호 안에 다른 괄호가 끼어들지 않은 채로 여러 개의 자리표시자가 포함되어 있다면, 이들은 왼쪽부터 오른쪽 순서로 인자가 됩니다. 다음은 몇 가지 예시입니다.
namespace Ex3
#check (· + 1)
#check (2 - ·)
#eval [1, 2, 3, 4, 5].foldl (· * ·) 1
def f (x y z : Nat) :=
x + y + z
#check (f · 1 ·)
#eval [(1, 2), (3, 4), (5, 6)].map (·.1)end Ex3
중첩된 괄호는 새로운 함수를 도입합니다. 다음 예제에서는 서로 다른 두 개의 람다 표현식이 생성됩니다.
6.15. 명명된 인자
이름 붙은 인자를 사용하면 매개변수 목록에서의 위치가 아니라 이름을 일치시켜 매개변수에 대한 인자를 지정할 수 있습니다. 매개변수의 순서는 기억나지 않지만 이름을 알고 있다면, 인자를 어떤 순서로든 전달할 수 있습니다. 또한 Lean이 암시적 매개변수를 추론하지 못한 경우 해당 값을 직접 제공할 수도 있습니다. 이름 붙은 인자는 각 인자가 나타내는 바를 명시함으로써 코드의 가독성도 높여줍니다.
def sum (xs : List Nat) :=
xs.foldl (init := 0) (·+·)
#eval sum [1, 2, 3, 4]-- 10
example {a b : Nat} {p : Nat → Nat → Nat → Prop}
(h₁ : p a b b) (h₂ : b = a) :
p a a b :=
Eq.subst (motive := fun x => p a x b) h₂ h₁
다음 예제에서는 이름 붙은 인자와 기본 인자 사이의 상호작용을 보여줍니다.
def f (x : Nat) (y : Nat := 1) (w : Nat := 2) (z : Nat) :=
x + y + w - z
example (x z : Nat) : f (z := z) x = x + 1 + 2 - z := rfl
example (x z : Nat) : f x (z := z) = x + 1 + 2 - z := rfl
example (x y : Nat) : f x y = fun z => x + y + 2 - z := rfl
example : f = (fun x z => x + 1 + 2 - z) := rfl
example (x : Nat) : f x = fun z => x + 1 + 2 - z := rfl
example (y : Nat) : f (y := 5) = fun x z => x + 5 + 2 - z := rfl
def g {α} [Add α] (a : α) (b? : Option α := none) (c : α) : α :=
match b? with
| none => a + c
| some b => a + b + c
variable {α} [Add α]
example : g = fun (a c : α) => a + c := rfl
example (x : α) : g (c := x) = fun (a : α) => a + x := rfl
example (x : α) : g (b? := some x) = fun (a c : α) => a + x + c := rfl
example (x : α) : g x = fun (c : α) => x + c := rfl
example (x y : α) : g x y = fun (c : α) => x + y + c := rfl
..을 사용하면 누락된 명시적 인자를 _로 제공할 수 있습니다. 이 기능은 이름 붙은 인자와 결합하면 패턴을 작성하는 데 유용합니다. 다음은 예시입니다.
inductive Term where
| var (name : String)
| num (val : Nat)
| app (fn : Term) (arg : Term)
| lambda (name : String) (type : Term) (body : Term)
def getBinderName : Term → Option String
| Term.lambda (name := n) .. => some n
| _ => none
def getBinderType : Term → Option Term
| Term.lambda (type := t) .. => some t
| _ => none
명시적 인자를 Lean이 자동으로 추론할 수 있어 _의 나열을 피하고자 할 때도 줄임표가 유용합니다.