12. 공리와 계산
Lean에 구현된 구성적 계산법(Calculus of Constructions) 버전은 의존 함수 타입, 귀납적 타입, 그리고 맨 아래에 비서술적(impredicative)이고 증명 무관성(proof-irrelevant)을 가진 Prop으로 시작하는 유니버스 계층을 포함한다는 것을 살펴보았습니다. 이 장에서는 CIC를 추가적인 공리와 규칙으로 확장하는 방법을 살펴봅니다. 이러한 방식으로 기초 체계를 확장하는 것은 종종 편리합니다. 이는 더 많은 정리를 증명할 수 있게 해줄 뿐만 아니라, 다른 방법으로도 증명할 수 있었던 정리를 더 쉽게 증명할 수 있게 해줍니다. 그러나 추가적인 공리를 도입하는 데에는 부정적인 결과가 따를 수 있으며, 이러한 결과는 그 공리의 정합성에 대한 우려를 넘어설 수 있습니다. 특히, 공리의 사용은 정의와 정리의 계산적 내용에 영향을 미치는데, 여기서는 그 방식을 살펴봅니다.
Lean은 계산적 추론과 고전적 추론을 모두 지원하도록 설계되었습니다. 그렇게 하고자 하는 사용자는 “계산적으로 순수한” 부분집합을 고수할 수 있으며, 이는 시스템 내 닫힌 표현식이 정규 형태로 계산됨을 보장합니다. 특히, 예를 들어 타입이 Nat인 닫힌 계산적으로 순수한 표현식은 어떤 것이든 숫자로 귀결됩니다.
Lean의 표준 라이브러리는 추가적인 공리인 명제적 외연성(propositional extensionality)과, 함수 외연성 원리를 함의하는 몫 구성(quotient construction)을 정의합니다. 이러한 확장들은 예를 들어 집합과 유한 집합의 이론을 전개하는 데 사용됩니다. 아래에서 이러한 정리들을 사용하면 Lean의 커널에서 계산이 막혀, Nat 타입의 닫힌 항이 더 이상 숫자로 계산되지 않을 수 있음을 살펴보겠습니다. 그러나 Lean은 정의를 실행 가능한 코드로 컴파일할 때 타입과 명제 정보를 소거하며, 이러한 공리들은 새로운 명제만을 추가할 뿐이므로 그러한 계산적 해석과 양립 가능합니다. 계산에 관심이 있는 사용자라도 계산에 대해 추론하기 위해 고전적인 배중률(law of the excluded middle)을 사용하고 싶을 수 있습니다. 이 역시 커널에서의 계산을 막지만, 컴파일된 코드와는 양립 가능합니다.
표준 라이브러리는 계산적 해석과는 완전히 상반되는 선택 원리도 정의합니다. 이 원리는 어떤 것의 존재를 주장하는 명제로부터 마치 마법처럼 “데이터”를 만들어내기 때문입니다. 이 원리의 사용은 일부 고전적인 구성에서 필수적이며, 사용자는 필요할 때 이를 가져올 수 있습니다. 하지만 이 구성을 사용해 데이터를 만들어내는 표현식은 계산적 내용을 갖지 않으며, Lean에서는 이러한 사실을 나타내기 위해 그런 정의에 noncomputable 표시를 붙이도록 요구됩니다.
영리한 트릭(디아코네스쿠의 정리로 알려져 있음)을 사용하면, 명제 외연성, 함수 외연성, 선택 공리를 이용하여 배중률을 도출할 수 있습니다. 그러나 위에서 언급했듯이, 배중률의 사용은 데이터를 만들어 내는 데 사용되지 않는 한 다른 고전적 원리들과 마찬가지로 컴파일과 여전히 호환됩니다.
요약하자면, 유니버스, 의존 함수 타입, 귀납적 타입이라는 기저 프레임워크 위에, 표준 라이브러리는 세 가지 추가 구성 요소를 더합니다.
-
명제 외연성 공리
-
함수 외연성을 함의하는 몫 구성
-
존재 명제로부터 데이터를 생성하는 선택 원리입니다.
이 중 처음 두 가지는 Lean 내에서의 정규화를 차단하지만 코드 생성과는 호환되는 반면, 세 번째는 계산적 해석에 적합하지 않습니다. 아래에서 세부 사항을 더 정확하게 설명하겠습니다.
12.1. 역사적, 철학적 맥락
수학은 그 역사 대부분에 걸쳐 본질적으로 계산적이었습니다. 기하학은 기하학적 대상의 작도를 다루었고, 대수학은 방정식 체계에 대한 알고리즘적 해법에 관심을 두었으며, 해석학은 시간에 따라 변화하는 시스템의 미래 거동을 계산하는 수단을 제공했습니다. “모든 x에 대해, ...를 만족하는 y가 존재한다”는 취지의 정리에 대한 증명으로부터, x가 주어졌을 때 그러한 y를 계산하는 알고리즘을 추출하는 것은 일반적으로 어렵지 않은 일이었습니다.
그러나 19세기에 들어서면서 수학적 논증의 복잡성이 증가함에 따라, 수학자들은 알고리즘적 정보를 배제하고 수학적 대상이 어떻게 표현되는지에 대한 세부 사항을 추상화하는 방식으로 그 대상을 기술하는 새로운 형태의 추론 방식을 개발하게 되었습니다. 그 목표는 계산적 세부 사항에 얽매이지 않으면서도 강력한 “개념적” 이해를 얻는 것이었지만, 이는 직접적인 계산적 해석으로는 그저 거짓인 수학 정리들을 받아들이는 결과를 낳았습니다.
오늘날에도 계산이 수학에서 중요하다는 데에는 여전히 상당히 일치된 의견이 존재합니다. 하지만 계산적 관심사를 어떻게 다루는 것이 최선인지에 대해서는 견해가 다릅니다. constructive(구성적) 관점에서 보면, 수학을 그 계산적 뿌리로부터 분리하는 것은 잘못이며, 의미 있는 모든 수학적 정리는 직접적인 계산적 해석을 가져야 합니다. classical(고전적) 관점에서 보면, 관심사를 분리해서 유지하는 편이 더 유익합니다. 즉, 컴퓨터 프로그램을 작성할 때는 하나의 언어와 방법 체계를 사용하되, 그것에 대해 추론할 때는 비구성적 이론과 방법을 사용할 자유를 유지할 수 있습니다. Lean은 이 두 접근 방식을 모두 지원하도록 설계되었습니다. 라이브러리의 핵심 부분은 구성적으로 개발되었지만, 이 시스템은 고전적 수학적 추론을 수행할 수 있는 지원도 제공합니다.
계산적으로, 의존 타입 이론에서 가장 순수한 부분은 Prop의 사용을 완전히 피합니다. 귀납적 타입과 의존 함수 타입은 데이터 타입으로 볼 수 있으며, 이러한 타입의 항은 더 이상 적용할 수 있는 규칙이 없을 때까지 축약 규칙을 적용함으로써 “평가”될 수 있습니다. 원칙적으로 Nat 타입의 임의의 닫힌 항(즉, 자유 변수가 없는 항)은 수치, 즉 succ (… (succ zero)…)으로 평가되어야 합니다.
증명 무관성을 갖는 Prop을 도입하고 정리를 축약 불가능한 것으로 표시하는 것은 관심사 분리를 향한 첫걸음에 해당합니다. 의도는 타입 p : Prop의 원소가 계산에서 아무 역할도 하지 않아야 한다는 것이며, 그런 의미에서 항 prf : p의 구체적인 구성은 “무관”합니다. 그럼에도 Prop 타입의 원소를 포함하는 계산적 객체를 정의할 수 있습니다. 요점은 이러한 원소들이 계산의 효과에 대해 추론하는 데 도움을 줄 수 있지만, 항에서 “코드”를 추출할 때는 무시할 수 있다는 것입니다. 하지만 Prop 타입의 원소가 전적으로 무해한 것은 아닙니다. 이는 임의의 타입 α에 대한 방정식 s = t : α를 포함하며, 이러한 방정식은 항의 타입을 검사하기 위한 캐스트로 사용될 수 있습니다. 아래에서는 이러한 캐스트가 시스템에서 계산을 어떻게 가로막을 수 있는지 예시를 살펴보겠습니다. 그러나 명제적 내용을 소거하고, 중간 타입 제약을 무시하며, 항이 정규형에 도달할 때까지 축약하는 평가 방식에서는 여전히 계산이 가능합니다. 이것이 바로 Lean의 가상 머신이 수행하는 작업입니다.
증명 무관성을 갖는 Prop을 채택했다면, 예를 들어 배중률인 p ∨ ¬p를 사용하는 것이 정당하다고 여길 수 있는데, 여기서 p는 임의의 명제입니다. 물론 이 또한 CIC의 규칙에 따라 계산을 막을 수는 있지만, 앞서 설명한 것처럼 실행 가능한 코드의 생성을 막지는 않습니다. 이론에서 증명 무관 부분과 데이터 관련 부분 사이의 구분을 완전히 지워버리는 것은 오직 선택에 관한 절에서 논의하는 선택 원리뿐입니다.
12.2. 명제적 확장성
명제 외연성(propositional extensionality)은 다음과 같은 공리입니다:
axiom propext {a b : Prop} : (a ↔ b) → a = b
이는 두 명제가 서로를 함의할 때, 실제로 두 명제가 같다는 것을 단언합니다. 이는 임의의 원소 a : Prop가 공집합이거나, 어떤 특정 원소 \ast에 대해 단집합 \{\ast\}인 집합론적 해석과 일치합니다. 이 공리는 동치인 명제들이 어떤 맥락에서든 서로 대체될 수 있다는 효과를 가집니다.
12.3. 함수 외연성
명제적 외연성과 마찬가지로, 함수 외연성은 모든 입력에 대해 값이 일치하는 (x : α) → β x 타입의 두 함수는 서로 같다고 주장합니다:
funext.{u, v}
{α : Sort u} {β : α → Sort v}
{f g : (x : α) → β x}
(h : ∀ (x : α), f x = g x) :
f = g
고전적인 집합론적 관점에서 보면, 이것이 바로 두 함수가 같다는 것이 의미하는 바입니다. 이는 함수에 대한 “외연적(extensional)” 관점으로 알려져 있습니다. 그러나 구성적 관점에서는 함수를 어떤 명시적인 방식으로 제시되는 알고리즘, 즉 컴퓨터 프로그램으로 생각하는 것이 더 자연스러울 때가 있습니다. 두 컴퓨터 프로그램이 구문적으로는 상당히 다르더라도 모든 입력에 대해 동일한 답을 계산할 수 있는 경우는 분명히 존재합니다. 이와 매우 비슷하게, 입력/출력 동작이 같은 두 함수를 반드시 동일시하지는 않는 함수 관점을 유지하고 싶을 수도 있습니다. 이는 함수에 대한 “내포적(intensional)” 관점으로 알려져 있습니다.
사실, 함수 외연성은 몫의 존재로부터 따라 나오는데, 이는 다음 절에서 다루겠습니다. 따라서 Lean 표준 라이브러리에서 funext는 몫 구성으로부터 증명됩니다.
α : Type u에 대해 α의 부분집합 타입을 나타내기 위해 Set α:= α → Prop를 정의한다고 가정하면, 이는 본질적으로 부분집합을 술어와 동일시하는 것입니다. funext와 propext를 결합함으로써, 우리는 이러한 집합에 대한 외연적 이론을 얻습니다.
def Set (α : Type u) := α → Prop
namespace Set
def mem (x : α) (a : Set α) := a x
infix:50 (priority := high) "∈" => mem
theorem setext {a b : Set α} (h : ∀ x, x ∈ a ↔ x ∈ b) : a = b :=
funext (fun x => propext (h x))
end Set
그런 다음 예를 들어 공집합과 집합 교집합을 정의하고, 집합에 대한 항등식을 증명할 수 있습니다.
def Set (α : Type u) := α → Prop
namespace Set
def mem (x : α) (a : Set α) := a x
infix:50 (priority := high) "∈" => mem
theorem setext {a b : Set α} (h : ∀ x, x ∈ a ↔ x ∈ b) : a = b :=
funext (fun x => propext (h x))
def empty : Set α := fun _ => False
notation (priority := high) "∅" => empty
def inter (a b : Set α) : Set α :=
fun x => x ∈ a ∧ x ∈ b
infix:70 " ∩ " => inter
theorem inter_self (a : Set α) : a ∩ a = a :=
setext fun x => Iff.intro
(fun ⟨h, _⟩ => h)
(fun h => ⟨h, h⟩)
theorem inter_empty (a : Set α) : a ∩ ∅ = ∅ :=
setext fun _ => Iff.intro
(fun ⟨_, h⟩ => h)
(fun h => False.elim h)
theorem empty_inter (a : Set α) : ∅ ∩ a = ∅ :=
setext fun _ => Iff.intro
(fun ⟨h, _⟩ => h)
(fun h => False.elim h)
theorem inter.comm (a b : Set α) : a ∩ b = b ∩ a :=
setext fun _ => Iff.intro
(fun ⟨h₁, h₂⟩ => ⟨h₂, h₁⟩)
(fun ⟨h₁, h₂⟩ => ⟨h₂, h₁⟩)
end Set
다음은 함수 외연성이 Lean 커널 내부에서 계산을 어떻게 막는지 보여주는 예시입니다:
def f (x : Nat) := x
def g (x : Nat) := 0 + x
theorem f_eq_g : f = g :=
funext fun x => (Nat.zero_add x).symm
def val : Nat :=
Eq.recOn (motive := fun _ _ => Nat) f_eq_g 0
-- does not reduce to 0
#reduce val
-- evaluates to 0
#eval val
먼저 함수 외연성을 사용하여 두 함수 f와 g가 같음을 보이고, 그다음 타입에서 f를 g로 치환하여 Nat 타입의 0을 캐스팅합니다. 물론 Nat는 f에 의존하지 않으므로 이 캐스팅은 공허합니다. 하지만 그것만으로도 문제를 일으키기에 충분합니다. 시스템의 계산 규칙 하에서, 우리는 이제 숫자로 축약되지 않는 Nat의 닫힌 항을 갖게 됩니다. 이 경우, 우리는 표현식을 0으로 축약하고 싶은 유혹을 느낄 수 있습니다. 하지만 자명하지 않은 예제에서는 캐스팅을 제거하면 항의 타입이 변경되어, 주변 표현식의 타입이 부정확해질 수 있습니다. 그러나 가상 머신은 표현식을 0으로 평가하는 데 아무런 문제가 없습니다. 다음은 propext가 어떻게 방해가 될 수 있는지를 보여주는, 이와 유사하게 고안된 예제입니다.
theorem tteq : (True ∧ True) = True :=
propext (Iff.intro (fun ⟨h, _⟩ => h) (fun h => ⟨h, h⟩))
def val : Nat :=
Eq.recOn (motive := fun _ _ => Nat) tteq 0
-- does not reduce to 0
#reduce val
-- evaluates to 0
#eval val관찰적 타입 이론과 큐빅 타입 이론 연구를 비롯한 현재의 연구 프로그램들은 함수 외연성, 몫(quotient) 등을 포함하는 캐스트에 대한 축약을 허용하는 방식으로 타입 이론을 확장하는 것을 목표로 합니다. 그러나 그 해법들은 그리 명확하지 않으며, Lean의 근간이 되는 계산법의 규칙은 그러한 축약을 허용하지 않습니다.
하지만 어떤 의미에서는 캐스트가 표현식의 의미를 바꾸지는 않습니다. 오히려 이는 표현식의 타입에 대해 추론하기 위한 메커니즘입니다. 적절한 의미론이 주어지면, 축소가 타입상 올바르게 되도록 하는 데 필요한 중간 부기 작업을 무시하고, 항을 그 의미를 보존하는 방식으로 축소하는 것이 타당해집니다. 그런 경우, Prop에 새로운 공리를 추가하는 것은 문제가 되지 않습니다. 증명 무관성에 의해, Prop에 속한 표현식은 아무 정보도 담고 있지 않으므로, 축소 절차에서 안전하게 무시될 수 있습니다.
12.4. 몫
α를 임의의 타입이라 하고, r을 α에 대한 동치 관계라 합시다. “몫” α / r, 즉 α의 원소들을 r로 “나눈” 타입을 구성하는 것은 수학적으로 흔한 일입니다. 집합론적으로는 α / r을 r에 대한 α의 동치류들의 집합으로 볼 수 있습니다. f : α → β가 모든 x y : α에 대해 r x y가 f x = f y를 함의한다는 의미에서 동치 관계를 존중하는 임의의 함수라면, f는 각 동치류 ⟦x⟧에서 f' ⟦x⟧ = f x로 정의되는 함수 f' : α / r → β로 “들어올려집니다”. Lean의 표준 라이브러리는 바로 이러한 구성들을 수행하는 추가 상수들로 구성 계산법(Calculus of Constructions)을 확장하며, 이 마지막 방정식을 정의적 축약 규칙으로 설치합니다.
가장 기본적인 형태에서, 몫 구성은 r이 동치 관계일 것을 요구하지도 않습니다. 다음 상수들은 Lean에 내장되어 있습니다:
universe u v
axiom Quot : {α : Sort u} → (α → α → Prop) → Sort u
axiom Quot.mk : {α : Sort u} → (r : α → α → Prop) → α → Quot r
axiom Quot.ind :
∀ {α : Sort u} {r : α → α → Prop} {β : Quot r → Prop},
(∀ a, β (Quot.mk r a)) → (q : Quot r) → β q
axiom Quot.lift :
{α : Sort u} → {r : α → α → Prop} → {β : Sort u} → (f : α → β)
→ (∀ a b, r a b → f a = f b) → Quot r → β
첫 번째 원리는 α 위의 임의의 이항 관계 r에 의해, 타입 α가 주어졌을 때 타입 Quot r을 형성합니다. 두 번째 원리는 α를 Quot α로 사상하며, 이에 따라 r : α → α → Prop이고 a : α이면 Quot.mk r a는 Quot r의 원소가 됩니다. 세 번째 원리인 Quot.ind는 Quot.mk r a의 모든 원소가 이러한 형태임을 말합니다. Quot.lift에 관해서는, 함수 f : α → β가 주어졌을 때 h가 f가 관계 r을 보존한다는 증명이라면, Quot.lift f h는 Quot r 위의 대응하는 함수가 됩니다. 그 개념은, α의 각 원소 a에 대해 함수 Quot.lift f h가 Quot.mk r a(a를 포함하는 r-클래스)를 f a로 사상하며, 이때 h가 이 함수가 well-defined임을 보여준다는 것입니다. 실제로, 아래의 증명에서 명확히 드러나듯이 계산 원리는 축약 규칙으로 선언됩니다.
def mod7Rel (x y : Nat) : Prop :=
x % 7 = y % 7
-- the quotient type
#check (Quot mod7Rel : Type)
-- the class of numbers equivalent to 4
#check (Quot.mk mod7Rel 4 : Quot mod7Rel)
def f (x : Nat) : Bool :=
x % 7 = 0
theorem f_respects (a b : Nat) (h : mod7Rel a b) : f a = f b := a:Natb:Nath:mod7Rel a b⊢ f a = f b
a:Natb:Nath:a % 7 = b % 7⊢ a % 7 = 0 ↔ b % 7 = 0
All goals completed! 🐙
#check (Quot.lift f f_respects : Quot mod7Rel → Bool)
-- the computation principle
example (a : Nat) : Quot.lift f f_respects (Quot.mk mod7Rel a) = f a :=
rfl
Quot, Quot.mk, Quot.ind, Quot.lift라는 네 개의 상수는 그 자체만으로는 그리 강력하지 않습니다. Quot r을 단순히 α로 두고 Quot.lift를 (h를 무시한) 항등 함수로 두면 Quot.ind가 만족됨을 확인할 수 있습니다. 이러한 이유로 이 네 개의 상수는 추가적인 공리로 간주되지 않습니다.
이들은 귀납적으로 정의된 타입 및 그와 연관된 생성자와 재귀자와 마찬가지로, 논리적 프레임워크의 일부로 간주됩니다.
Quot 구성을 진정한 몫으로 만드는 것은 다음의 추가 공리입니다.
이것은 r에 의해 관계된 α의 임의의 두 원소가 몫에서 동일시된다고 단언하는 공리입니다. 정리나 정의가 Quot.sound를 사용하면, 이는 #print axioms 명령에 나타납니다.
물론 몫 구성은 r이 동치 관계인 상황에서 가장 흔히 사용됩니다. 위와 같이 r이 주어졌을 때, r' a b가 Quot.mk r a = Quot.mk r b와 동치라는 규칙에 따라 r'을 정의하면, r'이 동치 관계임이 분명합니다. 실제로 r'은 함수 fun a => Quot.mk r a의 커널입니다. 공리 Quot.sound는 r a b가 r' a b를 함의함을 말합니다. Quot.lift와 Quot.ind를 사용하면, r'이 r을 포함하는 가장 작은 동치 관계임을 보일 수 있습니다. 이는 r''이 r을 포함하는 임의의 동치 관계라면 r' a b가 r'' a b를 함의한다는 의미입니다. 특히, r이 애초에 동치 관계였다면, 모든 a와 b에 대해 r a b iff r' a b가 성립합니다.
이러한 일반적인 사용 사례를 지원하기 위해, 표준 라이브러리는 setoid라는 개념을 정의합니다. 이는 단순히 연관된 동치 관계를 갖는 타입입니다.
class Setoid (α : Sort u) where
r : α → α → Prop
iseqv : Equivalence r
instance {α : Sort u} [Setoid α] : HasEquiv α :=
⟨Setoid.r⟩
namespace Setoid
variable {α : Sort u} [Setoid α]
theorem refl (a : α) : a ≈ a :=
iseqv.refl a
theorem symm {a b : α} (hab : a ≈ b) : b ≈ a :=
iseqv.symm hab
theorem trans {a b c : α} (hab : a ≈ b) (hbc : b ≈ c) : a ≈ c :=
iseqv.trans hab hbc
end Setoid
타입 α, α 위의 관계 r, 그리고 r이 동치 관계임을 나타내는 증명 iseqv가 주어지면, Setoid 클래스의 인스턴스를 정의할 수 있습니다.
상수 Quotient.mk, Quotient.ind, Quotient.lift, Quotient.sound는 Quot의 해당 요소들을 특수화한 것에 지나지 않습니다. 타입 클래스 추론이 타입 α와 연관된 세토이드(setoid)를 찾아낼 수 있다는 사실은 여러 이점을 가져다줍니다. 먼저, Setoid.r a b에 대해 표기법 a ≈ b(\approx로 입력)를 사용할 수 있는데, 이때 표기법 Setoid.r에서 Setoid의 인스턴스는 암묵적으로 처리됩니다. 일반적인 정리 Setoid.refl, Setoid.symm, Setoid.trans를 사용해 그 관계에 대해 추론할 수 있습니다. 특히 몫(quotient)에 대해서는 정리 Quotient.exact를 사용할 수 있습니다.
Quotient.exact {α : Sort u} {s : Setoid α} {a b : α} :
Quotient.mk s a = Quotient.mk s b →
a ≈ b
Quotient.sound와 함께, 이는 몫의 원소들이 α에 속한 원소들의 동치류에 정확히 대응함을 의미합니다.
표준 라이브러리에서 α × β는 타입 α와 β의 데카르트 곱을 나타낸다는 것을 상기하십시오. 몫의 사용을 보여주기 위해, 타입 α의 원소들로 이루어진 순서 없는 쌍의 타입을 타입 α × α의 몫으로 정의해 봅시다. 먼저, 관련된 동치 관계를 정의합니다.
private def eqv (p₁ p₂ : α × α) : Prop :=
(p₁.1 = p₂.1 ∧ p₁.2 = p₂.2) ∨ (p₁.1 = p₂.2 ∧ p₁.2 = p₂.1)
infix:50 " ~ " => eqv
다음 단계는 eqv가 실제로 동치 관계, 즉 반사적이고 대칭적이며 추이적임을 증명하는 것입니다. 의존 패턴 매칭을 사용하여 경우 분석을 수행하고 가설을 조각으로 나눈 뒤 이를 다시 조합하여 결론을 도출함으로써, 이 세 가지 사실을 편리하고 가독성 있는 방식으로 증명할 수 있습니다.
private def eqv (p₁ p₂ : α × α) : Prop :=
(p₁.1 = p₂.1 ∧ p₁.2 = p₂.2) ∨ (p₁.1 = p₂.2 ∧ p₁.2 = p₂.1)
infix:50 " ~ " => eqv
private theorem eqv.refl (p : α × α) : p ~ p :=
Or.inl ⟨rfl, rfl⟩
private theorem eqv.symm : ∀ {p₁ p₂ : α × α}, p₁ ~ p₂ → p₂ ~ p₁
| (a₁, a₂), (b₁, b₂), (Or.inl ⟨a₁b₁, a₂b₂⟩) =>
Or.inl (α:Type u_1a₁:αa₂:αb₁:αb₂:αa₁b₁:(a₁, a₂).fst = (b₁, b₂).fsta₂b₂:(a₁, a₂).snd = (b₁, b₂).snd⊢ (b₁, b₂).fst = (a₁, a₂).fst ∧ (b₁, b₂).snd = (a₁, a₂).snd All goals completed! 🐙)
| (a₁, a₂), (b₁, b₂), (Or.inr ⟨a₁b₂, a₂b₁⟩) =>
Or.inr (α:Type u_1a₁:αa₂:αb₁:αb₂:αa₁b₂:(a₁, a₂).fst = (b₁, b₂).snda₂b₁:(a₁, a₂).snd = (b₁, b₂).fst⊢ (b₁, b₂).fst = (a₁, a₂).snd ∧ (b₁, b₂).snd = (a₁, a₂).fst All goals completed! 🐙)
private theorem eqv.trans : ∀ {p₁ p₂ p₃ : α × α}, p₁ ~ p₂ → p₂ ~ p₃ → p₁ ~ p₃
| (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inl ⟨a₁b₁, a₂b₂⟩, Or.inl ⟨b₁c₁, b₂c₂⟩ =>
Or.inl (α:Type u_1a₁:αa₂:αb₁:αb₂:αc₁:αc₂:αa₁b₁:(a₁, a₂).fst = (b₁, b₂).fsta₂b₂:(a₁, a₂).snd = (b₁, b₂).sndb₁c₁:(b₁, b₂).fst = (c₁, c₂).fstb₂c₂:(b₁, b₂).snd = (c₁, c₂).snd⊢ (a₁, a₂).fst = (c₁, c₂).fst ∧ (a₁, a₂).snd = (c₁, c₂).snd All goals completed! 🐙)
| (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inl ⟨a₁b₁, a₂b₂⟩, Or.inr ⟨b₁c₂, b₂c₁⟩ =>
Or.inr (α:Type u_1a₁:αa₂:αb₁:αb₂:αc₁:αc₂:αa₁b₁:(a₁, a₂).fst = (b₁, b₂).fsta₂b₂:(a₁, a₂).snd = (b₁, b₂).sndb₁c₂:(b₁, b₂).fst = (c₁, c₂).sndb₂c₁:(b₁, b₂).snd = (c₁, c₂).fst⊢ (a₁, a₂).fst = (c₁, c₂).snd ∧ (a₁, a₂).snd = (c₁, c₂).fst All goals completed! 🐙)
| (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inr ⟨a₁b₂, a₂b₁⟩, Or.inl ⟨b₁c₁, b₂c₂⟩ =>
Or.inr (α:Type u_1a₁:αa₂:αb₁:αb₂:αc₁:αc₂:αa₁b₂:(a₁, a₂).fst = (b₁, b₂).snda₂b₁:(a₁, a₂).snd = (b₁, b₂).fstb₁c₁:(b₁, b₂).fst = (c₁, c₂).fstb₂c₂:(b₁, b₂).snd = (c₁, c₂).snd⊢ (a₁, a₂).fst = (c₁, c₂).snd ∧ (a₁, a₂).snd = (c₁, c₂).fst All goals completed! 🐙)
| (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inr ⟨a₁b₂, a₂b₁⟩, Or.inr ⟨b₁c₂, b₂c₁⟩ =>
Or.inl (α:Type u_1a₁:αa₂:αb₁:αb₂:αc₁:αc₂:αa₁b₂:(a₁, a₂).fst = (b₁, b₂).snda₂b₁:(a₁, a₂).snd = (b₁, b₂).fstb₁c₂:(b₁, b₂).fst = (c₁, c₂).sndb₂c₁:(b₁, b₂).snd = (c₁, c₂).fst⊢ (a₁, a₂).fst = (c₁, c₂).fst ∧ (a₁, a₂).snd = (c₁, c₂).snd All goals completed! 🐙)
private theorem is_equivalence : Equivalence (@eqv α) :=
{ refl := eqv.refl, symm := eqv.symm, trans := eqv.trans }
이제 eqv가 동치 관계임을 증명했으므로, Setoid (α × α)를 구성할 수 있으며, 이를 이용해 순서 없는 쌍의 타입 UProd α를 정의할 수 있습니다.
private def eqv (p₁ p₂ : α × α) : Prop :=
(p₁.1 = p₂.1 ∧ p₁.2 = p₂.2) ∨ (p₁.1 = p₂.2 ∧ p₁.2 = p₂.1)
infix:50 " ~ " => eqv
private theorem eqv.refl (p : α × α) : p ~ p :=
Or.inl ⟨rfl, rfl⟩
private theorem eqv.symm : ∀ {p₁ p₂ : α × α}, p₁ ~ p₂ → p₂ ~ p₁
| (a₁, a₂), (b₁, b₂), (Or.inl ⟨a₁b₁, a₂b₂⟩) =>
Or.inl (α:Type u_1a₁:αa₂:αb₁:αb₂:αa₁b₁:(a₁, a₂).fst = (b₁, b₂).fsta₂b₂:(a₁, a₂).snd = (b₁, b₂).snd⊢ (b₁, b₂).fst = (a₁, a₂).fst ∧ (b₁, b₂).snd = (a₁, a₂).snd All goals completed! 🐙)
| (a₁, a₂), (b₁, b₂), (Or.inr ⟨a₁b₂, a₂b₁⟩) =>
Or.inr (α:Type u_1a₁:αa₂:αb₁:αb₂:αa₁b₂:(a₁, a₂).fst = (b₁, b₂).snda₂b₁:(a₁, a₂).snd = (b₁, b₂).fst⊢ (b₁, b₂).fst = (a₁, a₂).snd ∧ (b₁, b₂).snd = (a₁, a₂).fst All goals completed! 🐙)
private theorem eqv.trans : ∀ {p₁ p₂ p₃ : α × α}, p₁ ~ p₂ → p₂ ~ p₃ → p₁ ~ p₃
| (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inl ⟨a₁b₁, a₂b₂⟩, Or.inl ⟨b₁c₁, b₂c₂⟩ =>
Or.inl (α:Type u_1a₁:αa₂:αb₁:αb₂:αc₁:αc₂:αa₁b₁:(a₁, a₂).fst = (b₁, b₂).fsta₂b₂:(a₁, a₂).snd = (b₁, b₂).sndb₁c₁:(b₁, b₂).fst = (c₁, c₂).fstb₂c₂:(b₁, b₂).snd = (c₁, c₂).snd⊢ (a₁, a₂).fst = (c₁, c₂).fst ∧ (a₁, a₂).snd = (c₁, c₂).snd All goals completed! 🐙)
| (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inl ⟨a₁b₁, a₂b₂⟩, Or.inr ⟨b₁c₂, b₂c₁⟩ =>
Or.inr (α:Type u_1a₁:αa₂:αb₁:αb₂:αc₁:αc₂:αa₁b₁:(a₁, a₂).fst = (b₁, b₂).fsta₂b₂:(a₁, a₂).snd = (b₁, b₂).sndb₁c₂:(b₁, b₂).fst = (c₁, c₂).sndb₂c₁:(b₁, b₂).snd = (c₁, c₂).fst⊢ (a₁, a₂).fst = (c₁, c₂).snd ∧ (a₁, a₂).snd = (c₁, c₂).fst All goals completed! 🐙)
| (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inr ⟨a₁b₂, a₂b₁⟩, Or.inl ⟨b₁c₁, b₂c₂⟩ =>
Or.inr (α:Type u_1a₁:αa₂:αb₁:αb₂:αc₁:αc₂:αa₁b₂:(a₁, a₂).fst = (b₁, b₂).snda₂b₁:(a₁, a₂).snd = (b₁, b₂).fstb₁c₁:(b₁, b₂).fst = (c₁, c₂).fstb₂c₂:(b₁, b₂).snd = (c₁, c₂).snd⊢ (a₁, a₂).fst = (c₁, c₂).snd ∧ (a₁, a₂).snd = (c₁, c₂).fst All goals completed! 🐙)
| (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inr ⟨a₁b₂, a₂b₁⟩, Or.inr ⟨b₁c₂, b₂c₁⟩ =>
Or.inl (α:Type u_1a₁:αa₂:αb₁:αb₂:αc₁:αc₂:αa₁b₂:(a₁, a₂).fst = (b₁, b₂).snda₂b₁:(a₁, a₂).snd = (b₁, b₂).fstb₁c₂:(b₁, b₂).fst = (c₁, c₂).sndb₂c₁:(b₁, b₂).snd = (c₁, c₂).fst⊢ (a₁, a₂).fst = (c₁, c₂).fst ∧ (a₁, a₂).snd = (c₁, c₂).snd All goals completed! 🐙)
private theorem is_equivalence : Equivalence (@eqv α) :=
{ refl := eqv.refl, symm := eqv.symm, trans := eqv.trans }
instance uprodSetoid (α : Type u) : Setoid (α × α) where
r := eqv
iseqv := is_equivalence
def UProd (α : Type u) : Type u :=
Quotient (uprodSetoid α)
namespace UProd
def mk {α : Type} (a₁ a₂ : α) : UProd α :=
Quotient.mk' (a₁, a₂)
notation "{ " a₁ ", " a₂ " }" => mk a₁ a₂
end UProd
순서 없는 쌍에 대한 표기법 {a₁, a₂}를 Quotient.mk' (a₁, a₂)로 지역적으로 정의하고 있음에 주목하십시오. 이는 예시를 보여주는 목적으로는 유용하지만, 이 표기법이 레코드나 집합 등에 쓰이는 중괄호의 다른 용법을 가려버리므로 일반적으로는 좋은 방법이 아닙니다.
(a₁, a₂) ~ (a₂, a₁)이 성립하므로, Quot.sound를 사용하여 {a₁, a₂} = {a₂, a₁}임을 쉽게 증명할 수 있습니다.
private def eqv (p₁ p₂ : α × α) : Prop :=
(p₁.1 = p₂.1 ∧ p₁.2 = p₂.2) ∨ (p₁.1 = p₂.2 ∧ p₁.2 = p₂.1)
infix:50 " ~ " => eqv
private theorem eqv.refl (p : α × α) : p ~ p :=
Or.inl ⟨rfl, rfl⟩
private theorem eqv.symm : ∀ {p₁ p₂ : α × α}, p₁ ~ p₂ → p₂ ~ p₁
| (a₁, a₂), (b₁, b₂), (Or.inl ⟨a₁b₁, a₂b₂⟩) =>
Or.inl (α:Type u_1a₁:αa₂:αb₁:αb₂:αa₁b₁:(a₁, a₂).fst = (b₁, b₂).fsta₂b₂:(a₁, a₂).snd = (b₁, b₂).snd⊢ (b₁, b₂).fst = (a₁, a₂).fst ∧ (b₁, b₂).snd = (a₁, a₂).snd All goals completed! 🐙)
| (a₁, a₂), (b₁, b₂), (Or.inr ⟨a₁b₂, a₂b₁⟩) =>
Or.inr (α:Type u_1a₁:αa₂:αb₁:αb₂:αa₁b₂:(a₁, a₂).fst = (b₁, b₂).snda₂b₁:(a₁, a₂).snd = (b₁, b₂).fst⊢ (b₁, b₂).fst = (a₁, a₂).snd ∧ (b₁, b₂).snd = (a₁, a₂).fst All goals completed! 🐙)
private theorem eqv.trans : ∀ {p₁ p₂ p₃ : α × α}, p₁ ~ p₂ → p₂ ~ p₃ → p₁ ~ p₃
| (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inl ⟨a₁b₁, a₂b₂⟩, Or.inl ⟨b₁c₁, b₂c₂⟩ =>
Or.inl (α:Type u_1a₁:αa₂:αb₁:αb₂:αc₁:αc₂:αa₁b₁:(a₁, a₂).fst = (b₁, b₂).fsta₂b₂:(a₁, a₂).snd = (b₁, b₂).sndb₁c₁:(b₁, b₂).fst = (c₁, c₂).fstb₂c₂:(b₁, b₂).snd = (c₁, c₂).snd⊢ (a₁, a₂).fst = (c₁, c₂).fst ∧ (a₁, a₂).snd = (c₁, c₂).snd All goals completed! 🐙)
| (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inl ⟨a₁b₁, a₂b₂⟩, Or.inr ⟨b₁c₂, b₂c₁⟩ =>
Or.inr (α:Type u_1a₁:αa₂:αb₁:αb₂:αc₁:αc₂:αa₁b₁:(a₁, a₂).fst = (b₁, b₂).fsta₂b₂:(a₁, a₂).snd = (b₁, b₂).sndb₁c₂:(b₁, b₂).fst = (c₁, c₂).sndb₂c₁:(b₁, b₂).snd = (c₁, c₂).fst⊢ (a₁, a₂).fst = (c₁, c₂).snd ∧ (a₁, a₂).snd = (c₁, c₂).fst All goals completed! 🐙)
| (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inr ⟨a₁b₂, a₂b₁⟩, Or.inl ⟨b₁c₁, b₂c₂⟩ =>
Or.inr (α:Type u_1a₁:αa₂:αb₁:αb₂:αc₁:αc₂:αa₁b₂:(a₁, a₂).fst = (b₁, b₂).snda₂b₁:(a₁, a₂).snd = (b₁, b₂).fstb₁c₁:(b₁, b₂).fst = (c₁, c₂).fstb₂c₂:(b₁, b₂).snd = (c₁, c₂).snd⊢ (a₁, a₂).fst = (c₁, c₂).snd ∧ (a₁, a₂).snd = (c₁, c₂).fst All goals completed! 🐙)
| (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inr ⟨a₁b₂, a₂b₁⟩, Or.inr ⟨b₁c₂, b₂c₁⟩ =>
Or.inl (α:Type u_1a₁:αa₂:αb₁:αb₂:αc₁:αc₂:αa₁b₂:(a₁, a₂).fst = (b₁, b₂).snda₂b₁:(a₁, a₂).snd = (b₁, b₂).fstb₁c₂:(b₁, b₂).fst = (c₁, c₂).sndb₂c₁:(b₁, b₂).snd = (c₁, c₂).fst⊢ (a₁, a₂).fst = (c₁, c₂).fst ∧ (a₁, a₂).snd = (c₁, c₂).snd All goals completed! 🐙)
private theorem is_equivalence : Equivalence (@eqv α) :=
{ refl := eqv.refl, symm := eqv.symm, trans := eqv.trans }
instance uprodSetoid (α : Type u) : Setoid (α × α) where
r := eqv
iseqv := is_equivalence
def UProd (α : Type u) : Type u :=
Quotient (uprodSetoid α)
namespace UProd
def mk {α : Type} (a₁ a₂ : α) : UProd α :=
Quotient.mk' (a₁, a₂)
notation "{ " a₁ ", " a₂ " }" => mk a₁ a₂
theorem mk_eq_mk (a₁ a₂ : α) : {a₁, a₂} = {a₂, a₁} :=
Quot.sound (Or.inr ⟨rfl, rfl⟩)
end UProd
예제를 완성하기 위해, a : α와 u : UProd α가 주어졌을 때, a ∈ u가 성립해야 함을 나타내는 명제를 정의합니다. 이는 a가 순서 없는 쌍 u의 원소 중 하나일 때 성립해야 하는 명제입니다. 먼저, (순서가 있는) 쌍에 대한 유사한 명제 mem_fnau를 정의한 다음, mem_fn이 보조정리 mem_respects를 통해 동치 관계 eqv를 보존함을 보입니다. 이는 Lean 표준 라이브러리에서 광범위하게 사용되는 관용구입니다.
set_option linter.unusedVariables false
private def eqv (p₁ p₂ : α × α) : Prop :=
(p₁.1 = p₂.1 ∧ p₁.2 = p₂.2) ∨ (p₁.1 = p₂.2 ∧ p₁.2 = p₂.1)
infix:50 " ~ " => eqv
private theorem eqv.refl (p : α × α) : p ~ p :=
Or.inl ⟨rfl, rfl⟩
private theorem eqv.symm : ∀ {p₁ p₂ : α × α}, p₁ ~ p₂ → p₂ ~ p₁
| (a₁, a₂), (b₁, b₂), (Or.inl ⟨a₁b₁, a₂b₂⟩) =>
Or.inl (α:Type u_1a₁:αa₂:αb₁:αb₂:αa₁b₁:(a₁, a₂).fst = (b₁, b₂).fsta₂b₂:(a₁, a₂).snd = (b₁, b₂).snd⊢ (b₁, b₂).fst = (a₁, a₂).fst ∧ (b₁, b₂).snd = (a₁, a₂).snd All goals completed! 🐙)
| (a₁, a₂), (b₁, b₂), (Or.inr ⟨a₁b₂, a₂b₁⟩) =>
Or.inr (α:Type u_1a₁:αa₂:αb₁:αb₂:αa₁b₂:(a₁, a₂).fst = (b₁, b₂).snda₂b₁:(a₁, a₂).snd = (b₁, b₂).fst⊢ (b₁, b₂).fst = (a₁, a₂).snd ∧ (b₁, b₂).snd = (a₁, a₂).fst All goals completed! 🐙)
private theorem eqv.trans : ∀ {p₁ p₂ p₃ : α × α}, p₁ ~ p₂ → p₂ ~ p₃ → p₁ ~ p₃
| (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inl ⟨a₁b₁, a₂b₂⟩, Or.inl ⟨b₁c₁, b₂c₂⟩ =>
Or.inl (α:Type u_1a₁:αa₂:αb₁:αb₂:αc₁:αc₂:αa₁b₁:(a₁, a₂).fst = (b₁, b₂).fsta₂b₂:(a₁, a₂).snd = (b₁, b₂).sndb₁c₁:(b₁, b₂).fst = (c₁, c₂).fstb₂c₂:(b₁, b₂).snd = (c₁, c₂).snd⊢ (a₁, a₂).fst = (c₁, c₂).fst ∧ (a₁, a₂).snd = (c₁, c₂).snd All goals completed! 🐙)
| (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inl ⟨a₁b₁, a₂b₂⟩, Or.inr ⟨b₁c₂, b₂c₁⟩ =>
Or.inr (α:Type u_1a₁:αa₂:αb₁:αb₂:αc₁:αc₂:αa₁b₁:(a₁, a₂).fst = (b₁, b₂).fsta₂b₂:(a₁, a₂).snd = (b₁, b₂).sndb₁c₂:(b₁, b₂).fst = (c₁, c₂).sndb₂c₁:(b₁, b₂).snd = (c₁, c₂).fst⊢ (a₁, a₂).fst = (c₁, c₂).snd ∧ (a₁, a₂).snd = (c₁, c₂).fst All goals completed! 🐙)
| (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inr ⟨a₁b₂, a₂b₁⟩, Or.inl ⟨b₁c₁, b₂c₂⟩ =>
Or.inr (α:Type u_1a₁:αa₂:αb₁:αb₂:αc₁:αc₂:αa₁b₂:(a₁, a₂).fst = (b₁, b₂).snda₂b₁:(a₁, a₂).snd = (b₁, b₂).fstb₁c₁:(b₁, b₂).fst = (c₁, c₂).fstb₂c₂:(b₁, b₂).snd = (c₁, c₂).snd⊢ (a₁, a₂).fst = (c₁, c₂).snd ∧ (a₁, a₂).snd = (c₁, c₂).fst All goals completed! 🐙)
| (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inr ⟨a₁b₂, a₂b₁⟩, Or.inr ⟨b₁c₂, b₂c₁⟩ =>
Or.inl (α:Type u_1a₁:αa₂:αb₁:αb₂:αc₁:αc₂:αa₁b₂:(a₁, a₂).fst = (b₁, b₂).snda₂b₁:(a₁, a₂).snd = (b₁, b₂).fstb₁c₂:(b₁, b₂).fst = (c₁, c₂).sndb₂c₁:(b₁, b₂).snd = (c₁, c₂).fst⊢ (a₁, a₂).fst = (c₁, c₂).fst ∧ (a₁, a₂).snd = (c₁, c₂).snd All goals completed! 🐙)
private theorem is_equivalence : Equivalence (@eqv α) :=
{ refl := eqv.refl, symm := eqv.symm, trans := eqv.trans }
instance uprodSetoid (α : Type u) : Setoid (α × α) where
r := eqv
iseqv := is_equivalence
def UProd (α : Type u) : Type u :=
Quotient (uprodSetoid α)
namespace UProd
def mk {α : Type} (a₁ a₂ : α) : UProd α :=
Quotient.mk' (a₁, a₂)
notation "{ " a₁ ", " a₂ " }" => mk a₁ a₂
theorem mk_eq_mk (a₁ a₂ : α) : {a₁, a₂} = {a₂, a₁} :=
Quot.sound (Or.inr ⟨rfl, rfl⟩)
private def mem_fn (a : α) : α × α → Prop
| (a₁, a₂) => a = a₁ ∨ a = a₂
-- auxiliary lemma for proving mem_respects
private theorem mem_swap {a : α} :
∀ {p : α × α}, mem_fn a p = mem_fn a (⟨p.2, p.1⟩)
α:Type u_1a:αa₁:αa₂:α⊢ mem_fn a (a₁, a₂) = mem_fn a ((a₁, a₂).snd, (a₁, a₂).fst) α:Type u_1a:αa₁:αa₂:α⊢ mem_fn a (a₁, a₂) = mem_fn a ((a₁, a₂).snd, (a₁, a₂).fst)
α:Type u_1a:αa₁:αa₂:α⊢ mem_fn a (a₁, a₂) ↔ mem_fn a ((a₁, a₂).snd, (a₁, a₂).fst)
α:Type u_1a:αa₁:αa₂:α⊢ mem_fn a (a₁, a₂) → mem_fn a ((a₁, a₂).snd, (a₁, a₂).fst)α:Type u_1a:αa₁:αa₂:α⊢ mem_fn a ((a₁, a₂).snd, (a₁, a₂).fst) → mem_fn a (a₁, a₂)
α:Type u_1a:αa₁:αa₂:α⊢ mem_fn a (a₁, a₂) → mem_fn a ((a₁, a₂).snd, (a₁, a₂).fst) intro
α:Type u_1a:αa₁:αa₂:αx✝:mem_fn a (a₁, a₂)h:a = a₁⊢ mem_fn a ((a₁, a₂).snd, (a₁, a₂).fst) All goals completed! 🐙
α:Type u_1a:αa₁:αa₂:αx✝:mem_fn a (a₁, a₂)h:a = a₂⊢ mem_fn a ((a₁, a₂).snd, (a₁, a₂).fst) All goals completed! 🐙
α:Type u_1a:αa₁:αa₂:α⊢ mem_fn a ((a₁, a₂).snd, (a₁, a₂).fst) → mem_fn a (a₁, a₂) intro
α:Type u_1a:αa₁:αa₂:αx✝:mem_fn a ((a₁, a₂).snd, (a₁, a₂).fst)h:a = (a₁, a₂).snd⊢ mem_fn a (a₁, a₂) All goals completed! 🐙
α:Type u_1a:αa₁:αa₂:αx✝:mem_fn a ((a₁, a₂).snd, (a₁, a₂).fst)h:a = (a₁, a₂).fst⊢ mem_fn a (a₁, a₂) All goals completed! 🐙
private theorem mem_respects : {p₁ p₂ : α × α} → (a : α) → p₁ ~ p₂ → mem_fn a p₁ = mem_fn a p₂
α:Type u_1a₁:αa₂:αb₁:αb₂:αa:αa₁b₁:(a₁, a₂).fst = (b₁, b₂).fsta₂b₂:(a₁, a₂).snd = (b₁, b₂).snd⊢ mem_fn a (a₁, a₂) = mem_fn a (b₁, b₂) α:Type u_1a₁:αa₂:αb₁:αb₂:αa:αa₁b₁:(a₁, a₂).fst = (b₁, b₂).fsta₂b₂:(a₁, a₂).snd = (b₁, b₂).snd⊢ mem_fn a (a₁, a₂) = mem_fn a (b₁, b₂)
All goals completed! 🐙
α:Type u_1a₁:αa₂:αb₁:αb₂:αa:αa₁b₂:(a₁, a₂).fst = (b₁, b₂).snda₂b₁:(a₁, a₂).snd = (b₁, b₂).fst⊢ mem_fn a (a₁, a₂) = mem_fn a (b₁, b₂) α:Type u_1a₁:αa₂:αb₁:αb₂:αa:αa₁b₂:(a₁, a₂).fst = (b₁, b₂).snda₂b₁:(a₁, a₂).snd = (b₁, b₂).fst⊢ mem_fn a (a₁, a₂) = mem_fn a (b₁, b₂)
α:Type u_1a₁:αa₂:αb₁:αb₂:αa:αa₁b₂:a₁ = b₂a₂b₁:a₂ = b₁⊢ mem_fn a (b₂, b₁) = mem_fn a (b₁, b₂)
All goals completed! 🐙
def mem (a : α) (u : UProd α) : Prop :=
Quot.liftOn u (fun p => mem_fn a p) (fun p₁ p₂ e => mem_respects a e)
infix:50 (priority := high) " ∈ " => mem
theorem mem_mk_left (a b : α) : a ∈ {a, b} :=
Or.inl rfl
theorem mem_mk_right (a b : α) : b ∈ {a, b} :=
Or.inr rfl
theorem mem_or_mem_of_mem_mk {a b c : α} : c ∈ {a, b} → c = a ∨ c = b :=
fun h => h
end UProd
편의를 위해 표준 라이브러리는 이항 함수를 리프팅하기 위한 Quotient.lift₂와 두 변수에 대한 귀납법을 위한 Quotient.ind₂도 정의합니다.
몫 구성이 왜 함수 외연성을 함의하는지에 대한 몇 가지 힌트로 이 절을 마무리하겠습니다. (x : α) → β x에서 외연적 동치가 동치 관계임을 보이는 것은 어렵지 않으며, 따라서 “동치까지” 함수들의 타입 extfun α β를 고려할 수 있습니다. 물론 적용은 그 동치를 존중하는데, 이는 f₁이 f₂와 동치이면 f₁ a가 f₂ a와 같다는 의미에서입니다. 따라서 적용은 함수 extfun_app : extfun α β → (x : α) → β x를 만들어냅니다. 하지만 모든 f에 대해, extfun_app (.mk _ f)는 fun x => f x와 정의적으로 같고, 이는 다시 f와 정의적으로 같습니다. 그러므로 f₁과 f₂가 외연적으로 동치일 때, 다음과 같은 동치의 연쇄를 얻습니다:
variable {α : Sort u} {β : α → Sort v}
def extfun (α : Sort u) (β : α → Sort v) := Quot (fun (f g : (x : α) → β x) => ∀ x, f x = g x)
def extfun_app {α β} (f : extfun α β) (x : α) : β x :=
Quot.lift (· x) (α✝:Sort uβ✝:α✝ → Sort vα:Sort ?u.9β:α → Sort ?u.8f:extfun α βx:α⊢ ∀ (a b : (x : α) → β x), (∀ (x : α), a x = b x) → a x = b x α✝:Sort uβ✝:α✝ → Sort vα:Sort ?u.9β:α → Sort ?u.8f:extfun α βx:αa✝¹:(x : α) → β xb✝:(x : α) → β xa✝:∀ (x : α), a✝¹ x = b✝ x⊢ a✝¹ x = b✝ x; All goals completed! 🐙) f
example (f₁ f₂ : (x : α) → β x) (h : ∀ x, f₁ x = f₂ x) :=
calc f₁
_ = extfun_app (.mk _ f₁) := rfl
_ = extfun_app (.mk _ f₂) := α:Sort uβ:α → Sort vf₁:(x : α) → β xf₂:(x : α) → β xh:∀ (x : α), f₁ x = f₂ x⊢ extfun_app (Quot.mk (fun f g => ∀ (x : α), f x = g x) f₁) = extfun_app (Quot.mk (fun f g => ∀ (x : α), f x = g x) f₂) α:Sort uβ:α → Sort vf₁:(x : α) → β xf₂:(x : α) → β xh:∀ (x : α), f₁ x = f₂ x⊢ ∀ (x : α), f₁ x = f₂ x; All goals completed! 🐙
_ = f₂ := rfl
결과적으로, f₁은(는) f₂와(과) 같습니다.
12.5. 선택
표준 라이브러리에서 정의된 마지막 공리를 서술하려면, 다음과 같이 정의되는 Nonempty 타입이 필요합니다.
class inductive Nonempty (α : Sort u) : Prop where
| intro (val : α) : Nonempty α
Nonempty α는 타입 Prop을 가지며 그 생성자가 데이터를 포함하므로, Prop으로만 소거될 수 있습니다. 실제로 Nonempty α는 ∃ x : α, True와 동치입니다:
example (α : Type u) : Nonempty α ↔ ∃ x : α, True :=
Iff.intro (fun ⟨a⟩ => ⟨a, trivial⟩) (fun ⟨a, h⟩ => ⟨a⟩)
이제 선택 공리는 다음과 같이 간단하게 표현됩니다:
α가 공집합이 아니라는 주장 h만 주어지면, choice h는 마치 마법처럼 α의 원소 하나를 만들어냅니다. 물론 이는 의미 있는 계산을 모두 가로막습니다. Prop의 해석에 따르면, h에는 그러한 원소를 어떻게 찾을지에 대한 정보가 전혀 담겨 있지 않기 때문입니다.
이는 Classical 네임스페이스에 있으므로, 이 정리의 전체 이름은 Classical.choice입니다. 선택 원리는 비한정 기술의 원리와 동치이며, 이는 서브타입을 사용하여 다음과 같이 표현할 수 있습니다.
noncomputable def indefiniteDescription {α : Sort u}
(p : α → Prop) (h : ∃ x, p x) : {x // p x} :=
choice <| let ⟨x, px⟩ := h; ⟨⟨x, px⟩⟩
choice에 의존하기 때문에, Lean은 indefiniteDescription에 대해 실행 가능한 코드를 생성할 수 없으며, 따라서 이 정의를 noncomputable로 표시하도록 요구합니다. 또한 Classical 네임스페이스에서 함수 choose와 속성 choose_spec은 indefiniteDescription 출력의 두 부분을 분해합니다:
variable {α : Sort u} {p : α → Prop}
noncomputable def choose (h : ∃ x, p x) : α :=
(indefiniteDescription p h).val
theorem choose_spec (h : ∃ x, p x) : p (choose h) :=
(indefiniteDescription p h).property
choice 원리는 Nonempty인 성질과 더 구성적인 성질인 Inhabited의 구분도 없애 버립니다.
open Classical
noncomputable def inhabited_of_nonempty (h : Nonempty α) : Inhabited α :=
choice (let ⟨a⟩ := h; ⟨⟨a⟩⟩)
다음 절에서는 propext, funext, choice를 함께 사용하면 배중률과 모든 명제의 결정 가능성이 따라온다는 것을 살펴보겠습니다. 이를 이용하면 다음과 같이 비한정 기술의 원리를 강화할 수 있습니다.
strongIndefiniteDescription {α : Sort u} (p : α → Prop)
(h : Nonempty α) :
{x // (∃ (y : α), p y) → p x}
주변 타입 α가 공집합이 아니라고 가정하면, strongIndefiniteDescription p는 p를 만족하는 원소가 존재할 경우 α의 원소를 생성합니다. 이 정의의 데이터 구성 요소는 관례적으로 힐베르트 엡실론 함수라고 알려져 있습니다:
epsilon {α : Sort u} [h : Nonempty α] (p : α → Prop) : α
epsilon_spec {α : Sort u} {p : α → Prop}
(hex : ∃ (y : α), p y) :
p (@epsilon _ hex.nonempty p)
12.6. 배중률
배중률은 다음과 같습니다:
Classical.em : ∀ (p : Prop), p ∨ ¬p
Diaconescu의 정리는 선택 공리가 배중률을 도출하기에 충분함을 보여줍니다. 더 정확히 말하면, 배중률이 Classical.choice, propext, funext로부터 따라 나옴을 보여줍니다. 표준 라이브러리에서 찾을 수 있는 증명을 개략적으로 살펴보겠습니다.
먼저 필요한 공리들을 가져오고, 두 술어 U와 V를 정의합니다:
open Classical
theorem em (p : Prop) : p ∨ ¬p := p:Prop⊢ p ∨ ¬p
p:PropU:Prop → Prop := fun x => x = True ∨ p⊢ p ∨ ¬p
p:PropU:Prop → Prop := fun x => x = True ∨ pV:Prop → Prop := fun x => x = False ∨ p⊢ p ∨ ¬p
p:PropU:Prop → Prop := fun x => x = True ∨ pV:Prop → Prop := fun x => x = False ∨ pexU:∃ x, U x⊢ p ∨ ¬p
p:PropU:Prop → Prop := fun x => x = True ∨ pV:Prop → Prop := fun x => x = False ∨ pexU:∃ x, U xexV:∃ x, V x⊢ p ∨ ¬p
p가 참이면, Prop의 모든 원소는 U와 V 둘 다에 속합니다. p가 거짓이면, U는 단일원소 True이고, V는 단일원소 False입니다.
다음으로, choose를 사용하여 U와 V 각각에서 원소를 하나씩 선택합니다:
p:PropU:Prop → Prop := fun x => x = True ∨ pV:Prop → Prop := fun x => x = False ∨ pexU:∃ x, U xexV:∃ x, V xu:Prop := choose exU⊢ p ∨ ¬p
p:PropU:Prop → Prop := fun x => x = True ∨ pV:Prop → Prop := fun x => x = False ∨ pexU:∃ x, U xexV:∃ x, V xu:Prop := choose exUv:Prop := choose exV⊢ p ∨ ¬p
p:PropU:Prop → Prop := fun x => x = True ∨ pV:Prop → Prop := fun x => x = False ∨ pexU:∃ x, U xexV:∃ x, V xu:Prop := choose exUv:Prop := choose exVu_def:U u⊢ p ∨ ¬p
p:PropU:Prop → Prop := fun x => x = True ∨ pV:Prop → Prop := fun x => x = False ∨ pexU:∃ x, U xexV:∃ x, V xu:Prop := choose exUv:Prop := choose exVu_def:U uv_def:V v⊢ p ∨ ¬p
U와 V 각각은 선언지이므로, u_def와 v_def는 네 가지 경우를 나타냅니다. 이 경우들 중 하나에서는 u = True이고 v = False이며, 나머지 모든 경우에서는 p가 참입니다. 따라서 다음과 같습니다:
p:PropU:Prop → Prop := fun x => x = True ∨ pV:Prop → Prop := fun x => x = False ∨ pexU:∃ x, U xexV:∃ x, V xu:Prop := choose exUv:Prop := choose exVu_def:U uv_def:V vnot_uv_or_p:u ≠ v ∨ p⊢ p ∨ ¬p
반면, p가 참이라면, 함수 외연성과 명제적 외연성에 의해 U와 V는 같습니다. u와 v의 정의에 의해, 이는 이들도 같음을 의미합니다.
p:PropU:Prop → Prop := fun x => x = True ∨ pV:Prop → Prop := fun x => x = False ∨ pexU:∃ x, U xexV:∃ x, V xu:Prop := choose exUv:Prop := choose exVu_def:U uv_def:V vnot_uv_or_p:u ≠ v ∨ pp_implies_uv:p → u = v⊢ p ∨ ¬p
이 마지막 두 사실을 결합하면 원하는 결론을 얻습니다:
match not_uv_or_p with
p:PropU:Prop → Prop := fun x => x = True ∨ pV:Prop → Prop := fun x => x = False ∨ pexU:∃ x, U xexV:∃ x, V xu:Prop := choose exUv:Prop := choose exVu_def:U uv_def:V vnot_uv_or_p:u ≠ v ∨ pp_implies_uv:p → u = vhne:u ≠ v⊢ p ∨ ¬p
All goals completed! 🐙
p:PropU:Prop → Prop := fun x => x = True ∨ pV:Prop → Prop := fun x => x = False ∨ pexU:∃ x, U xexV:∃ x, V xu:Prop := choose exUv:Prop := choose exVu_def:U uv_def:V vnot_uv_or_p:u ≠ v ∨ pp_implies_uv:p → u = vh:p⊢ p ∨ ¬p
All goals completed! 🐙
배중률의 귀결에는 이중 부정 제거, 경우에 의한 증명, 귀류법이 있으며, 이들은 모두 고전 논리에 관한 절에서 설명합니다. 배중률과 명제적 확장성은 명제적 완전성을 함의합니다:
open Classical
theorem propComplete (a : Prop) : a = True ∨ a = False :=
match em a with
| Or.inl ha =>
Or.inl (propext (Iff.intro (fun _ => True.intro) (fun _ => ha)))
| Or.inr hn =>
Or.inr (propext (Iff.intro (fun h => hn h) (fun h => False.elim h)))
선택 공리와 함께, 모든 명제가 결정 가능하다는 더 강한 원리도 얻게 됩니다. Decidable 명제의 클래스가 다음과 같이 정의된다는 것을 상기하십시오.
namespace Hidden
class inductive Decidable (p : Prop) where
| isFalse (h : ¬p) : Decidable p
| isTrue (h : p) : Decidable p
end Hidden
Prop으로만 소거될 수 있는 p ∨ ¬ p와 달리, 타입 Decidable p는 임의의 타입으로 소거될 수 있는 합 타입 Sum p (¬ p)와 동치입니다. if-then-else 식을 작성하는 데 필요한 것이 바로 이 데이터입니다.
고전적 추론의 예로, f : α → β가 단사 함수이고 α가 원소를 가진다면 f가 좌측 역함수를 가짐을 보이기 위해 choose를 사용합니다. 좌측 역함수 linv를 정의하기 위해, 의존적인 if-then-else 표현식을 사용합니다. if h : c then t else e는 dite c (fun h : c => t) (fun h : ¬ c => e)의 표기법임을 상기하십시오. linv의 정의에서 선택은 두 번 사용됩니다. 첫 번째로 (∃ a : α, f a = b)가 “판정 가능함”을 보이는 데 사용되고, 두 번째로 f a = b를 만족하는 a를 선택하는 데 사용됩니다. propDecidable은 범위가 지정된 인스턴스이며 open Classical 명령에 의해 활성화됨에 주목하십시오. 우리는 이 인스턴스를 사용하여 if-then-else 표현식을 정당화합니다. (판정 가능한 명제에서의 논의도 참고하십시오.)
open Classical
noncomputable def linv [Inhabited α] (f : α → β) : β → α :=
fun b : β => if ex : (∃ a : α, f a = b) then choose ex else default
theorem linv_comp_self {f : α → β} [Inhabited α]
(inj : ∀ {a b}, f a = f b → a = b)
: linv f ∘ f = id :=
funext fun a =>
have ex : ∃ a₁ : α, f a₁ = f a := ⟨a, rfl⟩
have feq : f (choose ex) = f a := choose_spec ex
calc linv f (f a)
_ = choose ex := rfl
_ = a := inj feq
고전적인 관점에서 linv는 하나의 함수입니다. 구성적인 관점에서는 이것이 받아들여질 수 없습니다. 일반적으로 그러한 함수를 구현할 방법이 없기 때문에, 이 구성은 정보를 담고 있지 않습니다.