Introducción
La clase de infantil está aprendiendo a cultivar plantas.
La maestra pensó que sería buena idea dar a la clase semillas para plantarlas y hacerlas crecer en la tierra.
Con ese fin, los niños han colocado vasitos a lo largo de los alféizares de las ventanas y han plantado un tipo de planta en cada vasito.
Los niños pudieron elegir sus favoritas entre cuatro tipos de semillas disponibles: grass, clover, radishes y violets.
Instrucciones
Tu tarea consiste en determinar, dado un diagrama, qué plantas le corresponden a cada niño de la clase de infantil.
En la clase hay 12 niños:
- Alice, Bob, Charlie, David, Eve, Fred, Ginny, Harriet, Ileana, Joseph, Kincaid y Larry.
Se plantan cuatro tipos distintos de semillas:
| Planta |
Codificación en el diagrama |
| Grass |
G |
| Clover |
C |
| Radish |
R |
| Violet |
V |
Cada niño recibe cuatro vasos, dos en cada fila:
[window][window][window]
........................ # each dot represents a cup
........................
Su profesor asigna los vasos a los niños por orden alfabético de sus nombres, lo que significa que Alice es la primera y Larry el último.
Aquí tienes un diagrama de ejemplo que representa las plantas de Alice:
[window][window][window]
VR......................
RG......................
En la primera fila, la más cercana a las ventanas, tiene «violet» y «radish».
En la segunda fila tiene «radish» y un poco de «grass».
A tu programa se le darán las plantas de izquierda a derecha, empezando por la fila más cercana a las ventanas.
A partir de esto, debería poder determinar qué plantas le corresponden a cada alumno.
Por ejemplo, si se le dice que el jardín tiene este aspecto:
[window][window][window]
VRCGVVRVCGGCCGVRGCVCGCGV
VRCCCGCRRGVCGCRVVCVGCGCV
Entonces, si se le piden las plantas de Alice, debería devolver:
- Violets, radishes, violets, radishes
Y si se le piden las plantas de Bob, debería devolver:
- Clover, grass, clover, clover
Vectores
El valor devuelto de la función plants es un Vector Plant 4.
Los vectores representan arrays de longitud fija.
Esta longitud también puede determinarse en tiempo de ejecución.
Se pueden concebir como un par formado por un Array y una prueba de que el array tiene la longitud requerida.
Esto significa que debes proporcionar esta prueba para poder construir un Vector.
Este capítulo ofrece una buena introducción a la demostración de teoremas en Lean.
Para profundizar más, este libro figura como recurso oficial en el sitio web de Lean.
Lean ofrece muchas tácticas que pueden automatizar una demostración o partes de ella.
Puede que quieras consultar una referencia del lenguaje.
