Koşullu deyim dalında bağımlı işlevi söyle o koşul doğru

Question

(x, y : SomeType) -> (cond x y) = True -> SomeType imzalı bir işleve sahibim. If-then-else/case/with ifadesindeki durumu kontrol ettiğimde, ilgili bir branştaki fonksiyona nasıl geçebilirim, bu koşul doğru mu?

Answer 1

Bunu kolayca yapmak için DecEq kullanabilirsiniz:

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" 

Ama atlatma.

Booleanları kullanmak (= veya So aracılığıyla), bir şeyin doğru olduğunu bildirebilir, ancak neden. Kanıtları bir araya getirmek ya da parçalamak istiyorsanız, niçin çok önemlidir. add'un x + y < 20 numaralı bir fonksiyona ihtiyaç duyduğunu düşünün. x + y < 10 = True'un ispatını geçemeyiz, çünkü İdris yalnızca bu işlem hakkında hiçbir şey bilmiyor, sadece bu doğru. Bunun yerine, nedeninin neden olduğunu doğru bir şekilde yazmanız gerekir. LTE daha az-daha karşılaştırmalar için yapan bir türüdür: Artık

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" 

, add bir LTE (x + y) 20 biz kısıtlamasını genişletmek için bir işlev yazabilirsiniz gerekli bir işlev çağrılırsa:

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

budur sadece boole ile yapabileceğimiz bir şey değil.