Οδηγίες
Η αποστολή σου είναι να αποδείξεις την ισότητα ανάμεσα σε μια δική σου συνάρτηση αντιστροφής λίστας και στην ενσωματωμένη List.reverse.
Λόγω της φύσης αυτής της άσκησης, αντί να βασιζόμαστε σε παραδοσιακά tests χρόνου εκτέλεσης, η απόδειξη ελέγχεται από ένα θεώρημα check.
Μπορείς να θεωρήσεις ότι το test πέρασε αν αυτό το θεώρημα περνάει τον έλεγχο τύπων.
Αν δουλεύεις τοπικά ή στο διαδικτυακό playground του Lean, θα παίρνεις άμεση ανατροφοδότηση για το αν κάποιο θεώρημα πετυχαίνει ή αποτυγχάνει, και γιατί αποτυγχάνει, μέσα από το Lean InfoView.
Είναι ένα ανεκτίμητο εργαλείο, ικανό να δείξει όλες τις τοπικές τιμές που χρησιμοποιεί η απόδειξή σου, και τον τρέχοντα στόχο σου.
Η τακτική sorry κάνει κάθε απόδειξη να φαίνεται σωστή.
Για αυτόν τον λόγο, το θεώρημα check μπορεί να φαίνεται ότι περνάει αυτόματα τον έλεγχο τύπων πριν καν γραφτεί η πραγματική απόδειξη.
Μόλις αφαιρέσεις το sorry από την απόδειξή σου, το Lean InfoView θα δείξει τη σωστή ανατροφοδότηση.
Αποδεικνύοντας θεωρήματα στη Lean
Η απόδειξη θεωρημάτων είναι αναπόσπαστο κομμάτι της Lean.
Δίνει τη δυνατότητα στους προγραμματιστές να αποδεικνύουν ιδιότητες των προγραμμάτων τους, να συλλογίζονται τη συμπεριφορά τους και να κωδικοποιούν περιορισμούς και προδιαγραφές σε επίπεδο τύπων.
Αυτό το κεφάλαιο αποτελεί μια καλή εισαγωγή στην απόδειξη θεωρημάτων στη Lean.
Για μια πιο βαθιά ματιά, αυτό το βιβλίο αναφέρεται ως επίσημος πόρος στην ιστοσελίδα της Lean.
Η Lean προσφέρει πολλές τακτικές που μπορούν να αυτοματοποιήσουν αποδείξεις, ή μέρη τους.
Ίσως θελήσεις να δεις μια αναφορά γλώσσας.
Μπορούμε να χρησιμοποιήσουμε το χαρακτηριστικό του μεταγλωττιστή csimp σε ένα θεώρημα που αποδεικνύει την ισότητα μεταξύ δύο ορισμών.
Αυτό το χαρακτηριστικό δίνει εντολή στον μεταγλωττιστή να χρησιμοποιήσει τον δεύτερο ορισμό στη θέση του πρώτου:
@[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`.
Είναι ιδιαίτερα χρήσιμο σε περιπτώσεις όπου μια υλοποίηση είναι πιο αποδοτική αλλά λιγότερο σαφής.
Μπορούμε να γράψουμε μια απλή προδιαγραφή και να αφήσουμε τον μεταγλωττισμένο κώδικα να χρησιμοποιήσει την πιο αποδοτική υλοποίηση αντ' αυτής.
Πολλές συναρτήσεις των List και Array χρησιμοποιούν αυτό το μοτίβο.
