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! 🐙