2.1. Predicados e Quantificadores🔗

A Aula 1 excluiu "x é par" das proposições porque a sua verdade depende da variável livre x. Um predicado torna essa dependência explícita. Um predicado sobre um tipo α atribui uma proposição a cada elemento de α, então em Lean um predicado é uma função de tipo α → Prop.

fun n => n > 3 : Nat → Prop#check fun n : Nat => n > 3

fun n => n > 3 : Nat → Prop

Quantificadores ligam a variável de um predicado e produzem uma proposição, e a Tabela 2.1.1 nomeia os dois.G. Frege, Begriffsschrift, eine der arithmetischen nachgebildete Formelsprache des reinen Denkens, Verlag von Louis Nebert, Halle, 1879. Escrevemos P x para a proposição que o predicado P produz em x.

Símbolo	Nome	Leitura
∀ x, P x	quantificador universal	P x vale para todo x
∃ x, P x	quantificador existencial	P x vale para algum x

Tabela 2.1.1. Os dois quantificadores, com os seus símbolos e leituras.

O quantificador liga a sua variável, então ∀ x, P x não depende de variável livre e é uma proposição. A variável percorre um tipo. Por exemplo, ∃ n : Nat, n * n = 9 afirma que algum número natural elevado ao quadrado dá 9. Quando o contexto determina o tipo, Lean o infere e omitimos a anotação.

2.1.1. Exemplos🔗

Os exemplos abaixo escrevem predicados e proposições quantificadas e leem os seus tipos com #check. Um predicado tem tipo α → Prop, e uma proposição quantificada, que liga a sua variável, tem tipo Prop. O comando #eval informa o valor de verdade de um predicado decidível num ponto concreto através de decide.

Exemplo 1. Aplicar um predicado a um argumento produz uma proposição.

(fun n => n < 5) 3 : Prop#check (fun n : Nat => n < 5) 3

(fun n => n < 5) 3 : Prop

Exemplo 2. Um predicado pode percorrer qualquer tipo, entre eles as cadeias de caracteres.

fun s => s.length > 0 : String → Prop#check fun s : String => s.length > 0

fun s => s.length > 0 : String → Prop

Exemplo 3. Um predicado de dois argumentos é uma relação binária, uma função em Prop em duas etapas.

fun m n => m ≤ n : Nat → Nat → Prop#check fun m n : Nat => m ≤ n

fun m n => m ≤ n : Nat → Nat → Prop

Exemplo 4. Um enunciado universalmente quantificado é uma proposição.

∀ (n : Nat), n + 0 = n : Prop#check ∀ n : Nat, n + 0 = n

∀ (n : Nat), n + 0 = n : Prop

Exemplo 5. E um enunciado existencialmente quantificado também.

∃ n, n > 100 : Prop#check ∃ n : Nat, n > 100

∃ n, n > 100 : Prop

Exemplo 6. Quantificadores aninhados de tipos diferentes ainda produzem uma proposição.

∀ (m : Nat), ∃ n, m < n : Prop#check ∀ m : Nat, ∃ n : Nat, m < n

∀ (m : Nat), ∃ n, m < n : Prop

Exemplo 7. A variável ligada de um existencial pode percorrer cadeias de caracteres.

∃ s, s.length = 3 : Prop#check ∃ s : String, s.length = 3

∃ s, s.length = 3 : Prop

Exemplo 8. Uma relação binária aplicada aos seus dois argumentos é de novo uma proposição.

(fun m n => m ≤ n) 2 3 : Prop#check (fun m n : Nat => m ≤ n) 2 3

(fun m n => m ≤ n) 2 3 : Prop

Exemplo 9. Num ponto concreto um predicado decidível tem um valor de verdade computável, aqui verdadeiro.

true#eval decide (3 < 5)

true

Exemplo 10. A mesma computação informa falso onde o predicado não vale.

false#eval decide (2 = 3)

false