4.5. Táticas de Reescrita
A tática rw aplica uma equação como regra de reescrita da esquerda para a direita, uma vez. Ela encontra o primeiro subtermo que casa com o lado esquerdo, instancia as variáveis da equação de acordo, substitui toda ocorrência daquele subtermo instanciado e então tenta rfl. Um ← à frente usa a equação da direita para a esquerda, at h reescreve a hipótese h em vez da conclusão, e at * reescreve em toda parte. Dado o nome de uma constante em vez de uma equação, rw usa as equações que definem a constante, e é assim que rw [Not] expande uma negação e rw [add] desdobra o nosso add.
namespace Backward
theorem Eq_trans_symm_rw {α : Type} (a b c : α)
(hab : a = b) (hcb : c = b) : a = c := α:Typea:αb:αc:αhab:a = bhcb:c = b⊢ a = c
α:Typea:αb:αc:αhab:a = bhcb:c = b⊢ b = c
All goals completed! 🐙
theorem a_proof_of_negation (a : Prop) : a → ¬¬ a := a:Prop⊢ a → ¬¬a
a:Prop⊢ a → ¬a → False
a:Prop⊢ a → (a → False) → False
a:Propha:ahna:a → False⊢ False
a:Propha:ahna:a → False⊢ a
All goals completed! 🐙
end Backward
A tática simp aplica um conjunto padrão de regras de reescrita, o conjunto simp, exaustivamente. A sintaxe simp [t₁, …, tₙ] adiciona teoremas ou constantes por uma invocação, simp [-t] remove um, simp [*] at * usa cada hipótese sobre cada hipótese e sobre a conclusão, e o atributo @[simp] registra um teorema permanentemente.
namespace Backward
theorem cong_two_args_1p1 {α : Type} (a b c d : α)
(g : α → α → ℕ → α) (hab : a = b) (hcd : c = d) :
g a c (1 + 1) = g b d 2 := α:Typea:αb:αc:αd:αg:α → α → ℕ → αhab:a = bhcd:c = d⊢ g a c (1 + 1) = g b d 2
All goals completed! 🐙
end Backward
A reescrita é onde as provas deixam de ser previsíveis. O conselho do guia é tentar uma tática, estudar os subobjetivos que surgem e ajustar, em vez de planejar cada passo de antemão. Nas palavras do próprio guia, NÃO ENTRE EM PÂNICO.
4.5.1. Exemplos
Os exemplos abaixo reescrevem na conclusão e nas hipóteses, nas duas direções, e comparam rw com simp sobre o mesmo objetivo.
Example 1. rw [h] reescreve a conclusão da esquerda para a direita e o fecha com o rfl que tenta ao final.
example (f : ℕ → ℕ) (a b : ℕ) (h : a = b) :
f a = f b := f:ℕ → ℕa:ℕb:ℕh:a = b⊢ f a = f b
All goals completed! 🐙
Example 2. rw [←h] usa a mesma equação da direita para a esquerda.
example (f : ℕ → ℕ) (a b : ℕ) (h : a = b) :
f b = f a := f:ℕ → ℕa:ℕb:ℕh:a = b⊢ f b = f a
All goals completed! 🐙
Example 3. rw [h₁, h₂] aplica duas equações, uma após a outra.
example (a b c : ℕ) (h₁ : a = b) (h₂ : b = c) :
a = c := a:ℕb:ℕc:ℕh₁:a = bh₂:b = c⊢ a = c
All goals completed! 🐙
Example 4. rw [h₂] at h₁ reescreve a hipótese, e a hipótese reescrita fecha o objetivo.
example (a b c : ℕ) (h₁ : a = b) (h₂ : b = c) :
a = c := a:ℕb:ℕc:ℕh₁:a = bh₂:b = c⊢ a = c
a:ℕb:ℕc:ℕh₁:a = ch₂:b = c⊢ a = c
All goals completed! 🐙
Example 5. rw fecha o objetivo sozinho quando os dois lados coincidem, porque tenta rfl depois de reescrever.
example (a b : ℕ) (h : a = b) : a = b := a:ℕb:ℕh:a = b⊢ a = b
All goals completed! 🐙
Example 6. rw [add] desdobra uma equação que define o nosso add.
example (m n : ℕ) :
add m (Nat.succ n) = Nat.succ (add m n) := m:ℕn:ℕ⊢ add m n.succ = (add m n).succ
All goals completed! 🐙
Example 7. rw [Not] at h expande a negação em uma hipótese, que então se aplica como implicação.
example (a : Prop) (h : ¬a) : a → False := a:Proph:¬a⊢ a → False
a:Proph:a → False⊢ a → False
All goals completed! 🐙
Example 8. simp sozinho fecha um objetivo aritmético a partir do conjunto simp padrão.
example (n : ℕ) : n + 0 + 0 = n := n:ℕ⊢ n + 0 + 0 = n
All goals completed! 🐙
Example 9. simp [h] reescreve toda ocorrência, enquanto rw [h] reescreve apenas as ocorrências do primeiro subtermo que casa. O primeiro roteiro precisa de duas reescritas, uma por instância do padrão, e o segundo precisa de um simp.
example (f : ℕ → ℕ) (hf : ∀ x, f x = 0) :
f 1 + f 2 = 0 := f:ℕ → ℕhf:∀ (x : ℕ), f x = 0⊢ f 1 + f 2 = 0
f:ℕ → ℕhf:∀ (x : ℕ), f x = 0⊢ 0 + f 2 = 0
All goals completed! 🐙
example (f : ℕ → ℕ) (hf : ∀ x, f x = 0) :
f 1 + f 2 = 0 := f:ℕ → ℕhf:∀ (x : ℕ), f x = 0⊢ f 1 + f 2 = 0
All goals completed! 🐙
Example 10. simp [*] at * usa cada hipótese em toda parte e fecha um objetivo a partir de duas hipóteses encadeadas.
example (a b c : ℕ) (h₁ : a = b) (h₂ : b = c) :
a = c := a:ℕb:ℕc:ℕh₁:a = bh₂:b = c⊢ a = c
All goals completed! 🐙