4.7. Exemplos Trabalhados
Cada exemplo abaixo é realizado por completo e verbalizado, como o guia faz. Eles são disjuntos dos exercícios, e Lean verifica cada linha quando as notas são construídas.
4.7.1. Distribuir uma conjunção sobre uma disjunção
O enunciado a ∧ (b ∨ c) → (a ∧ b) ∨ (a ∧ c) usa apenas intro, apply, exact e marcadores. A regra de eliminação de ∨ conduz a prova, e a justaposição a instancia com o conjunto direito da hipótese.
namespace Backward
theorem and_or_distrib (a b c : Prop) :
a ∧ (b ∨ c) → (a ∧ b) ∨ (a ∧ c) := a:Propb:Propc:Prop⊢ a ∧ (b ∨ c) → a ∧ b ∨ a ∧ c
a:Propb:Propc:Prophabc:a ∧ (b ∨ c)⊢ a ∧ b ∨ a ∧ c
a:Propb:Propc:Prophabc:a ∧ (b ∨ c)⊢ b → a ∧ b ∨ a ∧ ca:Propb:Propc:Prophabc:a ∧ (b ∨ c)⊢ c → a ∧ b ∨ a ∧ c
a:Propb:Propc:Prophabc:a ∧ (b ∨ c)⊢ b → a ∧ b ∨ a ∧ c a:Propb:Propc:Prophabc:a ∧ (b ∨ c)hb:b⊢ a ∧ b ∨ a ∧ c
a:Propb:Propc:Prophabc:a ∧ (b ∨ c)hb:b⊢ a ∧ b
a:Propb:Propc:Prophabc:a ∧ (b ∨ c)hb:b⊢ aa:Propb:Propc:Prophabc:a ∧ (b ∨ c)hb:b⊢ b
a:Propb:Propc:Prophabc:a ∧ (b ∨ c)hb:b⊢ a All goals completed! 🐙
a:Propb:Propc:Prophabc:a ∧ (b ∨ c)hb:b⊢ b All goals completed! 🐙
a:Propb:Propc:Prophabc:a ∧ (b ∨ c)⊢ c → a ∧ b ∨ a ∧ c a:Propb:Propc:Prophabc:a ∧ (b ∨ c)hc:c⊢ a ∧ b ∨ a ∧ c
a:Propb:Propc:Prophabc:a ∧ (b ∨ c)hc:c⊢ a ∧ c
a:Propb:Propc:Prophabc:a ∧ (b ∨ c)hc:c⊢ aa:Propb:Propc:Prophabc:a ∧ (b ∨ c)hc:c⊢ c
a:Propb:Propc:Prophabc:a ∧ (b ∨ c)hc:c⊢ a All goals completed! 🐙
a:Propb:Propc:Prophabc:a ∧ (b ∨ c)hc:c⊢ c All goals completed! 🐙
end Backward
Em palavras. Suponha a ∧ (b ∨ c). O seu conjunto direito é uma disjunção, e basta provar a conclusão a partir de cada disjunto. Se b vale, basta provar o disjunto esquerdo a ∧ b, cujas partes são o conjunto esquerdo da hipótese e o próprio b. Se c vale, o disjunto direito a ∧ c segue do mesmo modo. Cada marcador fecha um ramo, e a prova se lê exatamente como a sua contraparte de papel e caneta.
4.7.2. Um objetivo indemonstrável e um retrocesso
A disjunção do enunciado a ∧ b → a ∨ c admite duas regras de introdução, e apenas uma conduz a uma prova. Or.inl e Or.inr podem transformar um objetivo demonstrável em um indemonstrável. A primeira tentativa se compromete com o disjunto direito, e o trace mostra uma conclusão c que nenhuma hipótese prova, então só sorry fecha o bloco.
example (a b c : Prop) : a ∧ b → a ∨ c := a:Propb:Propc:Prop⊢ a ∧ b → a ∨ c
a:Propb:Propc:Prophab:a ∧ b⊢ a ∨ c
a:Propb:Propc:Prophab:a ∧ b⊢ c
a:Propb:Propc:Prophab:a ∧ b⊢ c
All goals completed! 🐙
O remédio é lembrar o ponto de escolha e retroceder. A segunda tentativa se compromete com o disjunto esquerdo, e o conjunto esquerdo da hipótese o fecha.
namespace Backward
theorem and_imp_or (a b c : Prop) : a ∧ b → a ∨ c := a:Propb:Propc:Prop⊢ a ∧ b → a ∨ c
a:Propb:Propc:Prophab:a ∧ b⊢ a ∨ c
a:Propb:Propc:Prophab:a ∧ b⊢ a
All goals completed! 🐙
end Backward
4.7.3. rw versus simp
Dados f e a equação hf : ∀ x, f x = x + 1, qualquer das duas táticas prova a conclusão f (f 0) = 2, de modos diferentes. rw [hf] reescreve as ocorrências do primeiro subtermo que casa, aqui a aplicação externa, e precisa de uma segunda invocação para a interna, após a qual o rfl que ela tenta fecha o objetivo. simp [hf] reescreve exaustivamente e precisa de uma invocação.
example (f : ℕ → ℕ) (hf : ∀ x, f x = x + 1) :
f (f 0) = 2 := f:ℕ → ℕhf:∀ (x : ℕ), f x = x + 1⊢ f (f 0) = 2
All goals completed! 🐙
example (f : ℕ → ℕ) (hf : ∀ x, f x = x + 1) :
f (f 0) = 2 := f:ℕ → ℕhf:∀ (x : ℕ), f x = x + 1⊢ f (f 0) = 2
All goals completed! 🐙
O objetivo residual torna concreto o "primeiro subtermo que casa". Um rw [hf] reescreve a aplicação externa e deixa a interna no lugar.
example (f : ℕ → ℕ) (hf : ∀ x, f x = x + 1) :
f (f 0) = 2 := f:ℕ → ℕhf:∀ (x : ℕ), f x = x + 1⊢ f (f 0) = 2
f:ℕ → ℕhf:∀ (x : ℕ), f x = x + 1⊢ f 0 + 1 = 2
f:ℕ → ℕhf:∀ (x : ℕ), f x = x + 1⊢ f 0 + 1 = 2
All goals completed! 🐙
4.7.4. Descarregar reverse_cons
O último exemplo trabalhado da Aula 3 enunciou reverse (x :: xs) = snoc (reverse xs) x e o deixou com sorry. Desdobrar reverse transforma o lado esquerdo em appendPretty (reverse xs) [x], então o enunciado mistura appendPretty e snoc, e a peça que falta é o teorema que os relaciona. Esta é a dica do guia em ação: um caso difícil costuma sinalizar um teorema auxiliar que falta.
namespace Backward
theorem append_snoc {α : Type} (ys : List α) (x : α) :
appendPretty ys [x] = snoc ys x := α:Typeys:List αx:α⊢ appendPretty ys [x] = snoc ys x
induction ys with
α:Typex:α⊢ appendPretty [] [x] = snoc [] x All goals completed! 🐙
α:Typex:αy:αys':List αih:appendPretty ys' [x] = snoc ys' x⊢ appendPretty (y :: ys') [x] = snoc (y :: ys') x All goals completed! 🐙
theorem reverse_cons {α : Type} (x : α) (xs : List α) :
reverse (x :: xs) = snoc (reverse xs) x := α:Typex:αxs:List α⊢ reverse (x :: xs) = snoc (reverse xs) x
All goals completed! 🐙
end Backward
O teorema auxiliar induz sobre a lista que a recursão de appendPretty consome, e o teorema principal fica então a um simp de distância, usando as equações que definem reverse e o teorema auxiliar como regras de reescrita.