Introduzione
La classe della scuola dell'infanzia sta imparando a coltivare le piante.
L'insegnante ha pensato che sarebbe stata una buona idea dare alla classe dei semi da piantare e far crescere nella terra.
A questo scopo, i bambini hanno messo dei bicchierini sui davanzali e hanno piantato un tipo di pianta in ogni bicchiere.
I bambini hanno potuto scegliere i loro preferiti tra quattro tipi di semi disponibili: grass, clover, radishes e violets.
Istruzioni
Il tuo compito è, dato un diagramma, determinare quali piante spettano a ciascun bambino della classe dell'asilo.
Nella classe ci sono 12 bambini:
- Alice, Bob, Charlie, David, Eve, Fred, Ginny, Harriet, Ileana, Joseph, Kincaid, and Larry.
Vengono piantati quattro tipi diversi di semi:
| Pianta |
Codifica nel diagramma |
| Grass |
G |
| Clover |
C |
| Radish |
R |
| Violet |
V |
Ogni bambino riceve quattro bicchieri, due su ogni riga:
[window][window][window]
........................ # each dot represents a cup
........................
L'insegnante assegna i bicchieri ai bambini in ordine alfabetico in base ai loro nomi: Alice viene per prima e Larry per ultimo.
Ecco un esempio di diagramma che rappresenta le piante di Alice:
[window][window][window]
VR......................
RG......................
Nella prima riga, quella più vicina alle finestre, ha una violet ed un radish.
Nella seconda riga ha un radish e del grass.
Il programma riceverà le piante da sinistra a destra, a partire dalla riga più vicina alle finestre.
Da qui dovrebbe riuscire a determinare quali piante appartengono a ciascun bambino.
Per esempio, se gli viene detto che il giardino è questo:
[window][window][window]
VRCGVVRVCGGCCGVRGCVCGCGV
VRCCCGCRRGVCGCRVVCVGCGCV
Se poi gli vengono chieste le piante di Alice, dovrebbe restituire:
- Violets, radishes, violets, radishes
Mentre chiedendo le piante di Bob si otterrebbe:
- Clover, grass, clover, clover
Vettori
Il valore restituito dalla funzione plants è un Vector Plant 4.
I vettori rappresentano array con una lunghezza fissa.
Questa lunghezza può anche essere determinata a runtime.
Si possono pensare come una coppia formata da un Array e da una prova che l'array ha la lunghezza richiesta.
Questo significa che devi fornire questa prova per costruire un Vector.
Questo capitolo fornisce una buona introduzione alla dimostrazione di teoremi in Lean.
Per un approfondimento, questo libro è elencato come risorsa ufficiale sul sito di Lean.
Lean offre molte tattiche che possono automatizzare una dimostrazione o parti di essa.
Potresti voler consultare un riferimento del linguaggio.
