6.4. Estruturas e Registros
Uma estrutura é um tipo indutivo com um único construtor e campos nomeados, e Lean deriva uma projeção para cada campo. É a forma natural para um registro de valores relacionados. O construtor anônimo ⟨…⟩, a sintaxe de campos { … } e a sintaxe de atualização { r with … } constroem ou modificam uma estrutura, e extends constrói uma estrutura maior sobre uma menor. O And.intro da Aula 1 e o par da Aula 3 são eles próprios estruturas de um único construtor.
namespace Func
structure Segment where
lo : ℤ
hi : ℤ
def width (s : Segment) : ℤ := s.hi - s.lo
structure NamedSegment extends Segment where
name : String
end Func
Um NamedSegment carrega os dois campos de Segment e mais um, e uma projeção alcança os campos herdados diretamente.
6.4.1. Exemplos
Os exemplos abaixo constroem, projetam, atualizam e estendem registros.
Example 1. Uma projeção lê um campo, e width computa a partir de dois deles.
namespace Func
def seg1 : Segment := { lo := 1, hi := 5 }
example : width seg1 = 4 := ⊢ width seg1 = 4 All goals completed! 🐙
end Func
Example 2. A sintaxe de campos { … } e o construtor anônimo ⟨…⟩ constroem o mesmo valor.
namespace Func
def seg2 : Segment := ⟨1, 5⟩
example : seg1 = seg2 := rfl
end Func
Example 3. A sintaxe de atualização { r with … } copia um registro e muda um campo.
namespace Func
def widen (s : Segment) : Segment :=
{ s with hi := s.hi + 1 }
example : (widen seg1).hi = 6 := ⊢ (widen seg1).hi = 6 All goals completed! 🐙
end Func
Example 4. extends acrescenta um campo, e os campos herdados permanecem acessíveis.
namespace Func
def ns1 : NamedSegment :=
{ lo := 0, hi := 2, name := "a" }
example : ns1.lo = 0 := ⊢ ns1.lo = 0 All goals completed! 🐙
end Func
Example 5. O novo campo é alcançado como qualquer outro.
namespace Func
example : ns1.name = "a" := rfl
end Func
Example 6. Um campo pode ser ele próprio uma função, e a projeção o recupera.
namespace Func
structure Handler where
run : ℕ → ℕ
def dbl : Handler := { run := fun n => n + n }
example : dbl.run 3 = 6 := rfl
end Func
Example 7. Construir um registro e projetar um campo devolve o campo, por computação.
namespace Func
example : (⟨1, 5⟩ : Segment).lo = 1 := rfl
end Func
Example 8. Uma função de um registro computada a partir dos seus campos.
namespace Func
def midpoint (s : Segment) : ℤ :=
(s.lo + s.hi) / 2
example : midpoint ⟨0, 4⟩ = 2 := ⊢ midpoint { lo := 0, hi := 4 } = 2 All goals completed! 🐙
end Func
Example 9. Prod é a estrutura canônica de dois campos, com Prod.fst e Prod.snd as suas projeções.
example : (Prod.fst (3, 5) : ℕ) = 3 := rfl
Example 10. O And.intro da Aula 1 é uma estrutura de dois campos, e o construtor anônimo o constrói.
example (a b : Prop) (ha : a) (hb : b) : a ∧ b :=
⟨ha, hb⟩