Introdução
A turma do jardim de infância está a aprender a cultivar plantas.
A professora achou que seria uma boa ideia dar à turma sementes para plantar e fazer crescer na terra.
Para isso, as crianças colocaram copinhos ao longo dos peitoris das janelas e plantaram um tipo de planta em cada copo.
As crianças puderam escolher as suas preferidas entre quatro tipos de sementes disponíveis: relva, trevo, rabanetes e violetas.
Instruções
A tua tarefa é, dado um diagrama, determinar que plantas cada criança da turma do jardim de infância tem a seu cargo.
Há 12 crianças na turma:
- Alice, Bob, Charlie, David, Eve, Fred, Ginny, Harriet, Ileana, Joseph, Kincaid e Larry.
Plantam-se quatro tipos diferentes de sementes:
| Planta |
Codificação no diagrama |
| Grass |
G |
| Clover |
C |
| Radish |
R |
| Violet |
V |
Cada criança recebe quatro copos, dois em cada fila:
[window][window][window]
........................ # each dot represents a cup
........................
O professor atribui os copos às crianças por ordem alfabética dos seus nomes, o que significa que Alice vem primeiro e Larry por último.
Aqui está um diagrama de exemplo que representa as plantas da Alice:
[window][window][window]
VR......................
RG......................
Na primeira fila, a mais próxima das janelas, tem um violet e um radish.
Na segunda fila tem um radish e algum grass.
O teu programa receberá as plantas da esquerda para a direita, começando pela fila mais próxima das janelas.
A partir disto, deverá conseguir determinar que plantas pertencem a cada criança.
Por exemplo, se lhe for dito que o jardim tem o seguinte aspeto:
[window][window][window]
VRCGVVRVCGGCCGVRGCVCGCGV
VRCCCGCRRGVCGCRVVCVGCGCV
Então, se lhe pedirem as plantas da Alice, deve fornecer:
- Violets, radishes, violets, radishes
Já se lhe pedirem as plantas do Bob, obteria:
- Clover, grass, clover, clover
Vetores
O valor devolvido da função plants é um Vector Plant 4.
Os vetores representam arrays com um comprimento fixo.
Esse comprimento também pode ser determinado em tempo de execução.
Podes pensar neles como um par formado por um Array e uma prova de que o array tem o comprimento necessário.
Isto significa que tens de fornecer essa prova para construir um Vector.
Este capítulo dá uma boa introdução à prova de teoremas em Lean.
Para um estudo mais aprofundado, este livro consta como recurso oficial no site do Lean.
O Lean oferece muitas táticas que conseguem automatizar uma prova ou partes dela.
Talvez queiras consultar uma referência da linguagem.
