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 α. Nesse cenário tipado, a coleção de todos os conjuntos que não contêm a si mesmos não pode ser escrita, então o paradoxo de Russell não surge.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 instância abaixo registra a notação x ∈ s, que se desdobra por definição na aplicação s x. Nesta instância e nas seguintes, Lean liga a variável de tipo livre α automaticamente.
instance : Membership α (Set α) :=
⟨fun s a => s a⟩
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 tal conjunto por compreensão, como o conjunto de todos os n tais que ∃ 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⟩
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⟩
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 tal igualdade requer princípios de extensionalidade além da lógica apresentada até aqui, então enunciamos identidades de conjuntos como inclusões.