2.2. O Quantificador Universal
Para provar ∀ x, P x, considere um elemento arbitrário e prove a proposição nele. A tática intro, que introduziu implicações na Aula 1, também introduz quantificadores universais.
example (α : Type) (P Q : α → Prop)
(h : ∀ x, P x ∧ Q x) : ∀ x, P x := α:TypeP:α → PropQ:α → Proph:∀ (x : α), P x ∧ Q x⊢ ∀ (x : α), P x
α:TypeP:α → PropQ:α → Proph:∀ (x : α), P x ∧ Q xa:α⊢ P a
All goals completed! 🐙
A prova também usa a regra de eliminação. Uma hipótese h : ∀ x, P x ∧ Q x é uma função que retorna uma prova de P a ∧ Q a para cada a, então a aplicação h a a instancia em a. Isso espelha a Aula 1, em que uma prova de uma implicação era uma função sobre provas. A tática specialize instancia uma hipótese universal no próprio contexto.
example (α : Type) (P Q : α → Prop) (h : ∀ x, P x → Q x)
(a : α) (hPa : P a) : Q a := α:TypeP:α → PropQ:α → Proph:∀ (x : α), P x → Q xa:αhPa:P a⊢ Q a
α:TypeP:α → PropQ:α → Propa:αh:P a → Q ahPa:P a⊢ Q a
All goals completed! 🐙
O quantificador universal distribui sobre a conjunção. A prova combina as regras do quantificador com as regras da Aula 1 para a conjunção e o bicondicional.
theorem forall_and_distrib (α : Type) (P Q : α → Prop) :
(∀ x, P x ∧ Q x) ↔ (∀ x, P x) ∧ (∀ x, Q x) := α:TypeP:α → PropQ:α → Prop⊢ (∀ (x : α), P x ∧ Q x) ↔ (∀ (x : α), P x) ∧ ∀ (x : α), Q x
α:TypeP:α → PropQ:α → Prop⊢ (∀ (x : α), P x ∧ Q x) → (∀ (x : α), P x) ∧ ∀ (x : α), Q xα:TypeP:α → PropQ:α → Prop⊢ ((∀ (x : α), P x) ∧ ∀ (x : α), Q x) → ∀ (x : α), P x ∧ Q x
α:TypeP:α → PropQ:α → Prop⊢ (∀ (x : α), P x ∧ Q x) → (∀ (x : α), P x) ∧ ∀ (x : α), Q x α:TypeP:α → PropQ:α → Proph:∀ (x : α), P x ∧ Q x⊢ (∀ (x : α), P x) ∧ ∀ (x : α), Q x
α:TypeP:α → PropQ:α → Proph:∀ (x : α), P x ∧ Q x⊢ ∀ (x : α), P xα:TypeP:α → PropQ:α → Proph:∀ (x : α), P x ∧ Q x⊢ ∀ (x : α), Q x
α:TypeP:α → PropQ:α → Proph:∀ (x : α), P x ∧ Q x⊢ ∀ (x : α), P x α:TypeP:α → PropQ:α → Proph:∀ (x : α), P x ∧ Q xa:α⊢ P a
All goals completed! 🐙
α:TypeP:α → PropQ:α → Proph:∀ (x : α), P x ∧ Q x⊢ ∀ (x : α), Q x α:TypeP:α → PropQ:α → Proph:∀ (x : α), P x ∧ Q xa:α⊢ Q a
All goals completed! 🐙
α: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
All goals completed! 🐙
2.2.1. Exemplos
Os exemplos abaixo combinam as duas regras desta seção com os conectivos da Aula 1.
Exemplo 1. A implicação é reflexiva em cada elemento.
example (α : Type) (P : α → Prop) : ∀ x, P x → P x := α:TypeP:α → Prop⊢ ∀ (x : α), P x → P x
α:TypeP:α → Propa:αhPa:P a⊢ P a
All goals completed! 🐙
Exemplo 2. Uma hipótese universal se instancia em qualquer elemento dado. A aplicação h a já é a prova, então nenhuma tática é necessária.
example (α : Type) (P : α → Prop)
(h : ∀ x, P x) (a : α) : P a := h a
Exemplo 3. Instanciar as duas variáveis de um predicado binário no mesmo elemento produz a diagonal. A tática apply unifica a hipótese com o objetivo e encontra as duas instanciações.
example (α : Type) (R : α → α → Prop)
(h : ∀ x, ∀ y, R x y) : ∀ x, R x x := α:TypeR:α → α → Proph:∀ (x y : α), R x y⊢ ∀ (x : α), R x x
α:TypeR:α → α → Proph:∀ (x y : α), R x ya:α⊢ R a a
All goals completed! 🐙
Exemplo 4. Quantificadores universais consecutivos comutam.
example (α β : Type) (R : α → β → Prop)
(h : ∀ x, ∀ y, R x y) : ∀ y, ∀ x, R x y := α:Typeβ:TypeR:α → β → Proph:∀ (x : α) (y : β), R x y⊢ ∀ (y : β) (x : α), R x y
α:Typeβ:TypeR:α → β → Proph:∀ (x : α) (y : β), R x yb:βa:α⊢ R a b
All goals completed! 🐙
Exemplo 5. A conjunção comuta sob o quantificador. A tática have registra a hipótese instanciada, e constructor divide o objetivo nas duas partes da conjunção.
example (α : Type) (P Q : α → Prop)
(h : ∀ x, P x ∧ Q x) : ∀ x, Q x ∧ P x := α:TypeP:α → PropQ:α → Proph:∀ (x : α), P x ∧ Q x⊢ ∀ (x : α), Q x ∧ P x
α:TypeP:α → PropQ:α → Proph:∀ (x : α), P x ∧ Q xa:α⊢ Q a ∧ P a
α:TypeP:α → PropQ:α → Proph:∀ (x : α), P x ∧ Q xa:αha:P a ∧ Q a⊢ Q a ∧ P a
α:TypeP:α → PropQ:α → Proph:∀ (x : α), P x ∧ Q xa:αha:P a ∧ Q a⊢ Q aα:TypeP:α → PropQ:α → Proph:∀ (x : α), P x ∧ Q xa:αha:P a ∧ Q a⊢ P a
α:TypeP:α → PropQ:α → Proph:∀ (x : α), P x ∧ Q xa:αha:P a ∧ Q a⊢ Q a All goals completed! 🐙
α:TypeP:α → PropQ:α → Proph:∀ (x : α), P x ∧ Q xa:αha:P a ∧ Q a⊢ P a All goals completed! 🐙
Exemplo 6. Um disjunto implica a disjunção em cada elemento. Aplicar Or.inl reduz a disjunção ao seu lado esquerdo.
example (α : Type) (P Q : α → Prop)
(h : ∀ x, P x) : ∀ x, P x ∨ Q x := α:TypeP:α → PropQ:α → Proph:∀ (x : α), P x⊢ ∀ (x : α), P x ∨ Q x
α:TypeP:α → PropQ:α → Proph:∀ (x : α), P xa:α⊢ P a ∨ Q a
α:TypeP:α → PropQ:α → Proph:∀ (x : α), P xa:α⊢ P a
All goals completed! 🐙
Exemplo 7. Uma disjunção pontual cujo lado esquerdo falha em todo elemento produz o seu lado direito.
example (α : Type) (P Q : α → Prop)
(h : ∀ x, P x ∨ Q x) (hn : ∀ x, ¬P x) : ∀ x, Q x := α:TypeP:α → PropQ:α → Proph:∀ (x : α), P x ∨ Q xhn:∀ (x : α), ¬P x⊢ ∀ (x : α), Q x
α:TypeP:α → PropQ:α → Proph:∀ (x : α), P x ∨ Q xhn:∀ (x : α), ¬P xa:α⊢ Q a
cases h a with
α:TypeP:α → PropQ:α → Proph:∀ (x : α), P x ∨ Q xhn:∀ (x : α), ¬P xa:αhPa:P a⊢ Q a All goals completed! 🐙
α:TypeP:α → PropQ:α → Proph:∀ (x : α), P x ∨ Q xhn:∀ (x : α), ¬P xa:αhQa:Q a⊢ Q a All goals completed! 🐙
Exemplo 8. A contraposição se aplica em cada elemento. A prova raciocina para frente, derivando Q a com have antes de chegar à contradição.
example (α : Type) (P Q : α → Prop)
(h : ∀ x, P x → Q x) (hn : ∀ x, ¬Q x) : ∀ x, ¬P x := α:TypeP:α → PropQ:α → Proph:∀ (x : α), P x → Q xhn:∀ (x : α), ¬Q x⊢ ∀ (x : α), ¬P x
α:TypeP:α → PropQ:α → Proph:∀ (x : α), P x → Q xhn:∀ (x : α), ¬Q xa:αhPa:P a⊢ False
α:TypeP:α → PropQ:α → Proph:∀ (x : α), P x → Q xhn:∀ (x : α), ¬Q xa:αhPa:P ahQa:Q a⊢ False
All goals completed! 🐙
Exemplo 9. Um antecedente que não menciona a variável quantificada move-se para dentro do quantificador.
example (α : Type) (P : Prop) (Q : α → Prop)
(h : P → ∀ x, Q x) : ∀ x, P → Q x := α:TypeP:PropQ:α → Proph:P → ∀ (x : α), Q x⊢ ∀ (x : α), P → Q x
α:TypeP:PropQ:α → Proph:P → ∀ (x : α), Q xa:αhP:P⊢ Q a
All goals completed! 🐙
Exemplo 10. Quando o tipo tem um elemento, ∀ x, P x refuta ∀ x, ¬P x.
example (α : Type) (P : α → Prop)
(a : α) (h : ∀ x, P x) : ¬∀ x, ¬P x := α:TypeP:α → Propa:αh:∀ (x : α), P x⊢ ¬∀ (x : α), ¬P x
α:TypeP:α → Propa:αh:∀ (x : α), P xhn:∀ (x : α), ¬P x⊢ False
All goals completed! 🐙