Beweise über Funktionen, die von der Reihenfolge ihrer Alternativen abhängen

Question

Mit einiger Erfahrung in Haskell, habe ich gerade angefangen, Idris für Theoremprüfung zu verwenden. Dies ist ein minimales Beispiel, das ein Problem veranschaulicht, das ich beim Versuch, ziemlich einfache Aussagen zu beweisen, festgestellt habe.

Betrachten wir eine Gesamtfunktion test haben: es

total test : Integer -> Integer 
test 1 = 1 
test n = n 

Natürlich sehen wir, dass die Funktion test n = n vereinfacht werden könnten, aber wir beweisen. Ich werde einfach über alle Fälle:

total lemma_test : (n : Integer) -> test n = n 
lemma_test 1 = Refl 
lemma_test n = Refl 

Aber diese typüberprüft nicht:

Type mismatch between 
     n = n (Type of Refl) and 
     test n = n (Expected type) 

Specifically: 
     Type mismatch between 
       n 
     and 
       test n 

Also, das Problem zu sein scheint, dass Idris nicht für den zweiten Fall von lemma_test ableiten kann dass n ungleich 1 ist und dass auch der zweite Fall von test angewendet werden muss.

Wir können natürlich versuchen, ausdrücklich die Fälle ALL, aufzuzählen, die mühsam sein kann, oder unmöglich machen, wie im Fall für Integer s:

total lemma_test : (n : Integer) -> test n = n 
lemma_test 1 = Refl 
lemma_test 2 = Refl 
lemma_test 3 = Refl 
... 

Gibt es eine Möglichkeit Aussagen wie dies zu beweisen für Funktionen, die nicht über eine endliche Menge von Datenkonstruktoren definiert sind, sondern stattdessen davon abhängen, dass die Mustererkennung von oben nach unten funktioniert, wie in diesem Beispiel test?

Vielleicht gibt es eine ziemlich einfache Lösung, die ich einfach nicht sehe, wenn man bedenkt, dass Funktionen wie diese recht häufig auftreten.

Answer 1

Wie andere gesagt haben, Integer ist primitiv, und nicht eine induktiv definierte Idris Art, daher können wir nicht erschöpfende Muster passen darauf. Genauer gesagt, das Problem ist, dass wir in Idris (und tatsächlich auch in der hochmodernen Agda!) Dinge über "Standard" -Musterübereinstimmungen nicht wirklich beweisen können, weil sie keine Informationen über alle vorherigen Muster enthalten das konnte nicht übereinstimmen. In unserem Fall gibt test n = 1 uns keinen Beweis, dass n ungleich 1 ist.

Die übliche Lösung ist entscheidbar Gleichheit zu verwenden (Boolean Gleichheit könnte auch gut) anstelle von Durchfall:

import Prelude 

%default total 

test : Integer -> Integer 
test n with (decEq n 1) 
    test n | Yes p = 1 
    test n | No p = n 

lemma_test : (n : Integer) -> (test n) = n 
lemma_test n with (decEq n 1) 
lemma_test _ | (Yes Refl) = Refl 
lemma_test n | (No contra) = Refl 

Hier wird das No Ergebnis trägt explizite Aussage über das ausgefallene Spiel.

Answer 2

Ich bin mir nicht sicher, wie Integer definiert ist, oder wie Induktion auf es usw. zu tun, so ist dies keine vollständige Antwort auf Ihre Frage; aber vielleicht wird die Nat Version auch informativ für Sie sein? (Auch, vielleicht bedeutete Sie tatsächlich Nat, da in Ihrem zweiten Beispiel nur Sie die positiven Naturals aufzählen?)

Wenn Sie test ändern Nat s zu verwenden:

total test : Nat -> Nat 
test (S Z) = 1 
test n = n 

dann können Sie Anspruch auf Vollständigkeit Muster tun passende in lemma_test:

total lemma_test : (n : Nat) -> test n = n 
lemma_test (S Z) = Refl 
lemma_test Z = Refl 
lemma_test (S (S k)) = Refl 

Answer 3

Integer nicht in Idris definiert, aber aufschiebt eher zu GMP bigints. Es ist effektiv undurchsichtig für Idris, und anscheinend nicht etwas, was Sie auf diese Weise über Fälle von Kompilierungszeit zu verstehen. Mit etwas wie Nat, das induktiv definiert ist, können Sie über Beweise in Form eines Basisfalls und eines rekursiven Falls sprechen.

Dieser Typ Fehler über n nicht test n sagt Ihnen, dass Idris den Ausdruck test n nicht reduzieren kann. Ich bin mir nicht sicher, ob es sich so verhält - offensichtlich ist es eine totale Funktion, und es soll die Gesamtfunktionen afaik reduzieren. Vielleicht hängt das mit der Undurchsichtigkeit von Integer für Idris zusammen?

Sie können die Reduktion am repl testen, indem Sie die freie Variable als labmda param einbringen. Z.B.\n => test n nur Echos zurück \n => test n : Integer -> Integer (mit nichts geändert), jedoch, wenn Sie den test 1 = 1 Fall aus Ihrer Definition entfernen und versuchen Sie es erneut, es Echos zurück \n => n : Integer -> Integer - es ist test n auf n reduziert. Und dann würde dein Beweis funktionieren wie er ist.