5.5. Raciocínio Progressivo com Táticas
As provas reais entrelaçam as duas direções. No modo de táticas, have h : P := pf e have h : P := by … acrescentam um fato provado ao contexto, e let x := t acrescenta uma abreviação, ambos trabalhando de forma progressiva enquanto a prova ao redor trabalha de forma regressiva. A tática specialize da Aula 2 e a eliminação obtain ⟨…⟩ := h são outros passos progressivos. A composição de implicações, provada de forma progressiva como termo mais cedo nesta aula, se lê no estilo misto como um único have progressivo dentro de uma prova regressiva.
namespace Forward
theorem prop_comp_tactical (a b c : Prop)
(hab : a → b) (hbc : b → c) : a → c := a:Propb:Propc:Prophab:a → bhbc:b → c⊢ a → c
a:Propb:Propc:Prophab:a → bhbc:b → cha:a⊢ c
a:Propb:Propc:Prophab:a → bhbc:b → cha:ahb:b⊢ c
All goals completed! 🐙
end Forward
O have progressivo constrói b a partir de ha e hab, e o exact regressivo fecha o objetivo com hbc aplicado a ele. A prova mista costuma ser a mais curta, porque toma cada fato de onde é mais fácil alcançá-lo.
5.5.1. Exemplos
Os exemplos abaixo acrescentam fatos com have, abreviam com let, instanciam com specialize, eliminam com obtain e misturam as duas direções.
Example 1. Um have progressivo constrói o fato intermediário, e um exact regressivo fecha o objetivo.
namespace Forward
example (a b c : Prop) (hab : a → b) (hbc : b → c)
(ha : a) : c := a:Propb:Propc:Prophab:a → bhbc:b → cha:a⊢ c
a:Propb:Propc:Prophab:a → bhbc:b → cha:ahb:b⊢ c
All goals completed! 🐙
end Forward
Example 2. O mesmo teorema escrito de forma puramente regressiva, para contraste.
namespace Forward
example (a b c : Prop) (hab : a → b) (hbc : b → c)
(ha : a) : c := a:Propb:Propc:Prophab:a → bhbc:b → cha:a⊢ c
All goals completed! 🐙
end Forward
Example 3. have … := by … prova o fato intermediário por um bloco de táticas próprio.
namespace Forward
example (a b : Prop) (hab : a → b) (ha : a) : b := a:Propb:Prophab:a → bha:a⊢ b
a:Propb:Prophab:a → bha:ahb:b⊢ b
All goals completed! 🐙
end Forward
Example 4. let x := t abrevia um termo, e show reafirma o objetivo em termos da abreviação.
namespace Forward
example (n : ℕ) : n + n = n + n := n:ℕ⊢ n + n = n + n
n:ℕm:ℕ := n + n⊢ n + n = n + n
n:ℕm:ℕ := n + n⊢ m = m
All goals completed! 🐙
end Forward
Example 5. specialize instancia uma hipótese universal de forma progressiva, recordando a Aula 2.
namespace Forward
example (P : ℕ → Prop) (h : ∀ n, P n) : P 7 := P:ℕ → Proph:∀ (n : ℕ), P n⊢ P 7
P:ℕ → Proph:P 7⊢ P 7
All goals completed! 🐙
end Forward
Example 6. Um have progressivo faz um simp posterior ter sucesso.
namespace Forward
example (f : ℕ → ℕ) (a : ℕ) (h : f a = 0) :
f a + 1 = 1 := f:ℕ → ℕa:ℕh:f a = 0⊢ f a + 1 = 1
f:ℕ → ℕa:ℕh:f a = 0hf:f a = 0⊢ f a + 1 = 1
All goals completed! 🐙
end Forward
Example 7. obtain ⟨a, ha⟩ := h elimina uma hipótese existencial de forma progressiva, nomeando a sua testemunha.
namespace Forward
example (α : Type) (P : α → Prop) (Q : Prop)
(hex : ∃ x, P x) (h : ∀ x, P x → Q) : Q := α:TypeP:α → PropQ:Prophex:∃ x, P xh:∀ (x : α), P x → Q⊢ Q
α:TypeP:α → PropQ:Proph:∀ (x : α), P x → Qa:αha:P a⊢ Q
All goals completed! 🐙
end Forward
Example 8. Dois passos have encadeados, o segundo usando o primeiro.
namespace Forward
example (a b c : Prop) (hab : a → b) (hbc : b → c)
(ha : a) : c := a:Propb:Propc:Prophab:a → bhbc:b → cha:a⊢ c
a:Propb:Propc:Prophab:a → bhbc:b → cha:ahb:b⊢ c
a:Propb:Propc:Prophab:a → bhbc:b → cha:ahb:bhc:c⊢ c
All goals completed! 🐙
end Forward
Example 9. Uma prova que mistura um apply regressivo com um have progressivo.
namespace Forward
example (a b c : Prop) (hab : a → b) (hbc : b → c)
(ha : a) : c := a:Propb:Propc:Prophab:a → bhbc:b → cha:a⊢ c
a:Propb:Propc:Prophab:a → bhbc:b → cha:a⊢ b
a:Propb:Propc:Prophab:a → bhbc:b → cha:ahb:b⊢ b
All goals completed! 🐙
end Forward
Example 10. O mesmo teorema apenas regressivo e misto, para que o misto mostre a sua economia.
namespace Forward
example (a b : Prop) (hab : a → b) (ha : a) : b := a:Propb:Prophab:a → bha:a⊢ b
a:Propb:Prophab:a → bha:a⊢ a
All goals completed! 🐙
example (a b : Prop) (hab : a → b) (ha : a) : b := a:Propb:Prophab:a → bha:a⊢ b
All goals completed! 🐙
end Forward