взаимная рекурсия по индуктивному типу и нат - PullRequest
Новая
       19

взаимная рекурсия по индуктивному типу и нат

0 голосов
/ 23 мая 2018

Рассмотрим этот пример: 

Inductive T :=
| foo : T
| bar : nat -> T -> T.

Fixpoint evalT (t:T) {struct t} : nat :=
  match t with
  | foo => 1
  | bar n x => evalBar x n
  end
with evalBar (x:T) (n:nat) {struct n} : nat :=
  match n with
  | O => 0
  | S n' => (evalT x) + (evalBar x n')
  end.

Coq отклоняет его с ошибкой: Рекурсивный вызов evalBar имеет главный аргумент, равный "n" вместо "x" .

Я понимаю, что проверка завершения была сбита с толку двумя не связанными индуктивными типами (T и nat).Однако похоже, что функция, которую я пытаюсь определить, действительно прекратит работу.Как я могу заставить Coq принять это?

Ответы [ 2 ]

0 голосов
/ 23 мая 2018

Другое решение заключается в использовании вложенной точки фиксации. 

Fixpoint evalT (t:T) {struct t} : nat :=
  match t with
  | foo => 1
  | bar n x => let fix evalBar n {struct n} :=
                 match n with
                 | 0 => 0
                 | S n' => Nat.add (evalT x) (evalBar n')
                 end
               in evalBar n
  end.

Важным моментом является удаление аргумента x из evalBar.Таким образом, рекурсивный вызов evalT выполняется для x из bar n x, а не x, заданного в качестве аргумента для evalBar, и, таким образом, средство проверки завершения может проверить определение evalT.

Это та же идея, которая заставляет работать версию с nat_rec, предложенную в другом ответе.

0 голосов
/ 23 мая 2018

Я нашел одно решение - использовать nat_rec вместо evalBar: 

Fixpoint evalT (t:T) {struct t} : nat :=
  match t with
  | foo => 1
  | bar n x => @nat_rec _ 0 (fun n' t' => (evalT x) + t') n
  end.

Это работает, но я бы хотел скрыть nat_rec в evalBar определении, чтобы скрыть детали.В моем реальном проекте такая конструкция используется несколько раз.

...