3.1.1. O tipo Prop e Provas🔗

O que diferencia Lean de outras linguagens como Python ou Java, é a capacidade de usarmos a mesma linguagem para programar funções e escrever provas sobre estas funções.

Uma proposição é um enunciado que pode ser verdadeiro ou falso. O enunciado 1 = 1 é verdadeiro, enquanto square₁ 12 = 2 é falso. Toda proposição é um tipo em Prop  (Yingchareonthawornchai, 2025)Sorrachai Yingchareonthawornchai (2025). “Formalizing Analysis of Algorithms, Autumn 2025”. Manuscrito não publicado. .. Podemos declarar proposições, mas não podemos avaliar uma proposição. Note que perguntar pelo tipo não é o mesmo que decidir se ela é verdadeira.

Em Lean, proposições são tipos e provas são termos desses tipos. Ou seja, provar algo é exatamente o mesmo ato de construir um valor em Prop. Por isso a forma mais direta de provar é escrever o termo à mão, do mesmo jeito que definimos qualquer função. Provar 1 = 1 é exibir um termo de tipo 1 = 1, exatamente o que o construtor refl do tipo Eq faz abaixo. Este tipo representa a relação de igualdade. Podemos notar que declarar um teorema é muito parecido com declarar uma função, como vimos em IntroL.

Acontece que, para propriedades um pouco menos triviais, o termo para provar uma proposição pode ficar grande e pouco natural de escrever manualmente. É aí que entra a palavra by. Ela introduz um modo chamado 'tactic mode' onde usamos uma pequena linguagem de comandos (táticas) em que descrevemos como a prova deve ser montada e deixamos o Lean construir o termo por nós.

A tática rfl prova igualdades quando os dois lados são iguais por definição, isto é, quando Lean consegue reduzi-los até a mesma expressão por computação. Essa redução inclui, por exemplo, a expansão de definições, a aplicação de funções e a avaliação de let. Isso é uma consequência importante da fundação de Lean em Calculus of Inductive Constructions (CIC)  (Nederpelt and Geuvers, 2014)Rob Nederpelt and Herman Geuvers (2014). “Type Theory and Formal Proof: An Introduction”. Cambridge University Press, Cambridge. .: expressões de tipos e programas podem ser computadas e comparadas por redução. Assim, rfl é frequentemente usado para dizer que os dois lados são iguais porque são o mesmo valor depois de reduzir o código. O comando #print double_theorem irá mostrar que a tática rfl construiu o termo Eq.refl.

A tática rfl só funciona quando os dois lados são idênticos por definição. Para propriedades que exigem leis algébricas (como a comutatividade da multiplicação), precisamos aplicar teoremas específicos, como Nat.mul_comm.

3.1.2. Lógica Proposicional em Lean🔗

Os conectivos lógicos ∧, ∨, →, ↔ e ¬ estão disponíveis diretamente no Lean, de modo que uma fórmula proposicional pode ser representada como uma proposição em Lean. Isso nos fornece uma ponte conveniente entre a semântica da linguagem natural e o raciocínio formal. Podemos traduzir o conteúdo semântico de uma sentença para uma proposição em Lean e, em seguida, usar Lean para verificar se uma conclusão decorre de um conjunto de hipóteses.

Chamamos "sistema dedutivo" um conjunto das regras de dedução. Existem vários sistemas dedutivos. A formalização de Prop em Lean corresponde a implementação do sistema chamado dedução natural definido por Gerhard Gentzen em 1930. Usando as regras de dedução natural, podemos provar que uma fórmula α pode ser derivada a partir de um conjunto de fórmulas Γ, dizemos que Γ ⊢ α. Dizemos que ⊢ α quando a fórmula α é válida, uma tautologia.

Neste sistema dedutivo, cada conectivo vem com dois tipos de regra. As de introdução, que dizem como construir uma prova cuja conclusão usa o conectivo, e as de eliminação, que dizem como usar uma prova cuja hipótese o usa.

A regra de introdução de → diz que para provar P → Q, supomos P e derivamos Q. A tatica intro move o antecedente para as hipóteses.

A regra de eliminação é a chamada regra modus ponens. A partir de P → Q e de P, podemos concluir Q. O termo Lean h hP já é a prova de Q. A tática apply faz o mesmo de trás para frente, ela transforma o objetivo Q no novo objetivo P. A exact fecha a prova fornecendo a hipótese cujo tipo coincide com o tipo do objetivo. A assumption busca automaticamente se alguma hipótese do contexto coincide com o objetivo, sem que seja necessário nomeá-la explicitamente.

Para a conjunção, provar P ∧ Q depende de uma prova de P e de uma prova de Q. A tática constructor divide o objetivo em dois novos objetivos; o construtor anônimo ⟨_, _⟩ faz o mesmo em forma de termo. A eliminação de ∧ em P ∧ Q significa que podemos concluir P ou Q. São duas regras, e em Lean são as projeções .1 (ou .left) e .2 (ou .right). A tática obtain desmonta a hipótese de uma vez, dando nome às duas partes.

