Primitive Operationen in Beweisen

Question

Für lernabhängige Typen, schreibe ich mein altes Haskell-Spiel in Idris um. Derzeit verwendet das Spiel "engine" integrierte Typen wie Word8. Ich würde einige Lemmas beweisen wollen, die numerische Eigenschaften dieser Zahlen beinhalten (so wie die doppelte Negation eine Identität ist). Es ist jedoch nicht möglich, etwas über das Verhalten primitiver arithmetischer Operationen zu sagen. Was wäre besser, einfach believe_me oder andere Handwaving zu verwenden (zumindest für die grundlegendsten Eigenschaften), oder meinen Code mit Nat, Fin und anderen "high-level" numerischen Typen umzuschreiben?

Answer 1

Ich würde vorschlagen, postulate für jede der primitiven Eigenschaften, die Sie benötigen, vorsichtig zu sein, nur Dinge zu verwenden, die tatsächlich für die fraglichen numerischen Typen natürlich gelten (was im Grunde nur bedeutet, vorsichtig mit Überlauf). So kann man sagen Dinge wie:

postulate add_commutes : (x, y : Int) -> x + y = y + x 

believe_me wird am besten vermieden werden, wenn Sie einige Rechenverhalten des Beweises bedarf. Aber, um ehrlich zu sein, wir versuchen immer noch, diese Sachen auszuarbeiten, wenn wir über Primitive nachdenken ...

Answer 2

Ich glaube für den Moment ist es im Allgemeinen besser, Nat zu verwenden, wenn Sie können. Die Idris-Entwickler planen schließlich, einen allgemeinen Mechanismus zum Ersetzen proof-freundlicher Typen durch schnelle primitive in der Kompilierung zu implementieren, aber im Moment passiert das nur für Nat. Sie könnten believe_me durch, wenn Sie wirklich wollten, aber Sie würden mit Funktionen enden, die nicht so einfach in Proofs arbeiten. Beachten Sie, dass, wenn Sie sich entscheiden, mit believe_me zu spielen, sollten Sie auch really_believe_me betrachten, die es scheinbar glaubwürdiger zum Typüberprüfer macht.