Mix von Bool und Datatypes.bool nach Import erforderlich Omega

Question

Ich gehe durch Software-Grundlagen und lief in einen Fehler.

ERROR: Der Begriff "true" hat "Bool" geben, während es Typen "Datatypes.bool" unter

für den Beweis haben, wird erwartet.

Theorem beq_nat_true : forall n m, 
    beq_nat n m = true -> n = m. 

Ich fand heraus, dass dies passiert, wenn ich Require Import Omega verwende.
Irgendwelche Tipps, Vorschläge oder Erklärungen was Omega in die Umwelt einführt?

Answer 1

Das Modul Omega importiert indirekt viele Definitionen der Standardbibliothek, die natürliche Zahlen manipulieren, von denen einige Teile von Software Foundations überschatten. Die beq_nat Funktion ist eine von ihnen. Das Problem tritt auf, weil die Version der Standardbibliothek für beq_nat Standard booleans zurückgibt, während die Version von SF seine redefined booleans zurückgibt.

Wir haben dieses Problem vor einer Weile bemerkt, und haben es bereits in current version behoben. Wenn Sie nicht alles neu herunterladen möchten (oder wenn Sie selbst Omega importiert haben), können Sie auch einfach beq_nat qualifizieren, um die richtige Version zu verwenden. Meine Vermutung ist, dass Basics.beq_nat sollte funktionieren.