2.3. O Quantificador Existencial
Para provar ∃ x, P x, exiba uma testemunha e prove a proposição nela. O construtor anônimo da Aula 1 emparelha a testemunha com a prova. O termo rfl prova uma equação cujos dois lados computam para o mesmo valor.
example : ∃ n : Nat, n * n = 9 := ⟨3, rfl⟩
A tática exists fornece a testemunha no modo de táticas e fecha o objetivo restante quando ele vale por computação.
example : ∃ n : Nat, n * n = 9 := ⊢ ∃ n, n * n = 9
All goals completed! 🐙
Para usar uma hipótese h : ∃ x, P x, nomeie uma testemunha e a prova de que ela satisfaz P. A proposição ∃ x, P x tem o único construtor intro, então a tática cases a trata como tratou a disjunção na Aula 1, agora com um caso.
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
cases h with
α:TypeP:α → PropQ:α → Propa:αha:P a ∧ Q a⊢ ∃ x, P x All goals completed! 🐙
A tática obtain desestrutura a hipótese em um passo, com um padrão que espelha o construtor anônimo.
example (α : Type) (P Q : α → Prop)
(h : ∃ x, P x ∧ Q x) : ∃ x, Q x := α:TypeP:α → PropQ:α → Proph:∃ x, P x ∧ Q x⊢ ∃ x, Q x
α:TypeP:α → PropQ:α → Propa:αha:P a ∧ Q a⊢ ∃ x, Q x
All goals completed! 🐙
O teorema abaixo combina os dois quantificadores. Uma implicação ponto a ponto transporta a existência de P para Q, e a testemunha não muda.
theorem exists_imp_exists (α : Type) (P Q : α → Prop)
(h : ∀ 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 xhex:∃ x, P x⊢ ∃ x, Q x
α:TypeP:α → PropQ:α → Proph:∀ (x : α), P x → Q xa:αhPa:P a⊢ ∃ x, Q x
All goals completed! 🐙