Anleitung
Eine rationale Zahl ist als der Quotient zweier Ganzzahlen a und b definiert, die man Zähler bzw. Nenner nennt, wobei b != 0 gilt.
Beachte, dass der Nenner mathematisch nicht null sein kann.
In vielen Implementierungen rationaler Zahlen ist der Nenner jedoch null erlaubt, mit einem Verhalten ähnlich wie positiv oder negativ Unendlich bei Gleitkommazahlen.
In diesen Fällen können Nenner und Zähler trotzdem im Allgemeinen nicht gleichzeitig null sein.
Der Betrag |r| der rationalen Zahl r = a/b ist gleich |a|/|b|.
Die Summe zweier rationaler Zahlen r₁ = a₁/b₁ und r₂ = a₂/b₂ ist r₁ + r₂ = a₁/b₁ + a₂/b₂ = (a₁ * b₂ + a₂ * b₁) / (b₁ * b₂).
Die Differenz zweier rationaler Zahlen r₁ = a₁/b₁ und r₂ = a₂/b₂ ist r₁ - r₂ = a₁/b₁ - a₂/b₂ = (a₁ * b₂ - a₂ * b₁) / (b₁ * b₂).
Das Produkt (die Multiplikation) zweier rationaler Zahlen r₁ = a₁/b₁ und r₂ = a₂/b₂ ist r₁ * r₂ = (a₁ * a₂) / (b₁ * b₂).
Die Division einer rationalen Zahl r₁ = a₁/b₁ durch eine andere r₂ = a₂/b₂ ergibt r₁ / r₂ = (a₁ * b₂) / (a₂ * b₁), wenn a₂ nicht null ist.
Das Potenzieren einer rationalen Zahl r = a/b mit einer nicht negativen ganzzahligen Potenz n ergibt r^n = (a^n)/(b^n).
Das Potenzieren einer rationalen Zahl r = a/b mit einer negativen ganzzahligen Potenz n ergibt r^n = (b^m)/(a^m), wobei m = |n| ist.
Das Potenzieren einer rationalen Zahl r = a/b mit einer reellen (Gleitkomma-)Zahl x ergibt den Quotienten (a^x)/(b^x), der eine reelle Zahl ist.
Das Potenzieren einer reellen Zahl x mit einer rationalen Zahl r = a/b ergibt x^(a/b) = root(x^a, b), wobei root(p, q) die q-te Wurzel von p ist.
Implementiere die folgenden Operationen:
- Addition, Subtraktion, Multiplikation und Division zweier rationaler Zahlen,
- Betrag, Potenzieren einer gegebenen rationalen Zahl mit einer ganzzahligen Potenz, Potenzieren einer gegebenen rationalen Zahl mit einer reellen (Gleitkomma-)Potenz, Potenzieren einer reellen Zahl mit einer rationalen Zahl.
Deine Implementierung rationaler Zahlen sollte immer vollständig gekürzt sein.
Zum Beispiel sollte 4/4 zu 1/1 gekürzt werden, 30/60 zu 1/2, 12/8 zu 3/2 usw.
Um eine rationale Zahl r = a/b zu kürzen, teilst du a und b durch den größten gemeinsamen Teiler (ggT) von a und b.
So ist zum Beispiel gcd(12, 8) = 4, also lässt sich r = 12/8 zu (12/4)/(8/4) = 3/2 kürzen.
Die gekürzte Form einer rationalen Zahl sollte in „Standardform“ vorliegen (der Nenner sollte immer eine positive Ganzzahl sein).
Wenn ein Nenner mit einer negativen Ganzzahl vorliegt, multipliziere sowohl den Zähler als auch den Nenner mit -1, um die Standardform zu erreichen.
Zum Beispiel sollte 3/-4 zu -3/4 gekürzt werden.
Gehe davon aus, dass die Programmiersprache, die du verwendest, keine Implementierung rationaler Zahlen hat.
Eigenschaften beweisen
In dieser Übung definierst du einen Typ RationalNumber, der eine vollständig gekürzte, gültige rationale Zahl repräsentiert.
Das wird direkt durch eine Eigenschaft erzwungen, die Teil des Typs selbst ist.
Spezifikationen und Einschränkungen direkt auf der Ebene des Typs zu kodieren, macht ungültige Zustände praktisch nicht darstellbar.
Allerdings bedeutet das auch eine zusätzliche Last für dich als Programmierer: Du musst beweisen, dass die Eigenschaft immer gilt.
Dieses Kapitel bietet eine gute Einführung in das Beweisen von Theoremen in Lean.
Für einen tieferen Einblick ist dieses Buch als offizielle Ressource auf der Lean-Website aufgeführt.
Vielleicht möchtest du auch einen Blick in eine Referenz zur Sprache werfen.
