Coq-зависимые типы

Question

Я новичок в Coq и нуждаюсь в некоторой помощи с некоторыми тривиальными примерами, чтобы начать меня. В частности, меня интересует определение некоторых операций векторов (списки фиксированного размера) с использованием зависимых типов. Я начал с пакета Vector и попытался реализовать некоторые дополнительные функции. Например, мне трудно реализовать тривиальные функции «взять» и «отбросить», которые берут или удаляют первые «р» элементы из списка.

Require Import Vector. 

Fixpoint take {A} {n} (p:nat) (a: t A n) : p<=n -> t A p := 
    match a return (p<=n -> t A p) with 
    | cons A v (S m) => cons (hd v) (take m (tl v)) m 
    | nil => fun pf => a 
    end. 

Погрешность (в случае nil) является:

The term "a" has type "t A n" while it is expected to have type "t A p". 

Может кто-нибудь помочь мне с некоторыми исходными точками? Благодаря!

Answer 1

Я не понимаю ваш подход. Вы всегда возвращаете непустой вектор, когда аргумент является непустым вектором, но take должен возвращать nil, когда p=0 независимо от вектора.

Вот один из подходов к строительству take. Вместо того, чтобы использовать гипотезу p <= n, я выражаю длину аргумента n как сумму числа p элементов, которые нужно взять, и количество обратных элементов m, что возможно, если p <= n. Это позволяет упростить рекурсивное определение, поскольку (S p') + m структурно равно S (p' + m). Обратите внимание, что дискриминация зависит от количества элементов: return nil, если принимать 0, вернуть cons head new_tail в противном случае.

Эта версия функции take имеет требуемое вычислительное поведение, поэтому все, что осталось, это определить ее с нужным содержимым. Я использую функцию Program, чтобы сделать это удобно: заполните вычислительный контент (тривиальный, мне просто нужно сказать, что я хочу использовать m = n - p), а затем выполнить обязательства по доказательству (которые являются простой арифметикой).

Require Import Arith. 
Require Import Vector. 

Fixpoint take_plus {A} {m} (p:nat) : t A (p+m) -> t A p := 
    match p return t A (p+m) -> t A p with 
    | 0 => fun a => nil _ 
    | S p' => fun a => cons A (hd a) _ (take_plus p' (tl a)) 
    end. 
Program Definition take A n p (a : t A n) (H : p <= n) : t A p := 
      take_plus (m := n - p) p a. 
Solve Obligations using auto with arith. 

---

Для вашего newdrop : forall A n p, t A n -> p <= n -> t A (n-p) следующий подход работает. Вам нужно помочь Coq, сообщив ему, что p и n станут в рекурсивном звонке.

Program Fixpoint newdrop {A} {n} p : t A n -> p <= n -> t A (n-p) := 
    match p return t A n -> p <= n -> t A (n-p) with 
    | 0 => fun a H => a 
    | S p' => fun a H => newdrop p' (tl a) (_ : p' <= n - 1) 
    end. 
Next Obligation. 
omega. 
Qed. 
Next Obligation. 
omega. 
Qed. 
Next Obligation. 
omega. 
Qed. 
Next Obligation. 
omega. 
Qed. 

Я не знаю, почему Solve Obligations using omega. не работает, но решение каждого обязательства индивидуально работает.