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)

这可以用来推理排序列表。

在 Coq 中，也可以编写一个函数Fixpoint is_sorted: {A: Type} (l: List A) : bool，然后利用is_sorted someList = true 之类的类型来证明事情，通过unfold 定义is_sorted。后一种方法在 Idris 中是否可行，还是仅支持前一种方法？

此外，就我自己的理解而言：后一种情况是否是“反射证明”的示例，是否存在后一种方法比前一种方法更可取的情况？

Answer 1

我认为以下部分可以满足您的需求（我会补充一点，我没有使用 Coq 的经验）：

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

重要的细节是，如果您的函数定义是一组简单的方程，那么在需要时，统一会在某种程度上神奇地用方程的一侧替换另一侧。 （我使用了效率较低的非短路版本的逻辑“and”运算符，因为标准的“&&”或“if/then/else”运算符引入了懒惰的复杂性。）

理想情况下，应该有一些直接的方法来展开定义，包括基于 'with' 的模式匹配，但我不知道如何使其工作，例如：

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