재귀 유형의 중첩 생성자 내부에있는 증명

Question

아래 코드를 사용하는 데 문제가 있습니다. 본질적으로 슬라이스 유형을 만들고 싶습니다. 동기 부여는 Python에서 이루어지며 슬라이스는 [start:end:step]이며 목록에서 하위 목록을 분할하는 데 사용됩니다. 이것은 개념적으로 일련의 인덱스 인 [start, start+step, start+2*step, ..., end]과 같습니다.

캡처하려고 시도한 방식은 Slice n이며 Vect (n+m) a에 적용 할 수 있습니다. 기본 생성자 FwdS은 0이 아닌 단계 (증명 단계 NZ)로 슬라이스를 만듭니다. SLen 생성자는 기존 슬라이스의 Vect 크기 요구 사항을 step (stepOf을 사용하여 계산)만큼 증가시킵니다. 슬라이스가 [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.

자네 말이 맞아 아니라는 것을 증명을 가지고 있습니다. 다음, getPrf : (x : Slice n) -> (k ** stepOf x = (S k)) 같은 몇 가지 k에 대한 stepOf slice이 S k임을 증명을 얻을 : :t trouble 사용하면 컴파일러가 (plus (plus len (stepOf slice)) m) 것을 추론 할 수있는 충분한 정보가없는 것을 알 수 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 및 stepOf 첫째를 제공하지 않고 매개 변수 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