再帰型のネストされたコンストラクタ内の証明

Question

以下のコードで問題が発生しています。基本的にスライスタイプを作りたいと思っています。動機づけはPythonから来ており、スライスは[start:end:step]であり、リストからサブリストをスライスするために使用されます。これは、概念的には、インデックスのシーケンスと同じである[start, start+step, start+2*step, ..., end]です。

私がそれをキャプチャしようとした方法はSlice nはVect (n+m) aに適用できます。基本コンストラクタFwdSは、非ゼロステップ（証明ステップNZ）のスライスを作成します。 SLenコンストラクタは、既存のスライスのVectサイズ要件をstep（​​を使用して計算）だけインクリメントします。スライスが[start:stop:step]場合

start := # of SStart in slice 
stop := start + (# of SLen) * step 
step := constructor argument in FwdS 

：同様SStart 1.

によってスライスのVectサイズ要件は、最終的な値は、概念的に対応するインクリメント。

mutual 
    data Slice : Nat -> Type where 
    FwdS : (step : Nat) -> {stepNZ : Not (step = Z)} -> Slice Z 
    SLen : (x : Slice len) -> Slice (len + (stepOf x)) 
    SStart : Slice len -> Slice (S len) 

    stepOf : Slice n -> Nat 
    stepOf (FwdS step) = step 
    stepOf (SLen slice) = stepOf slice 
    stepOf (SStart slice) = stepOf slice 

length : Slice n -> Nat 
length (FwdS step) = Z 
length (SLen slice) = let step = stepOf slice 
          len = length slice 
         in len + step 
length (SStart slice) = length slice 

select : (slice: Slice n) -> Vect (n+m) a -> Vect (length slice) a 
select (FwdS step) xs   = [] 
select (SStart slice) (x :: xs) = select slice xs 
select (SLen slice) (xs)  = ?trouble 

トラブルは最後のパターンです。問題が何であるかわからない - xsで分割を試みると、[]と(_::_)の両方が不可能になる。

select (SLen slice) (x :: xs) = let rec = drop (stepOf slice) (x::xs) 
           in x :: (select slice rec) 

とイドリスは、最初の引数がSLenコンストラクタであれば、2番目の引数は[]できないことを認識してい：理想的には私は、その場合にはこのような何かを読んでいるしたいと思います。私の直感は、SLenレベルで、IdrisはそれがすでにstepOf sliceがZではないという証拠を持っていることを理解していません。しかし、私はそのアイデアをどのようにテストするのかは分かりません。

Answer 1

私の直感はすでにSLENレベルで、イドリスはそれを理解していないということですstepOfスライスがZ.

あなたが正しいではないことを証明しています。 stepOf sliceがgetPrf : (x : Slice n) -> (k ** stepOf x = (S k))のようないくつかのkためS kであることの証明を取得し、その後：:t troubleを使用すると、コンパイラは(plus (plus len (stepOf slice)) m)は、次の2つの問題を解決しなければならない0

a : Type 
    m : Nat 
    len : Nat 
    slice : Slice len 
    xs : Vect (plus (plus len (stepOf slice)) m) a 
-------------------------------------- 
trouble : Vect (plus (length slice) (stepOf slice)) a 

ではないことを推測するのに十分な情報を持っていないことを確認しますVect (plus (plus len (stepOf slice)) m) aをVect (S (plus k (plus len m))) aのようなものに書き直すので、コンパイラは少なくともこのxsが空ではないことを知ることができます。しかし、そこからは簡単にはなりません。 :-)

基本的に、引数に関数を使用する関数がある場合は、それらの情報を型に書き換えることができます。 selectのように、length sliceまたはSLenをstepOf xとします。ここでの実装例です：

data Slice : (start : Nat) -> (len : Nat) -> (step : Nat) -> (cnt : Nat) -> Type where 
    FwdS : (step : Nat) -> Slice Z Z step Z 
    SLen : Slice Z len step cnt -> Slice Z (S step + len) step (S cnt) 
    SStart : Slice start len step cnt -> Slice (S start) len step cnt 

あなたがこのことから多くを得る：あなたは、最初の関数lengthと​​を証明することなく、直接パラメータlenとstepにアクセスすることができます。また、許可されたデータをより詳細に管理することもできます。たとえば、あなたの定義では、SLen $ SStart $ SLen $ SStart $ FwdS 3が有効で、ステップをミックスして増分を開始します。

selectは、次のようになります。

select : Slice start len step cnt -> Vect (start + len + m) a -> Vect cnt a 
select (FwdS k) xs = [] 
select (SStart s) (x :: xs) = select s xs 
select (SLen s) [] impossible 
select (SLen s {step} {len} {cnt}) (x::xs) {m} {a} = 
    let is = replace (sym $ plusAssociative step len m) xs {P=\t => Vect t a} in 
    (x :: select s (drop step is)) 

あなたが証明して運動をしたい場合は、あなたがそうstart + lenを切り替え、select : Slice start len step cnt -> Vect (len + start + m) a -> Vect cnt aを実装しようとすることができます。 4のステップで1から始まる

となって二つの要素：

> select (SStart $ SLen $ SLen $ FwdS 3) [0,1,2,3,4,5,6,7,8,9] 
[1, 5] : Vect 2 Integer