5.2. Construções Estruturadas
Os quatro construtos estruturados são as contrapartes, no modo de termos, de táticas da Aula 4. fix x : α descarrega um objetivo universalmente quantificado fixando um x arbitrário, como intro faz para um ∀ no modo de táticas. assume h : P descarrega uma implicação supondo o seu antecedente, como intro faz para uma →. have h : P := pf; resto nomeia como h uma prova pf de P para uso em resto, o passo progressivo que acrescenta um fato ao que já se sabe. show P from pf reafirma o objetivo como P, por definição, e fornece pf, o que documenta a prova e guia a elaboração. Um let x := t; resto no nível de termos abrevia um termo, não uma prova.
A composição de duas implicações, provada de forma regressiva na Aula 4 como três passos de "basta provar", se lê de forma progressiva como dois passos have que constroem o fato intermediário e depois a conclusão.
namespace Forward
theorem prop_comp (a b c : Prop) (hab : a → b)
(hbc : b → c) : a → c :=
assume ha : a;
have hb : b := hab ha;
show c from hbc hb
end Forward
Leia a prova como texto corrido. Suponha a. De ha e hab temos b, que nomeamos hb. De hb e hbc temos c, que é o objetivo. Cada have é uma inferência progressiva, e o termo de prova registra a derivação de cima para baixo.
5.2.1. Exemplos
Os exemplos abaixo usam fix, assume, have, show e um let no nível de termos, e cada um fica ao lado da tática que espelha.
Example 1. fix sozinho descarrega um objetivo universalmente quantificado, e o fun escrito da outra maneira é o mesmo termo.
namespace Forward
example : ∀ n : ℕ, n = n :=
fix n : ℕ; rfl
example : ∀ n : ℕ, n = n :=
fun n => rfl
end Forward
Example 2. assume sozinho descarrega uma implicação. A prova por táticas usa intro para o mesmo passo.
namespace Forward
example (a : Prop) : a → a :=
assume h : a; h
example (a : Prop) : a → a := a:Prop⊢ a → a
a:Proph:a⊢ a
All goals completed! 🐙
end Forward
Example 3. fix e assume juntos provam a projeção de forma progressiva, e o roteiro da Aula 4 com intro e apply fica ao lado.
namespace Forward
example : ∀ a b : Prop, a → b → a :=
fix a b : Prop; assume ha : a; assume hb : b; ha
example : ∀ a b : Prop, a → b → a := ⊢ ∀ (a b : Prop), a → b → a
a:Propb:Propha:ahb:b⊢ a
All goals completed! 🐙
end Forward
Example 4. have insere um passo progressivo, nomeando o fato derivado. A mesma prova insere o termo diretamente.
namespace Forward
example (a b : Prop) (hab : a → b) (ha : a) : b :=
have hb : b := hab ha; hb
example (a b : Prop) (hab : a → b) (ha : a) : b :=
hab ha
end Forward
Example 5. show P from pf documenta o objetivo, onde um termo simples o deixa implícito. As duas provas são a mesma.
namespace Forward
example (a : Prop) (ha : a) : a :=
show a from ha
example (a : Prop) (ha : a) : a :=
ha
end Forward
Example 6. A composição de implicações por dois passos have, depois a mesma prova reduzida a uma única aplicação.
namespace Forward
example (a b c : Prop) (hab : a → b) (hbc : b → c) :
a → c :=
assume ha : a;
have hb : b := hab ha;
show c from hbc hb
example (a b c : Prop) (hab : a → b) (hbc : b → c) :
a → c :=
assume ha : a; hbc (hab ha)
end Forward
Example 7. Um let no nível de termos abrevia um valor dentro de uma prova. Aqui os dois lados coincidem por computação, uma vez desdobrado o let.
namespace Forward
example : (2 : ℕ) + 2 = 4 :=
let n : ℕ := 2;
(rfl : n + n = 4)
end Forward
Example 8. Um have nomeia um fato que o resto da prova usa mais de uma vez. Aqui a implicação nomeada é aplicada a duas hipóteses diferentes.
namespace Forward
example (a b : Prop) (hab : a → b) (ha ha' : a) :
b ∧ b :=
have f : a → b := hab;
And.intro (f ha) (f ha')
end Forward
Example 9. O mesmo teorema no modo de táticas e no modo de termos estruturado, para que a correspondência seja visível linha a linha.
namespace Forward
example (a b : Prop) (hab : a → b) (ha : a) : b := a:Propb:Prophab:a → bha:a⊢ b
All goals completed! 🐙
example (a b : Prop) (hab : a → b) (ha : a) : b :=
show b from hab ha
end Forward
Example 10. show pode reafirmar o objetivo em uma forma definicionalmente igual, mas sintaticamente diferente, já que ¬ a se desdobra em a → False, e o modo de termos aceita a mudança.
namespace Forward
example (a : Prop) (h : a → False) : ¬ a :=
show a → False from h
end Forward