5.4. Provas Calculacionais
Uma prova calculacional dispõe uma cadeia de igualdades para o leitor, um passo por linha, cada passo justificado por uma reescrita ou por um lema. A palavra-chave calc compõe os passos em uma única derivação transitiva, fazendo o papel de Eq.trans para que quem escreve não precise fazê-lo. Cada passo é exatamente o tipo de igualdade que rw consome, e um passo que vale apenas a menos de associatividade e comutatividade é fechado pelo ac_rfl da Aula 4. A disposição se lê como um matemático escreve, com o termo corrente à esquerda e a justificativa à direita.
namespace Forward
theorem two_mul_example (m n : ℕ) :
2 * m + n = m + n + m := m:ℕn:ℕ⊢ 2 * m + n = m + n + m
calc 2 * m + n = (m + m) + n := m:ℕn:ℕ⊢ 2 * m + n = m + m + n All goals completed! 🐙
_ = m + n + m := m:ℕn:ℕ⊢ m + m + n = m + n + m All goals completed! 🐙
end Forward
O mesmo argumento escrito com passos have aninhados e Eq.trans mostra o que calc abrevia. A cadeia de duas igualdades vira dois fatos nomeados unidos por transitividade.
namespace Forward
theorem two_mul_example_have (m n : ℕ) :
2 * m + n = m + n + m := m:ℕn:ℕ⊢ 2 * m + n = m + n + m
m:ℕn:ℕh1:2 * m + n = m + m + n⊢ 2 * m + n = m + n + m
m:ℕn:ℕh1:2 * m + n = m + m + nh2:m + m + n = m + n + m⊢ 2 * m + n = m + n + m
All goals completed! 🐙
end Forward
calc também encadeia qualquer relação transitiva, não só a igualdade, e os exemplos incluem uma cadeia sobre ↔ fechada por Iff.trans.
5.4.1. Exemplos
Os exemplos abaixo constroem cadeias calculacionais, justificam os seus passos por reescritas e por lemas, e comparam calc com as alternativas que ele abrevia.
Example 1. Uma cadeia de dois passos sobre ℕ, cada passo fechado por rfl.
namespace Forward
example : (1 : ℕ) + 1 + 1 = 3 := ⊢ 1 + 1 + 1 = 3
calc (1 : ℕ) + 1 + 1 = 2 + 1 := rfl
_ = 3 := rfl
end Forward
Example 2. A mesma identidade por Eq.trans, que expõe o que a cadeia abrevia.
namespace Forward
example : (1 : ℕ) + 1 + 1 = 3 :=
Eq.trans
(rfl : (1 : ℕ) + 1 + 1 = 2 + 1)
(rfl : (2 : ℕ) + 1 = 3)
end Forward
Example 3. Um único passo justificado por reescrita com a comutatividade.
namespace Forward
example (a b : ℕ) : a + b = b + a := a:ℕb:ℕ⊢ a + b = b + a
calc a + b = b + a := a:ℕb:ℕ⊢ a + b = b + a All goals completed! 🐙
end Forward
Example 4. Um passo justificado por um lema nomeado da Aula 4, a associatividade do nosso add.
namespace Forward
example (l m n : ℕ) :
add (add l m) n = add l (add m n) := l:ℕm:ℕn:ℕ⊢ add (add l m) n = add l (add m n)
calc add (add l m) n
= add l (add m n) := Backward.add_assoc l m n
end Forward
Example 5. Uma cadeia que mistura um passo rw com um passo ac_rfl, a identidade completa da duplicação.
namespace Forward
example (m n : ℕ) : 2 * m + n = m + n + m := m:ℕn:ℕ⊢ 2 * m + n = m + n + m
calc 2 * m + n = (m + m) + n := m:ℕn:ℕ⊢ 2 * m + n = m + m + n All goals completed! 🐙
_ = m + n + m := m:ℕn:ℕ⊢ m + m + n = m + n + m All goals completed! 🐙
end Forward
Example 6. Uma cadeia cujo último passo é ac_rfl e cujo primeiro é um rfl.
namespace Forward
example (a b c : ℕ) : a + b + c = c + (a + b) := a:ℕb:ℕc:ℕ⊢ a + b + c = c + (a + b)
calc a + b + c = (a + b) + c := rfl
_ = c + (a + b) := a:ℕb:ℕc:ℕ⊢ a + b + c = c + (a + b) All goals completed! 🐙
end Forward
Example 7. Uma cadeia de três igualdades construída a partir de duas hipóteses.
namespace Forward
example (a b c d : ℕ) (h1 : a = b) (h2 : b = c)
(h3 : c = d) : a = d := a:ℕb:ℕc:ℕd:ℕh1:a = bh2:b = ch3:c = d⊢ a = d
calc a = b := h1
_ = c := h2
_ = d := h3
end Forward
Example 8. calc encadeia dois bicondicionais com Iff.trans exatamente como encadeia igualdades.
namespace Forward
example (a b c : Prop) (h1 : a ↔ b) (h2 : b ↔ c) :
a ↔ c := a:Propb:Propc:Proph1:a ↔ bh2:b ↔ c⊢ a ↔ c
calc a ↔ b := h1
_ ↔ c := h2
end Forward
Example 9. O mesmo objetivo por uma cadeia explícita e por um único simp, o que mostra quando a cadeia justifica o seu comprimento.
namespace Forward
example (a b : ℕ) : (a + b) * 1 = a + b := a:ℕb:ℕ⊢ (a + b) * 1 = a + b
calc (a + b) * 1 = a + b := a:ℕb:ℕ⊢ (a + b) * 1 = a + b All goals completed! 🐙
example (a b : ℕ) : (a + b) * 1 = a + b := a:ℕb:ℕ⊢ (a + b) * 1 = a + b
All goals completed! 🐙
end Forward
Example 10. Um passo que se lê da direita para a esquerda, justificado por uma reescrita com a igualdade invertida.
namespace Forward
example (a b : ℕ) (h : a = b) : b = a := a:ℕb:ℕh:a = b⊢ b = a
calc b = a := a:ℕb:ℕh:a = b⊢ b = a All goals completed! 🐙
end Forward