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와 같은 계층적 이름으로 주어집니다. 네임스페이스에서 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! 🐙
그다음 단순화기는 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
연산자의 종류(연산자의 “고정성(fixity)”)를 나타내는 첫 명령어 이름 뒤에는 콜론 :을 붙이고 연산자의 파싱 우선순위를 적습니다. 그다음 큰따옴표로 둘러싼 새 토큰이나 기존 토큰을 적습니다(공백은 보기 좋게 출력하는 데 쓰입니다). 마지막으로 화살표 => 뒤에 이 연산자가 변환될 함수를 적습니다.
우선순위는 연산자가 자신의 인자에 얼마나 “단단히” 결합하는지를 나타내는 자연수로, 연산 순서를 표현합니다. 위 코드가 펼쳐져 만들어지는 명령들을 살펴보면 이를 더 정확하게 이해할 수 있습니다:
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입니다. 즉, 그 자리에 어떤 우선순위의 표기법이든 올 수 있습니다. 두 표기법이 겹치는 경우에는 여기서도 최장 파싱 규칙을 적용합니다.
새 표기법은 이항 표기법보다 우선시되는데, 연쇄가 도입되기 전의 이항 표기법은 1 + 2 이후에서 파싱을 멈추기 때문입니다. 동일한 최장 파싱을 받아들이는 표기법이 여러 개 있으면 선택은 정교화 단계까지 미뤄지며, 정확히 하나의 오버로드만 타입이 올바른 경우가 아니면 정교화는 실패합니다.
6.8. 강제 변환
Lean에서 자연수의 타입인 Nat은 정수의 타입인 Int와 다릅니다. 하지만 자연수를 정수에 임베딩하는 함수 Int.ofNat이 있으므로, 필요할 때 임의의 자연수를 정수로 볼 수 있습니다. Lean에는 이러한 종류의 강제 변환을 감지하여 삽입하는 메커니즘이 있습니다. 강제 변환은 오버로드된 ↑ 연산자를 사용하여 명시적으로 요청할 수 있습니다.
6.9. 정보 표시하기
Lean에 현재 상태와 현재 컨텍스트에서 사용할 수 있는 객체 및 정리에 관한 정보를 질의하는 방법은 여러 가지가 있습니다. 그중 가장 흔히 쓰이는 두 가지인 #check와 #eval은 이미 살펴보았습니다. #check는 흔히 @ 연산자와 함께 사용된다는 점을 기억하십시오. 이 연산자는 정리나 정의의 모든 인자를 명시적으로 만듭니다. 또한 #print 명령을 사용하면 어떤 식별자에 관한 정보든 얻을 수 있습니다. 식별자가 정의나 정리를 가리키면 Lean은 그 기호의 타입과 정의를 출력합니다. 식별자가 상수나 공리이면 Lean은 그 사실을 알려 주고 타입을 보여 줍니다.
6.10. 옵션 설정
Lean은 사용자가 설정하여 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이지만, open Nat 명령을 사용하면 더 짧은 이름을 사용할 수 있습니다(protected로 표시되지 않은 이름에 한합니다). 귀납적 타입과 구조체와 레코드에 관한 장에서 살펴보겠지만, 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는 자동 바인딩 암시적 인자(auto bound implicit arguments)라는 새로운 기능을 지원합니다. 이 기능을 사용하면 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이 명시적 인자를 자동으로 추론할 수 있어서 _를 여러 개 연달아 쓰지 않으려 할 때에도 생략 부호가 유용합니다.