Как убедить Идриса в длине вектора

Question

Просто начинайте в Идрисе (это Идрис 2, если это имеет значение), и натыкайтесь на эту проблему. Я пытаюсь реализовать функцию, которая возвращает вектор всех чисел Фибоначчи до заданного n. Вот определение до сих пор (оно не компилируется):

fibs : (n : Nat) -> Vect (n + 1) Int
fibs Z = [0]
fibs (S Z) = [0, 1]
fibs (S k) =
    case (fibs k) of
        (x :: y :: xs) => (x + y) :: x :: y :: xs

Я получаю следующую ошибку:

Can't solve constraint between:
    S (S ?len)
and
    plus ?_ (fromInteger 1)

Ошибка указывает на выражение (x :: y :: xs).

Я понимаю, что нужно доказать Идрису, что длина fibs k будет как минимум 2, но я не понимаю, как это сделать, и почему это не очевидно из существующих определений. Для меня это выглядит так: k в fibs (S k) обязательно должно быть> = 1, потому что в противном случае либо fibs Z, либо fibs (S Z) будет соответствовать. Следовательно, длина fibs k, где k >= 1 должна быть> = 2, по определению fibs : (n : Nat) -> Vect (n + 1) Int. Чего мне не хватает и как express это в Идрисе?

Answer 1

Сначала 1 + n легче рассуждать о проверке типов, чем n + 1, поскольку шаблон plus соответствует левой стороне:

> :printdef plus
plus : Nat -> Nat -> Nat
plus 0 right = right
plus (S left) right = S (plus left right)

Так что n + 1 в определении типа не может быть уменьшается без знания n, в то время как 1 + n может быть уменьшено до S n.

С этим одним компилируется fibs. Но если вы хотите проверить, является ли функция итоговой, вы получите:

> :total fibs
Main.fibs is possibly not total due to:
Main.case block in fibs at test.idr:7:10-17, which is not total as there are missing cases

Поскольку средство проверки типов не просматривает другие предложения, оно не знает, что fibs (S Z) уже обрабатывается в другом месте. Таким образом, в fibs (S k) = case (fibs k) of … k может быть Z, а затем результат Vect (S Z), который не обрабатывается в переключателе регистра.

Но исправление так же просто, как первый, просто сопоставление с образцом на S (S k):

fibs (S (S k)) = case (fibs (S k)) of
    (x :: y :: xs) => (x + y) :: x :: y :: xs