4.1. Provas Regressivas🔗

Uma tática opera sobre um objetivo de prova e o prova ou cria novos subobjetivos. Um objetivo consiste em um contexto local, que lista declarações de variáveis x : σ e hipóteses h : P, e uma conclusão, a proposição por provar. Escrevemos o objetivo como o sequente C ⊢ Q, cujo antecedente C é o contexto local e cujo consequente Q é a conclusão.J. Avigad, L. de Moura, S. Kong, S. Ullrich, Theorem Proving in Lean 4, capítulo 5.

Táticas são um mecanismo de prova regressivo. Uma prova regressiva parte do objetivo e trabalha em direção às hipóteses e aos teoremas disponíveis, e a sua frase característica é "basta provar". Uma prova progressiva parte das hipóteses e trabalha em direção ao objetivo, e a Aula 5 a desenvolve. Dadas as hipóteses ha : a, hab : a → b, hbc : b → c e a conclusão c, as duas direções se leem assim.

Regressiva, a partir do objetivo:
  para provar c, por hbc basta provar b;
  para provar b, por hab basta provar a;
  e ha prova a.

Progressiva, a partir das hipóteses:
  de ha e hab, temos b;
  de b e hbc, temos c.

Uma derivação na dedução natural da Aula 1 se escreve empilhando aplicações de regras, com as premissas de cada regra acima do traço de inferência e a sua conclusão abaixo dele. As fórmulas do topo, que nenhuma regra deriva, são as suposições e os axiomas, e a fórmula final, embaixo, é a conclusão da derivação. A derivação admite as duas leituras, progressiva das suposições para a conclusão e regressiva da conclusão para as suposições.G. Gentzen, Investigations into Logical Deduction, in M. E. Szabo (ed.), The Collected Papers of Gerhard Gentzen, North-Holland, 1969, pp. 68–131.

A palavra-chave by entra no modo de táticas, e cada linha depois dela é uma tática. A prova abaixo introduz as variáveis universalmente quantificadas e as duas hipóteses, e fecha o objetivo. As linhas trace_state imprimem o objetivo entre os passos, e as saídas seguem o código.

Depois de intro a b, as duas proposições entraram no contexto, e a conclusão é a implicação que resta.

a b:Prop⊢ a → b → a

Depois de intro ha hb, as duas hipóteses estão disponíveis, e a conclusão é a.

a b:Propha:ahb:b⊢ a

A prova abaixo encadeia duas implicações. Leia-a como três passos de "basta provar": para provar c, por hbc basta provar b; para provar b, por hab basta provar a; e ha prova a.