2016-04-07 14 views
2

Die folgende Funktion erstellt:Verständnis `k: Nat ** 5 * k = n 'Signature

onlyModByFive : (n : Nat) -> (k : Nat ** 5 * k = n) -> Nat 
onlyModByFive n k = 100 

Aber was bedeutet k repräsentiert mit ihrer Nat ** 5 * k = n Syntax?

Auch, wie kann ich es nennen? Hier ist, was ich versucht habe, aber ich verstehe die Ausgabe nicht.

*Test> onlyModByFive 5 5 
When checking an application of function Main.onlyModByFive: 
     (k : Nat ** plus k (plus k (plus k (plus k (plus k 0)))) = 5) is not a 
     numeric type 

Quelle der Antwort - https://groups.google.com/d/msg/idris-lang/ZPi9wCd95FY/eo3tRijGAAAJ

Antwort

5

(k : Nat) ** (5 * k = n) ist ein abhängiges Paar

bestehend
  • Ein erstes Element k : Nat
  • Ein zweites Element prf : 5 * k = n

Mit anderen Worten Dies ist ein existentieller Typ, der besagt: "Es gibt einige k : Nat, so dass 5 * k = n". Um konstruktiv zu sein, müssen Sie eine solche k und einen Beweis geben, dass es tatsächlich 5 * k = n erfüllt.

In Ihrem Beispiel, wenn Sie teilweise onlyModByFive-5 anwenden, erhalten Sie etwas vom Typ

onlyModModByFive 5 : ((k : Nat) ** (5 * k = 5)) -> Nat 

so das zweite Argument des Typs (k : Nat) ** (5 * k = 5) sein muss. Es gibt nur eine Wahl von k können wir hier machen, indem sie sie zu 1 Einstellung, und beweisen, dass 5 * 1 = 5:

foo : Nat 
foo = onlyModByFive 5 (1 ** Refl) 

Dies funktioniert, weil 5 * 1-5 reduziert, so haben wir 5 = 5 zu beweisen, was trivialerweise getan werden kann, unter Verwendung von Refl : a = a direkt (vereinheitlichen a ~ 5).

+0

Danke, Kaktus. Aber ich denke, dass mein def von 'onlyModByFive' ​​ungültig ist, da es überhaupt keinen' mod' beinhaltet, nein? Ich fragte dieses Follow-up: http://stackoverflow.com/questions/36531852/function-to-determinine-if-nat-is-divisible-by-5-at-compile-time. –

+0

Auch - könnten Sie bitte irgendwelche Lesungen auf der Beweis bezogenen 'Refl 'empfehlen, die Sie notiert hatten? –

+2

@KevinMeredith könnten Sie beginnen, indem Sie lesen http://jozefg.bitbucket.org/posts/2014-08-06-equality.html und zur Kenntnis nehmen, dass wir hier über intensional propositional Gleichheit sprechen. – Cactus