1.6. A Sintaxe de Lean🔗

As seções seguintes leem e escrevem Lean, então esta fixa a notação. Ela explica como uma declaração é escrita, não o que torna uma prova correta, assunto das seções posteriores.

Uma declaração dá nome a um enunciado e apresenta a sua prova. A palavra-chave vem primeiro, depois o nome, depois as hipóteses entre parênteses, depois o enunciado após os dois-pontos, e por fim a prova após :=.

theorem and_swap (P Q : Prop) (h : P ∧ Q) : Q ∧ P :=
  ⟨h.right, h.left⟩

Aqui theorem dá ao resultado o nome and_swap. Os parâmetros (P Q : Prop) e (h : P ∧ Q) introduzem duas proposições e uma hipótese. O enunciado a provar é Q ∧ P, e a prova é o termo após :=. A palavra-chave example substitui theorem quando o resultado dispensa nome.

A Tabela 1.6.1 lista as construções de sintaxe que as seções seguintes usam.

Escrito	Lido como
`example (h : P) : Q := e`	enunciado anônimo com hipótese h, provado por e
`fun h => e`	a função que leva h em e
`f a`	f aplicada a a, sem parênteses
`⟨a, b⟩`	o construtor anônimo, aqui um par
`h.left`, `h.right`	as duas componentes de uma conjunção
`by`	entra no modo de táticas, uma tática por linha
`·`	foca o objetivo seguinte dentro de um bloco de táticas
`sorry`	marcador de uma prova ausente
`-- texto`	comentário até o fim da linha

Tabela 1.6.1. A sintaxe de declarações, termos e blocos de táticas.

Os símbolos lógicos são unicode, e a Tabela 1.6.2 dá a abreviação que digita cada um. Digitar a abreviação com contrabarra e em seguida espaço ou tabulação insere o caractere no VS Code.

Símbolo	Significado	Digitado como
→	implicação	`\to`
∧	conjunção	`\and`
∨	disjunção	`\or`
¬	negação	`\not`
↔	bicondicional	`\iff`
⊥	absurdo	`\bot`
⟨ ⟩	construtor anônimo	`\langle`, `\rangle`
·	foco de objetivo	`\.`

Tabela 1.6.2. Os símbolos lógicos e as abreviações que os digitam.

O mesmo enunciado se prova por um termo ou no modo de táticas, e os dois produzem a mesma prova subjacente. As seções seguintes usam ambos.

example (P Q : Prop) (h : P ∧ Q) : Q ∧ P :=
  ⟨h.right, h.left⟩

example (P Q : Prop) (h : P ∧ Q) : Q ∧ P := byP:PropQ:Proph:P ∧ Q⊢ Q ∧ P
  exact ⟨h.right, h.left⟩All goals completed! 🐙

Os comandos que inspecionam uma declaração começam com #. O comando #check imprime o tipo de um termo, que no caso de uma prova é a proposição que ela prova.

fun P Q h => ⟨h.right, h.left⟩ : ∀ (P Q : Prop), P ∧ Q → Q ∧ P#check fun (P Q : Prop) (h : P ∧ Q) =>
  (⟨h.right, h.left⟩ : Q ∧ P)

fun P Q h => ⟨h.right, h.left⟩ : ∀ (P Q : Prop), P ∧ Q → Q ∧ P