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 := by⊢ ∃ n, n * n = 9
  exists 3All 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 := byα:TypeP:α → PropQ:α → Proph:∃ x, P x ∧ Q x⊢ ∃ x, P x
  cases h with
  | intro a ha =>introα:TypeP:α → PropQ:α → Propa:αha:P a ∧ Q a⊢ ∃ x, P x exact ⟨a, ha.left⟩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 := byα:TypeP:α → PropQ:α → Proph:∃ x, P x ∧ Q x⊢ ∃ x, Q x
  obtain ⟨a, ha⟩ := hα:TypeP:α → PropQ:α → Propa:αha:P a ∧ Q a⊢ ∃ x, Q x
  exact ⟨a, ha.right⟩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 := byα:TypeP:α → PropQ:α → Proph:∀ (x : α), P x → Q x⊢ (∃ x, P x) → ∃ x, Q x
  intro hexα:TypeP:α → PropQ:α → Proph:∀ (x : α), P x → Q xhex:∃ x, P x⊢ ∃ x, Q x
  obtain ⟨a, hPa⟩ := hexα:TypeP:α → PropQ:α → Proph:∀ (x : α), P x → Q xa:αhPa:P a⊢ ∃ x, Q x
  exact ⟨a, h a hPa⟩All goals completed! 🐙

2.3.1. Exemplos🔗

Os exemplos abaixo combinam a regra da testemunha e a eliminação do existencial com os conectivos da Aula 1.

Exemplo 1. A testemunha 7 prova um existencial concreto por computação.

example : ∃ n : Nat, n + 5 = 12 := ⟨7, rfl⟩

Exemplo 2. Tanto 0 quanto 1 satisfazem n * n = n, e a prova escolhe a testemunha 1.

example : ∃ n : Nat, n * n = n := by⊢ ∃ n, n * n = n
  exists 1All goals completed! 🐙

Exemplo 3. Um elemento junto com uma prova nele é a regra de introdução empacotada como um par.

example (α : Type) (P : α → Prop)
    (a : α) (hPa : P a) : ∃ x, P x := ⟨a, hPa⟩

Exemplo 4. Em um tipo habitado, uma afirmação universal produz uma existencial. A tática specialize instancia a hipótese, e exists a encontra como hipótese do contexto.

example (α : Type) (P : α → Prop)
    (a : α) (h : ∀ x, P x) : ∃ x, P x := byα:TypeP:α → Propa:αh:∀ (x : α), P x⊢ ∃ x, P x
  specialize h aα:TypeP:α → Propa:αh:P a⊢ ∃ x, P x
  exists aAll goals completed! 🐙

Exemplo 5. Uma proposição que não menciona a variável ligada escapa do quantificador.

example (α : Type) (P : Prop) (h : ∃ _ : α, P) : P := byα:TypeP:Proph:∃ x, P⊢ P
  obtain ⟨_, hP⟩ := hα:TypeP:Propw✝:αhP:P⊢ P
  exact hPAll goals completed! 🐙

Exemplo 6. A conjunção comuta sob o quantificador.

example (α : Type) (P Q : α → Prop)
    (h : ∃ x, P x ∧ Q x) : ∃ x, Q x ∧ P x := byα:TypeP:α → PropQ:α → Proph:∃ x, P x ∧ Q x⊢ ∃ x, Q x ∧ P x
  cases h with
  | intro a ha =>introα:TypeP:α → PropQ:α → Propa:αha:P a ∧ Q a⊢ ∃ x, Q x ∧ P x exact ⟨a, ha.right, ha.left⟩All goals completed! 🐙

Exemplo 7. Um existencial de uma conjunção se divide, e as duas partes compartilham a testemunha. O padrão do obtain desestrutura a conjunção sob o quantificador em um só passo.

example (α : Type) (P Q : α → Prop)
    (h : ∃ x, P x ∧ Q x) : (∃ x, P x) ∧ (∃ x, Q x) := byα:TypeP:α → PropQ:α → Proph:∃ x, P x ∧ Q x⊢ (∃ x, P x) ∧ ∃ x, Q x
  obtain ⟨a, hPa, hQa⟩ := hα:TypeP:α → PropQ:α → Propa:αhPa:P ahQa:Q a⊢ (∃ x, P x) ∧ ∃ x, Q x
  constructorleftα:TypeP:α → PropQ:α → Propa:αhPa:P ahQa:Q a⊢ ∃ x, P xrightα:TypeP:α → PropQ:α → Propa:αhPa:P ahQa:Q a⊢ ∃ x, Q x
  ·leftα:TypeP:α → PropQ:α → Propa:αhPa:P ahQa:Q a⊢ ∃ x, P x exact ⟨a, hPa⟩All goals completed! 🐙
  ·rightα:TypeP:α → PropQ:α → Propa:αhPa:P ahQa:Q a⊢ ∃ x, Q x exact ⟨a, hQa⟩All goals completed! 🐙

Exemplo 8. A testemunha de P x também testemunha Q x → P x.

example (α : Type) (P Q : α → Prop)
    (h : ∃ x, P x) : ∃ x, Q x → P x := byα:TypeP:α → PropQ:α → Proph:∃ x, P x⊢ ∃ x, Q x → P x
  obtain ⟨a, hPa⟩ := hα:TypeP:α → PropQ:α → Propa:αhPa:P a⊢ ∃ x, Q x → P x
  exists aα:TypeP:α → PropQ:α → Propa:αhPa:P a⊢ Q a → P a
  intro _hQα:TypeP:α → PropQ:α → Propa:αhPa:P a_hQ:Q a⊢ P a
  exact hPaAll goals completed! 🐙

Exemplo 9. Quantificadores existenciais consecutivos comutam.

example (α β : Type) (R : α → β → Prop)
    (h : ∃ x, ∃ y, R x y) : ∃ y, ∃ x, R x y := byα:Typeβ:TypeR:α → β → Proph:∃ x y, R x y⊢ ∃ y x, R x y
  obtain ⟨a, b, hab⟩ := hα:Typeβ:TypeR:α → β → Propa:αb:βhab:R a b⊢ ∃ y x, R x y
  exact ⟨b, a, hab⟩All goals completed! 🐙

Exemplo 10. Uma disjunção existencial cujo lado direito falha em todo elemento testemunha o seu lado esquerdo.

example (α : Type) (P Q : α → Prop)
    (h : ∃ x, P x ∨ Q x) (hn : ∀ x, ¬Q x) : ∃ x, P x := byα:TypeP:α → PropQ:α → Proph:∃ x, P x ∨ Q xhn:∀ (x : α), ¬Q x⊢ ∃ x, P x
  obtain ⟨a, ha⟩ := hα:TypeP:α → PropQ:α → Prophn:∀ (x : α), ¬Q xa:αha:P a ∨ Q a⊢ ∃ x, P x
  cases ha with
  | inl hPa =>inlα:TypeP:α → PropQ:α → Prophn:∀ (x : α), ¬Q xa:αhPa:P a⊢ ∃ x, P x exact ⟨a, hPa⟩All goals completed! 🐙
  | inr hQa =>inrα:TypeP:α → PropQ:α → Prophn:∀ (x : α), ¬Q xa:αhQa:Q a⊢ ∃ x, P x exact absurd hQa (hn a)All goals completed! 🐙