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) 

これは、その後、ソートされたリストについて推論するために使用することができます。

コックでは、1にも機能Fixpoint is_sorted: {A: Type} (l: List A) : boolを書き、その後、is_sortedの定義するunfoldことで、物事を証明するためにis_sorted someList = trueのようなタイプを使用することができます。この後者のアプローチはIdrisで可能ですか、それとも前のアプローチだけをサポートしていますか？

さらに、私自身の理解のために、後者の場合は「反映による証明」の例であり、前者の方が後者の方が好ましいと思われる状況はありますか？

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 

重要な詳細は、お使いの関数定義は、簡単な設定されている場合ということです必要ならば、統一は幾分魔法のようにもう一方の方程式の片方を置き換えるでしょう。 （私は、論理的な「及び」オペレータの少ない効率的な非短絡バージョンを使用する標準的な「その後、他/ /場合は、」事業者は怠惰の合併症を紹介。「&は&」または理由）

理想的には、いくつかの簡単ながあるはずです「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