#coq
#coq
Вопрос:
Я пытаюсь изменить вектор в Coq. Моя реализация заключается в следующем:
Fixpoint vappend {T : Type} {n m} (v1 : vect T n) (v2 : vect T m) : vect T (plus n m) := match v1 in vect _ n return vect T (plus n m) with | vnil =gt; v2 | x ::: v1' =gt; x ::: (vappend v1' v2) end. Theorem plus_n_S : forall n m, plus n (S m) = S (plus n m). Proof. intros. induction n; auto. - simpl. rewrite lt;- IHn. auto. Qed. Theorem plus_n_O : forall n, plus n O = n. Proof. induction n. - reflexivity. - simpl. rewrite IHn. reflexivity. Qed. Definition vreverse {T : Type} {n} (v : vect T n) : vect T n. induction v. - apply [[]]. - rewrite lt;- plus_n_O. simpl. rewrite lt;- plus_n_S. apply (vappend IHv (t ::: [[]])). Show Proof. Defined. Проблема в том, что когда я пытаюсь вычислить функцию, она выдает что-то вроде:
match plus_n_O (S (S O)) in (_ = y) return (vect nat y) with ... и не смог продвинуться дальше. В чем здесь проблема? Как я могу это исправить?
Комментарии:
1. Какое именно выражение вы пытаетесь вычислить?
2. На самом деле любое выражение, которое не является пустым, например O ::: O ::: [[]]
Ответ №1:
Проблема в том, что ваши функции используют непрозрачные доказательства, plus_n_S и plus_n_O . Чтобы вычислить vreverse , вам нужно вычислить эти доказательства, и если они непрозрачны, вычисление будет заблокировано.
Вы можете устранить эту проблему, прозрачно определив функции. Лично я предпочитаю при этом не использовать режим доказательства, так как легче видеть, что происходит. (Здесь я использовал определение векторов в стандартной библиотеке.)
Require Import Coq.Vectors.Vector. Import VectorNotations. Fixpoint vappend {T : Type} {n m} (v1 : t T n) (v2 : t T m) : t T (plus n m) := match v1 in t _ n return t T (plus n m) with | [] =gt; v2 | x :: v1' =gt; x :: vappend v1' v2 end. Fixpoint plus_n_S n m : n S m = S (n m) := match n with | 0 =gt; eq_refl | S n =gt; f_equal S (plus_n_S n m) end. Fixpoint plus_n_O n : n 0 = n := match n with | 0 =gt; eq_refl | S n =gt; f_equal S (plus_n_O n) end. Fixpoint vreverse {T : Type} {n} (v : t T n) : t T n := match v in t _ n return t T n with | [] =gt; [] | x :: v =gt; eq_rect _ (t T) (eq_rect _ (t T) (vappend (vreverse v) [x]) _ (plus_n_S _ 0)) _ (f_equal S ( plus_n_O _)) end. Compute vreverse (1 :: 2 :: 3 :: []).