Proof inside nested constructor of recursive type

Question

I am having some trouble with the code below. Essentially I want to create a slice type. The motivation comes from Python, where a slice is [start:end:step], used for slicing a sublist out of a list. This is conceptually the same as a sequence of indices [start, start+step, start+2*step, ..., end].

The way I've tried to capture it is Slice n can be applied to a Vect (n+m) a. The basic constructor FwdS will create a slice with a non-zero step (proof stepNZ). The SLen constructor will increment an existing slice's Vect size requirement by its step (computed using stepOf). Similarly SStart increments a slice's Vect size requirement by 1.

Then the final value conceptually corresponds to:

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

If the slice is [start:stop:step].

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

The trouble is in the last pattern. I'm not sure what the issue is - if I try to case split on xs I get both [] and (_::_) impossible. Ideally I'd like to have that case read something like this:

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

and have Idris recognize that if the first argument is an SLen constructor, the second argument cannot be []. My intuition is that at the SLen level, Idris does not understand it already has a proof that stepOf slice is not Z. But I'm not sure how to test that idea.

xash xash · Accepted Answer · 2018-02-07T07:05:07

My intuition is that at the SLen level, Idris does not understand it already has a proof that stepOf slice is not Z.

You are right. With :t trouble you see that the compiler doesn't have enough information to infer that (plus (plus len (stepOf slice)) m) is not 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

You would have to solve two problems: get a proof that stepOf slice is S k for some k like getPrf : (x : Slice n) -> (k ** stepOf x = (S k)), then rewrite Vect (plus (plus len (stepOf slice)) m) a to something like Vect (S (plus k (plus len m))) a so the compiler can at least know that this xs is not empty. But it doesn't get easier from thereon. :-)

Basically whenever you have a function where you use functions in the arguments, you probably can rewrite those informations into the type. Like select with length slice or SLen with stepOf x. Here is an example implementation:

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

You gain a lot from this: you can access the parameters len and step directly without proving the functions length and stepOf first. Also you can have better control about your allowed data. For example, in your definiton SLen $ SStart $ SLen $ SStart $ FwdS 3 would have been valid, mixing steps and start increments.

select could look like this:

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))

If you want an exercise with proving, you could try to implement select : Slice start len step cnt -> Vect (len + start + m) a -> Vect cnt a, so switching start + len.

And getting two elements starting at 1 in steps of 4:

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

Proof inside nested constructor of recursive type

1 Answers