2.7. Exemplos Resolvidos
Cada exemplo abaixo aparece de duas formas, como um termo de prova e como uma prova por táticas. As duas apresentam a mesma prova, e Lean verifica os dois scripts na construção das notas. As regras dos quantificadores seguem a mesma disciplina de introdução e eliminação dos conectivos da Aula 1, então omitimos as árvores de derivação e deixamos os termos espelhá-las. Estas proposições são disjuntas dos exemplos das seções anteriores e dos exercícios.
2.7.1. Contraposição sob quantificadores
A testemunha da falha de Q também testemunha a falha de P, pois a implicação naquele elemento leva uma prova de P a a uma prova de Q a. O padrão em intro destrói o existencial.
example (α : Type) (P Q : α → Prop)
(h : ∀ x, P x → Q x) : (∃ x, ¬Q x) → ∃ x, ¬P x :=
fun ⟨a, hnQa⟩ => ⟨a, fun hPa => hnQa (h a hPa)⟩
example (α : Type) (P Q : α → Prop)
(h : ∀ x, P x → Q x) : (∃ x, ¬Q x) → ∃ x, ¬P x := α:TypeP:α → PropQ:α → Proph:∀ (x : α), P x → Q x⊢ (∃ x, ¬Q x) → ∃ x, ¬P x
α:TypeP:α → PropQ:α → Proph:∀ (x : α), P x → Q xa:αhnQa:¬Q a⊢ ∃ x, ¬P x
α:TypeP:α → PropQ:α → Proph:∀ (x : α), P x → Q xa:αhnQa:¬Q a⊢ ¬P a
α:TypeP:α → PropQ:α → Proph:∀ (x : α), P x → Q xa:αhnQa:¬Q ahPa:P a⊢ False
All goals completed! 🐙
2.7.2. Uma disjunção de universais
Qualquer que seja o lado que valha, a sua instância em cada elemento prova a disjunção ponto a ponto. O termo elimina a disjunção com .elim, e a prova por táticas com cases.
example (α : Type) (P Q : α → Prop) :
(∀ x, P x) ∨ (∀ x, Q x) → ∀ x, P x ∨ Q x :=
fun h a =>
h.elim (fun hp => Or.inl (hp a))
(fun hq => Or.inr (hq a))
example (α : Type) (P Q : α → Prop) :
(∀ x, P x) ∨ (∀ x, Q x) → ∀ x, P x ∨ Q x := α:TypeP:α → PropQ:α → Prop⊢ ((∀ (x : α), P x) ∨ ∀ (x : α), Q x) → ∀ (x : α), P x ∨ Q x
α:TypeP:α → PropQ:α → Proph:(∀ (x : α), P x) ∨ ∀ (x : α), Q xa:α⊢ P a ∨ Q a
cases h with
α:TypeP:α → PropQ:α → Propa:αhp:∀ (x : α), P x⊢ P a ∨ Q a All goals completed! 🐙
α:TypeP:α → PropQ:α → Propa:αhq:∀ (x : α), Q x⊢ P a ∨ Q a All goals completed! 🐙
2.7.3. A interseção preserva a inclusão
A inclusão aplica-se à parte esquerda da pertinência, e a parte direita passa sem mudança.
example (α : Type) (s t u : Set α)
(h : s ⊆ t) : s ∩ u ⊆ t ∩ u :=
fun x hx => ⟨h x hx.left, hx.right⟩
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
α:Types:Set αt:Set αu:Set αh:s ⊆ tx:αhx:x ∈ s ∩ u⊢ x ∈ tα:Types:Set αt:Set αu:Set αh:s ⊆ tx:αhx:x ∈ s ∩ u⊢ x ∈ u
α:Types:Set αt:Set αu:Set αh:s ⊆ tx:αhx:x ∈ s ∩ u⊢ x ∈ t All goals completed! 🐙
α:Types:Set αt:Set αu:Set αh:s ⊆ tx:αhx:x ∈ s ∩ u⊢ x ∈ u All goals completed! 🐙
2.7.4. Existência clássica
O teorema not_forall_exists da seção de leis de negação produz uma testemunha onde ¬P falha, e Classical.byContradiction remove a dupla negação, como na Aula 1.
example (α : Type) (P : α → Prop)
(h : ¬∀ x, ¬P x) : ∃ x, P x :=
(not_forall_exists α (fun x => ¬P x) h).elim
fun a hnnPa => ⟨a, Classical.byContradiction hnnPa⟩
example (α : Type) (P : α → Prop)
(h : ¬∀ x, ¬P x) : ∃ x, P x := α:TypeP:α → Proph:¬∀ (x : α), ¬P x⊢ ∃ x, P x
α:TypeP:α → Proph:¬∀ (x : α), ¬P xa:αhnnPa:¬¬P a⊢ ∃ x, P x
All goals completed! 🐙