12. 공리와 계산
Lean에 구현된 구성 계산법(Calculus of Constructions) 버전이 의존 함수 타입과 귀납적 타입, 그리고 맨 아래의 비서술적이고 증명 무관한 Prop에서 시작하는 유니버스 계층을 포함한다는 것을 살펴보았습니다. 이 장에서는 추가적인 공리와 규칙으로 CIC를 확장하는 방법을 살펴봅니다. 이런 방식으로 기초 체계를 확장하면 편리할 때가 많습니다. 더 많은 정리를 증명할 수 있게 될 뿐 아니라, 확장하지 않고도 증명할 수 있었던 정리도 더 쉽게 증명할 수 있습니다. 하지만 공리를 추가하면 부정적인 결과가 생길 수 있으며, 그러한 결과는 공리가 올바른지에 대한 우려를 넘어설 수도 있습니다. 특히 공리를 사용하면 정의와 정리의 계산적 내용에 영향을 미치는데, 여기서는 그 방식을 살펴보겠습니다.
Lean은 계산적 추론과 고전적 추론을 모두 지원하도록 설계되었습니다. 원하는 사용자는 “계산적으로 순수한” 부분에만 머무를 수 있으며, 이 부분에서는 시스템의 닫힌 표현식이 표준 정규형으로 평가됨이 보장됩니다. 특히 예를 들어 Nat 타입의 닫힌 계산적으로 순수한 표현식은 어떤 것이든 숫자로 환원됩니다.
Lean의 표준 라이브러리는 추가 공리인 명제 외연성(propositional extensionality)과, 함수 외연성(function extensionality) 원리를 함의하는 몫 구성(quotient construction)을 정의합니다. 이러한 확장은 예를 들어 집합과 유한 집합의 이론을 전개하는 데 사용됩니다. 아래에서 보겠지만, 이러한 정리를 사용하면 Lean 커널에서의 평가가 막힐 수 있으며, 그 결과 Nat 타입의 닫힌 항이 더 이상 숫자로 평가되지 않게 됩니다. 그러나 Lean은 정의를 실행 가능한 코드로 컴파일할 때 타입과 명제 정보를 소거하며, 이 공리들은 새로운 명제만을 추가하므로 그러한 계산적 해석과 양립합니다. 계산을 중시하는 사용자라 하더라도 계산에 대해 추론할 때 고전적인 배중률(law of the excluded middle)을 사용하고 싶을 수 있습니다. 이 역시 커널에서의 평가를 막지만, 컴파일된 코드와는 양립합니다.
표준 라이브러리는 계산적 해석과 완전히 상반되는 선택 원리도 정의합니다. 이 원리는 어떤 것의 존재를 주장하는 명제로부터 마법처럼 “데이터”를 만들어 내기 때문입니다. 이 원리는 일부 고전적 구성에 반드시 필요하며, 사용자는 필요할 때 이를 가져올 수 있습니다. 그러나 이 구성을 사용하여 데이터를 만들어 내는 표현식에는 계산적 내용이 없으며, Lean에서는 이러한 사실을 드러내기 위해 그러한 정의를 noncomputable로 표시해야 합니다.
영리한 기법(디아코네스쿠 정리로 알려져 있습니다)을 사용하면 명제 외연성, 함수 외연성, 선택 공리로부터 배중률을 유도할 수 있습니다. 그러나 앞서 언급했듯이, 배중률을 사용하더라도 데이터를 만들어 내는 데 쓰지 않는 한 여전히 컴파일과 양립할 수 있으며, 다른 고전적 원리들도 마찬가지입니다.
요약하자면, 표준 라이브러리는 유니버스, 의존 함수 타입, 귀납적 타입으로 이루어진 기반 프레임워크 위에 다음 세 가지 구성 요소를 추가로 더합니다.
-
명제 외연성 공리
-
함수 외연성을 함의하는 몫 구성
-
존재 명제로부터 데이터를 만들어 내는 선택 원리
이 중 처음 두 가지는 Lean 내부에서 정규화를 막지만 코드 생성과는 호환되는 반면, 세 번째는 계산적 해석이 불가능합니다. 자세한 내용은 아래에서 더 정확하게 설명하겠습니다.
12.1. 역사적·철학적 배경
수학은 그 역사의 대부분에 걸쳐 본질적으로 계산적인 학문이었습니다. 기하학은 기하학적 대상의 작도를 다루었고, 대수학은 연립방정식의 알고리즘적 해법에 관심을 두었으며, 해석학은 시간에 따라 변화하는 계의 미래 거동을 계산하는 수단을 제공했습니다. “모든 x에 대해, ...를 만족하는 y가 존재한다”는 취지의 정리에 대한 증명으로부터, x가 주어졌을 때 그러한 y를 계산하는 알고리즘을 추출하는 것은 일반적으로 어렵지 않은 일이었습니다.
그러나 19세기에 들어 수학적 논증이 점점 복잡해지자, 수학자들은 알고리즘적 정보를 배제하고, 수학적 대상이 어떻게 표현되는지에 관한 세부 사항을 추상화하여 그 대상을 기술하는 새로운 추론 방식을 개발하게 되었습니다. 그 목표는 계산의 세부 사항에 얽매이지 않고 강력한 “개념적” 이해를 얻는 것이었지만, 그 결과 직접 계산적으로 해석하면 그야말로 거짓인 수학적 정리까지 받아들이게 되었습니다.
오늘날에도 계산이 수학에서 중요하다는 데에는 여전히 상당히 폭넓은 합의가 있습니다. 그러나 계산과 관련된 문제를 어떻게 다루는 것이 가장 좋은지에 대해서는 견해가 다릅니다. 구성적 관점에서 보면, 수학을 그 계산적 뿌리로부터 분리하는 것은 잘못이며, 의미 있는 모든 수학적 정리는 직접적인 계산적 해석을 가져야 합니다. 고전적 관점에서 보면, 관심사를 분리해 두는 편이 더 유익합니다. 즉, 하나의 언어와 방법 체계로 컴퓨터 프로그램을 작성하면서도, 그 프로그램에 대해 추론할 때는 비구성적 이론과 방법을 사용할 자유를 유지할 수 있습니다. 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)” 관점이라고 합니다.
사실 함수 외연성은 다음 절에서 설명할 몫(quotient)의 존재로부터 도출됩니다. 따라서 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관찰적 타입 이론과 큐비컬 타입 이론에 관한 연구를 비롯한 현재의 연구 프로그램들은 함수 외연성, 몫 등이 관련된 캐스트에 대해 축약을 허용하는 방식으로 타입 이론을 확장하는 것을 목표로 합니다. 그러나 그 해법들은 그리 명확하지 않으며, 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는 이 함수가 잘 정의되어 있음을 보여 줍니다. 실제로 아래의 증명에서 분명히 드러나듯이, 계산 원리는 환원 규칙으로 선언되어 있습니다.
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 구성을 진정한 몫(quotient)으로 만들어 주는 것은 다음의 추가 공리입니다:
이것은 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의 핵(kernel)입니다. 공리 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와 r' a b는 동치입니다.
이처럼 흔한 사용 사례를 지원하기 위해 표준 라이브러리는 setoid라는 개념을 정의합니다. 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의 인스턴스는 표기법 Setoid.r 안에 암묵적으로 들어 있습니다. 일반적인 정리 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_respects로 mem_fn이 동치 관계 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입니다. 선택 원리는 비한정 기술(indefinite description) 원리와 동치이며, 이 원리는 부분 타입을 사용하여 다음과 같이 표현할 수 있습니다.
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
디아코네스쿠 정리는 선택 공리만으로 배중률을 유도할 수 있음을 말합니다. 더 정확히 말하면, 이 정리는 배중률이 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 표현식을 작성하는 데 필요한 것이 바로 이 데이터입니다.
고전적 추론의 예로, choose를 사용하여 f : α → β가 단사이고 α가 거주된(inhabited) 타입이면 f가 왼쪽 역함수를 가진다는 것을 보이겠습니다. 왼쪽 역함수 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은 범위 지정(scoped) 인스턴스이며 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는 함수입니다. 구성적인 관점에서 보면 이는 받아들일 수 없습니다. 일반적으로 그러한 함수를 구현할 방법이 없으므로, 이 구성은 아무런 정보도 주지 않습니다.