Idris是否支持展開函數定義？

Question

對於從屬類型，它可以定義一個感應式的有序列表，例如：

data IsSorted : {a: Type} -> (ltRel: (a -> a -> Type)) -> List a -> Type where 
    IsSortedZero : IsSorted {a=a} ltRel Nil 
    IsSortedOne : (x: a) -> IsSorted ltRel [x] 
    IsSortedMany : (x: a) -> (y: a) -> .IsSorted rel (y::ys) -> .(rel x y) -> IsSorted rel (x::y::ys) 

這可以被用來推理排序的列表。

在勒柯克，人們也可以編寫一個函數Fixpoint is_sorted: {A: Type} (l: List A) : bool，然後利用一種類似is_sorted someList = true來證明的東西，由荷蘭國際集團unfold的is_sorted定義。伊德里斯可能採用後一種方法，還是僅支持前一種方法？

此外，爲了我自己的理解：後一種情況是「反思證明」的一個例子，是否存在後一種方法比前者更可取的情況？

Answer 1

我認爲部分下面的你想要做什麼（我會補充一點，我沒有使用勒柯克的經驗告誡）：

infixl 4 & 

(&) : Bool -> Bool -> Bool 
(&) True True = True 
(&) _ _ = False 

elim_and : x & y = True -> (x = True, y = True) 
elim_and {x = False} {y = False} x_and_y_is_true = (x_and_y_is_true, x_and_y_is_true) 
elim_and {x = False} {y = True} x_and_y_is_true = (x_and_y_is_true, Refl) 
elim_and {x = True} {y = False} x_and_y_is_true = (Refl, x_and_y_is_true) 
elim_and {x = True} {y = True} x_and_y_is_true = (Refl, Refl) 

is_sorted : {a: Type} -> (ltRel: a -> a -> Bool) -> List a -> Bool 
is_sorted ltRel [] = True 
is_sorted ltRel (x :: []) = True 
is_sorted ltRel (x :: y :: xs) = (ltRel x y) & (is_sorted ltRel (y :: xs)) 

is_sorted_true_elim : {x : a} -> is_sorted ltRel (x :: y :: xs) = True -> (ltRel x y = True, 
                      is_sorted ltRel (y :: xs) = True) 
is_sorted_true_elim {x} {y} {xs} {ltRel} is_sorted_x_y_xs = elim_and is_sorted_x_y_xs 

重要細節是，如果你的函數定義是一組簡單的方程式，那麼當需要時，統一將有點神奇地用等式的一邊代替另一邊。 （I使用的邏輯「與」操作者的效率較低的非短路的版本，因爲標準的「& &」或「如果/ THEN/ELSE」運營商介紹懶惰的併發症。）

在理想情況下，應該有一些簡單的方式展開定義，包括'與'基於模式匹配，但我不知道如何使這項工作，例如：

is_sorted : {a: Type} -> (ltRel: a -> a -> Bool) -> List a -> Bool 
is_sorted ltRel [] = True 
is_sorted ltRel (x :: []) = True 
is_sorted ltRel (x :: y :: xs) with (ltRel x y) 
    | True = is_sorted ltRel (y :: xs) 
    | False = False 

is_sorted_true_elim : {x : a} -> is_sorted ltRel (x :: y :: xs) = True -> (ltRel x y = True, 
                      is_sorted ltRel (y :: xs) = True) 
is_sorted_true_elim {x} {y} {xs} {ltRel} is_sorted_x_y_xs with (ltRel x y) proof x_lt_y_value 
    | True = ?hole 
    | False = ?hole2