5.3. Raciocínio Progressivo sobre Conectivos e Quantificadores
A Aula 4 aplicou as regras dos conectivos de forma regressiva com apply. De forma progressiva, as mesmas regras se usam por justaposição, fornecendo a hipótese diretamente. Uma regra de eliminação desmonta uma hipótese, e uma regra de introdução constrói o objetivo. Assim, And.left h e And.right h extraem as duas conjunções, And.intro ha hb e o construtor anônimo ⟨ha, hb⟩ constroem uma conjunção, Or.inl e Or.inr constroem uma disjunção, Or.elim h f g a consome com dois ramos funcionais, Iff.mp e Iff.mpr aplicam uma equivalência em cada direção, Exists.intro t pf fornece uma testemunha, e Exists.elim h f nomeia a testemunha de uma hipótese existencial. Cada um é um passo progressivo, e uma prova estruturada os encadeia com have.
A comutatividade da conjunção, provada de forma regressiva na Aula 4, se lê de forma progressiva como três passos have.
namespace Forward
theorem And_swap (a b : Prop) : a ∧ b → b ∧ a :=
assume h : a ∧ b;
have ha : a := And.left h;
have hb : b := And.right h;
show b ∧ a from And.intro hb ha
end Forward
A comutatividade da disjunção consome a hipótese com Or.elim e a reconstrói do outro lado. modus_ponens e Not_Not_intro combinam os passos vistos até aqui, lembrando que ¬ a é a → False.
namespace Forward
theorem Or_swap (a b : Prop) : a ∨ b → b ∨ a :=
assume h : a ∨ b;
Or.elim h
(fun ha => Or.inr ha)
(fun hb => Or.inl hb)
theorem modus_ponens (a b : Prop) :
(a → b) → a → b :=
assume hab : a → b;
assume ha : a;
show b from hab ha
theorem Not_Not_intro (a : Prop) : a → ¬¬ a :=
assume ha : a;
assume hna : ¬ a;
show False from hna ha
end Forward
O ponto alto da seção é o par de regras do ponto único, que colapsam um quantificador cuja variável ligada é presa a um valor fixo por uma igualdade. A regra para ∀ diz que uma implicação universalmente quantificada guardada por x = t é equivalente à sua instância em t; a regra para ∃ é o seu espelho existencial. Cada prova é estruturada, e cada uma é mais natural de forma progressiva do que regressiva.
namespace Forward
theorem Forall_one_point (α : Type) (t : α)
(P : α → Prop) :
(∀ x, x = t → P x) ↔ P t :=
Iff.intro
(assume h : ∀ x, x = t → P x; h t rfl)
(assume hpt : P t;
fix x : α; assume hxt : x = t; hxt ▸ hpt)
theorem Exists_one_point (α : Type) (t : α)
(P : α → Prop) :
(∃ x, x = t ∧ P x) ↔ P t :=
Iff.intro
(assume h : ∃ x, x = t ∧ P x;
Exists.elim h (fun x hx => hx.1 ▸ hx.2))
(assume hpt : P t;
Exists.intro t (And.intro rfl hpt))
end Forward
Na direção progressiva da regra para ∀, a hipótese é instanciada em t e a guarda t = t é descarregada por rfl. Na direção regressiva, um x arbitrário é fixado, a guarda x = t é suposta, e a igualdade reescreve P t em P x pelo operador de substituição ▸. A regra para ∃ fornece a testemunha t de um lado e nomeia a testemunha do outro.
5.3.1. Exemplos
Os exemplos abaixo aplicam cada regra de forma progressiva por justaposição, depois provam as duas regras do ponto único.
Example 1. And.left e And.right extraem as duas conjunções de forma progressiva.
namespace Forward
example (a b : Prop) (h : a ∧ b) : a :=
And.left h
example (a b : Prop) (h : a ∧ b) : b :=
And.right h
end Forward
Example 2. And.intro e o construtor anônimo constroem uma conjunção, e os dois termos são o mesmo.
namespace Forward
example (a b : Prop) (ha : a) (hb : b) : a ∧ b :=
And.intro ha hb
example (a b : Prop) (ha : a) (hb : b) : a ∧ b :=
⟨ha, hb⟩
end Forward
Example 3. A comutatividade da conjunção de forma progressiva, ao lado do seu roteiro regressivo da Aula 4.
namespace Forward
example (a b : Prop) : a ∧ b → b ∧ a :=
assume h : a ∧ b;
And.intro (And.right h) (And.left h)
example (a b : Prop) : a ∧ b → b ∧ a := a:Propb:Prop⊢ a ∧ b → b ∧ a
a:Propb:Proph:a ∧ b⊢ b ∧ a
a:Propb:Proph:a ∧ b⊢ ba:Propb:Proph:a ∧ b⊢ a
a:Propb:Proph:a ∧ b⊢ b All goals completed! 🐙
a:Propb:Proph:a ∧ b⊢ a All goals completed! 🐙
end Forward
Example 4. Or.inl e Or.inr constroem uma disjunção escolhendo um lado.
namespace Forward
example (a b : Prop) (ha : a) : a ∨ b :=
Or.inl ha
example (a b : Prop) (hb : b) : a ∨ b :=
Or.inr hb
end Forward
Example 5. Or.elim h f g consome uma disjunção com dois ramos funcionais.
namespace Forward
example (a b c : Prop) (h : a ∨ b) (f : a → c)
(g : b → c) : c :=
Or.elim h f g
end Forward
Example 6. Iff.mp e Iff.mpr aplicam uma equivalência em cada direção por justaposição.
namespace Forward
example (a b : Prop) (h : a ↔ b) (ha : a) : b :=
Iff.mp h ha
example (a b : Prop) (h : a ↔ b) (hb : b) : a :=
Iff.mpr h hb
end Forward
Example 7. Exists.intro t pf fornece uma testemunha de forma progressiva, e o construtor anônimo é o mesmo termo.
namespace Forward
example (P : ℕ → Prop) (h : P 3) : ∃ n, P n :=
Exists.intro 3 h
example (P : ℕ → Prop) (h : P 3) : ∃ n, P n :=
⟨3, h⟩
end Forward
Example 8. Exists.elim h f nomeia a testemunha de uma hipótese existencial em um ramo funcional.
namespace Forward
example (α : Type) (P : α → Prop) (Q : Prop)
(h : ∃ x, P x) (f : ∀ x, P x → Q) : Q :=
Exists.elim h f
end Forward
Example 9. A regra do ponto único para ∀ de forma progressiva, instanciando em t de um lado e reescrevendo com a guarda do outro.
namespace Forward
example (α : Type) (t : α) (P : α → Prop) :
(∀ x, x = t → P x) ↔ P t :=
Iff.intro
(assume h : ∀ x, x = t → P x; h t rfl)
(assume hpt : P t;
fix x : α; assume hxt : x = t; hxt ▸ hpt)
end Forward
Example 10. A regra do ponto único para ∃ de forma progressiva, contrastando a testemunha fornecida de um lado com a testemunha nomeada do outro.
namespace Forward
example (α : Type) (t : α) (P : α → Prop) :
(∃ x, x = t ∧ P x) ↔ P t :=
Iff.intro
(assume h : ∃ x, x = t ∧ P x;
Exists.elim h (fun x hx => hx.1 ▸ hx.2))
(assume hpt : P t;
Exists.intro t (And.intro rfl hpt))
end Forward