Οδηγίες
Ένας ρητός αριθμός ορίζεται ως το πηλίκο δύο ακεραίων a και b, που ονομάζονται αριθμητής και παρονομαστής αντίστοιχα, όπου b != 0.
Σημείωσε ότι μαθηματικά, ο παρονομαστής δε μπορεί να είναι μηδέν.
Ωστόσο, σε πολλές υλοποιήσεις ρητών αριθμών, θα διαπιστώσεις ότι ο παρονομαστής επιτρέπεται να είναι μηδέν, με συμπεριφορά παρόμοια με το θετικό ή αρνητικό άπειρο στους αριθμούς κινητής υποδιαστολής.
Σε αυτές τις περιπτώσεις, ο παρονομαστής και ο αριθμητής γενικά και πάλι δε μπορούν να είναι ταυτόχρονα μηδέν.
Η απόλυτη τιμή |r| του ρητού αριθμού r = a/b είναι ίση με |a|/|b|.
Το άθροισμα δύο ρητών αριθμών r₁ = a₁/b₁ και r₂ = a₂/b₂ είναι r₁ + r₂ = a₁/b₁ + a₂/b₂ = (a₁ * b₂ + a₂ * b₁) / (b₁ * b₂).
Η διαφορά δύο ρητών αριθμών r₁ = a₁/b₁ και r₂ = a₂/b₂ είναι r₁ - r₂ = a₁/b₁ - a₂/b₂ = (a₁ * b₂ - a₂ * b₁) / (b₁ * b₂).
Το γινόμενο (ο πολλαπλασιασμός) δύο ρητών αριθμών r₁ = a₁/b₁ και r₂ = a₂/b₂ είναι r₁ * r₂ = (a₁ * a₂) / (b₁ * b₂).
Η διαίρεση ενός ρητού αριθμού r₁ = a₁/b₁ με έναν άλλον r₂ = a₂/b₂ είναι r₁ / r₂ = (a₁ * b₂) / (a₂ * b₁) αν το a₂ δεν είναι μηδέν.
Η ύψωση ενός ρητού αριθμού r = a/b σε μη αρνητική ακέραια δύναμη n είναι r^n = (a^n)/(b^n).
Η ύψωση ενός ρητού αριθμού r = a/b σε αρνητική ακέραια δύναμη n είναι r^n = (b^m)/(a^m), όπου m = |n|.
Η ύψωση ενός ρητού αριθμού r = a/b σε πραγματικό (κινητής υποδιαστολής) αριθμό x είναι το πηλίκο (a^x)/(b^x), που είναι ένας πραγματικός αριθμός.
Η ύψωση ενός πραγματικού αριθμού x σε ρητό αριθμό r = a/b είναι x^(a/b) = root(x^a, b), όπου root(p, q) είναι η q-οστή ρίζα του p.
Υλοποίησε τις παρακάτω πράξεις:
- πρόσθεση, αφαίρεση, πολλαπλασιασμό και διαίρεση δύο ρητών αριθμών,
- απόλυτη τιμή, ύψωση ενός δεδομένου ρητού αριθμού σε ακέραια δύναμη, ύψωση ενός δεδομένου ρητού αριθμού σε πραγματική (κινητής υποδιαστολής) δύναμη, ύψωση ενός πραγματικού αριθμού σε ρητό αριθμό.
Η υλοποίησή σου των ρητών αριθμών θα πρέπει πάντα να είναι ανηγμένη στους ελάχιστους όρους.
Για παράδειγμα, το 4/4 θα πρέπει να ανάγεται σε 1/1, το 30/60 θα πρέπει να ανάγεται σε 1/2, το 12/8 θα πρέπει να ανάγεται σε 3/2, κ.λπ.
Για να ανάγεις έναν ρητό αριθμό r = a/b, διαίρεσε το a και το b με τον μέγιστο κοινό διαιρέτη (ΜΚΔ) των a και b.
Έτσι, για παράδειγμα, gcd(12, 8) = 4, άρα το r = 12/8 μπορεί να αναχθεί σε (12/4)/(8/4) = 3/2.
Η ανηγμένη μορφή ενός ρητού αριθμού θα πρέπει να είναι σε "τυπική μορφή" (ο παρονομαστής θα πρέπει πάντα να είναι ένας θετικός ακέραιος).
Αν υπάρχει παρονομαστής με αρνητικό ακέραιο, πολλαπλασίασε και τον αριθμητή και τον παρονομαστή με -1 για να διασφαλίσεις ότι επιτυγχάνεται η τυπική μορφή.
Για παράδειγμα, το 3/-4 θα πρέπει να ανάγεται σε -3/4
Θεώρησε ότι η γλώσσα προγραμματισμού που χρησιμοποιείς δε έχει κάποια υλοποίηση ρητών αριθμών.
Απόδειξη ιδιοτήτων
Σε αυτή την άσκηση, πρέπει να ορίσεις έναν τύπο RationalNumber που αναπαριστά έναν πλήρως ανηγμένο, έγκυρο, ρητό αριθμό.
Αυτό επιβάλλεται άμεσα από μια ιδιότητα που αποτελεί μέρος του ίδιου του τύπου.
Η κωδικοποίηση προδιαγραφών και περιορισμών απευθείας στο επίπεδο του τύπου κάνει τις μη έγκυρες καταστάσεις ουσιαστικά μη αναπαραστάσιμες.
Ωστόσο, αυτό θέτει επίσης ένα επιπλέον βάρος στον προγραμματιστή, ο οποίος πρέπει να αποδείξει ότι η ιδιότητα ισχύει πάντα.
Αυτό το κεφάλαιο παρέχει μια καλή εισαγωγή στην απόδειξη θεωρημάτων στη Lean.
Για μια πιο εις βάθος ανάλυση, αυτό το βιβλίο αναφέρεται ως επίσημος πόρος στον ιστότοπο της Lean.
Μπορεί επίσης να θέλεις να συμβουλευτείς μια αναφορά για τη γλώσσα.
