Introduction
La classe de maternelle apprend à faire pousser des plantes.
L'enseignant a jugé bon de donner à la classe des graines à planter et à faire pousser dans la terre.
Pour ce faire, les enfants ont disposé de petits gobelets le long des rebords de fenêtre et ont planté un type de plante dans chaque gobelet.
Les enfants ont pu choisir leurs préférées parmi quatre types de graines disponibles : gazon, trèfle, radis et violettes.
Instructions
Ta tâche est de déterminer, à partir d'un diagramme, quelles plantes chaque enfant de la classe de maternelle a la charge de cultiver.
La classe compte 12 enfants :
- Alice, Bob, Charlie, David, Eve, Fred, Ginny, Harriet, Ileana, Joseph, Kincaid et Larry.
Quatre types de graines différentes sont plantés :
| Plante |
Encodage du diagramme |
| Grass |
G |
| Clover |
C |
| Radish |
R |
| Violet |
V |
Chaque enfant reçoit quatre godets, deux sur chaque rangée :
[window][window][window]
........................ # each dot represents a cup
........................
Leur professeur attribue les godets aux enfants par ordre alphabétique de leur prénom, ce qui signifie qu'Alice arrive en premier et Larry en dernier.
Voici un exemple de diagramme qui représente les plantes d'Alice :
[window][window][window]
VR......................
RG......................
Dans la première rangée, la plus proche des fenêtres, elle a un violet et un radish. Dans la deuxième rangée, elle a un radish et du grass.
Ton programme recevra les plantes de gauche à droite, en commençant par la rangée la plus proche des fenêtres. À partir de ces informations, il doit pouvoir déterminer quelles plantes appartiennent à chaque enfant.
Par exemple, si on lui indique que le jardin ressemble à ceci :
[window][window][window]
VRCGVVRVCGGCCGVRGCVCGCGV
VRCCCGCRRGVCGCRVVCVGCGCV
Alors, si on lui demande les plantes d'Alice, il doit fournir :
- Violets, radishes, violets, radishes
tandis que si on lui demande les plantes de Bob, on obtient :
- Clover, grass, clover, clover
Vecteurs
La valeur de retour de la fonction plants est un Vector Plant 4.
Les vecteurs représentent des tableaux de longueur fixe.
Cette longueur peut aussi être déterminée à l'exécution.
On peut les voir comme un couple composé d'un Array et d'une preuve que le tableau possède la longueur requise.
Cela signifie que tu dois fournir cette preuve pour construire un Vector.
Ce chapitre est une bonne introduction à la démonstration de théorèmes en Lean.
Pour aller plus loin, ce livre est cité comme ressource officielle sur le site de Lean.
Lean propose de nombreuses tactiques qui peuvent automatiser une preuve, en tout ou en partie.
Tu peux aussi consulter une référence du langage.
