5.7. Exemplos Resolvidos
Cada exemplo abaixo inverte um artefato da Aula 4 para o estilo progressivo e estruturado, de modo que as duas aulas se leiam como um único argumento visto de ambos os extremos. Lean verifica cada linha quando as notas são compiladas.
5.7.1. A lei distributiva, progressivamente
O enunciado a ∧ (b ∨ c) → (a ∧ b) ∨ (a ∧ c) foi o primeiro exemplo resolvido da Aula 4, provado de forma regressiva. De forma progressiva ele se lê como um termo estruturado. Da hipótese temos a e temos b ∨ c; de b ∨ c obtemos dois casos; em cada um construímos a disjunção correspondente com o construtor anônimo.
namespace Forward
theorem and_or_distrib (a b c : Prop) :
a ∧ (b ∨ c) → (a ∧ b) ∨ (a ∧ c) :=
assume habc : a ∧ (b ∨ c);
have ha : a := And.left habc;
Or.elim (And.right habc)
(fun hb => Or.inl (And.intro ha hb))
(fun hc => Or.inr (And.intro ha hc))
end Forward
Em palavras. Suponha a ∧ (b ∨ c), e nomeie a sua conjunção esquerda ha. A sua conjunção direita é uma disjunção, então raciocinamos por casos. Se b vale, a disjunção esquerda a ∧ b segue de ha e b. Se c vale, a disjunção direita a ∧ c segue de ha e c. A prova regressiva da Aula 4 aplicou Or.elim para dividir o objetivo e fechou cada ramo com marcadores; a prova progressiva consome a mesma disjunção com Or.elim e devolve a disjunção construída diretamente. O compromisso é o de sempre, o roteiro regressivo planejando a partir do objetivo e o termo progressivo construindo a partir das hipóteses.
5.7.2. Forall_one_point por extenso
A regra do ponto único (∀ x, x = t → P x) ↔ P t é o ápice da seção de conectivos, e é uma prova de quantificador que é natural de forma progressiva e desajeitada de forma regressiva.
namespace Forward
theorem Forall_one_point_worked (α : 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
A direção progressiva instancia a hipótese h no valor fixo t e descarrega a guarda t = t com rfl, de modo que h t rfl prova P t. A direção regressiva fixa um x arbitrário, supõe a guarda x = t, e reescreve P t em P x com a substituição hxt ▸ hpt, onde hxt : x = t carrega a igualdade. De forma regressiva a mesma prova deixaria uma metavariável para a testemunha e uma igualdade desajeitada por descarregar; de forma progressiva a testemunha é simplesmente t.
5.7.3. Uma prova calculacional
A identidade 2 * m + n = m + n + m tem três provas, e compará-las revela a moral do estilo calculacional.
namespace Forward
theorem two_mul_example_calc (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! 🐙
theorem two_mul_example_trans (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! 🐙
theorem two_mul_example_ac (m n : ℕ) :
2 * m + n = m + n + m := m:ℕn:ℕ⊢ 2 * m + n = m + n + m
m:ℕn:ℕ⊢ m + m + n = m + n + m
All goals completed! 🐙
end Forward
A prova por calc documenta a cadeia que o leitor segue. A prova por Eq.trans mostra a transitividade que calc esconde. A prova por ac_rfl esconde a cadeia por completo e deixa o verificador rearranjar os termos. As três estão corretas e se apoiam nos mesmos fatos; a escolha é sobre o leitor, não sobre o verificador.
5.7.4. reverse_reverse por recursão
Reverter uma lista duas vezes devolve a lista, e a prova recorre sobre a lista, usando o reverse_append provado acima como sua auxiliar. Isto fecha o ciclo com o quarto exemplo resolvido da Aula 4, que descarregou reverse_cons.
namespace Forward
theorem reverse_reverse {α : Type} :
∀ (xs : List α), reverse (reverse xs) = xs
| [] => rfl
α:Typex:αxs:List α⊢ reverse (reverse (x :: xs)) = x :: xs α:Typex:αxs:List α⊢ reverse (reverse (x :: xs)) = x :: xs
All goals completed! 🐙
end Forward
O caso base reverte a lista vazia duas vezes e fecha por rfl. No caso do passo, reverter x :: xs dá appendPretty (reverse xs) [x], e reverter isso, por reverse_append, traz a cabeça de volta à frente e deixa reverse (reverse xs), que a chamada recursiva, a hipótese de indução, reescreve para xs. A tática induction da Aula 4 provaria o mesmo enunciado com ih no lugar da chamada recursiva; as duas são a mesma prova. As semanas 6 e 7 dão o método geral para tipos indutivos arbitrários.