Istruzioni
Il tuo compito è dimostrare l'uguaglianza tra una funzione personalizzata che inverte una lista e la funzione integrata List.reverse.
Data la natura di questo esercizio, invece di basarsi sui tradizionali test a runtime, la dimostrazione viene verificata da un teorema check.
Puoi considerare il test superato se questo teorema supera il controllo dei tipi.
Se lavori in locale o nel playground online di Lean, tramite Lean InfoView riceverai un feedback immediato su quali teoremi hanno successo e quali no, e sul perché falliscono.
È uno strumento preziosissimo: può mostrare tutti i valori locali usati nella dimostrazione e l'obiettivo corrente.
La tattica sorry fa sembrare corretta qualsiasi dimostrazione.
Per questo motivo, il teorema check potrebbe sembrare superare automaticamente il controllo dei tipi prima che una dimostrazione sia davvero scritta.
Una volta rimosso sorry dalla dimostrazione, Lean InfoView mostrerà il feedback corretto.
Dimostrare teoremi in Lean
La dimostrazione di teoremi è parte integrante di Lean.
Permette a chi programma di dimostrare proprietà sui propri programmi, di ragionare sul loro comportamento e di codificare vincoli e specifiche a livello di tipo.
Questo capitolo offre una buona introduzione alla dimostrazione di teoremi in Lean.
Per approfondire, questo libro è elencato tra le risorse ufficiali sul sito di Lean.
Lean offre molte tattiche in grado di automatizzare le dimostrazioni, o parti di esse.
Potresti voler dare un'occhiata a una guida di riferimento del linguaggio.
Possiamo usare l'attributo del compilatore csimp su un teorema che dimostra l'uguaglianza tra due definizioni.
Questo attributo indica al compilatore di usare la seconda definizione al posto della prima:
@[csimp]
theorem custom_reverse_eq_spec_reverse : @Extra.custom_reverse = @List.reverse := by
... -- proof here
-- now any occurrence of `Extra.custom_reverse` may now compile to `List.reverse`.
È particolarmente utile quando un'implementazione è più efficiente ma meno chiara.
Possiamo scrivere una specifica semplice e far usare al codice compilato l'implementazione più efficiente.
Molte funzioni di List e Array usano questo schema.
