2.6. Conjuntos
O capítulo 3 de HTPIwL desenvolve provas sobre conjuntos. Um conjunto de elementos de um tipo α é determinado por quais elementos pertencem a ele, então o predicado de pertinência determina o conjunto. Em Lean, tomamos essa propriedade como a definição.
def Set (α : Type) : Type := α → Prop
Todo elemento de um conjunto vem do tipo fixo α, e essa disciplina de tipos bloqueia o paradoxo de Russell.B. Russell, carta a Frege, 16 de junho de 1902. Em J. van Heijenoort, From Frege to Gödel: A Source Book in Mathematical Logic, 1879–1931, Harvard University Press, 1967, pp. 124–125. A teoria ingênua de conjuntos admite um conjunto para cada propriedade. Tome R como o conjunto de todos os conjuntos que não são elementos de si mesmos. Então R ∈ R vale exatamente quando R ∉ R, o que é uma contradição, e a teoria colapsa. Em Lean, um conjunto s : Set α contém apenas elementos de α, e o próprio s tem tipo Set α, não α, então a expressão s ∈ s não é bem tipada. Não há como enunciar a propriedade que define R nem formar a coleção, então o paradoxo não ocorre.
Nada até aqui dá ao símbolo ∈ um significado nos nossos conjuntos, e Lean não traz um embutido. Uma classe de tipos declara uma operação e a deixa sem significado, e uma declaração instance fornece o significado em um tipo. A notação x ∈ s chega aos nossos conjuntos em três passos, e cada passo mora em um lugar diferente.
O símbolo é notação comum, declarada no módulo do núcleo Init.Notation. Ele abrevia uma aplicação, e nada mais.
notation:50 a:50 " ∈ " b:50 => Membership.mem b a
O nome Membership.mem à direita é o único campo de uma classe declarada no módulo do núcleo Init.Prelude. A classe fixa a forma da operação, tomando o tipo dos elementos e o tipo do recipiente, e não dá definição alguma.
class Membership (α : outParam (Type u)) (γ : Type v) where mem : γ → α → Prop
O recipiente vem primeiro em mem e vem depois na notação, então x ∈ s abrevia Membership.mem s x.
O terceiro passo é nosso. Quando Lean elabora x ∈ s, ele procura entre as instâncias registradas uma cujo tipo de recipiente case com o tipo de s. Set α é uma definição desta aula, então essa busca nada encontra e a notação não elabora. A instância abaixo encerra a busca e dá a mem a sua definição em Set α. Nesta instância e nas seguintes, Lean liga a variável de tipo livre α automaticamente.
instance : Membership α (Set α) :=
⟨fun s a => s a⟩
Imprimir uma pertinência com a notação desligada mostra os dois passos de uma vez, a expansão do símbolo e a instância que o elaborador encontrou.
set_option pp.notation false in
#check fun (α : Type) (s : Set α) (x : α) => x ∈ s
Com a instância em escopo, x ∈ s é a aplicação s x por definição, então as duas são intercambiáveis e rfl prova que são iguais.
example (α : Type) (s : Set α) (x : α) :
(x ∈ s) = s x := rfl
Os três passos repartem-se entre dois dos componentes da Figura 1.1. O expansor de macros faz o primeiro, trocando o símbolo pela aplicação, e o elaborador faz o terceiro, escolhendo a instância a partir do tipo de s.
Um conjunto dado por uma propriedade é o próprio predicado, e uma prova de pertinência é uma prova da propriedade. A notação matemática escreve esse conjunto por compreensão, como o conjunto de todos os n que satisfazem ∃ k, n = 2 * k. O núcleo de Lean não tem notação por compreensão, então escrevemos o predicado diretamente.
def Evens : Set Nat := fun n => ∃ k, n = 2 * k
example : (6 : Nat) ∈ Evens := ⟨3, rfl⟩
A inclusão s ⊆ t afirma que todo elemento de s pertence a t.
instance : HasSubset (Set α) :=
⟨fun s t => ∀ x, x ∈ s → x ∈ t⟩
A notação desdobra-se na sua definição. Uma hipótese h : s ⊆ t aplica-se a um elemento e a uma prova de pertinência.
example (α : Type) (s t : Set α) (h : s ⊆ t)
(x : α) (hx : x ∈ s) : x ∈ t := h x hx
Uma inclusão é uma implicação universalmente quantificada, então as suas provas começam considerando um elemento arbitrário junto com a suposição de que ele pertence ao lado esquerdo. A união e a interseção aplicam os conectivos da Aula 1 ponto a ponto.
instance : Union (Set α) :=
⟨fun s t => fun x => x ∈ s ∨ x ∈ t⟩
instance : Inter (Set α) :=
⟨fun s t => fun x => x ∈ s ∧ x ∈ t⟩
As duas notações desdobram-se do mesmo modo, então os termos de prova da Aula 1 constroem e usam pertinências diretamente.
example (α : Type) (s t : Set α) (x : α)
(hx : x ∈ s) : x ∈ s ∪ t := Or.inl hx
example (α : Type) (s t : Set α) (x : α)
(hx : x ∈ s ∩ t) : x ∈ t := hx.right
A pertinência a uma interseção é por definição uma conjunção, então as projeções da Aula 1 se aplicam a ela.
theorem inter_subset_left (α : Type) (s t : Set α) :
s ∩ t ⊆ s := α:Types:Set αt:Set α⊢ s ∩ t ⊆ s
α:Types:Set αt:Set αx:αhx:x ∈ s ∩ t⊢ x ∈ s
All goals completed! 🐙
A pertinência a uma união é uma disjunção, então a tática cases a divide.
theorem union_subset_swap (α : Type) (s t : Set α) :
s ∪ t ⊆ t ∪ s := α:Types:Set αt:Set α⊢ s ∪ t ⊆ t ∪ s
α:Types:Set αt:Set αx:αhx:x ∈ s ∪ t⊢ x ∈ t ∪ s
cases hx with
α:Types:Set αt:Set αx:αh:x ∈ s⊢ x ∈ t ∪ s All goals completed! 🐙
α:Types:Set αt:Set αx:αh:x ∈ t⊢ x ∈ t ∪ s All goals completed! 🐙
Dois conjuntos com os mesmos elementos são iguais. Provar essa igualdade requer princípios de extensionalidade além da lógica apresentada até aqui, então enunciamos identidades de conjuntos como inclusões.
2.6.1. Exemplos
Os exemplos abaixo provam pertinências e inclusões diretamente a partir das definições. Cada prova de inclusão começa introduzindo um elemento e a sua hipótese de pertinência, e as notações desdobram-se nos conectivos e quantificadores das seções anteriores.
Exemplo 1. Um conjunto dado por um predicado contém um elemento exatamente quando o predicado vale nele. A testemunha 3 prova que 9 é um quadrado.
def Squares : Set Nat := fun n => ∃ k, n = k * k
example : (9 : Nat) ∈ Squares := ⟨3, rfl⟩
Exemplo 2. A inclusão é reflexiva. A prova introduz um elemento e a sua hipótese de pertinência e devolve a hipótese sem mudança.
example (α : Type) (s : Set α) : s ⊆ s := α:Types:Set α⊢ s ⊆ s
α:Types:Set αx:αhx:x ∈ s⊢ x ∈ s
All goals completed! 🐙
Exemplo 3. A união contém o seu lado esquerdo. A pertinência à união é uma disjunção, e Or.inl escolhe o lado esquerdo.
example (α : Type) (s t : Set α) : s ⊆ s ∪ t := α:Types:Set αt:Set α⊢ s ⊆ s ∪ t
α:Types:Set αt:Set αx:αhx:x ∈ s⊢ x ∈ s ∪ t
All goals completed! 🐙
Exemplo 4. A interseção comuta como inclusão. A pertinência à interseção é uma conjunção, e o construtor anônimo troca as suas partes.
example (α : Type) (s t : Set α) : s ∩ t ⊆ t ∩ s := α:Types:Set αt:Set α⊢ s ∩ t ⊆ t ∩ s
α:Types:Set αt:Set αx:αhx:x ∈ s ∩ t⊢ x ∈ t ∩ s
All goals completed! 🐙
Exemplo 5. A união contém a interseção.
example (α : Type) (s t : Set α) : s ∩ t ⊆ s ∪ t := α:Types:Set αt:Set α⊢ s ∩ t ⊆ s ∪ t
α:Types:Set αt:Set αx:αhx:x ∈ s ∩ t⊢ x ∈ s ∪ t
All goals completed! 🐙
Exemplo 6. Quando t e u contêm s, a sua interseção contém s.
example (α : Type) (s t u : Set α)
(h1 : s ⊆ t) (h2 : s ⊆ u) : s ⊆ t ∩ u := α:Types:Set αt:Set αu:Set αh1:s ⊆ th2:s ⊆ u⊢ s ⊆ t ∩ u
α:Types:Set αt:Set αu:Set αh1:s ⊆ th2:s ⊆ ux:αhx:x ∈ s⊢ x ∈ t ∩ u
All goals completed! 🐙
Exemplo 7. Quando u contém os dois lados de uma união, u contém a união. A tática cases divide a disjunção.
example (α : Type) (s t u : Set α)
(h1 : s ⊆ u) (h2 : t ⊆ u) : s ∪ t ⊆ u := α:Types:Set αt:Set αu:Set αh1:s ⊆ uh2:t ⊆ u⊢ s ∪ t ⊆ u
α:Types:Set αt:Set αu:Set αh1:s ⊆ uh2:t ⊆ ux:αhx:x ∈ s ∪ t⊢ x ∈ u
cases hx with
α:Types:Set αt:Set αu:Set αh1:s ⊆ uh2:t ⊆ ux:αhs:x ∈ s⊢ x ∈ u All goals completed! 🐙
α:Types:Set αt:Set αu:Set αh1:s ⊆ uh2:t ⊆ ux:αht:x ∈ t⊢ x ∈ u All goals completed! 🐙
Exemplo 8. A união com um conjunto fixo preserva a inclusão.
example (α : Type) (s t u : Set α)
(h : s ⊆ t) : s ∪ u ⊆ t ∪ u := α:Types:Set αt:Set αu:Set αh:s ⊆ t⊢ s ∪ u ⊆ t ∪ u
α:Types:Set αt:Set αu:Set αh:s ⊆ tx:αhx:x ∈ s ∪ u⊢ x ∈ t ∪ u
cases hx with
α:Types:Set αt:Set αu:Set αh:s ⊆ tx:αhs:x ∈ s⊢ x ∈ t ∪ u All goals completed! 🐙
α:Types:Set αt:Set αu:Set αh:s ⊆ tx:αhu:x ∈ u⊢ x ∈ t ∪ u All goals completed! 🐙
Exemplo 9. O conjunto vazio, cujo predicado de pertinência é False em cada elemento, é subconjunto de todo conjunto. False.elim fecha o objetivo.
def EmptySet (α : Type) : Set α := fun _ => False
example (α : Type) (s : Set α) : EmptySet α ⊆ s := α:Types:Set α⊢ EmptySet α ⊆ s
α:Types:Set αx:αhx:x ∈ EmptySet α⊢ x ∈ s
All goals completed! 🐙
Exemplo 10. Todo conjunto é subconjunto do conjunto universo, cujo predicado de pertinência é True em cada elemento.
def UnivSet (α : Type) : Set α := fun _ => True
example (α : Type) (s : Set α) : s ⊆ UnivSet α := α:Types:Set α⊢ s ⊆ UnivSet α
α:Types:Set αx:α_hx:x ∈ s⊢ x ∈ UnivSet α
All goals completed! 🐙