Tell abhängige Funktion in bedingten Anweisung Zweig, die Bedingung ist wahr

Question

Ich habe eine Funktion mit einem Typ Unterschrift (x, y : SomeType) -> (cond x y) = True -> SomeType. Wenn ich die Bedingung in if-then-else/case/with-Anweisung überprüfe, wie übertrage ich die Funktion in einem entsprechenden Zweig die Tatsache, diese Bedingung ist wahr?

Answer 1

können Sie DecEq verwenden, um dies einfach zu machen:

add : (x, y : Nat) -> x + y < 10 = True -> Nat 
add x y _ = x + y 

main : IO() 
main = 
    let x = S Z 
    in let y = Z 
    in case decEq (x + y < 10) True of 
      Yes prf => print (add x y prf) 
      No _ => putStrLn "x + y is not less than 10" 

Aber Sie sollten nicht.

Mit booleans (via = oder So) kann Ihnen sagen, dass etwas wahr ist, aber nicht warum. Die warum ist sehr wichtig, wenn Sie Proofs zusammen komponieren oder auseinander brechen wollen. Stellen Sie sich vor, add genannt eine Funktion, die benötigt x + y < 20 - wir können nicht nur unseren Beweis, dass x + y < 10 = True übergeben, weil Idris nichts über die Operation weiß, nur dass es wahr ist.

Stattdessen sollten Sie das obige mit einem Datentyp schreiben, der enthält, warum es stimmt. LTE ist ein Typ, der macht das für weniger als Vergleiche:

add : (x, y : Nat) -> LTE (x + y) 10 -> Nat 
add x y _ = x + y 

main : IO() 
main = 
    let x = S Z 
    in let y = Z 
    in case isLTE (x + y) 10 of 
      Yes prf => print (add x y prf) 
      No _ => putStrLn "x + y is not less than 10" 

Wenn nun add eine Funktion, die ein LTE (x + y) 20 Bedarf aufgerufen wir eine Funktion schreiben, kann die Einschränkung zu erweitern:

widen : a `LTE` b -> (c : Nat) -> a `LTE` (b + c) 
widen LTEZero c = LTEZero 
widen (LTESucc x) c = LTESucc (widen x c) 

Dies ist Nicht etwas, was wir einfach mit Booleans machen können.