Para provar P ∨ Q basta provar um dos dois lados. São duas regras, e os construtores Or.inl (aplicado pela tática left) e Or.inr (aplicado pela tática right) formalizam elas. A regra de eliminação da disjunção é o teorema Or.elim, a chamada "prova por casos". Dada a hipótese P ∨ Q, não sabemos qual das duas proposições é verdadeira. Portanto, para concluir R, precisamos provar R em ambos os casos (assumindo P no primeiro e Q no segundo). A tática cases gera exatamente esses dois cenários.

Não há um conectivo primitivo para a negação: ¬ P é notação para P → False onde False é a proposição que não possui prova. Desta forma, a introdução da negação usa a mesma regra da introdução da implicação →. Para provar ¬P, supomos P para derivar False. A eliminação é a eliminação de →. A regra que a tradição chama de ex falso quodlibet (princípio da explosão), a partir de uma contradição ou de uma premissa falsa, qualquer conclusão pode ser deduzida. False.elim em Lean. As duas juntas são absurd.

A bicondicional P ↔ Q é definida como a conjunção das duas implicações ((P → Q) ∧ (Q → P)), a tática constructor evoca Iff.intro que transforma o objetivo da prova em duas provas, uma para cada implicação. Os parâmetros do construtor explicam as regras de eliminação, duas regras dado tratar-se de uma conjunção de implicações, Iff.mpr e Iff.mp.

Até este ponto, todas as regras que utilizamos pertencem à lógica construtiva (ou intuicionista). Nela, provar uma disjunção P ∨ Q exige construir explicitamente uma prova de P ou uma prova de Q. Não é permitido afirmar que "um dos dois é verdade" sem saber qual. Em particular, a lógica construtiva não assume que toda proposição é necessariamente verdadeira ou falsa. A lógica clássica acrescenta o princípio do terceiro excluído, Classical.em, que afirma que para qualquer proposição P, vale P ∨ ¬P. A partir desse princípio, derivamos duas táticas fundamentais para provas clássicas:

• by_cases. Quando usamos by_cases (hP : P), o objetivo atual é dividido em dois casos independentes, um assumindo hP : P (P é verdadeiro) e outro assumindo hP : ¬P (P é falso).

• by_contra: Realiza a prova por redução ao absurdo. Para provar P, supõe-se que ¬ P e o objetivo torna-se derivar uma contradição (False).

3.1.3. As regras dos Quantificadores em Lean🔗

O tipo Prop não está limitado ao raciocínio proposicional; ele também nos permite representar proposições da lógica de primeira ordem. Como vimos, o Lean é fundamentado na teoria dos tipos, na qual toda variável pertence a algum tipo. Podemos entender um tipo como o "universo" ou "domínio de discurso" da lógica formal. No entanto, como veremos, há uma diferença importante: enquanto a lógica de primeira ordem clássica exige que o domínio de interpretação seja sempre um conjunto não-vazio, em Lean um tipo não precisa ser necessariamente habitado.

A expressividade de Prop vai além de lógica de primeira ordem. Poderíamos ainda falar de lógicas polissortidas onde poderíamos ter mais de um tipo usado em uma mesma expressão lógica. Por exemplo, podemos querer usar a lógica de primeira ordem para geometria, com quantificadores sobre pontos e linhas. Mas nesta seção, nos restringimos os predicados a um único universo U.

Seguindo a estrutura da seção anterior, explicaremos quatro novas regras: duas para o quantificador universal (∀) e duas para o existencial (∃).

A introdução de ∀ estabelece que, para provar que uma propriedade vale para todo x, basta tomar um x arbitrário e demonstrar que a propriedade se aplica a ele. Em modo de tática, usamos a mesma tática intro, mas agora ela adiciona um novo objeto no contexto, também como variável do tipo apropriado, em vez de uma hipótese do tipo Prop. A eliminação de ∀ é feita por aplicação direta: se temos uma prova h : ∀ x, P x e um objeto d, a aplicação h d nos fornece uma prova de P d, desde que os tipos obviamente sejam compatíveis.

A introdução de ∃ exige uma testemunha (o objeto que satisfaz a propriedade). Em modo de tática, a tática use substitui a variável quantificada pelo objeto fornecido e deixa como novo objetivo a prova de que tal objeto satisfaz o predicado. Em modo de termo, isso é feito pelo construtor Exists.intro.

A eliminação de ∃ é a regra mais delicada. De ∃ x, P x sabe-se que há uma testemunha, mas não sabemos qual elemento do domínio usar. A tática obtain aplica o teorema Exists.elim, introduzindo a testemunha com um nome no contexto, junto com a propriedade que ela satisfaz.

Tendo apresentado as regras de introdução e eliminação dos quantificadores, é importante observar como o Lean trata a existência de valores em um tipo na prática.

A demonstração abaixo de (∀ x, P x) → ∃ x, P x só é válida se declararmos previamente uma variável u : U. Isso evidencia uma diferença sutil entre a lógica de primeira ordem tradicional e a implementação no Lean: enquanto a dedução natural clássica assume implicitamente que o universo de discurso é sempre não-vazio, no Lean um tipo pode ser vazio (não-habitado). Assim, para instanciar a testemunha com use u, precisamos fornecer a suposição explícita de que existe ao menos um elemento u : U. Uma outra forma de ter o mesmo efeito seria demandar que o tipo U implemente a classe Nonempty.