3.6. Enunciados de Teoremas
Um theorem é uma definição cujo tipo é uma proposição. Enunciá-lo não exige prova; o marcador sorry fica onde a prova entrará, e Lean assinala cada uso dele. Os enunciados abaixo especificam as funções desta aula, e o espaço de nomes evita que seus nomes colidam com os de Mathlib.
namespace SorryTheorems
theorem add_comm (m n : ℕ) :
add m n = add n m := m:ℕn:ℕ⊢ add m n = add n m
All goals completed! 🐙
theorem add_assoc (l m n : ℕ) :
add (add l m) n = add l (add m n) := l:ℕm:ℕn:ℕ⊢ add (add l m) n = add l (add m n)
All goals completed! 🐙
theorem mul_comm (m n : ℕ) :
mul m n = mul n m := m:ℕn:ℕ⊢ mul m n = mul n m
All goals completed! 🐙
theorem mul_assoc (l m n : ℕ) :
mul (mul l m) n = mul l (mul m n) := l:ℕm:ℕn:ℕ⊢ mul (mul l m) n = mul l (mul m n)
All goals completed! 🐙
theorem mul_add (l m n : ℕ) :
mul l (add m n) = add (mul l m) (mul l n) := l:ℕm:ℕn:ℕ⊢ mul l (add m n) = add (mul l m) (mul l n)
All goals completed! 🐙
theorem reverse_reverse {α : Type} (xs : List α) :
reverse (reverse xs) = xs := α:Typexs:List α⊢ reverse (reverse xs) = xs
All goals completed! 🐙
end SorryTheorems
A computação não os prova. rfl resolve add 2 7 = add 7 2, pois os dois lados computam para 9, mas em add m n = add n m as variáveis bloqueiam a computação, e a lei geral precisa de indução estrutural, o assunto das próximas aulas.
Os axiomas são a outra maneira de afirmar sem provar, e merecem mais desconfiança. Uma constante opaque tem tipo e nenhuma definição, e um axiom afirma uma proposição sem prova nenhuma. Nada o verifica, então um axioma inconsistente quebra silenciosamente todo o desenvolvimento. A disciplina enuncia axiomas apenas para discuti-los.
opaque a : ℤ
opaque b : ℤ
axiom a_less_b : a < b
3.6.1. Exemplos
Os exemplos abaixo releem os enunciados, separam o que a computação resolve do que ela não resolve e rastreiam de quais axiomas uma prova depende. O espaço de nomes MoreTheorems mantém os nomes novos longe dos de Mathlib.
Exemplo 1. Um enunciado com parâmetros nomeados é uma proposição universalmente quantificada.
#check @SorryTheorems.add_comm
Exemplo 2. Um parâmetro implícito aparece entre chaves, e o enunciado quantifica também sobre o tipo.
#check @SorryTheorems.reverse_reverse
Exemplo 3. O comando #print axioms informa em que uma prova se apoia, e sorry deixa o rastro sorryAx.
#print axioms SorryTheorems.add_comm
Exemplo 4. Uma lei que a computação resolve dispensa indução. O zero à direita casa a primeira equação de add, então rfl a prova para todo n.
namespace MoreTheorems
theorem add_zero_right (n : ℕ) : add n 0 = n := rfl
end MoreTheorems
#print axioms MoreTheorems.add_zero_right
Exemplo 5. O mesmo vale para a primeira equação de eval, qualquer que seja o ambiente.
namespace MoreTheorems
theorem eval_num (env : String → ℤ) (i : ℤ) :
eval env (AExp.num i) = i := rfl
end MoreTheorems
#check @MoreTheorems.eval_num
Exemplo 6. Uma equação fechada merece um nome tanto quanto uma lei geral.
namespace MoreTheorems
theorem fib_seven : fib 7 = 13 := rfl
theorem reverse_nil : reverse ([] : List ℕ) = [] := rfl
end MoreTheorems
Exemplo 7. Ligadores à esquerda dos dois-pontos e um ∀ explícito enunciam a mesma proposição.
namespace MoreTheorems
theorem all_add_zero : ∀ n : ℕ, add n 0 = n :=
fun _ => rfl
end MoreTheorems
#check @MoreTheorems.all_add_zero
Exemplo 8. Aplicar um teorema enunciado a argumentos instancia o enunciado, exista ou não uma prova.
#check SorryTheorems.add_comm 2 3
Exemplo 9. #print axioms mostra tudo o que uma prova usa. A prova abaixo se apoia no axioma desta seção e em propext, usado pelo lema de Mathlib.
namespace MoreTheorems
theorem a_ne_b : a ≠ b := ne_of_lt a_less_b
end MoreTheorems
#print axioms MoreTheorems.a_ne_b
Exemplo 10. As variáveis bloqueiam a computação, então a lei abaixo espera pela indução estrutural e carrega sorryAx enquanto isso.
namespace MoreTheorems
theorem half_double (n : ℕ) : half (add n n) = n := n:ℕ⊢ half (add n n) = n
All goals completed! 🐙
end MoreTheorems
#print axioms MoreTheorems.half_double