4.4. Raciocínio sobre Igualdade
A tática rfl prova uma conclusão l = r quando os dois lados se tornam sintaticamente idênticos sob computação, e ela tem sucesso aproximadamente onde um matemático diz "por definição". O termo rfl da Aula 3 é a sua forma de termo. A computação aqui nomeia seis conversões.
Conversão | O que ela faz |
|---|---|
α | renomeia uma variável ligada |
β | aplica uma função anônima ao seu argumento |
δ | desdobra uma definição |
ζ |
substitui um |
η |
identifica |
ι | projeta uma aplicação de construtor |
A igualdade também é um conjunto de regras. Eq.refl a introduz, Eq.symm e Eq.trans dizem que ela é uma relação de equivalência, e Eq.subst substitui iguais por iguais em um contexto que uma metavariável representa. Uma nota de sintaxe: = liga mais forte que os conectivos, então a = b ∧ c = d se lê (a = b) ∧ (c = d).
Eq.refl : ∀ (a : ?α), a = a Eq.symm : ?a = ?b → ?b = ?a Eq.trans : ?a = ?b → ?b = ?c → ?a = ?c Eq.subst : ?a = ?b → ?P ?a → ?P ?b
namespace Backward
theorem Eq_trans_symm {α : Type} (a b c : α)
(hab : a = b) (hcb : c = b) : a = c := α:Typea:αb:αc:αhab:a = bhcb:c = b⊢ a = c
α:Typea:αb:αc:αhab:a = bhcb:c = b⊢ a = ?bα:Typea:αb:αc:αhab:a = bhcb:c = b⊢ ?b = cα:Typea:αb:αc:αhab:a = bhcb:c = b⊢ α
α:Typea:αb:αc:αhab:a = bhcb:c = b⊢ a = ?b All goals completed! 🐙
α:Typea:αb:αc:αhab:a = bhcb:c = b⊢ b = c α:Typea:αb:αc:αhab:a = bhcb:c = b⊢ c = b
All goals completed! 🐙
end Backward
A tática ac_rfl estende rfl com associatividade e comutatividade para os operadores registrados como associativos e comutativos, e a §4.6 registra o nosso add entre eles.
4.4.1. Exemplos
Os exemplos abaixo nomeiam a conversão que cada rfl realiza e então raciocinam com as regras da igualdade. A definição de double sustenta a conversão δ.
namespace Backward
def double (n : ℕ) : ℕ := n + n
end Backward
Example 1. A conversão α renomeia a variável ligada.
namespace Backward
theorem α_example {α β : Type} (f : α → β) :
(fun x => f x) = (fun y => f y) := α:Typeβ:Typef:α → β⊢ (fun x => f x) = fun y => f y
All goals completed! 🐙
end Backward
Example 2. A conversão β aplica uma função anônima ao seu argumento.
namespace Backward
theorem β_example {α β : Type} (f : α → β) (a : α) :
(fun x => f x) a = f a := α:Typeβ:Typef:α → βa:α⊢ (fun x => f x) a = f a
All goals completed! 🐙
end Backward
Example 3. A conversão δ desdobra a definição de double.
namespace Backward
theorem δ_example : double 5 = 5 + 5 := ⊢ double 5 = 5 + 5
All goals completed! 🐙
end Backward
Example 4. A conversão ζ substitui o let de escopo local.
namespace Backward
theorem ζ_example :
(let n : ℕ := 2
n + n) = 4 := ⊢ (let n := 2;
n + n) =
4
All goals completed! 🐙
end Backward
Example 5. A conversão η identifica fun x => f x com a própria f.
namespace Backward
theorem η_example {α β : Type} (f : α → β) :
(fun x => f x) = f := α:Typeβ:Typef:α → β⊢ (fun x => f x) = f
All goals completed! 🐙
end Backward
Example 6. A conversão ι projeta um componente de uma aplicação de construtor.
namespace Backward
theorem ι_example {α β : Type} (a : α) (b : β) :
Prod.fst (a, b) = a := α:Typeβ:Typea:αb:β⊢ (a, b).1 = a
All goals completed! 🐙
end Backward
Example 7. rfl prova add m 0 = m e não add 0 m = m, pois add recorre sobre o seu segundo argumento, como o terceiro exemplo trabalhado da Aula 3 mostrou. O segundo enunciado espera a §4.6.
example (m : ℕ) : add m 0 = m := m:ℕ⊢ add m 0 = m
All goals completed! 🐙
example (m : ℕ) : add 0 m = m := m:ℕ⊢ add 0 m = m
All goals completed! 🐙
Example 8. ac_rfl prova uma equação a menos de associatividade e comutatividade de +.
example (a b c : ℕ) : a + b + c = c + b + a := a:ℕb:ℕc:ℕ⊢ a + b + c = c + b + a
All goals completed! 🐙
Example 9. A mesma forma vale para *, também registrado como associativo e comutativo.
example (a b c : ℕ) : a * b * c = c * b * a := a:ℕb:ℕc:ℕ⊢ a * b * c = c * b * a
All goals completed! 🐙
Example 10. apply Eq.subst substitui iguais por iguais sob um predicado arbitrário, que a unificação recupera.
example (α : Type) (P : α → Prop) (a b : α)
(hab : a = b) (hPa : P a) : P b := α:TypeP:α → Propa:αb:αhab:a = bhPa:P a⊢ P b
α:TypeP:α → Propa:αb:αhab:a = bhPa:P a⊢ P a
All goals completed! 🐙