4.2. Táticas Básicas
As táticas básicas desta aula são intro, apply, exact, assumption, sorry, clear e rename. Elas são básicas porque cada uma realiza uma única transformação elementar do estado da prova e porque nenhuma depende de um conectivo, de um quantificador ou de uma teoria em particular. Quase toda prova por táticas as utiliza.
A tática intro move a variável ligada por ∀ à frente, ou a suposição à frente de uma implicação, da conclusão para o contexto local, sob um nome escolhido. Dado um objetivo demonstrável, ela sempre produz um objetivo demonstrável.
A tática apply casa a conclusão do objetivo com a conclusão de um teorema ou de uma hipótese, a menos de computação, e adiciona os seus argumentos e premissas não resolvidos como novos objetivos. Ela pode transformar um objetivo demonstrável em um indemonstrável. A tática exact fecha o objetivo com um termo que o prova. Quando as duas fecham o objetivo, exact declara a intenção com mais clareza. A tática assumption procura no contexto local uma hipótese que case com a conclusão.
Lean insere os parâmetros escritos à esquerda dos dois-pontos no contexto local do objetivo inicial, então as provas abaixo não precisam de intro.
namespace Backward
theorem fst_of_two_props_params (a b : Prop)
(ha : a) (hb : b) : a := a:Propb:Propha:ahb:b⊢ a
All goals completed! 🐙
theorem fst_of_two_props_exact (a b : Prop)
(ha : a) (hb : b) : a := a:Propb:Propha:ahb:b⊢ a
All goals completed! 🐙
theorem fst_of_two_props_assumption (a b : Prop)
(ha : a) (hb : b) : a := a:Propb:Propha:ahb:b⊢ a
All goals completed! 🐙
end Backward
A tática sorry fecha qualquer objetivo sem prová-lo, exatamente como o termo sorry fez na Aula 3, e Lean marca cada uso. O exemplo abaixo mostra como apply transforma um objetivo demonstrável em um indemonstrável. A conclusão a ∨ b segue da hipótese hb pela regra Or.inr, mas apply Or.inl se compromete com o disjunto esquerdo e deixa o objetivo a, que nenhuma hipótese prova.
example (a b : Prop) (hb : b) : a ∨ b := a:Propb:Prophb:b⊢ a ∨ b
a:Propb:Prophb:b⊢ a
a:Propb:Prophb:b⊢ a
All goals completed! 🐙
Com a regra Or.inr a prova fecha o objetivo.
example (a b : Prop) (hb : b) : a ∨ b := a:Propb:Prophb:b⊢ a ∨ b
a:Propb:Prophb:b⊢ b
All goals completed! 🐙
Duas táticas limpam o contexto local. A tática clear descarta as variáveis ou hipóteses que você nomeia, e Lean apenas verifica que nada mais depende delas, não que a prova ainda se conclui, então clear pode transformar um objetivo demonstrável em um indemonstrável. A tática rename renomeia uma hipótese, selecionada pela sua proposição.
namespace Backward
theorem cleanup_example (a b c : Prop) (ha : a) (hb : b)
(hab : a → b) (hbc : b → c) : c := a:Propb:Propc:Propha:ahb:bhab:a → bhbc:b → c⊢ c
b:Propc:Prophb:bhbc:b → c⊢ c
b:Propc:Prophb:bhbc:b → c⊢ b
b:Prophb:b⊢ b
b:Proph:b⊢ b
All goals completed! 🐙
end Backward
4.2.1. Exemplos
Os exemplos abaixo exercitam intro, apply, exact, assumption, sorry, clear e rename, e distinguem as táticas que preservam a demonstrabilidade das que podem perdê-la.
Example 1. intro em um objetivo com ∀ move a variável ligada para o contexto. O trace mostra o objetivo antes e depois.
example : ∀ n : ℕ, add n 0 = n := ⊢ ∀ (n : ℕ), add n 0 = n
⊢ ∀ (n : ℕ), add n 0 = n
n:ℕ⊢ add n 0 = n
n:ℕ⊢ add n 0 = n
All goals completed! 🐙
Example 2. Um intro com vários nomes abrevia vários intros. Os dois roteiros provam o mesmo teorema.
example : ∀ a b : Prop, a → a := ⊢ ∀ (a b : Prop), a → a
a:Propb:Propha:a⊢ a
All goals completed! 🐙
example : ∀ a b : Prop, a → a := ⊢ ∀ (a b : Prop), a → a
a:Prop⊢ ∀ (b : Prop), a → a
a:Propb:Prop⊢ a → a
a:Propb:Propha:a⊢ a
All goals completed! 🐙
Example 3. Parâmetros à esquerda dos dois-pontos dispensam intro, pois Lean os insere no contexto local do objetivo inicial.
example : ∀ a : Prop, a → a := ⊢ ∀ (a : Prop), a → a
a:Propha:a⊢ a
All goals completed! 🐙
example (a : Prop) (ha : a) : a := a:Propha:a⊢ a
All goals completed! 🐙
Example 4. exact h e apply h fecham o mesmo objetivo, e exact diz mais.
example (a b : Prop) (hab : a → b) (ha : a) : b := a:Propb:Prophab:a → bha:a⊢ b
All goals completed! 🐙
example (a b : Prop) (hab : a → b) (ha : a) : b := a:Propb:Prophab:a → bha:a⊢ b
All goals completed! 🐙
Example 5. assumption fecha o objetivo sem nomear a hipótese.
example (a b c : Prop) (ha : a) (hb : b) (hc : c) : b := a:Propb:Propc:Propha:ahb:bhc:c⊢ b
All goals completed! 🐙
Example 6. Dois applys em sequência aplicam duas implicações regressivamente.
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:a⊢ a
All goals completed! 🐙
Example 7. apply pode perder um objetivo demonstrável. Escolher o disjunto errado deixa uma conclusão que nenhuma hipótese prova, e só sorry o fecha.
example (a b : Prop) (ha : a) : a ∨ b := a:Propb:Propha:a⊢ a ∨ b
a:Propb:Propha:a⊢ b
All goals completed! 🐙
Example 8. sorry fecha qualquer objetivo, e #print axioms relata o uso de sorryAx, como na Aula 3.
namespace Backward
theorem unproved (a : Prop) : a := a:Prop⊢ a
All goals completed! 🐙
end Backward
#print axioms Backward.unproved
Example 9. clear remove uma hipótese e uma variável que a prova não usa.
example (a b : Prop) (ha : a) (hb : b) : b := a:Propb:Propha:ahb:b⊢ b
b:Prophb:b⊢ b
All goals completed! 🐙
Example 10. rename renomeia uma hipótese, selecionada pela sua proposição.
example (a b : Prop) (h : a ∧ b) : a ∧ b := a:Propb:Proph:a ∧ b⊢ a ∧ b
a:Propb:Prophab:a ∧ b⊢ a ∧ b
All goals completed! 🐙