5.1. Provas Progressivas e o Princípio PAT
Uma prova progressiva parte das hipóteses e deriva novos fatos até alcançar o objetivo. A sua frase característica é "de … temos …", o espelho do "basta provar" da Aula 4. Dadas as hipóteses ha : a, hab : a → b, hbc : b → c e o objetivo c, a leitura progressiva constrói b a partir de ha e hab, depois c a partir de b e hbc, exatamente a direção que uma derivação em dedução natural admite quando lida de cima para baixo, a partir das suas suposições.
Uma prova estruturada é um termo cuja forma segue a proposição que ela prova. A prova de um enunciado universalmente quantificado fixa uma variável arbitrária; a prova de uma implicação supõe o seu antecedente; a prova de uma conjunção ou de um existencial se constrói com o construtor anônimo; e os fatos intermediários são nomeados à medida que a prova avança. Lean escreve essas quatro formas como fix, assume, o construtor anônimo ⟨…, …⟩ e have, com show para reafirmar o objetivo atual.
A leitura que unifica o modo de termos e o modo de táticas é o princípio PAT, proposições como tipos e provas como termos.W. A. Howard, "The formulae-as-types notion of construction", in To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, Academic Press, 1980, pp. 479–490. Uma proposição é um tipo, e uma prova dela é um termo desse tipo. Sob essa leitura, uma implicação a → b é ao mesmo tempo um enunciado lógico e o tipo das funções que levam provas de a em provas de b, de modo que a prova de uma implicação é uma função, como a Aula 1 já sugeria. Um enunciado universalmente quantificado ∀ x, P x é um tipo de função dependente, cujo tipo de resultado P x depende do argumento x, e a única seta dos tipos de função dependente dá conta tanto de → quanto de ∀.J. Avigad, L. de Moura, S. Kong, S. Ullrich, Theorem Proving in Lean 4, o capítulo sobre proposições e provas.
Os construtos fix e assume não fazem parte do núcleo de Lean. Eles vêm da biblioteca de apoio LoVe, Lectures/LoVe/LoVelib.lean, que a cadeia de importações destas notas torna disponível, e são analisadores de termos que expandem fix x : τ; e e assume h : P; e nas funções anônimas fun x : τ ↦ e e fun h : P ↦ e. A prova da projeção de três argumentos abaixo mostra a forma estruturada. Ela fixa as duas proposições, supõe as duas hipóteses e afirma o objetivo que devolve.
namespace Forward
theorem fst_of_two_props :
∀ a b : Prop, a → b → a :=
fix a b : Prop;
assume ha : a;
assume hb : b;
show a from ha
end Forward
Como fix e assume são literalmente fun, o mesmo teorema escrito com fun, e a variante que descarta o show final, elaboram para o termo idêntico.
namespace Forward
theorem fst_of_two_props_no_show :
∀ a b : Prop, a → b → a :=
fix a b : Prop;
assume ha : a;
assume hb : b;
ha
theorem fst_of_two_props_fun :
∀ a b : Prop, a → b → a :=
fun a b ha hb => ha
end Forward
Que uma prova é uma função não é uma metáfora, e sim o estado de coisas literal, e #check o torna visível. A prova identidade de a → a é a função identidade, e assume se imprime de volta como o fun que abrevia.
#check (fun (a : Prop) (h : a) => h)
#check (assume h : True; h)